-- 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
have : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
have₁ :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree),
    Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
      (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
have₂ : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
have₃ have₄ have₅ :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree),
    Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
      (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
have₆ :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree) (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)),
    Eq (α := Subgroup (Equiv.Perm (↑(p.rootSet ℂ) : Type))) (MonoidHom.range (galActionHom p ℂ)) ⊤
h0 :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree) (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)),
    Nat.Prime (Fintype.card (↑(p.rootSet ℂ) : Type))
h1 :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree) (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)),
    Fintype.card (↑(p.rootSet ℂ) : Type) ∣ Fintype.card ↥(MonoidHom.range (galActionHom p ℂ))
h2 :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree),
    let 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))
h3 :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree),
    let conj' : p.Gal := (restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe);
    ∀ (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)),
      Equiv.Perm.IsSwap (α := (↑(p.rootSet ℂ) : Type))
        ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')
τ :
  (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree) →
    (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)) → Equiv.Perm (↑(p.rootSet ℂ) : Type)
h1₁ :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree) (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)),
    Fintype.card (↑(p.rootSet ℂ) : Type) ∣ Fintype.card ↥(MonoidHom.range (galActionHom p ℂ))
h2₁ :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree),
    let 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))
h3₁ :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree),
    let conj' : p.Gal := (restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe);
    ∀ (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)),
      Equiv.Perm.IsSwap (α := (↑(p.rootSet ℂ) : Type))
        ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')
τ₁ :
  (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree) →
    (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)) → Equiv.Perm (↑(p.rootSet ℂ) : Type)
h2₂ :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree),
    let 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))
h3₂ :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree),
    let conj' : p.Gal := (restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe);
    ∀ (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)),
      Equiv.Perm.IsSwap (α := (↑(p.rootSet ℂ) : Type))
        ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')
τ₂ :
  (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree) →
    (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)) → Equiv.Perm (↑(p.rootSet ℂ) : Type)
h3₃ :
  ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree),
    let conj' : p.Gal := (restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe);
    ∀ (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)),
      Equiv.Perm.IsSwap (α := (↑(p.rootSet ℂ) : Type))
        ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')
⊢ Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))

Tactic:
classical
  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)
  let conj' := restrict p ℂ (Complex.conjAe.restrictScalars ℚ)
  refine
    ⟨galActionHom_injective p ℂ, fun x =>
      (congr_arg (x ∈ ·) (show (galActionHom p ℂ).range = ⊤ from ?_)).mpr
        (Subgroup.mem_top x)⟩
  apply Equiv.Perm.subgroup_eq_top_of_swap_mem
  · rwa [h1]
  · rw [h1]
    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
  · exact ⟨conj', rfl⟩
  · rw [← Equiv.Perm.card_support_eq_two]
    apply Nat.add_left_cancel
    rw [← p_roots, ← Set.toFinset_card (rootSet p ℝ), ← Set.toFinset_card (rootSet p ℂ)]
    exact (card_complex_roots_eq_card_real_add_card_not_gal_inv p).symm

Premises used: Polynomial.Gal.galActionHom_injective, Real, Polynomial.rootSet, Polynomial.Gal.prime_degree_dvd_card, MulEquiv.toEquiv, Set.toFinset_card, Nat.card_congr, Equiv.Perm.subgroup_eq_top_of_swap_mem, Nat.add_left_cancel, Equiv.Perm.card_support_eq_two, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, Complex, Equiv.symm, MonoidHom.ofInjective, Eq.symm, Fintype.card_eq_nat_card