Theorem: Matrix.upperTriangular_toUpperTri (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
A : Matrix m m ℝ
⊢ A.toUpperTri.upperTriangular
Tactic:
intros i j hij
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
i j : m
hij : id j < id i
⊢ A.toUpperTri i j = 0

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
i j : m
hij : id j < id i
⊢ A.toUpperTri i j = 0
Tactic:
unfold toUpperTri
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
i j : m
hij : id j < id i
⊢ (if i ≤ j then A i j else 0) = 0

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
i j : m
hij : id j < id i
⊢ (if i ≤ j then A i j else 0) = 0
Tactic:
rw [if_neg]
State after:
case hnc
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
i j : m
hij : id j < id i
⊢ ¬i ≤ j

State before:
case hnc
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
i j : m
hij : id j < id i
⊢ ¬i ≤ j
Tactic:
simpa using hij
State after:
no goals