awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (hypothesis)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
inst_3 : NumberField K
inst_4 : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
ψ : L →+* ℂ
hψ : ψ ∈ (↑(Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) ⋯) : Set (L →+* ℂ))
⊢ ψ ∈ AlgHom.toRingHom '' (↑univ : Set (L →ₐ[K] ℂ))
have hψ₁ : ComplexEmbedding.LiesOver ψ v.embedding
Tactic: simp only [Set.Finite.toFinset_setOf, coe_filter, mem_univ, true_and, Set.mem_setOf_eq] at hψ
Cleared hypotheses: hψ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
inst_3 : NumberField K
inst_4 : NumberField L
let let₁ let₂ :
  Set.ncard (α := InfinitePlace L) (unramifiedPlacesOver L v) +
      2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    finrank K L
⊢ Set.ncard (α := InfinitePlace L) (unramifiedPlacesOver L v) +
      2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    finrank K L
have let₃ : let this := v.embedding.toAlgebra;
Finset.card.{u_5} (α := L →+* ℂ)
    (Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) sorry) =
  Fintype.card.{u_5} (L →ₐ[K] ℂ)
Tactic: classical
  let : Algebra K ℂ := v.embedding.toAlgebra
  rw [← AlgHom.card K L ℂ, ramifiedPlacesOver_ncard, unramifiedPlacesOver_ncard,
    ← Set.ncard_union_eq (disjoint_unmixedEmbeddingsOver_mixedEmbeddingsOver L v.embedding),
    union_unmixedEmbeddingsOver_mixedEmbeddingsOver, Set.ncard_eq_toFinset_card]
  apply (card_nbij AlgHom.toRingHom (fun σ _ ↦ by simpa using ⟨by aesop⟩)
    AlgHom.coe_ringHom_injective.injOn (fun ψ hψ ↦ ?_)).symm
  simp only [Set.Finite.toFinset_setOf, coe_filter, mem_univ, true_and, Set.mem_setOf_eq] at hψ
  exact ⟨⟨ψ, fun _ ↦ by simp [RingHom.algebraMap_toAlgebra, ← hψ.over]⟩, by simp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
inst_3 : NumberField K
inst_4 : NumberField L
let let₁ let₂ :
  Set.ncard (α := InfinitePlace L) (unramifiedPlacesOver L v) +
      2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    finrank K L
let₃ :
  let this := v.embedding.toAlgebra;
  Finset.card.{u_5} (α := L →+* ℂ)
      (Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) ⋯) =
    Fintype.card.{u_5} (L →ₐ[K] ℂ)
⊢ Set.ncard (α := InfinitePlace L) (unramifiedPlacesOver L v) +
      2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    finrank K L
have let₄ : let this := v.embedding.toAlgebra;
∀ (ψ : L →+* ℂ)
  (hψ : ψ ∈ (↑(Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) sorry) : Set (L →+* ℂ))),
  ψ ∈ AlgHom.toRingHom '' (↑univ : Set (L →ₐ[K] ℂ))
Tactic: classical
  let : Algebra K ℂ := v.embedding.toAlgebra
  rw [← AlgHom.card K L ℂ, ramifiedPlacesOver_ncard, unramifiedPlacesOver_ncard,
    ← Set.ncard_union_eq (disjoint_unmixedEmbeddingsOver_mixedEmbeddingsOver L v.embedding),
    union_unmixedEmbeddingsOver_mixedEmbeddingsOver, Set.ncard_eq_toFinset_card]
  apply (card_nbij AlgHom.toRingHom (fun σ _ ↦ by simpa using ⟨by aesop⟩)
    AlgHom.coe_ringHom_injective.injOn (fun ψ hψ ↦ ?_)).symm
  simp only [Set.Finite.toFinset_setOf, coe_filter, mem_univ, true_and, Set.mem_setOf_eq] at hψ
  exact ⟨⟨ψ, fun _ ↦ by simp [RingHom.algebraMap_toAlgebra, ← hψ.over]⟩, by simp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
inst_3 : NumberField K
inst_4 : NumberField L
let let₁ let₂ :
  Set.ncard (α := InfinitePlace L) (unramifiedPlacesOver L v) +
      2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    finrank K L
let₃ :
  let this := v.embedding.toAlgebra;
  Finset.card.{u_5} (α := L →+* ℂ)
      (Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) ⋯) =
    Fintype.card.{u_5} (L →ₐ[K] ℂ)
let₄ :
  let this := v.embedding.toAlgebra;
  ∀ (ψ : L →+* ℂ)
    (hψ :
      ψ ∈ (↑(Set.Finite.toFinset (s := {φ : L →+* ℂ | ComplexEmbedding.LiesOver φ v.embedding}) ⋯) : Set (L →+* ℂ))),
    ψ ∈ AlgHom.toRingHom '' (↑univ : Set (L →ₐ[K] ℂ))
⊢ Set.ncard (α := InfinitePlace L) (unramifiedPlacesOver L v) +
      2 * Set.ncard (α := InfinitePlace L) (ramifiedPlacesOver L v) =
    finrank K L
have let₅ : let this := v.embedding.toAlgebra;
∀ (ψ : L →+* ℂ) (hψ : ComplexEmbedding.LiesOver ψ v.embedding), ψ ∈ AlgHom.toRingHom '' (↑univ : Set (L →ₐ[K] ℂ))
Tactic: classical
  let : Algebra K ℂ := v.embedding.toAlgebra
  rw [← AlgHom.card K L ℂ, ramifiedPlacesOver_ncard, unramifiedPlacesOver_ncard,
    ← Set.ncard_union_eq (disjoint_unmixedEmbeddingsOver_mixedEmbeddingsOver L v.embedding),
    union_unmixedEmbeddingsOver_mixedEmbeddingsOver, Set.ncard_eq_toFinset_card]
  apply (card_nbij AlgHom.toRingHom (fun σ _ ↦ by simpa using ⟨by aesop⟩)
    AlgHom.coe_ringHom_injective.injOn (fun ψ hψ ↦ ?_)).symm
  simp only [Set.Finite.toFinset_setOf, coe_filter, mem_univ, true_and, Set.mem_setOf_eq] at hψ
  exact ⟨⟨ψ, fun _ ↦ by simp [RingHom.algebraMap_toAlgebra, ← hψ.over]⟩, by simp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : IsTotallyReal K
inst_3 : Algebra F K
inst_4 : Algebra.IsAlgebraic F K
w : InfinitePlace F
⊢ w.IsReal
have obtain : ∀ (W : InfinitePlace K), IsReal (W.comap (algebraMap F K))
Tactic: obtain ⟨W, rfl⟩ : ∃ W : InfinitePlace K, W.comap (algebraMap F K) = w := comap_surjective w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
h : IsTotallyReal K
⊢ finrank ℚ K = nrRealPlaces K
have rw : nrRealPlaces K + 2 * nrComplexPlaces K = nrRealPlaces K
Tactic: rw [← card_add_two_mul_card_eq_rank, nrComplexPlaces_eq_zero_iff.mpr h, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
h : IsTotallyReal K
rw : nrRealPlaces K + 2 * nrComplexPlaces K = nrRealPlaces K
⊢ finrank ℚ K = nrRealPlaces K
have rw₁ : nrRealPlaces K + HMul.hMul (α := ℕ) 2 0 = nrRealPlaces K
Tactic: rw [← card_add_two_mul_card_eq_rank, nrComplexPlaces_eq_zero_iff.mpr h, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
h : IsTotallyReal K
rw : nrRealPlaces K + 2 * nrComplexPlaces K = nrRealPlaces K
rw₁ : nrRealPlaces K + HMul.hMul (α := ℕ) 2 0 = nrRealPlaces K
⊢ finrank ℚ K = nrRealPlaces K
have rw₂ : nrRealPlaces K + 0 = nrRealPlaces K
Tactic: rw [← card_add_two_mul_card_eq_rank, nrComplexPlaces_eq_zero_iff.mpr h, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
h : IsTotallyReal K
rw : nrRealPlaces K + 2 * nrComplexPlaces K = nrRealPlaces K
rw₁ : nrRealPlaces K + HMul.hMul (α := ℕ) 2 0 = nrRealPlaces K
rw₂ : nrRealPlaces K + 0 = nrRealPlaces K
⊢ finrank ℚ K = nrRealPlaces K
have rw₃ : nrRealPlaces K = nrRealPlaces K
Tactic: rw [← card_add_two_mul_card_eq_rank, nrComplexPlaces_eq_zero_iff.mpr h, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
v : InfinitePlace ℚ
⊢ v.IsReal
have rw : Rat.infinitePlace.IsReal
Tactic: rw [Subsingleton.elim v Rat.infinitePlace]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
⊢ IsTotallyReal.{u_2} ↥⊥
have rw : IsTotallyReal.{u_2} ↥(RingHom.fieldRange (algebraMap ℚ K))
Tactic: rw [Subfield.bot_eq_of_charZero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
a b : K
hx :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} a
hy :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} b
x : K →+* ℂ
⊢ Eq (α := ℂ) (star ((x : (a : K) → ℂ) (a * b)) : ℂ) ((x : (a : K) → ℂ) (a * b) : ℂ)
have rw : star (HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)) =
  HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
Tactic: rw [map_mul, star_mul, hx, hy, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
a b : K
hx :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} a
hy :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} b
x : K →+* ℂ
rw :
  star (HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
⊢ Eq (α := ℂ) (star ((x : (a : K) → ℂ) (a * b)) : ℂ) ((x : (a : K) → ℂ) (a * b) : ℂ)
have rw₁ : HMul.hMul (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) (star ((x : (a : K) → ℂ) a) : ℂ) =
  HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
Tactic: rw [map_mul, star_mul, hx, hy, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
a b : K
hx :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} a
hy :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} b
x : K →+* ℂ
rw :
  star (HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₁ :
  HMul.hMul (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) (star ((x : (a : K) → ℂ) a) : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
⊢ Eq (α := ℂ) (star ((x : (a : K) → ℂ) (a * b)) : ℂ) ((x : (a : K) → ℂ) (a * b) : ℂ)
have rw₂ : HMul.hMul (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) ((x : (a : K) → ℂ) a : ℂ) =
  HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
Tactic: rw [map_mul, star_mul, hx, hy, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
a b : K
hx :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} a
hy :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} b
x : K →+* ℂ
rw :
  star (HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₁ :
  HMul.hMul (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) (star ((x : (a : K) → ℂ) a) : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₂ :
  HMul.hMul (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) ((x : (a : K) → ℂ) a : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
⊢ Eq (α := ℂ) (star ((x : (a : K) → ℂ) (a * b)) : ℂ) ((x : (a : K) → ℂ) (a * b) : ℂ)
have rw₃ : HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) b : ℂ) ((x : (a : K) → ℂ) a : ℂ) =
  HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
Tactic: rw [map_mul, star_mul, hx, hy, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
a b : K
hx :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} a
hy :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} b
x : K →+* ℂ
rw :
  star (HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₁ :
  HMul.hMul (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) (star ((x : (a : K) → ℂ) a) : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₂ :
  HMul.hMul (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) ((x : (a : K) → ℂ) a : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₃ :
  HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) b : ℂ) ((x : (a : K) → ℂ) a : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
⊢ Eq (α := ℂ) (star ((x : (a : K) → ℂ) (a * b)) : ℂ) ((x : (a : K) → ℂ) (a * b) : ℂ)
have rw₄ : HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ) =
  HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
Tactic: rw [map_mul, star_mul, hx, hy, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
a b : K
hx :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} a
hy :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} b
x : K →+* ℂ
⊢ Eq (α := ℂ) (star ((x : (a : K) → ℂ) (a + b)) : ℂ) ((x : (a : K) → ℂ) (a + b) : ℂ)
have rw : star (HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)) =
  HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
Tactic: rw [map_add, star_add, hx, hy]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
a b : K
hx :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} a
hy :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} b
x : K →+* ℂ
rw :
  star (HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
⊢ Eq (α := ℂ) (star ((x : (a : K) → ℂ) (a + b)) : ℂ) ((x : (a : K) → ℂ) (a + b) : ℂ)
have rw₁ : HAdd.hAdd (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) a) : ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) =
  HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
Tactic: rw [map_add, star_add, hx, hy]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
a b : K
hx :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} a
hy :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} b
x : K →+* ℂ
rw :
  star (HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₁ :
  HAdd.hAdd (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) a) : ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
⊢ Eq (α := ℂ) (star ((x : (a : K) → ℂ) (a + b)) : ℂ) ((x : (a : K) → ℂ) (a + b) : ℂ)
have rw₂ : HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) =
  HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
Tactic: rw [map_add, star_add, hx, hy]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
a b : K
hx :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} a
hy :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} b
x : K →+* ℂ
rw :
  star (HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₁ :
  HAdd.hAdd (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) a) : ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₂ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
⊢ Eq (α := ℂ) (star ((x : (a : K) → ℂ) (a + b)) : ℂ) ((x : (a : K) → ℂ) (a + b) : ℂ)
have rw₃ : HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ) =
  HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
Tactic: rw [map_add, star_add, hx, hy]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
E : Subfield K
inst_1 : IsTotallyReal.{u_2} ↥E
x : K
hx : x ∈ E
φ : K →+* ℂ
⊢ Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)
have rw : Eq (α := ℂ) ((conjugate (φ.comp E.subtype) : (a : ↥E) → ℂ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) x hx) : ℂ)
  ((φ.comp E.subtype : (a : ↥E) → ℂ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) x hx) : ℂ)
Tactic: rw [show φ x = (φ.comp E.subtype) ⟨x, hx⟩ by simp, RCLike.star_def, ← conjugate_coe_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
E : Subfield K
inst_1 : IsTotallyReal.{u_2} ↥E
x : K
hx : x ∈ E
φ : K →+* ℂ
⊢ Eq (α := ℂ) ((conjugate (φ.comp E.subtype) : (a : ↥E) → ℂ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) x hx) : ℂ)
    ((φ.comp E.subtype : (a : ↥E) → ℂ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) x hx) : ℂ)
have refine : conjugate (φ.comp E.subtype) = φ.comp E.subtype
Tactic: refine RingHom.congr_fun ?_ _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
⊢ w.IsReal
have rw : conjugate w.embedding = w.embedding
Tactic: rw [InfinitePlace.isReal_iff, ComplexEmbedding.isReal_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
⊢ conjugate w.embedding = w.embedding
have a : ∀ (x : ↥(maximalRealSubfield K)),
  Eq (α := ℂ) ((conjugate w.embedding : (a : ↥(maximalRealSubfield K)) → ℂ) x : ℂ)
    ((w.embedding : (a : ↥(maximalRealSubfield K)) → ℂ) x : ℂ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
x : ↥(maximalRealSubfield K)
⊢ Eq (α := ℂ) ((conjugate w.embedding : (a : ↥(maximalRealSubfield K)) → ℂ) x : ℂ)
    ((w.embedding : (a : ↥(maximalRealSubfield K)) → ℂ) x : ℂ)
have a : Eq (α := ℂ)
  (star
      ((lift K w.embedding : (a : K) → ℂ)
        ((algebraMap (↥(maximalRealSubfield K)) K : (a : ↥(maximalRealSubfield K)) → K) x : K)) :
    ℂ)
  ((lift K w.embedding : (a : K) → ℂ)
      ((algebraMap (↥(maximalRealSubfield K)) K : (a : ↥(maximalRealSubfield K)) → K) x : K) :
    ℂ)
Tactic: rw [RingHom.star_apply, ← lift_algebraMap_apply K w.embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
E : Subfield K
⊢ IsTotallyReal.{u_2} ↥E ↔ E ≤ maximalRealSubfield K
have refine : ∀ (h : E ≤ maximalRealSubfield K), IsTotallyReal.{u_2} ↥E
Tactic: refine ⟨fun h ↦ h.le_maximalRealSubfield, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (hypothesis)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
E : Subfield K
h : E ≤ maximalRealSubfield K
x : Algebra ↥E ↥(maximalRealSubfield K) := (Subfield.inclusion h).toAlgebra
⊢ IsTotallyReal.{u_2} ↥E
have this : IsScalarTower (↥E) (↥(maximalRealSubfield K)) K
Tactic: have : IsScalarTower E (maximalRealSubfield K) K := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (hypothesis)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
E : Subfield K
h : E ≤ maximalRealSubfield K
x : Algebra ↥E ↥(maximalRealSubfield K) := (Subfield.inclusion h).toAlgebra
this : IsScalarTower (↥E) (↥(maximalRealSubfield K)) K
⊢ IsTotallyReal.{u_2} ↥E
have this₁ : Algebra.IsAlgebraic.{u_2, u_2} ↥E ↥(maximalRealSubfield K)
Tactic: have : Algebra.IsAlgebraic E (maximalRealSubfield K) :=
      Algebra.IsAlgebraic.tower_bot E (maximalRealSubfield K) K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F_1 : Type u_1
inst : Field F_1
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
E F : Subfield K
hE : IsTotallyReal.{u_2} ↥E
hF : IsTotallyReal.{u_2} ↥F
⊢ IsTotallyReal.{u_2} ↥(E ⊔ F)
have rw : IsTotallyReal.{u_2} ↥E ∧ IsTotallyReal.{u_2} ↥F
Tactic: rw [isTotallyReal_iff_le_maximalRealSubfield, sup_le_iff,
    ← isTotallyReal_iff_le_maximalRealSubfield, ← isTotallyReal_iff_le_maximalRealSubfield]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst_4 : ∀ (i : ι), IsTotallyReal.{u_2} ↥(k i)
⊢ IsTotallyReal.{u_2} ↥(⨆ (i : ι), k i)
have inl : ∀ (hι : IsEmpty ι), IsTotallyReal.{u_2} ↥(⨆ (i : ι), k i)
Tactic: obtain hι | ⟨⟨i⟩⟩ := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst_4 : ∀ (i : ι), IsTotallyReal.{u_2} ↥(k i)
inl : ∀ (hι : IsEmpty ι), IsTotallyReal.{u_2} ↥(⨆ (i : ι), k i)
⊢ IsTotallyReal.{u_2} ↥(⨆ (i : ι), k i)
have inr : ∀ (i : ι), IsTotallyReal.{u_2} ↥(⨆ (i : ι), k i)
Tactic: obtain hι | ⟨⟨i⟩⟩ := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst_4 : ∀ (i : ι), IsTotallyReal.{u_2} ↥(k i)
hι : IsEmpty ι
⊢ IsTotallyReal.{u_2} ↥(⨆ (i : ι), k i)
have inl : IsTotallyReal.{u_2} ↥⊥
Tactic: rw [iSup_of_empty]