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 : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : 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
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
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
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
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₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m : M
simp_rw :
  Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, 0)) :
      P)
    (0 : P)
simp_rw₁ : Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) 0 : P) (0 : P)
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, 0)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        0 :
      P)

Tactic:
simp_rw [map_zero, FreeAddMonoid.lift_eval_of, map_zero]

Premises used: map_zero, FreeAddMonoid.lift_eval_of
-- 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 : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : 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
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
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
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
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₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
rw :
  Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (s • m, n).1 : N →+ P) : (a : N) → P) (s • m, n).2 : P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, s • n)) :
      P)
rw₁ :
  Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (s • m, n).1 : N →+ P) : (a : N) → P) (s • m, n).2 : P)
    ((((f : (a : M) → N →+ P) (m, s • n).1 : N →+ P) : (a : N) → P) (m, s • n).2 : P)
rw₂ rw₃ :
  Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (s • (s • m, n).2) : P)
    ((((f : (a : M) → N →+ P) (m, s • n).1 : N →+ P) : (a : N) → P) (m, s • n).2 : P)
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (s • m, n)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (m, s • n)) :
      P)

Tactic:
rw [FreeAddMonoid.lift_eval_of, FreeAddMonoid.lift_eval_of, hf]

Premises used: FreeAddMonoid.lift_eval_of
-- 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 : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : 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
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
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
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
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₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x_1 y_1 : FreeAddMonoid (M × N)
hxy : Eqv R M N x_1 y_1
x y : FreeAddMonoid (M × N)
simp_rw :
  HAdd.hAdd (α := P) (β := P)
      (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
              (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
            (a : FreeAddMonoid (M × N)) → P)
          x :
        P)
      (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
              (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
            (a : FreeAddMonoid (M × N)) → P)
          y :
        P) =
    HAdd.hAdd (α := P) (β := P)
      (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
              (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
            (a : FreeAddMonoid (M × N)) → P)
          y :
        P)
      (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
              (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
            (a : FreeAddMonoid (M × N)) → P)
          x :
        P)
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (x + y) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (y + x) :
      P)

Tactic:
simp_rw [map_add, add_comm]

Premises used: map_add, add_comm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
m : M
n : N
⊢ Eq.{u_9 + 1} (α := P) ((liftAddHom f hf : (a : M ⊗[R] N) → P) (m ⊗ₜ[R] n) : P)
    ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) n : P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- 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 : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : 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
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
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
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
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
f : M →ₗ[R] N →ₗ[R] P
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
r : R
m : M
n : N
dsimp :
  Eq.{u_17 + 1} (α := P₂) ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) (r • m) : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)
    ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) (r • n) : P₂)
⊢ Eq.{u_17 + 1} (α := P₂)
    ((((AddMonoidHom.comp LinearMap.toAddMonoidHom' f'.toAddMonoidHom : (a : M) → N →+ P₂) (r • m) : N →+ P₂) :
          (a : N) → P₂)
        n :
      P₂)
    ((((AddMonoidHom.comp LinearMap.toAddMonoidHom' f'.toAddMonoidHom : (a : M) → N →+ P₂) m : N →+ P₂) : (a : N) → P₂)
        (r • n) :
      P₂)

Tactic:
dsimp
-- 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 : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : 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
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
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
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
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
f : M →ₗ[R] N →ₗ[R] P
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
r : R
m : M
n : N
rw :
  HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂) =
    (((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) (r • n)
rw₁ rw₂ :
  HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂) =
    HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)
⊢ Eq.{u_17 + 1} (α := P₂) ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) (r • m) : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)
    ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) (r • n) : P₂)

Tactic:
rw [LinearMap.map_smulₛₗ₂, map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ, LinearMap.map_smulₛₗ₂
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P₂
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R₂ P₂
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
m : M
n : N
⊢ Eq.{u_17 + 1} (α := P₂) ((liftAux f' : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)
    ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P₂
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R₂ P₂
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
r : R
x : M ⊗[R] N
p : M
q : N
simp_rw :
  (liftAux f' : (a : M ⊗[R] N) → P₂) (p ⊗ₜ[R] (r • q)) =
    HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      ((liftAux f' : (a : M ⊗[R] N) → P₂) (p ⊗ₜ[R] q) : P₂)
simp_rw₁ :
  (((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) p : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) (r • q) =
    HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) p : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) q : P₂)
⊢ (liftAux f' : (a : M ⊗[R] N) → P₂) (HSMul.hSMul (β := M ⊗[R] N) r (p ⊗ₜ[R] q)) =
    HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      ((liftAux f' : (a : M ⊗[R] N) → P₂) (p ⊗ₜ[R] q) : P₂)

Tactic:
simp_rw [← tmul_smul, liftAux_tmul, (f' p).map_smulₛₗ]

Premises used: TensorProduct.liftAux_tmul, TensorProduct.tmul_smul, LinearMap.map_smulₛₗ, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P₂
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R₂ P₂
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
r : R
x p q : M ⊗[R] N
ih1 :
  (liftAux f' : (a : M ⊗[R] N) → P₂) (r • p) =
    HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      ((liftAux f' : (a : M ⊗[R] N) → P₂) p : P₂)
ih2 :
  (liftAux f' : (a : M ⊗[R] N) → P₂) (r • q) =
    HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      ((liftAux f' : (a : M ⊗[R] N) → P₂) q : P₂)
simp_rw :
  (liftAux f' : (a : M ⊗[R] N) → P₂) (r • p + r • q) =
    HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      ((liftAux f' : (a : M ⊗[R] N) → P₂) (p + q) : P₂)
simp_rw₁ :
  HAdd.hAdd (α := P₂) (β := P₂) ((liftAux f' : (a : M ⊗[R] N) → P₂) (r • p) : P₂)
      ((liftAux f' : (a : M ⊗[R] N) → P₂) (r • q) : P₂) =
    HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      (HAdd.hAdd (α := P₂) (β := P₂) ((liftAux f' : (a : M ⊗[R] N) → P₂) p : P₂)
        ((liftAux f' : (a : M ⊗[R] N) → P₂) q : P₂))
simp_rw₂ :
  HAdd.hAdd (β := P₂)
      (HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
        ((liftAux f' : (a : M ⊗[R] N) → P₂) p : P₂))
      ((liftAux f' : (a : M ⊗[R] N) → P₂) (r • q) : P₂) =
    HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      (HAdd.hAdd (α := P₂) (β := P₂) ((liftAux f' : (a : M ⊗[R] N) → P₂) p : P₂)
        ((liftAux f' : (a : M ⊗[R] N) → P₂) q : P₂))
simp_rw₃ :
  HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
        ((liftAux f' : (a : M ⊗[R] N) → P₂) p : P₂) +
      HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
        ((liftAux f' : (a : M ⊗[R] N) → P₂) q : P₂) =
    HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      (HAdd.hAdd (α := P₂) (β := P₂) ((liftAux f' : (a : M ⊗[R] N) → P₂) p : P₂)
        ((liftAux f' : (a : M ⊗[R] N) → P₂) q : P₂))
⊢ (liftAux f' : (a : M ⊗[R] N) → P₂) (r • (p + q)) =
    HSMul.hSMul.{u_2, u_17, u_17} (α := R₂) (β := P₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      ((liftAux f' : (a : M ⊗[R] N) → P₂) (p + q) : P₂)

Tactic:
simp_rw [smul_add, (liftAux f').map_add, ih1, ih2, smul_add]

Premises used: TensorProduct.liftAux, AddMonoidHom.map_add, smul_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
r : R
x : M ⊗[R] N
⊢ (liftAux f : (a : M ⊗[R] N) → P) (r • x) = HSMul.hSMul (β := P) r ((liftAux f : (a : M ⊗[R] N) → P) x : P)

Tactic:
liftAux.smulₛₗ _ _

Premises used: TensorProduct.liftAux.smulₛₗ
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P₂
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R₂ P₂
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
x : M
y : N
⊢ Eq.{u_17 + 1} (α := P₂) ((lift f' : (a : M ⊗[R] N) → P₂) (x ⊗ₜ[R] y) : P₂)
    ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) x : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) y : P₂)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P₂
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R₂ P₂
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
x : M
y : N
⊢ Eq.{u_17 + 1} (α := P₂) (((lift f').toAddHom : (a : M ⊗[R] N) → P₂) (x ⊗ₜ[R] y) : P₂)
    ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) x : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) y : P₂)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P₂
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R₂ P₂
g h : M ⊗[R] N →ₛₗ[σ₁₂] P₂
H :
  ∀ (x : M) (y : N),
    Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N) → P₂) (x ⊗ₜ[R] y) : P₂) ((h : (a : M ⊗[R] N) → P₂) (x ⊗ₜ[R] y) : P₂)
z : M ⊗[R] N
⊢ Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N) → P₂) 0 : P₂) ((h : (a : M ⊗[R] N) → P₂) 0 : P₂)

Tactic:
simp_rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P₂
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R₂ P₂
g h : M ⊗[R] N →ₛₗ[σ₁₂] P₂
H :
  ∀ (x : M) (y : N),
    Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N) → P₂) (x ⊗ₜ[R] y) : P₂) ((h : (a : M ⊗[R] N) → P₂) (x ⊗ₜ[R] y) : P₂)
z x y : M ⊗[R] N
ihx : Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N) → P₂) x : P₂) ((h : (a : M ⊗[R] N) → P₂) x : P₂)
ihy : Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N) → P₂) y : P₂) ((h : (a : M ⊗[R] N) → P₂) y : P₂)
rw :
  HAdd.hAdd (α := P₂) (β := P₂) ((g : (a : M ⊗[R] N) → P₂) x : P₂) ((g : (a : M ⊗[R] N) → P₂) y : P₂) =
    (h : (a : M ⊗[R] N) → P₂) (x + y)
rw₁ :
  HAdd.hAdd (α := P₂) (β := P₂) ((g : (a : M ⊗[R] N) → P₂) x : P₂) ((g : (a : M ⊗[R] N) → P₂) y : P₂) =
    HAdd.hAdd (α := P₂) (β := P₂) ((h : (a : M ⊗[R] N) → P₂) x : P₂) ((h : (a : M ⊗[R] N) → P₂) y : P₂)
rw₂ :
  HAdd.hAdd (α := P₂) (β := P₂) ((h : (a : M ⊗[R] N) → P₂) x : P₂) ((g : (a : M ⊗[R] N) → P₂) y : P₂) =
    HAdd.hAdd (α := P₂) (β := P₂) ((h : (a : M ⊗[R] N) → P₂) x : P₂) ((h : (a : M ⊗[R] N) → P₂) y : P₂)
rw₃ rw₄ :
  HAdd.hAdd (α := P₂) (β := P₂) ((h : (a : M ⊗[R] N) → P₂) x : P₂) ((h : (a : M ⊗[R] N) → P₂) y : P₂) =
    HAdd.hAdd (α := P₂) (β := P₂) ((h : (a : M ⊗[R] N) → P₂) x : P₂) ((h : (a : M ⊗[R] N) → P₂) y : P₂)
⊢ Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N) → P₂) (x + y) : P₂) ((h : (a : M ⊗[R] N) → P₂) (x + y) : P₂)

Tactic:
rw [g.map_add, h.map_add, ihx, ihy]

Premises used: LinearMap.map_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P₂
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R₂ P₂
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
g : M ⊗[R] N →ₛₗ[σ₁₂] P₂
H :
  ∀ (x : M) (y : N),
    Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N) → P₂) (x ⊗ₜ[R] y) : P₂)
      ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) x : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) y : P₂)
m : M
n : N
rw :
  Eq.{u_17 + 1} (α := P₂) ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)
    ((lift f' : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)
rw₁ rw₂ :
  Eq.{u_17 + 1} (α := P₂) ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)
    ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)
⊢ Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)
    ((lift f' : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)

Tactic:
rw [H, lift.tmul]

Premises used: TensorProduct.lift.tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (lift (mk R M N)) LinearMap.id

Tactic:
Eq.symm <| lift.unique fun _ _ => rfl

Premises used: TensorProduct.lift.unique, Eq.symm, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
M : Type u_7
N : Type u_8
P₂ : Type u_17
P₃ : Type u_18
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P₂
inst_6 : AddCommMonoid P₃
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R₂ P₂
inst_10 : Module R₃ P₃
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
h : P₂ →ₛₗ[σ₂₃] P₃
x : M
x_1 : N
⊢ Eq.{u_18 + 1} (α := P₃) ((h ∘ₛₗ lift f' : (a : M ⊗[R] N) → P₃) (x ⊗ₜ[R] x_1) : P₃)
    ((((f'.compr₂ₛₗ h : (a : M) → N →ₛₗ[σ₁₃] P₃) x : N →ₛₗ[σ₁₃] P₃) : (a : N) → P₃) x_1 : P₃)

Tactic:
simp