Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i j : n
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) (Sum.inl i) (Sum.inl j) =
    fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂) (Sum.inl i) (Sum.inl j)

pp: case inl.inr
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i : n
j : m
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) (Sum.inl i) (Sum.inr j) =
    fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂) (Sum.inl i) (Sum.inr j)

pp: case inr.inl
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i : m
j : n
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) (Sum.inr i) (Sum.inl j) =
    fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂) (Sum.inr i) (Sum.inl j)

pp: case inr.inr
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i j : m
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) (Sum.inr i) (Sum.inr j) =
    fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂) (Sum.inr i) (Sum.inr j)

Tactic:
<;>

Goal state after:
case inl.inl
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i j : n
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) (Sum.inl i) (Sum.inl j) =
    fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂) (Sum.inl i) (Sum.inl j)

case inl.inr
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i : n
j : m
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) (Sum.inl i) (Sum.inr j) =
    fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂) (Sum.inl i) (Sum.inr j)

case inr.inl
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i : m
j : n
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) (Sum.inr i) (Sum.inl j) =
    fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂) (Sum.inr i) (Sum.inl j)

case inr.inr
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i j : m
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) (Sum.inr i) (Sum.inr j) =
    fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂) (Sum.inr i) (Sum.inr j)