awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ rTensor M (f + g) = HAdd.hAdd (α := N ⊗[R] M →ₗ[R] P ⊗[R] M) (rTensor M f) (rTensor M g)
have H : ∀ (x : N) (y : M),
  Eq (α := P ⊗[R] M)
    ((((compr₂ₛₗ (TensorProduct.mk R N M) (rTensor M (f + g)) : (a : N) → M →ₗ[R] P ⊗[R] M) x : M →ₗ[R] P ⊗[R] M) :
          (a : M) → P ⊗[R] M)
        y :
      P ⊗[R] M)
    ((((compr₂ₛₗ (TensorProduct.mk R N M) (HAdd.hAdd (α := N ⊗[R] M →ₗ[R] P ⊗[R] M) (rTensor M f) (rTensor M g)) :
                (a : N) → M →ₗ[R] P ⊗[R] M)
              x :
            M →ₗ[R] P ⊗[R] M) :
          (a : M) → P ⊗[R] M)
        y :
      P ⊗[R] M)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ rTensor M (r • f) =
    HSMul.hSMul (α := R) (β := N ⊗[R] M →ₗ[R] P ⊗[R] M) ((RingHom.id R : (a : R) → R) r : R) (rTensor M f)
have dsimp : rTensor M (r • f) = HSMul.hSMul (β := N ⊗[R] M →ₗ[R] P ⊗[R] M) r (rTensor M f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ rTensor M (r • f) = HSMul.hSMul (β := N ⊗[R] M →ₗ[R] P ⊗[R] M) r (rTensor M f)
have H : ∀ (x : N) (y : M),
  Eq (α := P ⊗[R] M)
    ((((compr₂ₛₗ (TensorProduct.mk R N M) (rTensor M (r • f)) : (a : N) → M →ₗ[R] P ⊗[R] M) x : M →ₗ[R] P ⊗[R] M) :
          (a : M) → P ⊗[R] M)
        y :
      P ⊗[R] M)
    ((((compr₂ₛₗ (TensorProduct.mk R N M) (HSMul.hSMul (β := N ⊗[R] M →ₗ[R] P ⊗[R] M) r (rTensor M f)) :
                (a : N) → M →ₗ[R] P ⊗[R] M)
              x :
            M →ₗ[R] P ⊗[R] M) :
          (a : M) → P ⊗[R] M)
        y :
      P ⊗[R] M)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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 (g ∘ₗ f)) (lTensor M g ∘ₗ lTensor M f)
have H : ∀ (m : M) (n : N),
  Eq (α := M ⊗[R] Q)
    ((((compr₂ₛₗ (TensorProduct.mk R M N) (lTensor M (g ∘ₗ f)) : (a : M) → N →ₗ[R] M ⊗[R] Q) m : N →ₗ[R] M ⊗[R] Q) :
          (a : N) → M ⊗[R] Q)
        n :
      M ⊗[R] Q)
    ((((compr₂ₛₗ (TensorProduct.mk R M N) (lTensor M g ∘ₗ lTensor M f) : (a : M) → N →ₗ[R] M ⊗[R] Q) m :
            N →ₗ[R] M ⊗[R] Q) :
          (a : N) → M ⊗[R] Q)
        n :
      M ⊗[R] Q)
Tactic: ext m n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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 (g ∘ₗ f) : (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)
have rw : Eq (α := M ⊗[R] Q)
  (Function.comp (β := M ⊗[R] P) (⇑(lTensor M g) : (a : M ⊗[R] P) → M ⊗[R] Q)
      (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) 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: rw [lTensor_comp, coe_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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 (g ∘ₗ f)) (rTensor M g ∘ₗ rTensor M f)
have H : ∀ (m : N) (n : M),
  Eq (α := Q ⊗[R] M)
    ((((compr₂ₛₗ (TensorProduct.mk R N M) (rTensor M (g ∘ₗ f)) : (a : N) → M →ₗ[R] Q ⊗[R] M) m : M →ₗ[R] Q ⊗[R] M) :
          (a : M) → Q ⊗[R] M)
        n :
      Q ⊗[R] M)
    ((((compr₂ₛₗ (TensorProduct.mk R N M) (rTensor M g ∘ₗ rTensor M f) : (a : N) → M →ₗ[R] Q ⊗[R] M) m :
            M →ₗ[R] Q ⊗[R] M) :
          (a : M) → Q ⊗[R] M)
        n :
      Q ⊗[R] M)
Tactic: ext m n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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 : N ⊗[R] M
⊢ Eq (α := Q ⊗[R] M) ((rTensor M (g ∘ₗ f) : (a : N ⊗[R] M) → Q ⊗[R] M) x : Q ⊗[R] M)
    ((rTensor M g : (a : P ⊗[R] M) → Q ⊗[R] M) ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) x) : Q ⊗[R] M)
have rw : Eq (α := Q ⊗[R] M)
  (Function.comp (β := P ⊗[R] M) (⇑(rTensor M g) : (a : P ⊗[R] M) → Q ⊗[R] M)
      (⇑(rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M) x :
    Q ⊗[R] M)
  ((rTensor M g : (a : P ⊗[R] M) → Q ⊗[R] M) ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) x) : Q ⊗[R] M)
Tactic: rw [rTensor_comp, coe_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ (lTensor M id : (a : M ⊗[R] N) → M ⊗[R] N) x = x
have rw : (id : (a : M ⊗[R] N) → M ⊗[R] N) x = x
Tactic: rw [lTensor_id, id_coe, _root_.id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ (lTensor M id : (a : M ⊗[R] N) → M ⊗[R] N) x = x
have rw₁ : _root_.id x = x
Tactic: rw [lTensor_id, id_coe, _root_.id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ (lTensor M id : (a : M ⊗[R] N) → M ⊗[R] N) x = x
have rw₂ : x = x
Tactic: rw [lTensor_id, id_coe, _root_.id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ (rTensor M id : (a : N ⊗[R] M) → N ⊗[R] M) x = x
have rw : (id : (a : N ⊗[R] M) → N ⊗[R] M) x = x
Tactic: rw [rTensor_id, id_coe, _root_.id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ (rTensor M id : (a : N ⊗[R] M) → N ⊗[R] M) x = x
have rw₁ : _root_.id x = x
Tactic: rw [rTensor_id, id_coe, _root_.id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ (rTensor M id : (a : N ⊗[R] M) → N ⊗[R] M) x = x
have rw₂ : x = x
Tactic: rw [rTensor_id, id_coe, _root_.id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (hypothesis)
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) (rTensor N f) n = rTensor N (f ^ n)
have h : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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)
⊢ HPow.hPow (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (rTensor N f) n = rTensor N (f ^ n)
have 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)
Tactic: rwa [Module.End.id_pow] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (hypothesis)
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) (lTensor M f) n = lTensor M (f ^ n)
have h : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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)
⊢ HPow.hPow (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (lTensor M f) n = lTensor M (f ^ n)
have 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)
Tactic: rwa [Module.End.id_pow] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ (lTensor M (refl R N) : (a : M ⊗[R] N) → M ⊗[R] N) x = x
have rw : (refl R (M ⊗[R] N) : (a : M ⊗[R] N) → M ⊗[R] N) x = x
Tactic: rw [lTensor_refl, refl_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ (lTensor M (refl R N) : (a : M ⊗[R] N) → M ⊗[R] N) x = x
have rw₁ : x = x
Tactic: rw [lTensor_refl, refl_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ (rTensor M (refl R N) : (a : N ⊗[R] M) → N ⊗[R] M) y = y
have rw : (refl R (N ⊗[R] M) : (a : N ⊗[R] M) → N ⊗[R] M) y = y
Tactic: rw [rTensor_refl, refl_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
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
⊢ (rTensor M (refl R N) : (a : N ⊗[R] M) → N ⊗[R] M) y = y
have rw₁ : y = y
Tactic: rw [rTensor_refl, refl_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : Module R A'
inst_4 : Module R B'
eA : A ≃ A'
eB : B ≃ B'
⊢ Eq (α := A ⊗[R] B ≃ₗ[R] B ⊗[R] A) (TensorProduct.comm R A B)
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
      (TensorProduct.comm R A' B' ≪≫ₗ
        TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))))
have h : ∀ (x : A ⊗[R] B),
  Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
            (TensorProduct.comm R A' B' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
          (a : A ⊗[R] B) → B ⊗[R] A)
        x :
      B ⊗[R] A)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : Module R A'
inst_4 : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x : A ⊗[R] B
⊢ Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
            (TensorProduct.comm R A' B' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
          (a : A ⊗[R] B) → B ⊗[R] A)
        x :
      B ⊗[R] A)
have h : Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) 0)
  ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ
          TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
      (a : A ⊗[R] B) → B ⊗[R] A)
    0)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : Module R A'
inst_4 : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x : A ⊗[R] B
h :
  Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) 0)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
          (TensorProduct.comm R A' B' ≪≫ₗ
            TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
        (a : A ⊗[R] B) → B ⊗[R] A)
      0)
⊢ Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
            (TensorProduct.comm R A' B' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
          (a : A ⊗[R] B) → B ⊗[R] A)
        x :
      B ⊗[R] A)
have h₁ : ∀ (x : A) (y : B),
  Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) (x ⊗ₜ[R] y) : B ⊗[R] A)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
            (TensorProduct.comm R A' B' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
          (a : A ⊗[R] B) → B ⊗[R] A)
        (x ⊗ₜ[R] y) :
      B ⊗[R] A)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Map (goal)
Goal:
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : Module R A'
inst_4 : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x : A ⊗[R] B
h :
  Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) 0)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
          (TensorProduct.comm R A' B' ≪≫ₗ
            TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
        (a : A ⊗[R] B) → B ⊗[R] A)
      0)
h₁ :
  ∀ (x : A) (y : B),
    Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) (x ⊗ₜ[R] y) : B ⊗[R] A)
      ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
              (TensorProduct.comm R A' B' ≪≫ₗ
                TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
            (a : A ⊗[R] B) → B ⊗[R] A)
          (x ⊗ₜ[R] y) :
        B ⊗[R] A)
⊢ Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
    ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
            (TensorProduct.comm R A' B' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
          (a : A ⊗[R] B) → B ⊗[R] A)
        x :
      B ⊗[R] A)
have h₂ : ∀ (x y : A ⊗[R] B),
  Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) x : B ⊗[R] A)
      ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
              (TensorProduct.comm R A' B' ≪≫ₗ
                TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
            (a : A ⊗[R] B) → B ⊗[R] A)
          x :
        B ⊗[R] A) →
    Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) y : B ⊗[R] A)
        ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
                (TensorProduct.comm R A' B' ≪≫ₗ
                  TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
              (a : A ⊗[R] B) → B ⊗[R] A)
            y :
          B ⊗[R] A) →
      Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) (x + y) : B ⊗[R] A)
        ((TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
                (TensorProduct.comm R A' B' ≪≫ₗ
                  TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eA))) :
              (a : A ⊗[R] B) → B ⊗[R] A)
            (x + y) :
          B ⊗[R] A)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Matrix (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : Finite ι'
inst_5 : Finite κ'
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup M'
inst_10 : AddCommGroup N'
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R M'
inst_14 : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
⊢ Eq (α := Matrix (ι' × κ') (ι × κ) R)
    (((toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') :
            (M ⊗[R] N →ₗ[R] M' ⊗[R] N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
          (a : M ⊗[R] N →ₗ[R] M' ⊗[R] N') → Matrix (ι' × κ') (ι × κ) R)
        (map f g) :
      Matrix (ι' × κ') (ι × κ) R)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) ((toMatrix bM bM' : (a : M →ₗ[R] M') → Matrix ι' ι R) f)
        ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) g) :
      Matrix (ι' × κ') (ι × κ) R)
have a : ∀ (i : ι') (j : κ') (i' : ι) (j' : κ),
  Eq.{u_1 + 1} (α := R)
    (((toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') :
            (M ⊗[R] N →ₗ[R] M' ⊗[R] N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
          (a : M ⊗[R] N →ₗ[R] M' ⊗[R] N') → Matrix (ι' × κ') (ι × κ) R)
        (map f g) (i, j) (i', j') :
      R)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) ((toMatrix bM bM' : (a : M →ₗ[R] M') → Matrix ι' ι R) f)
        ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) g) (i, j) (i', j') :
      R)
Tactic: ext ⟨i, j⟩ ⟨i', j'⟩