case mp
m n k l : ℕ
⊢ min m n = 0 → m = 0 ∨ n = 0

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

case mp.inr
m n k l : ℕ
h : min m n = 0
H : n ≤ m
⊢ m = 0 ∨ n = 0
case mp
m n k l : ℕ
h : min m n = 0
⊢ m = 0 ∨ n = 0
cases' le_total m n with H H
no goals
case mp.inl
m n k l : ℕ
h : min m n = 0
H : m ≤ n
⊢ m = 0 ∨ n = 0
simpa [H] using Or.inl h
no goals
case mp.inr
m n k l : ℕ
h : min m n = 0
H : n ≤ m
⊢ m = 0 ∨ n = 0
simpa [H] using Or.inr h
no goals
case mpr
m n k l : ℕ
⊢ m = 0 ∨ n = 0 → min m n = 0
rintro (rfl | rfl) <;> simp