awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S,
      ∀ c ∈ f.rootSet S,
        ∀ d ∈ f.rootSet S,
          Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
            Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
              a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}
hπ : ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)
x : (↑(f.rootSet S) : Type u_2)
hx : g • x ≠ x
⊢ (↑(g • g • x) : S) = (↑x : S)
have key : Eq (α := Set S) {g • g • (↑x : S), g • (↑x : S)} {g • (↑x : S), (↑x : S)}
Tactic: have key := hp (g • g • x) (g • g • x).2 (g • x) (g • x).2 (g • x) (g • x).2 x x.2
      (by simp [hπ]) (by simp [hπ]) (by simpa [← rootSet.coe_smul]) (by simpa [← rootSet.coe_smul])
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
hp : (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ p) (f.rootSet (S ⧸ p)) + 1
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
⊢ Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g :
        Equiv.Perm (↑(f.rootSet S) : Type u_2))
      (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
    Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g)
have pos : ∀ (hfp : Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0),
  Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g :
        Equiv.Perm (↑(f.rootSet S) : Type u_2))
      (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
    Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g)
Tactic: classical
  by_cases hfp : f.map (algebraMap R (S ⧸ p)) = 0
  · rw [rootSet_def f (S ⧸ p), aroots_def, hfp, roots_zero, Multiset.toFinset_zero,
      Finset.coe_empty, Set.ncard_empty, zero_add, Set.ncard_le_one_iff_subsingleton,
      ← Set.subsingleton_coe] at hp
    exact Or.inl (Subsingleton.elim _ _)
  let π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
  rw [← hf.image_rootSet_of_map_ne_zero π hfp, Set.ncard_le_ncard_image_add_one_iff] at hp
  have hπ (x : S) : π (g • x) = π x := (Ideal.Quotient.mk_eq_mk_iff_sub_mem (g • x) x).mpr (hg x)
  rw [or_iff_not_imp_left, Equiv.ext_iff, not_forall]
  rintro ⟨x, hx : g • x ≠ x⟩
  refine ⟨g • x, x, hx, ?_⟩
  ext z
  simp only [Equiv.swap_apply_def, MulAction.toPermHom_apply, MulAction.toPerm_apply]
  split_ifs with hz hz'
  · subst hz
    have key := hp (g • g • x) (g • g • x).2 (g • x) (g • x).2 (g • x) (g • x).2 x x.2
      (by simp [hπ]) (by simp [hπ]) (by simpa [← rootSet.coe_smul]) (by simpa [← rootSet.coe_smul])
    grind [rootSet.coe_smul]
  · simp [hz']
  · grind [rootSet.coe_smul, SetLike.coe_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
hp : (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ p) (f.rootSet (S ⧸ p)) + 1
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
pos :
  ∀ (hfp : Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0),
    Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g :
          Equiv.Perm (↑(f.rootSet S) : Type u_2))
        (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
      Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g)
⊢ Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g :
        Equiv.Perm (↑(f.rootSet S) : Type u_2))
      (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
    Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g)
have neg : ∀ (hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0),
  Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g :
        Equiv.Perm (↑(f.rootSet S) : Type u_2))
      (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
    Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g)
Tactic: classical
  by_cases hfp : f.map (algebraMap R (S ⧸ p)) = 0
  · rw [rootSet_def f (S ⧸ p), aroots_def, hfp, roots_zero, Multiset.toFinset_zero,
      Finset.coe_empty, Set.ncard_empty, zero_add, Set.ncard_le_one_iff_subsingleton,
      ← Set.subsingleton_coe] at hp
    exact Or.inl (Subsingleton.elim _ _)
  let π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
  rw [← hf.image_rootSet_of_map_ne_zero π hfp, Set.ncard_le_ncard_image_add_one_iff] at hp
  have hπ (x : S) : π (g • x) = π x := (Ideal.Quotient.mk_eq_mk_iff_sub_mem (g • x) x).mpr (hg x)
  rw [or_iff_not_imp_left, Equiv.ext_iff, not_forall]
  rintro ⟨x, hx : g • x ≠ x⟩
  refine ⟨g • x, x, hx, ?_⟩
  ext z
  simp only [Equiv.swap_apply_def, MulAction.toPermHom_apply, MulAction.toPerm_apply]
  split_ifs with hz hz'
  · subst hz
    have key := hp (g • g • x) (g • g • x).2 (g • x) (g • x).2 (g • x) (g • x).2 x x.2
      (by simp [hπ]) (by simp [hπ]) (by simpa [← rootSet.coe_smul]) (by simpa [← rootSet.coe_smul])
    grind [rootSet.coe_smul]
  · simp [hz']
  · grind [rootSet.coe_smul, SetLike.coe_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
hf : Splits (map (algebraMap R S) f)
inst_7 : MulAction.IsPretransitive.{u_3, u_2} G (↑(f.rootSet S) : Type u_2)
h :
  ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ m.asIdeal) (f.rootSet (S ⧸ m.asIdeal)) + 1
hG : Eq.{u_3 + 1} (α := Subgroup G) (⨆ (m : MaximalSpectrum S), Ideal.inertia G m.asIdeal) ⊤
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := G) (β := Equiv.Perm (↑(f.rootSet S) : Type u_2))
    (⇑(MulAction.toPermHom G (↑(f.rootSet S) : Type u_2)) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2))
have hS1 : ∀ (σ : G),
  Membership.mem (γ := Set G) (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)) σ →
    Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ :
          Equiv.Perm (↑(f.rootSet S) : Type u_2))
        (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
      Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ)
Tactic: apply surjective_of_isSwap_of_isPretransitive'
      (⋃ m : MaximalSpectrum S, m.asIdeal.inertia G)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
hf : Splits (map (algebraMap R S) f)
inst_7 : MulAction.IsPretransitive.{u_3, u_2} G (↑(f.rootSet S) : Type u_2)
h :
  ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ m.asIdeal) (f.rootSet (S ⧸ m.asIdeal)) + 1
hG : Eq.{u_3 + 1} (α := Subgroup G) (⨆ (m : MaximalSpectrum S), Ideal.inertia G m.asIdeal) ⊤
hS1 :
  ∀ (σ : G),
    Membership.mem (γ := Set G) (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)) σ →
      Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
          ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ :
            Equiv.Perm (↑(f.rootSet S) : Type u_2))
          (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
        Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
          ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ)
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := G) (β := Equiv.Perm (↑(f.rootSet S) : Type u_2))
    (⇑(MulAction.toPermHom G (↑(f.rootSet S) : Type u_2)) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2))
have hS2 : Eq.{u_3 + 1} (α := Subgroup G) (Subgroup.closure (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G))) ⊤
Tactic: apply surjective_of_isSwap_of_isPretransitive'
      (⋃ m : MaximalSpectrum S, m.asIdeal.inertia G)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
hf : Splits (map (algebraMap R S) f)
inst_7 : MulAction.IsPretransitive.{u_3, u_2} G (↑(f.rootSet S) : Type u_2)
h :
  ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ m.asIdeal) (f.rootSet (S ⧸ m.asIdeal)) + 1
hG : Eq.{u_3 + 1} (α := Subgroup G) (⨆ (m : MaximalSpectrum S), Ideal.inertia G m.asIdeal) ⊤
σ : G
hσ : Membership.mem (γ := Set G) (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)) σ
⊢ Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ :
        Equiv.Perm (↑(f.rootSet S) : Type u_2))
      (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
    Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ)
have hS1 : ∀ (m : MaximalSpectrum S) (hm : σ ∈ (↑(Ideal.inertia G m.asIdeal) : Set G)),
  Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ :
        Equiv.Perm (↑(f.rootSet S) : Type u_2))
      (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
    Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ)
Tactic: obtain ⟨m, hm⟩ := Set.mem_iUnion.mp hσ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
hf : Splits (map (algebraMap R S) f)
inst_7 : MulAction.IsPretransitive.{u_3, u_2} G (↑(f.rootSet S) : Type u_2)
h :
  ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ m.asIdeal) (f.rootSet (S ⧸ m.asIdeal)) + 1
hG : Eq.{u_3 + 1} (α := Subgroup G) (⨆ (m : MaximalSpectrum S), Ideal.inertia G m.asIdeal) ⊤
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := G) (β := Equiv.Perm (↑(f.rootSet S) : Type u_2))
    (⇑(MulAction.toPermHom G (↑(f.rootSet S) : Type u_2)) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2))
have hS1 : ∀ (σ : G),
  Membership.mem (γ := Set G) (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)) σ →
    Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ :
          Equiv.Perm (↑(f.rootSet S) : Type u_2))
        (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
      Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ)
Tactic: classical
  apply surjective_of_isSwap_of_isPretransitive'
      (⋃ m : MaximalSpectrum S, m.asIdeal.inertia G)
  · intro σ hσ
    obtain ⟨m, hm⟩ := Set.mem_iUnion.mp hσ
    exact hf.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia m.asIdeal (h m) σ hm
  · simpa [Subgroup.closure_iUnion]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
hf : Splits (map (algebraMap R S) f)
inst_7 : MulAction.IsPretransitive.{u_3, u_2} G (↑(f.rootSet S) : Type u_2)
h :
  ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ m.asIdeal) (f.rootSet (S ⧸ m.asIdeal)) + 1
hG : Eq.{u_3 + 1} (α := Subgroup G) (⨆ (m : MaximalSpectrum S), Ideal.inertia G m.asIdeal) ⊤
hS1 :
  ∀ (σ : G),
    Membership.mem (γ := Set G) (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)) σ →
      Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
          ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ :
            Equiv.Perm (↑(f.rootSet S) : Type u_2))
          (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
        Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
          ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ)
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := G) (β := Equiv.Perm (↑(f.rootSet S) : Type u_2))
    (⇑(MulAction.toPermHom G (↑(f.rootSet S) : Type u_2)) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2))
have hS2 : Eq.{u_3 + 1} (α := Subgroup G) (Subgroup.closure (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G))) ⊤
Tactic: classical
  apply surjective_of_isSwap_of_isPretransitive'
      (⋃ m : MaximalSpectrum S, m.asIdeal.inertia G)
  · intro σ hσ
    obtain ⟨m, hm⟩ := Set.mem_iUnion.mp hσ
    exact hf.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia m.asIdeal (h m) σ hm
  · simpa [Subgroup.closure_iUnion]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
r : R
inst : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
have refine : IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
Tactic: refine Commute.isNilpotent_mul_right (commute_X_pow _ _).symm ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
r : R
inst : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
have obtain : ∀ (m : ℕ) (hm : r ^ m = 0), IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
Tactic: obtain ⟨m, hm⟩ := hnil
Cleared hypotheses: hnil
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
r : R
inst : Semiring R
n m : ℕ
hm : r ^ m = 0
⊢ IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
have refine : HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) m = 0
Tactic: refine ⟨m, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
r : R
inst : Semiring R
n m : ℕ
hm : r ^ m = 0
⊢ HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) m = 0
have rw : Eq (α := R[X]) ((C : (a : R) → R[X]) (r ^ m) : R[X]) (0 : R[X])
Tactic: rw [← C_pow, hm, C_0]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
r : R
inst : Semiring R
n m : ℕ
hm : r ^ m = 0
rw : Eq (α := R[X]) ((C : (a : R) → R[X]) (r ^ m) : R[X]) (0 : R[X])
⊢ HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) m = 0
have rw₁ : Eq.{u_1 + 1} (α := R[X]) ((C : (a : R) → R[X]) 0) 0
Tactic: rw [← C_pow, hm, C_0]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
r : R
inst : Semiring R
n m : ℕ
hm : r ^ m = 0
rw : Eq (α := R[X]) ((C : (a : R) → R[X]) (r ^ m) : R[X]) (0 : R[X])
rw₁ : Eq.{u_1 + 1} (α := R[X]) ((C : (a : R) → R[X]) 0) 0
⊢ HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) m = 0
have rw₂ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [← C_pow, hm, C_0]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
r : R
inst : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X]))
have rw : IsNilpotent (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: rw [commute_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P
have refine_1 : ∀ (h : IsNilpotent (X * P)), IsNilpotent P
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
refine_1 : ∀ (h : IsNilpotent (X * P)), IsNilpotent P
⊢ IsNilpotent (X * P) ↔ IsNilpotent P
have refine_2 : IsNilpotent P → IsNilpotent (X * P)
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : IsNilpotent (X * P)
⊢ IsNilpotent P
have refine_1 : ∀ (h : IsNilpotent P), IsNilpotent P
Tactic: rwa [Commute.isNilpotent_mul_left_iff (commute_X P) (by simp)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
⊢ IsNilpotent (P * X) ↔ IsNilpotent P
have rw : IsNilpotent (X * P) ↔ IsNilpotent P
Tactic: rw [← commute_X P]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
⊢ IsNilpotent P ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)
have refine_1 : ∀ (h : ∀ (i : ℕ), IsNilpotent (P.coeff i)), IsNilpotent P
Tactic: refine
    ⟨P.recOnHorner (by simp) (fun p r hp₀ _ hp hpr i ↦ ?_) (fun p _ hnp hpX i ↦ ?_), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
refine_1 : ∀ (h : ∀ (i : ℕ), IsNilpotent (P.coeff i)), IsNilpotent P
⊢ IsNilpotent P ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)
have refine_2 : ∀ (p : R[X]) (r : R) (hp₀ : p.coeff 0 = 0),
  r ≠ 0 →
    ∀ (hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i))
      (hpr : IsNilpotent (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]))) (i : ℕ),
      IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff i)
Tactic: refine
    ⟨P.recOnHorner (by simp) (fun p r hp₀ _ hp hpr i ↦ ?_) (fun p _ hnp hpX i ↦ ?_), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
refine_1 : ∀ (h : ∀ (i : ℕ), IsNilpotent (P.coeff i)), IsNilpotent P
refine_2 :
  ∀ (p : R[X]) (r : R) (hp₀ : p.coeff 0 = 0),
    r ≠ 0 →
      ∀ (hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i))
        (hpr : IsNilpotent (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]))) (i : ℕ),
        IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff i)
⊢ IsNilpotent P ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)
have refine_3 : ∀ (p : R[X]),
  p ≠ 0 →
    ∀ (hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)) (hpX : IsNilpotent (p * X)) (i : ℕ),
      IsNilpotent ((p * X).coeff i)
Tactic: refine
    ⟨P.recOnHorner (by simp) (fun p r hp₀ _ hp hpr i ↦ ?_) (fun p _ hnp hpX i ↦ ?_), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
⊢ IsNilpotent P
have refine_1 : IsNilpotent (R := R[X]) (P.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a)
Tactic: rw [← sum_monomial_eq P]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]))
i : ℕ
⊢ IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
have obtain : ∀ (k : ℕ) (hk : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) ^ k = 0),
  IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
Tactic: obtain ⟨k, hk⟩ := hpr
Cleared hypotheses: hpr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
i k : ℕ
hk : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) ^ k = 0
⊢ eval 0 p = 0
have rwa : ∀ (hp₀ : Eq (α := R) ((aeval 0 : (a : R[X]) → R) p : R) (0 : R)),
  r ≠ 0 →
    ∀ (hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)) (i k : ℕ)
      (hk : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) ^ k = 0), eval 0 p = 0
Tactic: rwa [coeff_zero_eq_aeval_zero] at hp₀
Cleared hypotheses: hp₀, h, hp, i, k, hk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
i k : ℕ
hk : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) ^ k = 0
⊢ IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
have hp₁ : eval 0 p = 0
Tactic: replace hp : eval 0 p = 0 := by rwa [coeff_zero_eq_aeval_zero] at hp₀
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
i k : ℕ
hk : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) ^ k = 0
hp : eval 0 p = 0
⊢ IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
have refine : r ^ k = 0
Tactic: refine isNilpotent_C_iff.mpr ⟨k, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]))
i : ℕ
⊢ IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff i)
have hr : IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
Tactic: have hr : IsNilpotent (C r) := by
      obtain ⟨k, hk⟩ := hpr
      replace hp : eval 0 p = 0 := by rwa [coeff_zero_eq_aeval_zero] at hp₀
      refine isNilpotent_C_iff.mpr ⟨k, ?_⟩
      simpa [coeff_zero_eq_aeval_zero, hp] using congr_arg (fun q ↦ coeff q 0) hk