case mk
n : Type u_1
p : Type ?u.32998
R : Type u₂
𝕜 : Type ?u.33003
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
i✝ j✝ : n
t_hij : i✝ ≠ j✝
c✝ : R
⊢ toMatrix (TransvectionStruct.inv { i := i✝, j := j✝, hij := t_hij, c := c✝ }) ⬝
      toMatrix { i := i✝, j := j✝, hij := t_hij, c := c✝ } =
    1
n : Type u_1
p : Type ?u.32998
R : Type u₂
𝕜 : Type ?u.33003
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
t : TransvectionStruct n R
⊢ toMatrix (TransvectionStruct.inv t) ⬝ toMatrix t = 1
rcases t with ⟨_, _, t_hij⟩
no goals
case mk
n : Type u_1
p : Type ?u.32998
R : Type u₂
𝕜 : Type ?u.33003
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
i✝ j✝ : n
t_hij : i✝ ≠ j✝
c✝ : R
⊢ toMatrix (TransvectionStruct.inv { i := i✝, j := j✝, hij := t_hij, c := c✝ }) ⬝
      toMatrix { i := i✝, j := j✝, hij := t_hij, c := c✝ } =
    1
simp [toMatrix, transvection_mul_transvection_same, t_hij]