awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid N₂
inst_7 : AddCommMonoid M₃
inst_8 : AddCommMonoid N₃
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R₂ M₂
inst_12 : Module R₂ N₂
inst_13 : Module R₃ M₃
inst_14 : Module R₃ N₃
σ₂₁ : R₂ →+* R
inst_15 : RingHomInvPair σ₁₂ σ₂₁
inst_16 : RingHomInvPair σ₂₁ σ₁₂
σ₃₂ : R₃ →+* R₂
inst_17 : RingHomInvPair σ₂₃ σ₃₂
inst_18 : RingHomInvPair σ₃₂ σ₂₃
σ₃₁ : R₃ →+* R
inst_19 : RingHomInvPair σ₁₃ σ₃₁
inst_20 : RingHomInvPair σ₃₁ σ₁₃
inst_21 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_22 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
f₂ : M₂ ≃ₛₗ[σ₂₃] M₃
g₂ : N₂ ≃ₛₗ[σ₂₃] N₃
f₁ : M ≃ₛₗ[σ₁₂] M₂
g₁ : N ≃ₛₗ[σ₁₂] N₂
⊢ Eq (α := M ⊗[R] N ≃ₛₗ[σ₁₃] M₃ ⊗[R₃] N₃) (congr (f₁.trans f₂) (g₁.trans g₂)) ((congr f₁ g₁).trans (congr f₂ g₂))

Tactic:
LinearEquiv.toLinearMap_injective <| map_comp _ _ _ _

Premises used: LinearEquiv.toLinearMap_injective, TensorProduct.map_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid N₂
inst_7 : AddCommMonoid M₃
inst_8 : AddCommMonoid N₃
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R₂ M₂
inst_12 : Module R₂ N₂
inst_13 : Module R₃ M₃
inst_14 : Module R₃ N₃
σ₂₁ : R₂ →+* R
inst_15 : RingHomInvPair σ₁₂ σ₂₁
inst_16 : RingHomInvPair σ₂₁ σ₁₂
σ₃₂ : R₃ →+* R₂
inst_17 : RingHomInvPair σ₂₃ σ₃₂
inst_18 : RingHomInvPair σ₃₂ σ₂₃
σ₃₁ : R₃ →+* R
inst_19 : RingHomInvPair σ₁₃ σ₃₁
inst_20 : RingHomInvPair σ₃₁ σ₁₃
inst_21 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_22 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
f₂ : M₂ ≃ₛₗ[σ₂₃] M₃
g₂ : N₂ ≃ₛₗ[σ₂₃] N₃
f₁ : M ≃ₛₗ[σ₁₂] M₂
g₁ : N ≃ₛₗ[σ₁₂] N₂
x : M ⊗[R] N
⊢ Eq (α := M₃ ⊗[R₃] N₃)
    ((congr f₂ g₂ : (a : M₂ ⊗[R₂] N₂) → M₃ ⊗[R₃] N₃) ((congr f₁ g₁ : (a : M ⊗[R] N) → M₂ ⊗[R₂] N₂) x) : M₃ ⊗[R₃] N₃)
    ((congr (f₁.trans f₂) (g₁.trans g₂) : (a : M ⊗[R] N) → M₃ ⊗[R₃] N₃) x : M₃ ⊗[R₃] N₃)

Tactic:
DFunLike.congr_fun (congr_trans ..).symm x

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, TensorProduct.congr_trans, Eq.symm
-- 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
g : N ≃ₗ[R] N
f' : M ≃ₗ[R] M
g' : N ≃ₗ[R] N
⊢ congr (f * f') (g * g') = congr f g * congr f' g'

Tactic:
congr_trans _ _ _ _

Premises used: TensorProduct.congr_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 : M ≃ₗ[R] M
g : N ≃ₗ[R] N
⊢ HPow.hPow (β := ℕ) (congr f g) 0 = congr (HPow.hPow (β := ℕ) f 0) (HPow.hPow (β := ℕ) g 0)

Tactic:
congr_refl_refl.symm

Premises used: TensorProduct.congr_refl_refl, npowRec, LinearEquiv.refl, Eq.symm
-- 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
g : N ≃ₗ[R] N
⊢ HPow.hPow (β := ℕ) (congr f g) 0 = congr (HPow.hPow (β := ℕ) f 0) (HPow.hPow (β := ℕ) g 0)

Tactic:
exact congr_refl_refl.symm

Premises used: TensorProduct.congr_refl_refl, Eq.symm
-- 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
g : N ≃ₗ[R] N
n : ℕ
ih : congr f g ^ n = congr (f ^ n) (g ^ n)
succ : congr f g ^ n * congr f g = congr (f ^ n * f) (g ^ n * g)
succ₁ : congr (f ^ n) (g ^ n) * congr f g = congr (f ^ n * f) (g ^ n * g)
⊢ congr f g ^ (n + 1) = congr (f ^ (n + 1)) (g ^ (n + 1))

Tactic:
simp_rw [pow_succ, ih, congr_mul]

Premises used: pow_succ, TensorProduct.congr_mul
-- 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
g : N ≃ₗ[R] N
n : ℕ
zero : HPow.hPow (β := ℕ) (congr f g) 0 = congr (HPow.hPow (β := ℕ) f 0) (HPow.hPow (β := ℕ) g 0)
succ : ∀ (n : ℕ) (ih : congr f g ^ n = congr (f ^ n) (g ^ n)), congr f g ^ (n + 1) = congr (f ^ (n + 1)) (g ^ (n + 1))
⊢ congr f g ^ n = congr (f ^ n) (g ^ n)

Tactic:
induction n with
  | zero => exact congr_refl_refl.symm
  | succ n ih => simp_rw [pow_succ, ih, congr_mul]

Premises used: pow_succ, TensorProduct.congr_refl_refl, TensorProduct.congr_mul, Eq.symm
-- 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
g : N ≃ₗ[R] N
n : ℕ
⊢ congr f g ^ Int.ofNat n = congr (f ^ Int.ofNat n) (g ^ Int.ofNat n)

Tactic:
congr_pow _ _ _

Premises used: zpowRec, TensorProduct.congr_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 : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ congr f g ^ Int.ofNat n = congr (f ^ Int.ofNat n) (g ^ Int.ofNat n)

Tactic:
exact congr_pow _ _ _

Premises used: TensorProduct.congr_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 : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
negSucc : (congr (f ^ (n + 1)) (g ^ (n + 1)))⁻¹ = congr (f ^ (n + 1))⁻¹ (g ^ (n + 1))⁻¹
⊢ congr f g ^ Int.negSucc n = congr (f ^ Int.negSucc n) (g ^ Int.negSucc n)

Tactic:
simp_rw [zpow_negSucc, congr_pow]

Premises used: zpow_negSucc, TensorProduct.congr_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 : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ (congr (f ^ (n + 1)) (g ^ (n + 1)))⁻¹ = congr (f ^ (n + 1))⁻¹ (g ^ (n + 1))⁻¹

Tactic:
congr_symm _ _

Premises used: TensorProduct.congr_symm
-- 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
g : N ≃ₗ[R] N
n : ℕ
⊢ (congr (f ^ (n + 1)) (g ^ (n + 1)))⁻¹ = congr (f ^ (n + 1))⁻¹ (g ^ (n + 1))⁻¹

Tactic:
exact congr_symm _ _

Premises used: TensorProduct.congr_symm
-- 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
g : N ≃ₗ[R] N
n : ℤ
ofNat : ∀ (n : ℕ), congr f g ^ Int.ofNat n = congr (f ^ Int.ofNat n) (g ^ Int.ofNat n)
negSucc : ∀ (n : ℕ), congr f g ^ Int.negSucc n = congr (f ^ Int.negSucc n) (g ^ Int.negSucc n)
⊢ congr f g ^ n = congr (f ^ n) (g ^ n)

Tactic:
cases n with
  | ofNat n => exact congr_pow _ _ _
  | negSucc n => simp_rw [zpow_negSucc, congr_pow]; exact congr_symm _ _

Premises used: TensorProduct.congr_symm, zpow_negSucc, TensorProduct.congr_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
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] N
g : P →ₗ[R] Q
hf : Function.Bijective.{u_7 + 1, u_8 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Bijective.{u_9 + 1, u_10 + 1} (α := P) (β := Q) (⇑g : (a : P) → Q)
⊢ Function.Bijective (α := M ⊗[R] P) (β := N ⊗[R] Q) (⇑(map f g) : (a : M ⊗[R] P) → N ⊗[R] Q)

Tactic:
(TensorProduct.congr (.ofBijective f hf) (.ofBijective g hg)).bijective

Premises used: LinearEquiv.bijective, TensorProduct.congr, LinearEquiv.ofBijective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R_1 : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R_1
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R_1 →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R_1 →+* R₃
A : Type u_6
M_1 : Type u_7
N_1 : 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_1
inst_6 : AddCommMonoid N_1
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_1
inst_21 : Module R'' M_1
inst_22 : Module R_1 M_1
inst_23 : Module R_1 N_1
inst_24 : Module R_1 S
inst_25 : Module R_1 P'
inst_26 : Module R_1 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_1 P
inst_36 : Module R_1 Q
σ₂₁ : R₂ →+* R_1
inst_37 : RingHomInvPair σ₁₂ σ₂₁
inst_38 : RingHomInvPair σ₂₁ σ₁₂
R : Type u_22
M : Type u_23
N : Type u_24
inst_39 : CommSemiring R
inst_40 : AddCommMonoid M
inst_41 : AddCommMonoid N
inst_42 : Module R M
inst_43 : Module R N
inst_44 : Small.{u, u_23} M
inst_45 : Small.{u, u_24} N
⊢ Small.{u, max u_24 u_23} (M ⊗[R] N)

Tactic:
⟨_, ⟨(TensorProduct.congr
    (Shrink.linearEquiv R M) (Shrink.linearEquiv R N)).symm.toEquiv⟩⟩

Premises used: LinearEquiv.symm, Small.mk, TensorProduct.congr, Nonempty.intro, LinearEquiv.toEquiv, Exists.intro, Shrink.linearEquiv
-- 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) (TensorProduct.map id f)

Tactic:
rfl

Premises used: LinearMap.lTensor, 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) (TensorProduct.map f id)

Tactic:
rfl

Premises used: 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
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
⊢ Eq (α := N →ₗ[R] M ⊗[R] P) (lTensor M f ∘ₗ (TensorProduct.mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) m)
    ((TensorProduct.mk R M P : (a : M) → P →ₗ[R] M ⊗[R] P) m ∘ₗ f)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.lTensor, List.foldl, TensorProduct.map, Quotient, TensorProduct, TensorProduct.tmul, AddCon.Quotient, TensorProduct.lift, 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
⊢ Eq (α := N →ₗ[R] P ⊗[R] M) (rTensor M f ∘ₗ (flip (TensorProduct.mk R N M) : (a : M) → N →ₗ[R] N ⊗[R] M) m)
    ((flip (TensorProduct.mk R P M) : (a : M) → P →ₗ[R] P ⊗[R] M) m ∘ₗ f)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.map, Quotient, TensorProduct, TensorProduct.tmul, AddCon.Quotient, TensorProduct.lift, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl, LinearMap.rTensor
-- 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 P Q) : P ⊗[R] Q →ₗ[R] Q ⊗[R] P) ∘ₗ
      rTensor Q g ∘ₗ (↑(TensorProduct.comm R Q N) : Q ⊗[R] N →ₗ[R] N ⊗[R] Q))
    (lTensor Q g)

Tactic:
TensorProduct.ext rfl

Premises used: 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 Q P) : Q ⊗[R] P →ₗ[R] P ⊗[R] Q) ∘ₗ
      lTensor Q g ∘ₗ (↑(TensorProduct.comm R N Q) : N ⊗[R] Q →ₗ[R] Q ⊗[R] N))
    (rTensor Q g)

Tactic:
TensorProduct.ext rfl

Premises used: 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
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
⊢ Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ↔
    Function.Injective (α := N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M)

Tactic:
simp [← comm_comp_rTensor_comp_comm_eq]

Premises used: LinearMap.comm_comp_rTensor_comp_comm_eq
-- 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
⊢ Function.Surjective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ↔
    Function.Surjective (α := N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M)

Tactic:
simp [← comm_comp_rTensor_comp_comm_eq]

Premises used: LinearMap.comm_comp_rTensor_comp_comm_eq
-- 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
⊢ Function.Bijective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) ↔
    Function.Bijective (α := N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M)

Tactic:
simp [← comm_comp_rTensor_comp_comm_eq]

Premises used: LinearMap.comm_comp_rTensor_comp_comm_eq
-- 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
S : Type u_22
inst_7 : CommSemiring S
inst_8 : SMul R S
inst_9 : Module S M
inst_10 : IsScalarTower R S M
inst_11 : SMulCommClass R S M
s : S
m : M ⊗[R] N
⊢ HSMul.hSMul (β := M ⊗[R] P) s ((lTensor M f : (a : M ⊗[R] N) → M ⊗[R] P) m : M ⊗[R] P) =
    (lTensor M f : (a : M ⊗[R] N) → M ⊗[R] P) (s • m)

Tactic:
have h : s • (f.lTensor M) = f.lTensor M ∘ₗ (LinearMap.lsmul S (M ⊗[R] N) s).restrictScalars R :=
    TensorProduct.ext rfl
  congrFun (congrArg DFunLike.coe h) m

Premises used: Quotient.liftOn', congrArg, AddCon.liftOn, congrFun, TensorProduct.ext, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g_1 : P →ₗ[R] Q
f_1 f g : N →ₗ[R] P
H :
  ∀ (x : M) (y : N),
    Eq (α := M ⊗[R] P)
      ((((compr₂ₛₗ (TensorProduct.mk R M N) (lTensor M (f + g)) : (a : M) → N →ₗ[R] M ⊗[R] P) x : N →ₗ[R] M ⊗[R] P) :
            (a : N) → M ⊗[R] P)
          y :
        M ⊗[R] P)
      ((((compr₂ₛₗ (TensorProduct.mk R M N) (HAdd.hAdd (α := M ⊗[R] N →ₗ[R] M ⊗[R] P) (lTensor M f) (lTensor M g)) :
                  (a : M) → N →ₗ[R] M ⊗[R] P)
                x :
              N →ₗ[R] M ⊗[R] P) :
            (a : N) → M ⊗[R] P)
          y :
        M ⊗[R] P)
⊢ lTensor M (f + g) = HAdd.hAdd (α := M ⊗[R] N →ₗ[R] M ⊗[R] P) (lTensor M f) (lTensor M g)

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g_1 : P →ₗ[R] Q
f_1 f g : N →ₗ[R] P
x : M
y : N
⊢ Eq (α := M ⊗[R] P)
    ((((compr₂ₛₗ (TensorProduct.mk R M N) (lTensor M (f + g)) : (a : M) → N →ₗ[R] M ⊗[R] P) x : N →ₗ[R] M ⊗[R] P) :
          (a : N) → M ⊗[R] P)
        y :
      M ⊗[R] P)
    ((((compr₂ₛₗ (TensorProduct.mk R M N) (HAdd.hAdd (α := M ⊗[R] N →ₗ[R] M ⊗[R] P) (lTensor M f) (lTensor M g)) :
                (a : M) → N →ₗ[R] M ⊗[R] P)
              x :
            N →ₗ[R] M ⊗[R] P) :
          (a : N) → M ⊗[R] P)
        y :
      M ⊗[R] P)

Tactic:
simp only [compr₂ₛₗ_apply, mk_apply, add_apply, lTensor_tmul, tmul_add]

Premises used: LinearMap.add_apply, TensorProduct.mk_apply, TensorProduct.tmul_add, LinearMap.compr₂ₛₗ_apply, LinearMap.lTensor_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f_1 : N →ₗ[R] P
r : R
f : N →ₗ[R] P
dsimp : lTensor M (r • f) = HSMul.hSMul (β := M ⊗[R] N →ₗ[R] M ⊗[R] P) r (lTensor M f)
⊢ lTensor M (r • f) =
    HSMul.hSMul (α := R) (β := M ⊗[R] N →ₗ[R] M ⊗[R] P) ((RingHom.id R : (a : R) → R) r : R) (lTensor M f)

Tactic:
dsimp