Merge remote-tracking branch 'upstream/main' into golf-proofs

Author: pitmonticone

FLT/AutomorphicForm/QuaternionAlgebra.lean

@@ -40,11 +40,11 @@ instance : Algebra A (D ⊗[R] A) :=
     simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.includeRight_apply]
     intro a b
     apply TensorProduct.induction_on (motive := fun b ↦ 1 ⊗ₜ[R] a * b = b * 1 ⊗ₜ[R] a)
-    . simp only [mul_zero, zero_mul]
-    . intro d a'
+    · simp only [mul_zero, zero_mul]
+    · intro d a'
       simp only [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_one]
       rw [NonUnitalCommSemiring.mul_comm]
-    . intro x y hx hy
+    · intro x y hx hy
       rw [left_distrib, hx, hy, right_distrib]
     )
 
@@ -205,6 +205,6 @@ lemma sMul_eval (g : Dfx F D) (f : AutomorphicForm F D M) (x : (D ⊗[F] FiniteA
   (g • f) x = f (x * g) := rfl
 
 instance : MulAction (Dfx F D) (AutomorphicForm F D M) where
-  smul := (. • .)
+  smul := (· • ·)
   one_smul := by intros; ext; simp only [sMul_eval, mul_one]
   mul_smul := by intros; ext; simp only [sMul_eval, mul_assoc]

FLT/AutomorphicRepresentation/Example.lean

@@ -54,9 +54,6 @@ lemma ext (x y : ZHat) (h : ∀ n : ℕ+, x n = y n) : x = y := by
   ext n
   apply h
 
-lemma ext_iff (x y : ZHat) : (∀ n : ℕ+, x n = y n) ↔ x = y :=
-  ⟨ext x y, fun h n => congrFun (congrArg DFunLike.coe h) n⟩
-
 @[simp] lemma zero_val (n : ℕ+) : (0 : ZHat) n = 0 := rfl
 @[simp] lemma one_val (n : ℕ+) : (1 : ZHat) n = 1 := rfl
 @[simp] lemma ofNat_val (m : ℕ) [m.AtLeastTwo] (n : ℕ+) :
@@ -75,7 +72,7 @@ lemma zeroNeOne : (0 : ZHat) ≠ 1 := by
 instance nontrivial : Nontrivial ZHat := ⟨0, 1, zeroNeOne⟩
 
 instance charZero : CharZero ZHat := ⟨ fun a b h ↦ by
-  rw [← ext_iff] at h
+  rw [ZHat.ext_iff] at h
   specialize h ⟨_, (max a b).succ_pos⟩
   apply_fun ZMod.val at h
   rwa [natCast_val, ZMod.val_cast_of_lt, natCast_val, ZMod.val_cast_of_lt] at h
@@ -200,8 +197,7 @@ lemma torsionfree (N : ℕ+) : Function.Injective (fun z : ZHat ↦ N * z) := by
   rw [← AddMonoidHom.coe_mulLeft, injective_iff_map_eq_zero]
   intro a ha
   rw [AddMonoidHom.coe_mulLeft] at ha
-  rw [← ext_iff]
-  intro j
+  ext j
   rw [zero_val, ← a.prop j (N * j) (by simp)]
   apply torsionfree_aux
   apply Nat.dvd_of_mul_dvd_mul_left N.pos
@@ -824,7 +820,8 @@ lemma exists_near (a : ℍ) : ∃ q : 𝓞, dist a (toQuaternion q) < 1 := by
     rw [add_eq_zero_iff' (by positivity) (by positivity)]
     rw [add_eq_zero_iff' (by positivity) (by positivity)]
     rw [add_eq_zero_iff' (by positivity) (by positivity)]
-    simp_rw [and_assoc, sq_eq_zero_iff, sub_re, sub_imI, sub_imJ, sub_imK, sub_eq_zero, ← ext_iff]
+    simp_rw [and_assoc, sq_eq_zero_iff, sub_re, sub_imI, sub_imJ, sub_imK, sub_eq_zero,
+      ← Quaternion.ext_iff]
     symm
     apply leftInvOn_toQuaternion_fromQuaternion
     · simp only [Set.mem_setOf]

FLT/FLT_files.lean

@@ -1,13 +1,9 @@
 import FLT.Basic.Reductions
 import FLT.EllipticCurve.Torsion
-import FLT.for_mathlib.Coalgebra.Monoid
-import FLT.for_mathlib.Coalgebra.Sweedler
-import FLT.for_mathlib.Coalgebra.TensorProduct
-import FLT.for_mathlib.HopfAlgebra.Basic
-import FLT.for_mathlib.IsCentralSimple
 import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
 import FLT.GroupScheme.FiniteFlat
 import FLT.Hard.Results
 import FLT.TateCurve.TateCurve
 import FLT.AutomorphicRepresentation.Example
+import FLT.mathlibExperiments.IsCentralSimple