awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℂ)
hb : ∀ (z : ℂ), z ∈ b ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0
⊢ a.card = b.card + c.card
have hc0 : ∀ (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
Tactic: have hc0 :
    ∀ w : p.rootSet ℂ, galActionHom p ℂ (restrict p ℂ (Complex.conjAe.restrictScalars ℚ)) w = w ↔
        w.val.im = 0 := by
    intro w
    rw [Subtype.ext_iff, galActionHom_restrict]
    exact Complex.conj_eq_iff_im
-- 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
hc0 :
  ∀ (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
z : ℂ
⊢ z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
have simp_rw : (∃ (a : { x : ℂ // x ∈ p.rootSet ℂ }),
    Membership.mem (γ := Finset { x : ℂ // x ∈ p.rootSet ℂ })
        (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 ∧
      (↑a : ℂ) = z) ↔
  Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
Tactic: simp_rw [c, Finset.mem_image]
-- 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
hc0 :
  ∀ (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
z : ℂ
⊢ (∃ (a : { x : ℂ // x ∈ p.rootSet ℂ }),
      Membership.mem (γ := Finset { x : ℂ // x ∈ p.rootSet ℂ })
          (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 ∧
        (↑a : ℂ) = z) ↔
    Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
have mp : (∃ (a : { x : ℂ // x ∈ p.rootSet ℂ }),
    Membership.mem (γ := Finset { x : ℂ // x ∈ p.rootSet ℂ })
        (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 ∧
      (↑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 : ℂ)
hb : ∀ (z : ℂ), z ∈ b ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0
hc0 :
  ∀ (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
z : ℂ
mp :
  (∃ (a : { x : ℂ // x ∈ p.rootSet ℂ }),
      Membership.mem (γ := Finset { x : ℂ // x ∈ p.rootSet ℂ })
          (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 ∧
        (↑a : ℂ) = z) →
    Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
⊢ (∃ (a : { x : ℂ // x ∈ p.rootSet ℂ }),
      Membership.mem (γ := Finset { x : ℂ // x ∈ p.rootSet ℂ })
          (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 ∧
        (↑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 : { x : ℂ // x ∈ p.rootSet ℂ }),
    Membership.mem (γ := Finset { x : ℂ // x ∈ p.rootSet ℂ })
        (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 ∧
      (↑a : ℂ) = z
Tactic: constructor
-- 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 : ℂ)
hb : ∀ (z : ℂ), z ∈ b ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0
hc0 :
  ∀ (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
⊢ a.card = b.card + c.card
have hc : ∀ (z : ℂ), z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
Tactic: have hc : ∀ z : ℂ, z ∈ c ↔ aeval z p = 0 ∧ z.im ≠ 0 := by
    intro z
    simp_rw [c, Finset.mem_image]
    constructor
    · rintro ⟨w, hw, rfl⟩
      exact ⟨(mem_rootSet.mp w.2).2, mt (hc0 w).mpr (Equiv.Perm.mem_support.mp hw)⟩
    · rintro ⟨hz1, hz2⟩
      exact ⟨⟨z, mem_rootSet.mpr ⟨hp, hz1⟩⟩, Equiv.Perm.mem_support.mpr (mt (hc0 _).mp 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 : ℂ)
hb : ∀ (z : ℂ), z ∈ b ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0
hc0 :
  ∀ (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
hc : ∀ (z : ℂ), z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
⊢ a.card = b.card + c.card
have neg : a.card = (b ∪ c).card
Tactic: rw [← Finset.card_union_of_disjoint]
-- 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
hc0 :
  ∀ (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
hc : ∀ (z : ℂ), z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
neg : a.card = (b ∪ c).card
⊢ a.card = b.card + c.card
have neg₁ : Disjoint b c
Tactic: rw [← Finset.card_union_of_disjoint]
-- 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
hc0 :
  ∀ (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
hc : ∀ (z : ℂ), z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
⊢ a.card = (b ∪ c).card
have neg : a = b ∪ c
Tactic: apply congr_arg Finset.card
-- 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
hc0 :
  ∀ (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
hc : ∀ (z : ℂ), z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
⊢ a = b ∪ c
have neg : ∀ (a : ℂ),
  Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ↔
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0
Tactic: simp_rw [Finset.ext_iff, Finset.mem_union, ha, hb, hc]
-- 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
hc0 :
  ∀ (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
hc : ∀ (z : ℂ), z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
neg neg₁ :
  ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ↔
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
        Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0
⊢ ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ↔
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
        Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0
have neg₂ : ∀ (a : ℂ),
  Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) →
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0
Tactic: tauto
-- 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
hc0 :
  ∀ (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
hc : ∀ (z : ℂ), z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
neg neg₁ :
  ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ↔
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
        Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0
neg₂ :
  ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) →
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
        Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0
⊢ ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ↔
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
        Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0
have neg₃ : ∀ (a : ℂ),
  Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0 →
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
Tactic: tauto
-- 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
hc0 :
  ∀ (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
hc : ∀ (z : ℂ), z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
neg neg₁ :
  ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ↔
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
        Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0
neg₂ :
  ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) →
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
        Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0
neg₃ :
  ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
        Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0 →
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
neg₄ neg₅ :
  ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) →
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
        Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0
⊢ ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ↔
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0 ∨
        Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im ≠ 0
have neg₆ : ∀ (a : ℂ),
  Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) →
    ¬(Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0) →
      Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
Tactic: tauto