case h
α : Type u_1
β : Type ?u.104239
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
α : Type u_1
β : Type ?u.104239
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
ext x
case h.inl
α : Type u_1
β : Type ?u.104239
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : x < b
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)

case h.inr
α : Type u_1
β : Type ?u.104239
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
case h
α : Type u_1
β : Type ?u.104239
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
cases' lt_or_le x b with hba hba
no goals
case h.inl
α : Type u_1
β : Type ?u.104239
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : x < b
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
simp [hba, h₁]
case h.inr
α : Type u_1
β : Type ?u.104239
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x < b ∨ c < x ∧ x < d ↔ x < b ∨ x < d
case h.inr
α : Type u_1
β : Type ?u.104239
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
simp only [mem_Iio, mem_union, mem_Ioo, lt_max_iff]
case h.inr
α : Type u_1
β : Type ?u.104239
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x < d → c < x ∧ x < d
case h.inr
α : Type u_1
β : Type ?u.104239
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x < b ∨ c < x ∧ x < d ↔ x < b ∨ x < d
refine' or_congr Iff.rfl ⟨And.right, _⟩
no goals
case h.inr
α : Type u_1
β : Type ?u.104239
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x < d → c < x ∧ x < d
exact fun h₂ => ⟨h₁.trans_le hba, h₂⟩