awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HopfAlgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ IsGroupLikeElem R (A := A) ((antipode R : (a : A) → A) a : A)

Tactic:
ha.of_mul_eq_one ha.mul_antipode_cancel ha.antipode_mul_cancel

Premises used: IsGroupLikeElem.antipode_mul_cancel, IsGroupLikeElem.of_mul_eq_one, IsGroupLikeElem.mul_antipode_cancel
-- Module: Mathlib.RingTheory.HopfAlgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ (antipode R : (a : A) → A) ((antipode R : (a : A) → A) a : A) = a

Tactic:
left_inv_eq_right_inv ha.antipode.antipode_mul_cancel ha.antipode_mul_cancel

Premises used: left_inv_eq_right_inv, IsGroupLikeElem.antipode, IsGroupLikeElem.antipode_mul_cancel
-- Module: Mathlib.RingTheory.HopfAlgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : GroupLike R A
⊢ (↑a⁻¹ : A) = (antipode R : (a : A) → A) (↑a : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HopfAlgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a_1 b : A
a : GroupLike R A
val : (↑(a⁻¹ * a) : A) = (↑1 : A)
⊢ a⁻¹ * a = 1

Tactic:
ext
-- Module: Mathlib.RingTheory.HopfAlgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a_1 b : A
a : GroupLike R A
⊢ (↑(a⁻¹ * a) : A) = (↑1 : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
G : Type u_3
inst_3 : Group G
g : G
a : A
⊢ Eq (α := A[G]) ((antipode R : (a : A[G]) → A[G]) (single g a) : A[G])
    (single g⁻¹ ((antipode R : (a : A) → A) a) : A[G])

Tactic:
simp [MonoidAlgebra, antipode]

Premises used: MonoidAlgebra, HopfAlgebraStruct.antipode
-- Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
G : Type u_3
inst_3 : Group G
H :
  ∀ (a : G) (b : A),
    Eq (α := A[G])
      (((LinearMap.mul' R A[G] ∘ₗ LinearMap.rTensor A[G] (antipode R) ∘ₗ comul) ∘ₗ lsingle a : (a : A) → A[G]) b : A[G])
      (((Algebra.linearMap R A[G] ∘ₗ counit) ∘ₗ lsingle a : (a : A) → A[G]) b : A[G])
⊢ Eq (α := A[G] →ₗ[R] A[G]) (LinearMap.mul' R A[G] ∘ₗ LinearMap.rTensor A[G] (antipode R) ∘ₗ comul)
    (Algebra.linearMap R A[G] ∘ₗ counit)

Tactic:
ext a b : 2
-- Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
G : Type u_3
inst_3 : Group G
a : G
b : A
⊢ Eq (α := A[G])
    (((LinearMap.mul' R A[G] ∘ₗ LinearMap.rTensor A[G] (antipode R) ∘ₗ comul) ∘ₗ lsingle a : (a : A) → A[G]) b : A[G])
    (((Algebra.linearMap R A[G] ∘ₗ counit) ∘ₗ lsingle a : (a : A) → A[G]) b : A[G])

Tactic:
simpa [← (ℛ R b).eq] using congr(lsingle (R := R) (1 : G)
      $(sum_antipode_mul_eq_algebraMap_counit (ℛ R b)))

Premises used: Coalgebra.Repr.eq, Coalgebra.Repr.arbitrary
-- Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
G : Type u_3
inst_3 : Group G
H :
  ∀ (a : G) (b : A),
    Eq (α := A[G])
      (((LinearMap.mul' R A[G] ∘ₗ LinearMap.lTensor A[G] (antipode R) ∘ₗ comul) ∘ₗ lsingle a : (a : A) → A[G]) b : A[G])
      (((Algebra.linearMap R A[G] ∘ₗ counit) ∘ₗ lsingle a : (a : A) → A[G]) b : A[G])
⊢ Eq (α := A[G] →ₗ[R] A[G]) (LinearMap.mul' R A[G] ∘ₗ LinearMap.lTensor A[G] (antipode R) ∘ₗ comul)
    (Algebra.linearMap R A[G] ∘ₗ counit)

Tactic:
ext a b : 2
-- Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
G : Type u_3
inst_3 : Group G
a : G
b : A
⊢ Eq (α := A[G])
    (((LinearMap.mul' R A[G] ∘ₗ LinearMap.lTensor A[G] (antipode R) ∘ₗ comul) ∘ₗ lsingle a : (a : A) → A[G]) b : A[G])
    (((Algebra.linearMap R A[G] ∘ₗ counit) ∘ₗ lsingle a : (a : A) → A[G]) b : A[G])

Tactic:
simpa [← (ℛ R b).eq] using congr(lsingle (R := R) (1 : G)
      $(sum_mul_antipode_eq_algebraMap_counit (ℛ R b)))

Premises used: Coalgebra.Repr.eq, Coalgebra.Repr.arbitrary
-- Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
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⁻¹])
⊢ 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⁻¹])

Tactic:
rw [← single_eq_C, AddMonoidAlgebra.antipode_single]

Premises used: LaurentPolynomial.single_eq_C, AddMonoidAlgebra.antipode_single
-- Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
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⁻¹]) (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:
simp
-- Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
n : ℤ
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 ℤ)
⊢ 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 ℤ)

Tactic:
rw [AddMonoidAlgebra.antipode_single]

Premises used: AddMonoidAlgebra.antipode_single
-- Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
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⁻¹]) (AddMonoidAlgebra.single (-n) ((antipode R : (a : A) → A) 1) : AddMonoidAlgebra A ℤ)
    (AddMonoidAlgebra.single (-n) 1 : AddMonoidAlgebra A ℤ)

Tactic:
simp only [HopfAlgebra.antipode_one, single_eq_C_mul_T, map_one, one_mul]

Premises used: LaurentPolynomial.single_eq_C_mul_T, map_one, one_mul, HopfAlgebra.antipode_one
-- Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
n : ℤ
⊢ (antipode R : (a : A[T;T⁻¹]) → A[T;T⁻¹])
      (HMul.hMul (α := A[T;T⁻¹]) (β := A[T;T⁻¹]) ((C : (a : A) → A[T;T⁻¹]) a : A[T;T⁻¹]) (T n)) =
    HMul.hMul (α := A[T;T⁻¹]) (β := A[T;T⁻¹]) ((C : (a : A) → A[T;T⁻¹]) ((antipode R : (a : A) → A) a) : A[T;T⁻¹])
      (T (-n))

Tactic:
simp [← single_eq_C_mul_T]

Premises used: LaurentPolynomial.single_eq_C_mul_T
-- Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct
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)
⊢ 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

Premises used: Algebra.TensorProduct.lmul'_comp_map
-- Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct
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)
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)
⊢ 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)

Tactic:
rw [← Algebra.TensorProduct.lmul'_comp_map] at mul_antipode_rTensor_comul

Premises used: Algebra.TensorProduct.lmul'_comp_map
-- Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct
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
      (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)
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)

Tactic:
congr(($mul_antipode_rTensor_comul).toLinearMap)

Premises used: AlgHom.toLinearMap, congrArg, id
-- Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct
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
      (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)
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)

Tactic:
exact congr(($mul_antipode_rTensor_comul).toLinearMap)
-- Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct
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)
⊢ 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

Premises used: Algebra.TensorProduct.lmul'_comp_map
-- Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct
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
      (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)
⊢ 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)

Tactic:
congr(($mul_antipode_lTensor_comul).toLinearMap)

Premises used: AlgHom.toLinearMap, congrArg, id
-- Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct
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
      (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)
⊢ 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)

Tactic:
exact congr(($mul_antipode_lTensor_comul).toLinearMap)
-- Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : HopfAlgebra R A
inst_6 : HopfAlgebra S B
inst_7 : Algebra R B
inst_8 : IsScalarTower R S B
⊢ Eq (α := B ⊗[R] A →ₗ[S] B ⊗[R] A) (antipode S) (AlgebraTensorModule.map (antipode S) (antipode R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
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
⊢ P M

Tactic:
have ⟨ss, n, hn⟩ := (isSemiprimaryRing_iff R).mp ‹_›
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
⊢ let Jac : Ideal R := Ring.jacobson R;
  ∀ (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

Tactic:
set Jac := Ring.jacobson R

Premises used: Ring.jacobson
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
h0₁ :
  let Jac : Ideal R := Ring.jacobson R;
  ∀ (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
⊢ let Jac : Ideal R := Ring.jacobson R;
  ∀ (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

Tactic:
set Jac := Ring.jacobson R

Premises used: Ring.jacobson
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
ss : IsSemisimpleRing.{u_2} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
h0₁ :
  let Jac : Ideal R := Ring.jacobson R;
  ∀ (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₁ :
  let Jac : Ideal R := Ring.jacobson R;
  ∀ (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
⊢ let Jac : Ideal R := Ring.jacobson R;
  Jac ^ n = 0

Tactic:
set Jac := Ring.jacobson R

Premises used: Ring.jacobson
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
⊢ Jac ^ n ≤ Module.annihilator R M

Tactic:
replace hn : Jac ^ n ≤ Module.annihilator R M := hn ▸ bot_le
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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
rw : Module.IsTorsionBySet R M (↑Jac : Set R) → P M
⊢ Jac ≤ Module.annihilator R M → P M

Tactic:
rw [← SetLike.coe_subset_coe, ← Module.isTorsionBySet_iff_subset_annihilator]

Premises used: SetLike.coe_subset_coe, Module.isTorsionBySet_iff_subset_annihilator
-- Module: Mathlib.RingTheory.HopkinsLevitzki
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)
let : P M
⊢ P M

Tactic:
let _ := h.module