[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
⊢ ⋃ (i : α) (_ : i ∈ Ico m n), Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
[PROOFSTEP]
cases' le_total n m with hnm hmn
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hnm : n ≤ m
⊢ ⋃ (i : α) (_ : i ∈ Ico m n), Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
[PROOFSTEP]
rw [Ico_eq_empty_of_le hnm, Ioc_eq_empty_of_le (hf hnm), biUnion_empty]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
⊢ ⋃ (i : α) (_ : i ∈ Ico m n), Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
[PROOFSTEP]
refine' Succ.rec _ _ hmn
[GOAL]
case inr.refine'_1
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
⊢ ⋃ (i : α) (_ : i ∈ Ico m m), Ioc (f i) (f (succ i)) = Ioc (f m) (f m)
[PROOFSTEP]
simp only [Ioc_self, Ico_self, biUnion_empty]
[GOAL]
case inr.refine'_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
⊢ ∀ (n : α),
    m ≤ n →
      ⋃ (i : α) (_ : i ∈ Ico m n), Ioc (f i) (f (succ i)) = Ioc (f m) (f n) →
        ⋃ (i : α) (_ : i ∈ Ico m (succ n)), Ioc (f i) (f (succ i)) = Ioc (f m) (f (succ n))
[PROOFSTEP]
intro k hmk ihk
[GOAL]
case inr.refine'_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
⊢ ⋃ (i : α) (_ : i ∈ Ico m (succ k)), Ioc (f i) (f (succ i)) = Ioc (f m) (f (succ k))
[PROOFSTEP]
rw [← Ioc_union_Ioc_eq_Ioc (hf hmk) (hf <| le_succ _), union_comm, ← ihk]
[GOAL]
case inr.refine'_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
⊢ ⋃ (i : α) (_ : i ∈ Ico m (succ k)), Ioc (f i) (f (succ i)) =
    Ioc (f k) (f (succ k)) ∪ ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i))
[PROOFSTEP]
by_cases hk : IsMax k
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
hk : IsMax k
⊢ ⋃ (i : α) (_ : i ∈ Ico m (succ k)), Ioc (f i) (f (succ i)) =
    Ioc (f k) (f (succ k)) ∪ ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i))
[PROOFSTEP]
rw [hk.succ_eq, Ioc_self, empty_union]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
hk : ¬IsMax k
⊢ ⋃ (i : α) (_ : i ∈ Ico m (succ k)), Ioc (f i) (f (succ i)) =
    Ioc (f k) (f (succ k)) ∪ ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i))
[PROOFSTEP]
rw [Ico_succ_right_eq_insert_of_not_isMax hmk hk, biUnion_insert]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ Pairwise (Disjoint on fun n => Ioc (f (pred n)) (f n))
[PROOFSTEP]
simpa only [(· ∘ ·), dual_Ico] using hf.dual.pairwise_disjoint_on_Ico_succ
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ Pairwise (Disjoint on fun n => Ico (f (pred n)) (f n))
[PROOFSTEP]
simpa only [(· ∘ ·), dual_Ioc] using hf.dual.pairwise_disjoint_on_Ioc_succ
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ Pairwise (Disjoint on fun n => Ioo (f (pred n)) (f n))
[PROOFSTEP]
simpa only [(· ∘ ·), dual_Ioo] using hf.dual.pairwise_disjoint_on_Ioo_succ
