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

State before:
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
⊢ A.toUpperTri = A
Tactic:
ext i j
State after:
case a
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
⊢ A.toUpperTri i j = A i j

State before:
case a
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
⊢ A.toUpperTri i j = A i j
Tactic:
by_cases h : i ≤ j
State after:
case pos
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
h : i ≤ j
⊢ A.toUpperTri i j = A i j

case neg
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
h : ¬i ≤ j
⊢ A.toUpperTri i j = A i j

State before:
case pos
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
h : i ≤ j
⊢ A.toUpperTri i j = A i j

case neg
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
h : ¬i ≤ j
⊢ A.toUpperTri i j = A i j
Tactic:
simp [toUpperTri, h]
State after:
case neg
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
h : ¬i ≤ j
⊢ A.toUpperTri i j = A i j

State before:
case neg
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
h : ¬i ≤ j
⊢ A.toUpperTri i j = A i j
Tactic:
simp [toUpperTri, h, hA (lt_of_not_ge h)]
State after:
no goals