n m l : ℕ
⊢ ∀ (a : ℕ), ¬a ∈ Ico n m ∩ Ico m l
n m l : ℕ
⊢ Ico n m ∩ Ico m l = []
apply eq_nil_iff_forall_not_mem.2
n m l a : ℕ
⊢ ¬a ∈ Ico n m ∩ Ico m l
n m l : ℕ
⊢ ∀ (a : ℕ), ¬a ∈ Ico n m ∩ Ico m l
intro a
n m l a : ℕ
⊢ n ≤ a → a < m → m ≤ a → l ≤ a
n m l a : ℕ
⊢ ¬a ∈ Ico n m ∩ Ico m l
simp only [and_imp, not_and, not_lt, List.mem_inter, List.Ico.mem]
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ l ≤ a
n m l a : ℕ
⊢ n ≤ a → a < m → m ≤ a → l ≤ a
intro _ h₂ h₃
case h
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ False
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ l ≤ a
exfalso
no goals
case h
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ False
exact not_lt_of_ge h₃ h₂