case mp
m n k l : ℕ
⊢ max m n = 0 → m = 0 ∧ n = 0

case mpr
m n k l : ℕ
⊢ m = 0 ∧ n = 0 → max m n = 0
m n k l : ℕ
⊢ max m n = 0 ↔ m = 0 ∧ n = 0
constructor
case mp
m n k l : ℕ
h : max m n = 0
⊢ m = 0 ∧ n = 0
case mp
m n k l : ℕ
⊢ max m n = 0 → m = 0 ∧ n = 0
intro h
case mp.inl
m n k l : ℕ
h : max m n = 0
H : m ≤ n
⊢ m = 0 ∧ n = 0

case mp.inr
m n k l : ℕ
h : max m n = 0
H : n ≤ m
⊢ m = 0 ∧ n = 0
case mp
m n k l : ℕ
h : max m n = 0
⊢ m = 0 ∧ n = 0
cases' le_total m n with H H
case mp.inl
m n k l : ℕ
H : m ≤ n
h : n = 0
⊢ m = 0 ∧ n = 0
case mp.inl
m n k l : ℕ
h : max m n = 0
H : m ≤ n
⊢ m = 0 ∧ n = 0
simp only [H, max_eq_right] at h
no goals
case mp.inl
m n k l : ℕ
H : m ≤ n
h : n = 0
⊢ m = 0 ∧ n = 0
exact ⟨le_antisymm (H.trans h.le) (zero_le _), h⟩
case mp.inr
m n k l : ℕ
H : n ≤ m
h : m = 0
⊢ m = 0 ∧ n = 0
case mp.inr
m n k l : ℕ
h : max m n = 0
H : n ≤ m
⊢ m = 0 ∧ n = 0
simp only [H, max_eq_left] at h
no goals
case mp.inr
m n k l : ℕ
H : n ≤ m
h : m = 0
⊢ m = 0 ∧ n = 0
exact ⟨h, le_antisymm (H.trans h.le) (zero_le _)⟩
case mpr.intro
k l : ℕ
⊢ max 0 0 = 0
case mpr
m n k l : ℕ
⊢ m = 0 ∧ n = 0 → max m n = 0
rintro ⟨rfl, rfl⟩
no goals
case mpr.intro
k l : ℕ
⊢ max 0 0 = 0
simp