awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : p = 0
this : IsEmpty (↑(p.rootSet ℂ) : Type)
pos : (p.rootSet ℂ).toFinset.card = (p.rootSet ℝ).toFinset.card + Finset.card (α := (↑(p.rootSet ℂ) : Type)) ∅
pos₁ :
  (rootSet (T := ℚ) 0 ℂ).toFinset.card =
    (rootSet (T := ℚ) 0 ℝ).toFinset.card + Finset.card (α := (↑(p.rootSet ℂ) : Type)) ∅
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
have pos₂ : Finset.card (α := ℂ) (Set.toFinset ∅) =
  Finset.card (α := ℝ) (Set.toFinset ∅) + Finset.card (α := (↑(p.rootSet ℂ) : Type)) ∅
Tactic: simp_rw [(galActionHom p ℂ _).support.eq_empty_of_isEmpty, hp, rootSet_zero,
      Set.toFinset_empty, Finset.card_empty]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : p = 0
this : IsEmpty (↑(p.rootSet ℂ) : Type)
pos : (p.rootSet ℂ).toFinset.card = (p.rootSet ℝ).toFinset.card + Finset.card (α := (↑(p.rootSet ℂ) : Type)) ∅
pos₁ :
  (rootSet (T := ℚ) 0 ℂ).toFinset.card =
    (rootSet (T := ℚ) 0 ℝ).toFinset.card + Finset.card (α := (↑(p.rootSet ℂ) : Type)) ∅
pos₂ :
  Finset.card (α := ℂ) (Set.toFinset ∅) =
    Finset.card (α := ℝ) (Set.toFinset ∅) + Finset.card (α := (↑(p.rootSet ℂ) : Type)) ∅
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
have pos₃ : Finset.card (α := ℂ) ∅ = Finset.card (α := ℝ) ∅ + Finset.card (α := (↑(p.rootSet ℂ) : Type)) ∅
Tactic: simp_rw [(galActionHom p ℂ _).support.eq_empty_of_isEmpty, hp, rootSet_zero,
      Set.toFinset_empty, Finset.card_empty]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
Goal:
p : ℚ[X]
hp : ¬p = 0
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
have inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
Tactic: have inj : Function.Injective (IsScalarTower.toAlgHom ℚ ℝ ℂ) := (algebraMap ℝ ℂ).injective
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
have neg : (p.rootSet ℂ).toFinset.card =
  Finset.card (α := ℂ) (Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset) +
    Finset.card (α := ℂ)
      (Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal))))
Tactic: rw [← Finset.card_image_of_injective _ Subtype.coe_injective, ←
    Finset.card_image_of_injective _ inj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
neg :
  (p.rootSet ℂ).toFinset.card =
    Finset.card (α := ℂ) (Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset) +
      Finset.card (α := ℂ)
        (Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
          (Equiv.Perm.support
            ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
              ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal))))
⊢ (p.rootSet ℂ).toFinset.card =
    Finset.card (α := ℂ) (Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset) +
      Finset.card (α := ℂ)
        (Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
          (Equiv.Perm.support
            ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
              ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal))))
have neg₁ : Finset ℂ
Tactic: let a : Finset ℂ := ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
z : ℂ
⊢ z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
have rw : z ∈ p.rootSet ℂ ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
Tactic: rw [Set.mem_toFinset, mem_rootSet_of_ne hp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
z : ℂ
rw : z ∈ p.rootSet ℂ ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
have rw₁ : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
Tactic: rw [Set.mem_toFinset, mem_rootSet_of_ne hp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
⊢ a.card = b.card + c.card
have ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
Tactic: have ha : ∀ z : ℂ, z ∈ a ↔ aeval z p = 0 := by
    intro z; rw [Set.mem_toFinset, mem_rootSet_of_ne hp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
z : ℂ
⊢ z ∈ b ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0
have simp_rw : (∃ (a : ℝ),
    Eq (α := ℝ) ((aeval a : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ) ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) a = z) ↔
  Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0
Tactic: simp_rw [b, Finset.mem_image, Set.mem_toFinset, mem_rootSet_of_ne hp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
z : ℂ
⊢ (∃ (a : ℝ),
      Eq (α := ℝ) ((aeval a : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ) ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) a = z) ↔
    Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0
have mp : (∃ (a : ℝ),
    Eq (α := ℝ) ((aeval a : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ) ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) a = z) →
  Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
z : ℂ
mp :
  (∃ (a : ℝ),
      Eq (α := ℝ) ((aeval a : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ) ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) a = z) →
    Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0
⊢ (∃ (a : ℝ),
      Eq (α := ℝ) ((aeval a : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ) ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) a = z) ↔
    Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0
have mpr : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0 →
  ∃ (a : ℝ), Eq (α := ℝ) ((aeval a : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ) ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) a = z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
w : ℝ
hw : Eq (α := ℝ) ((aeval w : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ)
⊢ Eq (α := ℂ) (((aeval ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) w) : ℚ[X] →ₐ[ℚ] ℂ) : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
have rw : Eq (α := ℂ) ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) ((aeval w : (a : ℚ[X]) → ℝ) p : ℝ) : ℂ) (0 : ℂ)
Tactic: rw [aeval_algHom_apply, hw, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
w : ℝ
hw : Eq (α := ℝ) ((aeval w : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ)
rw : Eq (α := ℂ) ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) ((aeval w : (a : ℚ[X]) → ℝ) p : ℝ) : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) (((aeval ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) w) : ℚ[X] →ₐ[ℚ] ℂ) : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
have rw₁ : Eq (α := ℂ) ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) 0 : ℂ) (0 : ℂ)
Tactic: rw [aeval_algHom_apply, hw, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
w : ℝ
hw : Eq (α := ℝ) ((aeval w : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ)
rw : Eq (α := ℂ) ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) ((aeval w : (a : ℚ[X]) → ℝ) p : ℝ) : ℂ) (0 : ℂ)
rw₁ : Eq (α := ℂ) ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) 0 : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) (((aeval ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) w) : ℚ[X] →ₐ[ℚ] ℂ) : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
have rw₂ : Eq (α := ℂ) 0 0
Tactic: rw [aeval_algHom_apply, hw, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
z : ℂ
hz1 : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz2 : z.im = 0
⊢ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re = z
have a₁ : re ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re) = z.re
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
z : ℂ
hz1 : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz2 : z.im = 0
a₁ : re ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re) = z.re
⊢ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re = z
have a₂ : im ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re) = z.im
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
z : ℂ
hz1 : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz2 : z.im = 0
⊢ im ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re) = z.im
have a₁ : im ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re) = 0
Tactic: rw [hz2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
z : ℂ
hz1 : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz2 : z.im = 0
⊢ ∃ (a : ℝ), Eq (α := ℝ) ((aeval a : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ) ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) a = z
have key : (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re = z
Tactic: have key : IsScalarTower.toAlgHom ℚ ℝ ℂ z.re = z := by
        ext
        · rfl
        · rw [hz2]; rfl
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
z : ℂ
hz1 : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz2 : z.im = 0
key : (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re = z
⊢ Eq (α := ℂ) ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) ((aeval z.re : (a : ℚ[X]) → ℝ) p : ℝ) : ℂ)
    ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) 0 : ℂ)
have rwa : Eq (α := ℂ) (((aeval ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re) : ℚ[X] →ₐ[ℚ] ℂ) : (a : ℚ[X]) → ℂ) p : ℂ)
  ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) 0 : ℂ)
Tactic: rwa [← aeval_algHom_apply, key, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
z : ℂ
hz1 : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz2 : z.im = 0
key : (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re = z
rwa :
  Eq (α := ℂ) (((aeval ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re) : ℚ[X] →ₐ[ℚ] ℂ) : (a : ℚ[X]) → ℂ) p : ℂ)
    ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) 0 : ℂ)
⊢ Eq (α := ℂ) ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) ((aeval z.re : (a : ℚ[X]) → ℝ) p : ℝ) : ℂ)
    ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) 0 : ℂ)
have rwa₁ : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) 0 : ℂ)
Tactic: rwa [← aeval_algHom_apply, key, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ a.card = b.card + c.card
have hb : ∀ (z : ℂ), z ∈ b ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0
Tactic: have hb : ∀ z : ℂ, z ∈ b ↔ aeval z p = 0 ∧ z.im = 0 := by
    intro z
    simp_rw [b, Finset.mem_image, Set.mem_toFinset, mem_rootSet_of_ne hp]
    constructor
    · rintro ⟨w, hw, rfl⟩
      exact ⟨by rw [aeval_algHom_apply, hw, map_zero], rfl⟩
    · rintro ⟨hz1, hz2⟩
      have key : IsScalarTower.toAlgHom ℚ ℝ ℂ z.re = z := by
        ext
        · rfl
        · rw [hz2]; rfl
      exact ⟨z.re, inj (by rwa [← aeval_algHom_apply, key, map_zero]), key⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun (a : { x : ℂ // x ∈ p.rootSet ℂ }) ↦ (↑a : ℂ))
    (Equiv.Perm.support
      ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
ha : ∀ (z : ℂ), z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
hb : ∀ (z : ℂ), z ∈ b ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0
w : (↑(p.rootSet ℂ) : Type)
⊢ (((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
              ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal) :
            Equiv.Perm (↑(p.rootSet ℂ) : Type)) :
          (a : (↑(p.rootSet ℂ) : Type)) → (↑(p.rootSet ℂ) : Type))
        w =
      w ↔
    (↑w : ℂ).im = 0
have rw : (AlgEquiv.restrictScalars ℚ conjAe : (a : ℂ) → ℂ) (↑w : ℂ) = (↑w : ℂ) ↔ (↑w : ℂ).im = 0
Tactic: rw [Subtype.ext_iff, galActionHom_restrict]