[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
by_cases xy : x ≤ y
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : x ≤ y
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
by_cases yx : y ≤ x
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : ¬x ≤ y
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
by_cases yx : y ≤ x
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
simp [cmpLE, *, Ordering.swap]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
simp [cmpLE, *, Ordering.swap]
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
simp [cmpLE, *, Ordering.swap]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
[PROOFSTEP]
simp [cmpLE, *, Ordering.swap]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False
[PROOFSTEP]
cases not_or_of_not xy yx (total_of _ _ _)
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
by_cases xy : x ≤ y
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : x ≤ y
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
by_cases yx : y ≤ x
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : ¬x ≤ y
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
by_cases yx : y ≤ x
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
simp [cmpLE, lt_iff_le_not_le, *, cmp, cmpUsing]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
simp [cmpLE, lt_iff_le_not_le, *, cmp, cmpUsing]
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
simp [cmpLE, lt_iff_le_not_le, *, cmp, cmpUsing]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y
[PROOFSTEP]
simp [cmpLE, lt_iff_le_not_le, *, cmp, cmpUsing]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False
[PROOFSTEP]
cases not_or_of_not xy yx (total_of _ _ _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
o : Ordering
⊢ Compares (swap o) a b ↔ Compares o b a
[PROOFSTEP]
cases o
[GOAL]
case lt
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
⊢ Compares (swap lt) a b ↔ Compares lt b a
[PROOFSTEP]
exact Iff.rfl
[GOAL]
case eq
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
⊢ Compares (swap eq) a b ↔ Compares eq b a
[PROOFSTEP]
exact eq_comm
[GOAL]
case gt
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
⊢ Compares (swap gt) a b ↔ Compares gt b a
[PROOFSTEP]
exact Iff.rfl
[GOAL]
α : Type u_1
β : Type u_2
o o' : Ordering
⊢ swap o = o' ↔ o = swap o'
[PROOFSTEP]
rw [← swap_inj, swap_swap]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
h✝ : Compares eq a b
h : eq = lt
⊢ a < b
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
h✝ : Compares gt a b
h : gt = lt
⊢ a < b
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
h✝ : Compares eq a b
x✝ : b ≤ a
h : eq = lt
⊢ False
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
h✝ : Compares gt a b
x✝ : b ≤ a
h : gt = lt
⊢ False
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
h✝ : Compares lt a b
h : lt = eq
⊢ a = b
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
h✝ : Compares gt a b
h : gt = eq
⊢ a = b
[PROOFSTEP]
injection h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
⊢ Compares o a b ↔ Compares o a' b'
[PROOFSTEP]
refine' ⟨h, fun ho => _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
⊢ Compares o a b
[PROOFSTEP]
cases' lt_trichotomy a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab : a < b
⊢ Compares o a b
[PROOFSTEP]
have hab : Compares Ordering.lt a b := hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab✝ : a < b
hab : Compares lt a b
⊢ Compares o a b
[PROOFSTEP]
rwa [ho.inj (h hab)]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab : a = b ∨ b < a
⊢ Compares o a b
[PROOFSTEP]
cases' hab with hab hab
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab : a = b
⊢ Compares o a b
[PROOFSTEP]
have hab : Compares Ordering.eq a b := hab
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab✝ : a = b
hab : Compares eq a b
⊢ Compares o a b
[PROOFSTEP]
rwa [ho.inj (h hab)]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab : b < a
⊢ Compares o a b
[PROOFSTEP]
have hab : Compares Ordering.gt a b := hab
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, Compares o a b → Compares o a' b'
o : Ordering
ho : Compares o a' b'
hab✝ : b < a
hab : Compares gt a b
⊢ Compares o a b
[PROOFSTEP]
rwa [ho.inj (h hab)]
[GOAL]
α : Type u_1
β : Type u_2
o₁ o₂ : Ordering
⊢ swap (orElse o₁ o₂) = orElse (swap o₁) (swap o₂)
[PROOFSTEP]
cases o₁
[GOAL]
case lt
α : Type u_1
β : Type u_2
o₂ : Ordering
⊢ swap (orElse lt o₂) = orElse (swap lt) (swap o₂)
[PROOFSTEP]
rfl
[GOAL]
case eq
α : Type u_1
β : Type u_2
o₂ : Ordering
⊢ swap (orElse eq o₂) = orElse (swap eq) (swap o₂)
[PROOFSTEP]
rfl
[GOAL]
case gt
α : Type u_1
β : Type u_2
o₂ : Ordering
⊢ swap (orElse gt o₂) = orElse (swap gt) (swap o₂)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
o₁ o₂ : Ordering
⊢ orElse o₁ o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt
[PROOFSTEP]
cases o₁
[GOAL]
case lt
α : Type u_1
β : Type u_2
o₂ : Ordering
⊢ orElse lt o₂ = lt ↔ lt = lt ∨ lt = eq ∧ o₂ = lt
[PROOFSTEP]
cases o₂
[GOAL]
case eq
α : Type u_1
β : Type u_2
o₂ : Ordering
⊢ orElse eq o₂ = lt ↔ eq = lt ∨ eq = eq ∧ o₂ = lt
[PROOFSTEP]
cases o₂
[GOAL]
case gt
α : Type u_1
β : Type u_2
o₂ : Ordering
⊢ orElse gt o₂ = lt ↔ gt = lt ∨ gt = eq ∧ o₂ = lt
[PROOFSTEP]
cases o₂
[GOAL]
case lt.lt
α : Type u_1
β : Type u_2
⊢ orElse lt lt = lt ↔ lt = lt ∨ lt = eq ∧ lt = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse lt lt = lt ↔ lt = lt ∨ lt = eq ∧ lt = lt
[PROOFSTEP]
decide
[GOAL]
case lt.eq
α : Type u_1
β : Type u_2
⊢ orElse lt eq = lt ↔ lt = lt ∨ lt = eq ∧ eq = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse lt eq = lt ↔ lt = lt ∨ lt = eq ∧ eq = lt
[PROOFSTEP]
decide
[GOAL]
case lt.gt
α : Type u_1
β : Type u_2
⊢ orElse lt gt = lt ↔ lt = lt ∨ lt = eq ∧ gt = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse lt gt = lt ↔ lt = lt ∨ lt = eq ∧ gt = lt
[PROOFSTEP]
decide
[GOAL]
case eq.lt
α : Type u_1
β : Type u_2
⊢ orElse eq lt = lt ↔ eq = lt ∨ eq = eq ∧ lt = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse eq lt = lt ↔ eq = lt ∨ eq = eq ∧ lt = lt
[PROOFSTEP]
decide
[GOAL]
case eq.eq
α : Type u_1
β : Type u_2
⊢ orElse eq eq = lt ↔ eq = lt ∨ eq = eq ∧ eq = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse eq eq = lt ↔ eq = lt ∨ eq = eq ∧ eq = lt
[PROOFSTEP]
decide
[GOAL]
case eq.gt
α : Type u_1
β : Type u_2
⊢ orElse eq gt = lt ↔ eq = lt ∨ eq = eq ∧ gt = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse eq gt = lt ↔ eq = lt ∨ eq = eq ∧ gt = lt
[PROOFSTEP]
decide
[GOAL]
case gt.lt
α : Type u_1
β : Type u_2
⊢ orElse gt lt = lt ↔ gt = lt ∨ gt = eq ∧ lt = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse gt lt = lt ↔ gt = lt ∨ gt = eq ∧ lt = lt
[PROOFSTEP]
decide
[GOAL]
case gt.eq
α : Type u_1
β : Type u_2
⊢ orElse gt eq = lt ↔ gt = lt ∨ gt = eq ∧ eq = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse gt eq = lt ↔ gt = lt ∨ gt = eq ∧ eq = lt
[PROOFSTEP]
decide
[GOAL]
case gt.gt
α : Type u_1
β : Type u_2
⊢ orElse gt gt = lt ↔ gt = lt ∨ gt = eq ∧ gt = lt
[PROOFSTEP]
exact by decide
[GOAL]
α : Type u_1
β : Type u_2
⊢ orElse gt gt = lt ↔ gt = lt ∨ gt = eq ∧ gt = lt
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
o : Ordering
⊢ Compares o (↑toDual a) (↑toDual b) ↔ Compares o b a
[PROOFSTEP]
cases o
[GOAL]
case lt
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
⊢ Compares lt (↑toDual a) (↑toDual b) ↔ Compares lt b a
case eq
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
⊢ Compares eq (↑toDual a) (↑toDual b) ↔ Compares eq b a
case gt α : Type u_1 β : Type u_2 inst✝ : LT α a b : α ⊢ Compares gt (↑toDual a) (↑toDual b) ↔ Compares gt b a
[PROOFSTEP]
exacts [Iff.rfl, eq_comm, Iff.rfl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : αᵒᵈ
o : Ordering
⊢ Compares o (↑ofDual a) (↑ofDual b) ↔ Compares o b a
[PROOFSTEP]
cases o
[GOAL]
case lt
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : αᵒᵈ
⊢ Compares lt (↑ofDual a) (↑ofDual b) ↔ Compares lt b a
case eq
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : αᵒᵈ
⊢ Compares eq (↑ofDual a) (↑ofDual b) ↔ Compares eq b a
case gt α : Type u_1 β : Type u_2 inst✝ : LT α a b : αᵒᵈ ⊢ Compares gt (↑ofDual a) (↑ofDual b) ↔ Compares gt b a
[PROOFSTEP]
exacts [Iff.rfl, eq_comm, Iff.rfl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ Compares (cmp a b) a b
[PROOFSTEP]
obtain h | h | h := lt_trichotomy a b
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ Compares (cmp a b) a b
[PROOFSTEP]
simp [cmp, cmpUsing, h, h.not_lt]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ Compares (cmp a b) a b
[PROOFSTEP]
simp [cmp, cmpUsing, h, h.not_lt]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ Compares (cmp a b) a b
[PROOFSTEP]
simp [cmp, cmpUsing, h, h.not_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
⊢ swap (cmp a b) = cmp b a
[PROOFSTEP]
unfold cmp cmpUsing
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
by_cases h : a < b
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : a < b
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
by_cases h₂ : b < a
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : ¬a < b
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
by_cases h₂ : b < a
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : a < b
h₂ : b < a
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
simp [h, h₂, Ordering.swap]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : a < b
h₂ : ¬b < a
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
simp [h, h₂, Ordering.swap]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : ¬a < b
h₂ : b < a
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
simp [h, h₂, Ordering.swap]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : ¬a < b
h₂ : ¬b < a
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
[PROOFSTEP]
simp [h, h₂, Ordering.swap]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : a < b
h₂ : b < a
⊢ False
[PROOFSTEP]
exact lt_asymm h h₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
x y : α
⊢ cmp x x = eq
[PROOFSTEP]
rw [cmp_eq_eq_iff]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'
[PROOFSTEP]
rwa [← cmp_swap x', ← cmp_swap, swap_inj]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
⊢ cmp x y = cmp x' y'
[PROOFSTEP]
rwa [← cmp_swap y', ← cmp_swap, swap_inj]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x < y ↔ x' < y'
[PROOFSTEP]
rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff, h]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x ≤ y ↔ x' ≤ y'
[PROOFSTEP]
rw [← not_lt, ← not_lt]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ ¬y < x ↔ ¬y' < x'
[PROOFSTEP]
apply not_congr
[GOAL]
case h
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ y < x ↔ y' < x'
[PROOFSTEP]
apply lt_iff_lt_of_cmp_eq_cmp
[GOAL]
case h.h
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'
[PROOFSTEP]
rwa [cmp_eq_cmp_symm]
[GOAL]
α : Type u_1
β✝ : Type u_2
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x = y ↔ x' = y'
[PROOFSTEP]
rw [le_antisymm_iff, le_antisymm_iff, le_iff_le_of_cmp_eq_cmp h, le_iff_le_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 h)]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
⊢ IsBounded r ⊥ ↔ Nonempty α
[PROOFSTEP]
simp [IsBounded, exists_true_iff_nonempty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
⊢ IsBounded r ⊤ ↔ ∃ t, ∀ (x : α), r x t
[PROOFSTEP]
simp [IsBounded, eq_univ_iff_forall]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
s : Set α
⊢ IsBounded r (𝓟 s) ↔ ∃ t, ∀ (x : α), x ∈ s → r x t
[PROOFSTEP]
simp [IsBounded, subset_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
inst✝ : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun x x_1 => x ≤ x_1) l u
hv : v ≤ᶠ[l] u
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l v
[PROOFSTEP]
apply hu.imp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
inst✝ : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun x x_1 => x ≤ x_1) l u
hv : v ≤ᶠ[l] u
⊢ ∀ (a : β), (∀ᶠ (x : β) in map u l, (fun x x_1 => x ≤ x_1) x a) → ∀ᶠ (x : β) in map v l, (fun x x_1 => x ≤ x_1) x a
[PROOFSTEP]
exact fun b hb => (eventually_map.1 hb).mp <| hv.mono fun x => le_trans
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
⊢ ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
rintro ⟨b, hb⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (x : β) in map f l, (fun x x_1 => x ≤ x_1) x b
⊢ False
[PROOFSTEP]
rw [eventually_map] at hb
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
⊢ False
[PROOFSTEP]
obtain ⟨b', h⟩ := exists_gt b
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
b' : β
h : b < b'
⊢ False
[PROOFSTEP]
have hb' := (tendsto_atTop.mp hf) b'
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
⊢ False
[PROOFSTEP]
have : {x : α | f x ≤ b} ∩ {x : α | b' ≤ f x} = ∅ :=
  eq_empty_of_subset_empty fun x hx => (not_le_of_lt h) (le_trans hx.2 hx.1)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
this : {x | f x ≤ b} ∩ {x | b' ≤ f x} = ∅
⊢ False
[PROOFSTEP]
exact (nonempty_of_mem (hb.and hb')).ne_empty this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) cofinite f
⊢ BddAbove (range f)
[PROOFSTEP]
rcases hf with ⟨b, hb⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b
⊢ BddAbove (range f)
[PROOFSTEP]
haveI : Nonempty β := ⟨b⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b
this : Nonempty β
⊢ BddAbove (range f)
[PROOFSTEP]
rw [← image_univ, ← union_compl_self {x | f x ≤ b}, image_union, bddAbove_union]
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b
this : Nonempty β
⊢ BddAbove (f '' {x | f x ≤ b}) ∧ BddAbove (f '' {x | f x ≤ b}ᶜ)
[PROOFSTEP]
exact ⟨⟨b, ball_image_iff.2 fun x => id⟩, (hb.image f).bddAbove⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : ℕ → β
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop f
⊢ BddAbove (range f)
[PROOFSTEP]
rw [← Nat.cofinite_eq_atTop] at hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : ℕ → β
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) cofinite f
⊢ BddAbove (range f)
[PROOFSTEP]
exact hf.bddAbove_range_of_cofinite
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
⊢ IsCobounded r ⊥ ↔ ∃ b, ∀ (x : α), r b x
[PROOFSTEP]
simp [IsCobounded]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
⊢ IsCobounded r ⊤ ↔ Nonempty α
[PROOFSTEP]
simp (config := { contextual := true }) [IsCobounded, eq_univ_iff_forall, exists_true_iff_nonempty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
s : Set α
⊢ IsCobounded r (𝓟 s) ↔ ∃ b, ∀ (a : α), (∀ (x : α), x ∈ s → r x a) → r b a
[PROOFSTEP]
simp [IsCobounded, subset_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
l : Filter γ
u : γ → α
a : α
⊢ (∀ᶠ (x : β) in map (fun x => ↑e (u x)) l, (fun x x_1 => x ≤ x_1) x (↑e a)) ↔
    ∀ᶠ (x : α) in map u l, (fun x x_1 => x ≤ x_1) x a
[PROOFSTEP]
simp only [eventually_map, e.le_iff_le]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SemilatticeSup α
f : Filter β
u v : β → α
bu : α
hu : ∀ᶠ (x : β) in f, u x ≤ bu
bv : α
hv : ∀ᶠ (x : β) in f, v x ≤ bv
⊢ ∀ᶠ (x : β) in f, u x ⊔ v x ≤ bu ⊔ bv
[PROOFSTEP]
filter_upwards [hu, hv] with _ using sup_le_sup
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (blimsup u f fun x => True) = limsup u f
[PROOFSTEP]
simp [blimsup_eq, limsup_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun x => True) = liminf u f
[PROOFSTEP]
simp [bliminf_eq, liminf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p = limsup (u ∘ Subtype.val) (comap Subtype.val f)
[PROOFSTEP]
simp only [blimsup_eq, limsup_eq, Function.comp_apply, eventually_comap, SetCoe.forall, Subtype.coe_mk, mem_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = sInf {a | ∀ᶠ (b : β) in f, ∀ (a_1 : { x // p x }), ↑a_1 = b → u ↑a_1 ≤ a}
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = {a | ∀ᶠ (b : β) in f, ∀ (a_1 : { x // p x }), ↑a_1 = b → u ↑a_1 ≤ a}
[PROOFSTEP]
ext a
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (b : β) in f, ∀ (a_1 : { x // p x }), ↑a_1 = b → u ↑a_1 ≤ a}
[PROOFSTEP]
simp_rw [Subtype.forall]
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (b : β) in f, ∀ (a_1 : β), p a_1 → a_1 = b → u a_1 ≤ a}
[PROOFSTEP]
exact
  eventually_congr
    (eventually_of_forall fun x => ⟨fun hx y hy hxy => hxy.symm ▸ hx (hxy ▸ hy), fun hx hx' => hx x hx' rfl⟩)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : Set.Nonempty s
⊢ limsSup (𝓟 s) = sSup s
[PROOFSTEP]
simp only [limsSup, eventually_principal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : Set.Nonempty s
⊢ sInf {a | ∀ (x : α), x ∈ s → x ≤ a} = sSup s
[PROOFSTEP]
exact csInf_upper_bounds_eq_csSup h hs
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_5
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ limsup u f = limsup v f
[PROOFSTEP]
rw [limsup_eq]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_5
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ sInf {a | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f
[PROOFSTEP]
congr with b
[GOAL]
case e_a.h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_5
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
⊢ b ∈ {a | ∀ᶠ (n : α) in f, u n ≤ a} ↔ b ∈ {a | ∀ᶠ (n : β) in map v f, n ≤ a}
[PROOFSTEP]
exact eventually_congr (h.mono fun x hx => by simp [hx])
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_5
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
x : α
hx : u x = v x
⊢ u x ≤ b ↔ v x ∈ {x | (fun n => n ≤ b) x}
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
⊢ blimsup u f p = blimsup v f p
[PROOFSTEP]
rw [blimsup_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = blimsup v f p
[PROOFSTEP]
congr with b
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
⊢ b ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ b ∈ {a | ∀ᶠ (x : β) in f, p x → v x ≤ a}
[PROOFSTEP]
refine' eventually_congr (h.mono fun x hx => ⟨fun h₁ h₂ => _, fun h₁ h₂ => _⟩)
[GOAL]
case e_a.h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → u x ≤ b
h₂ : p x
⊢ v x ≤ b
[PROOFSTEP]
rw [← hx h₂]
[GOAL]
case e_a.h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → u x ≤ b
h₂ : p x
⊢ u x ≤ b
[PROOFSTEP]
exact h₁ h₂
[GOAL]
case e_a.h.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → v x ≤ b
h₂ : p x
⊢ u x ≤ b
[PROOFSTEP]
rw [hx h₂]
[GOAL]
case e_a.h.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → v x ≤ b
h₂ : p x
⊢ v x ≤ b
[PROOFSTEP]
exact h₁ h₂
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : ConditionallyCompleteLattice α✝
α : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
f : Filter α
inst✝ : NeBot f
b : β
⊢ limsup (fun x => b) f = b
[PROOFSTEP]
simpa only [limsup_eq, eventually_const] using csInf_Ici
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
⊢ ⊥ ∈ {a | ∀ᶠ (n : α) in ⊥, n ≤ a}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : β → α
⊢ limsup f ⊥ = ⊥
[PROOFSTEP]
simp [limsup]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
⊢ ⊤ ∈ {a | ∀ᶠ (n : α) in ⊥, a ≤ n}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : β → α
⊢ liminf f ⊥ = ⊤
[PROOFSTEP]
simp [liminf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
⊢ ∀ (b : α), b ∈ {a | ∀ᶠ (n : α) in ⊤, n ≤ a} → ⊤ ≤ b
[PROOFSTEP]
simp [eq_univ_iff_forall]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
⊢ ∀ (b : α), (∀ (x : α), x ≤ b) → b = ⊤
[PROOFSTEP]
exact fun b hb => top_unique <| hb _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
⊢ ∀ (b : α), b ∈ {a | ∀ᶠ (n : α) in ⊤, a ≤ n} → b ≤ ⊥
[PROOFSTEP]
simp [eq_univ_iff_forall]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
⊢ ∀ (b : α), (∀ (x : α), b ≤ x) → b = ⊥
[PROOFSTEP]
exact fun b hb => bot_unique <| hb _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ (blimsup u f fun x => False) = ⊥
[PROOFSTEP]
simp [blimsup_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun x => False) = ⊤
[PROOFSTEP]
simp [bliminf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
⊢ limsup (fun x => ⊥) f = ⊥
[PROOFSTEP]
rw [limsup_eq, eq_bot_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
⊢ sInf {a | ∀ᶠ (n : β) in f, ⊥ ≤ a} ≤ ⊥
[PROOFSTEP]
exact sInf_le (eventually_of_forall fun _ => le_rfl)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ IsCoboundedUnder (fun x x_1 => x ≥ x_1) f u
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ ⨅ (i : Set β) (_ : i ∈ f), sSup (u '' id i) = ⨅ (s : Set β) (_ : s ∈ f), ⨆ (a : β) (_ : a ∈ s), u a
[PROOFSTEP]
simp only [sSup_image, id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ (i : ℕ) (_ : True), sSup (u '' Ici i) = ⨅ (n : ℕ), ⨆ (i : ℕ) (_ : i ≥ n), u i
[PROOFSTEP]
simp only [sSup_image, iInf_const]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ (i : ℕ), ⨆ (a : ℕ) (_ : a ∈ Ici i), u a = ⨅ (n : ℕ), ⨆ (i : ℕ) (_ : i ≥ n), u i
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
u : ℕ → α
⊢ limsup u atTop = ⨅ (n : ℕ), ⨆ (i : ℕ), u (i + n)
[PROOFSTEP]
simp only [limsup_eq_iInf_iSup_of_nat, iSup_ge_eq_iSup_nat_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
p : ι → Prop
s : ι → Set β
f : Filter β
u : β → α
h : HasBasis f p s
⊢ ⨅ (i : ι) (_ : p i), sSup (u '' s i) = ⨅ (i : ι) (_ : p i), ⨆ (a : β) (_ : a ∈ s i), u a
[PROOFSTEP]
simp only [sSup_image, id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ blimsup u f p = blimsup u f q
[PROOFSTEP]
simp only [blimsup_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = sInf {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
[PROOFSTEP]
ext a
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
[PROOFSTEP]
refine' eventually_congr (h.mono fun b hb => _)
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
[PROOFSTEP]
cases' eq_or_ne (u b) ⊥ with hu hu
[GOAL]
case e_a.h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b = ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
[PROOFSTEP]
simp [hu]
[GOAL]
case e_a.h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
[PROOFSTEP]
rw [hb hu]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ blimsup u f p = ⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
[PROOFSTEP]
refine' le_antisymm (sInf_le_sInf _) (iInf_le_iff.mpr fun a ha => le_sInf_iff.mpr fun a' ha' => _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (range fun s => ⨅ (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b) ⊆ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
[PROOFSTEP]
rintro - ⟨s, rfl⟩
[GOAL]
case refine'_1.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
⊢ (fun s => ⨅ (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b) s ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
[PROOFSTEP]
simp only [mem_setOf_eq, le_iInf_iff]
[GOAL]
case refine'_1.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
⊢ ∀ᶠ (x : β) in f, p x → s ∈ f → u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
[PROOFSTEP]
conv =>
  congr
  ext
  rw [Imp.swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
| ∀ᶠ (x : β) in f, p x → s ∈ f → u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
[PROOFSTEP]
  congr
  ext
  rw [Imp.swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
| ∀ᶠ (x : β) in f, p x → s ∈ f → u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
[PROOFSTEP]
  congr
  ext
  rw [Imp.swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
| ∀ᶠ (x : β) in f, p x → s ∈ f → u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
[PROOFSTEP]
congr
[GOAL]
case p
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
| fun x => p x → s ∈ f → u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
case f
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
| f
[PROOFSTEP]
ext
[GOAL]
case p.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
x✝ : β
| p x✝ → s ∈ f → u x✝ ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
case f
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
| f
[PROOFSTEP]
rw [Imp.swap]
[GOAL]
case refine'_1.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
⊢ ∀ᶠ (x : β) in f, s ∈ f → p x → u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
[PROOFSTEP]
refine' eventually_imp_distrib_left.mpr fun h => eventually_iff_exists_mem.2 ⟨s, h, fun x h₁ h₂ => _⟩
[GOAL]
case refine'_1.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
h : s ∈ f
x : β
h₁ : x ∈ s
h₂ : p x
⊢ u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
[PROOFSTEP]
exact @le_iSup₂ α β (fun b => p b ∧ b ∈ s) _ (fun b _ => u b) x ⟨h₂, h₁⟩
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
⊢ a ≤ a'
[PROOFSTEP]
obtain ⟨s, hs, hs'⟩ := eventually_iff_exists_mem.mp ha'
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
⊢ a ≤ a'
[PROOFSTEP]
have : ∀ (y : β), p y → y ∈ s → u y ≤ a' := fun y ↦ by rw [Imp.swap]; exact hs' y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
y : β
⊢ p y → y ∈ s → u y ≤ a'
[PROOFSTEP]
rw [Imp.swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
y : β
⊢ y ∈ s → p y → u y ≤ a'
[PROOFSTEP]
exact hs' y
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
this : ∀ (y : β), p y → y ∈ s → u y ≤ a'
⊢ a ≤ a'
[PROOFSTEP]
exact (le_iInf_iff.mp (ha s) hs).trans (by simpa only [iSup₂_le_iff, and_imp])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
this : ∀ (y : β), p y → y ∈ s → u y ≤ a'
⊢ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b ≤ a'
[PROOFSTEP]
simpa only [iSup₂_le_iff, and_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
p : ℕ → Prop
u : ℕ → α
⊢ blimsup u atTop p = ⨅ (i : ℕ), ⨆ (j : ℕ) (_ : p j ∧ i ≤ j), u j
[PROOFSTEP]
simp only [blimsup_eq_limsup_subtype, Function.comp, (atTop_basis.comap ((↑) : {x | p x} → ℕ)).limsup_eq_iInf_iSup,
  iSup_subtype, iSup_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
p : ℕ → Prop
u : ℕ → α
⊢ ⨅ (i : ℕ) (_ : True),
      ⨆ (i_1 : ℕ) (x : i_1 ∈ {x | p x}) (_ : { val := i_1, property := (_ : i_1 ∈ {x | p x}) } ∈ Subtype.val ⁻¹' Ici i),
        u i_1 =
    ⨅ (i : ℕ), ⨆ (j : ℕ) (_ : p j) (_ : i ≤ j), u j
[PROOFSTEP]
simp only [mem_setOf_eq, mem_preimage, mem_Ici, not_le, iInf_pos]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F = sInf ((fun I => sSup (a '' I)) '' F.sets)
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F ≤ sInf ((fun I => sSup (a '' I)) '' F.sets)
[PROOFSTEP]
rw [limsup_eq]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1} ≤ sInf ((fun I => sSup (a '' I)) '' F.sets)
[PROOFSTEP]
refine' sInf_le_sInf fun x hx => _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I => sSup (a '' I)) '' F.sets
⊢ x ∈ {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1}
[PROOFSTEP]
rcases(mem_image _ F.sets x).mp hx with ⟨I, ⟨I_mem_F, hI⟩⟩
[GOAL]
case refine'_1.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I => sSup (a '' I)) '' F.sets
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
⊢ x ∈ {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1}
[PROOFSTEP]
filter_upwards [I_mem_F] with i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I => sSup (a '' I)) '' F.sets
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
i : ι
hi : i ∈ I
⊢ a i ≤ x
[PROOFSTEP]
exact hI ▸ le_sSup (mem_image_of_mem _ hi)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I => sSup (a '' I)) '' F.sets) ≤ limsup a F
[PROOFSTEP]
refine' le_sInf_iff.mpr fun b hb => sInf_le_of_le (mem_image_of_mem _ <| Filter.mem_sets.mpr hb) <| sSup_le _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
b : R
hb : b ∈ {a_1 | ∀ᶠ (n : R) in map a F, n ≤ a_1}
⊢ ∀ (b_1 : R), b_1 ∈ a '' (a ⁻¹' {x | (fun n => n ≤ b) x}) → b_1 ≤ b
[PROOFSTEP]
rintro _ ⟨_, h, rfl⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
b : R
hb : b ∈ {a_1 | ∀ᶠ (n : R) in map a F, n ≤ a_1}
w✝ : ι
h : w✝ ∈ a ⁻¹' {x | (fun n => n ≤ b) x}
⊢ a w✝ ≤ b
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ liminf (fun i => f (i + k)) atTop = liminf f atTop
[PROOFSTEP]
simp_rw [liminf_eq_iSup_iInf_of_nat]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f (i + k) = ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f i
[PROOFSTEP]
exact iSup_iInf_ge_nat_add f k
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ liminf u f ≤ x
[PROOFSTEP]
rw [liminf_eq]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ sSup {a | ∀ᶠ (n : α) in f, a ≤ u n} ≤ x
[PROOFSTEP]
refine' sSup_le fun b hb => _
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ b ≤ x
[PROOFSTEP]
have hbx : ∃ᶠ _ in f, b ≤ x := by
  revert h
  rw [← not_imp_not, not_frequently, not_frequently]
  exact fun h => hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ ∃ᶠ (x_1 : α) in f, b ≤ x
[PROOFSTEP]
revert h
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ (∃ᶠ (a : α) in f, u a ≤ x) → ∃ᶠ (x_1 : α) in f, b ≤ x
[PROOFSTEP]
rw [← not_imp_not, not_frequently, not_frequently]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ (∀ᶠ (x_1 : α) in f, ¬b ≤ x) → ∀ᶠ (x_1 : α) in f, ¬u x_1 ≤ x
[PROOFSTEP]
exact fun h => hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
hbx : ∃ᶠ (x_1 : α) in f, b ≤ x
⊢ b ≤ x
[PROOFSTEP]
exact hbx.exists.choose_spec
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ↑f (limsup (fun n => (↑f)^[n] a) atTop) = limsup (fun n => (↑f)^[n] a) atTop
[PROOFSTEP]
rw [limsup_eq_iInf_iSup_of_nat', map_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ (i : ℕ), ↑f (⨆ (i_1 : ℕ), (↑f)^[i_1 + i] a) = ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f)^[i + n] a
[PROOFSTEP]
simp_rw [_root_.map_iSup, ← Function.comp_apply (f := f), ← Function.iterate_succ' f, ← Nat.add_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ (i : ℕ), ⨆ (i_1 : ℕ), (↑f)^[i_1 + Nat.succ i] a = ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f)^[i + n] a
[PROOFSTEP]
conv_rhs => rw [iInf_split _ ((· < ·) (0 : ℕ))]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
| ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f)^[i + n] a
[PROOFSTEP]
rw [iInf_split _ ((· < ·) (0 : ℕ))]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
| ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f)^[i + n] a
[PROOFSTEP]
rw [iInf_split _ ((· < ·) (0 : ℕ))]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
| ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f)^[i + n] a
[PROOFSTEP]
rw [iInf_split _ ((· < ·) (0 : ℕ))]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ (i : ℕ), ⨆ (i_1 : ℕ), (↑f)^[i_1 + Nat.succ i] a =
    (⨅ (i : ℕ) (_ : (fun x x_1 => x < x_1) 0 i), ⨆ (i_1 : ℕ), (↑f)^[i_1 + i] a) ⊓
      ⨅ (i : ℕ) (_ : ¬(fun x x_1 => x < x_1) 0 i), ⨆ (i_1 : ℕ), (↑f)^[i_1 + i] a
[PROOFSTEP]
simp only [not_lt, le_zero_iff, iInf_iInf_eq_left, add_zero, iInf_nat_gt_zero_eq, left_eq_inf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ (i : ℕ), ⨆ (i_1 : ℕ), (↑f)^[i_1 + Nat.succ i] a ≤ ⨆ (i : ℕ), (↑f)^[i] a
[PROOFSTEP]
refine' (iInf_le (fun i => ⨆ j, f^[j + (i + 1)] a) 0).trans _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨆ (j : ℕ), (↑f)^[j + (0 + 1)] a ≤ ⨆ (i : ℕ), (↑f)^[i] a
[PROOFSTEP]
simp only [zero_add, Function.comp_apply, iSup_le_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ∀ (i : ℕ), (↑f)^[i + 1] a ≤ ⨆ (i : ℕ), (↑f)^[i] a
[PROOFSTEP]
exact fun i => le_iSup (fun i => f^[i] a) (i + 1)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
h : ∀ (x : β), p x → q x
a : α
ha : a ∈ {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
⊢ ∀ (x : β), (q x → u x ≤ a) → p x → u x ≤ a
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
h : ∀ (x : β), p x → q x
a : α
ha : a ∈ {a | ∀ᶠ (x : β) in f, q x → a ≤ u x}
⊢ ∀ (x : β), (q x → a ≤ u x) → p x → a ≤ u x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
⊢ ∀ (x : β), p x ∧ q x → p x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
⊢ ∀ (x : β), p x ∧ q x → q x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
⊢ ∀ (x : β), p x → p x ∨ q x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
⊢ ∀ (x : β), q x → p x ∨ q x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ ↑e (blimsup u f p) = blimsup (↑e ∘ u) f p
[PROOFSTEP]
simp only [blimsup_eq, map_sInf, Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ sInf ((fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}) = sInf {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ (fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
[PROOFSTEP]
ext c
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
c : γ
⊢ c ∈ (fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ c ∈ {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
[PROOFSTEP]
obtain ⟨a, rfl⟩ := e.surjective c
[GOAL]
case e_a.h.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
a : α
⊢ ↑e a ∈ (fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ ↑e a ∈ {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g✝ : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ↑g (blimsup u f p) ≤ blimsup (↑g ∘ u) f p
[PROOFSTEP]
simp only [blimsup_eq_iInf_biSup, Function.comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g✝ : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ↑g (⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b) ≤
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), ↑g (u b)
[PROOFSTEP]
refine' ((OrderHomClass.mono g).map_iInf₂_le _).trans _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g✝ : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ⨅ (i : Set β) (_ : i ∈ f), ↑g (⨆ (b : β) (_ : p b ∧ b ∈ i), u b) ≤
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), ↑g (u b)
[PROOFSTEP]
simp only [_root_.map_iSup, le_refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (blimsup u f fun x => p x ∨ q x) = blimsup u f p ⊔ blimsup u f q
[PROOFSTEP]
refine' le_antisymm _ blimsup_sup_le_or
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (blimsup u f fun x => p x ∨ q x) ≤ blimsup u f p ⊔ blimsup u f q
[PROOFSTEP]
simp only [blimsup_eq, sInf_sup_eq, sup_sInf_eq, le_iInf₂_iff, mem_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ ∀ (i : α),
    (∀ᶠ (x : β) in f, q x → u x ≤ i) →
      ∀ (i_1 : α), (∀ᶠ (x : β) in f, p x → u x ≤ i_1) → sInf {a | ∀ᶠ (x : β) in f, p x ∨ q x → u x ≤ a} ≤ i_1 ⊔ i
[PROOFSTEP]
refine' fun a' ha' a ha => sInf_le ((ha.and ha').mono fun b h hb => _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
a' : α
ha' : ∀ᶠ (x : β) in f, q x → u x ≤ a'
a : α
ha : ∀ᶠ (x : β) in f, p x → u x ≤ a
b : β
h : (p b → u b ≤ a) ∧ (q b → u b ≤ a')
hb : p b ∨ q b
⊢ u b ≤ a ⊔ a'
[PROOFSTEP]
exact Or.elim hb (fun hb => le_sup_of_le_left <| h.1 hb) fun hb => le_sup_of_le_right <| h.2 hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
⊢ a ⊔ limsup u f = limsup (fun x => a ⊔ u x) f
[PROOFSTEP]
simp only [limsup_eq_iInf_iSup, iSup_sup_eq, sup_iInf₂_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
⊢ ⨅ (i : Set β) (_ : i ∈ f), a ⊔ ⨆ (a : β) (_ : a ∈ i), u a =
    ⨅ (s : Set β) (_ : s ∈ f), (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
[PROOFSTEP]
congr
[GOAL]
case e_s
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
⊢ (fun i => ⨅ (_ : i ∈ f), a ⊔ ⨆ (a : β) (_ : a ∈ i), u a) = fun s =>
    ⨅ (_ : s ∈ f), (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
[PROOFSTEP]
ext s
[GOAL]
case e_s.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
⊢ ⨅ (_ : s ∈ f), a ⊔ ⨆ (a : β) (_ : a ∈ s), u a = ⨅ (_ : s ∈ f), (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
[PROOFSTEP]
congr
[GOAL]
case e_s.h.e_s
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
⊢ (fun j => a ⊔ ⨆ (a : β) (_ : a ∈ s), u a) = fun x => (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
[PROOFSTEP]
ext hs
[GOAL]
case e_s.h.e_s.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
hs : s ∈ f
⊢ a ⊔ ⨆ (a : β) (_ : a ∈ s), u a = (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
[PROOFSTEP]
congr
[GOAL]
case e_s.h.e_s.h.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
hs : s ∈ f
⊢ a = ⨆ (x : β) (_ : x ∈ s), a
[PROOFSTEP]
exact (biSup_const (nonempty_of_mem hs)).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
a : α
⊢ a ⊔ liminf u f = liminf (fun x => a ⊔ u x) f
[PROOFSTEP]
simp only [liminf_eq_iSup_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
a : α
⊢ a ⊔ ⨆ (s : Set β) (_ : s ∈ f), ⨅ (a : β) (_ : a ∈ s), u a =
    ⨆ (s : Set β) (_ : s ∈ f), ⨅ (a_1 : β) (_ : a_1 ∈ s), a ⊔ u a_1
[PROOFSTEP]
rw [sup_comm, biSup_sup (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
a : α
⊢ ⨆ (i : Set β) (_ : i ∈ f), (⨅ (a : β) (_ : a ∈ i), u a) ⊔ a =
    ⨆ (s : Set β) (_ : s ∈ f), ⨅ (a_1 : β) (_ : a_1 ∈ s), a ⊔ u a_1
[PROOFSTEP]
simp_rw [iInf₂_sup_eq, sup_comm (a := a)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ (limsup u f)ᶜ = liminf (compl ∘ u) f
[PROOFSTEP]
simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ (liminf u f)ᶜ = limsup (compl ∘ u) f
[PROOFSTEP]
simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ limsup u f \ a = limsup (fun b => u b \ a) f
[PROOFSTEP]
simp only [limsup_eq_iInf_iSup, sdiff_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (⨅ (s : Set β) (_ : s ∈ f), ⨆ (a : β) (_ : a ∈ s), u a) ⊓ aᶜ =
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (a_1 : β) (_ : a_1 ∈ s), u a_1 ⊓ aᶜ
[PROOFSTEP]
rw [biInf_inf (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ ⨅ (i : Set β) (_ : i ∈ f), (⨆ (a : β) (_ : a ∈ i), u a) ⊓ aᶜ =
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (a_1 : β) (_ : a_1 ∈ s), u a_1 ⊓ aᶜ
[PROOFSTEP]
simp_rw [inf_comm, inf_iSup₂_eq, inf_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : NeBot f
a : α
⊢ liminf u f \ a = liminf (fun b => u b \ a) f
[PROOFSTEP]
simp only [sdiff_eq, inf_comm (b := aᶜ), inf_liminf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : NeBot f
a : α
⊢ a \ limsup u f = liminf (fun b => a \ u b) f
[PROOFSTEP]
rw [← compl_inj_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : NeBot f
a : α
⊢ (a \ limsup u f)ᶜ = (liminf (fun b => a \ u b) f)ᶜ
[PROOFSTEP]
simp only [sdiff_eq, liminf_compl, (· ∘ ·), compl_inf, compl_compl, sup_limsup]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ a \ liminf u f = limsup (fun b => a \ u b) f
[PROOFSTEP]
rw [← compl_inj_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (a \ liminf u f)ᶜ = (limsup (fun b => a \ u b) f)ᶜ
[PROOFSTEP]
simp only [sdiff_eq, limsup_compl, (· ∘ ·), compl_inf, compl_compl, sup_liminf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ blimsup s cofinite p = {x | Set.Infinite {n | p n ∧ x ∈ s n}}
[PROOFSTEP]
simp only [blimsup_eq, le_eq_subset, eventually_cofinite, not_forall, sInf_eq_sInter, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}} = {x | Set.Infinite {n | p n ∧ x ∈ s n}}
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
⊢ x ∈ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}} ↔ x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
[PROOFSTEP]
refine' ⟨fun h => _, fun hx t h => _⟩
[GOAL]
case h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∈ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}}
⊢ x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
[PROOFSTEP]
contrapose! h
[GOAL]
case h.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
t : Set α
h : t ∈ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}}
⊢ x ∈ t
[PROOFSTEP]
contrapose! h
[GOAL]
case h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ ¬x ∈ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}}
[PROOFSTEP]
simp only [mem_sInter, mem_setOf_eq, not_forall, exists_prop]
[GOAL]
case h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ ∃ x_1, Set.Finite {x | p x ∧ ¬s x ⊆ x_1} ∧ ¬x ∈ x_1
[PROOFSTEP]
exact ⟨{ x }ᶜ, by simpa using h, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ Set.Finite {x_1 | p x_1 ∧ ¬s x_1 ⊆ {x}ᶜ}
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ ¬x ∈ {x}ᶜ
[PROOFSTEP]
simp
[GOAL]
case h.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
t : Set α
h : ¬x ∈ t
⊢ ¬t ∈ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}}
[PROOFSTEP]
exact hx.mono fun i hi => ⟨hi.1, fun hit => h (hit hi.2)⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ bliminf s cofinite p = {x | Set.Finite {n | p n ∧ ¬x ∈ s n}}
[PROOFSTEP]
rw [← compl_inj_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ (bliminf s cofinite p)ᶜ = {x | Set.Finite {n | p n ∧ ¬x ∈ s n}}ᶜ
[PROOFSTEP]
simp only [bliminf_eq_iSup_biInf, compl_iInf, compl_iSup, ← blimsup_eq_iInf_biSup, cofinite.blimsup_set_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ {x | Set.Infinite {n | p n ∧ x ∈ (s n)ᶜ}} = {x | Set.Finite {n | p n ∧ ¬x ∈ s n}}ᶜ
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ limsup s cofinite = {x | Set.Infinite {n | x ∈ s n}}
[PROOFSTEP]
simp only [← cofinite.blimsup_true s, cofinite.blimsup_set_eq, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ liminf s cofinite = {x | Set.Finite {n | ¬x ∈ s n}}
[PROOFSTEP]
simp only [← cofinite.bliminf_true s, cofinite.bliminf_set_eq, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
[PROOFSTEP]
rw [blimsup_eq_iInf_biSup] at hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ ⨅ (s : Set β) (_ : s ∈ l), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
[PROOFSTEP]
simp only [iSup_eq_iUnion, iInf_eq_iInter, mem_iInter, mem_iUnion, exists_prop] at hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
hx : ∀ (i : Set β), i ∈ l → ∃ i_2, (p i_2 ∧ i_2 ∈ i) ∧ x ∈ u i_2
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
[PROOFSTEP]
choose g hg hg' using hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → i ∈ l → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
[PROOFSTEP]
refine' ⟨fun i : {i | q i} => g (b i) (hl.mem_of_mem i.2), fun i => ⟨_, _⟩⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → i ∈ l → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
i : ↑{i | q i}
⊢ x ∈ u ((fun i => g (b ↑i) (_ : b ↑i ∈ l)) i)
[PROOFSTEP]
exact hg' (b i) (hl.mem_of_mem i.2)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → i ∈ l → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
i : ↑{i | q i}
⊢ p ((fun i => g (b ↑i) (_ : b ↑i ∈ l)) i) ∧ (fun i => g (b ↑i) (_ : b ↑i ∈ l)) i ∈ b ↑i
[PROOFSTEP]
exact hg (b i) (hl.mem_of_mem i.2)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
hl : HasBasis l (fun x => True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
[PROOFSTEP]
obtain ⟨f, hf⟩ := exists_forall_mem_of_hasBasis_mem_blimsup hl hx
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
hl : HasBasis l (fun x => True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
f : ↑{i | True} → β
hf : ∀ (i : ↑{i | True}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
[PROOFSTEP]
exact ⟨fun i => f ⟨i, trivial⟩, fun i => hf ⟨i, trivial⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝
h : a < limsSup f
⊢ ∃ᶠ (n : α) in f, a < n
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝
h : ¬∃ᶠ (n : α) in f, a < n
⊢ limsSup f ≤ a
[PROOFSTEP]
simp only [not_frequently, not_lt] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝
h : ∀ᶠ (x : α) in f, x ≤ a
⊢ limsSup f ≤ a
[PROOFSTEP]
exact limsSup_le_of_le hf h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
⊢ ∀ᶠ (a : α) in f, b < u a
[PROOFSTEP]
obtain ⟨c, hc, hbc⟩ : ∃ (c : β) (_ : c ∈ {c : β | ∀ᶠ n : α in f, c ≤ u n}), b < c :=
  by
  simp_rw [exists_prop]
  exact exists_lt_of_lt_csSup hu h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
⊢ ∃ c x, b < c
[PROOFSTEP]
simp_rw [exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
⊢ ∃ c, c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n} ∧ b < c
[PROOFSTEP]
exact exists_lt_of_lt_csSup hu h
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
c : β
hc : c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}
hbc : b < c
⊢ ∀ᶠ (a : α) in f, b < u a
[PROOFSTEP]
exact hc.mono fun x hx => lt_of_lt_of_le hbc hx
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu_le : ∃ᶠ (x : α) in f, b ≤ u x
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ b ≤ limsup u f
[PROOFSTEP]
revert hu_le
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ (∃ᶠ (x : α) in f, b ≤ u x) → b ≤ limsup u f
[PROOFSTEP]
rw [← not_imp_not, not_frequently]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ ¬b ≤ limsup u f → ∀ᶠ (x : α) in f, ¬b ≤ u x
[PROOFSTEP]
simp_rw [← lt_iff_not_ge]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ limsup u f < b → ∀ᶠ (x : α) in f, u x < b
[PROOFSTEP]
exact fun h => eventually_lt_of_limsup_lt h hu
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h : b < limsup u f
⊢ ∃ᶠ (x : α) in f, b < u x
[PROOFSTEP]
contrapose! h
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h : ¬∃ᶠ (x : α) in f, b < u x
⊢ limsup u f ≤ b
[PROOFSTEP]
apply limsSup_le_of_le hu
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h : ¬∃ᶠ (x : α) in f, b < u x
⊢ ∀ᶠ (n : β) in map u f, n ≤ b
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l (g ∘ f) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
refine' ⟨_, fun h => h.isBoundedUnder (α := β) hg⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l (g ∘ f) → IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
rintro ⟨c, hc⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (x : γ) in map (g ∘ f) l, (fun x x_1 => x ≤ x_1) x c
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
rw [eventually_map] at hc
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((g ∘ f) a) c
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
obtain ⟨b, hb⟩ : ∃ b, ∀ a ≥ b, c < g a := eventually_atTop.1 (hg'.eventually_gt_atTop c)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((g ∘ f) a) c
b : β
hb : ∀ (a : β), a ≥ b → c < g a
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
exact ⟨b, hc.mono fun x hx => not_lt.1 fun h => (hb _ h.le).not_le hx⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝
⊢ l (limsup v f) ≤ limsup (fun x => l (v x)) f
[PROOFSTEP]
refine' le_limsSup_of_le hlv fun c hc => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝
c : γ
hc : ∀ᶠ (n : γ) in map (fun x => l (v x)) f, n ≤ c
⊢ l (limsup v f) ≤ c
[PROOFSTEP]
rw [Filter.eventually_map] at hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝
c : γ
hc : ∀ᶠ (a : α) in f, l (v a) ≤ c
⊢ l (limsup v f) ≤ c
[PROOFSTEP]
simp_rw [gc _ _] at hc ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝
c : γ
hc : ∀ᶠ (a : α) in f, v a ≤ u c
⊢ limsup v f ≤ u c
[PROOFSTEP]
exact limsSup_le_of_le hv_co hc
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ ↑g (limsup u f) = limsup (fun x => ↑g (u x)) f
[PROOFSTEP]
refine' le_antisymm ((OrderIso.to_galoisConnection g).l_limsup_le hgu hu_co) _
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ limsup (fun x => ↑g (u x)) f ≤ ↑g (limsup u f)
[PROOFSTEP]
rw [← g.symm.symm_apply_apply <| limsup (fun x => g (u x)) f, g.symm_symm]
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ ↑g (↑(symm g) (limsup (fun x => ↑g (u x)) f)) ≤ ↑g (limsup u f)
[PROOFSTEP]
refine' g.monotone _
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ ↑(symm g) (limsup (fun x => ↑g (u x)) f) ≤ limsup u f
[PROOFSTEP]
have hf : u = fun i => g.symm (g (u i)) := funext fun i => (g.symm_apply_apply (u i)).symm
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ ↑(symm g) (limsup (fun x => ↑g (u x)) f) ≤ limsup u f
[PROOFSTEP]
nth_rw 2 [hf]
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ ↑(symm g) (limsup (fun x => ↑g (u x)) f) ≤ limsup (fun i => ↑(symm g) (↑g (u i))) f
[PROOFSTEP]
refine' (OrderIso.to_galoisConnection g.symm).l_limsup_le _ hgu_co
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑(symm g) (↑g (u x))
[PROOFSTEP]
simp_rw [g.symm_apply_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => u x
[PROOFSTEP]
exact hu


[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝¹ : IsPreorder α r
inst✝ : Inhabited α
⊢ Inhabited (Antisymmetrization α r)
[PROOFSTEP]
unfold Antisymmetrization
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝¹ : IsPreorder α r
inst✝ : Inhabited α
⊢ Inhabited (Quotient (AntisymmRel.setoid α r))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
⊢ Relation.Fibration (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (toAntisymmetrization fun x x_1 => x ≤ x_1)
[PROOFSTEP]
rintro a ⟨b⟩ h
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝ b✝¹ a : α
b✝ : Antisymmetrization α fun x x_1 => x ≤ x_1
b : α
h : Quot.mk Setoid.r b < toAntisymmetrization (fun x x_1 => x ≤ x_1) a
⊢ ∃ a', (fun x x_1 => x < x_1) a' a ∧ toAntisymmetrization (fun x x_1 => x ≤ x_1) a' = Quot.mk Setoid.r b
[PROOFSTEP]
exact ⟨b, h, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝¹ b : α
a✝ : (Antisymmetrization α fun x x_1 => x ≤ x_1)ᵒᵈ
a : α
⊢ Quotient.map' id
      (_ :
        ∀ (x x_1 : αᵒᵈ),
          (fun x x_2 => x ≤ x_2) x x_1 ∧ (fun x x_2 => x ≤ x_2) x_1 x →
            (fun x x_2 => x ≤ x_2) x_1 x ∧ (fun x x_2 => x ≤ x_2) x x_1)
      (Quotient.map' id
        (_ :
          ∀ (x x_1 : α),
            (fun x x_2 => x ≤ x_2) x x_1 ∧ (fun x x_2 => x ≤ x_2) x_1 x →
              (fun x x_2 => x ≤ x_2) x_1 x ∧ (fun x x_2 => x ≤ x_2) x x_1)
        (Quotient.mk'' a)) =
    Quotient.mk'' a
[PROOFSTEP]
simp_rw [Quotient.map'_mk'', id]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝¹ b : α
a✝ : Antisymmetrization αᵒᵈ fun x x_1 => x ≤ x_1
a : αᵒᵈ
⊢ Quotient.map' id
      (_ :
        ∀ (x x_1 : α),
          (fun x x_2 => x ≤ x_2) x x_1 ∧ (fun x x_2 => x ≤ x_2) x_1 x →
            (fun x x_2 => x ≤ x_2) x_1 x ∧ (fun x x_2 => x ≤ x_2) x x_1)
      (Quotient.map' id
        (_ :
          ∀ (x x_1 : αᵒᵈ),
            (fun x x_2 => x ≤ x_2) x x_1 ∧ (fun x x_2 => x ≤ x_2) x_1 x →
              (fun x x_2 => x ≤ x_2) x_1 x ∧ (fun x x_2 => x ≤ x_2) x x_1)
        (Quotient.mk'' a)) =
    Quotient.mk'' a
[PROOFSTEP]
simp_rw [Quotient.map'_mk'', id]


[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
⊢ IsCoatomic α
[PROOFSTEP]
refine ⟨fun x => le_top.eq_or_lt.imp_right fun hx => ?_⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
⊢ ∃ a, IsCoatom a ∧ x ≤ a
[PROOFSTEP]
have : ∃ y ∈ Ico x ⊤, x ≤ y ∧ ∀ z ∈ Ico x ⊤, y ≤ z → z = y :=
  by
  refine zorn_nonempty_partialOrder₀ (Ico x ⊤) (fun c hxc hc y hy => ?_) x (left_mem_Ico.2 hx)
  rcases h c hc ⟨y, hy⟩ fun h => (hxc h).2.ne rfl with ⟨z, hz, hcz⟩
  exact ⟨z, ⟨le_trans (hxc hy).1 (hcz hy), hz.lt_top⟩, hcz⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
⊢ ∃ y, y ∈ Ico x ⊤ ∧ x ≤ y ∧ ∀ (z : α), z ∈ Ico x ⊤ → y ≤ z → z = y
[PROOFSTEP]
refine zorn_nonempty_partialOrder₀ (Ico x ⊤) (fun c hxc hc y hy => ?_) x (left_mem_Ico.2 hx)
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun x x_1 => x ≤ x_1) c
y : α
hy : y ∈ c
⊢ ∃ ub, ub ∈ Ico x ⊤ ∧ ∀ (z : α), z ∈ c → z ≤ ub
[PROOFSTEP]
rcases h c hc ⟨y, hy⟩ fun h => (hxc h).2.ne rfl with ⟨z, hz, hcz⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun x x_1 => x ≤ x_1) c
y : α
hy : y ∈ c
z : α
hz : z ≠ ⊤
hcz : z ∈ upperBounds c
⊢ ∃ ub, ub ∈ Ico x ⊤ ∧ ∀ (z : α), z ∈ c → z ≤ ub
[PROOFSTEP]
exact ⟨z, ⟨le_trans (hxc hy).1 (hcz hy), hz.lt_top⟩, hcz⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
this : ∃ y, y ∈ Ico x ⊤ ∧ x ≤ y ∧ ∀ (z : α), z ∈ Ico x ⊤ → y ≤ z → z = y
⊢ ∃ a, IsCoatom a ∧ x ≤ a
[PROOFSTEP]
rcases this with ⟨y, ⟨hxy, hy⟩, -, hy'⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hy : y < ⊤
hy' : ∀ (z : α), z ∈ Ico x ⊤ → y ≤ z → z = y
⊢ ∃ a, IsCoatom a ∧ x ≤ a
[PROOFSTEP]
refine ⟨y, ⟨hy.ne, fun z hyz => le_top.eq_or_lt.resolve_right fun hz => ?_⟩, hxy⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hy : y < ⊤
hy' : ∀ (z : α), z ∈ Ico x ⊤ → y ≤ z → z = y
z : α
hyz : y < z
hz : z < ⊤
⊢ False
[PROOFSTEP]
exact hyz.ne' (hy' z ⟨hxy.trans hyz.le, hz⟩ hyz.le)