ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α
h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
rw [Ico_disjoint_Ico, min_eq_left (le_of_lt h2.2), le_max_iff] at h
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ x₂ ≤ y₁
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
apply le_antisymm h2.1
no goals
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ x₂ ≤ y₁
exact h.elim (fun h => absurd hx (not_lt_of_le h)) id