awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
M : Type u_3
inst_3 : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral.{0, u_1} ℤ (A := K) ((f : (a : M) → K) x : K)
x y : M
⊢ restrict (⇑f : (a : M) → K) h (x * y) = restrict (⇑f : (a : M) → K) h x * restrict (⇑f : (a : M) → K) h y
have simp : Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
    (HMul.hMul (α := K) (β := K) ((f : (a : M) → K) x : K) ((f : (a : M) → K) y : K)) sorry =
  HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) ((f : (a : M) → K) x)
        sorry :
      ↥(integralClosure ℤ K))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) ((f : (a : M) → K) y)
        sorry :
      ↥(integralClosure ℤ K))
Tactic: simp only [restrict, map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (hypothesis)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : 𝓞 K
hx : Eq.{u_5 + 1} (α := 𝓞 L) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x : 𝓞 L) (0 : 𝓞 L)
⊢ x = 0
have h : Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) (↑x : K) : L)
  ((↑((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x) : L) : L)
Tactic: have h : (algebraMap K L) x = (algebraMap (𝓞 K) (𝓞 L)) x := rfl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Basic (goal)
Goal:
z : 𝓞 ℚ
⊢ Eq (α := ℚ) ((↑((ringOfIntegersEquiv : (a : 𝓞 ℚ) → ℤ) z) : ℚ) : ℚ) ((algebraMap (𝓞 ℚ) ℚ : (a : 𝓞 ℚ) → ℚ) z : ℚ)
have obtain : ∀ (z : ℤ),
  Eq (α := ℚ) ((↑((ringOfIntegersEquiv : (a : 𝓞 ℚ) → ℤ) ((ringOfIntegersEquiv.symm : (a : ℤ) → 𝓞 ℚ) z : 𝓞 ℚ)) : ℚ) : ℚ)
    ((algebraMap (𝓞 ℚ) ℚ : (a : 𝓞 ℚ) → ℚ) ((ringOfIntegersEquiv.symm : (a : ℤ) → 𝓞 ℚ) z : 𝓞 ℚ) : ℚ)
Tactic: obtain ⟨z, rfl⟩ := Rat.ringOfIntegersEquiv.symm.surjective z
Cleared hypotheses: z
-- 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
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)
have rw : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]
-- 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 : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)
have rw₁ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = nrRealPlaces K + nrComplexPlaces K
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]
-- 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 : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
rw₁ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = nrRealPlaces K + nrComplexPlaces K
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)
have rw₂ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = 0 + nrComplexPlaces K
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]
-- 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 : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
rw₁ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = nrRealPlaces K + nrComplexPlaces K
rw₂ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = 0 + nrComplexPlaces K
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)
have rw₃ : nrRealPlaces.{u_1} ↥K⁺ + 0 = 0 + nrComplexPlaces K
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]
-- 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 : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
rw₁ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = nrRealPlaces K + nrComplexPlaces K
rw₂ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = 0 + nrComplexPlaces K
rw₃ : nrRealPlaces.{u_1} ↥K⁺ + 0 = 0 + nrComplexPlaces K
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)
have rw₄ : nrRealPlaces.{u_1} ↥K⁺ + 0 = nrComplexPlaces K
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]
-- 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 : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
rw₁ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = nrRealPlaces K + nrComplexPlaces K
rw₂ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = 0 + nrComplexPlaces K
rw₃ : nrRealPlaces.{u_1} ↥K⁺ + 0 = 0 + nrComplexPlaces K
rw₄ : nrRealPlaces.{u_1} ↥K⁺ + 0 = nrComplexPlaces K
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)
have rw₅ : nrRealPlaces.{u_1} ↥K⁺ = nrComplexPlaces K
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]
-- 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 : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
rw₁ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = nrRealPlaces K + nrComplexPlaces K
rw₂ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = 0 + nrComplexPlaces K
rw₃ : nrRealPlaces.{u_1} ↥K⁺ + 0 = 0 + nrComplexPlaces K
rw₄ : nrRealPlaces.{u_1} ↥K⁺ + 0 = nrComplexPlaces K
rw₅ : nrRealPlaces.{u_1} ↥K⁺ = nrComplexPlaces K
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)
have rw₆ : Module.finrank.{0, u_1} ℚ ↥K⁺ = nrComplexPlaces K
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]
-- 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 : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
rw₁ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = nrRealPlaces K + nrComplexPlaces K
rw₂ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = 0 + nrComplexPlaces K
rw₃ : nrRealPlaces.{u_1} ↥K⁺ + 0 = 0 + nrComplexPlaces K
rw₄ : nrRealPlaces.{u_1} ↥K⁺ + 0 = nrComplexPlaces K
rw₅ : nrRealPlaces.{u_1} ↥K⁺ = nrComplexPlaces K
rw₆ : Module.finrank.{0, u_1} ℚ ↥K⁺ = nrComplexPlaces K
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)
have rw₇ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = 2 * nrComplexPlaces K
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]
-- 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 : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
rw₁ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = nrRealPlaces K + nrComplexPlaces K
rw₂ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = 0 + nrComplexPlaces K
rw₃ : nrRealPlaces.{u_1} ↥K⁺ + 0 = 0 + nrComplexPlaces K
rw₄ : nrRealPlaces.{u_1} ↥K⁺ + 0 = nrComplexPlaces K
rw₅ : nrRealPlaces.{u_1} ↥K⁺ = nrComplexPlaces K
rw₆ : Module.finrank.{0, u_1} ℚ ↥K⁺ = nrComplexPlaces K
rw₇ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = 2 * nrComplexPlaces K
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)
have rw₈ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = Module.finrank ℚ K
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]
-- 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 : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
rw₁ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = nrRealPlaces K + nrComplexPlaces K
rw₂ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = 0 + nrComplexPlaces K
rw₃ : nrRealPlaces.{u_1} ↥K⁺ + 0 = 0 + nrComplexPlaces K
rw₄ : nrRealPlaces.{u_1} ↥K⁺ + 0 = nrComplexPlaces K
rw₅ : nrRealPlaces.{u_1} ↥K⁺ = nrComplexPlaces K
rw₆ : Module.finrank.{0, u_1} ℚ ↥K⁺ = nrComplexPlaces K
rw₇ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = 2 * nrComplexPlaces K
rw₈ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = Module.finrank ℚ K
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)
have rw₉ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = Module.finrank.{0, u_1} ℚ ↥K⁺ * Module.finrank (↥K⁺) K
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]
-- 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 : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
rw₁ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = nrRealPlaces K + nrComplexPlaces K
rw₂ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = 0 + nrComplexPlaces K
rw₃ : nrRealPlaces.{u_1} ↥K⁺ + 0 = 0 + nrComplexPlaces K
rw₄ : nrRealPlaces.{u_1} ↥K⁺ + 0 = nrComplexPlaces K
rw₅ : nrRealPlaces.{u_1} ↥K⁺ = nrComplexPlaces K
rw₆ : Module.finrank.{0, u_1} ℚ ↥K⁺ = nrComplexPlaces K
rw₇ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = 2 * nrComplexPlaces K
rw₈ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = Module.finrank ℚ K
rw₉ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = Module.finrank.{0, u_1} ℚ ↥K⁺ * Module.finrank (↥K⁺) K
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)
have rw₁₀ : Module.finrank.{0, u_1} ℚ ↥K⁺ * 2 = Module.finrank.{0, u_1} ℚ ↥K⁺ * Module.finrank (↥K⁺) K
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]
-- 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 : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = Fintype.card.{u_1} (InfinitePlace K)
rw₁ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = nrRealPlaces K + nrComplexPlaces K
rw₂ : nrRealPlaces.{u_1} ↥K⁺ + nrComplexPlaces.{u_1} ↥K⁺ = 0 + nrComplexPlaces K
rw₃ : nrRealPlaces.{u_1} ↥K⁺ + 0 = 0 + nrComplexPlaces K
rw₄ : nrRealPlaces.{u_1} ↥K⁺ + 0 = nrComplexPlaces K
rw₅ : nrRealPlaces.{u_1} ↥K⁺ = nrComplexPlaces K
rw₆ : Module.finrank.{0, u_1} ℚ ↥K⁺ = nrComplexPlaces K
rw₇ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = 2 * nrComplexPlaces K
rw₈ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = Module.finrank ℚ K
rw₉ : 2 * Module.finrank.{0, u_1} ℚ ↥K⁺ = Module.finrank.{0, u_1} ℚ ↥K⁺ * Module.finrank (↥K⁺) K
rw₁₀ : Module.finrank.{0, u_1} ℚ ↥K⁺ * 2 = Module.finrank.{0, u_1} ℚ ↥K⁺ * Module.finrank (↥K⁺) K
⊢ Fintype.card.{u_1} (InfinitePlace ↥K⁺) = Fintype.card.{u_1} (InfinitePlace K)
have rw₁₁ : Module.finrank.{0, u_1} ℚ ↥K⁺ * 2 = Module.finrank.{0, u_1} ℚ ↥K⁺ * 2
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]
-- 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⁺
x : ↥K⁺
⊢ Eq (α := ℝ)
    ((((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w : InfinitePlace K) :
          (a : K) → ℝ)
        ((algebraMap (↥K⁺) K : (a : ↥K⁺) → K) x : K) :
      ℝ)
    ((w : (a : ↥K⁺) → ℝ) x : ℝ)
have rw : Eq (α := ℝ)
  ((comap ((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w) (algebraMap (↥K⁺) K) :
        (a : ↥K⁺) → ℝ)
      x :
    ℝ)
  ((w : (a : ↥K⁺) → ℝ) x : ℝ)
Tactic: rw [← comap_apply, ← equivInfinitePlace_apply, Equiv.apply_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⁺
x : ↥K⁺
rw :
  Eq (α := ℝ)
    ((comap ((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w) (algebraMap (↥K⁺) K) :
          (a : ↥K⁺) → ℝ)
        x :
      ℝ)
    ((w : (a : ↥K⁺) → ℝ) x : ℝ)
⊢ Eq (α := ℝ)
    ((((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w : InfinitePlace K) :
          (a : K) → ℝ)
        ((algebraMap (↥K⁺) K : (a : ↥K⁺) → K) x : K) :
      ℝ)
    ((w : (a : ↥K⁺) → ℝ) x : ℝ)
have rw₁ : Eq (α := ℝ)
  ((((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺)
            ((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w) :
          InfinitePlace ↥K⁺) :
        (a : ↥K⁺) → ℝ)
      x :
    ℝ)
  ((w : (a : ↥K⁺) → ℝ) x : ℝ)
Tactic: rw [← comap_apply, ← equivInfinitePlace_apply, Equiv.apply_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⁺
x : ↥K⁺
rw :
  Eq (α := ℝ)
    ((comap ((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w) (algebraMap (↥K⁺) K) :
          (a : ↥K⁺) → ℝ)
        x :
      ℝ)
    ((w : (a : ↥K⁺) → ℝ) x : ℝ)
rw₁ :
  Eq (α := ℝ)
    ((((equivInfinitePlace K : (a : InfinitePlace K) → InfinitePlace ↥K⁺)
              ((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w) :
            InfinitePlace ↥K⁺) :
          (a : ↥K⁺) → ℝ)
        x :
      ℝ)
    ((w : (a : ↥K⁺) → ℝ) x : ℝ)
⊢ Eq (α := ℝ)
    ((((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w : InfinitePlace K) :
          (a : K) → ℝ)
        ((algebraMap (↥K⁺) K : (a : ↥K⁺) → K) x : K) :
      ℝ)
    ((w : (a : ↥K⁺) → ℝ) x : ℝ)
have rw₂ : Eq (α := ℝ) ((w : (a : ↥K⁺) → ℝ) x : ℝ) ((w : (a : ↥K⁺) → ℝ) x : ℝ)
Tactic: rw [← comap_apply, ← equivInfinitePlace_apply, Equiv.apply_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
⊢ Units.rank.{u_1} ↥K⁺ = Units.rank K
have rw : Fintype.card.{u_1} (InfinitePlace ↥K⁺) - 1 = Units.rank K
Tactic: rw [Units.rank, Units.rank, card_infinitePlace_eq_card_infinitePlace K]
-- 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 : Fintype.card.{u_1} (InfinitePlace ↥K⁺) - 1 = Units.rank K
⊢ Units.rank.{u_1} ↥K⁺ = Units.rank K
have rw₁ : Fintype.card.{u_1} (InfinitePlace ↥K⁺) - 1 = Fintype.card.{u_1} (InfinitePlace K) - 1
Tactic: rw [Units.rank, Units.rank, card_infinitePlace_eq_card_infinitePlace K]
-- 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 : Fintype.card.{u_1} (InfinitePlace ↥K⁺) - 1 = Units.rank K
rw₁ : Fintype.card.{u_1} (InfinitePlace ↥K⁺) - 1 = Fintype.card.{u_1} (InfinitePlace K) - 1
⊢ Units.rank.{u_1} ↥K⁺ = Units.rank K
have rw₂ : Fintype.card.{u_1} (InfinitePlace K) - 1 = Fintype.card.{u_1} (InfinitePlace K) - 1
Tactic: rw [Units.rank, Units.rank, card_infinitePlace_eq_card_infinitePlace K]
-- 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
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
⊢ σ = τ
have this : Nat.card.{u_1} Gal(K/↥K⁺) = 2
Tactic: have : Nat.card (K ≃ₐ[K⁺] K) = 2 :=
    (IsQuadraticExtension.finrank_eq_two K⁺ K) ▸ IsGalois.card_aut_eq_finrank K⁺ K
-- 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
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
this : Nat.card.{u_1} Gal(K/↥K⁺) = 2
⊢ σ = τ
have this₁ : ∃! y : Gal(K/↥K⁺), y ≠ 1
Tactic: rw [Nat.card_eq_two_iff' 1] at this
Cleared hypotheses: this
-- 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 : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
⊢ ComplexEmbedding.IsConj φ (complexConj K)
have obtain : ∀ (σ : Gal(K/↥K⁺)) (hσ : ComplexEmbedding.IsConj φ σ), ComplexEmbedding.IsConj φ (complexConj K)
Tactic: obtain ⟨σ, hσ⟩ := exists_isConj _ φ
-- 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 : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
σ : Gal(K/↥K⁺)
hσ : ComplexEmbedding.IsConj φ σ
⊢ ComplexEmbedding.IsConj φ (complexConj K)
have this : ComplexEmbedding.IsConj (Classical.choice sorry) (Exists.choose (p := ComplexEmbedding.IsConj (Classical.choice sorry)) sorry)
Tactic: have := (exists_isConj K (Classical.choice (inferInstance : Nonempty (K →+* ℂ)))).choose_spec
-- 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 : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
σ : Gal(K/↥K⁺)
hσ : ComplexEmbedding.IsConj φ σ
this :
  ComplexEmbedding.IsConj (Classical.choice ⋯) (Exists.choose (p := ComplexEmbedding.IsConj (Classical.choice ⋯)) ⋯)
⊢ ComplexEmbedding.IsConj φ (complexConj K)
have rwa : ∀ (hσ : ComplexEmbedding.IsConj φ (Exists.choose (p := ComplexEmbedding.IsConj (Classical.choice sorry)) sorry))
  (this :
    ComplexEmbedding.IsConj (Classical.choice sorry) (Exists.choose (p := ComplexEmbedding.IsConj (Classical.choice sorry)) sorry)),
  ComplexEmbedding.IsConj φ (complexConj K)
Tactic: rwa [isConj_eq_isConj K hσ this] at hσ
Cleared hypotheses: hσ, this
-- 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 : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
x : K
⊢ Eq (α := ℂ) ((φ : (a : K) → ℂ) ((complexConj K : (a : K) → K) x : K) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
have rw : Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
Tactic: rw [IsConj.eq (isConj_complexConj K φ), RCLike.star_def]
-- 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 : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
x : K
rw : Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
⊢ Eq (α := ℂ) ((φ : (a : K) → ℂ) ((complexConj K : (a : K) → K) x : K) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
have rw₁ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
  ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
Tactic: rw [IsConj.eq (isConj_complexConj K φ), RCLike.star_def]
-- 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 : Algebra.IsIntegral ℚ K
w : InfinitePlace K
x : K
⊢ Eq (α := ℝ) ((w : (a : K) → ℝ) ((complexConj K : (a : K) → K) x : K) : ℝ) ((w : (a : K) → ℝ) x : ℝ)
have rw : Norm.norm (E := ℂ) ((w.embedding : (a : K) → ℂ) ((complexConj K : (a : K) → K) x : K) : ℂ) = (w : (a : K) → ℝ) x
Tactic: rw [← norm_embedding_eq, complexEmbedding_complexConj, Complex.norm_conj, norm_embedding_eq]