Theorem: Matrix.det_add_det_le_det_add (CvxLean/Lib/Math/Subadditivity.lean)

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
⊢ A.det + B.det ≤ (A + B).det
Tactic:
by_cases hA' : A.det = 0
State after:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
⊢ A.det + B.det ≤ (A + B).det

case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : ¬A.det = 0
⊢ A.det + B.det ≤ (A + B).det

State before:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
⊢ A.det + B.det ≤ (A + B).det

case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : ¬A.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
{ by_cases hB' : B.det = 0
  { simp [hA', hB']
    apply (hA.add hB).det_nonneg }
  { rw [add_comm A B, add_comm A.det B.det]
    apply det_add_det_le_det_add' _ _ (hB.PosDef_iff_det_ne_zero.2 hB') hA } }
State after:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : ¬A.det = 0
⊢ A.det + B.det ≤ (A + B).det

State before:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : ¬A.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
{ apply det_add_det_le_det_add' _ _ (hA.PosDef_iff_det_ne_zero.2 hA') hB }
State after:
no goals

State before:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
by_cases hB' : B.det = 0
State after:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : B.det = 0
⊢ A.det + B.det ≤ (A + B).det

case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ A.det + B.det ≤ (A + B).det

State before:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : B.det = 0
⊢ A.det + B.det ≤ (A + B).det

case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
{ simp [hA', hB']
  apply (hA.add hB).det_nonneg }
State after:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ A.det + B.det ≤ (A + B).det

State before:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
{ rw [add_comm A B, add_comm A.det B.det]
  apply det_add_det_le_det_add' _ _ (hB.PosDef_iff_det_ne_zero.2 hB') hA }
State after:
no goals

State before:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : B.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
simp [hA', hB']
State after:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : B.det = 0
⊢ 0 ≤ (A + B).det

State before:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : B.det = 0
⊢ 0 ≤ (A + B).det
Tactic:
apply (hA.add hB).det_nonneg
State after:
no goals

State before:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
rw [add_comm A B, add_comm A.det B.det]
State after:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ B.det + A.det ≤ (B + A).det

State before:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ B.det + A.det ≤ (B + A).det
Tactic:
apply det_add_det_le_det_add' _ _ (hB.PosDef_iff_det_ne_zero.2 hB') hA
State after:
no goals

State before:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : ¬A.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
apply det_add_det_le_det_add' _ _ (hA.PosDef_iff_det_ne_zero.2 hA') hB
State after:
no goals