awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 : ℂ),
    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) → 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
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
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 : ℂ)
neg₇ :
  ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) →
      ¬(Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 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 : ℂ)
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
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 : ℂ)
neg₇ :
  ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) →
      ¬(Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ a.im = 0) → a.im ≠ 0
neg₈ :
  ∀ (a : ℂ),
    Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) →
      a.im = 0 → Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (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 : ℂ)
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
⊢ Disjoint b c
have neg : ∀ ⦃a : ℂ⦄, a ∈ b → a ∉ c
Tactic: rw [Finset.disjoint_left]
-- 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
z : ℂ
⊢ z ∈ b → z ∉ c
have neg : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0 →
  ¬(Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0)
Tactic: rw [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
z : ℂ
⊢ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0 →
    ¬(Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0)
have neg : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) →
  z.im = 0 → ¬(Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.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
z : ℂ
neg neg₁ :
  Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) →
    z.im = 0 → ¬(Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0)
neg₂ :
  Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) →
    z.im = 0 → Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0 → False
⊢ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0 →
    ¬(Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0)
have neg₃ : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) →
  z.im = 0 → Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) → z.im ≠ 0 → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
⊢ Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
have simp_rw : (p.aroots ℂ).toFinset.card = p.natDegree
Tactic: simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
⊢ (p.aroots ℂ).toFinset.card = p.natDegree
have rw : (map (algebraMap ℚ ℂ) p).Splits
Tactic: rw [Multiset.toFinset_card_of_nodup, ← Splits.natDegree_eq_card_roots, natDegree_map]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
rw : (map (algebraMap ℚ ℂ) p).Splits
⊢ (p.aroots ℂ).toFinset.card = p.natDegree
have rw₁ : (p.aroots ℂ).Nodup
Tactic: rw [Multiset.toFinset_card_of_nodup, ← Splits.natDegree_eq_card_roots, natDegree_map]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
⊢ Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
have h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
Tactic: have h1 : Fintype.card (p.rootSet ℂ) = p.natDegree := by
    simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
    rw [Multiset.toFinset_card_of_nodup, ← Splits.natDegree_eq_card_roots, natDegree_map]
    · exact IsAlgClosed.splits _
    · exact nodup_roots ((separable_map (algebraMap ℚ ℂ)).mpr p_irr.separable)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
conj' : p.Gal := (restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe)
⊢ Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
have p₁ : ∀ (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)),
  Eq (α := Subgroup (Equiv.Perm (↑(p.rootSet ℂ) : Type))) (MonoidHom.range (galActionHom p ℂ)) ⊤
Tactic: refine
    ⟨galActionHom_injective p ℂ, fun x =>
      (congr_arg (x ∈ ·) (show (galActionHom p ℂ).range = ⊤ from ?_)).mpr
        (Subgroup.mem_top x)⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
conj' : p.Gal := (restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm (↑(p.rootSet ℂ) : Type)
⊢ Eq (α := Subgroup (Equiv.Perm (↑(p.rootSet ℂ) : Type))) (MonoidHom.range (galActionHom p ℂ)) ⊤
have h0 : Nat.Prime (Fintype.card (↑(p.rootSet ℂ) : Type))
Tactic: apply Equiv.Perm.subgroup_eq_top_of_swap_mem
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
conj' : p.Gal := (restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm (↑(p.rootSet ℂ) : Type)
h0 : Nat.Prime (Fintype.card (↑(p.rootSet ℂ) : Type))
⊢ Eq (α := Subgroup (Equiv.Perm (↑(p.rootSet ℂ) : Type))) (MonoidHom.range (galActionHom p ℂ)) ⊤
have h1₁ : Fintype.card (↑(p.rootSet ℂ) : Type) ∣ Fintype.card ↥(MonoidHom.range (galActionHom p ℂ))
Tactic: apply Equiv.Perm.subgroup_eq_top_of_swap_mem
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
conj' : p.Gal := (restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm (↑(p.rootSet ℂ) : Type)
h0 : Nat.Prime (Fintype.card (↑(p.rootSet ℂ) : Type))
h1₁ : Fintype.card (↑(p.rootSet ℂ) : Type) ∣ Fintype.card ↥(MonoidHom.range (galActionHom p ℂ))
⊢ Eq (α := Subgroup (Equiv.Perm (↑(p.rootSet ℂ) : Type))) (MonoidHom.range (galActionHom p ℂ)) ⊤
have h2 : Membership.mem (α := Equiv.Perm (↑(p.rootSet ℂ) : Type)) (γ := Subgroup (Equiv.Perm (↑(p.rootSet ℂ) : Type)))
  (MonoidHom.range (galActionHom p ℂ))
  ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj' : Equiv.Perm (↑(p.rootSet ℂ) : Type))
Tactic: apply Equiv.Perm.subgroup_eq_top_of_swap_mem
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
conj' : p.Gal := (restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm (↑(p.rootSet ℂ) : Type)
h0 : Nat.Prime (Fintype.card (↑(p.rootSet ℂ) : Type))
h1₁ : Fintype.card (↑(p.rootSet ℂ) : Type) ∣ Fintype.card ↥(MonoidHom.range (galActionHom p ℂ))
h2 :
  Membership.mem (α := Equiv.Perm (↑(p.rootSet ℂ) : Type)) (γ := Subgroup (Equiv.Perm (↑(p.rootSet ℂ) : Type)))
    (MonoidHom.range (galActionHom p ℂ))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj' : Equiv.Perm (↑(p.rootSet ℂ) : Type))
⊢ Eq (α := Subgroup (Equiv.Perm (↑(p.rootSet ℂ) : Type))) (MonoidHom.range (galActionHom p ℂ)) ⊤
have h3 : Equiv.Perm.IsSwap (α := (↑(p.rootSet ℂ) : Type))
  ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')
Tactic: apply Equiv.Perm.subgroup_eq_top_of_swap_mem
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
conj' : p.Gal := (restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm (↑(p.rootSet ℂ) : Type)
⊢ Fintype.card (↑(p.rootSet ℂ) : Type) ∣ Fintype.card ↥(MonoidHom.range (galActionHom p ℂ))
have h1₁ : p.natDegree ∣ Fintype.card ↥(MonoidHom.range (galActionHom p ℂ))
Tactic: rw [h1]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
conj' : p.Gal := (restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm (↑(p.rootSet ℂ) : Type)
⊢ Equiv.Perm.IsSwap (α := (↑(p.rootSet ℂ) : Type))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')
have h3 : Finset.card (α := (↑(p.rootSet ℂ) : Type))
    (Equiv.Perm.support ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')) =
  2
Tactic: rw [← Equiv.Perm.card_support_eq_two]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
conj' : p.Gal := (restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm (↑(p.rootSet ℂ) : Type)
⊢ Finset.card (α := (↑(p.rootSet ℂ) : Type))
      (Equiv.Perm.support ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')) =
    2
have h3 : Fintype.card (↑(p.rootSet ℝ) : Type) +
    Finset.card (α := (↑(p.rootSet ℂ) : Type))
      (Equiv.Perm.support ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')) =
  Fintype.card (↑(p.rootSet ℝ) : Type) + 2
Tactic: apply Nat.add_left_cancel