Theorem: Matrix.toUpperTri_add (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 B : Matrix m m ℝ
⊢ (A + B).toUpperTri = A.toUpperTri + B.toUpperTri
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
A B : Matrix m m ℝ
i j : m
⊢ (A + B).toUpperTri i j = (A.toUpperTri + B.toUpperTri) 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
A B : Matrix m m ℝ
i j : m
⊢ (A + B).toUpperTri i j = (A.toUpperTri + B.toUpperTri) i j
Tactic:
rw [Pi.add_apply, Pi.add_apply]
State after:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A B : Matrix m m ℝ
i j : m
⊢ (A + B).toUpperTri i j = A.toUpperTri i j + B.toUpperTri 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
A B : Matrix m m ℝ
i j : m
⊢ (A + B).toUpperTri i j = A.toUpperTri i j + B.toUpperTri i j
Tactic:
simp only [Matrix.toUpperTri]
State after:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A B : Matrix m m ℝ
i j : m
⊢ (if i ≤ j then (A + B) i j else 0) = (if i ≤ j then A i j else 0) + if i ≤ j then B i j else 0

State before:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A B : Matrix m m ℝ
i j : m
⊢ (if i ≤ j then (A + B) i j else 0) = (if i ≤ j then A i j else 0) + if i ≤ j then B i j else 0
Tactic:
by_cases h : i ≤ j <;> simp [h]
State after:
no goals