awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
f g : Module.End R N
⊢ lTensor M (f * g) = HMul.hMul (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (lTensor M f) (lTensor M g)

Tactic:
lTensor_comp M f g

Premises used: LinearMap.lTensor_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
f g : Module.End R N
⊢ rTensor M (f * g) = HMul.hMul (α := N ⊗[R] M →ₗ[R] N ⊗[R] M) (rTensor M f) (rTensor M g)

Tactic:
rTensor_comp M f g

Premises used: LinearMap.rTensor_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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) (lTensor M id) id

Tactic:
map_id

Premises used: LinearMap.lTensor, TensorProduct.map_id
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
x : M ⊗[R] N
rw : (id : (a : M ⊗[R] N) → M ⊗[R] N) x = x
rw₁ : _root_.id x = x
rw₂ rw₃ : x = x
⊢ (lTensor M id : (a : M ⊗[R] N) → M ⊗[R] N) x = x

Tactic:
rw [lTensor_id, id_coe, _root_.id]

Premises used: LinearMap.id_coe, id, LinearMap.lTensor_id
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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 (α := N ⊗[R] M →ₗ[R] N ⊗[R] M) (rTensor M id) id

Tactic:
map_id

Premises used: TensorProduct.map_id, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
x : N ⊗[R] M
rw : (id : (a : N ⊗[R] M) → N ⊗[R] M) x = x
rw₁ : _root_.id x = x
rw₂ rw₃ : x = x
⊢ (rTensor M id : (a : N ⊗[R] M) → N ⊗[R] M) x = x

Tactic:
rw [rTensor_id, id_coe, _root_.id]

Premises used: LinearMap.rTensor_id, LinearMap.id_coe, id
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
r : R
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (lTensor M (DistribSMul.toLinearMap R N r)) (DistribSMul.toLinearMap R (M ⊗[R] N) r)

Tactic:
(lTensor_smul M r LinearMap.id).trans (congrArg _ (lTensor_id M N))

Premises used: LinearMap.id, LinearMap.lTensor_smul, DistribSMul.toLinearMap, congrArg, LinearMap.lTensor_id, Eq.trans
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
r : R
⊢ Eq (α := N ⊗[R] M →ₗ[R] N ⊗[R] M) (rTensor M (DistribSMul.toLinearMap R N r)) (DistribSMul.toLinearMap R (N ⊗[R] M) r)

Tactic:
(rTensor_smul M r LinearMap.id).trans (congrArg _ (rTensor_id M N))

Premises used: LinearMap.id, LinearMap.rTensor_id, DistribSMul.toLinearMap, congrArg, LinearMap.rTensor_smul, Eq.trans
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid 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
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ lTensor P g ∘ₗ rTensor N f = map f g

Tactic:
simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Premises used: LinearMap.lTensor, TensorProduct.map_comp, LinearMap.comp_id, LinearMap.id_comp, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid 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
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ rTensor Q f ∘ₗ lTensor M g = map f g

Tactic:
simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Premises used: LinearMap.lTensor, TensorProduct.map_comp, LinearMap.comp_id, LinearMap.id_comp, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : Module R P
inst_10 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
f' : S →ₗ[R] M
⊢ map f g ∘ₗ rTensor N f' = map (f ∘ₗ f') g

Tactic:
simp only [rTensor, ← map_comp, comp_id]

Premises used: TensorProduct.map_comp, LinearMap.comp_id, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : Module R P
inst_10 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
f' : S →ₗ[R] M
x : S ⊗[R] N
⊢ Eq (α := P ⊗[R] Q) ((map f g : (a : M ⊗[R] N) → P ⊗[R] Q) ((rTensor N f' : (a : S ⊗[R] N) → M ⊗[R] N) x) : P ⊗[R] Q)
    ((map (f ∘ₗ f') g : (a : S ⊗[R] N) → P ⊗[R] Q) x : P ⊗[R] Q)

Tactic:
LinearMap.congr_fun (map_comp_rTensor _ _ _ _) x

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.map_comp_rTensor, LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : Module R P
inst_10 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
g' : S →ₗ[R] N
⊢ map f g ∘ₗ lTensor M g' = map f (g ∘ₗ g')

Tactic:
simp only [lTensor, ← map_comp, comp_id]

Premises used: LinearMap.lTensor, TensorProduct.map_comp, LinearMap.comp_id
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : Module R P
inst_10 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
g' : S →ₗ[R] N
x : M ⊗[R] S
⊢ Eq (α := P ⊗[R] Q) ((map f g : (a : M ⊗[R] N) → P ⊗[R] Q) ((lTensor M g' : (a : M ⊗[R] S) → M ⊗[R] N) x) : P ⊗[R] Q)
    ((map f (g ∘ₗ g') : (a : M ⊗[R] S) → P ⊗[R] Q) x : P ⊗[R] Q)

Tactic:
LinearMap.congr_fun (map_comp_lTensor _ _ _ _) x

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.map_comp_lTensor, LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : Module R P
inst_10 : Module R Q
f' : P →ₗ[R] S
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ rTensor Q f' ∘ₗ map f g = map (f' ∘ₗ f) g

Tactic:
simp only [rTensor, ← map_comp, id_comp]

Premises used: TensorProduct.map_comp, LinearMap.id_comp, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : Module R P
inst_10 : Module R Q
g' : Q →ₗ[R] S
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ lTensor P g' ∘ₗ map f g = map f (g' ∘ₗ g)

Tactic:
simp only [lTensor, ← map_comp, id_comp]

Premises used: LinearMap.lTensor, TensorProduct.map_comp, LinearMap.id_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R S
inst_9 : Module R P
inst_10 : Module R Q
g' : Q →ₗ[R] S
f : M →ₗ[R] P
g : N →ₗ[R] Q
x : M ⊗[R] N
⊢ Eq (α := P ⊗[R] S) ((lTensor P g' : (a : P ⊗[R] Q) → P ⊗[R] S) ((map f g : (a : M ⊗[R] N) → P ⊗[R] Q) x) : P ⊗[R] S)
    ((map f (g' ∘ₗ g) : (a : M ⊗[R] N) → P ⊗[R] S) x : P ⊗[R] S)

Tactic:
LinearMap.congr_fun (lTensor_comp_map _ _ f g) x

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.congr_fun, LinearMap.lTensor_comp_map
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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] P
⊢ Eq (α := M ⊗[R] N →ₗ[R] N ⊗[R] P) (lTensor N f ∘ₗ (↑(TensorProduct.comm R M N) : M ⊗[R] N →ₗ[R] N ⊗[R] M))
    ((↑(TensorProduct.comm R P N) : P ⊗[R] N →ₗ[R] N ⊗[R] P) ∘ₗ rTensor N f)

Tactic:
TensorProduct.map_comp_comm_eq _ _

Premises used: TensorProduct.map_comp_comm_eq, LinearMap.lTensor, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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] P
⊢ Eq (α := N ⊗[R] M →ₗ[R] P ⊗[R] N) (rTensor N f ∘ₗ (↑(TensorProduct.comm R N M) : N ⊗[R] M →ₗ[R] M ⊗[R] N))
    ((↑(TensorProduct.comm R N P) : N ⊗[R] P →ₗ[R] P ⊗[R] N) ∘ₗ lTensor N f)

Tactic:
TensorProduct.map_comp_comm_eq _ _

Premises used: TensorProduct.map_comp_comm_eq, LinearMap.lTensor, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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] P
x : M ⊗[R] N
⊢ Eq (α := N ⊗[R] P)
    ((lTensor N f : (a : N ⊗[R] M) → N ⊗[R] P) ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) x) : N ⊗[R] P)
    ((TensorProduct.comm R P N : (a : P ⊗[R] N) → N ⊗[R] P) ((rTensor N f : (a : M ⊗[R] N) → P ⊗[R] N) x) : N ⊗[R] P)

Tactic:
congr($(LinearMap.lTensor_comp_comm f) _)

Premises used: congrArg, LinearMap.lTensor_comp_comm, id, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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] P
x : N ⊗[R] M
⊢ Eq (α := P ⊗[R] N)
    ((rTensor N f : (a : M ⊗[R] N) → P ⊗[R] N) ((TensorProduct.comm R N M : (a : N ⊗[R] M) → M ⊗[R] N) x) : P ⊗[R] N)
    ((TensorProduct.comm R N P : (a : N ⊗[R] P) → P ⊗[R] N) ((lTensor N f : (a : N ⊗[R] M) → N ⊗[R] P) x) : P ⊗[R] N)

Tactic:
congr($(LinearMap.rTensor_comp_comm f) _)

Premises used: congrArg, id, LinearMap.rTensor_comp_comm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
f : M →ₗ[R] M
n : ℕ
⊢ HPow.hPow (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (map f id) n = map (f ^ n) (HPow.hPow (α := N →ₗ[R] N) id n)

Tactic:
have h := TensorProduct.map_pow f (id : N →ₗ[R] N) n
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
f : M →ₗ[R] M
n : ℕ
h : HPow.hPow (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (map f id) n = map (f ^ n) (HPow.hPow (α := N →ₗ[R] N) id n)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : HPow.hPow (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (map f id) n = map (f ^ n) id),
    HPow.hPow (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (rTensor N f) n = rTensor N (f ^ n)
⊢ HPow.hPow (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (rTensor N f) n = rTensor N (f ^ n)

Tactic:
rwa [Module.End.id_pow] at h

Premises used: Module.End.id_pow
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
f : N →ₗ[R] N
n : ℕ
⊢ HPow.hPow (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (map id f) n = map (HPow.hPow (α := M →ₗ[R] M) id n) (f ^ n)

Tactic:
have h := TensorProduct.map_pow (id : M →ₗ[R] M) f n
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
f : N →ₗ[R] N
n : ℕ
h : HPow.hPow (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (map id f) n = map (HPow.hPow (α := M →ₗ[R] M) id n) (f ^ n)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : HPow.hPow (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (map id f) n = map id (f ^ n)),
    HPow.hPow (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (lTensor M f) n = lTensor M (f ^ n)
⊢ HPow.hPow (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (lTensor M f) n = lTensor M (f ^ n)

Tactic:
rwa [Module.End.id_pow] at h

Premises used: Module.End.id_pow
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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 : N ≃ₗ[R] P
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] P) (↑(lTensor M f) : M ⊗[R] N →ₗ[R] M ⊗[R] P) (LinearMap.lTensor M (↑f : N →ₗ[R] P))

Tactic:
rfl

Premises used: LinearMap.lTensor, TensorProduct.map, TensorProduct.lift, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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 : N ≃ₗ[R] P
⊢ Eq (α := M ⊗[R] P →ₗ[R] M ⊗[R] N) (↑(symm (lTensor M f)) : M ⊗[R] P →ₗ[R] M ⊗[R] N)
    (LinearMap.lTensor M (↑f.symm : P →ₗ[R] N))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.lTensor, TensorProduct.map, TensorProduct, TensorProduct.lift, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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 : N ≃ₗ[R] P
⊢ Eq (α := N ⊗[R] M →ₗ[R] P ⊗[R] M) (↑(rTensor M f) : N ⊗[R] M →ₗ[R] P ⊗[R] M) (LinearMap.rTensor M (↑f : N →ₗ[R] P))

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, rfl, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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 : N ≃ₗ[R] P
⊢ Eq (α := P ⊗[R] M →ₗ[R] N ⊗[R] M) (↑(symm (rTensor M f)) : P ⊗[R] M →ₗ[R] N ⊗[R] M)
    (LinearMap.rTensor M (↑f.symm : P →ₗ[R] N))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.map, TensorProduct, TensorProduct.lift, rfl, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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 : N ≃ₗ[R] P
m : M
n : N
⊢ Eq (α := M ⊗[R] P) ((lTensor M f : (a : M ⊗[R] N) → M ⊗[R] P) (m ⊗ₜ[R] n) : M ⊗[R] P)
    (m ⊗ₜ[R] (f : (a : N) → P) n : M ⊗[R] P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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 : N ≃ₗ[R] P
m : M
p : P
⊢ Eq (α := M ⊗[R] N) ((symm (lTensor M f) : (a : M ⊗[R] P) → M ⊗[R] N) (m ⊗ₜ[R] p) : M ⊗[R] N)
    (m ⊗ₜ[R] (f.symm : (a : P) → N) p : M ⊗[R] N)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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 : N ≃ₗ[R] P
m : M
n : N
⊢ Eq (α := P ⊗[R] M) ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) (n ⊗ₜ[R] m) : P ⊗[R] M)
    ((f : (a : N) → P) n ⊗ₜ[R] m : P ⊗[R] M)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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 : N ≃ₗ[R] P
m : M
p : P
⊢ Eq (α := N ⊗[R] M) ((symm (rTensor M f) : (a : P ⊗[R] M) → N ⊗[R] M) (p ⊗ₜ[R] m) : N ⊗[R] M)
    ((f.symm : (a : P) → N) p ⊗ₜ[R] m : N ⊗[R] M)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N ≃ₗ[R] P
⊢ Eq (α := Q ⊗[R] N ≃ₗ[R] Q ⊗[R] P) (TensorProduct.comm R Q N ≪≫ₗ rTensor Q g ≪≫ₗ TensorProduct.comm R P Q)
    (lTensor Q g)

Tactic:
toLinearMap_injective <| TensorProduct.ext rfl

Premises used: LinearEquiv.toLinearMap_injective, TensorProduct.ext, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N ≃ₗ[R] P
⊢ Eq (α := N ⊗[R] Q ≃ₗ[R] P ⊗[R] Q) (TensorProduct.comm R N Q ≪≫ₗ lTensor Q g ≪≫ₗ TensorProduct.comm R Q P)
    (rTensor Q g)

Tactic:
toLinearMap_injective <| TensorProduct.ext rfl

Premises used: LinearEquiv.toLinearMap_injective, TensorProduct.ext, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid 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
g : P ≃ₗ[R] Q
f : N ≃ₗ[R] P
⊢ Eq (α := M ⊗[R] N ≃ₗ[R] M ⊗[R] Q) (lTensor M (f ≪≫ₗ g)) (lTensor M f ≪≫ₗ lTensor M g)

Tactic:
toLinearMap_injective <| LinearMap.lTensor_comp M _ _

Premises used: LinearEquiv.toLinearMap_injective, LinearMap.lTensor_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid 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
g : P ≃ₗ[R] Q
f : N ≃ₗ[R] P
x : M ⊗[R] N
⊢ Eq (α := M ⊗[R] Q) ((lTensor M (f ≪≫ₗ g) : (a : M ⊗[R] N) → M ⊗[R] Q) x : M ⊗[R] Q)
    ((lTensor M g : (a : M ⊗[R] P) → M ⊗[R] Q) ((lTensor M f : (a : M ⊗[R] N) → M ⊗[R] P) x) : M ⊗[R] Q)

Tactic:
LinearMap.lTensor_comp_apply M _ _ x

Premises used: LinearMap.lTensor_comp_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid 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
g : P ≃ₗ[R] Q
f : N ≃ₗ[R] P
⊢ Eq (α := N ⊗[R] M ≃ₗ[R] Q ⊗[R] M) (rTensor M (f ≪≫ₗ g)) (rTensor M f ≪≫ₗ rTensor M g)

Tactic:
toLinearMap_injective <| LinearMap.rTensor_comp M _ _

Premises used: LinearEquiv.toLinearMap_injective, LinearMap.rTensor_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid 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
g : P ≃ₗ[R] Q
f : N ≃ₗ[R] P
y : N ⊗[R] M
⊢ Eq (α := Q ⊗[R] M) ((rTensor M (f ≪≫ₗ g) : (a : N ⊗[R] M) → Q ⊗[R] M) y : Q ⊗[R] M)
    ((rTensor M g : (a : P ⊗[R] M) → Q ⊗[R] M) ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) y) : Q ⊗[R] M)

Tactic:
LinearMap.rTensor_comp_apply M _ _ y

Premises used: LinearMap.rTensor_comp_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
f g : N ≃ₗ[R] N
⊢ lTensor M (f * g) = HMul.hMul (α := M ⊗[R] N ≃ₗ[R] M ⊗[R] N) (lTensor M f) (lTensor M g)

Tactic:
lTensor_trans M f g

Premises used: LinearEquiv.lTensor_trans
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
f g : N ≃ₗ[R] N
⊢ rTensor M (f * g) = HMul.hMul (α := N ⊗[R] M ≃ₗ[R] N ⊗[R] M) (rTensor M f) (rTensor M g)

Tactic:
rTensor_trans M f g

Premises used: LinearEquiv.rTensor_trans
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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) (lTensor M (refl R N)) (refl R (M ⊗[R] N))

Tactic:
TensorProduct.congr_refl_refl

Premises used: TensorProduct.congr_refl_refl, LinearEquiv.lTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
x : M ⊗[R] N
rw : (refl R (M ⊗[R] N) : (a : M ⊗[R] N) → M ⊗[R] N) x = x
rw₁ rw₂ : x = x
⊢ (lTensor M (refl R N) : (a : M ⊗[R] N) → M ⊗[R] N) x = x

Tactic:
rw [lTensor_refl, refl_apply]

Premises used: LinearEquiv.lTensor_refl, LinearEquiv.refl_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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 (α := N ⊗[R] M ≃ₗ[R] N ⊗[R] M) (rTensor M (refl R N)) (refl R (N ⊗[R] M))

Tactic:
TensorProduct.congr_refl_refl

Premises used: LinearEquiv.rTensor, TensorProduct.congr_refl_refl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
y : N ⊗[R] M
rw : (refl R (N ⊗[R] M) : (a : N ⊗[R] M) → N ⊗[R] M) y = y
rw₁ rw₂ : y = y
⊢ (rTensor M (refl R N) : (a : N ⊗[R] M) → N ⊗[R] M) y = y

Tactic:
rw [rTensor_refl, refl_apply]

Premises used: LinearEquiv.rTensor_refl, LinearEquiv.refl_apply