Theorem: Matrix.toUpperTri_zero (CvxLean/Lib/Math/LinearAlgebra/Matrix/ToUpperTri.lean)

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
⊢ toUpperTri 0 = 0
Tactic:
funext i j
State after:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
i j : m
⊢ toUpperTri 0 i j = 0 i j

State before:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
i j : m
⊢ toUpperTri 0 i j = 0 i j
Tactic:
simp [Matrix.toUpperTri]
State after:
no goals