Golf a few proofs

FLT/Basic/Reductions.lean

@@ -108,20 +108,17 @@ lemma gcdab_eq_gcdac {a b c : ℤ} {p : ℕ} (hp : 0 < p) (h : a ^ p + b ^ p = c
   have foo : gcd a b ∣ gcd a c := by
     apply dvd_gcd (gcd_dvd_left a b)
     rw [← Int.pow_dvd_pow_iff hp.ne', ← h]
-    apply dvd_add
-    · rw [Int.pow_dvd_pow_iff hp.ne']
-      exact gcd_dvd_left a b
-    · rw [Int.pow_dvd_pow_iff hp.ne']
-      exact gcd_dvd_right a b
+    apply dvd_add <;> rw [Int.pow_dvd_pow_iff hp.ne']
+    · exact gcd_dvd_left a b
+    · exact gcd_dvd_right a b
   have bar : gcd a c ∣ gcd a b := by
     apply dvd_gcd (gcd_dvd_left a c)
     have h2 : b ^ p = c ^ p - a ^ p := eq_sub_of_add_eq' h
     rw [← Int.pow_dvd_pow_iff hp.ne', h2]
     apply dvd_add
     · rw [Int.pow_dvd_pow_iff hp.ne']
       exact gcd_dvd_right a c
-    · rw [dvd_neg]
-      rw [Int.pow_dvd_pow_iff hp.ne']
+    · rw [dvd_neg, Int.pow_dvd_pow_iff hp.ne']
       exact gcd_dvd_left a c
   change _ ∣ (Int.gcd a c : ℤ) at foo
   apply Int.ofNat_dvd.1 at bar
@@ -226,45 +223,35 @@ def FreyCurve (P : FreyPackage) : EllipticCurve ℚ := {
       simp_rw [← mul_pow]
       refine pow_ne_zero 2 <| pow_ne_zero P.p <| (mul_ne_zero (mul_ne_zero P.ha0 P.hb0) P.hc0)
     coe_Δ' := by
-      simp only [Units.val_mk0]
-      rw [← Int.cast_pow P.c, ← P.hFLT]
+      simp only [Units.val_mk0, ← Int.cast_pow P.c, ← P.hFLT]
       field_simp [EllipticCurve.Δ', WeierstrassCurve.Δ, WeierstrassCurve.b₂, WeierstrassCurve.b₄,
         WeierstrassCurve.b₆, WeierstrassCurve.b₈]
       ring }
 
 lemma FreyCurve.b₂ (P : FreyPackage) :
     P.FreyCurve.b₂ = P.b ^ P.p - P.a ^ P.p := by
   simp [FreyCurve, WeierstrassCurve.b₂]
-  field_simp
-  norm_cast
   ring
 
 lemma FreyCurve.b₄ (P : FreyPackage) :
     P.FreyCurve.b₄ = - (P.a * P.b) ^ P.p / 8 := by
   simp [FreyCurve, WeierstrassCurve.b₄]
-  field_simp
-  norm_cast
   ring
 
 lemma FreyCurve.c₄ (P : FreyPackage) :
     P.FreyCurve.c₄ = (P.a ^ P.p) ^ 2 + P.a ^ P.p * P.b ^ P.p + (P.b ^ P.p) ^ 2 := by
   simp [FreyCurve.b₂, FreyCurve.b₄, WeierstrassCurve.c₄]
-  field_simp
-  norm_cast
   ring
 
 lemma FreyCurve.c₄' (P : FreyPackage) :
     P.FreyCurve.c₄ = P.c ^ (2 * P.p) - (P.a * P.b) ^ P.p := by
   rw [FreyCurve.c₄]
-  norm_cast
-  rw [pow_mul', ← hFLT]
+  rw_mod_cast [pow_mul', ← hFLT]
   ring
 
 lemma FreyCurve.Δ'inv (P : FreyPackage) :
     (↑(P.FreyCurve.Δ'⁻¹) : ℚ) = 2 ^ 8 / (P.a*P.b*P.c)^(2*P.p) := by
   simp [FreyCurve]
-  congr 1
-  norm_cast
   ring
 
 lemma FreyCurve.j (P : FreyPackage) :
@@ -282,7 +269,7 @@ private lemma j_pos_aux (a b : ℤ) (hb : b ≠ 0) : 0 < (a + b) ^ 2 - a * b :=
     apply mul_self_pos.mpr hb
   | inr h =>
     rw [sub_pos]
-    apply h.trans_le (sq_nonneg _)
+    exact h.trans_le (sq_nonneg _)
 
 /-- 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. -/
@@ -292,8 +279,7 @@ lemma FreyCurve.j_valuation_of_bad_prime (P : FreyPackage) {q : ℕ} (hqPrime :
   have := Fact.mk hqPrime
   have hqPrime' := Nat.prime_iff_prime_int.mp hqPrime
   have h₀ : ((P.c ^ (2 * P.p) - (P.a * P.b) ^ P.p) ^ 3 : ℚ) ≠ 0 := by
-    norm_cast
-    rw [pow_mul', ← P.hFLT, mul_pow]
+    rw_mod_cast [pow_mul', ← P.hFLT, mul_pow]
     exact pow_ne_zero _ <| ne_of_gt <| j_pos_aux _ _ (pow_ne_zero _ P.hb0)
   have h₁ : P.a * P.b * P.c ≠ 0 := mul_ne_zero (mul_ne_zero P.ha0 P.hb0) P.hc0
   rw [FreyCurve.j, padicValRat.div (mul_ne_zero (by norm_num) h₀) (pow_ne_zero _ (mod_cast h₁)),
@@ -326,10 +312,6 @@ lemma FreyCurve.j_valuation_of_bad_prime (P : FreyPackage) {q : ℕ} (hqPrime :
 
 end FreyPackage
 
-
-
-
-
 /-!
 
 Given an elliptic curve over `ℚ`, the p-torsion points defined over an algebraic
@@ -366,9 +348,7 @@ It follows that there is no Frey package.
 /-- There is no Frey package. This profound result is proved using
 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
-  apply Wiles_Frey P
-  exact Mazur_Frey P
+theorem FreyPackage.false (P : FreyPackage) : False := Wiles_Frey P (Mazur_Frey P)
 
 -- Fermat's Last Theorem is true
 theorem Wiles_Taylor_Wiles : FermatLastTheorem := by

FLT/for_mathlib/Frobenius.lean

@@ -378,7 +378,7 @@ noncomputable instance : Field (A ⧸ P) := Ideal.Quotient.field P
 lemma is_primepow_char_A_quot_P : IsPrimePow q := Fintype.isPrimePow_card_of_field
 
 lemma ex_primepow_char_A_quot_P : ∃ p n : ℕ , Prime p ∧ 0 < n ∧ p ^ n = q := by
-  apply is_primepow_char_A_quot_P
+  exact is_primepow_char_A_quot_P _
 
 local notation "p" => Classical.choose (CharP.exists (A ⧸ P))
 local notation "p'" => Classical.choose (ex_primepow_char_A_quot_P P)
@@ -401,7 +401,7 @@ lemma p_is_p' : p = p' := by
   have h1 : p ∣ q := charP_iff (A ⧸ P) p |>.1 (p_is_char P) q |>.1 eq0
   have eq1 : p' ^ n = q := q_is_p'_pow_n P
   rw [← eq1] at h1
-  refine Nat.dvd_prime (p'_is_prime P) |>.1
+  exact Nat.dvd_prime (p'_is_prime P) |>.1
     (Nat.Prime.dvd_of_dvd_pow (p_is_prime P) h1) |>.resolve_left <| Nat.Prime.ne_one <| p_is_prime P
 
 lemma q_is_p_pow_n : p ^ n = q := by
@@ -415,7 +415,7 @@ theorem pow_eq_expand (a : (A ⧸ P)[X]) :
   have pprime : Nat.Prime p := p_is_prime P
   have factprime : Fact (Nat.Prime p) := { out := pprime }
   rw [← q_is_p_pow_n, ← map_expand_pow_char, map_expand, FiniteField.frobenius_pow]
-  · simp only [exists_and_left, RingHom.one_def, map_id]
+  · simp [exists_and_left, RingHom.one_def, map_id]
   · exact (q_is_p_pow_n P).symm
 
 end FreshmansDream
@@ -482,11 +482,7 @@ theorem gal_smul_F_eq  (σ : L ≃ₐ[K] L) :
     ∏ τ : L ≃ₐ[K] L,
     (X - C (galRestrict A K L B σ
       (galRestrict A K L B τ α))):= by
-  rw [Finset.smul_prod]
-  simp_rw [smul_sub]
-  ext
-  congr
-  simp only [smul_X, smul_C, AlgEquiv.smul_def]
+  simp [Finset.smul_prod, smul_sub, smul_X, smul_C, AlgEquiv.smul_def]
 
 /-- use `Finset.prod_bij` to show
 `(galRestrict A K L B σ • (∏ τ : L ≃ₐ[K] L, (X - C (galRestrict A K L B τ α))) =
@@ -497,11 +493,11 @@ lemma F_invariant_under_finite_aut (σ :  L ≃ₐ[K] L)  :
   set i : (τ : L ≃ₐ[K] L) → τ ∈ Finset.univ → L ≃ₐ[K] L := fun τ _ => σ * τ
   -- needed to use `set i` instead of `have i`, in order to be able to use `i` later on, in proof
   have hi : ∀ (τ : L ≃ₐ[K] L) (hτ : τ ∈ Finset.univ), i τ hτ ∈ Finset.univ := by
-    simp only [Finset.mem_univ, forall_true_left, forall_const]
+    simp [Finset.mem_univ, forall_true_left, forall_const]
   have i_inj : ∀ (τ₁ : L ≃ₐ[K] L) (hτ₁ : τ₁ ∈ Finset.univ) (τ₂ : L ≃ₐ[K] L)
       (hτ₂ : τ₂ ∈ Finset.univ), i τ₁ hτ₁ = i τ₂ hτ₂ → τ₁ = τ₂ := by
     intros τ₁ _ τ₂ _ h
-    simpa only [i, mul_right_inj] using h
+    simpa [i, mul_right_inj] using h
   have i_surj : ∀ σ ∈ Finset.univ, ∃ (τ : L ≃ₐ[K] L) (hτ : τ ∈ Finset.univ), i τ hτ = σ := by
     intro τ'
     simp only [Finset.mem_univ, exists_true_left, forall_true_left, i]
@@ -514,7 +510,7 @@ lemma F_invariant_under_finite_aut (σ :  L ≃ₐ[K] L)  :
     simp only [i, map_mul, sub_right_inj, C_inj]
     rw [AlgEquiv.aut_mul]
     rfl
-  apply Finset.prod_bij i hi i_inj i_surj h
+  exact Finset.prod_bij i hi i_inj i_surj h
 
 /-- ` L ≃ₐ[K] L` fixes `F`. -/
 theorem gal_smul_F_eq_self (σ : L ≃ₐ[K] L) :
@@ -526,9 +522,8 @@ theorem gal_smul_F_eq_self (σ : L ≃ₐ[K] L) :
 
 theorem gal_smul_coeff_eq (n : ℕ) (h : ∀ σ : L ≃ₐ[K] L, galRestrict A K L B σ • F = F)
     (σ : L ≃ₐ[K] L) : galRestrict A K L B σ • (coeff F n) = coeff F n := by
-  simp only [AlgEquiv.smul_def]
   nth_rewrite 2 [← h σ]
-  simp only [coeff_smul, AlgEquiv.smul_def]
+  simp [coeff_smul, AlgEquiv.smul_def]
 
 variable {A K L B Q}
 
@@ -574,7 +569,7 @@ theorem coeff_lives_in_A (n : ℕ) : ∃ a : A, algebraMap B L (coeff F n) = (al
     exact NoZeroSMulDivisors.algebraMap_injective K L
   cases' h1.1 h2 with a' ha'
   use a'
-  simpa only [eq0, RingHom.coe_comp, Function.comp_apply, ha']
+  simpa [eq0, RingHom.coe_comp, Function.comp_apply, ha']
 
 /-- `α` is a root of `F`. -/
 lemma isRoot_α : eval α F = 0 := by
@@ -597,14 +592,12 @@ lemma isRoot_α : eval α F = 0 := by
   apply eq0 at evalid
   rwa [← eqF]
 
-lemma quotient_isRoot_α : (eval α F) ∈ Q := by
-  rw [isRoot_α Q_ne_bot]
-  apply Ideal.zero_mem
+lemma quotient_isRoot_α : (eval α F) ∈ Q := (isRoot_α Q_ne_bot) ▸ Ideal.zero_mem _
 
 lemma conjugate_isRoot_α (σ : L ≃ₐ[K] L) : (eval (galRestrict A K L B σ α) F) = 0 := by
   have evalσ : eval  (galRestrict A K L B σ α)
       (X - C (galRestrict A K L B σ α)) = 0 := by
-    simp only [eval_sub, eval_X, eval_C, sub_self]
+    simp [eval_sub, eval_X, eval_C, sub_self]
   have eqF : (eval (galRestrict A K L B σ α) (∏ τ : L ≃ₐ[K] L,
       (X - C (galRestrict A K L B τ α)))) =
       eval (galRestrict A K L B σ α) F := rfl
@@ -624,9 +617,7 @@ lemma conjugate_isRoot_α (σ : L ≃ₐ[K] L) : (eval (galRestrict A K L B σ 
   rw [← eqF, evalσ]
 
 lemma conjugate_quotient_isRoot_α (σ : L ≃ₐ[K] L) :
-    (eval (galRestrict A K L B σ α) F) ∈ Q := by
-  rw [conjugate_isRoot_α Q_ne_bot]
-  apply Ideal.zero_mem
+    (eval (galRestrict A K L B σ α) F) ∈ Q := (conjugate_isRoot_α Q_ne_bot) _ ▸ Ideal.zero_mem _
 
 lemma F_is_root_iff_is_conjugate {x : B} :
     IsRoot F x ↔ (∃ σ : L ≃ₐ[K] L, x = (galRestrict A K L B σ α)) := by
@@ -650,7 +641,7 @@ lemma F_is_root_iff_is_conjugate {x : B} :
   · intros h
     rcases h with ⟨σ, hσ⟩
     rw [Polynomial.IsRoot.def, hσ]
-    apply conjugate_isRoot_α Q_ne_bot
+    exact conjugate_isRoot_α Q_ne_bot _
 
 lemma F_eval_zero_is_conjugate {x : B} (h : eval x F = 0) : ∃ σ : L ≃ₐ[K] L,
     x = ((galRestrict A K L B σ) α) := by
@@ -672,17 +663,15 @@ lemma ex_poly_in_A : ∃ m : A[X], Polynomial.map (algebraMap A B) m = F := by
         apply Iff.not
         rw [← _root_.map_eq_zero_iff (algebraMap B L), this, map_eq_zero_iff]
         have I : NoZeroSMulDivisors A L := NoZeroSMulDivisors.trans A K L
-        · apply NoZeroSMulDivisors.algebraMap_injective
-        · apply NoZeroSMulDivisors.algebraMap_injective
+        · exact NoZeroSMulDivisors.algebraMap_injective _ _
+        · exact NoZeroSMulDivisors.algebraMap_injective _ _
         }}
   use m
   ext n
-  have := Classical.choose_spec (h n)
   simp only [coeff_map, coeff_ofFinsupp, Finsupp.coe_mk]
   set s := Classical.choose (h n)
   apply NoZeroSMulDivisors.algebraMap_injective B L
-  rw [this]
-  exact (IsScalarTower.algebraMap_apply A B L _).symm
+  exact (Classical.choose_spec (h n)) ▸ (IsScalarTower.algebraMap_apply A B L _).symm
 
 /--`m' : A[X]` such that `Polynomial.map (algebraMap A B) m = F`.  -/
 noncomputable def m' : A[X] := Classical.choose (ex_poly_in_A Q_ne_bot)
@@ -697,11 +686,11 @@ lemma m_eq_F_in_B_quot_Q :
     Polynomial.map (algebraMap B (B ⧸ Q)) F := by
   suffices h : Polynomial.map (algebraMap A B) m = F  by
     exact congrArg (map (algebraMap B (B ⧸ Q))) h
-  apply m_mapsto_F
+  exact m_mapsto_F _
 
 lemma m_expand_char_q : (Polynomial.map (algebraMap A (A ⧸ P)) m) ^ q =
     (expand _ q (Polynomial.map (algebraMap A (A ⧸ P)) m)) := by
-  apply pow_eq_expand
+  exact pow_eq_expand _ _
 
 lemma B_m_expand_char_q : (Polynomial.map (algebraMap A (B ⧸ Q)) m) ^ q =
     (expand _ q (Polynomial.map (algebraMap A (B ⧸ Q)) m)) := by
@@ -735,23 +724,22 @@ lemma pow_expand_A_B_scalar_tower_F :
 lemma F_expand_eval_eq_eval_pow :
     (eval₂ (Ideal.Quotient.mk Q) (Ideal.Quotient.mk Q α) F) ^ q =
     (eval₂ (Ideal.Quotient.mk Q) (Ideal.Quotient.mk Q (α ^ q)) F) := by
-  simp only [← Polynomial.eval_map,  ←  Ideal.Quotient.algebraMap_eq, ← Polynomial.coe_evalRingHom,
-    ← map_pow, pow_expand_A_B_scalar_tower_F]
-  simp only [Ideal.Quotient.algebraMap_eq, coe_evalRingHom, expand_eval, map_pow]
+  simp_rw [← Polynomial.eval_map,  ←  Ideal.Quotient.algebraMap_eq, ← Polynomial.coe_evalRingHom,
+    ← map_pow, pow_expand_A_B_scalar_tower_F, Ideal.Quotient.algebraMap_eq, coe_evalRingHom,
+    expand_eval, map_pow]
 
 lemma quotient_F_is_product_of_quot :
     (Polynomial.map (Ideal.Quotient.mk Q) F) =
     ∏ τ : L ≃ₐ[K] L, (X - C ((Ideal.Quotient.mk Q) ((galRestrict A K L B τ) α))) := by
-  rw [← Polynomial.coe_mapRingHom]
-  erw [map_prod]
-  simp only [map_sub, coe_mapRingHom, map_X, map_C]
+  erw [← Polynomial.coe_mapRingHom, map_prod]
+  simp [map_sub, coe_mapRingHom, map_X, map_C]
 
 lemma quotient_F_is_root_iff_is_conjugate (x : (B ⧸ Q)) :
     IsRoot (Polynomial.map  (Ideal.Quotient.mk Q) F) x ↔
     (∃ σ : L ≃ₐ[K] L, x = ((Ideal.Quotient.mk Q) ((galRestrict A K L B σ) α)))  := by
   rw [quotient_F_is_product_of_quot, Polynomial.isRoot_prod]
   simp only [Finset.mem_univ, eval_sub, eval_X, eval_C, true_and, Polynomial.root_X_sub_C]
-  simp only [eq_comm (a := x)]
+  simp [eq_comm]
 
 lemma pow_eval_root_in_Q : ((eval α F) ^ q) ∈ Q := by
   have h : (eval α F) ∈ Q := quotient_isRoot_α Q_ne_bot
@@ -761,16 +749,15 @@ lemma pow_eval_root_in_Q : ((eval α F) ^ q) ∈ Q := by
 
 lemma expand_eval_root_eq_zero :
     (eval₂ (Ideal.Quotient.mk Q) (Ideal.Quotient.mk Q (α ^ q)) F) = 0 := by
-  rw [← F_expand_eval_eq_eval_pow P Q_ne_bot]
-  simp only [eval₂_at_apply, ne_eq, Fintype.card_ne_zero, not_false_eq_true, pow_eq_zero_iff]
+  simp only [← F_expand_eval_eq_eval_pow P Q_ne_bot, eval₂_at_apply, ne_eq, Fintype.card_ne_zero,
+    not_false_eq_true, pow_eq_zero_iff]
   have h : eval α F ∈ Q := quotient_isRoot_α Q_ne_bot
   rwa [← Ideal.Quotient.eq_zero_iff_mem] at h
 
 -- now, want `∃ σ, α ^ q ≡ σ α mod Q`
 lemma pow_q_is_conjugate : ∃ σ : L ≃ₐ[K] L, (Ideal.Quotient.mk Q (α ^ q)) =
     (Ideal.Quotient.mk Q ((((galRestrict A K L B) σ)) α)) := by
-  rw [← quotient_F_is_root_iff_is_conjugate]
-  simp only [map_pow, IsRoot.def, Polynomial.eval_map]
+  rw [← quotient_F_is_root_iff_is_conjugate, map_pow, IsRoot.def, Polynomial.eval_map]
   exact expand_eval_root_eq_zero P Q_ne_bot
 
 -- following lemma suggested by Amelia
@@ -779,7 +766,7 @@ lemma pow_quotient_IsRoot_α : (eval (α ^ q) F) ∈ Q := by
   have h2 : (eval₂ (Ideal.Quotient.mk Q) (Ideal.Quotient.mk Q (α ^ q)) F) = 0 :=
     expand_eval_root_eq_zero P Q_ne_bot
   convert h2
-  simp only [eval₂_at_apply]
+  rw [eval₂_at_apply]
 
 /--`α ^ q ≡ σ • α mod Q` for some `σ : L ≃ₐ[K] L` -/
 lemma pow_q_conjugate :
@@ -802,9 +789,8 @@ lemma inv_aut_not_mem_decomp (h : Frob ∉ decomposition_subgroup_Ideal' Q) : (F
 lemma gen_zero_mod_inv_aut (h1 : Frob ∉ decomposition_subgroup_Ideal' Q) :
     α ∈ (Frob⁻¹ • Q) := by
   have inv : Frob⁻¹ ∉ decomposition_subgroup_Ideal' Q := by
-    simpa only [inv_mem_iff]
-  apply generator_well_defined
-  exact inv
+    simpa [inv_mem_iff]
+  exact generator_well_defined _ _ inv
 
 lemma prop_Frob : (α ^ q - (galRestrict A K L B Frob) α) ∈ Q :=
   Classical.choose_spec (pow_q_conjugate P Q_ne_bot)
@@ -824,11 +810,9 @@ lemma is_zero_pow_gen_mod_Q (h : α ∈ (Frob⁻¹ • Q)) :
   rw [← Ideal.neg_mem_iff] at h1
   have h3 : ((α ^ q - (galRestrict A K L B Frob) α) -
       (-(galRestrict A K L B Frob) α)) ∈ Q := by
-    apply Ideal.sub_mem
-    · exact h2
-    · exact h1
+    exact Ideal.sub_mem Q h2 h1
   convert h3
-  simp only [sub_neg_eq_add, sub_add_cancel]
+  simp [sub_neg_eq_add, sub_add_cancel]
 
 /-- `Frob ∈ decomposition_subgroup_Ideal'  A K L B Q`. -/
 theorem Frob_is_in_decompositionSubgroup :
@@ -846,13 +830,12 @@ lemma γ_not_in_Q_is_pow_gen {γ : B} (h : γ ∉ Q) :  ∃ (i : ℕ), γ - (α
    let g :=  Units.mk0 (((Ideal.Quotient.mk Q γ))) <| by
     intro h1
     rw [Ideal.Quotient.eq_zero_iff_mem] at h1
-    apply h
-    exact h1
+    exact h h1
    rcases generator_mem_submonoid_powers Q_ne_bot g with ⟨i, hi⟩
    use i
    rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem]
-   simp only [g, Units.ext_iff, Units.val_pow_eq_pow_val, IsUnit.unit_spec, Units.val_mk0] at hi
-   simp only [g, map_pow, hi]
+   simp [g, Units.ext_iff, Units.val_pow_eq_pow_val, IsUnit.unit_spec, Units.val_mk0] at hi
+   simp [g, map_pow, hi]
 
 /--`i' : ℕ` such that, for `(γ : B) (h : γ ∉ Q)`, `γ - (α ^ i) ∈ Q`. -/
 noncomputable def i' {γ : B} (h : γ ∉ Q) : ℕ :=
@@ -868,12 +851,11 @@ lemma eq_pow_gen_apply {γ : B} (h: γ ∉ Q) : (galRestrict A K L B Frob) γ -
     galRestrict A K L B Frob (α ^ (i h)) ∈ Q := by
   rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem]
   have h1 : γ - (α ^ (i h)) ∈ Q := prop_γ_not_in_Q_is_pow_gen Q_ne_bot h
-  rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem] at h1
+  rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.Quotient.eq] at h1
   rw [Ideal.Quotient.eq, ← map_sub]
-  rw [Ideal.Quotient.eq] at h1
   have := Frob_is_in_decompositionSubgroup P Q_ne_bot
   rw [mem_decomposition_iff] at this
-  apply (this _).1 h1
+  exact (this _).1 h1
 
 -- γ ∈ B \ Q is α^i mod Q
 /-- `Frob • (α ^ i)  ≡ α ^ (i * q) mod Q` -/
@@ -910,10 +892,7 @@ theorem Frob_γ_not_in_Q_is_pow {γ : B} (h : γ ∉ Q) :
     · exact h3
   simp only [map_pow, sub_sub_sub_cancel_right] at h5
   have h6 : (( (((galRestrict A K L B) Frob)) γ - α ^ (i h * q)) +
-      (((α ^ ((i h) * q)) - (γ ^ q)))) ∈ Q := by
-    apply Ideal.add_mem
-    · exact h5
-    · exact h4
+      (((α ^ ((i h) * q)) - (γ ^ q)))) ∈ Q := Ideal.add_mem _ h5 h4
   simp only [sub_add_sub_cancel] at h6
   rw [← Ideal.neg_mem_iff] at h6
   simp only [neg_sub] at h6