awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
inst_4 : CharZero K
inst_5 : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) ℤ (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) ℤ (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)
⊢ Nonempty (K ≃+* L)
have obtain : ∀ (e : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)), Nonempty (K ≃+* L)
Tactic: obtain ⟨e⟩ := Cardinal.lift_mk_eq'.1 this
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
⊢ Nonempty (K ≃+* L)
have obtain : ∀ (s : Set K)
  (hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))),
  Nonempty (K ≃+* L)
Tactic: obtain ⟨s, hs⟩ := exists_isTranscendenceBasis (ZMod p) K
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
⊢ Nonempty (K ≃+* L)
have obtain : ∀ (t : Set L)
  (ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))),
  Nonempty (K ≃+* L)
Tactic: obtain ⟨t, ht⟩ := exists_isTranscendenceBasis (ZMod p) L
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
⊢ ℵ₀ < #L
have rwa : ℵ₀ < Cardinal.lift.{u, v} #L
Tactic: rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
rwa : ℵ₀ < Cardinal.lift.{u, v} #L
⊢ ℵ₀ < #L
have rwa₁ : ℵ₀ < Cardinal.lift.{v, u} #K
Tactic: rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
⊢ Nonempty (K ≃+* L)
have hL : ℵ₀ < #L
Tactic: have hL : ℵ₀ < #L := by
    rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)
have rw : Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L
Tactic: rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        hs (le_of_lt (lt_aleph0_of_finite _)) hK),
      ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        ht (le_of_lt (lt_aleph0_of_finite _)) hL)]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
⊢ Nonempty (K ≃+* L)
have this₁ : Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)
Tactic: have : Cardinal.lift.{v} #s = Cardinal.lift.{u} #t := by
    rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        hs (le_of_lt (lt_aleph0_of_finite _)) hK),
      ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        ht (le_of_lt (lt_aleph0_of_finite _)) hL)]
    exact Cardinal.lift_mk_eq'.2 hKL
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : Fact (Nat.Prime p)
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this_1 : Algebra (ZMod p) K := ZMod.algebra K p
this_2 : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis.{u, 0, u} (ι := { x : K // x ∈ s }) (ZMod p) (Subtype.val (p := fun (x : K) ↦ x ∈ s))
t : Set L
ht : IsTranscendenceBasis.{v, 0, v} (ι := { x : L // x ∈ t }) (ZMod p) (Subtype.val (p := fun (x : L) ↦ x ∈ t))
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #(↑s : Type u) = Cardinal.lift.{u, v} #(↑t : Type v)
⊢ Nonempty (K ≃+* L)
have obtain : ∀ (e : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)), Nonempty (K ≃+* L)
Tactic: obtain ⟨e⟩ := Cardinal.lift_mk_eq'.1 this
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : CharP K p
inst_5 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
⊢ Nonempty (K ≃+* L)
have inl : ∀ (hp : Nat.Prime p), Nonempty (K ≃+* L)
Tactic: rcases CharP.char_is_prime_or_zero K p with (hp | hp)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : CharP K p
inst_5 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
inl : ∀ (hp : Nat.Prime p), Nonempty (K ≃+* L)
⊢ Nonempty (K ≃+* L)
have inr : ∀ (hp : p = 0), Nonempty (K ≃+* L)
Tactic: rcases CharP.char_is_prime_or_zero K p with (hp | hp)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : CharP K p
inst_5 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : Nat.Prime p
⊢ Nonempty (K ≃+* L)
have this : Fact (Nat.Prime p)
Tactic: haveI : Fact p.Prime := ⟨hp⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : IsAlgClosed K
inst_3 : IsAlgClosed L
p : ℕ
inst_4 : CharP K p
inst_5 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : p = 0
⊢ Nonempty (K ≃+* L)
have inst : CharP K 0
Tactic: simp only [hp] at *
Cleared hypotheses: inst_4, inst_5, hp
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (hypothesis)
Goal:
K : Type u
L : Type v
inst_1 : Field K
inst_2 : Field L
inst_3 : IsAlgClosed K
inst_4 : IsAlgClosed L
p : ℕ
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : p = 0
inst : CharP K 0
⊢ Nonempty (K ≃+* L)
have inst₁ : CharP L 0
Tactic: simp only [hp] at *
Cleared hypotheses: inst_5, inst_6, hp
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Classification (hypothesis)
Goal:
K : Type u
L : Type v
inst_1 : Field K
inst_2 : Field L
inst_3 : IsAlgClosed K
inst_4 : IsAlgClosed L
p : ℕ
inst_5 : CharP K p
inst_6 : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : p = 0
inst : CharP K 0
inst₁ : CharP L 0
⊢ Nonempty (K ≃+* L)
have hp₁ : True
Tactic: simp only [hp] at *
Cleared hypotheses: inst_5, inst_6, hp
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
p : R[X]
a : A
h :
  ¬IsUnit.{v} (M := A)
      ((aeval a : (a : R[X]) → A)
          (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              p.roots)) :
        A)
⊢ ∃ k ∈ σ a, eval k p = 0
have h₁ : ¬IsUnit.{v} (M := A)
    (List.prod
      (List.map (α := R[X]) (⇑(aeval a) : (a : R[X]) → A)
        (Multiset.toList
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p.roots))))
Tactic: rw [← Multiset.prod_toList, map_list_prod] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
p : R[X]
a : A
h :
  ¬IsUnit.{v} (M := A)
      (List.prod
        (List.map (α := R[X]) (⇑(aeval a) : (a : R[X]) → A)
          (Multiset.toList
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              p.roots))))
⊢ ∃ k ∈ σ a, eval k p = 0
have h₁ : ¬∀ (m : A),
    Membership.mem (γ := List A)
        (List.map (α := R[X]) (⇑(aeval a) : (a : R[X]) → A)
          (Multiset.toList
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p.roots)))
        m →
      IsUnit m
Tactic: replace h := mt List.prod_isUnit h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
p : R[X]
a : A
h :
  ¬∀ (m : A),
      Membership.mem (γ := List A)
          (List.map (α := R[X]) (⇑(aeval a) : (a : R[X]) → A)
            (Multiset.toList
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
                p.roots)))
          m →
        IsUnit m
⊢ ∃ k ∈ σ a, eval k p = 0
have h₁ : ∃ a_1 ∈ p.roots, ¬IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : R) → A) a_1 : A))
Tactic: simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map, aeval_X,
    exists_exists_and_eq_and, Multiset.mem_map, map_sub] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
p : R[X]
a : A
h : ∃ a_1 ∈ p.roots, ¬IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : R) → A) a_1 : A))
⊢ ∃ k ∈ σ a, eval k p = 0
have rcases : ∀ (r : R) (r_mem : r ∈ p.roots) (r_nu : ¬IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : R) → A) r : A))),
  ∃ k ∈ σ a, eval k p = 0
Tactic: rcases h with ⟨r, r_mem, r_nu⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ p.roots
r_nu : ¬IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : R) → A) r : A))
⊢ r ∈ σ a
have rwa : ¬IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
Tactic: rwa [mem_iff, ← IsUnit.sub_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
⊢ (fun (x : 𝕜) ↦ eval x p) k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)
have hroot : q.IsRoot k
Tactic: have hroot : IsRoot q k := by simp only [q, eval_C, eval_sub, sub_self, IsRoot.def]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
hroot : q.IsRoot k
⊢ (fun (x : 𝕜) ↦ eval x p) k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)
have hroot₁ : HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X *
    -(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X])) =
  q
Tactic: rw [← mul_div_eq_iff_isRoot, ← neg_mul_neg, neg_sub] at hroot
Cleared hypotheses: hroot
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
hroot :
  HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X *
      -(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X])) =
    q
⊢ (fun (x : 𝕜) ↦ eval x p) k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)
have aeval_q_eq : HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) (eval k p) : A) ((aeval a : (a : 𝕜[X]) → A) p : A) =
  (aeval a : (a : 𝕜[X]) → A) q
Tactic: have aeval_q_eq : ↑ₐ (eval k p) - aeval a p = aeval a q := by
    simp only [q, aeval_C, map_sub]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
hroot :
  HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X *
      -(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X])) =
    q
aeval_q_eq :
  HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) (eval k p) : A) ((aeval a : (a : 𝕜[X]) → A) p : A) =
    (aeval a : (a : 𝕜[X]) → A) q
⊢ (fun (x : 𝕜) ↦ eval x p) k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)
have rw : ¬IsUnit
    (HMul.hMul (α := A) (β := A)
      ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)
      ((aeval a : (a : 𝕜[X]) → A) (-(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]))) : A))
Tactic: rw [mem_iff, aeval_q_eq, ← hroot, aeval_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
hroot :
  HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X *
      -(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X])) =
    q
aeval_q_eq :
  HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) (eval k p) : A) ((aeval a : (a : 𝕜[X]) → A) p : A) =
    (aeval a : (a : 𝕜[X]) → A) q
⊢ ¬IsUnit
      (HMul.hMul (α := A) (β := A)
        ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)
        ((aeval a : (a : 𝕜[X]) → A) (-(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]))) : A))
have hcomm : Commute.{v} (S := A)
  ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)
  ((aeval a : (a : 𝕜[X]) → A) (-(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]))) : A)
Tactic: have hcomm := (Commute.all (C k - X) (-(q / (X - C k)))).map (aeval a : 𝕜[X] →ₐ[𝕜] A)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (eval k p) : 𝕜[X]) p
hroot :
  HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X *
      -(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X])) =
    q
aeval_q_eq :
  HSub.hSub (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) (eval k p) : A) ((aeval a : (a : 𝕜[X]) → A) p : A) =
    (aeval a : (a : 𝕜[X]) → A) q
hcomm :
  Commute.{v} (S := A)
    ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)
    ((aeval a : (a : 𝕜[X]) → A) (-(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]))) : A)
⊢ ¬IsUnit
      (HMul.hMul (α := A) (β := A)
        ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)
        ((aeval a : (a : 𝕜[X]) → A) (-(q / HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]))) : A))
have apply : ¬IsUnit.{v} (M := A)
    ((aeval a : (a : 𝕜[X]) → A) (HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) X) : A)
Tactic: apply mt fun h => (hcomm.isUnit_mul_iff.mp h).1
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
⊢ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A) = (fun (x : 𝕜) ↦ eval x p) '' σ a
have refine : ∀ (k : 𝕜) (hk : k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)),
  Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' σ a) k
Tactic: refine Set.eq_of_subset_of_subset (fun k hk => ?_) (subset_polynomial_aeval a p)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)
⊢ Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' σ a) k
have hprod : HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p =
  HMul.hMul (α := 𝕜[X]) (β := 𝕜[X])
    ((C : (a : 𝕜) → 𝕜[X]) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff : 𝕜[X])
    (Multiset.prod
        (Multiset.map (fun (x : 𝕜) ↦ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) x : 𝕜[X]))
          (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).roots) :
      𝕜[X])
Tactic: have hprod := (IsAlgClosed.splits (C k - p)).eq_prod_roots
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)
hprod :
  HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p =
    HMul.hMul (α := 𝕜[X]) (β := 𝕜[X])
      ((C : (a : 𝕜) → 𝕜[X]) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff : 𝕜[X])
      (Multiset.prod
          (Multiset.map (fun (x : 𝕜) ↦ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) x : 𝕜[X]))
            (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).roots) :
        𝕜[X])
⊢ Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' σ a) k
have h_ne : HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p ≠ 0
Tactic: have h_ne : C k - p ≠ 0 := ne_zero_of_degree_gt <| by
    rwa [degree_sub_eq_right_of_degree_lt (lt_of_le_of_lt degree_C_le hdeg)]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)
hprod :
  HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p =
    HMul.hMul (α := 𝕜[X]) (β := 𝕜[X])
      ((C : (a : 𝕜) → 𝕜[X]) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff : 𝕜[X])
      (Multiset.prod
          (Multiset.map (fun (x : 𝕜) ↦ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) x : 𝕜[X]))
            (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).roots) :
        𝕜[X])
h_ne : HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p ≠ 0
⊢ Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' σ a) k
have lead_ne : (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff ≠ 0
Tactic: have lead_ne := leadingCoeff_ne_zero.mpr h_ne
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Spectrum (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : k ∈ spectrum.{u, v} 𝕜 (A := A) ((aeval a : (a : 𝕜[X]) → A) p : A)
hprod :
  HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p =
    HMul.hMul (α := 𝕜[X]) (β := 𝕜[X])
      ((C : (a : 𝕜) → 𝕜[X]) (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff : 𝕜[X])
      (Multiset.prod
          (Multiset.map (fun (x : 𝕜) ↦ HSub.hSub (α := 𝕜[X]) (β := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) x : 𝕜[X]))
            (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).roots) :
        𝕜[X])
h_ne : HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p ≠ 0
lead_ne : (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff ≠ 0
⊢ Membership.mem (γ := Set 𝕜) ((fun (x : 𝕜) ↦ eval x p) '' σ a) k
have lead_unit : IsUnit.{v} (M := A)
  (↑(((Units.map (↑↑ₐ : 𝕜 →* A) : MonoidHom.{u, v} 𝕜ˣ Aˣ) : (a : 𝕜ˣ) → Aˣ)
        (Units.mk0 (HSub.hSub (α := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) k : 𝕜[X]) p).leadingCoeff lead_ne)) :
    A)
Tactic: have lead_unit := (Units.map ↑ₐ.toMonoidHom (Units.mk0 _ lead_ne)).isUnit