case pos
n a b : ℕ
h₁ : n < a
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b

case neg
n a b : ℕ
h₁ : ¬n < a
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b
n a b : ℕ
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b
by_cases h₁ : n < a
case pos.h
n a b : ℕ
h₁ : n < a
⊢ n < a
case pos
n a b : ℕ
h₁ : n < a
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b
left
no goals
case pos.h
n a b : ℕ
h₁ : n < a
⊢ n < a
exact h₁
case neg.h
n a b : ℕ
h₁ : ¬n < a
⊢ b ≤ n ∨ n ∈ Ico a b
case neg
n a b : ℕ
h₁ : ¬n < a
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b
right
case pos
n a b : ℕ
h₁ : ¬n < a
h₂ : n ∈ Ico a b
⊢ b ≤ n ∨ n ∈ Ico a b

case neg
n a b : ℕ
h₁ : ¬n < a
h₂ : ¬n ∈ Ico a b
⊢ b ≤ n ∨ n ∈ Ico a b
case neg.h
n a b : ℕ
h₁ : ¬n < a
⊢ b ≤ n ∨ n ∈ Ico a b
by_cases h₂ : n ∈ Ico a b
case pos.h
n a b : ℕ
h₁ : ¬n < a
h₂ : n ∈ Ico a b
⊢ n ∈ Ico a b
case pos
n a b : ℕ
h₁ : ¬n < a
h₂ : n ∈ Ico a b
⊢ b ≤ n ∨ n ∈ Ico a b
right
no goals
case pos.h
n a b : ℕ
h₁ : ¬n < a
h₂ : n ∈ Ico a b
⊢ n ∈ Ico a b
exact h₂
case neg.h
n a b : ℕ
h₁ : ¬n < a
h₂ : ¬n ∈ Ico a b
⊢ b ≤ n
case neg
n a b : ℕ
h₁ : ¬n < a
h₂ : ¬n ∈ Ico a b
⊢ b ≤ n ∨ n ∈ Ico a b
left
case neg.h
n a b : ℕ
h₁ : a ≤ n
h₂ : a ≤ n → b ≤ n
⊢ b ≤ n
case neg.h
n a b : ℕ
h₁ : ¬n < a
h₂ : ¬n ∈ Ico a b
⊢ b ≤ n
simp only [Ico.mem, not_and, not_lt] at *
no goals
case neg.h
n a b : ℕ
h₁ : a ≤ n
h₂ : a ≤ n → b ≤ n
⊢ b ≤ n
exact h₂ h₁