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
H :
  ∀ (x : M) (x_1 : N),
    Eq (α := M ⊗[R] N)
      ((((compr₂ₛₗ (mk R M N) (map LinearMap.id LinearMap.id) : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
            (a : N) → M ⊗[R] N)
          x_1 :
        M ⊗[R] N)
      ((((compr₂ₛₗ (mk R M N) LinearMap.id : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) : (a : N) → M ⊗[R] N)
          x_1 :
        M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (map LinearMap.id LinearMap.id) LinearMap.id

Tactic:
ext
-- 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
x_1 : N
⊢ Eq (α := M ⊗[R] N)
    ((((compr₂ₛₗ (mk R M N) (map LinearMap.id LinearMap.id) : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) :
          (a : N) → M ⊗[R] N)
        x_1 :
      M ⊗[R] N)
    ((((compr₂ₛₗ (mk R M N) LinearMap.id : (a : M) → N →ₗ[R] M ⊗[R] N) x : N →ₗ[R] M ⊗[R] N) : (a : N) → M ⊗[R] N) x_1 :
      M ⊗[R] N)

Tactic:
simp only [mk_apply, id_coe, compr₂ₛₗ_apply, _root_.id, map_tmul]

Premises used: LinearMap.id_coe, TensorProduct.mk_apply, id, TensorProduct.map_tmul, LinearMap.compr₂ₛₗ_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 (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (map 1 1) 1

Tactic:
map_id

Premises used: 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
f₁ f₂ : M →ₗ[R] M
g₁ g₂ : N →ₗ[R] N
⊢ map (f₁ * f₂) (g₁ * g₂) = map f₁ g₁ * map f₂ g₂

Tactic:
map_comp ..

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

Tactic:
simp only [pow_zero, TensorProduct.map_one]

Premises used: pow_zero, TensorProduct.map_one
-- 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 : map f g ^ n = map (f ^ n) (g ^ n)
⊢ map f g ^ (n + 1) = map (f ^ (n + 1)) (g ^ (n + 1))

Tactic:
simp only [pow_succ', ih, TensorProduct.map_mul]

Premises used: TensorProduct.map_mul, pow_succ'
-- 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 (β := ℕ) (map f g) 0 = map (HPow.hPow (β := ℕ) f 0) (HPow.hPow (β := ℕ) g 0)
succ : ∀ (n : ℕ) (ih : map f g ^ n = map (f ^ n) (g ^ n)), map f g ^ (n + 1) = map (f ^ (n + 1)) (g ^ (n + 1))
⊢ map f g ^ n = map (f ^ n) (g ^ n)

Tactic:
induction n with
  | zero => simp only [pow_zero, TensorProduct.map_one]
  | succ n ih => simp only [pow_succ', ih, TensorProduct.map_mul]

Premises used: pow_zero, TensorProduct.map_one, TensorProduct.map_mul, pow_succ'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
f₁ f₂ : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
H :
  ∀ (x : M) (x_1 : N),
    Eq (α := M₂ ⊗[R₂] N₂)
      ((((compr₂ₛₗ (mk R M N) (map (f₁ + f₂) g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
            (a : N) → M₂ ⊗[R₂] N₂)
          x_1 :
        M₂ ⊗[R₂] N₂)
      ((((compr₂ₛₗ (mk R M N) (map f₁ g + map f₂ g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
            (a : N) → M₂ ⊗[R₂] N₂)
          x_1 :
        M₂ ⊗[R₂] N₂)
⊢ map (f₁ + f₂) g = map f₁ g + map f₂ g

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
f₁ f₂ : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
x : M
x_1 : N
⊢ Eq (α := M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (map (f₁ + f₂) g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (map f₁ g + map f₂ g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)

Tactic:
simp only [add_tmul, compr₂ₛₗ_apply, mk_apply, map_tmul, add_apply]

Premises used: LinearMap.add_apply, TensorProduct.mk_apply, TensorProduct.map_tmul, TensorProduct.add_tmul, LinearMap.compr₂ₛₗ_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
f : M →ₛₗ[σ₁₂] M₂
g₁ g₂ : N →ₛₗ[σ₁₂] N₂
H :
  ∀ (x : M) (x_1 : N),
    Eq (α := M₂ ⊗[R₂] N₂)
      ((((compr₂ₛₗ (mk R M N) (map f (g₁ + g₂)) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
            (a : N) → M₂ ⊗[R₂] N₂)
          x_1 :
        M₂ ⊗[R₂] N₂)
      ((((compr₂ₛₗ (mk R M N) (map f g₁ + map f g₂) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
            (a : N) → M₂ ⊗[R₂] N₂)
          x_1 :
        M₂ ⊗[R₂] N₂)
⊢ map f (g₁ + g₂) = map f g₁ + map f g₂

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
f : M →ₛₗ[σ₁₂] M₂
g₁ g₂ : N →ₛₗ[σ₁₂] N₂
x : M
x_1 : N
⊢ Eq (α := M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (map f (g₁ + g₂)) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (map f g₁ + map f g₂) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)

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

Premises used: LinearMap.add_apply, TensorProduct.mk_apply, TensorProduct.map_tmul, TensorProduct.tmul_add, LinearMap.compr₂ₛₗ_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
r : R₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
H :
  ∀ (x : M) (x_1 : N),
    Eq (α := M₂ ⊗[R₂] N₂)
      ((((compr₂ₛₗ (mk R M N) (map (r • f) g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
            (a : N) → M₂ ⊗[R₂] N₂)
          x_1 :
        M₂ ⊗[R₂] N₂)
      ((((compr₂ₛₗ (mk R M N) (r • map f g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
            (a : N) → M₂ ⊗[R₂] N₂)
          x_1 :
        M₂ ⊗[R₂] N₂)
⊢ map (r • f) g = r • map f g

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
r : R₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
x : M
x_1 : N
⊢ Eq (α := M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (map (r • f) g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (r • map f g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)

Tactic:
simp only [smul_tmul, compr₂ₛₗ_apply, mk_apply, map_tmul, smul_apply, tmul_smul]

Premises used: TensorProduct.smul_tmul, LinearMap.smul_apply, TensorProduct.mk_apply, TensorProduct.tmul_smul, TensorProduct.map_tmul, LinearMap.compr₂ₛₗ_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
r : R₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
H :
  ∀ (x : M) (x_1 : N),
    Eq (α := M₂ ⊗[R₂] N₂)
      ((((compr₂ₛₗ (mk R M N) (map f (r • g)) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
            (a : N) → M₂ ⊗[R₂] N₂)
          x_1 :
        M₂ ⊗[R₂] N₂)
      ((((compr₂ₛₗ (mk R M N) (r • map f g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
            (a : N) → M₂ ⊗[R₂] N₂)
          x_1 :
        M₂ ⊗[R₂] N₂)
⊢ map f (r • g) = r • map f g

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
r : R₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
x : M
x_1 : N
⊢ Eq (α := M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (map f (r • g)) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)
    ((((compr₂ₛₗ (mk R M N) (r • map f g) : (a : M) → N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) x : N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : N) → M₂ ⊗[R₂] N₂)
        x_1 :
      M₂ ⊗[R₂] N₂)

Tactic:
simp only [compr₂ₛₗ_apply, mk_apply, map_tmul, smul_apply, tmul_smul]

Premises used: LinearMap.smul_apply, TensorProduct.mk_apply, TensorProduct.tmul_smul, TensorProduct.map_tmul, LinearMap.compr₂ₛₗ_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
⊢ (((mapBilinear σ₁₂ M N M₂ N₂ : (a : M →ₛₗ[σ₁₂] M₂) → (N →ₛₗ[σ₁₂] N₂) →ₗ[R₂] M ⊗[R] N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) f :
          (N →ₛₗ[σ₁₂] N₂) →ₗ[R₂] M ⊗[R] N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
        (a : N →ₛₗ[σ₁₂] N₂) → M ⊗[R] N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂)
      g =
    map f g

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
P : Type u_9
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₂
inst_5 : Module R₂ M₂
inst_6 : Module R₂ N₂
inst_7 : Module R P
m₂ : M₂
f : P →ₛₗ[σ₁₂] N₂
p : P
⊢ Eq (α := M₂ ⊗[R₂] N₂)
    ((((lTensorHomToHomLTensor σ₁₂ P M₂ N₂ : (a : M₂ ⊗[R₂] (P →ₛₗ[σ₁₂] N₂)) → P →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) (m₂ ⊗ₜ[R₂] f) :
            P →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : P) → M₂ ⊗[R₂] N₂)
        p :
      M₂ ⊗[R₂] N₂)
    (m₂ ⊗ₜ[R₂] (f : (a : P) → N₂) p : M₂ ⊗[R₂] N₂)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
P : Type u_9
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₂
inst_5 : Module R₂ M₂
inst_6 : Module R₂ N₂
inst_7 : Module R P
f : P →ₛₗ[σ₁₂] M₂
n₂ : N₂
p : P
⊢ Eq (α := M₂ ⊗[R₂] N₂)
    ((((rTensorHomToHomRTensor σ₁₂ P M₂ N₂ : (a : (P →ₛₗ[σ₁₂] M₂) ⊗[R₂] N₂) → P →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) (f ⊗ₜ[R₂] n₂) :
            P →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) :
          (a : P) → M₂ ⊗[R₂] N₂)
        p :
      M₂ ⊗[R₂] N₂)
    ((f : (a : P) → M₂) p ⊗ₜ[R₂] n₂ : M₂ ⊗[R₂] N₂)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
⊢ (homTensorHomMap σ₁₂ M N M₂ N₂ : (a : (M →ₛₗ[σ₁₂] M₂) ⊗[R₂] (N →ₛₗ[σ₁₂] N₂)) → M ⊗[R] N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂)
      (f ⊗ₜ[R₂] g) =
    map f g

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.map, TensorProduct.lift, FreeAddMonoid.sumAux, rfl
-- 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₃
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₃
f : M →ₛₗ[σ₁₃] M₂ →ₛₗ[σ₂₃] M₃
g : N →ₛₗ[σ₁₃] N₂ →ₛₗ[σ₂₃] N₃
m : M
n : N
⊢ Eq (α := M₂ ⊗[R₂] N₂ →ₛₗ[σ₂₃] M₃ ⊗[R₃] N₃)
    ((map₂ f g : (a : M ⊗[R] N) → M₂ ⊗[R₂] N₂ →ₛₗ[σ₂₃] M₃ ⊗[R₃] N₃) (m ⊗ₜ[R] n) : M₂ ⊗[R₂] N₂ →ₛₗ[σ₂₃] M₃ ⊗[R₃] N₃)
    (map ((f : (a : M) → M₂ →ₛₗ[σ₂₃] M₃) m) ((g : (a : N) → N₂ →ₛₗ[σ₂₃] N₃) n) : M₂ ⊗[R₂] N₂ →ₛₗ[σ₂₃] M₃ ⊗[R₃] N₃)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.map, TensorProduct.lift, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
g : N →ₛₗ[σ₁₂] N₂
⊢ Eq (α := M ⊗[R] N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) (map 0 g) 0

Tactic:
(mapBilinear _ M N M₂ N₂).map_zero₂ _

Premises used: TensorProduct.map, TensorProduct.mapBilinear, LinearMap.map_zero₂, TensorProduct.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
f : M →ₛₗ[σ₁₂] M₂
⊢ Eq (α := M ⊗[R] N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) (map f 0) 0

Tactic:
(mapBilinear _ M N M₂ N₂ f).map_zero

Premises used: LinearMap.map_zero, TensorProduct.map, TensorProduct.mapBilinear, TensorProduct.lift, DFunLike.coe
-- 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
σ₂₁ : R₂ →+* R
inst_37 : RingHomInvPair σ₁₂ σ₂₁
inst_38 : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] M₂
g : N ≃ₛₗ[σ₁₂] N₂
m : M₂
n : N₂
⊢ Eq (α := M₂ ⊗[R₂] N₂)
    ((map (↑f : M →ₛₗ[σ₁₂] M₂) (↑g : N →ₛₗ[σ₁₂] N₂) ∘ₛₗ map (↑f.symm : M₂ →ₛₗ[σ₂₁] M) (↑g.symm : N₂ →ₛₗ[σ₂₁] N) :
          (a : M₂ ⊗[R₂] N₂) → M₂ ⊗[R₂] N₂)
        (m ⊗ₜ[R₂] n) :
      M₂ ⊗[R₂] N₂)
    ((LinearMap.id : (a : M₂ ⊗[R₂] N₂) → M₂ ⊗[R₂] N₂) (m ⊗ₜ[R₂] n) : M₂ ⊗[R₂] N₂)

Tactic:
simp
-- 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
σ₂₁ : R₂ →+* R
inst_37 : RingHomInvPair σ₁₂ σ₂₁
inst_38 : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] M₂
g : N ≃ₛₗ[σ₁₂] N₂
m : M
n : N
⊢ Eq (α := M ⊗[R] N)
    ((map (↑f.symm : M₂ →ₛₗ[σ₂₁] M) (↑g.symm : N₂ →ₛₗ[σ₂₁] N) ∘ₛₗ map (↑f : M →ₛₗ[σ₁₂] M₂) (↑g : N →ₛₗ[σ₁₂] N₂) :
          (a : M ⊗[R] N) → M ⊗[R] N)
        (m ⊗ₜ[R] n) :
      M ⊗[R] N)
    ((LinearMap.id : (a : M ⊗[R] N) → M ⊗[R] N) (m ⊗ₜ[R] n) : M ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] M₂
g : N ≃ₛₗ[σ₁₂] N₂
⊢ (↑(congr f g) : M ⊗[R] N →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂) = map (↑f : M →ₛₗ[σ₁₂] M₂) (↑g : N →ₛₗ[σ₁₂] N₂)

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] M₂
g : N ≃ₛₗ[σ₁₂] N₂
m : M
n : N
⊢ Eq (α := M₂ ⊗[R₂] N₂) ((congr f g : (a : M ⊗[R] N) → M₂ ⊗[R₂] N₂) (m ⊗ₜ[R] n) : M₂ ⊗[R₂] N₂)
    ((f : (a : M) → M₂) m ⊗ₜ[R₂] (g : (a : N) → N₂) 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.Map
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
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] M₂
g : N ≃ₛₗ[σ₁₂] N₂
p : M₂
q : N₂
⊢ Eq (α := M ⊗[R] N) (((congr f g).symm : (a : M₂ ⊗[R₂] N₂) → M ⊗[R] N) (p ⊗ₜ[R₂] q) : M ⊗[R] N)
    ((f.symm : (a : M₂) → M) p ⊗ₜ[R] (g.symm : (a : N₂) → N) q : 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
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] M₂
g : N ≃ₛₗ[σ₁₂] N₂
⊢ (congr f g).symm = congr f.symm g.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, TensorProduct.congr, 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
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) (congr (LinearEquiv.refl R M) (LinearEquiv.refl R N))
    (LinearEquiv.refl R (M ⊗[R] N))

Tactic:
LinearEquiv.toLinearMap_injective <| ext' fun _ _ ↦ rfl

Premises used: LinearEquiv.toLinearMap_injective, TensorProduct.ext', rfl