Theorem: Matrix.toUpperTri_smul (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 = (κ • A).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 : Matrix m m ℝ
κ : ℝ
i j : m
⊢ (κ • A.toUpperTri) i j = (κ • A).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 : Matrix m m ℝ
κ : ℝ
i j : m
⊢ (κ • A.toUpperTri) i j = (κ • A).toUpperTri i j
Tactic:
rw [Pi.smul_apply, Pi.smul_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 : Matrix m m ℝ
κ : ℝ
i j : m
⊢ κ • A.toUpperTri i j = (κ • A).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 : Matrix m m ℝ
κ : ℝ
i j : m
⊢ κ • A.toUpperTri i j = (κ • A).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 : Matrix m m ℝ
κ : ℝ
i j : m
⊢ (κ • if i ≤ j then A i j else 0) = if i ≤ j then (κ • A) 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 : Matrix m m ℝ
κ : ℝ
i j : m
⊢ (κ • if i ≤ j then A i j else 0) = if i ≤ j then (κ • A) i j else 0
Tactic:
by_cases h : i ≤ j <;> simp [h]
State after:
no goals