Commit 2024-07-01 10:39 8ed158e6

View on Github →

style(Mathlib/Tactic/*): rename wrongly capitalized filenames (#13279) Mathlib.Tactic.CongrmMathlib.Tactic.CongrM Mathlib.Tactic.ExistsiMathlib.Tactic.ExistsI Mathlib.Tactic.Widget.CongrmMathlib.Tactic.Widget.CongrM Mathlib.Tactic.Widget.GcongrMathlib.Tactic.Widget.GCongr Also, we rename the namespaces and subroutines in these files.

Estimated changes