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 : Algebra.IsIntegral ℚ K
w : InfinitePlace K
x : K
rw : Norm.norm (E := ℂ) ((w.embedding : (a : K) → ℂ) ((complexConj K : (a : K) → K) x : K) : ℂ) = (w : (a : K) → ℝ) x
⊢ Eq (α := ℝ) ((w : (a : K) → ℝ) ((complexConj K : (a : K) → K) x : K) : ℝ) ((w : (a : K) → ℝ) x : ℝ)
have rw₁ : Norm.norm (E := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) : ℂ) = (w : (a : K) → ℝ) x
Tactic: rw [← norm_embedding_eq, complexEmbedding_complexConj, Complex.norm_conj, norm_embedding_eq]
-- 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
rw : Norm.norm (E := ℂ) ((w.embedding : (a : K) → ℂ) ((complexConj K : (a : K) → K) x : K) : ℂ) = (w : (a : K) → ℝ) x
rw₁ : Norm.norm (E := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) : ℂ) = (w : (a : K) → ℝ) x
⊢ Eq (α := ℝ) ((w : (a : K) → ℝ) ((complexConj K : (a : K) → K) x : K) : ℝ) ((w : (a : K) → ℝ) x : ℝ)
have rw₂ : Norm.norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x
Tactic: rw [← norm_embedding_eq, complexEmbedding_complexConj, Complex.norm_conj, norm_embedding_eq]
-- 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
rw : Norm.norm (E := ℂ) ((w.embedding : (a : K) → ℂ) ((complexConj K : (a : K) → K) x : K) : ℂ) = (w : (a : K) → ℝ) x
rw₁ : Norm.norm (E := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) : ℂ) = (w : (a : K) → ℝ) x
rw₂ : Norm.norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x
⊢ Eq (α := ℝ) ((w : (a : K) → ℝ) ((complexConj K : (a : K) → K) x : K) : ℝ) ((w : (a : K) → ℝ) x : ℝ)
have rw₃ : Eq (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) ((w : (a : K) → ℝ) x : ℝ)
Tactic: rw [← norm_embedding_eq, complexEmbedding_complexConj, Complex.norm_conj, norm_embedding_eq]
-- 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
⊢ HPow.hPow (α := Gal(K/↥K⁺)) (β := ℕ) (complexConj K) 2 = 1
have h : ∀ (a : K),
  Eq (α := K) ((HPow.hPow (α := Gal(K/↥K⁺)) (β := ℕ) (complexConj K) 2 : (a : K) → K) a : K) ((1 : (a : K) → K) a : K)
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 : Algebra.IsIntegral ℚ K
⊢ Eq (α := Subgroup Gal(K/↥K⁺)) (Subgroup.zpowers (complexConj K)) ⊤
have refine : Nat.card.{u_1} ↥(Subgroup.zpowers (complexConj K)) = Nat.card.{u_1} Gal(K/↥K⁺)
Tactic: refine Subgroup.eq_top_of_card_eq _ ?_
-- 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
⊢ Nat.card.{u_1} ↥(Subgroup.zpowers (complexConj K)) = Nat.card.{u_1} Gal(K/↥K⁺)
have rw : orderOf (G := Gal(K/↥K⁺)) (complexConj K) = Nat.card.{u_1} Gal(K/↥K⁺)
Tactic: rw [Nat.card_zpowers, orderOf_complexConj, IsGalois.card_aut_eq_finrank,
    IsQuadraticExtension.finrank_eq_two]
-- 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
rw : orderOf (G := Gal(K/↥K⁺)) (complexConj K) = Nat.card.{u_1} Gal(K/↥K⁺)
⊢ Nat.card.{u_1} ↥(Subgroup.zpowers (complexConj K)) = Nat.card.{u_1} Gal(K/↥K⁺)
have rw₁ : 2 = Nat.card.{u_1} Gal(K/↥K⁺)
Tactic: rw [Nat.card_zpowers, orderOf_complexConj, IsGalois.card_aut_eq_finrank,
    IsQuadraticExtension.finrank_eq_two]
-- 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
rw : orderOf (G := Gal(K/↥K⁺)) (complexConj K) = Nat.card.{u_1} Gal(K/↥K⁺)
rw₁ : 2 = Nat.card.{u_1} Gal(K/↥K⁺)
⊢ Nat.card.{u_1} ↥(Subgroup.zpowers (complexConj K)) = Nat.card.{u_1} Gal(K/↥K⁺)
have rw₂ : 2 = Module.finrank (↥K⁺) K
Tactic: rw [Nat.card_zpowers, orderOf_complexConj, IsGalois.card_aut_eq_finrank,
    IsQuadraticExtension.finrank_eq_two]
-- 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
rw : orderOf (G := Gal(K/↥K⁺)) (complexConj K) = Nat.card.{u_1} Gal(K/↥K⁺)
rw₁ : 2 = Nat.card.{u_1} Gal(K/↥K⁺)
rw₂ : 2 = Module.finrank (↥K⁺) K
⊢ Nat.card.{u_1} ↥(Subgroup.zpowers (complexConj K)) = Nat.card.{u_1} Gal(K/↥K⁺)
have rw₃ : Eq (α := ℕ) 2 2
Tactic: rw [Nat.card_zpowers, orderOf_complexConj, IsGalois.card_aut_eq_finrank,
    IsQuadraticExtension.finrank_eq_two]
-- 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
x : K
⊢ (complexConj K : (a : K) → K) x = x ↔ Membership.mem (γ := Subfield K) K⁺ x
have h : (complexConj K : (a : K) → K) x = x ↔
  ∀ (f : Gal(K/↥K⁺)), Membership.mem (γ := Subgroup Gal(K/↥K⁺)) ⊤ f → (f : (a : K) → K) x = x
Tactic: convert! (IntermediateField.mem_fixedField_iff (⊤ : Subgroup (K ≃ₐ[K⁺] K)) x).symm using 1
-- 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
x : K
h :
  (complexConj K : (a : K) → K) x = x ↔
    ∀ (f : Gal(K/↥K⁺)), Membership.mem (γ := Subgroup Gal(K/↥K⁺)) ⊤ f → (f : (a : K) → K) x = x
⊢ (complexConj K : (a : K) → K) x = x ↔ Membership.mem (γ := Subfield K) K⁺ x
have h₁ : Membership.mem (γ := Subfield K) K⁺ x ↔
  Membership.mem (γ := IntermediateField (↥K⁺) K) (IntermediateField.fixedField ⊤) x
Tactic: convert! (IntermediateField.mem_fixedField_iff (⊤ : Subgroup (K ≃ₐ[K⁺] K)) x).symm using 1
-- 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
x : K
⊢ (complexConj K : (a : K) → K) x = x ↔
    ∀ (f : Gal(K/↥K⁺)), Membership.mem (γ := Subgroup Gal(K/↥K⁺)) ⊤ f → (f : (a : K) → K) x = x
have h : (complexConj K : (a : K) → K) x = x ↔ ∀ (m : ℤ), (HPow.hPow (α := Gal(K/↥K⁺)) (complexConj K) m : (a : K) → K) x = x
Tactic: rw [← zpowers_complexConj_eq_top, Subgroup.forall_mem_zpowers]
-- 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
x : K
⊢ Membership.mem (γ := Subfield K) K⁺ x ↔
    Membership.mem (γ := IntermediateField (↥K⁺) K) (IntermediateField.fixedField ⊤) x
have h : Membership.mem (γ := Subfield K) K⁺ x ↔
  Membership.mem (γ := Set K) (Set.range (ι := ↥K⁺) (⇑(algebraMap (↥K⁺) K) : (a : ↥K⁺) → K)) x
Tactic: rw [IsGalois.fixedField_top, IntermediateField.mem_bot]
-- 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
x : 𝓞 K
⊢ (complexConj K : (a : K) → K) (↑x : K) = (↑x : K) ↔
    ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
have rw : Membership.mem (γ := Subfield K) K⁺ (↑x : K) ↔ ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
Tactic: rw [complexConj_eq_self_iff]
-- 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
x : 𝓞 K
⊢ Membership.mem (γ := Subfield K) K⁺ (↑x : K) ↔ ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
have refine_1 : ∀ (h : Membership.mem (γ := Subfield K) K⁺ (↑x : K)),
  ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
Tactic: refine ⟨fun h ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩
-- 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
x : 𝓞 K
refine_1 :
  ∀ (h : Membership.mem (γ := Subfield K) K⁺ (↑x : K)),
    ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
⊢ Membership.mem (γ := Subfield K) K⁺ (↑x : K) ↔ ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
have refine_2 : (∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)) →
  ∀ (y : 𝓞 ↥K⁺) (hy : (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)),
    Membership.mem (γ := Subfield K) K⁺ (↑x : K)
Tactic: refine ⟨fun h ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩
-- 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
x : 𝓞 K
h : Membership.mem (γ := Subfield K) K⁺ (↑x : K)
⊢ ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
have this : IsIntegral ℤ (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h)
Tactic: have : IsIntegral ℤ (⟨x, h⟩ : K⁺) :=
      (isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective K⁺ K)).mp x.isIntegral_coe
-- 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
x : 𝓞 K
h : Membership.mem (γ := Subfield K) K⁺ (↑x : K)
this : IsIntegral ℤ (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h)
⊢ ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
have refine_1 : (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K)
    (Subtype.mk (p := fun (x : ↥K⁺) ↦ Membership.mem (γ := Subalgebra ℤ ↥K⁺) (integralClosure ℤ ↥K⁺) x)
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h) this) =
  (↑x : K)
Tactic: refine ⟨⟨⟨x, 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
x : 𝓞 K
h : Membership.mem (γ := Subfield K) K⁺ (↑x : K)
this : IsIntegral ℤ (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h)
⊢ (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K)
      (Subtype.mk (p := fun (x : ↥K⁺) ↦ Membership.mem (γ := Subalgebra ℤ ↥K⁺) (integralClosure ℤ ↥K⁺) x)
        (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h) this) =
    (↑x : K)
have refine_1 : (algebraMap (↥K⁺) K : (a : ↥K⁺) → K)
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h) =
  (↑x : K)
Tactic: rw [IsScalarTower.algebraMap_apply (𝓞 K⁺) K⁺, RingOfIntegers.map_mk]
-- 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
x : 𝓞 K
h : ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
⊢ Membership.mem (γ := Subfield K) K⁺ (↑x : K)
have refine_2 : Membership.mem (α := K) (γ := Subfield K) K⁺
  ((algebraMap (↥K⁺) K : (a : ↥K⁺) → K) ((algebraMap (𝓞 ↥K⁺) ↥K⁺ : (a : 𝓞 ↥K⁺) → ↥K⁺) y : ↥K⁺) : K)
Tactic: rw [← hy, IsScalarTower.algebraMap_apply (𝓞 K⁺) 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 : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ Eq (α := K) ((complexConj K : (a : K) → K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ),
      Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
have rw : (∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) ↔
  ∃ (v : (𝓞 ↥K⁺)ˣ),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
Tactic: rw [RingOfIntegers.complexConj_eq_self_iff, Units.coe_coe]
-- 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
u : (𝓞 K)ˣ
h :
  ∃ (v : (𝓞 ↥K⁺)ˣ),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
v : (𝓞 ↥K⁺)ˣ
hv :
  Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
⊢ Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
have rw : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
Tactic: rw [hv]
-- 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
u : (𝓞 K)ˣ
⊢ (∃ (y : 𝓞 ↥K⁺),
      Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ),
      Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
have refine : (∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) →
  ∀ (y : 𝓞 ↥K⁺)
    (hy :
      Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)),
    ∃ (v : (𝓞 ↥K⁺)ˣ),
      Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
Tactic: refine ⟨fun ⟨y, hy⟩ ↦ ?_, fun ⟨v, hv⟩ ↦ ⟨v, by rw [hv]⟩⟩
-- 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
u : (𝓞 K)ˣ
h :
  ∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
y : 𝓞 ↥K⁺
hy : Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
⊢ IsUnit y
have h : IsUnit (M := 𝓞 K) ((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) y : 𝓞 K)
Tactic: apply IsUnit.of_map (algebraMap (𝓞 K⁺) (𝓞 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 : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
h :
  ∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
y : 𝓞 ↥K⁺
hy : Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
⊢ IsUnit (M := 𝓞 K) ((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) y : 𝓞 K)
have h : IsUnit (↑u : 𝓞 K)
Tactic: rw [show algebraMap (𝓞 K⁺) (𝓞 K) y = u by exact RingOfIntegers.ext hy]
-- 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
u : (𝓞 K)ˣ
h :
  ∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
y : 𝓞 ↥K⁺
hy : Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
⊢ ∃ (v : (𝓞 ↥K⁺)ˣ),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
have this : IsUnit y
Tactic: have : IsUnit y := by
    apply IsUnit.of_map (algebraMap (𝓞 K⁺) (𝓞 K))
    rw [show algebraMap (𝓞 K⁺) (𝓞 K) y = u by exact RingOfIntegers.ext hy]
    exact u.isUnit
-- 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
x x_1 : K
⊢ (complexConj K : (a : K) → K) (x * x_1) =
    HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x_1 : K) ((complexConj K : (a : K) → K) x : K)
have rw : HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x : K) ((complexConj K : (a : K) → K) x_1 : K) =
  HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x_1 : K) ((complexConj K : (a : K) → K) x : K)
Tactic: rw [map_mul, mul_comm]
-- 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
x x_1 : K
rw :
  HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x : K) ((complexConj K : (a : K) → K) x_1 : K) =
    HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x_1 : K) ((complexConj K : (a : K) → K) x : K)
⊢ (complexConj K : (a : K) → K) (x * x_1) =
    HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x_1 : K) ((complexConj K : (a : K) → K) x : K)
have rw₁ : HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x_1 : K) ((complexConj K : (a : K) → K) x : K) =
  HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x_1 : K) ((complexConj K : (a : K) → K) x : K)
Tactic: rw [map_mul, mul_comm]
-- 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
x x_1 : K
⊢ (complexConj K : (a : K) → K) (x + x_1) =
    HAdd.hAdd (α := K) (β := K) ((complexConj K : (a : K) → K) x : K) ((complexConj K : (a : K) → K) x_1 : K)
have rw : HAdd.hAdd (α := K) (β := K) ((complexConj K : (a : K) → K) x : K) ((complexConj K : (a : K) → K) x_1 : K) =
  HAdd.hAdd (α := K) (β := K) ((complexConj K : (a : K) → K) x : K) ((complexConj K : (a : K) → K) x_1 : K)
Tactic: rw [map_add]
-- 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
x : 𝓞 K
⊢ (ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) x = x ↔
    Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x
have refine_1 : ∀ (h : (ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) x = x),
  Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x
Tactic: refine ⟨fun 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 : Algebra.IsIntegral ℚ K
x : 𝓞 K
refine_1 :
  ∀ (h : (ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) x = x),
    Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x
⊢ (ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) x = x ↔
    Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x
have refine_2 : Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x →
  (ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) x = x
Tactic: refine ⟨fun 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 : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : (ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) x = x
⊢ Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x
have h₁ : ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
Tactic: rw [RingOfIntegers.ext_iff, coe_ringOfIntegersComplexConj,
      RingOfIntegers.complexConj_eq_self_iff] at h
Cleared hypotheses: 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 : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
⊢ Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x
have refine_1 : ∀ (y : 𝓞 ↥K⁺) (hy : (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)),
  Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x
Tactic: obtain ⟨y, hy⟩ := h
Cleared hypotheses: 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 : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u = u ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
have simp_rw : (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
Tactic: simp_rw [Units.ext_iff, mem_realUnits_iff, RingOfIntegers.ext_iff, Units.coe_mapEquiv,
    RingEquiv.coe_toMulEquiv, RingOfIntegers.mapRingEquiv_apply,
    AlgEquiv.coe_ringEquiv, Units.complexConj_eq_self_iff,
    IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) 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 : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
simp_rw :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
⊢ (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u = u ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
have simp_rw₁ : (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
  ∃ (v : (𝓞 ↥K⁺)ˣ), (algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺) = (↑u : 𝓞 K)
Tactic: simp_rw [Units.ext_iff, mem_realUnits_iff, RingOfIntegers.ext_iff, Units.coe_mapEquiv,
    RingEquiv.coe_toMulEquiv, RingOfIntegers.mapRingEquiv_apply,
    AlgEquiv.coe_ringEquiv, Units.complexConj_eq_self_iff,
    IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) 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 : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
simp_rw :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
simp_rw₁ :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺) = (↑u : 𝓞 K)
⊢ (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u = u ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
have simp_rw₂ : (↑(↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) : K) = (↑(↑u : 𝓞 K) : K) ↔
  ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
Tactic: simp_rw [Units.ext_iff, mem_realUnits_iff, RingOfIntegers.ext_iff, Units.coe_mapEquiv,
    RingEquiv.coe_toMulEquiv, RingOfIntegers.mapRingEquiv_apply,
    AlgEquiv.coe_ringEquiv, Units.complexConj_eq_self_iff,
    IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) K]