chore: golf a bit

FLT/AutomorphicRepresentation/Example.lean

@@ -96,8 +96,7 @@ lemma _root_.Nat.sum_factorial_lt_factorial_succ {j : ℕ} (hj : 1 < j) :
     ∑ i ∈ range (j + 1), i ! < ∑ _i ∈ range (j + 1), j ! := ?_
     _ = (j + 1) * (j !) := by rw [sum_const, card_range, smul_eq_mul]
     _ = (j + 1)! := Nat.factorial_succ _
-  apply sum_lt_sum
-  apply (fun i hi => factorial_le <| by simpa only [mem_range, lt_succ] using hi)
+  apply sum_lt_sum (fun i hi => factorial_le <| by simpa only [mem_range, lt_succ] using hi) ?_
   use 0
   rw [factorial_zero]
   simp [hj]

FLT/Basic/Reductions.lean

@@ -254,17 +254,10 @@ lemma FreyCurve.j (P : FreyPackage) :
   rw [mul_div_right_comm, EllipticCurve.j, FreyCurve.Δ'inv, FreyCurve.c₄']
 
 private lemma j_pos_aux (a b : ℤ) (hb : b ≠ 0) : 0 < (a + b) ^ 2 - a * b := by
-  cases le_or_lt 0 (a * b) with
-  | inl h =>
-    calc
-      0 < a * a + a * b + b * b := ?_
-      _ = _ := by ring
-    apply add_pos_of_nonneg_of_pos
-    apply add_nonneg (mul_self_nonneg _) h
-    apply mul_self_pos.mpr hb
-  | inr h =>
-    rw [sub_pos]
-    exact h.trans_le (sq_nonneg _)
+  rify
+  calc
+    (0 : ℝ) < (a ^ 2 + (a + b) ^ 2 + b ^ 2) / 2 := by positivity
+    _ = (a + b) ^ 2 - a * b := by ring
 
 /-- The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is
 a prime of bad reduction. -/
@@ -344,13 +337,14 @@ It follows that there is no Frey package.
 work of Mazur and Wiles/Ribet to rule out all possibilities for the
 $p$-torsion in the corresponding Frey curve. -/
 theorem FreyPackage.false (P : FreyPackage) : False := by
+  -- by Wiles' result, the p-torsion is not irreducible
   apply Wiles_Frey P
+  -- but by Mazur's result, the p-torsion is irreducible!
   exact Mazur_Frey P
+  -- Contradiction!
 
 -- Fermat's Last Theorem is true
 theorem Wiles_Taylor_Wiles : FermatLastTheorem := by
-  apply of_p_ge_5
-  intro p hp5 pp a b c ha hb _ h
-  refine Nonempty.elim ?_ FreyPackage.false
+  refine of_p_ge_5 fun p hp5 pp a b c ha hb _ h ↦  Nonempty.elim ?_ FreyPackage.false
   apply FreyPackage.of_not_FermatLastTheorem_p_ge_5 (a := a) (b := b) (c := c)
     <;> assumption_mod_cast

FLT/ForMathlib/MiscLemmas.lean

@@ -2,8 +2,6 @@ import Mathlib.Algebra.Module.Projective
 import Mathlib.Topology.Algebra.Monoid
 import Mathlib.RingTheory.OreLocalization.Ring
 import Mathlib
-
-
 section elsewhere
 
 variable {A : Type*} [AddCommGroup A]
@@ -54,9 +52,7 @@ theorem coinduced_prod_eq_prod_coinduced {X Y S T : Type*} [AddCommGroup X] [Add
   · intro h x y hxy
     rw [Set.mem_preimage, Prod.map_apply] at hxy
     obtain ⟨U1, U2, hU1, hU2, hx1, hy2, h12⟩ := h (f x) (g y) hxy
-    use f ⁻¹' U1, g ⁻¹' U2, hU1, hU2, hx1, hy2
-    intro ⟨x', y'⟩ ⟨hx', hy'⟩
-    exact h12 ⟨hx', hy'⟩
+    exact ⟨f ⁻¹' U1, g ⁻¹' U2, hU1, hU2, hx1, hy2, fun ⟨x', y'⟩ ⟨hx', hy'⟩ ↦ h12 ⟨hx', hy'⟩⟩
 
 end elsewhere
 
@@ -103,7 +99,7 @@ theorem finsum_option {ι : Type*} {B : Type*} [Finite ι]
   rw [← finsum_mem_univ]
   convert finsum_mem_insert φ (show none ∉ Set.range Option.some by aesop)
     (Set.finite_range some)
-  · aesop
+  · exact (Set.insert_none_range_some ι).symm
   · rw [finsum_mem_range]
     exact Option.some_injective ι
 
@@ -126,8 +122,8 @@ def LinearEquiv.sumPiEquivProdPi (S T : Type*) (A : S ⊕ T → Type*)
     [∀ st, AddCommMonoid (A st)] [∀ st, Module R (A st)] :
     (∀ (st : S ⊕ T), A st) ≃ₗ[R] (∀ (s : S), A (.inl s)) × (∀ (t : T), A (.inr t)) where
       toFun f := (fun s ↦ f (.inl s), fun t ↦ f (.inr t))
-      map_add' f g := by aesop
-      map_smul' := by aesop
+      map_add' f g := rfl
+      map_smul' _ _ := rfl
       invFun fg st := Sum.rec (fun s => fg.1 s) (fun t => fg.2 t) st
       left_inv := by intro x; aesop
       right_inv := by intro x; aesop
@@ -152,8 +148,8 @@ def Homeomorph.sumPiEquivProdPi (S T : Type*) (A : S ⊕ T → Type*)
 def Homeomorph.pUnitPiEquiv (f : PUnit → Type*) [∀ x, TopologicalSpace (f x)]: ((t : PUnit) → (f t)) ≃ₜ f () where
   toFun a := a ()
   invFun a _t := a
-  left_inv x := by aesop
-  right_inv x := by aesop
+  left_inv x := rfl
+  right_inv x := rfl
   continuous_toFun := by simp; fun_prop
   continuous_invFun := by simp; fun_prop
 
@@ -163,10 +159,10 @@ def LinearEquiv.pUnitPiEquiv (f : PUnit → Type*) [∀ x, AddCommMonoid (f x)]
     ((t : PUnit) → (f t)) ≃ₗ[R] f () where
   toFun a := a ()
   invFun a _t := a
-  left_inv x := by aesop
-  right_inv x := by aesop
-  map_add' f g := rfl
-  map_smul' r f := rfl
+  left_inv _ := rfl
+  right_inv _ := rfl
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
 
 -- elsewhere
 theorem finsum_apply {α ι N : Type*} [AddCommMonoid N] [Finite ι]

FLT/GlobalLanglandsConjectures/GLnDefs.lean

@@ -129,10 +129,10 @@ theorem diamond_fix :
   conv_lhs => rw [← @bracketBilin_apply_apply R _ _ _ _]
   rw [← @bracketBilin_apply_apply R _ _ _ (_) (.ofAssociativeAlgebra) _ _ (_) (_) x y]
   rotate_left
-  exact @lieAlgebraSelfModule _ _ _ (_) (_)
+  exact @lieAlgebraSelfModule ..
   refine LinearMap.congr_fun₂ ?_ x y
   ext xa xb ya yb
-  change @Bracket.bracket _ _ (_) (xa ⊗ₜ[R] xb) (ya ⊗ₜ[R] yb) = _
+  change @Bracket.bracket _ _ _ (xa ⊗ₜ[R] xb) (ya ⊗ₜ[R] yb) = _
   dsimp [Ring.lie_def]
   rw [TensorProduct.tmul_sub, mul_comm]
 
@@ -168,9 +168,9 @@ variable (G : Type) [TopologicalSpace G] [Group G]
 def action :
     LeftInvariantDerivation 𝓘(ℝ, E) G →ₗ⁅ℝ⁆ (Module.End ℝ C^∞⟮𝓘(ℝ, E), G; ℝ⟯) where
   toFun l := Derivation.toLinearMap l
-  map_add' := by simp
-  map_smul' := by simp
-  map_lie' {x y} := rfl
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+  map_lie' {_ _} := rfl
 
 open scoped TensorProduct
 
@@ -284,8 +284,8 @@ noncomputable def preweight.fdRep (n : ℕ) (w : preweight n) :
   ρ := {
     toFun := fun A ↦ {
       toFun := fun x ↦ (w.rho A).1 *ᵥ x
-      map_add' := fun _ _ ↦ Matrix.mulVec_add _ _ _
-      map_smul' := fun _ _ ↦ by simpa using Matrix.mulVec_smul _ _ _ }
+      map_add' := fun _ _ ↦ Matrix.mulVec_add ..
+      map_smul' := fun _ _ ↦ by simpa using Matrix.mulVec_smul .. }
     map_one' := by aesop
     map_mul' := fun _ _ ↦ by
       simp only [obj_carrier, MonCat.mul_of, _root_.map_mul, Units.val_mul, ← Matrix.mulVec_mulVec]

FLT/HIMExperiments/flatness.lean

@@ -92,8 +92,7 @@ noncomputable def _root_.Ideal.isoBaseOfIsPrincipal {I : Ideal R} [IsDomain R]
     rw [LinearMap.mem_ker] at h
     apply (AddSubmonoid.mk_eq_zero _).mp at h
     rw [Ideal.mem_bot]
-    refine eq_zero_of_ne_zero_of_mul_right_eq_zero ?_ h
-    refine mt (fun h3 ↦ ?_) hI
+    refine eq_zero_of_ne_zero_of_mul_right_eq_zero (mt (fun h3 ↦ ?_) hI) h
     rwa [Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero I])
   (by
     rintro ⟨i, hi⟩

FLT/MathlibExperiments/IsFrobenius.lean

@@ -110,12 +110,8 @@ lemma IsMaximal_not_eq_bot [NumberField K] (Q : Ideal (𝓞 K)) [Ideal.IsMaximal
   Ring.ne_bot_of_isMaximal_of_not_isField inferInstance (RingOfIntegers.not_isField K)
 
 lemma NumberField_Ideal_IsPrime_iff_IsMaximal  [NumberField K]
-    (Q : Ideal (𝓞 K)) (h1: Q ≠ ⊥) : Ideal.IsPrime Q ↔ Ideal.IsMaximal Q := by
-  constructor
-  · intro h
-    exact Ideal.IsPrime.isMaximal h h1
-  · intro h
-    exact Ideal.IsMaximal.isPrime h
+    (Q : Ideal (𝓞 K)) (h1: Q ≠ ⊥) : Ideal.IsPrime Q ↔ Ideal.IsMaximal Q :=
+  ⟨fun h => Ideal.IsPrime.isMaximal h h1, fun h => Ideal.IsMaximal.isPrime h⟩
 
 instance Fintype_Quot_of_IsMaximal [NumberField K] (P : Ideal (𝓞 K)) [Ideal.IsMaximal P] : Fintype ((𝓞 K) ⧸ P) := by
   sorry