ι : Type ?u.201690
ι' : Type ?u.201693
α : Type u_1
β : Type ?u.201699
γ : Type ?u.201702
inst✝ : LinearOrderedAddCommGroup α
⊢ ∀ (i' : α × α), True ∧ True → ∃ i, True ∧ abs ⁻¹' Ici i ⊆ Iic i'.fst ∪ Ici i'.snd
ι : Type ?u.201690
ι' : Type ?u.201693
α : Type u_1
β : Type ?u.201699
γ : Type ?u.201702
inst✝ : LinearOrderedAddCommGroup α
⊢ comap abs atTop = atBot ⊔ atTop
refine'
  le_antisymm (((atTop_basis.comap _).le_basis_iff (atBot_basis.sup atTop_basis)).2 _)
    (sup_le tendsto_abs_atBot_atTop.le_comap tendsto_abs_atTop_atTop.le_comap)
case mk
ι : Type ?u.201690
ι' : Type ?u.201693
α : Type u_1
β : Type ?u.201699
γ : Type ?u.201702
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ ∃ i, True ∧ abs ⁻¹' Ici i ⊆ Iic (a, b).fst ∪ Ici (a, b).snd
ι : Type ?u.201690
ι' : Type ?u.201693
α : Type u_1
β : Type ?u.201699
γ : Type ?u.201702
inst✝ : LinearOrderedAddCommGroup α
⊢ ∀ (i' : α × α), True ∧ True → ∃ i, True ∧ abs ⁻¹' Ici i ⊆ Iic i'.fst ∪ Ici i'.snd
rintro ⟨a, b⟩ -
case mk
ι : Type ?u.201690
ι' : Type ?u.201693
α : Type u_1
β : Type ?u.201699
γ : Type ?u.201702
inst✝ : LinearOrderedAddCommGroup α
a b x : α
hx : x ∈ abs ⁻¹' Ici (max (-a) b)
⊢ x ∈ Iic (a, b).fst ∪ Ici (a, b).snd
case mk
ι : Type ?u.201690
ι' : Type ?u.201693
α : Type u_1
β : Type ?u.201699
γ : Type ?u.201702
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ ∃ i, True ∧ abs ⁻¹' Ici i ⊆ Iic (a, b).fst ∪ Ici (a, b).snd
refine' ⟨max (-a) b, trivial, fun x hx => _⟩
case mk
ι : Type ?u.201690
ι' : Type ?u.201693
α : Type u_1
β : Type ?u.201699
γ : Type ?u.201702
inst✝ : LinearOrderedAddCommGroup α
a b x : α
hx : x ≤ a ∧ x ≤ -b ∨ -a ≤ x ∧ b ≤ x
⊢ x ∈ Iic (a, b).fst ∪ Ici (a, b).snd
case mk
ι : Type ?u.201690
ι' : Type ?u.201693
α : Type u_1
β : Type ?u.201699
γ : Type ?u.201702
inst✝ : LinearOrderedAddCommGroup α
a b x : α
hx : x ∈ abs ⁻¹' Ici (max (-a) b)
⊢ x ∈ Iic (a, b).fst ∪ Ici (a, b).snd
rw [mem_preimage, mem_Ici, le_abs', max_le_iff, ← min_neg_neg, le_min_iff, neg_neg] at hx
no goals
case mk
ι : Type ?u.201690
ι' : Type ?u.201693
α : Type u_1
β : Type ?u.201699
γ : Type ?u.201702
inst✝ : LinearOrderedAddCommGroup α
a b x : α
hx : x ≤ a ∧ x ≤ -b ∨ -a ≤ x ∧ b ≤ x
⊢ x ∈ Iic (a, b).fst ∪ Ici (a, b).snd
exact hx.imp And.left And.right