-- 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 : ℂ)
neg₉ :
  ∀ (a : ℂ),
    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 : ℂ) →
      a.im = 0 → Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
neg₁₁ :
  ∀ (a : ℂ),
    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 : ℂ) →
      a.im = 0 → Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
neg₁₃ :
  ∀ (a : ℂ),
    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 : ℂ) →
      a.im = 0 → ¬Eq (α := ℂ) ((aeval a : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) → False
⊢ ∀ (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 → ¬a.im = 0 → False
Tactic: tauto