awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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
⊢ re ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re) = z.re

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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₁ : im ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re) = 0
⊢ im ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re) = z.im

Tactic:
rw [hz2]
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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) = 0

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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

Tactic:
have key : IsScalarTower.toAlgHom ℚ ℝ ℂ z.re = z := by
        ext
        · rfl
        · rw [hz2]; rfl
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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 : ℂ)
rwa₁ : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) 0 : ℂ)
rwa₂ rwa₃ rwa₄ rwa₅ : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) ((aeval z.re : (a : ℚ[X]) → ℝ) p : ℝ) : ℂ)
    ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) 0 : ℂ)

Tactic:
rwa [← aeval_algHom_apply, key, map_zero]

Premises used: map_zero, Polynomial.aeval_algHom_apply
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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
⊢ ∃ (a : ℝ), Eq (α := ℝ) ((aeval a : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ) ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) a = z

Tactic:
exact ⟨z.re, inj (by rwa [← aeval_algHom_apply, key, map_zero]), key⟩
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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

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⟩
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)
rw : (AlgEquiv.restrictScalars ℚ conjAe : (a : ℂ) → ℂ) (↑w : ℂ) = (↑w : ℂ) ↔ (↑w : ℂ).im = 0
⊢ (((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:
rw [Subtype.ext_iff, galActionHom_restrict]

Premises used: Polynomial.Gal.galActionHom_restrict, Subtype.ext_iff
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)
⊢ (AlgEquiv.restrictScalars ℚ conjAe : (a : ℂ) → ℂ) (↑w : ℂ) = (↑w : ℂ) ↔ (↑w : ℂ).im = 0

Tactic:
Complex.conj_eq_iff_im

Premises used: Complex.conj_eq_iff_im
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)
⊢ (AlgEquiv.restrictScalars ℚ conjAe : (a : ℂ) → ℂ) (↑w : ℂ) = (↑w : ℂ) ↔ (↑w : ℂ).im = 0

Tactic:
exact Complex.conj_eq_iff_im

Premises used: Complex.conj_eq_iff_im
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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

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
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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 : ℂ
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
⊢ z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0

Tactic:
simp_rw [c, Finset.mem_image]

Premises used: Finset.mem_image
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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
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
⊢ (∃ (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
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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
w : { x : ℂ // x ∈ p.rootSet ℂ }
hw :
  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)))
    w
⊢ Eq (α := ℂ) ((aeval (↑w : ℂ) : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ (↑w : ℂ).im ≠ 0

Tactic:
⟨(mem_rootSet.mp w.2).2, mt (hc0 w).mpr (Equiv.Perm.mem_support.mp hw)⟩

Premises used: Iff.mpr, Equiv.Perm.mem_support, mt, And.right, And.intro, Iff.mp, Polynomial.mem_rootSet, Subtype.property
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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
w : { x : ℂ // x ∈ p.rootSet ℂ }
hw :
  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)))
    w
⊢ Eq (α := ℂ) ((aeval (↑w : ℂ) : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ (↑w : ℂ).im ≠ 0

Tactic:
exact ⟨(mem_rootSet.mp w.2).2, mt (hc0 w).mpr (Equiv.Perm.mem_support.mp hw)⟩
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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 : ℂ
hz1 : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz2 : 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:
⟨⟨z, mem_rootSet.mpr ⟨hp, hz1⟩⟩, Equiv.Perm.mem_support.mpr (mt (hc0 _).mp hz2), rfl⟩

Premises used: Iff.mpr, Equiv.Perm.mem_support, mt, Subtype.mk, And.intro, Exists.intro, Iff.mp, Polynomial.mem_rootSet, rfl
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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 : ℂ
hz1 : Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
hz2 : 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:
exact ⟨⟨z, mem_rootSet.mpr ⟨hp, hz1⟩⟩, Equiv.Perm.mem_support.mpr (mt (hc0 _).mp hz2), rfl⟩
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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

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⟩