awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst_1 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_2 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))
⊢ ∀ (j : Subtype p), (s (↑j : ι')).Nonempty

Tactic:
push Not at H

Premises used: Not
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst_1 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_2 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
hv : v.HasBasis p s
f : ι → α
H' : ¬∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))
H : ∀ (j : Subtype p), (s (↑j : ι')).Nonempty
⊢ ∀ (j : Subtype p), (s (↑j : ι')).Nonempty

Tactic:
simpa only [nonempty_iff_ne_empty] using H

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst_1 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_2 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))
⊢ ∃ (j : Subtype p), BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))

Tactic:
push Not at H'

Premises used: Not
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst_1 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_2 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
H' : ∃ (j : Subtype p), BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))
⊢ ∃ (j : Subtype p), BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))

Tactic:
H'
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst_1 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_2 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
H' : ∃ (j : Subtype p), BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))
⊢ ∃ (j : Subtype p), BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))

Tactic:
exact H'
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst_1 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_2 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s (↑j : ι')).Nonempty
H : ∃ (j : Subtype p), BddAbove.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))
⊢ limsup f v = ⨅ (j : Subtype p), ⨆ (i : (↑(s (↑(limsup_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)

Tactic:
HasBasis.liminf_eq_ciSup_ciInf (α := αᵒᵈ) hv hs H

Premises used: Filter.limsSup, iInf, iSup, setOf, Filter.limsup, OrderDual, Filter.HasBasis.liminf_eq_ciSup_ciInf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst_1 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_2 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
hv : v.HasBasis p s
f : ι → α
⊢ limsup f v =
    if ∃ (j : Subtype p), s (↑j : ι') = ∅ then sInf univ
    else
      if ∀ (j : Subtype p), ¬BddAbove.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
        sInf ∅
      else ⨅ (j : Subtype p), ⨆ (i : (↑(s (↑(limsup_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)

Tactic:
HasBasis.liminf_eq_ite (α := αᵒᵈ) hv f

Premises used: Filter.limsSup, Filter.HasBasis.liminf_eq_ite, iInf, Set.Mem, iSup, setOf, upperBounds, BddAbove, Filter.limsup, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ l (v x)
hv_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
⊢ l (limsup v f) ≤ limsup (fun (x : α) ↦ l (v x)) f

Tactic:
le_limsSup_of_le hlv fun c hc => ?_

Premises used: Filter.le_limsSup_of_le, Filter.limsup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ l (v x)
hv_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
refine : ∀ (c : γ) (hc : ∀ᶠ (n : γ) in map (fun (x : α) ↦ l (v x)) f, n ≤ c), l (limsup v f) ≤ c
⊢ l (limsup v f) ≤ limsup (fun (x : α) ↦ l (v x)) f

Tactic:
refine le_limsSup_of_le hlv fun c hc => ?_

Premises used: Filter.le_limsSup_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ l (v x)
hv_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
c : γ
hc : ∀ᶠ (n : γ) in map (fun (x : α) ↦ l (v x)) f, n ≤ c
⊢ ∀ᶠ (a : α) in f, l (v a) ≤ c

Tactic:
rw [Filter.eventually_map] at hc

Premises used: Filter.eventually_map
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ l (v x)
hv_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
c : γ
hc : ∀ᶠ (a : α) in f, l (v a) ≤ c
simp_rw : ∀ (hc : ∀ᶠ (a : α) in f, v a ≤ u c), limsup v f ≤ u c
⊢ l (limsup v f) ≤ c

Tactic:
simp_rw [gc _ _] at hc ⊢
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ l (v x)
hv_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
c : γ
hc : ∀ᶠ (a : α) in f, v a ≤ u c
⊢ limsup v f ≤ u c

Tactic:
limsSup_le_of_le hv_co hc

Premises used: Filter.limsup, Filter.limsSup_le_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ l (v x)
hv_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
c : γ
hc : ∀ᶠ (a : α) in f, v a ≤ u c
⊢ limsup v f ≤ u c

Tactic:
exact limsSup_le_of_le hv_co hc

Premises used: Filter.limsSup_le_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
⊢ Eq.{u_6 + 1} (α := γ) ((g : (a : β) → γ) (limsup u f) : γ) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f : γ)

Tactic:
le_antisymm ((OrderIso.to_galoisConnection g).l_limsup_le hgu hu_co) ?_

Premises used: OrderIso.to_galoisConnection, le_antisymm, GaloisConnection.l_limsup_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
refine :
  LE.le.{u_6} (α := γ) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f : γ) ((g : (a : β) → γ) (limsup u f) : γ)
⊢ Eq.{u_6 + 1} (α := γ) ((g : (a : β) → γ) (limsup u f) : γ) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f : γ)

Tactic:
refine le_antisymm ((OrderIso.to_galoisConnection g).l_limsup_le hgu hu_co) ?_

Premises used: OrderIso.to_galoisConnection, le_antisymm, GaloisConnection.l_limsup_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
rw :
  LE.le.{u_6} (α := γ)
    ((g : (a : β) → γ) ((g.symm : (a : γ) → β) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f) : β) : γ)
    ((g : (a : β) → γ) (limsup u f) : γ)
⊢ LE.le.{u_6} (α := γ) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f : γ) ((g : (a : β) → γ) (limsup u f) : γ)

Tactic:
rw [← g.symm.symm_apply_apply <| limsup (fun x => g (u x)) f, g.symm_symm]

Premises used: OrderIso.symm_symm, OrderIso.symm, Filter.limsup, OrderIso.symm_apply_apply, DFunLike.coe
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
⊢ LE.le.{u_6} (α := γ)
    ((g : (a : β) → γ) ((g.symm : (a : γ) → β) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f) : β) : γ)
    ((g : (a : β) → γ) (limsup u f) : γ)

Tactic:
g.monotone ?_

Premises used: OrderIso.monotone
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
refine : (g.symm : (a : γ) → β) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f) ≤ limsup u f
⊢ LE.le.{u_6} (α := γ)
    ((g : (a : β) → γ) ((g.symm : (a : γ) → β) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f) : β) : γ)
    ((g : (a : β) → γ) (limsup u f) : γ)

Tactic:
refine g.monotone ?_

Premises used: OrderIso.monotone
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
⊢ u = fun (i : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u i) : γ)

Tactic:
have hf : u = fun i => g.symm (g (u i)) := funext fun i => (g.symm_apply_apply (u i)).symm
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hf : u = fun (i : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u i) : γ)
nth_rw :
  LE.le.{u_2} (α := β) ((g.symm : (a : γ) → β) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f) : β)
    (limsup (fun (i : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u i) : γ)) f : β)
⊢ (g.symm : (a : γ) → β) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f) ≤ limsup u f

Tactic:
nth_rw 2 [hf]
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hf : u = fun (i : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u i) : γ)
⊢ LE.le.{u_2} (α := β) ((g.symm : (a : γ) → β) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f) : β)
    (limsup (fun (i : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u i) : γ)) f : β)

Tactic:
(OrderIso.to_galoisConnection g.symm).l_limsup_le ?_ hgu_co

Premises used: OrderIso.to_galoisConnection, OrderIso.symm, GaloisConnection.l_limsup_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hf : u = fun (i : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u i) : γ)
refine : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (x : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u x) : γ)
⊢ LE.le.{u_2} (α := β) ((g.symm : (a : γ) → β) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f) : β)
    (limsup (fun (i : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u i) : γ)) f : β)

Tactic:
refine (OrderIso.to_galoisConnection g.symm).l_limsup_le ?_ hgu_co

Premises used: OrderIso.to_galoisConnection, OrderIso.symm, GaloisConnection.l_limsup_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hf : u = fun (i : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u i) : γ)
simp_rw : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (x : α) ↦ u x
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (x : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u x) : γ)

Tactic:
simp_rw [g.symm_apply_apply]

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hf : u = fun (i : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u i) : γ)
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (x : α) ↦ u x

Tactic:
hu
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hf : u = fun (i : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u i) : γ)
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (x : α) ↦ u x

Tactic:
exact hu
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_6
inst : ConditionallyCompleteLattice β
inst_1 : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
hu_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
hgu : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≥ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
hgu_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≥ x2) f fun (x : α) ↦ (g : (a : β) → γ) (u x)
⊢ Eq.{u_6 + 1} (α := γ) ((g : (a : β) → γ) (liminf u f) : γ) (liminf (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f : γ)

Tactic:
OrderIso.limsup_apply (β := βᵒᵈ) (γ := γᵒᵈ) g.dual hu hu_co hgu hgu_co

Premises used: Filter.limsInf, OrderIso.limsup_apply, Filter.liminf, setOf, OrderIso.dual, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)

Tactic:
have bddmax := IsBoundedUnder.sup h₃ h₄
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)

Tactic:
have cobddmax := isCoboundedUnder_le_max (v := v) (Or.inl h₁)
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
a : limsup (fun (a : α) ↦ max (u a) (v a)) f ≤ max (limsup u f) (limsup v f)
a₁ : max (limsup u f) (limsup v f) ≤ limsup (fun (a : α) ↦ max (u a) (v a)) f
⊢ limsup (fun (a : α) ↦ max (u a) (v a)) f = max (limsup u f) (limsup v f)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
⊢ limsup (fun (a : α) ↦ max (u a) (v a)) f ≤ max (limsup u f) (limsup v f)

Tactic:
(limsup_le_iff cobddmax bddmax).2 (fun b hb ↦ ?_)

Premises used: Iff.mpr, Filter.limsup_le_iff
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
a : ∀ (b : β) (hb : b > max (limsup u f) (limsup v f)), ∀ᶠ (a : α) in f, max (u a) (v a) < b
⊢ limsup (fun (a : α) ↦ max (u a) (v a)) f ≤ max (limsup u f) (limsup v f)

Tactic:
refine (limsup_le_iff cobddmax bddmax).2 (fun b hb ↦ ?_)

Premises used: Iff.mpr, Filter.limsup_le_iff
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
b : β
hb : b > max (limsup u f) (limsup v f)
⊢ ∀ᶠ (a : α) in f, u a < b

Tactic:
have hu := eventually_lt_of_limsup_lt (lt_of_le_of_lt (le_max_left _ _) hb) h₃
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
b : β
hb : b > max (limsup u f) (limsup v f)
hu : ∀ᶠ (a : α) in f, u a < b
⊢ ∀ᶠ (a : α) in f, v a < b

Tactic:
have hv := eventually_lt_of_limsup_lt (lt_of_le_of_lt (le_max_right _ _) hb) h₄
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
b : β
hb : b > max (limsup u f) (limsup v f)
hu : ∀ᶠ (a : α) in f, u a < b
hv : ∀ᶠ (a : α) in f, v a < b
x : α
⊢ Membership.mem (γ := Set α) ({x : α | (fun (a : α) ↦ u a < b) x} ∩ {x : α | (fun (a : α) ↦ v a < b) x}) x →
    Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ max (u a) (v a) < b) x} x

Tactic:
simp