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

case mpr
m n k l : ℕ
⊢ m = 0 ∨ n = 1 → m / n = m
m n k l : ℕ
⊢ m / n = m ↔ m = 0 ∨ n = 1
constructor
case mp
m n k l : ℕ
a✝ : m / n = m
⊢ m = 0 ∨ n = 1
case mp
m n k l : ℕ
⊢ m / n = m → m = 0 ∨ n = 1
intro
no goals
case mp
m n k l : ℕ
a✝ : m / n = m
⊢ m = 0 ∨ n = 1
match n with
| 0 => simp_all
| 1 =>
  right
  rfl
| n+2 =>
  left
  have : m / (n + 2) ≤ m / 2 := div_le_div_left (by simp) (by decide)
  refine eq_zero_of_le_half ?_
  simp_all
no goals
m n k l : ℕ
a✝ : m / 0 = m
⊢ m = 0 ∨ 0 = 1
simp_all
case h
m n k l : ℕ
a✝ : m / 1 = m
⊢ 1 = 1
m n k l : ℕ
a✝ : m / 1 = m
⊢ m = 0 ∨ 1 = 1
right
no goals
case h
m n k l : ℕ
a✝ : m / 1 = m
⊢ 1 = 1
rfl
case h
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
⊢ m = 0
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
⊢ m = 0 ∨ n + 2 = 1
left
case h
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
this : m / (n + 2) ≤ m / 2
⊢ m = 0
case h
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
⊢ m = 0
have : m / (n + 2) ≤ m / 2 := div_le_div_left (by simp) (by decide)
case h
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
this : m / (n + 2) ≤ m / 2
⊢ m ≤ m / 2
case h
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
this : m / (n + 2) ≤ m / 2
⊢ m = 0
refine eq_zero_of_le_half ?_
no goals
case h
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
this : m / (n + 2) ≤ m / 2
⊢ m ≤ m / 2
simp_all
no goals
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
⊢ 2 ≤ n + 2
simp
no goals
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
⊢ 0 < 2
decide
no goals
case mpr
m n k l : ℕ
⊢ m = 0 ∨ n = 1 → m / n = m
rintro (rfl | rfl) <;> simp