-- Mathlib/Analysis/Complex/Polynomial/Basic.lean
theorem galActionHom_bijective_of_prime_degree {p : ℚ[X]} (p_irr : Irreducible p)
    (p_deg : p.natDegree.Prime)
    (p_roots : Fintype.card (p.rootSet ℂ) = Fintype.card (p.rootSet ℝ) + 2) :
    Function.Bijective (galActionHom p ℂ)

Proof state:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ (galActionHom p ℂ).range = ⊤

Tactic:
apply Equiv.Perm.subgroup_eq_top_of_swap_mem

Result:
case h0
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ Nat.Prime (Fintype.card ↑(p.rootSet ℂ))

case h1
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ Fintype.card ↑(p.rootSet ℂ) ∣ Fintype.card ↥(galActionHom p ℂ).range

case h2
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ ?τ ∈ (galActionHom p ℂ).range

case h3
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ Equiv.Perm.IsSwap ?τ

case τ
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ Equiv.Perm ↑(p.rootSet ℂ)

Proof state:
case h1
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ Fintype.card ↑(p.rootSet ℂ) ∣ Fintype.card ↥(galActionHom p ℂ).range

Tactic:
rw [h1]

Result:
case h1
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ p.natDegree ∣ Fintype.card ↥(galActionHom p ℂ).range

Proof state:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
⊢ Fintype.card ↑(p.rootSet ℂ) = p.natDegree

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

Result:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
⊢ (p.aroots ℂ).toFinset.card = p.natDegree

Proof state:
case h1
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ p.natDegree ∣ Fintype.card ↥(galActionHom p ℂ).range

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

Result:
no goals