awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A_1 : Type u_6
M_1 : Type u_7
N_1 : Type u_8
P : Type u_9
Q : Type u_10
S_1 : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M_1
inst_6 : AddCommMonoid N_1
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S_1
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M_1
inst_21 : Module R'' M_1
inst_22 : Module R M_1
inst_23 : Module R N_1
inst_24 : Module R S_1
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : Module R P
inst_36 : Module R Q
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst_37 : AddCommMonoid M
inst_38 : AddCommMonoid N
inst_39 : Module R M
inst_40 : Module R N
inst_41 : CommSemiring A
inst_42 : Module A M
inst_43 : Module A N
inst_44 : SMulCommClass R A M
inst_45 : CommSemiring S
inst_46 : Module S M
inst_47 : SMulCommClass R S M
inst_48 : SMulCommClass A S M
inst_49 : CompatibleSMul R A M N
s : S
⊢ AddHom.toFun
      (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
        (lift
          {
            toFun := fun (m : M) ↦
              let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
              { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }))
      (HSMul.hSMul (β := M ⊗[A] N) s 0) =
    HSMul.hSMul (α := S) (β := M ⊗[R] N) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (M := M ⊗[A] N)
        (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
          (lift
            {
              toFun := fun (m : M) ↦
                let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
                { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N },
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] N →ₗ[A] M ⊗[R] N }))
        0)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A_1 : Type u_6
M_1 : Type u_7
N_1 : Type u_8
P : Type u_9
Q : Type u_10
S_1 : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M_1
inst_6 : AddCommMonoid N_1
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S_1
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M_1
inst_21 : Module R'' M_1
inst_22 : Module R M_1
inst_23 : Module R N_1
inst_24 : Module R S_1
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : Module R P
inst_36 : Module R Q
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst_37 : AddCommMonoid M
inst_38 : AddCommMonoid N
inst_39 : Module R M
inst_40 : Module R N
inst_41 : CommSemiring A
inst_42 : Module A M
inst_43 : Module A N
inst_44 : SMulCommClass R A M
inst_45 : CommSemiring S
inst_46 : Module S M
inst_47 : SMulCommClass R S M
inst_48 : SMulCommClass A S M
inst_49 : CompatibleSMul R A M N
s : S
x : M
y : N
⊢ AddHom.toFun
      (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
        (lift
          {
            toFun := fun (m : M) ↦
              let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
              { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }))
      (HSMul.hSMul (β := M ⊗[A] N) s (x ⊗ₜ[A] y)) =
    HSMul.hSMul (α := S) (β := M ⊗[R] N) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (M := M ⊗[A] N)
        (LinearMap.toAddHom (S := A) (σ := RingHom.id A)
          (lift
            {
              toFun := fun (m : M) ↦
                let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m;
                { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N },
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] N →ₗ[A] M ⊗[R] N }))
        (x ⊗ₜ[A] y))

Tactic:
simp [smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : CommSemiring A
inst_6 : Module A M
inst_7 : Module A N
inst_8 : SMulCommClass R A M
inst_9 : CommSemiring S
inst_10 : Module S M
inst_11 : SMulCommClass R S M
inst_12 : SMulCommClass A S M
inst_13 : CompatibleSMul R A M N
m : M
n : N
⊢ Eq (α := M ⊗[R] N) ((mapOfCompatibleSMul R A S M N : (a : M ⊗[A] N) → M ⊗[R] N) (m ⊗ₜ[A] n) : M ⊗[R] N)
    (m ⊗ₜ[R] n : M ⊗[R] N)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : CommSemiring A
inst_6 : Module A M
inst_7 : Module A N
inst_8 : SMulCommClass R A M
inst_9 : CommSemiring S
inst_10 : Module S M
inst_11 : SMulCommClass R S M
inst_12 : SMulCommClass A S M
inst_13 : CompatibleSMul R A M N
x_1 x_2 x_3 : M ⊗[R] N
h : ∃ (a : M ⊗[A] N), (mapOfCompatibleSMul R A S M N : (a : M ⊗[A] N) → M ⊗[R] N) a = x_2
h_1 : ∃ (a : M ⊗[A] N), (mapOfCompatibleSMul R A S M N : (a : M ⊗[A] N) → M ⊗[R] N) a = x_3
x : M ⊗[A] N
hx : (mapOfCompatibleSMul R A S M N : (a : M ⊗[A] N) → M ⊗[R] N) x = x_2
y : M ⊗[A] N
hy : (mapOfCompatibleSMul R A S M N : (a : M ⊗[A] N) → M ⊗[R] N) y = x_3
⊢ (mapOfCompatibleSMul R A S M N : (a : M ⊗[A] N) → M ⊗[R] N) (x + y) = x_2 + x_3

Tactic:
simpa using congr($hx + $hy)
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A_1 : Type u_6
M_1 : Type u_7
N_1 : Type u_8
P : Type u_9
Q : Type u_10
S_1 : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M_1
inst_6 : AddCommMonoid N_1
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S_1
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M_1
inst_21 : Module R'' M_1
inst_22 : Module R M_1
inst_23 : Module R N_1
inst_24 : Module R S_1
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : Module R P
inst_36 : Module R Q
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst_37 : AddCommMonoid M
inst_38 : AddCommMonoid N
inst_39 : Module R M
inst_40 : Module R N
inst_41 : CommSemiring A
inst_42 : Module A M
inst_43 : Module A N
inst_44 : SMulCommClass R A M
inst_45 : CommSemiring S
inst_46 : Module S M
inst_47 : SMulCommClass R S M
inst_48 : SMulCommClass A S M
inst_49 : CompatibleSMul R A M N
inst_50 : CompatibleSMul A R M N
x x_1 x_2 : M ⊗[A] N
h :
  (mapOfCompatibleSMul A R S M N : (a : M ⊗[R] N) → M ⊗[A] N)
      (AddHom.toFun (LinearMap.toAddHom (mapOfCompatibleSMul R A S M N)) x_1) =
    x_1
h' :
  (mapOfCompatibleSMul A R S M N : (a : M ⊗[R] N) → M ⊗[A] N)
      (AddHom.toFun (LinearMap.toAddHom (mapOfCompatibleSMul R A S M N)) x_2) =
    x_2
⊢ (mapOfCompatibleSMul A R S M N : (a : M ⊗[R] N) → M ⊗[A] N)
      (AddHom.toFun (LinearMap.toAddHom (mapOfCompatibleSMul R A S M N)) (x_1 + x_2)) =
    x_1 + x_2

Tactic:
simpa using congr($h + $h')
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A_1 : Type u_6
M_1 : Type u_7
N_1 : Type u_8
P : Type u_9
Q : Type u_10
S_1 : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M_1
inst_6 : AddCommMonoid N_1
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S_1
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M_1
inst_21 : Module R'' M_1
inst_22 : Module R M_1
inst_23 : Module R N_1
inst_24 : Module R S_1
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : Module R P
inst_36 : Module R Q
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst_37 : AddCommMonoid M
inst_38 : AddCommMonoid N
inst_39 : Module R M
inst_40 : Module R N
inst_41 : CommSemiring A
inst_42 : Module A M
inst_43 : Module A N
inst_44 : SMulCommClass R A M
inst_45 : CommSemiring S
inst_46 : Module S M
inst_47 : SMulCommClass R S M
inst_48 : SMulCommClass A S M
inst_49 : CompatibleSMul R A M N
inst_50 : CompatibleSMul A R M N
x x_1 x_2 : M ⊗[R] N
h :
  AddHom.toFun (M := M ⊗[A] N) (LinearMap.toAddHom (mapOfCompatibleSMul R A S M N))
      ((mapOfCompatibleSMul A R S M N : (a : M ⊗[R] N) → M ⊗[A] N) x_1) =
    x_1
h' :
  AddHom.toFun (M := M ⊗[A] N) (LinearMap.toAddHom (mapOfCompatibleSMul R A S M N))
      ((mapOfCompatibleSMul A R S M N : (a : M ⊗[R] N) → M ⊗[A] N) x_2) =
    x_2
⊢ AddHom.toFun (M := M ⊗[A] N) (LinearMap.toAddHom (mapOfCompatibleSMul R A S M N))
      ((mapOfCompatibleSMul A R S M N : (a : M ⊗[R] N) → M ⊗[A] N) (x_1 + x_2)) =
    x_1 + x_2

Tactic:
simpa using congr($h + $h')
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : M ⊗[R] N
⊢ Eq (α := M ⊗[R] N) (-0) 0

Tactic:
apply (Neg.aux R).map_zero

Premises used: LinearMap.map_zero, TensorProduct.Neg.aux
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 : M ⊗[R] N
x : M
y : N
⊢ HAdd.hAdd (α := M ⊗[R] N) ((-x) ⊗ₜ[R] y) (x ⊗ₜ[R] y) = (-x + x) ⊗ₜ[R] y

Tactic:
(add_tmul (R := R) (-x) x y).symm

Premises used: TensorProduct.add_tmul, Eq.symm, Neg.neg
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 : M ⊗[R] N
x : M
y : N
h : Eq (α := M ⊗[R] N) 0 ((-x + x) ⊗ₜ[R] y)
⊢ HAdd.hAdd (α := M ⊗[R] N) (-x ⊗ₜ[R] y) (x ⊗ₜ[R] y) = 0

Tactic:
convert! (add_tmul (R := R) (-x) x y).symm

Premises used: TensorProduct.add_tmul, Eq.symm, Neg.neg
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 : M ⊗[R] N
x : M
y : N
h : Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] y)
h₁ h₂ : Eq (α := M ⊗[R] N) 0 0
⊢ Eq (α := M ⊗[R] N) 0 ((-x + x) ⊗ₜ[R] y)

Tactic:
rw [neg_add_cancel, zero_tmul]

Premises used: TensorProduct.zero_tmul, neg_add_cancel
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
rw : -(x + y) + (x + y) = -x + x + (-y + y)
⊢ -(x + y) + (x + y) = 0

Tactic:
rw [← this]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
rw :
  HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) x : M ⊗[R] N)
        ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) y : M ⊗[R] N) +
      (x + y) =
    HAdd.hAdd (α := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) x : M ⊗[R] N) x +
      HAdd.hAdd (α := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) y : M ⊗[R] N) y
⊢ HAdd.hAdd (α := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) (x + y) : M ⊗[R] N) (x + y) =
    HAdd.hAdd (α := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) x : M ⊗[R] N) x +
      HAdd.hAdd (α := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) y : M ⊗[R] N) y

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) x : M ⊗[R] N)
        ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) y : M ⊗[R] N) +
      (x + y) =
    HAdd.hAdd (α := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) x : M ⊗[R] N) x +
      HAdd.hAdd (α := M ⊗[R] N) ((Neg.aux R : (a : M ⊗[R] N) → M ⊗[R] N) y : M ⊗[R] N) y

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
suffices : -x + x + (-y + y) = 0
⊢ -(x + y) + (x + y) = 0

Tactic:
suffices -x + x + (-y + y) = 0 by
      rw [← this]
      unfold Neg.neg neg
      simp only
      rw [map_add]
      abel
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
rw : 0 + (-y + y) = 0
rw₁ : HAdd.hAdd (α := M ⊗[R] N) 0 0 = 0
rw₂ rw₃ : Eq (α := M ⊗[R] N) 0 0
⊢ -x + x + (-y + y) = 0

Tactic:
rw [hx, hy, add_zero]

Premises used: add_zero
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
⊢ ∀ (a : M ⊗[R] N), HSMul.hSMul (α := ℤ) 0 a = 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
⊢ ∀ (n : ℕ) (a : M ⊗[R] N), HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a = HSMul.hSMul (α := ℤ) (↑n : ℤ) a + a

Tactic:
simp [add_comm, TensorProduct.add_smul]

Premises used: add_comm, TensorProduct.add_smul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
n : ℕ
x : M ⊗[R] N
change : HSMul.hSMul (α := ℤ) (-(↑n.succ : ℤ)) x = -(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • x)
⊢ Int.negSucc n • x = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) x

Tactic:
change (-n.succ : ℤ) • x = -(((n : ℤ) + 1) • x)

Premises used: Nat.cast, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, Nat.succ, Neg.neg
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
n : ℕ
x : M ⊗[R] N
rw : -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) x = -(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • x)
⊢ HSMul.hSMul (α := ℤ) (-(↑n.succ : ℤ)) x = -(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • x)

Tactic:
rw [← zero_add (_ • x), ← TensorProduct.neg_add_cancel ((n.succ : ℤ) • x), add_assoc,
      ← add_smul, ← sub_eq_add_neg, sub_self, zero_smul, add_zero]

Premises used: sub_self, add_assoc, sub_eq_add_neg, zero_add, Nat.cast, zero_smul, add_smul, HSMul.hSMul, add_zero, TensorProduct.neg_add_cancel, Nat.succ
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
n : ℕ
x : M ⊗[R] N
⊢ -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) x = -(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • x)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : M
n : N
⊢ Eq (α := M ⊗[R] N) ((-m) ⊗ₜ[R] n) (-m ⊗ₜ[R] n)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
P : Type u_4
inst_1 : AddCommGroup M
inst_2 : AddCommGroup P
inst_3 : Module R M
inst_4 : Module R P
m : M
p : P
⊢ Eq (α := M ⊗[R] P) (m ⊗ₜ[R] (-p)) (-m ⊗ₜ[R] p)

Tactic:
(mk R M P _).map_neg _

Premises used: LinearMap.map_neg, TensorProduct.tmul, DFunLike.coe, AddCon.toQuotient, TensorProduct.mk
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
P : Type u_4
inst_1 : AddCommGroup M
inst_2 : AddCommGroup P
inst_3 : Module R M
inst_4 : Module R P
m : M
p₁ p₂ : P
⊢ m ⊗ₜ[R] (p₁ - p₂) = HSub.hSub (α := M ⊗[R] P) (m ⊗ₜ[R] p₁) (m ⊗ₜ[R] p₂)

Tactic:
(mk R M P _).map_sub _ _

Premises used: LinearMap.map_sub, TensorProduct.tmul, DFunLike.coe, AddCon.toQuotient, TensorProduct.mk
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m₁ m₂ : M
n : N
⊢ (m₁ - m₂) ⊗ₜ[R] n = HSub.hSub (α := M ⊗[R] N) (m₁ ⊗ₜ[R] n) (m₂ ⊗ₜ[R] n)

Tactic:
(mk R M N).map_sub₂ _ _ _

Premises used: LinearMap.map_sub₂, TensorProduct.tmul, AddCon.toQuotient, TensorProduct.mk
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
r : ℤ
m : M
p : P
⊢ Eq (α := M ⊗[R] P) (HSMul.hSMul (α := ℤ) 0 m ⊗ₜ[R] p) (m ⊗ₜ[R] HSMul.hSMul (α := ℤ) 0 p)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
r_1 : ℤ
m : M
p : P
r : ℕ
ih : Eq (α := M ⊗[R] P) (HSMul.hSMul (α := ℤ) (↑r : ℤ) m ⊗ₜ[R] p) (m ⊗ₜ[R] HSMul.hSMul (α := ℤ) (↑r : ℤ) p)
⊢ Eq (α := M ⊗[R] P) ((HAdd.hAdd (α := ℤ) (↑r : ℤ) 1 • m) ⊗ₜ[R] p) (m ⊗ₜ[R] (HAdd.hAdd (α := ℤ) (↑r : ℤ) 1 • p))

Tactic:
simpa [add_smul, tmul_add, add_tmul] using ih

Premises used: add_smul, TensorProduct.tmul_add, TensorProduct.add_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
r_1 : ℤ
m : M
p : P
r : ℕ
ih : Eq (α := M ⊗[R] P) (HSMul.hSMul (α := ℤ) (-(↑r : ℤ)) m ⊗ₜ[R] p) (m ⊗ₜ[R] HSMul.hSMul (α := ℤ) (-(↑r : ℤ)) p)
⊢ Eq (α := M ⊗[R] P) ((HSub.hSub (α := ℤ) (-(↑r : ℤ)) 1 • m) ⊗ₜ[R] p) (m ⊗ₜ[R] (HSub.hSub (α := ℤ) (-(↑r : ℤ)) 1 • p))

Tactic:
simpa [sub_smul, tmul_sub, sub_tmul] using ih

Premises used: TensorProduct.tmul_sub, sub_smul, TensorProduct.sub_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S_1 : Type u_6
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : AddCommGroup P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
S : Type u_7
inst_9 : Monoid S
inst_10 : DistribMulAction S M
inst_11 : DistribMulAction S N
inst_12 : CompatibleSMul R S M N
⊢ CompatibleSMul.{u_1, u_7, u_2, u_3} R Sˣ M N

Tactic:
⟨fun s m n => CompatibleSMul.smul_tmul (s : S) m n⟩

Premises used: Units.val, TensorProduct.CompatibleSMul.smul_tmul, TensorProduct.CompatibleSMul.mk
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : AddCommMonoid N
inst_8 : Module R N
b : Basis ι S M
c : Basis κ R N
i : ι
j : κ
⊢ Eq (α := M ⊗[R] N) (((b.tensorProduct c : Basis (ι × κ) S (M ⊗[R] N)) : (a : ι × κ) → M ⊗[R] N) (i, j) : M ⊗[R] N)
    ((b : (a : ι) → M) i ⊗ₜ[R] (c : (a : κ) → N) j : M ⊗[R] N)

Tactic:
simp [tensorProduct]

Premises used: Module.Basis.tensorProduct