bump

FltRegular/CaseI/AuxLemmas.lean

@@ -25,7 +25,7 @@ section Zerok₁
 
 theorem aux_cong0k₁ {k : Fin p} (hcong : k ≡ -1 [ZMOD p]) :
   k = ⟨p.pred, pred_lt hpri.ne_zero⟩ := by
-  refine' Fin.ext _
+  refine Fin.ext ?_
   rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
   suffices ((k : ℤ) : ZMod p).val = p.pred by simpa
   rw [← ZMod.intCast_eq_intCast_iff] at hcong
@@ -39,7 +39,7 @@ theorem aux_cong0k₁ {k : Fin p} (hcong : k ≡ -1 [ZMOD p]) :
 def f0k₁ (b : ℤ) (p : ℕ) : ℕ → ℤ := fun x => if x = 1 then b else if x = p.pred then -b else 0
 
 theorem auxf0k₁ (hp5 : 5 ≤ p) (b : ℤ) : ∃ i : Fin P, f0k₁ b p (i : ℕ) = 0 := by
-  refine' ⟨⟨2, two_lt hp5⟩, _⟩
+  refine ⟨⟨2, two_lt hp5⟩, ?_⟩
   have hpred : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ p.pred := by
     intro h
     simp only [Fin.ext_iff, Fin.val_mk] at h
@@ -67,7 +67,7 @@ theorem aux0k₁ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot 
       Finset.range_filter_eq]
     simp [hpri.one_lt, Nat.sub_lt hpri.pos, sub_eq_add_neg]
   rw [sum_range] at key
-  refine' caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_left _ _) _)
+  refine caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_left ?_ _) _)
   replace hpri : (P : ℕ).Prime := hpri
   simpa [f0k₁] using dvd_coeff_cycl_integer hpri hζ (auxf0k₁ hpri hp5 b) key ⟨1, hpri.one_lt⟩
 
@@ -79,7 +79,7 @@ section Zerok₂
 def f0k₂ (a b : ℤ) : ℕ → ℤ := fun x => if x = 0 then a - b else if x = 1 then b - a else 0
 
 theorem aux_cong0k₂ {k : Fin p} (hcong : k ≡ 1 [ZMOD p]) : k = ⟨1, hpri.one_lt⟩ := by
-  refine' Fin.ext _
+  refine Fin.ext ?_
   rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
   suffices ((k : ℤ) : ZMod p).val = 1 by simpa
   rw [← ZMod.intCast_eq_intCast_iff] at hcong
@@ -88,7 +88,7 @@ theorem aux_cong0k₂ {k : Fin p} (hcong : k ≡ 1 [ZMOD p]) : k = ⟨1, hpri.on
   simp [ZMod.val_one]
 
 theorem auxf0k₂ (hp5 : 5 ≤ p) (a b : ℤ) : ∃ i : Fin P, f0k₂ a b (i : ℕ) = 0 := by
-  refine' ⟨⟨2, two_lt hp5⟩, _⟩
+  refine ⟨⟨2, two_lt hp5⟩, ?_⟩
   have h1 : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ 1 := by
     intro h
     simp only [Fin.ext_iff, Fin.val_mk] at h; contradiction
@@ -115,7 +115,7 @@ theorem aux0k₂ {a b : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ
     simp only [hpri.pos, hpri.one_lt, if_true, zsmul_eq_mul, Int.cast_sub, sum_singleton,
       _root_.pow_zero, mul_one, pow_one, Ne, zero_smul, sum_const_zero, add_zero, Fin.val_mk]
   rw [sum_range] at key
-  refine' hab _
+  refine hab ?_
   symm
   rw [← ZMod.intCast_eq_intCast_iff, ZMod.intCast_eq_intCast_iff_dvd_sub]
   have hpri₁ : (P : ℕ).Prime := hpri
@@ -126,7 +126,7 @@ end Zerok₂
 section OnekOne
 
 theorem aux_cong1k₁ {k : Fin p} (hcong : k ≡ 0 [ZMOD p]) : k = ⟨0, hpri.pos⟩ := by
-  refine' Fin.ext _
+  refine Fin.ext ?_
   rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
   suffices ((k : ℤ) : ZMod p).val = 0 by simpa
   rw [← ZMod.intCast_eq_intCast_iff] at hcong
@@ -153,7 +153,7 @@ def f1k₂ (a : ℤ) : ℕ → ℤ := fun x => if x = 0 then a else if x = 2 the
 
 theorem aux_cong1k₂ {k : Fin p} (hpri : p.Prime) (hp5 : 5 ≤ p) (hcong : k ≡ 1 + 1 [ZMOD p]) :
     k = ⟨2, two_lt hp5⟩ := by
-  refine' Fin.ext _
+  refine Fin.ext ?_
   rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
   suffices ((k : ℤ) : ZMod p).val = 2 by simpa
   rw [← ZMod.intCast_eq_intCast_iff] at hcong
@@ -167,15 +167,9 @@ theorem aux_cong1k₂ {k : Fin p} (hpri : p.Prime) (hp5 : 5 ≤ p) (hcong : k 
   linarith
 
 theorem auxf1k₂ (a : ℤ) : ∃ i : Fin P, f1k₂ a (i : ℕ) = 0 := by
-  refine' ⟨⟨1, hpri.one_lt⟩, _⟩
-  have h2 : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 2 :=
-    by
-    intro h
-    simp only [Fin.ext_iff, Fin.val_mk] at h; contradiction
-  have hzero : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 0 :=
-    by
-    intro h
-    simp only [Fin.ext_iff, Fin.val_mk] at h
+  refine ⟨⟨1, hpri.one_lt⟩, ?_⟩
+  have h2 : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 2 := fun h ↦ by simp at h
+  have hzero : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 0 := fun h ↦ by simp at h
   simp only [f1k₂, h2, if_false, hzero, one_lt_two.ne]
 
 theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p)
@@ -198,7 +192,7 @@ theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot 
   sum_neg_distrib, ne_eq, mem_range, not_and, not_not, zero_smul, sum_const_zero, add_zero]
     ring
   rw [sum_range] at key
-  refine' caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right _ _) _)
+  refine caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right ?_ _) _)
   have hpri₁ : (P : ℕ).Prime := hpri
   simpa [f1k₂] using dvd_coeff_cycl_integer hpri₁ hζ (auxf1k₂ hpri a) key ⟨0, hpri.pos⟩
 

FltRegular/CaseI/Statement.lean

@@ -36,8 +36,7 @@ theorem may_assume : SlightlyEasier → Statement := by
   have hodd : p ≠ 2 := by
     intro h
     rw [h] at H hI
-    refine' hI _
-    refine' Dvd.dvd.mul_left _ _
+    refine hI <| Dvd.dvd.mul_left ?_ _
     simp only [Nat.cast_ofNat] at hI ⊢
     rw [← even_iff_two_dvd, ← Int.odd_iff_not_even] at hI
     rw [← even_iff_two_dvd, ← Int.even_pow' (show 2 ≠ 0 by norm_num), ← H]
@@ -53,7 +52,7 @@ theorem may_assume : SlightlyEasier → Statement := by
     fin_cases this
     · exact MayAssume.p_ne_three hprod H rfl
     · rw [show 2 + 1 + 1 = 2 * 2 from rfl] at hpri
-      refine' Nat.not_prime_mul one_lt_two.ne' one_lt_two.ne' hpri.out
+      exact Nat.not_prime_mul one_lt_two.ne' one_lt_two.ne' hpri.out
   rcases MayAssume.coprime H hprod with ⟨Hxyz, hunit, hprodxyx⟩
   let d := ({a, b, c} : Finset ℤ).gcd id
   have hdiv : ¬↑p ∣ a / d * (b / d) * (c / d) :=
@@ -90,7 +89,7 @@ theorem ab_coprime {a b c : ℤ} (H : a ^ p + b ^ p = c ^ p) (hpzero : p ≠ 0)
     rw [← H]
     exact dvd_add (dvd_pow haq hpzero) (dvd_pow hbq hpzero)
   have Hq : ↑q ∣ ({a, b, c} : Finset ℤ).gcd id := by
-    refine' dvd_gcd fun x hx => _
+    refine dvd_gcd fun x hx ↦ ?_
     simp only [mem_insert, mem_singleton] at hx
     rcases hx with (H | H | H) <;> simpa [H]
   rw [hgcd] at Hq
@@ -108,8 +107,8 @@ theorem exists_ideal {a b c : ℤ} (h5p : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p)
     (hpri.out.eq_two_or_odd.resolve_left fun h => by simp [h] at h5p) hζ'] at H₁
   replace H₁ := congr_arg (fun x => span ({ x } : Set R)) H₁
   simp only [← prod_span_singleton, ← span_singleton_pow] at H₁
-  refine' Finset.exists_eq_pow_of_mul_eq_pow_of_coprime (fun η₁ hη₁ η₂ hη₂ hη => ?_) H₁ ζ hζ
-  refine' fltIdeals_coprime _ _ H (ab_coprime H hpri.out.ne_zero hgcd) hη₁ hη₂ hη caseI
+  refine exists_eq_pow_of_mul_eq_pow_of_coprime (fun η₁ hη₁ η₂ hη₂ hη => ?_) H₁ ζ hζ
+  refine fltIdeals_coprime ?_ ?_ H (ab_coprime H hpri.out.ne_zero hgcd) hη₁ hη₂ hη caseI
   · exact hpri.out
   · exact h5p
 
@@ -127,7 +126,7 @@ theorem is_principal_aux (K' : Type*) [Field K'] [CharZero K'] [IsCyclotomicExte
   replace hα := congr_arg (fun (J : Submodule _ _) => J ^ p) hα
   simp only [← hI, submodule_span_eq, span_singleton_pow, span_singleton_eq_span_singleton] at hα
   obtain ⟨u, hu⟩ := hα
-  refine' ⟨u⁻¹, α, _⟩
+  refine ⟨u⁻¹, α, ?_⟩
   rw [← hu, mul_comm ((_ + ζ * _)), ← mul_assoc]
   simp only [Units.inv_mul, one_mul]
 
@@ -161,10 +160,10 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
   obtain ⟨k, hk⟩ := FltRegular.CaseI.exists_int_sum_eq_zero hζ' hP hpri.out a b 1 hu.symm
   simp only [zpow_one, zpow_neg, PNat.mk_coe, mem_span_singleton, ← h] at hk
   have hpcoe : (p : ℤ) ≠ 0 := by simp [hpri.out.ne_zero]
-  refine' ⟨⟨(2 * k % p).natAbs, _⟩, ⟨((2 * k - 1) % p).natAbs, _⟩, _, _⟩
+  refine ⟨⟨(2 * k % p).natAbs, ?_⟩, ⟨((2 * k - 1) % p).natAbs, ?_⟩, ?_, ?_⟩
   repeat'
     rw [← natAbs_ofNat p]
-    refine' natAbs_lt_natAbs_of_nonneg_of_lt (emod_nonneg _ hpcoe) _
+    refine natAbs_lt_natAbs_of_nonneg_of_lt (emod_nonneg _ hpcoe) ?_
     rw [natAbs_ofNat]
     exact emod_lt_of_pos _ (by simp [hpri.out.pos])
   · simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_eq_intCast_iff,
@@ -197,7 +196,7 @@ theorem auxf' (hp5 : 5 ≤ p) (a b : ℤ) (k₁ k₂ : Fin p) :
   have h1 : 1 < p := by linarith
   let s := ({0, 1, k₁.1, k₂.1} : Finset ℕ)
   have : s.card ≤ 4 := by
-    repeat refine' le_trans (card_insert_le _ _) (succ_le_succ _)
+    repeat refine le_trans (card_insert_le _ _) (succ_le_succ ?_)
     exact rfl.ge
   replace this : s.card < 5 := lt_of_le_of_lt this (by norm_num)
   have hs : s ⊆ range p := insert_subset_iff.2 ⟨mem_range.2 h0, insert_subset_iff.2
@@ -208,7 +207,7 @@ theorem auxf' (hp5 : 5 ≤ p) (a b : ℤ) (k₁ k₂ : Fin p) :
     rw [← Finset.card_pos, hcard, card_range]
     exact Nat.sub_pos_of_lt (lt_of_lt_of_le this hp5)
   obtain ⟨i, hi⟩ := hcard
-  refine' ⟨i, sdiff_subset hi, _⟩
+  refine ⟨i, sdiff_subset hi, ?_⟩
   have hi0 : i ≠ 0 := fun h => by simp [h, s] at hi
   have hi1 : i ≠ 1 := fun h => by simp [h, s] at hi
   have hik₁ : i ≠ k₁ := fun h => by simp [h, s] at hi
@@ -246,7 +245,7 @@ theorem caseI_easier {a b c : ℤ} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p)
       add_zero]
     ring
   rw [sum_range] at key
-  refine' caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right _ _) _)
+  refine caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right ?_ _) _)
   simpa [f] using dvd_coeff_cycl_integer (by exact hpri.out) hζ (auxf hp5 a b k₁ k₂) key
     ⟨0, hpri.out.pos⟩
 

FltRegular/CaseII/AuxLemmas.lean

@@ -59,7 +59,7 @@ lemma dvd_iff_multiplicity_le {M : Type*}
     · simp only [ne_eq, mul_eq_zero, not_or] at ha
       rw [UniqueFactorizationMonoid.irreducible_iff_prime] at hq
       obtain ⟨c, rfl⟩ : a ∣ b := by
-        refine' IH ha.2 (fun p hp ↦ (le_trans ?_ (H p hp)))
+        refine IH ha.2 (fun p hp ↦ (le_trans ?_ (H p hp)))
         rw [multiplicity.mul hp]
         exact le_add_self
       rw [mul_comm]

FltRegular/MayAssume/Lemmas.lean

@@ -31,7 +31,7 @@ theorem coprime {a b c : ℤ} {n : ℕ} (H : a ^ n + b ^ n = c ^ n) (hprod : a *
   have hdzero : d ≠ 0 := fun hdzero => by
     simpa [ha] using Finset.gcd_eq_zero_iff.1 hdzero a (by simp [s])
   have hdp : d ^ n ≠ 0 := fun hdn => hdzero (pow_eq_zero hdn)
-  refine' ⟨_, _, fun habs => _⟩
+  refine ⟨?_, ?_, fun habs => ?_⟩
   · obtain ⟨na, hna⟩ := hadiv; obtain ⟨nb, hnb⟩ := hbdiv; obtain ⟨nc, hnc⟩ := hcdiv
     rwa [← mul_left_inj' hdp, add_mul, ← mul_pow, ← mul_pow, ← mul_pow, hna, hnb, hnc,
       Int.mul_ediv_cancel_left _ hdzero, Int.mul_ediv_cancel_left _ hdzero,
@@ -58,7 +58,7 @@ theorem p_dvd_c_of_ab_of_anegc {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp : p
   simp only [Int.cast_neg, Int.cast_mul, Int.cast_one, Int.cast_ofNat, neg_eq_zero,
     mul_eq_zero] at h
   rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]
-  refine' Or.resolve_right h fun h3 => _
+  refine Or.resolve_right h fun h3 => ?_
   rw [show (3 : ZMod p) = ((3 : ℕ) : ZMod p) by simp, ZMod.natCast_zmod_eq_zero_iff_dvd,
     Nat.dvd_prime Nat.prime_three] at h3
   cases' h3 with H₁ H₂
@@ -73,7 +73,7 @@ theorem a_not_cong_b {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp5 : 5 ≤ p) (h
   by_cases H : a ≡ b [ZMOD p]
   swap
   · exact ⟨a, b, c, ⟨h, hgcd, H, hprod, caseI⟩⟩
-  refine' ⟨a, -c, -b, ⟨_, _, fun habs => _, _, _⟩⟩
+  refine ⟨a, -c, -b, ⟨?_, ?_, fun habs => ?_, ?_, ?_⟩⟩
   · have hpodd : p ≠ 2 := by linarith
     rw [neg_pow, (Or.resolve_left hpri.eq_two_or_odd' hpodd).neg_one_pow, neg_pow,
       (Or.resolve_left hpri.eq_two_or_odd' hpodd).neg_one_pow]
@@ -83,7 +83,7 @@ theorem a_not_cong_b {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp5 : 5 ≤ p) (h
     exact h.symm
   · convert hgcd using 1
     have : ({a, -c, -b} : Finset ℤ) = {a, -b, -c} := by
-      refine' Finset.ext fun x => ⟨fun hx => _, fun hx => _⟩ <;>
+      refine Finset.ext fun x => ⟨fun hx => ?_, fun hx => ?_⟩ <;>
         · simp only [mem_insert, mem_singleton] at hx
           rcases hx with (H | H | H) <;> simp [H]
     rw [this]
@@ -102,7 +102,7 @@ theorem a_not_cong_b {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp5 : 5 ≤ p) (h
     rw [H] at habs
     rw [ZMod.intCast_eq_intCast_iff] at habs H
     obtain ⟨n, hn⟩ := p_dvd_c_of_ab_of_anegc hpri hp3 h H habs
-    refine' caseI ⟨a * b * n, _⟩
+    refine caseI ⟨a * b * n, ?_⟩
     rw [hn]
     ring
   · convert hprod using 1

FltRegular/NumberTheory/AuxLemmas.lean

@@ -85,7 +85,7 @@ lemma isIntegrallyClosed_of_isLocalization {R} [CommRing R] [IsIntegrallyClosed
   intro hx
   obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _
   obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp ‹_› hy
-  refine' ⟨IsLocalization.mk' S z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr _⟩
+  refine ⟨IsLocalization.mk' S z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr ?_⟩
   rw [RingHom.comp_id, hz, ← Algebra.smul_def]
   rfl
 

FltRegular/NumberTheory/Cyclotomic/CaseI.lean

@@ -48,7 +48,7 @@ theorem exists_int_sum_eq_zero' (hpodd : p ≠ 2) (hp : (p : ℕ).Prime) (x y i
   letI : NumberField K := IsCyclotomicExtension.numberField { p } ℚ _
   have : Fact (p : ℕ).Prime := ⟨hp⟩
   obtain ⟨k, H⟩ := unit_inv_conj_is_root_of_unity hζ hpodd hp u
-  refine' ⟨k, _⟩
+  refine ⟨k, ?_⟩
   rw [← exists_int_sum_eq_zero'_aux, h, ← H, Units.val_mul, mul_assoc, ← mul_sub, _root_.map_mul,
     ← coe_unitGalConj, ← mul_assoc, ← Units.val_mul, inv_mul_self, Units.val_one, one_mul]
   exact Ideal.mul_mem_left _ _ (pow_sub_intGalConj_mem hp α)

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -27,7 +27,7 @@ open Ideal IsCyclotomicExtension
 theorem exists_int_sub_pow_prime_dvd {A : Type _} [CommRing A] [IsCyclotomicExtension {p} ℤ A]
     [hp : Fact (p : ℕ).Prime] (a : A) : ∃ m : ℤ, a ^ (p : ℕ) - m ∈ span ({(p : A)} : Set A) := by
   have : a ∈ Algebra.adjoin ℤ _ := @adjoin_roots {p} ℤ A _ _ _ _ a
-  refine' Algebra.adjoin_induction this _ _ _ _
+  refine Algebra.adjoin_induction this ?_ ?_ ?_ ?_
   · intro x hx
     rcases hx with ⟨hx_w, hx_m, hx_p⟩
     simp only [Set.mem_singleton_iff] at hx_m
@@ -98,7 +98,7 @@ theorem not_coprime_not_top {S : Type _} [CommRing S] (a b : Ideal S) :
   rw [hxy]
   simp
   intro h
-  refine' ⟨1, 1, _⟩
+  refine ⟨1, 1, ?_⟩
   simp only [one_eq_top, top_mul, Submodule.add_eq_sup, ge_iff_le]
   rw [← h]
   rfl
@@ -176,19 +176,13 @@ theorem diff_of_roots [hp : Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η₁ η₂ :
   obtain ⟨u, hu⟩ :=
     CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one R ph hp.out hp.out.one_lt H
       hi1 h
-  refine' ⟨u, _⟩
-  rw [← hu, hi, pow_one]
+  exact ⟨u, by rw [← hu, hi, pow_one]⟩
 
 theorem diff_of_roots2 [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η₁ η₂ : R} (hη₁ : η₁ ∈ nthRootsFinset p R)
     (hη₂ : η₂ ∈ nthRootsFinset p R) (hdiff : η₁ ≠ η₂) (hwlog : η₁ ≠ 1) :
     ∃ u : Rˣ, η₂ - η₁ = u * (1 - η₁) := by
   obtain ⟨u, hu⟩ := diff_of_roots ph hη₁ hη₂ hdiff hwlog
-  refine' ⟨-u, _⟩
-  rw [Units.val_neg, neg_mul, ← hu]
-  ring
-
-noncomputable
-instance : AddCommGroup R := AddCommGroupWithOne.toAddCommGroup
+  exact ⟨-u, by simp [← hu]⟩
 
 lemma fltIdeals_coprime2_lemma [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {x y : ℤ} {η₁ η₂ : R}
     (hη₁ : η₁ ∈ nthRootsFinset p R)
@@ -273,7 +267,7 @@ lemma fltIdeals_coprime2_lemma [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {x y : ℤ}
       rw [H3] at H1
       have H4 : -↑y * (1 - η₁) ∈ P := by
         rw [← hηP]; rw [Ideal.mem_span_singleton']
-        refine' ⟨-(y : R), rfl⟩
+        exact ⟨-(y : R), rfl⟩
       apply (Ideal.add_mem_iff_left P H4).1 H1
     have hxyinP2 : x + y ∈ Ideal.span ({(p : ℤ)} : Set ℤ) := by rw [← hcapZ]; simp [hxyinP]
     rw [mem_span_singleton] at hxyinP2

FltRegular/NumberTheory/Cyclotomic/CyclotomicUnits.lean

@@ -44,7 +44,7 @@ theorem associated_one_sub_pow_primitive_root_of_coprime {n j k : ℕ} {ζ : A}
     exact (this hj).symm.trans (this hk)
   clear k j hk hj
   intro j hj
-  refine' associated_of_dvd_dvd ⟨∑ i in range j, ζ ^ i, by rw [← geom_sum_mul_neg, mul_comm]⟩ _
+  refine associated_of_dvd_dvd ⟨∑ i in range j, ζ ^ i, by rw [← geom_sum_mul_neg, mul_comm]⟩ ?_
   -- is there an easier way to do this?
   rcases eq_or_ne n 0 with (rfl | hn')
   · simp [j.coprime_zero_right.mp hj]

FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean

@@ -62,9 +62,7 @@ theorem conj_norm_one (x : ℂ) (h : Complex.abs x = 1) : conj x = x⁻¹ := by
     Complex.exp_neg, map_mul, Complex.conj_I, mul_neg, Complex.conj_ofReal]
 
 @[simp]
-theorem embedding_conj (x : K) (φ : K →+* ℂ) : conj (φ x) = φ (galConj K p x) :=
-  by
-  -- dependent type theory is my favourite
+theorem embedding_conj (x : K) (φ : K →+* ℂ) : conj (φ x) = φ (galConj K p x) := by
   change RingHom.comp conj φ x = (φ.comp <| ↑(galConj K p)) x
   revert x
   suffices φ (galConj K p ζ) = conj (φ ζ)
@@ -74,8 +72,7 @@ theorem embedding_conj (x : K) (φ : K →+* ℂ) : conj (φ x) = φ (galConj K
     apply (hζ.powerBasis ℚ).rat_hom_ext
     exact this.symm
   rw [conj_norm_one, galConj_zeta_runity hζ, map_inv₀]
-  refine' Complex.norm_eq_one_of_pow_eq_one _ p.ne_zero
-  rw [← map_pow, hζ.pow_eq_one, map_one]
+  exact Complex.norm_eq_one_of_pow_eq_one (by rw [← map_pow, hζ.pow_eq_one, map_one]) p.ne_zero
 
 variable (p)