awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
h₁g : DiffContOnCl.{0, 0, u_1} ℂ (F := E) (fun (z : ℂ) ↦ f (z + c)) (ball 0 R)
h₂g : Membership.mem (γ := Set ℂ) (ball 0 R) (w - c)
⊢ Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
simpa [← circleAverage_map_add_const, herglotzRieszKernel_def]
    using circleAverage_re_smul_on_ball_zero h₁g h₂g

Premises used: Real.circleAverage_map_add_const, herglotzRieszKernel_def, _private.0.DiffContOnCl.circleAverage_re_smul_on_ball_zero
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • f z) c R = f w

Tactic:
hf.circleAverage_re_herglotzRieszKernel_smul hw

Premises used: DiffContOnCl.circleAverage_re_herglotzRieszKernel_smul
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
simp_rw : Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
⊢ Real.circleAverage (poissonKernel c w • f) c R = f w

Tactic:
simp_rw [poissonKernel_eq_re_herglotzRieszKernel]

Premises used: poissonKernel_eq_re_herglotzRieszKernel
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
⊢ Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
apply hf.circleAverage_re_herglotzRieszKernel_smul hw

Premises used: DiffContOnCl.circleAverage_re_herglotzRieszKernel_smul
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
⊢ Real.circleAverage
      (fun (z : ℂ) ↦
        ((HPow.hPow (β := ℕ) ‖z - c‖ 2 - HPow.hPow (β := ℕ) ‖w - c‖ 2) / HPow.hPow (β := ℕ) ‖z - c - (w - c)‖ 2) • f z)
      c R =
    f w

Tactic:
apply hf.circleAverage_poissonKernel_smul hw

Premises used: DiffContOnCl.circleAverage_poissonKernel_smul
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
f : ℂ[X]
hf : 0 < f.degree
by_contra! : ∀ (hf' : ∀ (z : ℂ), ¬f.IsRoot z), False
⊢ ∃ (z : ℂ), f.IsRoot z

Tactic:
by_contra! hf'
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
z : ℂ
⊢ Filter.Tendsto (fun (x : ℂ) ↦ eval x f) (cobounded ℂ) (cobounded ℂ)

Tactic:
simpa only [tendsto_norm_atTop_iff_cobounded]
          using f.tendsto_norm_atTop hf tendsto_norm_cobounded_atTop

Premises used: Polynomial.tendsto_norm_atTop, tendsto_norm_cobounded_atTop, tendsto_norm_atTop_iff_cobounded
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
⊢ ∀ (z : ℂ), (eval z f)⁻¹ = 0

Tactic:
have (z : ℂ) : (f.eval z)⁻¹ = 0 :=
    (f.differentiable.inv hf').apply_eq_of_tendsto_cocompact z <|
      Metric.cobounded_eq_cocompact (α := ℂ) ▸ (Filter.tendsto_inv₀_cobounded.comp <| by
        simpa only [tendsto_norm_atTop_iff_cobounded]
          using f.tendsto_norm_atTop hf tendsto_norm_cobounded_atTop)
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
this : ∀ (z : ℂ), (eval z f)⁻¹ = 0
z : ℂ
⊢ (eval z f)⁻¹ = (eval z ((C : (a : ℂ) → ℂ[X]) 0))⁻¹

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
this : ∀ (z : ℂ), (eval z f)⁻¹ = 0
⊢ 0 < degree (R := ℂ) ((C : (a : ℂ) → ℂ[X]) 0)

Tactic:
obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this]

Premises used: Polynomial.C, Polynomial.funext, inv_injective, OfNat.ofNat, DFunLike.coe, rfl
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
this : ∀ (z : ℂ), (eval z f)⁻¹ = 0
hf₁ : 0 < degree (R := ℂ) ((C : (a : ℂ) → ℂ[X]) 0)
⊢ ∀ (z : ℂ), ¬IsRoot ((C : (a : ℂ) → ℂ[X]) 0) z

Tactic:
obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this]

Premises used: Polynomial.C, Polynomial.funext, inv_injective, OfNat.ofNat, DFunLike.coe, rfl
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
this : ∀ (z : ℂ), (eval z f)⁻¹ = 0
hf₁ : 0 < degree (R := ℂ) ((C : (a : ℂ) → ℂ[X]) 0)
hf'₁ : ∀ (z : ℂ), ¬IsRoot ((C : (a : ℂ) → ℂ[X]) 0) z
⊢ ∀ (z : ℂ), (eval z ((C : (a : ℂ) → ℂ[X]) 0))⁻¹ = 0

Tactic:
obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this]

Premises used: Polynomial.C, Polynomial.funext, inv_injective, OfNat.ofNat, DFunLike.coe, rfl
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
hf : 0 < degree (R := ℂ) ((C : (a : ℂ) → ℂ[X]) 0)
hf' : ∀ (z : ℂ), ¬IsRoot ((C : (a : ℂ) → ℂ[X]) 0) z
this : ∀ (z : ℂ), (eval z ((C : (a : ℂ) → ℂ[X]) 0))⁻¹ = 0
⊢ False

Tactic:
simp at hf
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
⊢ IsAlgClosed ℂ

Tactic:
IsAlgClosed.of_exists_root _ fun _p _ hp => Complex.exists_root <| degree_pos_of_irreducible hp

Premises used: Complex.exists_root, Polynomial.degree_pos_of_irreducible, IsAlgClosed.of_exists_root
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Algebra ℝ F
inst_2 : Algebra.IsAlgebraic ℝ F
⊢ Nonempty.{max 1 (u_1 + 1)} (F ≃ₐ[ℝ] ℝ) ∨ Nonempty.{max 1 (u_1 + 1)} (F ≃ₐ[ℝ] ℂ)

Tactic:
IsAlgClosed.nonempty_algEquiv_or_of_finrank_eq_two F Complex.finrank_real_complex

Premises used: Complex.finrank_real_complex, IsAlgClosed.nonempty_algEquiv_or_of_finrank_eq_two
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
⊢ Fact (map (algebraMap ℚ ℂ) p).Splits

Tactic:
⟨IsAlgClosed.splits _⟩

Premises used: Fact.mk, IsAlgClosed.splits
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
pos :
  ∀ (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)))
neg :
  ∀ (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)))
⊢ (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)))

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
hp : p = 0
rw : IsEmpty (↑∅ : Type)
⊢ IsEmpty (↑(p.rootSet ℂ) : Type)

Tactic:
rw [hp, rootSet_zero]

Premises used: Polynomial.rootSet_zero
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
hp : p = 0
⊢ IsEmpty (↑∅ : Type)

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
hp : p = 0
⊢ IsEmpty (↑(p.rootSet ℂ) : Type)

Tactic:
haveI : IsEmpty (p.rootSet ℂ) := by rw [hp, rootSet_zero]; infer_instance
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)) ∅
pos₃ : Finset.card (α := ℂ) ∅ = Finset.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)))

Tactic:
simp_rw [(galActionHom p ℂ _).support.eq_empty_of_isEmpty, hp, rootSet_zero,
      Set.toFinset_empty, Finset.card_empty]

Premises used: Equiv.Perm.support, Polynomial.rootSet_zero, Set.toFinset_empty, Finset.card_empty, Finset.eq_empty_of_isEmpty, Polynomial.Gal.galActionHom, Complex, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
hp : ¬p = 0
⊢ Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)

Tactic:
have inj : Function.Injective (IsScalarTower.toAlgHom ℚ ℝ ℂ) := (algebraMap ℝ ℂ).injective
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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 =
    (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)))

Tactic:
rw [← Finset.card_image_of_injective _ Subtype.coe_injective, ←
    Finset.card_image_of_injective _ inj]

Premises used: Finset.card_image_of_injective, Subtype.coe_injective
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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))))
neg₁ : Finset ℂ
⊢ (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:
let a : Finset ℂ := ?_
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
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))))
neg₁ : Finset ℂ
⊢ (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:
let b : Finset ℂ := ?_
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective (α := ℝ) (β := ℂ) (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ) : (a : ℝ) → ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
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))))
neg₁ : Finset ℂ
⊢ (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:
on_goal 1 => let b : Finset ℂ := ?_
-- 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
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))))
neg₁ : Finset ℂ
⊢ (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:
let c : Finset ℂ := ?_
-- 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
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))))
neg₁ : Finset ℂ
⊢ (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:
on_goal 1 => let c : Finset ℂ := ?_
-- 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)))
z : ℂ
rw : z ∈ p.rootSet ℂ ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
rw₁ rw₂ :
  Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ z ∈ a ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)

Tactic:
rw [Set.mem_toFinset, mem_rootSet_of_ne hp]

Premises used: Polynomial.mem_rootSet_of_ne, Set.mem_toFinset
-- 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)))
⊢ ∀ (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]
-- 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 : ℂ
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
⊢ z ∈ b ↔ 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]

Premises used: Finset.mem_image, Polynomial.mem_rootSet_of_ne, Set.mem_toFinset
-- 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 : ℂ
mp :
  (∃ (a : ℝ),
      Eq (α := ℝ) ((aeval a : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ) ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (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 : ℝ),
      Eq (α := ℝ) ((aeval a : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ) ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) a = z
⊢ (∃ (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
-- 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 : ℂ)
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 : ℂ)
rw₂ rw₃ : Eq (α := ℂ) 0 0
⊢ Eq (α := ℂ) (((aeval ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) w) : ℚ[X] →ₐ[ℚ] ℂ) : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ)

Tactic:
rw [aeval_algHom_apply, hw, 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 : ℂ)
w : ℝ
hw : Eq (α := ℝ) ((aeval w : (a : ℚ[X]) → ℝ) p : ℝ) (0 : ℝ)
⊢ Eq (α := ℂ) (((aeval ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) w) : ℚ[X] →ₐ[ℚ] ℂ) : (a : ℚ[X]) → ℂ) p : ℂ)
      (0 : ℂ) ∧
    im ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) w) = 0

Tactic:
exact ⟨by rw [aeval_algHom_apply, hw, map_zero], 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₁ : re ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re) = z.re
a₂ : im ((IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re) = z.im
⊢ (IsScalarTower.toAlgHom ℚ ℝ ℂ : (a : ℝ) → ℂ) z.re = z

Tactic:
ext