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)

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)
α : 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)
cases' le_total n m with hnm hmn
no goals
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)
rw [Ico_eq_empty_of_le hnm, Ioc_eq_empty_of_le (hf hnm), biUnion_empty]
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)

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))
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)
refine' Succ.rec _ _ hmn
no goals
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)
simp only [Ioc_self, Ico_self, biUnion_empty]
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))
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))
intro k hmk ihk
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))
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))
rw [← Ioc_union_Ioc_eq_Ioc (hf hmk) (hf <| le_succ _), union_comm, ← ihk]
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))

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))
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))
by_cases hk : IsMax k
no goals
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))
rw [hk.succ_eq, Ioc_self, empty_union]
no goals
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))
rw [Ico_succ_right_eq_insert_of_not_isMax hmk hk, biUnion_insert]