chore: tidy various files (#3233)

leanprover-community · Apr 2, 2023 · bb7d4c7 · bb7d4c7
1 parent 1c65b42
commit bb7d4c7
Show file tree

Hide file tree

Showing 11 changed files with 131 additions and 123 deletions.
diff --git a/Mathlib/Analysis/Convex/Extreme.lean b/Mathlib/Analysis/Convex/Extreme.lean
@@ -42,7 +42,7 @@ See chapter 8 of [Barry Simon, *Convexity*][simon2011]
 
 Prove lemmas relating extreme sets and points to the intrinsic frontier.
 
-More not-yet-PRed stuff is available on the branch `sperner_again`.
+More not-yet-PRed stuff is available on the mathlib3 branch `sperner_again`.
 -/
 
 
@@ -63,7 +63,7 @@ def IsExtreme (A B : Set E) : Prop :=
 #align is_extreme IsExtreme
 
 /-- A point `x` is an extreme point of a set `A` if `x` belongs to no open segment with ends in
-`A`, except for the obvious `open_segment x x`. -/
+`A`, except for the obvious `openSegment x x`. -/
 def Set.extremePoints (A : Set E) : Set E :=
   { x ∈ A | ∀ ⦃x₁⦄, x₁ ∈ A → ∀ ⦃x₂⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x }
 #align set.extreme_points Set.extremePoints

diff --git a/Mathlib/CategoryTheory/Elements.lean b/Mathlib/CategoryTheory/Elements.lean
@@ -56,7 +56,7 @@ lemma Functor.Elements.ext {F : C ⥤ Type w} (x y : F.Elements) (h₁ : x.fst =
   cases x
   cases y
   cases h₁
-  simp at h₂
+  simp only [eqToHom_refl, FunctorToTypes.map_id_apply] at h₂
   simp [h₂]
 
 /-- The category structure on `F.Elements`, for `F : C ⥤ Type`.
@@ -135,8 +135,7 @@ theorem map_π {F₁ F₂ : C ⥤ Type w} (α : F₁ ⟶ F₂) : map α ⋙ π F
 #align category_theory.category_of_elements.map_π CategoryTheory.CategoryOfElements.map_π
 
 /-- The forward direction of the equivalence `F.Elements ≅ (*, F)`. -/
-def toStructuredArrow : F.Elements ⥤ StructuredArrow PUnit F
-    where
+def toStructuredArrow : F.Elements ⥤ StructuredArrow PUnit F where
   obj X := StructuredArrow.mk fun _ => X.2
   map {X Y} f := StructuredArrow.homMk f.val (by funext; simp [f.2])
 
@@ -160,8 +159,7 @@ theorem to_comma_map_right {X Y} (f : X ⟶ Y) : ((toStructuredArrow F).map f).r
   CategoryTheory.CategoryOfElements.to_comma_map_right
 
 /-- The reverse direction of the equivalence `F.Elements ≅ (*, F)`. -/
-def fromStructuredArrow : StructuredArrow PUnit F ⥤ F.Elements
-    where
+def fromStructuredArrow : StructuredArrow PUnit F ⥤ F.Elements where
   obj X := ⟨X.right, X.hom PUnit.unit⟩
   map f := ⟨f.right, congr_fun f.w.symm PUnit.unit⟩
 #align category_theory.category_of_elements.from_structured_arrow
@@ -203,8 +201,8 @@ def toCostructuredArrow (F : Cᵒᵖ ⥤ Type v) : F.Elementsᵒᵖ ⥤ Costruct
   obj X := CostructuredArrow.mk ((yonedaSections (unop (unop X).fst) F).inv (ULift.up (unop X).2))
   map f := by
     fapply CostructuredArrow.homMk
-    . exact f.unop.val.unop
-    . ext Z
+    · exact f.unop.val.unop
+    · ext Z
       funext y
       dsimp
       simp only [FunctorToTypes.map_comp_apply, ← f.unop.2]
@@ -215,16 +213,14 @@ def toCostructuredArrow (F : Cᵒᵖ ⥤ Type v) : F.Elementsᵒᵖ ⥤ Costruct
 given by `CategoryTheory.yonedaEquiv`.
 -/
 @[simps]
-def fromCostructuredArrow (F : Cᵒᵖ ⥤ Type v) : (CostructuredArrow yoneda F)ᵒᵖ ⥤ F.Elements
-    where
+def fromCostructuredArrow (F : Cᵒᵖ ⥤ Type v) : (CostructuredArrow yoneda F)ᵒᵖ ⥤ F.Elements where
   obj X := ⟨op (unop X).1, yonedaEquiv.1 (unop X).3⟩
   map {X Y} f :=
     ⟨f.unop.1.op, by
       convert (congr_fun ((unop X).hom.naturality f.unop.left.op) (𝟙 _)).symm
       simp only [Equiv.toFun_as_coe, Quiver.Hom.unop_op, yonedaEquiv_apply, types_comp_apply,
         Category.comp_id, yoneda_obj_map]
-      have : yoneda.map f.unop.left ≫ (unop X).hom = (unop Y).hom :=
-        by
+      have : yoneda.map f.unop.left ≫ (unop X).hom = (unop Y).hom := by
         convert f.unop.3
       erw [← this]
       simp only [yoneda_map_app, FunctorToTypes.comp]
@@ -243,9 +239,9 @@ theorem fromCostructuredArrow_obj_mk (F : Cᵒᵖ ⥤ Type v) {X : C} (f : yoned
 theorem from_toCostructuredArrow_eq (F : Cᵒᵖ ⥤ Type v) :
     (toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F = 𝟭 _ := by
   refine' Functor.ext _ _
-  . intro X
+  · intro X
     exact Functor.Elements.ext _ _ rfl (by simp [yonedaEquiv])
-  . intro X Y f
+  · intro X Y f
     have : ∀ {a b : F.Elements} (H : a = b),
         (eqToHom H).1 = eqToHom (show a.fst = b.fst by cases H; rfl) := by
       rintro _ _ rfl
@@ -269,7 +265,7 @@ theorem to_fromCostructuredArrow_eq (F : Cᵒᵖ ⥤ Type v) :
     funext f
     convert congr_fun (X_hom.naturality f.op).symm (𝟙 X_left)
     simp
-  . intro X Y f
+  · intro X Y f
     ext
     simp [CostructuredArrow.eqToHom_left]
 #align category_theory.category_of_elements.to_from_costructured_arrow_eq

diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean
@@ -1184,8 +1184,6 @@ theorem ssubset_insert (h : a ∉ s) : s ⊂ insert a s :=
   ssubset_iff.mpr ⟨a, h, Subset.rfl⟩
 #align finset.ssubset_insert Finset.ssubset_insert
 
-#check Finset.mk
-
 @[elab_as_elim]
 theorem cons_induction {α : Type _} {p : Finset α → Prop} (empty : p ∅)
     (cons : ∀ ⦃a : α⦄ {s : Finset α} (h : a ∉ s), p s → p (cons a s h)) : ∀ s, p s

diff --git a/Mathlib/Data/MvPolynomial/Division.lean b/Mathlib/Data/MvPolynomial/Division.lean
@@ -161,44 +161,44 @@ local infixl:70 " /ᵐᵒⁿᵒᵐⁱᵃˡ " => divMonomial
 local infixl:70 " %ᵐᵒⁿᵒᵐⁱᵃˡ " => modMonomial
 
 @[simp]
-theorem x_mul_divMonomial (i : σ) (x : MvPolynomial σ R) :
+theorem X_mul_divMonomial (i : σ) (x : MvPolynomial σ R) :
     X i * x /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = x :=
   divMonomial_monomial_mul _ _
 set_option linter.uppercaseLean3 false in
-#align mv_polynomial.X_mul_div_monomial MvPolynomial.x_mul_divMonomial
+#align mv_polynomial.X_mul_div_monomial MvPolynomial.X_mul_divMonomial
 
 @[simp]
-theorem x_divMonomial (i : σ) : (X i : MvPolynomial σ R) /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 1 :=
+theorem X_divMonomial (i : σ) : (X i : MvPolynomial σ R) /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 1 :=
   divMonomial_monomial (Finsupp.single i 1)
 set_option linter.uppercaseLean3 false in
-#align mv_polynomial.X_div_monomial MvPolynomial.x_divMonomial
+#align mv_polynomial.X_div_monomial MvPolynomial.X_divMonomial
 
 @[simp]
-theorem mul_x_divMonomial (x : MvPolynomial σ R) (i : σ) :
+theorem mul_X_divMonomial (x : MvPolynomial σ R) (i : σ) :
     x * X i /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = x :=
   divMonomial_mul_monomial _ _
 set_option linter.uppercaseLean3 false in
-#align mv_polynomial.mul_X_div_monomial MvPolynomial.mul_x_divMonomial
+#align mv_polynomial.mul_X_div_monomial MvPolynomial.mul_X_divMonomial
 
 @[simp]
-theorem x_mul_modMonomial (i : σ) (x : MvPolynomial σ R) :
+theorem X_mul_modMonomial (i : σ) (x : MvPolynomial σ R) :
     X i * x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0 :=
   monomial_mul_modMonomial _ _
 set_option linter.uppercaseLean3 false in
-#align mv_polynomial.X_mul_mod_monomial MvPolynomial.x_mul_modMonomial
+#align mv_polynomial.X_mul_mod_monomial MvPolynomial.X_mul_modMonomial
 
 @[simp]
-theorem mul_x_modMonomial (x : MvPolynomial σ R) (i : σ) :
+theorem mul_X_modMonomial (x : MvPolynomial σ R) (i : σ) :
     x * X i %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0 :=
   mul_monomial_modMonomial _ _
 set_option linter.uppercaseLean3 false in
-#align mv_polynomial.mul_X_mod_monomial MvPolynomial.mul_x_modMonomial
+#align mv_polynomial.mul_X_mod_monomial MvPolynomial.mul_X_modMonomial
 
 @[simp]
-theorem modMonomial_x (i : σ) : (X i : MvPolynomial σ R) %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0 :=
+theorem modMonomial_X (i : σ) : (X i : MvPolynomial σ R) %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0 :=
   monomial_modMonomial _
 set_option linter.uppercaseLean3 false in
-#align mv_polynomial.mod_monomial_X MvPolynomial.modMonomial_x
+#align mv_polynomial.mod_monomial_X MvPolynomial.modMonomial_X
 
 theorem divMonomial_add_modMonomial_single (x : MvPolynomial σ R) (i : σ) :
     X i * (x /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1) + x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = x :=
@@ -210,11 +210,11 @@ theorem modMonomial_add_divMonomial_single (x : MvPolynomial σ R) (i : σ) :
   modMonomial_add_divMonomial _ _
 #align mv_polynomial.mod_monomial_add_div_monomial_single MvPolynomial.modMonomial_add_divMonomial_single
 
-theorem x_dvd_iff_modMonomial_eq_zero {i : σ} {x : MvPolynomial σ R} :
+theorem X_dvd_iff_modMonomial_eq_zero {i : σ} {x : MvPolynomial σ R} :
     X i ∣ x ↔ x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0 :=
   monomial_one_dvd_iff_modMonomial_eq_zero
 set_option linter.uppercaseLean3 false in
-#align mv_polynomial.X_dvd_iff_mod_monomial_eq_zero MvPolynomial.x_dvd_iff_modMonomial_eq_zero
+#align mv_polynomial.X_dvd_iff_mod_monomial_eq_zero MvPolynomial.X_dvd_iff_modMonomial_eq_zero
 
 end XLemmas
 
@@ -251,20 +251,20 @@ theorem monomial_one_dvd_monomial_one [Nontrivial R] {i j : σ →₀ ℕ} :
 #align mv_polynomial.monomial_one_dvd_monomial_one MvPolynomial.monomial_one_dvd_monomial_one
 
 @[simp]
-theorem x_dvd_x [Nontrivial R] {i j : σ} :
+theorem X_dvd_X [Nontrivial R] {i j : σ} :
     (X i : MvPolynomial σ R) ∣ (X j : MvPolynomial σ R) ↔ i = j := by
   refine' monomial_one_dvd_monomial_one.trans _
   simp_rw [Finsupp.single_le_iff, Nat.one_le_iff_ne_zero, Finsupp.single_apply_ne_zero, Ne.def,
     one_ne_zero, not_false_iff, and_true_iff]
 set_option linter.uppercaseLean3 false in
-#align mv_polynomial.X_dvd_X MvPolynomial.x_dvd_x
+#align mv_polynomial.X_dvd_X MvPolynomial.X_dvd_X
 
 @[simp]
-theorem x_dvd_monomial {i : σ} {j : σ →₀ ℕ} {r : R} :
+theorem X_dvd_monomial {i : σ} {j : σ →₀ ℕ} {r : R} :
     (X i : MvPolynomial σ R) ∣ monomial j r ↔ r = 0 ∨ j i ≠ 0 := by
   refine' monomial_dvd_monomial.trans _
   simp_rw [one_dvd, and_true_iff, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]
 set_option linter.uppercaseLean3 false in
-#align mv_polynomial.X_dvd_monomial MvPolynomial.x_dvd_monomial
+#align mv_polynomial.X_dvd_monomial MvPolynomial.X_dvd_monomial
 
 end MvPolynomial