awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
⊢ Eq (α := A[T;T⁻¹]) ((antipode R : (a : A[T;T⁻¹]) → A[T;T⁻¹]) ((C : (a : A) → A[T;T⁻¹]) a) : A[T;T⁻¹])
    ((C : (a : A) → A[T;T⁻¹]) ((antipode R : (a : A) → A) a) : A[T;T⁻¹])
have rw : Eq (α := A[T;T⁻¹]) (AddMonoidAlgebra.single (-0) ((antipode R : (a : A) → A) a) : AddMonoidAlgebra A ℤ)
  ((C : (a : A) → A[T;T⁻¹]) ((antipode R : (a : A) → A) a) : A[T;T⁻¹])
Tactic: rw [← single_eq_C, AddMonoidAlgebra.antipode_single]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
n : ℤ
⊢ Eq.{u_2 + 1} (α := A[T;T⁻¹]) ((antipode R : (a : A[T;T⁻¹]) → A[T;T⁻¹]) (AddMonoidAlgebra.single n 1) : A[T;T⁻¹])
    (AddMonoidAlgebra.single (-n) 1 : AddMonoidAlgebra A ℤ)
have rw : Eq.{u_2 + 1} (α := A[T;T⁻¹]) (AddMonoidAlgebra.single (-n) ((antipode R : (a : A) → A) 1) : AddMonoidAlgebra A ℤ)
  (AddMonoidAlgebra.single (-n) 1 : AddMonoidAlgebra A ℤ)
Tactic: rw [AddMonoidAlgebra.antipode_single]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.TensorProduct (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Bialgebra R A
antipode : A →ₐ[R] A
mul_antipode_rTensor_comul :
  AlgHom.comp (Algebra.TensorProduct.lift antipode (AlgHom.id R A) ⋯ : A ⊗[R] A →ₐ[R] A)
      (Bialgebra.comulAlgHom R A : A →ₐ[R] A ⊗[R] A) =
    AlgHom.comp (Algebra.ofId R A) (Bialgebra.counitAlgHom R A)
mul_antipode_lTensor_comul :
  AlgHom.comp (Algebra.TensorProduct.lift (AlgHom.id R A) antipode ⋯ : A ⊗[R] A →ₐ[R] A)
      (Bialgebra.comulAlgHom R A : A →ₐ[R] A ⊗[R] A) =
    AlgHom.comp (Algebra.ofId R A) (Bialgebra.counitAlgHom R A)
⊢ Eq (α := A →ₗ[R] A)
    (LinearMap.mul' R A ∘ₗ
      LinearMap.rTensor A
          (↑antipode :
            [inst_3 : FunLike (A →ₐ[R] A) A A] → [SemilinearMapClass (A →ₐ[R] A) (RingHom.id R) A A] → A →ₗ[R] A) ∘ₗ
        comul)
    (Algebra.linearMap R A ∘ₗ counit)
have mul_antipode_rTensor_comul₁ : AlgHom.comp
    (AlgHom.comp (Algebra.TensorProduct.lmul' R) (Algebra.TensorProduct.map antipode (AlgHom.id R A)) :
      A ⊗[R] A →ₐ[R] A)
    (Bialgebra.comulAlgHom R A : A →ₐ[R] A ⊗[R] A) =
  AlgHom.comp (Algebra.ofId R A) (Bialgebra.counitAlgHom R A)
Tactic: rw [← Algebra.TensorProduct.lmul'_comp_map] at mul_antipode_rTensor_comul
Cleared hypotheses: mul_antipode_rTensor_comul, mul_antipode_lTensor_comul
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.TensorProduct (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Bialgebra R A
antipode : A →ₐ[R] A
mul_antipode_rTensor_comul :
  AlgHom.comp (Algebra.TensorProduct.lift antipode (AlgHom.id R A) ⋯ : A ⊗[R] A →ₐ[R] A)
      (Bialgebra.comulAlgHom R A : A →ₐ[R] A ⊗[R] A) =
    AlgHom.comp (Algebra.ofId R A) (Bialgebra.counitAlgHom R A)
mul_antipode_lTensor_comul :
  AlgHom.comp (Algebra.TensorProduct.lift (AlgHom.id R A) antipode ⋯ : A ⊗[R] A →ₐ[R] A)
      (Bialgebra.comulAlgHom R A : A →ₐ[R] A ⊗[R] A) =
    AlgHom.comp (Algebra.ofId R A) (Bialgebra.counitAlgHom R A)
⊢ Eq (α := A →ₗ[R] A)
    (LinearMap.mul' R A ∘ₗ
      LinearMap.lTensor A
          (↑antipode :
            [inst_3 : FunLike (A →ₐ[R] A) A A] → [SemilinearMapClass (A →ₐ[R] A) (RingHom.id R) A A] → A →ₗ[R] A) ∘ₗ
        comul)
    (Algebra.linearMap R A ∘ₗ counit)
have mul_antipode_lTensor_comul₁ : AlgHom.comp
    (AlgHom.comp (Algebra.TensorProduct.lmul' R) (Algebra.TensorProduct.map (AlgHom.id R A) antipode) :
      A ⊗[R] A →ₐ[R] A)
    (Bialgebra.comulAlgHom R A : A →ₐ[R] A ⊗[R] A) =
  AlgHom.comp (Algebra.ofId R A) (Bialgebra.counitAlgHom R A)
Tactic: rw [← Algebra.TensorProduct.lmul'_comp_map] at mul_antipode_lTensor_comul
Cleared hypotheses: mul_antipode_lTensor_comul
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M
inst_4 : Module R₀ M
inst_5 : Module R M
inst_6 : IsScalarTower R₀ R M
inst_7 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑(Ring.jacobson R) : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤;
    P ↥N → P (M ⧸ N) → P M
⊢ P M
have have : ∀ (ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))) (n : ℕ)
  (hn : HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0), P M
Tactic: have ⟨ss, n, hn⟩ := (isSemiprimaryRing_iff R).mp ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M
inst_4 : Module R₀ M
inst_5 : Module R M
inst_6 : IsScalarTower R₀ R M
inst_7 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n = 0
⊢ P M
have hn₁ : Jac ^ n ≤ Module.annihilator R M
Tactic: replace hn : Jac ^ n ≤ Module.annihilator R M := hn ▸ bot_le
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
M_1 : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M_1
inst_4 : Module R₀ M_1
inst_5 : Module R M_1
inst_6 : IsScalarTower R₀ R M_1
inst_7 : IsSemiprimaryRing R
P : (M : Type u) → [inst_12 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_12 : AddCommGroup M] [inst_13 : Module R₀ M] [inst_14 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_12 : AddCommGroup M] [inst_13 : Module R₀ M] [inst_14 : Module R M]
    [inst_15 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M_1
M : Type u
inst_8 : AddCommGroup M
inst_9 : Module R₀ M
inst_10 : Module R M
inst_11 : IsScalarTower R₀ R M
⊢ Jac ≤ Module.annihilator R M → P M
have rw : Module.IsTorsionBySet R M (↑Jac : Set R) → P M
Tactic: rw [← SetLike.coe_subset_coe, ← Module.isTorsionBySet_iff_subset_annihilator]
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R₀ : Type u_1
R : Type u_2
M_1 : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M_1
inst_4 : Module R₀ M_1
inst_5 : Module R M_1
inst_6 : IsScalarTower R₀ R M_1
inst_7 : IsSemiprimaryRing R
P : (M : Type u) → [inst_12 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_12 : AddCommGroup M] [inst_13 : Module R₀ M] [inst_14 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_12 : AddCommGroup M] [inst_13 : Module R₀ M] [inst_14 : Module R M]
    [inst_15 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M_1
M : Type u
inst_8 : AddCommGroup M
inst_9 : Module R₀ M
inst_10 : Module R M
inst_11 : IsScalarTower R₀ R M
h : Module.IsTorsionBySet R M (↑Jac : Set R)
x : Module.{u_2, u} (R ⧸ Jac) M := h.module
⊢ P M
have this : IsSemisimpleModule R M
Tactic: have := (h.semilinearMap.isSemisimpleModule_iff_of_bijective Function.bijective_id).2
      inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M
inst_4 : Module R₀ M
inst_5 : Module R M
inst_6 : IsScalarTower R₀ R M
inst_7 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M
⊢ P M
have this : ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
  Jac ≤ Module.annihilator R M → P M
Tactic: have {M} [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] :
      Jac ≤ Module.annihilator R M → P M := by
    rw [← SetLike.coe_subset_coe, ← Module.isTorsionBySet_iff_subset_annihilator]
    intro h
    let _ := h.module
    have := (h.semilinearMap.isSemisimpleModule_iff_of_bijective Function.bijective_id).2
      inferInstance
    exact h0 _ h
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R₀ : Type u_1
R : Type u_2
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst_4 : AddCommGroup M
inst_5 : Module R₀ M
inst_6 : Module R M
inst_7 : IsScalarTower R₀ R M
hn : HPow.hPow (β := ℕ) Jac 0 ≤ Module.annihilator R M
⊢ P M
have hn₁ : LE.le (α := Ideal R) ⊤ (Module.annihilator R M)
Tactic: rw [Jac.pow_zero, Ideal.one_eq_top] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M
inst_4 : Module R₀ M
inst_5 : Module R M
inst_6 : IsScalarTower R₀ R M
inst_7 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
⊢ P M
have succ : ∀ (n : ℕ)
  (ih :
    ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
      (hn : Jac ^ n ≤ Module.annihilator R M), P M)
  (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
  (hn : Jac ^ (n + 1) ≤ Module.annihilator R M), P M
Tactic: induction n generalizing M with
  | zero => rw [Jac.pow_zero, Ideal.one_eq_top] at hn; exact this (le_top.trans hn)
  | succ n ih => ?_
Cleared hypotheses: M, inst_3, inst_4, inst_5, inst_6, n, hn
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
n : ℕ
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : Jac ^ n ≤ Module.annihilator R M), P M
M : Type u
inst_4 : AddCommGroup M
inst_5 : Module R₀ M
inst_6 : Module R M
inst_7 : IsScalarTower R₀ R M
hn : Jac ^ (n + 1) ≤ Module.annihilator R M
⊢ P M
have succ : ∀
  (ih :
    ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
      (hn : HPow.hPow (β := ℕ) Jac 0 ≤ Module.annihilator R M), P M)
  (hn : Jac ^ HAdd.hAdd (α := ℕ) 0 1 ≤ Module.annihilator R M), P M
Tactic: obtain _ | n := n
Cleared hypotheses: n, ih, hn
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
n : ℕ
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : Jac ^ n ≤ Module.annihilator R M), P M
M : Type u
inst_4 : AddCommGroup M
inst_5 : Module R₀ M
inst_6 : Module R M
inst_7 : IsScalarTower R₀ R M
hn : Jac ^ (n + 1) ≤ Module.annihilator R M
succ :
  ∀
    (ih :
      ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
        (hn : HPow.hPow (β := ℕ) Jac 0 ≤ Module.annihilator R M), P M)
    (hn : Jac ^ HAdd.hAdd (α := ℕ) 0 1 ≤ Module.annihilator R M), P M
⊢ P M
have succ₁ : ∀ (n : ℕ)
  (ih :
    ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
      (hn : Jac ^ (n + 1) ≤ Module.annihilator R M), P M)
  (hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M), P M
Tactic: obtain _ | n := n
Cleared hypotheses: n, ih, hn
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R₀ : Type u_1
R : Type u_2
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst_4 : AddCommGroup M
inst_5 : Module R₀ M
inst_6 : Module R M
inst_7 : IsScalarTower R₀ R M
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : HPow.hPow (β := ℕ) Jac 0 ≤ Module.annihilator R M), P M
hn : Jac ^ HAdd.hAdd (α := ℕ) 0 1 ≤ Module.annihilator R M
⊢ P M
have hn₁ : Jac ≤ Module.annihilator R M
Tactic: rw [Jac.pow_one] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst_4 : AddCommGroup M
inst_5 : Module R₀ M
inst_6 : Module R M
inst_7 : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : Jac ^ (n + 1) ≤ Module.annihilator R M), P M
hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M
⊢ P M
have succ : Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
Tactic: refine h1 _ (ih _ ?_) (ih _ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst_4 : AddCommGroup M
inst_5 : Module R₀ M
inst_6 : Module R M
inst_7 : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : Jac ^ (n + 1) ≤ Module.annihilator R M), P M
hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M
succ : Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
⊢ P M
have succ₁ : Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R (M ⧸ HSMul.hSMul (β := Submodule R M) Jac ⊤)
Tactic: refine h1 _ (ih _ ?_) (ih _ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R₀ : Type u_1
R : Type u_2
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : IsSemiprimaryRing R
P : (M : Type u) → [inst_8 : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M (↑Jac : Set R) → P M
h1 :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M]
    [inst_11 : IsScalarTower R₀ R M],
    let N := HSMul.hSMul (β := Submodule R M) Jac ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst_4 : AddCommGroup M
inst_5 : Module R₀ M
inst_6 : Module R M
inst_7 : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst_8 : AddCommGroup M] [inst_9 : Module R₀ M] [inst_10 : Module R M] [IsScalarTower R₀ R M]
    (hn : Jac ^ (n + 1) ≤ Module.annihilator R M), P M
hn : Jac ^ (n + 1 + 1) ≤ Module.annihilator R M
⊢ Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
have succ : ∀ (hn : Jac ^ (n + 1 + 1) ≤ Submodule.annihilator.{u_2, u} (M := M) ⊤),
  Jac ^ (n + 1) ≤ Module.annihilator.{u_2, u} R ↥(HSMul.hSMul (β := Submodule R M) Jac ⊤)
Tactic: rwa [← Submodule.annihilator_top, Submodule.le_annihilator_iff, Jac.pow_succ,
      Submodule.mul_smul, ← Submodule.le_annihilator_iff] at hn
Cleared hypotheses: hn