case mk
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
⊢ toMatrix (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }) =
    fromBlocks (toMatrix { i := i✝, j := j✝, hij := hij✝, c := c✝ }) 0 0 1
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j : n
t : TransvectionStruct n R
⊢ toMatrix (sumInl p t) = fromBlocks (toMatrix t) 0 0 1
cases t
case mk.a.h
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : n ⊕ p
⊢ toMatrix (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }) a b =
    fromBlocks (toMatrix { i := i✝, j := j✝, hij := hij✝, c := c✝ }) 0 0 1 a b
case mk
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
⊢ toMatrix (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }) =
    fromBlocks (toMatrix { i := i✝, j := j✝, hij := hij✝, c := c✝ }) 0 0 1
ext (a b)
case mk.a.h.inl.inl
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : n
⊢ toMatrix (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }) (inl a) (inl b) =
    fromBlocks (toMatrix { i := i✝, j := j✝, hij := hij✝, c := c✝ }) 0 0 1 (inl a) (inl b)

case mk.a.h.inl.inr
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a : n
b : p
⊢ toMatrix (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }) (inl a) (inr b) =
    fromBlocks (toMatrix { i := i✝, j := j✝, hij := hij✝, c := c✝ }) 0 0 1 (inl a) (inr b)

case mk.a.h.inr.inl
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a : p
b : n
⊢ toMatrix (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }) (inr a) (inl b) =
    fromBlocks (toMatrix { i := i✝, j := j✝, hij := hij✝, c := c✝ }) 0 0 1 (inr a) (inl b)

case mk.a.h.inr.inr
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
⊢ toMatrix (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }) (inr a) (inr b) =
    fromBlocks (toMatrix { i := i✝, j := j✝, hij := hij✝, c := c✝ }) 0 0 1 (inr a) (inr b)
case mk.a.h
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : n ⊕ p
⊢ toMatrix (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }) a b =
    fromBlocks (toMatrix { i := i✝, j := j✝, hij := hij✝, c := c✝ }) 0 0 1 a b
cases' a with a a <;> cases' b with b b
no goals
case mk.a.h.inl.inl
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : n
⊢ toMatrix (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }) (inl a) (inl b) =
    fromBlocks (toMatrix { i := i✝, j := j✝, hij := hij✝, c := c✝ }) 0 0 1 (inl a) (inl b)
by_cases h : a = b <;> simp [TransvectionStruct.sumInl, transvection, h, stdBasisMatrix]
no goals
case mk.a.h.inl.inr
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a : n
b : p
⊢ toMatrix (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }) (inl a) (inr b) =
    fromBlocks (toMatrix { i := i✝, j := j✝, hij := hij✝, c := c✝ }) 0 0 1 (inl a) (inr b)
simp [TransvectionStruct.sumInl, transvection]
no goals
case mk.a.h.inr.inl
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a : p
b : n
⊢ toMatrix (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }) (inr a) (inl b) =
    fromBlocks (toMatrix { i := i✝, j := j✝, hij := hij✝, c := c✝ }) 0 0 1 (inr a) (inl b)
simp [TransvectionStruct.sumInl, transvection]
no goals
case mk.a.h.inr.inr
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.48673
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
⊢ toMatrix (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }) (inr a) (inr b) =
    fromBlocks (toMatrix { i := i✝, j := j✝, hij := hij✝, c := c✝ }) 0 0 1 (inr a) (inr b)
by_cases h : a = b <;> simp [TransvectionStruct.sumInl, transvection, h]