-- Mathlib/Analysis/Complex/Polynomial/Basic.lean
theorem galActionHom_bijective_of_prime_degree' {p : ℚ[X]} (p_irr : Irreducible p)
    (p_deg : p.natDegree.Prime)
    (p_roots1 : Fintype.card (p.rootSet ℝ) + 1 ≤ Fintype.card (p.rootSet ℂ))
    (p_roots2 : Fintype.card (p.rootSet ℂ) ≤ Fintype.card (p.rootSet ℝ) + 3) :
    Function.Bijective (galActionHom p ℂ)

Proof state:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2

Tactic:
have hn : 2 ∣ n :=
  Equiv.Perm.two_dvd_card_support
    (by
       rw [← MonoidHom.map_pow, ← MonoidHom.map_pow,
        show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from
          AlgEquiv.ext Complex.conj_conj,
        MonoidHom.map_one, MonoidHom.map_one])

Result:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
hn : 2 ∣ n
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2

Proof state:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
⊢ (galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)) ^ 2 = 1

Tactic:
rw [← MonoidHom.map_pow, ← MonoidHom.map_pow,
 show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from
   AlgEquiv.ext Complex.conj_conj,
 MonoidHom.map_one, MonoidHom.map_one]

Result:
no goals

Proof state:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
hn : 2 ∣ n
key :
  Fintype.card ↑(p.rootSet ℂ) =
    Fintype.card ↑(p.rootSet ℝ) + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2

Tactic:
omega

Result:
no goals

Proof state:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
⊢ Function.Bijective ⇑(galActionHom p ℂ)

Tactic:
apply galActionHom_bijective_of_prime_degree p_irr p_deg

Result:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2

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

Tactic:
let n := (galActionHom p ℂ (restrict p ℂ (Complex.conjAe.restrictScalars ℚ))).support.card

Result:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2

Proof state:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
hn : 2 ∣ n
key :
  (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2

Tactic:
simp_rw [Set.toFinset_card] at key

Result:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
hn : 2 ∣ n
key :
  Fintype.card ↑(p.rootSet ℂ) =
    Fintype.card ↑(p.rootSet ℝ) + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2

Proof state:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
hn : 2 ∣ n
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2

Tactic:
have key := card_complex_roots_eq_card_real_add_card_not_gal_inv p

Result:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
hn : 2 ∣ n
key :
  (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2