mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') i j = fromBlocks (A + A') (B + B') (C + C') (D + D') i j

Tactic:
;

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') i j = fromBlocks (A + A') (B + B') (C + C') (D + D') i j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : MulOneClass R
x : n → R
i✝ : n
j✝ : m
⊢ vecMulVec x 1 i✝ j✝ = replicateCol m x i✝ j✝

Tactic:
;

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : MulOneClass R
x : n → R
i✝ : n
j✝ : m
⊢ vecMulVec x 1 i✝ j✝ = replicateCol m x i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : MulOneClass R
x : n → R
i✝ : m
j✝ : n
⊢ vecMulVec 1 x i✝ j✝ = replicateRow m x i✝ j✝

Tactic:
;

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : MulOneClass R
x : n → R
i✝ : m
j✝ : n
⊢ vecMulVec 1 x i✝ j✝ = replicateRow m x i✝ j✝
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
inst✝² : DecidableEq o
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : o → Matrix m n α
⊢ (blockDiagonal fun k ↦ (M k)ᵀ).map star = blockDiagonal fun k ↦ (M k)ᵀ.map star

Tactic:
rw [blockDiagonal_map _ star (star_zero α)]

Goal state after:
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: F : Type u_1
R✝ : Type u_2
A✝ : Type u_3
B✝ : Type u_4
C : Type u_5
inst✝¹⁸ : Add A✝
inst✝¹⁷ : Add B✝
inst✝¹⁶ : Mul A✝
inst✝¹⁵ : Mul B✝
inst✝¹⁴ : SMul R✝ A✝
inst✝¹³ : SMul R✝ B✝
inst✝¹² : Star A✝
inst✝¹¹ : Star B✝
inst✝¹⁰ : Add C
inst✝⁹ : Mul C
inst✝⁸ : SMul R✝ C
inst✝⁷ : Star C
R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Star A
inst✝ : Star B
f : A ≃⋆ₐ[R] B
r : R
⊢ r • f.toFun 1 = r • 1

Tactic:
;

Goal state after:
F : Type u_1
R✝ : Type u_2
A✝ : Type u_3
B✝ : Type u_4
C : Type u_5
inst✝¹⁸ : Add A✝
inst✝¹⁷ : Add B✝
inst✝¹⁶ : Mul A✝
inst✝¹⁵ : Mul B✝
inst✝¹⁴ : SMul R✝ A✝
inst✝¹³ : SMul R✝ B✝
inst✝¹² : Star A✝
inst✝¹¹ : Star B✝
inst✝¹⁰ : Add C
inst✝⁹ : Mul C
inst✝⁸ : SMul R✝ C
inst✝⁷ : Star C
R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Star A
inst✝ : Star B
f : A ≃⋆ₐ[R] B
r : R
⊢ r • f.toFun 1 = r • 1
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : Monoid R
inst✝¹⁷ : NonUnitalNonAssocSemiring A₁
inst✝¹⁶ : DistribMulAction R A₁
inst✝¹⁵ : Star A₁
inst✝¹⁴ : NonUnitalNonAssocSemiring A₂
inst✝¹³ : DistribMulAction R A₂
inst✝¹² : Star A₂
inst✝¹¹ : NonUnitalNonAssocSemiring A₃
inst✝¹⁰ : DistribMulAction R A₃
inst✝⁹ : Star A₃
inst✝⁸ : NonUnitalNonAssocSemiring A₁'
inst✝⁷ : DistribMulAction R A₁'
inst✝⁶ : Star A₁'
inst✝⁵ : NonUnitalNonAssocSemiring A₂'
inst✝⁴ : DistribMulAction R A₂'
inst✝³ : Star A₂'
inst✝² : NonUnitalNonAssocSemiring A₃'
inst✝¹ : DistribMulAction R A₃'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁ →⋆ₙₐ[R] A₂
x✝ : A₁
⊢ ((fun f ↦ (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom)
        ((fun f ↦ (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom) f))
      x✝ =
    f x✝

Tactic:
;

Goal state after:
R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : Monoid R
inst✝¹⁷ : NonUnitalNonAssocSemiring A₁
inst✝¹⁶ : DistribMulAction R A₁
inst✝¹⁵ : Star A₁
inst✝¹⁴ : NonUnitalNonAssocSemiring A₂
inst✝¹³ : DistribMulAction R A₂
inst✝¹² : Star A₂
inst✝¹¹ : NonUnitalNonAssocSemiring A₃
inst✝¹⁰ : DistribMulAction R A₃
inst✝⁹ : Star A₃
inst✝⁸ : NonUnitalNonAssocSemiring A₁'
inst✝⁷ : DistribMulAction R A₁'
inst✝⁶ : Star A₁'
inst✝⁵ : NonUnitalNonAssocSemiring A₂'
inst✝⁴ : DistribMulAction R A₂'
inst✝³ : Star A₂'
inst✝² : NonUnitalNonAssocSemiring A₃'
inst✝¹ : DistribMulAction R A₃'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁ →⋆ₙₐ[R] A₂
x✝ : A₁
⊢ ((fun f ↦ (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom)
        ((fun f ↦ (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom) f))
      x✝ =
    f x✝
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : Monoid R
inst✝¹⁷ : NonUnitalNonAssocSemiring A₁
inst✝¹⁶ : DistribMulAction R A₁
inst✝¹⁵ : Star A₁
inst✝¹⁴ : NonUnitalNonAssocSemiring A₂
inst✝¹³ : DistribMulAction R A₂
inst✝¹² : Star A₂
inst✝¹¹ : NonUnitalNonAssocSemiring A₃
inst✝¹⁰ : DistribMulAction R A₃
inst✝⁹ : Star A₃
inst✝⁸ : NonUnitalNonAssocSemiring A₁'
inst✝⁷ : DistribMulAction R A₁'
inst✝⁶ : Star A₁'
inst✝⁵ : NonUnitalNonAssocSemiring A₂'
inst✝⁴ : DistribMulAction R A₂'
inst✝³ : Star A₂'
inst✝² : NonUnitalNonAssocSemiring A₃'
inst✝¹ : DistribMulAction R A₃'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁' →⋆ₙₐ[R] A₂'
x✝ : A₁'
⊢ ((fun f ↦ (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom)
        ((fun f ↦ (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom) f))
      x✝ =
    f x✝

Tactic:
;

Goal state after:
R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : Monoid R
inst✝¹⁷ : NonUnitalNonAssocSemiring A₁
inst✝¹⁶ : DistribMulAction R A₁
inst✝¹⁵ : Star A₁
inst✝¹⁴ : NonUnitalNonAssocSemiring A₂
inst✝¹³ : DistribMulAction R A₂
inst✝¹² : Star A₂
inst✝¹¹ : NonUnitalNonAssocSemiring A₃
inst✝¹⁰ : DistribMulAction R A₃
inst✝⁹ : Star A₃
inst✝⁸ : NonUnitalNonAssocSemiring A₁'
inst✝⁷ : DistribMulAction R A₁'
inst✝⁶ : Star A₁'
inst✝⁵ : NonUnitalNonAssocSemiring A₂'
inst✝⁴ : DistribMulAction R A₂'
inst✝³ : Star A₂'
inst✝² : NonUnitalNonAssocSemiring A₃'
inst✝¹ : DistribMulAction R A₃'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁' →⋆ₙₐ[R] A₂'
x✝ : A₁'
⊢ ((fun f ↦ (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom)
        ((fun f ↦ (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom) f))
      x✝ =
    f x✝
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Semiring A₁
inst✝¹⁶ : Semiring A₂
inst✝¹⁵ : Semiring A₃
inst✝¹⁴ : Semiring A₁'
inst✝¹³ : Semiring A₂'
inst✝¹² : Semiring A₃'
inst✝¹¹ : Algebra R A₁
inst✝¹⁰ : Algebra R A₂
inst✝⁹ : Algebra R A₃
inst✝⁸ : Algebra R A₁'
inst✝⁷ : Algebra R A₂'
inst✝⁶ : Algebra R A₃'
inst✝⁵ : Star A₁
inst✝⁴ : Star A₂
inst✝³ : Star A₃
inst✝² : Star A₁'
inst✝¹ : Star A₂'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁ →⋆ₐ[R] A₂
x✝ : A₁
⊢ ((fun f ↦ (e₂.symm.toStarAlgHom.comp f).comp e₁.toStarAlgHom)
        ((fun f ↦ (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom) f))
      x✝ =
    f x✝

Tactic:
;

Goal state after:
R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Semiring A₁
inst✝¹⁶ : Semiring A₂
inst✝¹⁵ : Semiring A₃
inst✝¹⁴ : Semiring A₁'
inst✝¹³ : Semiring A₂'
inst✝¹² : Semiring A₃'
inst✝¹¹ : Algebra R A₁
inst✝¹⁰ : Algebra R A₂
inst✝⁹ : Algebra R A₃
inst✝⁸ : Algebra R A₁'
inst✝⁷ : Algebra R A₂'
inst✝⁶ : Algebra R A₃'
inst✝⁵ : Star A₁
inst✝⁴ : Star A₂
inst✝³ : Star A₃
inst✝² : Star A₁'
inst✝¹ : Star A₂'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁ →⋆ₐ[R] A₂
x✝ : A₁
⊢ ((fun f ↦ (e₂.symm.toStarAlgHom.comp f).comp e₁.toStarAlgHom)
        ((fun f ↦ (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom) f))
      x✝ =
    f x✝
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Semiring A₁
inst✝¹⁶ : Semiring A₂
inst✝¹⁵ : Semiring A₃
inst✝¹⁴ : Semiring A₁'
inst✝¹³ : Semiring A₂'
inst✝¹² : Semiring A₃'
inst✝¹¹ : Algebra R A₁
inst✝¹⁰ : Algebra R A₂
inst✝⁹ : Algebra R A₃
inst✝⁸ : Algebra R A₁'
inst✝⁷ : Algebra R A₂'
inst✝⁶ : Algebra R A₃'
inst✝⁵ : Star A₁
inst✝⁴ : Star A₂
inst✝³ : Star A₃
inst✝² : Star A₁'
inst✝¹ : Star A₂'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁' →⋆ₐ[R] A₂'
x✝ : A₁'
⊢ ((fun f ↦ (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom)
        ((fun f ↦ (e₂.symm.toStarAlgHom.comp f).comp e₁.toStarAlgHom) f))
      x✝ =
    f x✝

Tactic:
;

Goal state after:
R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Semiring A₁
inst✝¹⁶ : Semiring A₂
inst✝¹⁵ : Semiring A₃
inst✝¹⁴ : Semiring A₁'
inst✝¹³ : Semiring A₂'
inst✝¹² : Semiring A₃'
inst✝¹¹ : Algebra R A₁
inst✝¹⁰ : Algebra R A₂
inst✝⁹ : Algebra R A₃
inst✝⁸ : Algebra R A₁'
inst✝⁷ : Algebra R A₂'
inst✝⁶ : Algebra R A₃'
inst✝⁵ : Star A₁
inst✝⁴ : Star A₂
inst✝³ : Star A₃
inst✝² : Star A₁'
inst✝¹ : Star A₂'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁' →⋆ₐ[R] A₂'
x✝ : A₁'
⊢ ((fun f ↦ (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom)
        ((fun f ↦ (e₂.symm.toStarAlgHom.comp f).comp e₁.toStarAlgHom) f))
      x✝ =
    f x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ ((curry
          ((curry
              (lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))) ∘ₗ
                lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q))))
            x✝²))
        x✝¹)
      x✝ =
    ((curry ((curry LinearMap.id) x✝²)) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ ((curry
          ((curry
              (lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))) ∘ₗ
                lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q))))
            x✝²))
        x✝¹)
      x✝ =
    ((curry ((curry LinearMap.id) x✝²)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ (((curry
            (curry
              (lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q)) ∘ₗ
                lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))))))
          x✝²)
        x✝¹)
      x✝ =
    (((curry (curry LinearMap.id)) x✝²) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ (((curry
            (curry
              (lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q)) ∘ₗ
                lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))))))
          x✝²)
        x✝¹)
      x✝ =
    (((curry (curry LinearMap.id)) x✝²) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
Q : Type uQ
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : IsScalarTower R B M
inst✝⁶ : SMulCommClass A B M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
f : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry ((curry ((lTensor B M) f ∘ₗ ↑(cancelBaseChange R A B M N))) x✝¹)) 1) x✝ =
    ((curry ((curry (↑(cancelBaseChange R A B M Q) ∘ₗ (lTensor B M) ((lTensor A A) f))) x✝¹)) 1) x✝

Tactic:
;

Goal state after:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
Q : Type uQ
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : IsScalarTower R B M
inst✝⁶ : SMulCommClass A B M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
f : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry ((curry ((lTensor B M) f ∘ₗ ↑(cancelBaseChange R A B M N))) x✝¹)) 1) x✝ =
    ((curry ((curry (↑(cancelBaseChange R A B M Q) ∘ₗ (lTensor B M) ((lTensor A A) f))) x✝¹)) 1) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring A
inst✝²⁴ : Semiring B
inst✝²³ : Algebra R A
inst✝²² : Algebra R B
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
inst✝¹⁹ : Module A M
inst✝¹⁸ : Module B M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : IsScalarTower R B M
inst✝¹⁵ : SMulCommClass A B M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R N
inst✝¹² : AddCommMonoid P
inst✝¹¹ : Module A P
inst✝¹⁰ : AddCommMonoid P'
inst✝⁹ : Module A P'
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
x✝² : M
x✝¹ : Q
x✝ : P
⊢ (((curry
            (curry
              (lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))) ∘ₗ
                lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))))))
          x✝²)
        x✝¹)
      x✝ =
    (((curry (curry LinearMap.id)) x✝²) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring A
inst✝²⁴ : Semiring B
inst✝²³ : Algebra R A
inst✝²² : Algebra R B
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
inst✝¹⁹ : Module A M
inst✝¹⁸ : Module B M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : IsScalarTower R B M
inst✝¹⁵ : SMulCommClass A B M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R N
inst✝¹² : AddCommMonoid P
inst✝¹¹ : Module A P
inst✝¹⁰ : AddCommMonoid P'
inst✝⁹ : Module A P'
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
x✝² : M
x✝¹ : Q
x✝ : P
⊢ (((curry
            (curry
              (lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))) ∘ₗ
                lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))))))
          x✝²)
        x✝¹)
      x✝ =
    (((curry (curry LinearMap.id)) x✝²) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring A
inst✝²⁴ : Semiring B
inst✝²³ : Algebra R A
inst✝²² : Algebra R B
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
inst✝¹⁹ : Module A M
inst✝¹⁸ : Module B M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : IsScalarTower R B M
inst✝¹⁵ : SMulCommClass A B M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R N
inst✝¹² : AddCommMonoid P
inst✝¹¹ : Module A P
inst✝¹⁰ : AddCommMonoid P'
inst✝⁹ : Module A P'
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ (((curry
            (curry
              (lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))) ∘ₗ
                lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))))))
          x✝²)
        x✝¹)
      x✝ =
    (((curry (curry LinearMap.id)) x✝²) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring A
inst✝²⁴ : Semiring B
inst✝²³ : Algebra R A
inst✝²² : Algebra R B
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
inst✝¹⁹ : Module A M
inst✝¹⁸ : Module B M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : IsScalarTower R B M
inst✝¹⁵ : SMulCommClass A B M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R N
inst✝¹² : AddCommMonoid P
inst✝¹¹ : Module A P
inst✝¹⁰ : AddCommMonoid P'
inst✝⁹ : Module A P'
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ (((curry
            (curry
              (lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))) ∘ₗ
                lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))))))
          x✝²)
        x✝¹)
      x✝ =
    (((curry (curry LinearMap.id)) x✝²) x✝¹) x✝