awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
x y : M →ₛₗ[σ₁₂] M₂
h :
  ∀ (x_1 : M),
    Eq.{u_10 + 1} (α := M₂) (((x + y).toAddMonoidHom : (a : M) → M₂) x_1 : M₂)
      ((x.toAddMonoidHom + y.toAddMonoidHom : (a : M) → M₂) x_1 : M₂)
⊢ (x + y).toAddMonoidHom = x.toAddMonoidHom + y.toAddMonoidHom

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
x y : M →ₛₗ[σ₁₂] M₂
x_1 : M
⊢ Eq.{u_10 + 1} (α := M₂) (((x + y).toAddMonoidHom : (a : M) → M₂) x_1 : M₂)
    ((x.toAddMonoidHom + y.toAddMonoidHom : (a : M) → M₂) x_1 : M₂)

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
M : Type u_8
inst : Semiring R₁
inst_1 : AddCommMonoid M
inst_2 : Module R₁ M
inst_3 : Subsingleton M
⊢ Eq.{u_8 + 1} (α := M →ₗ[R₁] M) id 0

Tactic:
Subsingleton.eq_zero id

Premises used: LinearMap.id, Subsingleton.eq_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
R₂ : Type u_3
R₃ : Type u_4
S₃ : Type u_6
M : Type u_8
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : Monoid S₃
inst_11 : DistribMulAction S₃ M₃
inst_12 : SMulCommClass R₃ S₃ M₃
a : S₃
g : M₂ →ₛₗ[σ₂₃] M₃
f : M →ₛₗ[σ₁₂] M₂
⊢ (a • g) ∘ₛₗ f = a • g ∘ₛₗ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Monoid S
inst_6 : DistribMulAction S M₂
inst_7 : Module R M₂
inst_8 : Module R M₃
inst_9 : SMulCommClass R S M₂
inst_10 : DistribMulAction S M₃
inst_11 : SMulCommClass R S M₃
inst_12 : CompatibleSMul M₃ M₂ S R
g : M₃ →ₗ[R] M₂
a : S
f : M →ₗ[R] M₃
⊢ g ∘ₗ (a • f) = a • g ∘ₗ f

Tactic:
ext fun _ ↦ g.map_smul_of_tower _ _

Premises used: LinearMap.ext, LinearMap.map_smul_of_tower, DFunLike.coe
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
S : Type u_15
M : Type u_16
N : Type u_17
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module S M
inst_7 : Module S N
inst_8 : CompatibleSMul M N R S
⊢ Eq (α := M →ₗ[R] N)
    ((↑R :
        {S : Type u_15} →
          {M : Type u_16} →
            {M₂ : Type u_17} →
              [inst : Semiring R] →
                [inst_9 : Semiring S] →
                  [inst_10 : AddCommMonoid M] →
                    [inst_11 : AddCommMonoid M₂] →
                      [inst_12 : Module R M] →
                        [inst_13 : Module R M₂] →
                          [inst_14 : Module S M] →
                            [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := S) 0)
    0

Tactic:
rfl

Premises used: LinearMap.restrictScalars, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
S : Type u_15
M : Type u_16
N : Type u_17
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module S M
inst_7 : Module S N
inst_8 : CompatibleSMul M N R S
f g : M →ₗ[S] N
⊢ (↑R :
        {S : Type u_15} →
          {M : Type u_16} →
            {M₂ : Type u_17} →
              [inst : Semiring R] →
                [inst_9 : Semiring S] →
                  [inst_10 : AddCommMonoid M] →
                    [inst_11 : AddCommMonoid M₂] →
                      [inst_12 : Module R M] →
                        [inst_13 : Module R M₂] →
                          [inst_14 : Module S M] →
                            [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (f + g) =
    HAdd.hAdd (α := M →ₗ[R] N)
      ((↑R :
          {S : Type u_15} →
            {M : Type u_16} →
              {M₂ : Type u_17} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f)
      ((↑R :
          {S : Type u_15} →
            {M : Type u_16} →
              {M₂ : Type u_17} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        g)

Tactic:
rfl

Premises used: LinearMap.restrictScalars, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
S : Type u_15
inst : Semiring R
inst_1 : Semiring S
M : Type u_19
N : Type u_20
inst_2 : AddCommMonoid M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module S M
inst_7 : Module S N
inst_8 : CompatibleSMul M N R S
f : M →ₗ[S] N
⊢ Eq (α := M →ₗ[R] N)
    ((↑R :
        {S : Type u_15} →
          {M : Type u_19} →
            {M₂ : Type u_20} →
              [inst : Semiring R] →
                [inst_9 : Semiring S] →
                  [inst_10 : AddCommMonoid M] →
                    [inst_11 : AddCommMonoid M₂] →
                      [inst_12 : Module R M] →
                        [inst_13 : Module R M₂] →
                          [inst_14 : Module S M] →
                            [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (-f))
    (-(↑R :
          {S : Type u_15} →
            {M : Type u_19} →
              {M₂ : Type u_20} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f)

Tactic:
rfl

Premises used: LinearMap.restrictScalars, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
S : Type u_15
M : Type u_16
N : Type u_17
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module S M
inst_7 : Module S N
inst_8 : CompatibleSMul M N R S
R₁ : Type u_19
inst_9 : Semiring R₁
inst_10 : Module R₁ N
inst_11 : SMulCommClass S R₁ N
inst_12 : SMulCommClass R R₁ N
c : R₁
f : M →ₗ[S] N
⊢ (↑R :
        {S : Type u_15} →
          {M : Type u_16} →
            {M₂ : Type u_17} →
              [inst : Semiring R] →
                [inst_13 : Semiring S] →
                  [inst_14 : AddCommMonoid M] →
                    [inst_15 : AddCommMonoid M₂] →
                      [inst_16 : Module R M] →
                        [inst_17 : Module R M₂] →
                          [inst_18 : Module S M] →
                            [inst_19 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (c • f) =
    HSMul.hSMul (β := M →ₗ[R] N) c
      ((↑R :
          {S : Type u_15} →
            {M : Type u_16} →
              {M₂ : Type u_17} →
                [inst : Semiring R] →
                  [inst_13 : Semiring S] →
                    [inst_14 : AddCommMonoid M] →
                      [inst_15 : AddCommMonoid M₂] →
                        [inst_16 : Module R M] →
                          [inst_17 : Module R M₂] →
                            [inst_18 : Module S M] →
                              [inst_19 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f)

Tactic:
rfl

Premises used: LinearMap.restrictScalars, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
S : Type u_15
M : Type u_16
N : Type u_17
P : Type u_18
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module S M
inst_7 : Module S N
inst_8 : CompatibleSMul M N R S
inst_9 : AddCommMonoid P
inst_10 : Module S P
inst_11 : Module R P
inst_12 : CompatibleSMul N P R S
inst_13 : CompatibleSMul M P R S
f : N →ₗ[S] P
g : M →ₗ[S] N
⊢ Eq (α := M →ₗ[R] P)
    ((↑R :
        {S : Type u_15} →
          {M : Type u_16} →
            {M₂ : Type u_18} →
              [inst : Semiring R] →
                [inst_14 : Semiring S] →
                  [inst_15 : AddCommMonoid M] →
                    [inst_16 : AddCommMonoid M₂] →
                      [inst_17 : Module R M] →
                        [inst_18 : Module R M₂] →
                          [inst_19 : Module S M] →
                            [inst_20 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (f ∘ₗ g))
    ((↑R :
          {S : Type u_15} →
            {M : Type u_17} →
              {M₂ : Type u_18} →
                [inst : Semiring R] →
                  [inst_14 : Semiring S] →
                    [inst_15 : AddCommMonoid M] →
                      [inst_16 : AddCommMonoid M₂] →
                        [inst_17 : Module R M] →
                          [inst_18 : Module R M₂] →
                            [inst_19 : Module S M] →
                              [inst_20 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f ∘ₗ
      (↑R :
          {S : Type u_15} →
            {M : Type u_16} →
              {M₂ : Type u_17} →
                [inst : Semiring R] →
                  [inst_14 : Semiring S] →
                    [inst_15 : AddCommMonoid M] →
                      [inst_16 : AddCommMonoid M₂] →
                        [inst_17 : Module R M] →
                          [inst_18 : Module R M₂] →
                            [inst_19 : Module S M] →
                              [inst_20 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
S : Type u_15
M : Type u_16
N : Type u_17
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module S M
inst_7 : Module S N
inst_8 : CompatibleSMul M N R S
T : Type u_20
inst_9 : Semiring T
inst_10 : Module T M
inst_11 : Module T N
inst_12 : CompatibleSMul M N S T
inst_13 : CompatibleSMul M N R T
f : M →ₗ[T] N
⊢ Eq (α := M →ₗ[R] N)
    ((↑R :
        {S : Type u_15} →
          {M : Type u_16} →
            {M₂ : Type u_17} →
              [inst : Semiring R] →
                [inst_14 : Semiring S] →
                  [inst_15 : AddCommMonoid M] →
                    [inst_16 : AddCommMonoid M₂] →
                      [inst_17 : Module R M] →
                        [inst_18 : Module R M₂] →
                          [inst_19 : Module S M] →
                            [inst_20 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      ((↑S :
          {S_1 : Type u_20} →
            {M : Type u_16} →
              {M₂ : Type u_17} →
                [inst : Semiring S] →
                  [inst_14 : Semiring S_1] →
                    [inst_15 : AddCommMonoid M] →
                      [inst_16 : AddCommMonoid M₂] →
                        [inst_17 : Module S M] →
                          [inst_18 : Module S M₂] →
                            [inst_19 : Module S_1 M] →
                              [inst_20 : Module S_1 M₂] →
                                [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        f))
    ((↑R :
        {S : Type u_20} →
          {M : Type u_16} →
            {M₂ : Type u_17} →
              [inst : Semiring R] →
                [inst_14 : Semiring S] →
                  [inst_15 : AddCommMonoid M] →
                    [inst_16 : AddCommMonoid M₂] →
                      [inst_17 : Module R M] →
                        [inst_18 : Module R M₂] →
                          [inst_19 : Module S M] →
                            [inst_20 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f)

Tactic:
rfl

Premises used: LinearMap.restrictScalars, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
A : Type u_15
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a b : A
⊢ (mulLeft R a : (a : A) → A) b = a * b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
A : Type u_15
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
⊢ Eq (α := A →+ A) (↑(mulLeft R a) : A →+ A) (AddMonoidHom.mulLeft a)

Tactic:
rfl

Premises used: AddMonoidHom.mulLeft, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
A : Type u_15
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
⊢ Eq.{u_15 + 1} (α := A →ₗ[R] A) (mulLeft R 0) 0

Tactic:
ext zero_mul

Premises used: LinearMap.ext, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
A : Type u_15
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a b : A
⊢ (mulRight R a : (a : A) → A) b = b * a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
A : Type u_15
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
⊢ Eq (α := A →+ A) (↑(mulRight R a) : A →+ A) (AddMonoidHom.mulRight a)

Tactic:
rfl

Premises used: AddMonoidHom.mulRight, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
A : Type u_15
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
⊢ Eq.{u_15 + 1} (α := A →ₗ[R] A) (mulRight R 0) 0

Tactic:
ext mul_zero

Premises used: LinearMap.ext, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
A : Type u_15
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
a b x : A
⊢ (mulLeftRight R (a, b) : (a : A) → A) x = a * x * b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_4 + 1} (α := End R M) 1 LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : End R M
⊢ f * g = f ∘ₗ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ (1 : (a : M) → M) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : End R M
x : M
⊢ Eq (α := M) ((f * g : (a : M) → M) x : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_4 + 1} (α := (a : M) → M) (⇑1 : (a : M) → M) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : End R M
⊢ Eq (α := (a : M) → M) (⇑(f * g) : (a : M) → M) (Function.comp (β := M) (⇑f : (a : M) → M) (⇑g : (a : M) → M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommGroup N₁
inst_3 : Module R M
inst_4 : Module R N₁
inst_5 : Nontrivial M
obtain : ∀ (m : M) (ne : m ≠ 0), Nontrivial.{u_4} (End R M)
⊢ Nontrivial.{u_4} (End R M)

Tactic:
obtain ⟨m, ne⟩ := exists_ne (0 : M)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommGroup N₁
inst_3 : Module R M
inst_4 : Module R N₁
inst_5 : Nontrivial M
m : M
ne : m ≠ 0
⊢ Nontrivial.{u_4} (End R M)

Tactic:
nontrivial_of_ne 1 0 fun p => ne (LinearMap.congr_fun p m)

Premises used: nontrivial_of_ne, LinearMap.congr_fun, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommGroup N₁
inst_3 : Module R M
inst_4 : Module R N₁
inst_5 : Nontrivial M
m : M
ne : m ≠ 0
⊢ Nontrivial.{u_4} (End R M)

Tactic:
exact nontrivial_of_ne 1 0 fun p => ne (LinearMap.congr_fun p m)

Premises used: nontrivial_of_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
m : M
⊢ ((↑n : End R M) : (a : M) → M) m = n • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
inst_3 : n.AtLeastTwo
m : M
⊢ (OfNat.ofNat n : (a : M) → M) m = HSMul.hSMul (α := ℕ) (OfNat.ofNat n) m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommGroup N₁
inst_2 : Module R N₁
z : ℤ
m : N₁
⊢ ((↑z : End R N₁) : (a : N₁) → N₁) m = z • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommGroup N₁
inst_3 : Module R M
inst_4 : Module R N₁
inst_5 : Monoid S
inst_6 : DistribMulAction S M
inst_7 : SMulCommClass R S M
⊢ IsScalarTower.{u_3, u_4, u_4} S (End R M) (End R M)

Tactic:
⟨smul_comp⟩

Premises used: LinearMap.smul_comp, IsScalarTower.mk
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommGroup N₁
inst_3 : Module R M
inst_4 : Module R N₁
inst_5 : Monoid S
inst_6 : DistribMulAction S M
inst_7 : SMulCommClass R S M
inst_8 : SMul S R
inst_9 : IsScalarTower S R M
⊢ SMulCommClass.{u_3, u_4, u_4} S (End R M) (End R M)

Tactic:
⟨fun s _ _ ↦ (comp_smul _ s _).symm⟩

Premises used: LinearMap.comp_smul, SMulCommClass.mk, Eq.symm
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommGroup N₁
inst_3 : Module R M
inst_4 : Module R N₁
inst_5 : Monoid S
inst_6 : DistribMulAction S M
inst_7 : SMulCommClass R S M
inst_8 : SMul S R
inst_9 : IsScalarTower S R M
⊢ SMulCommClass.{u_4, u_3, u_4} (End R M) S (End R M)

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
h : IsUnit f
x : M
⊢ (f * h.unit.inv : (a : M) → M) x = x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
h : IsUnit f
x : M
⊢ (h.unit.inv * f : (a : M) → M) x = x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
n : ℕ
⊢ Eq (α := (a : M) → M) (⇑(f ^ n) : (a : M) → M) (⇑f : (a : M) → M)^[n]

Tactic:
hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _

Premises used: hom_coe_pow
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
n : ℕ
m : M
⊢ (f ^ n : (a : M) → M) m = (⇑f : (a : M) → M)^[n] m

Tactic:
congr_fun (coe_pow f n) m

Premises used: Module.End.coe_pow, congr_fun
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
m : M
k l : ℕ
hk : k ≤ l
hm : Eq (α := M) ((f ^ k : (a : M) → M) m : M) (0 : M)
rw : Eq (α := M) ((f ^ (l - k + k) : (a : M) → M) m : M) (0 : M)
rw₁ : Eq (α := M) ((f ^ (l - k) * f ^ k : (a : M) → M) m : M) (0 : M)
rw₂ : Eq (α := M) ((f ^ (l - k) : (a : M) → M) ((f ^ k : (a : M) → M) m : M) : M) (0 : M)
rw₃ : Eq (α := M) ((f ^ (l - k) : (a : M) → M) 0 : M) (0 : M)
rw₄ rw₅ : Eq.{u_4 + 1} (α := M) 0 0
⊢ Eq (α := M) ((f ^ l : (a : M) → M) m : M) (0 : M)

Tactic:
rw [← Nat.sub_add_cancel hk, pow_add, mul_apply, hm, map_zero]

Premises used: pow_add, map_zero, Nat.sub_add_cancel, Module.End.mul_apply
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
⊢ HPow.hPow (β := ℕ) g₂ 0 ∘ₛₗ f = f ∘ₛₗ HPow.hPow (β := ℕ) g 0

Tactic:
simp [one_eq_id]

Premises used: Module.End.one_eq_id