English
If c ≤ b and a ≤ d, then Icc a b ∪ Icc c d = Icc (min a c) (max b d).
Русский
Если c ≤ b и a ≤ d, то Icc(a,b) ∪ Icc(c,d) = Icc(min(a,c), max(b,d)).
LaTeX
$$$(c \le b) \land (a \le d) \implies \mathrm{Icc}(a,b) \cup \mathrm{Icc}(c,d) = \mathrm{Icc}(\min(a,c), \max(b,d))$$$
Lean4
theorem Icc_union_Icc' (h₁ : c ≤ b) (h₂ : a ≤ d) : Icc a b ∪ Icc c d = Icc (min a c) (max b d) :=
by
ext1 x
simp_rw [mem_union, mem_Icc, min_le_iff, le_max_iff]
by_cases hc : c ≤ x <;> by_cases hd : x ≤ d
· tauto
· have hax : a ≤ x := h₂.trans (le_of_not_ge hd)
tauto
· have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
tauto
· tauto