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 : ℂ)
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
neg₁ : Disjoint b c
⊢ a.card = b.card + c.card

Tactic:
rw [← Finset.card_union_of_disjoint]

Premises used: Finset.card_union_of_disjoint
-- 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
hc : ∀ (z : ℂ), z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
neg : a = b ∪ c
⊢ a.card = (b ∪ c).card

Tactic:
apply congr_arg Finset.card

Premises used: congr_arg, Finset.card
-- 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
hc : ∀ (z : ℂ), z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.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 = b ∪ c

Tactic:
simp_rw [Finset.ext_iff, Finset.mem_union, ha, hb, hc]

Premises used: Finset.ext_iff, Finset.mem_union
-- 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
hc : ∀ (z : ℂ), z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
neg : ∀ ⦃a : ℂ⦄, a ∈ b → a ∉ c
⊢ Disjoint b c

Tactic:
rw [Finset.disjoint_left]

Premises used: Finset.disjoint_left
-- 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
hc : ∀ (z : ℂ), z ∈ c ↔ Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0
z : ℂ
neg :
  Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im = 0 →
    ¬(Eq (α := ℂ) ((aeval z : (a : ℚ[X]) → ℂ) p : ℂ) (0 : ℂ) ∧ z.im ≠ 0)
⊢ z ∈ b → z ∉ c

Tactic:
rw [hb, hc]
-- 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
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
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)

Tactic:
tauto
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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
simp_rw : (p.aroots ℂ).toFinset.card = p.natDegree
⊢ Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree

Tactic:
simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]

Premises used: Finset.coe_sort_coe, Polynomial.rootSet_def, Fintype.card_coe
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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
rw₁ : (p.aroots ℂ).Nodup
⊢ (p.aroots ℂ).toFinset.card = p.natDegree

Tactic:
rw [Multiset.toFinset_card_of_nodup, ← Splits.natDegree_eq_card_roots, natDegree_map]

Premises used: Polynomial.natDegree_map, Polynomial.Splits.natDegree_eq_card_roots, Multiset.toFinset_card_of_nodup
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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
⊢ (map (algebraMap ℚ ℂ) p).Splits

Tactic:
IsAlgClosed.splits _

Premises used: IsAlgClosed.splits
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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
⊢ (map (algebraMap ℚ ℂ) p).Splits

Tactic:
exact IsAlgClosed.splits _

Premises used: IsAlgClosed.splits
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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 ℂ).Nodup

Tactic:
nodup_roots ((separable_map (algebraMap ℚ ℂ)).mpr p_irr.separable)

Premises used: Iff.mpr, Algebra.algebraMap, Rat, Irreducible.separable, Complex, Polynomial.nodup_roots, Polynomial.separable_map
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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 ℂ).Nodup

Tactic:
exact nodup_roots ((separable_map (algebraMap ℚ ℂ)).mpr p_irr.separable)

Premises used: Iff.mpr, Algebra.algebraMap, Rat, Irreducible.separable, Complex, Polynomial.nodup_roots, Polynomial.separable_map
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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

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

Tactic:
⟨galActionHom_injective p ℂ, fun x =>
      (congr_arg (x ∈ ·) (show (galActionHom p ℂ).range = ⊤ from ?_)).mpr
        (Subgroup.mem_top x)⟩

Premises used: Eq.mpr, Polynomial.Gal.galActionHom_injective, Membership.mem, congr_arg, And.intro, Subgroup.mem_top, Function.Bijective, Complex
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)
p₁ :
  ∀ (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)),
    Eq (α := Subgroup (Equiv.Perm (↑(p.rootSet ℂ) : Type))) (MonoidHom.range (galActionHom p ℂ)) ⊤
⊢ Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))

Tactic:
refine
    ⟨galActionHom_injective p ℂ, fun x =>
      (congr_arg (x ∈ ·) (show (galActionHom p ℂ).range = ⊤ from ?_)).mpr
        (Subgroup.mem_top x)⟩
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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))
h3 :
  Equiv.Perm.IsSwap (α := (↑(p.rootSet ℂ) : Type))
    ((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 ℂ)) ⊤

Tactic:
apply Equiv.Perm.subgroup_eq_top_of_swap_mem

Premises used: Equiv.Perm.subgroup_eq_top_of_swap_mem
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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 h0₁ h0₂ h0₃ : Nat.Prime p.natDegree
⊢ Nat.Prime (Fintype.card (↑(p.rootSet ℂ) : Type))

Tactic:
rwa [h1]
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)
h1₁ : p.natDegree ∣ Fintype.card ↥(MonoidHom.range (galActionHom p ℂ))
⊢ Fintype.card (↑(p.rootSet ℂ) : Type) ∣ Fintype.card ↥(MonoidHom.range (galActionHom p ℂ))

Tactic:
rw [h1]
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)
⊢ p.natDegree ∣ Fintype.card ↥(MonoidHom.range (galActionHom p ℂ))

Tactic:
simpa only [Fintype.card_eq_nat_card,
      Nat.card_congr (MonoidHom.ofInjective (galActionHom_injective p ℂ)).toEquiv.symm]
      using prime_degree_dvd_card p_irr p_deg

Premises used: Polynomial.Gal.galActionHom_injective, Polynomial.Gal.prime_degree_dvd_card, MulEquiv.toEquiv, Nat.card_congr, Complex, Equiv.symm, MonoidHom.ofInjective, Fintype.card_eq_nat_card
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)
⊢ 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:
⟨conj', rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)
⊢ 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:
exact ⟨conj', rfl⟩
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)
h3 :
  Finset.card (α := (↑(p.rootSet ℂ) : Type))
      (Equiv.Perm.support ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')) =
    2
⊢ Equiv.Perm.IsSwap (α := (↑(p.rootSet ℂ) : Type))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')

Tactic:
rw [← Equiv.Perm.card_support_eq_two]

Premises used: Equiv.Perm.card_support_eq_two
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)
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
h3₁ : ℕ
⊢ Finset.card (α := (↑(p.rootSet ℂ) : Type))
      (Equiv.Perm.support ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')) =
    2

Tactic:
apply Nat.add_left_cancel

Premises used: Nat.add_left_cancel
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)
⊢ (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')) =
    (p.rootSet ℂ).toFinset.card

Tactic:
(card_complex_roots_eq_card_real_add_card_not_gal_inv p).symm

Premises used: Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, Eq.symm
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
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)
⊢ (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')) =
    (p.rootSet ℂ).toFinset.card

Tactic:
exact (card_complex_roots_eq_card_real_add_card_not_gal_inv p).symm

Premises used: Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, Eq.symm
-- Module: Mathlib.Analysis.Complex.Polynomial.Basic
Goal:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card (↑(p.rootSet ℝ) : Type) + 1 ≤ Fintype.card (↑(p.rootSet ℂ) : Type)
p_roots2 : Fintype.card (↑(p.rootSet ℂ) : Type) ≤ Fintype.card (↑(p.rootSet ℝ) : Type) + 3
apply : 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))

Tactic:
apply galActionHom_bijective_of_prime_degree p_irr p_deg

Premises used: Polynomial.Gal.galActionHom_bijective_of_prime_degree