awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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
⊢ Finset.card (α := (↑(p.rootSet ℂ) : Type))
      (Equiv.Perm.support ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) conj')) =
    2
have h3₁ : ℕ
Tactic: apply Nat.add_left_cancel
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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
⊢ Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
have have : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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
⊢ Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
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))
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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))
⊢ Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
have 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 ℂ)) ⊤
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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 ℂ)) ⊤
⊢ Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
have h0 : ∀ (h1 : Fintype.card (↑(p.rootSet ℂ) : Type) = p.natDegree) (x : Equiv.Perm (↑(p.rootSet ℂ) : Type)),
  Nat.Prime (Fintype.card (↑(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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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))
⊢ Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
have 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 ℂ))
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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 ℂ))
⊢ Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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
⊢ Function.Bijective (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (⇑(galActionHom p ℂ) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
have apply : Fintype.card (↑(p.rootSet ℂ) : Type) = Fintype.card (↑(p.rootSet ℝ) : Type) + 2
Tactic: apply galActionHom_bijective_of_prime_degree p_irr p_deg
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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
n : ℕ :=
  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)))
⊢ HPow.hPow (α := Equiv.Perm (↑(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))
      2 =
    1
have rw : Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
  ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
      (HPow.hPow (α := p.Gal) (β := ℕ)
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal) 2) :
    Equiv.Perm (↑(p.rootSet ℂ) : Type))
  (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
Tactic: rw [← map_pow, ← map_pow,
          show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from
            AlgEquiv.ext Complex.conj_conj,
          map_one, map_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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
n : ℕ :=
  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)))
rw :
  Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        (HPow.hPow (α := p.Gal) (β := ℕ)
          ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal) 2) :
      Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
⊢ HPow.hPow (α := Equiv.Perm (↑(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))
      2 =
    1
have rw₁ : Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
  ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
      ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal)
          (HPow.hPow (α := Gal(ℂ/ℚ)) (β := ℕ) (AlgEquiv.restrictScalars ℚ conjAe) 2) :
        p.Gal) :
    Equiv.Perm (↑(p.rootSet ℂ) : Type))
  (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
Tactic: rw [← map_pow, ← map_pow,
          show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from
            AlgEquiv.ext Complex.conj_conj,
          map_one, map_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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
n : ℕ :=
  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)))
rw :
  Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        (HPow.hPow (α := p.Gal) (β := ℕ)
          ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal) 2) :
      Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
rw₁ :
  Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal)
            (HPow.hPow (α := Gal(ℂ/ℚ)) (β := ℕ) (AlgEquiv.restrictScalars ℚ conjAe) 2) :
          p.Gal) :
      Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
⊢ HPow.hPow (α := Equiv.Perm (↑(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))
      2 =
    1
have rw₂ : Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
  ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) 1) :
    Equiv.Perm (↑(p.rootSet ℂ) : Type))
  (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
Tactic: rw [← map_pow, ← map_pow,
          show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from
            AlgEquiv.ext Complex.conj_conj,
          map_one, map_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
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
n : ℕ :=
  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)))
rw :
  Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        (HPow.hPow (α := p.Gal) (β := ℕ)
          ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal) 2) :
      Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
rw₁ :
  Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
        ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal)
            (HPow.hPow (α := Gal(ℂ/ℚ)) (β := ℕ) (AlgEquiv.restrictScalars ℚ conjAe) 2) :
          p.Gal) :
      Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
rw₂ :
  Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
    ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) 1) :
      Equiv.Perm (↑(p.rootSet ℂ) : Type))
    (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
⊢ HPow.hPow (α := Equiv.Perm (↑(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))
      2 =
    1
have rw₃ : Eq (α := Equiv.Perm (↑(p.rootSet ℂ) : Type))
  ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type)) 1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
  (1 : Equiv.Perm (↑(p.rootSet ℂ) : Type))
Tactic: rw [← map_pow, ← map_pow,
          show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from
            AlgEquiv.ext Complex.conj_conj,
          map_one, map_one]