awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
ζ : ↥(torsion K)
hζ : Function.Surjective.{1, u_1 + 1} (β := ↥(torsion K)) fun (x : ℤ) ↦ ζ ^ x
⊢ ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))
have refine_2 : ∀
  (h :
    Function.Surjective (α := (𝓞 K)ˣ) (β := ↥(torsion K)) (⇑(unitsMulComplexConjInv K) : (a : (𝓞 K)ˣ) → ↥(torsion K)))
  (ζ : ↥(torsion K)) (hζ : Function.Surjective.{1, u_1 + 1} (β := ↥(torsion K)) fun (x : ℤ) ↦ ζ ^ x),
  ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))
Tactic: rw [Subgroup.index_eq_one, MonoidHom.range_eq_top] at h
Cleared hypotheses: h, ζ, hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h : Function.Surjective (α := (𝓞 K)ˣ) (β := ↥(torsion K)) (⇑(unitsMulComplexConjInv K) : (a : (𝓞 K)ˣ) → ↥(torsion K))
ζ : ↥(torsion K)
hζ : Function.Surjective.{1, u_1 + 1} (β := ↥(torsion K)) fun (x : ℤ) ↦ ζ ^ x
⊢ ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))
have refine_2 : ∀ (u : (𝓞 K)ˣ)
  (hζ :
    Function.Surjective.{1, u_1 + 1} (β := ↥(torsion K)) fun (x : ℤ) ↦
      HPow.hPow (α := ↥(torsion K)) ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u : ↥(torsion K)) x),
  ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))
Tactic: obtain ⟨u, rfl⟩ := h ζ
Cleared hypotheses: ζ, hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)
    (realUnits K ⊔ torsion K)
have this : Subgroup.map (Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) (torsion ↥K⁺) ≤ torsion K
Tactic: have : Subgroup.map (Units.map (algebraMap (𝓞 K⁺) (𝓞 K))) (torsion K⁺) ≤ torsion K := by
    rintro _ ⟨x, hx, rfl⟩
    exact MonoidHom.isOfFinOrder _ hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this : Subgroup.map (Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) (torsion ↥K⁺) ≤ torsion K
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)
    (realUnits K ⊔ torsion K)
have rw : Eq (α := Subgroup (𝓞 K)ˣ) (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)
  (Subgroup.closure
      (Set.image (α := (𝓞 ↥K⁺)ˣ) (⇑(Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ)
        (Set.range (ι := Fin (rank.{u_1} ↥K⁺)) (fundSystem ↥K⁺))) ⊔
    torsion K)
Tactic: rw [realUnits, MonoidHom.range_eq_map, ← closure_fundSystem_sup_torsion_eq_top, Subgroup.map_sup,
    sup_assoc, RingHom.toMonoidHom_eq_coe, sup_eq_right.mpr this, MonoidHom.map_closure]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this : Subgroup.map (Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) (torsion ↥K⁺) ≤ torsion K
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)
    (Subgroup.closure
        (Set.image (α := (𝓞 ↥K⁺)ˣ) (⇑(Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ)
          (Set.range (ι := Fin (rank.{u_1} ↥K⁺)) (fundSystem ↥K⁺))) ⊔
      torsion K)
have e_a : Eq (α := Set (𝓞 K)ˣ) (Set.range (ι := Fin (rank K)) (realFundSystem K))
  (Set.image (α := (𝓞 ↥K⁺)ˣ) (⇑(Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ)
    (Set.range (ι := Fin (rank.{u_1} ↥K⁺)) (fundSystem ↥K⁺)))
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this : Subgroup.map (Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) (torsion ↥K⁺) ≤ torsion K
⊢ Eq (α := Set (𝓞 K)ˣ) (Set.range (ι := Fin (rank K)) (realFundSystem K))
    (Set.image (α := (𝓞 ↥K⁺)ˣ) (⇑(Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ)
      (Set.range (ι := Fin (rank.{u_1} ↥K⁺)) (fundSystem ↥K⁺)))
have e_a : ∀ (x : (𝓞 K)ˣ),
  Membership.mem (γ := Set (𝓞 K)ˣ) (Set.range (ι := Fin (rank K)) (realFundSystem K)) x ↔
    Membership.mem (γ := Set (𝓞 K)ˣ)
      (Set.image (α := (𝓞 ↥K⁺)ˣ) (⇑(Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ)
        (Set.range (ι := Fin (rank.{u_1} ↥K⁺)) (fundSystem ↥K⁺)))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀
w : InfinitePlace K
⊢ w ≠ W₀ ↔
    Ne (α := InfinitePlace ↥K⁺)
      ((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺) w : InfinitePlace ↥K⁺)
      (w₀ : InfinitePlace ↥K⁺)
have rw : w = W₀ ↔
  Eq (α := InfinitePlace ↥K⁺) ((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺) w : InfinitePlace ↥K⁺)
    (w₀ : InfinitePlace ↥K⁺)
Tactic: rw [not_iff_not, Equiv.eq_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀
w : InfinitePlace K
rw :
  w = W₀ ↔
    Eq (α := InfinitePlace ↥K⁺)
      ((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺) w : InfinitePlace ↥K⁺)
      (w₀ : InfinitePlace ↥K⁺)
⊢ w ≠ W₀ ↔
    Ne (α := InfinitePlace ↥K⁺)
      ((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺) w : InfinitePlace ↥K⁺)
      (w₀ : InfinitePlace ↥K⁺)
have rw₁ : Eq (α := InfinitePlace ↥K⁺) ((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺) w : InfinitePlace ↥K⁺)
    (w₀ : InfinitePlace ↥K⁺) ↔
  Eq (α := InfinitePlace ↥K⁺) ((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺) w : InfinitePlace ↥K⁺)
    (w₀ : InfinitePlace ↥K⁺)
Tactic: rw [not_iff_not, Equiv.eq_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀
f : { w : InfinitePlace K // w ≠ W₀ } ≃ { w : InfinitePlace ↥K⁺ // w ≠ w₀ } :=
  Equiv.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ W₀) (q := fun (w : InfinitePlace ↥K⁺) ↦ w ≠ w₀)
    (equivInfinitePlace K) ⋯
g : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ W₀ } := Equiv.trans (Equiv.trans (finCongr ⋯) (equivFinRank ↥K⁺)) f.symm
⊢ HPow.hPow (α := ℝ) 2 (rank K) = |∏ w : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }, 2|
have rw : HPow.hPow (α := ℝ) 2 (Fintype.card.{u_1} (InfinitePlace ↥K⁺) - 1) =
  HPow.hPow (α := ℝ) 2 (Finset.card.{u_1} (α := { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) Finset.univ)
Tactic: rw [Finset.prod_const, abs_pow, abs_of_pos zero_lt_two, ← units_rank_eq_units_rank K, rank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀
f : { w : InfinitePlace K // w ≠ W₀ } ≃ { w : InfinitePlace ↥K⁺ // w ≠ w₀ } :=
  Equiv.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ W₀) (q := fun (w : InfinitePlace ↥K⁺) ↦ w ≠ w₀)
    (equivInfinitePlace K) ⋯
g : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ W₀ } := Equiv.trans (Equiv.trans (finCongr ⋯) (equivFinRank ↥K⁺)) f.symm
⊢ regOfFamily (realFundSystem K) = HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺
have rw : regOfFamily (realFundSystem K) = |∏ w : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }, 2| * regulator.{u_1} ↥K⁺
Tactic: rw [show (2 : ℝ) ^ rank K = |∏ w : {w : InfinitePlace K⁺ // w ≠ w₀}, 2| by
    rw [Finset.prod_const, abs_pow, abs_of_pos zero_lt_two, ← units_rank_eq_units_rank K, rank]
    simp]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
let let₁ let₂ let₃ let₄ : regOfFamily (realFundSystem K) = HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺
⊢ regOfFamily (realFundSystem K) = HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺
have let₅ : regOfFamily (realFundSystem K) = |∏ w : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }, 2| * regulator.{u_1} ↥K⁺
Tactic: classical
  let W₀ := (equivInfinitePlace K).symm w₀
  let f : {w : InfinitePlace K // w ≠ W₀} ≃ {w : InfinitePlace K⁺ // w ≠ w₀} :=
    (equivInfinitePlace K).subtypeEquiv fun w ↦ by rw [not_iff_not, Equiv.eq_symm_apply]
  let g := ((finCongr (units_rank_eq_units_rank K).symm).trans (equivFinRank K⁺)).trans f.symm
  rw [show (2 : ℝ) ^ rank K = |∏ w : {w : InfinitePlace K⁺ // w ≠ w₀}, 2| by
    rw [Finset.prod_const, abs_pow, abs_of_pos zero_lt_two, ← units_rank_eq_units_rank K, rank]
    simp]
  rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_eq_det _ W₀ g.symm, regOfFamily_eq_det',
    ← abs_mul, ← Matrix.det_mul_column, ← Matrix.det_reindex_self f, Matrix.reindex_apply]
  congr; ext i w
  rw [Matrix.submatrix_apply, Matrix.of_apply, Matrix.of_apply,
    show f.symm w = (equivInfinitePlace K).symm w.1 by rfl,
    show algebraMap (𝓞 K) K _ = algebraMap K⁺ K _ by rfl, equivInfinitePlace_symm_apply]
  simp [f, g]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (↑(indexRealUnits K) : ℝ)⁻¹
have rw : regulator K / regulator.{u_1} ↥K⁺ =
  HPow.hPow (α := ℝ) 2 (rank K) * (↑(Subgroup.index (G := (𝓞 K)ˣ) (realUnits K ⊔ torsion K)) : ℝ)⁻¹
Tactic: rw [indexRealUnits, ← closure_realFundSystem_sup_torsion, ← regOfFamily_div_regulator
    (realFundSystem K), regOfFamily_realFunSystem, inv_div, ← mul_div_assoc, mul_div_mul_comm,
    div_self (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
rw :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (↑(Subgroup.index (G := (𝓞 K)ˣ) (realUnits K ⊔ torsion K)) : ℝ)⁻¹
⊢ regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (↑(indexRealUnits K) : ℝ)⁻¹
have rw₁ : regulator K / regulator.{u_1} ↥K⁺ =
  HPow.hPow (α := ℝ) 2 (rank K) *
    (↑(Subgroup.index (G := (𝓞 K)ˣ) (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)) :
        ℝ)⁻¹
Tactic: rw [indexRealUnits, ← closure_realFundSystem_sup_torsion, ← regOfFamily_div_regulator
    (realFundSystem K), regOfFamily_realFunSystem, inv_div, ← mul_div_assoc, mul_div_mul_comm,
    div_self (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
rw :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (↑(Subgroup.index (G := (𝓞 K)ˣ) (realUnits K ⊔ torsion K)) : ℝ)⁻¹
rw₁ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) *
      (↑(Subgroup.index (G := (𝓞 K)ˣ)
              (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)) :
          ℝ)⁻¹
⊢ regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (↑(indexRealUnits K) : ℝ)⁻¹
have rw₂ : regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (regOfFamily (realFundSystem K) / regulator K)⁻¹
Tactic: rw [indexRealUnits, ← closure_realFundSystem_sup_torsion, ← regOfFamily_div_regulator
    (realFundSystem K), regOfFamily_realFunSystem, inv_div, ← mul_div_assoc, mul_div_mul_comm,
    div_self (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
rw :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (↑(Subgroup.index (G := (𝓞 K)ˣ) (realUnits K ⊔ torsion K)) : ℝ)⁻¹
rw₁ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) *
      (↑(Subgroup.index (G := (𝓞 K)ˣ)
              (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)) :
          ℝ)⁻¹
rw₂ :
  regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (regOfFamily (realFundSystem K) / regulator K)⁻¹
⊢ regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (↑(indexRealUnits K) : ℝ)⁻¹
have rw₃ : regulator K / regulator.{u_1} ↥K⁺ =
  HPow.hPow (α := ℝ) 2 (rank K) * (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺ / regulator K)⁻¹
Tactic: rw [indexRealUnits, ← closure_realFundSystem_sup_torsion, ← regOfFamily_div_regulator
    (realFundSystem K), regOfFamily_realFunSystem, inv_div, ← mul_div_assoc, mul_div_mul_comm,
    div_self (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
rw :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (↑(Subgroup.index (G := (𝓞 K)ˣ) (realUnits K ⊔ torsion K)) : ℝ)⁻¹
rw₁ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) *
      (↑(Subgroup.index (G := (𝓞 K)ˣ)
              (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)) :
          ℝ)⁻¹
rw₂ :
  regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (regOfFamily (realFundSystem K) / regulator K)⁻¹
rw₃ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺ / regulator K)⁻¹
⊢ regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (↑(indexRealUnits K) : ℝ)⁻¹
have rw₄ : regulator K / regulator.{u_1} ↥K⁺ =
  HPow.hPow (α := ℝ) 2 (rank K) * (regulator K / (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺))
Tactic: rw [indexRealUnits, ← closure_realFundSystem_sup_torsion, ← regOfFamily_div_regulator
    (realFundSystem K), regOfFamily_realFunSystem, inv_div, ← mul_div_assoc, mul_div_mul_comm,
    div_self (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
rw :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (↑(Subgroup.index (G := (𝓞 K)ˣ) (realUnits K ⊔ torsion K)) : ℝ)⁻¹
rw₁ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) *
      (↑(Subgroup.index (G := (𝓞 K)ˣ)
              (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)) :
          ℝ)⁻¹
rw₂ :
  regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (regOfFamily (realFundSystem K) / regulator K)⁻¹
rw₃ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺ / regulator K)⁻¹
rw₄ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (regulator K / (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺))
⊢ regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (↑(indexRealUnits K) : ℝ)⁻¹
have rw₅ : regulator K / regulator.{u_1} ↥K⁺ =
  HPow.hPow (α := ℝ) 2 (rank K) * regulator K / (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺)
Tactic: rw [indexRealUnits, ← closure_realFundSystem_sup_torsion, ← regOfFamily_div_regulator
    (realFundSystem K), regOfFamily_realFunSystem, inv_div, ← mul_div_assoc, mul_div_mul_comm,
    div_self (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
rw :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (↑(Subgroup.index (G := (𝓞 K)ˣ) (realUnits K ⊔ torsion K)) : ℝ)⁻¹
rw₁ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) *
      (↑(Subgroup.index (G := (𝓞 K)ˣ)
              (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)) :
          ℝ)⁻¹
rw₂ :
  regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (regOfFamily (realFundSystem K) / regulator K)⁻¹
rw₃ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺ / regulator K)⁻¹
rw₄ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (regulator K / (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺))
rw₅ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * regulator K / (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺)
⊢ regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (↑(indexRealUnits K) : ℝ)⁻¹
have rw₆ : regulator K / regulator.{u_1} ↥K⁺ =
  HPow.hPow (α := ℝ) 2 (rank K) / HPow.hPow (α := ℝ) 2 (rank K) * (regulator K / regulator.{u_1} ↥K⁺)
Tactic: rw [indexRealUnits, ← closure_realFundSystem_sup_torsion, ← regOfFamily_div_regulator
    (realFundSystem K), regOfFamily_realFunSystem, inv_div, ← mul_div_assoc, mul_div_mul_comm,
    div_self (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
rw :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (↑(Subgroup.index (G := (𝓞 K)ˣ) (realUnits K ⊔ torsion K)) : ℝ)⁻¹
rw₁ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) *
      (↑(Subgroup.index (G := (𝓞 K)ˣ)
              (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)) :
          ℝ)⁻¹
rw₂ :
  regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (regOfFamily (realFundSystem K) / regulator K)⁻¹
rw₃ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺ / regulator K)⁻¹
rw₄ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (regulator K / (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺))
rw₅ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * regulator K / (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺)
rw₆ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) / HPow.hPow (α := ℝ) 2 (rank K) * (regulator K / regulator.{u_1} ↥K⁺)
⊢ regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (↑(indexRealUnits K) : ℝ)⁻¹
have rw₇ : regulator K / regulator.{u_1} ↥K⁺ = 1 * (regulator K / regulator.{u_1} ↥K⁺)
Tactic: rw [indexRealUnits, ← closure_realFundSystem_sup_torsion, ← regOfFamily_div_regulator
    (realFundSystem K), regOfFamily_realFunSystem, inv_div, ← mul_div_assoc, mul_div_mul_comm,
    div_self (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
rw :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (↑(Subgroup.index (G := (𝓞 K)ˣ) (realUnits K ⊔ torsion K)) : ℝ)⁻¹
rw₁ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) *
      (↑(Subgroup.index (G := (𝓞 K)ˣ)
              (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)) :
          ℝ)⁻¹
rw₂ :
  regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (regOfFamily (realFundSystem K) / regulator K)⁻¹
rw₃ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺ / regulator K)⁻¹
rw₄ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * (regulator K / (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺))
rw₅ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) * regulator K / (HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺)
rw₆ :
  regulator K / regulator.{u_1} ↥K⁺ =
    HPow.hPow (α := ℝ) 2 (rank K) / HPow.hPow (α := ℝ) 2 (rank K) * (regulator K / regulator.{u_1} ↥K⁺)
rw₇ : regulator K / regulator.{u_1} ↥K⁺ = 1 * (regulator K / regulator.{u_1} ↥K⁺)
⊢ regulator K / regulator.{u_1} ↥K⁺ = HPow.hPow (α := ℝ) 2 (rank K) * (↑(indexRealUnits K) : ℝ)⁻¹
have rw₈ : regulator K / regulator.{u_1} ↥K⁺ = regulator K / regulator.{u_1} ↥K⁺
Tactic: rw [indexRealUnits, ← closure_realFundSystem_sup_torsion, ← regOfFamily_div_regulator
    (realFundSystem K), regOfFamily_realFunSystem, inv_div, ← mul_div_assoc, mul_div_mul_comm,
    div_self (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
⊢ E = maximalRealSubfield K
have refine : maximalRealSubfield K ≤ E
Tactic: refine le_antisymm (IsTotallyReal.le_maximalRealSubfield E) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
⊢ maximalRealSubfield K ≤ E
have by_contra! : ∀ (h : ¬maximalRealSubfield K ≤ E), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
⊢ E ⊔ maximalRealSubfield K = ⊤
have refine_2 : ∀ (this : L = ⊤), E ⊔ maximalRealSubfield K = ⊤
Tactic: have := ((IntermediateField.isSimpleOrder_of_finrank_prime E K
      (IsQuadraticExtension.finrank_eq_two E K ▸ Nat.prime_two)).eq_bot_or_eq_top L).resolve_left ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
refine_2 : ∀ (this : L = ⊤), E ⊔ maximalRealSubfield K = ⊤
⊢ E ⊔ maximalRealSubfield K = ⊤
have refine_1 : ¬L = ⊥
Tactic: have := ((IntermediateField.isSimpleOrder_of_finrank_prime E K
      (IsQuadraticExtension.finrank_eq_two E K ▸ Nat.prime_two)).eq_bot_or_eq_top L).resolve_left ?_