awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
rw :
  Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), (f : (a : α) → α) (⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i] a))
    (⨅ (n : ℕ), ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i + n] a)
⊢ Eq (α := α) ((f : (a : α) → α) (limsup (fun (n : ℕ) ↦ (⇑f : (a : α) → α)^[n] a) atTop) : α)
    (limsup (fun (n : ℕ) ↦ (⇑f : (a : α) → α)^[n] a) atTop : α)

Tactic:
rw [limsup_eq_iInf_iSup_of_nat', map_iInf]

Premises used: map_iInf, Filter.limsup_eq_iInf_iSup_of_nat'
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
simp_rw :
  Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i.succ] a)
    (⨅ (n : ℕ), ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i + n] a)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), (f : (a : α) → α) (⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i] a))
    (⨅ (n : ℕ), ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i + n] a)

Tactic:
simp_rw [_root_.map_iSup, ← Function.comp_apply (f := f), ← Function.iterate_succ' f,
    ← Nat.add_succ]

Premises used: Function.iterate_succ', Nat.add_succ, map_iSup, Function.comp_apply, DFunLike.coe
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
rw :
  (⨅ (i : ℕ), ⨅ (_ : 0 < i), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i] a) ⊓
    ⨅ (i : ℕ), ⨅ (_ : ¬0 < i), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i] a
| ⨅ (n : ℕ), ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i + n] a

Tactic:
rw [iInf_split _ (0 < ·)]

Premises used: iInf_split, LT.lt, OfNat.ofNat
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
conv_rhs :
  Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i.succ] a)
    ((⨅ (i : ℕ), ⨅ (_ : 0 < i), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i] a) ⊓
      ⨅ (i : ℕ), ⨅ (_ : ¬0 < i), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i] a)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i.succ] a)
    (⨅ (n : ℕ), ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i + n] a)

Tactic:
conv_rhs => rw [iInf_split _ (0 < ·)]

Premises used: iInf_split, LT.lt, OfNat.ofNat
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
simp :
  LE.le.{u_1} (α := α) (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i.succ] a)
    (⨆ (i : ℕ), (⇑f : (a : α) → α)^[i] a)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i.succ] a)
    ((⨅ (i : ℕ), ⨅ (_ : 0 < i), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i] a) ⊓
      ⨅ (i : ℕ), ⨅ (_ : ¬0 < i), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i] a)

Tactic:
simp only [not_lt, Nat.le_zero, iInf_iInf_eq_left, add_zero, iInf_nat_gt_zero_eq, left_eq_inf]

Premises used: Nat.le_zero, not_lt, iInf_iInf_eq_left, iInf_nat_gt_zero_eq, add_zero, left_eq_inf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ LE.le.{u_1} (α := α) (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i.succ] a)
    (⨆ (i : ℕ), (⇑f : (a : α) → α)^[i] a)

Tactic:
(iInf_le (fun i => ⨆ j, f^[j + (i + 1)] a) 0).trans ?_

Premises used: iSup, Nat.iterate, HAdd.hAdd, LE.le.trans, OfNat.ofNat, DFunLike.coe, iInf_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
refine :
  LE.le.{u_1} (α := α) (⨆ (j : ℕ), (⇑f : (a : α) → α)^[j + HAdd.hAdd (α := ℕ) 0 1] a)
    (⨆ (i : ℕ), (⇑f : (a : α) → α)^[i] a)
⊢ LE.le.{u_1} (α := α) (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i.succ] a)
    (⨆ (i : ℕ), (⇑f : (a : α) → α)^[i] a)

Tactic:
refine (iInf_le (fun i => ⨆ j, f^[j + (i + 1)] a) 0).trans ?_

Premises used: iSup, Nat.iterate, HAdd.hAdd, LE.le.trans, OfNat.ofNat, DFunLike.coe, iInf_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
simp : ∀ (i : ℕ), (⇑f : (a : α) → α)^[i + 1] a ≤ ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i] a
⊢ LE.le.{u_1} (α := α) (⨆ (j : ℕ), (⇑f : (a : α) → α)^[j + HAdd.hAdd (α := ℕ) 0 1] a)
    (⨆ (i : ℕ), (⇑f : (a : α) → α)^[i] a)

Tactic:
simp only [zero_add, iSup_le_iff]

Premises used: zero_add, iSup_le_iff
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ∀ (i : ℕ), (⇑f : (a : α) → α)^[i + 1] a ≤ ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i] a

Tactic:
fun i => le_iSup (fun i => f^[i] a) (i + 1)

Premises used: le_iSup, Nat.iterate, HAdd.hAdd, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ∀ (i : ℕ), (⇑f : (a : α) → α)^[i + 1] a ≤ ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i] a

Tactic:
exact fun i => le_iSup (fun i => f^[i] a) (i + 1)

Premises used: le_iSup, Nat.iterate, HAdd.hAdd, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ Eq (α := α) ((f : (a : α) → α) (liminf (fun (n : ℕ) ↦ (⇑f : (a : α) → α)^[n] a) atTop) : α)
    (liminf (fun (n : ℕ) ↦ (⇑f : (a : α) → α)^[n] a) atTop : α)

Tactic:
(CompleteLatticeHom.dual f).apply_limsup_iterate _

Premises used: Filter.limsSup, Filter.limsInf, CompleteLatticeHom.apply_limsup_iterate, Filter.liminf, setOf, Filter.limsup, CompleteLatticeHom.dual, OrderDual, DFunLike.coe
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ (x : β), p x → q x
a : α
ha : Membership.mem (γ := Set α) {a : α | ∀ᶠ (x : β) in f, q x → u x ≤ a} a
tauto tauto₁ tauto₂ : ∀ (x : β), (q x → u x ≤ a) → p x → u x ≤ a
inl : ∀ (x : β), p x → ¬q x → u x ≤ a
inr : ∀ (x : β), p x → u x ≤ a → u x ≤ a
inl₁ : ∀ (x : β), p x → ¬q x → u x ≤ a
inr₁ : ∀ (x : β), p x → u x ≤ a → u x ≤ a
inl₂ : ∀ (x : β), p x → ¬q x → u x ≤ a
inr₂ : ∀ (x : β), p x → u x ≤ a → u x ≤ a
inl₃ inl₄ inl₅ inl₆ inl₇ : ∀ (x : β), p x → ¬q x → u x ≤ a
⊢ ∀ (x : β), (q x → u x ≤ a) → p x → u x ≤ a

Tactic:
tauto
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ (x : β), p x → q x
a : α
ha : Membership.mem (γ := Set α) {a : α | ∀ᶠ (x : β) in f, q x → a ≤ u x} a
tauto tauto₁ tauto₂ : ∀ (x : β), (q x → a ≤ u x) → p x → a ≤ u x
inl : ∀ (x : β), p x → ¬q x → a ≤ u x
inr : ∀ (x : β), p x → a ≤ u x → a ≤ u x
inl₁ : ∀ (x : β), p x → ¬q x → a ≤ u x
inr₁ : ∀ (x : β), p x → a ≤ u x → a ≤ u x
inl₂ : ∀ (x : β), p x → ¬q x → a ≤ u x
inr₂ : ∀ (x : β), p x → a ≤ u x → a ≤ u x
inl₃ inl₄ inl₅ inl₆ inl₇ : ∀ (x : β), p x → ¬q x → a ≤ u x
⊢ ∀ (x : β), (q x → a ≤ u x) → p x → a ≤ u x

Tactic:
tauto
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p : β → Prop
u v : β → α
h : ∀ᶠ (x : β) in f, p x → u x ≤ v x
⊢ blimsup u f p ≤ blimsup v f p

Tactic:
sInf_le_sInf fun _ ha => (ha.and h).mono fun _ hx hx' => (hx.2 hx').trans (hx.1 hx')

Premises used: sInf_le_sInf, Filter.blimsup, Filter.Eventually.and, Filter.Eventually.mono, And.right, And.left, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p : β → Prop
u v : β → α
h : ∀ (x : β), p x → u x ≤ v x
⊢ blimsup u f p ≤ blimsup v f p

Tactic:
mono_blimsup' <| Eventually.of_forall h

Premises used: Filter.Eventually.of_forall, Filter.mono_blimsup'
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p : β → Prop
u v : β → α
h : ∀ᶠ (x : β) in f, p x → u x ≤ v x
⊢ bliminf u f p ≤ bliminf v f p

Tactic:
sSup_le_sSup fun _ ha => (ha.and h).mono fun _ hx hx' => (hx.1 hx').trans (hx.2 hx')

Premises used: Filter.bliminf, Filter.Eventually.and, Filter.Eventually.mono, And.right, And.left, LE.le.trans, sSup_le_sSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p : β → Prop
u v : β → α
h : ∀ (x : β), p x → u x ≤ v x
⊢ bliminf u f p ≤ bliminf v f p

Tactic:
mono_bliminf' <| Eventually.of_forall h

Premises used: Filter.Eventually.of_forall, Filter.mono_bliminf'
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f g : Filter β
p : β → Prop
u : β → α
h : f ≤ g
⊢ bliminf u g p ≤ bliminf u f p

Tactic:
sSup_le_sSup fun _ ha => ha.filter_mono h

Premises used: Filter.Eventually.filter_mono, Filter.bliminf, sSup_le_sSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f g : Filter β
p : β → Prop
u : β → α
h : f ≤ g
⊢ blimsup u f p ≤ blimsup u g p

Tactic:
sInf_le_sInf fun _ ha => ha.filter_mono h

Premises used: Filter.Eventually.filter_mono, sInf_le_sInf, Filter.blimsup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
tauto tauto₁ tauto₂ : ∀ (x : β), p x ∧ q x → p x
tauto₃ tauto₄ tauto₅ : ∀ (x : β), p x → q x → p x
⊢ ∀ (x : β), p x ∧ q x → p x

Tactic:
tauto
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
tauto tauto₁ tauto₂ : ∀ (x : β), p x ∧ q x → q x
tauto₃ tauto₄ tauto₅ : ∀ (x : β), p x → q x → q x
⊢ ∀ (x : β), p x ∧ q x → q x

Tactic:
tauto
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (blimsup u f fun (x : β) ↦ p x ∧ q x) ≤ blimsup u f p

Tactic:
blimsup_and_le_inf.trans inf_le_left

Premises used: Filter.blimsup_and_le_inf, inf_le_left, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (blimsup u f fun (x : β) ↦ p x ∧ q x) ≤ blimsup u f q

Tactic:
blimsup_and_le_inf.trans inf_le_right

Premises used: Filter.blimsup_and_le_inf, inf_le_right, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ bliminf u f p ⊔ bliminf u f q ≤ bliminf u f fun (x : β) ↦ p x ∧ q x

Tactic:
blimsup_and_le_inf (α := αᵒᵈ)

Premises used: Filter.blimsup_and_le_inf, setOf, Filter.bliminf, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ bliminf u f p ≤ bliminf u f fun (x : β) ↦ p x ∧ q x

Tactic:
le_sup_left.trans bliminf_sup_le_and

Premises used: Filter.bliminf_sup_le_and, le_sup_left, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ bliminf u f q ≤ bliminf u f fun (x : β) ↦ p x ∧ q x

Tactic:
le_sup_right.trans bliminf_sup_le_and

Premises used: Filter.bliminf_sup_le_and, le_sup_right, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
tauto tauto₁ tauto₂ tauto₃ tauto₄ : ∀ (x : β), p x → p x ∨ q x
tauto₅ tauto₆ : ∀ (x : β), p x → ¬p x → q x
⊢ ∀ (x : β), p x → p x ∨ q x

Tactic:
tauto
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
tauto tauto₁ tauto₂ tauto₃ tauto₄ : ∀ (x : β), q x → p x ∨ q x
tauto₅ : ∀ (x : β), q x → ¬p x → q x
⊢ ∀ (x : β), q x → p x ∨ q x

Tactic:
tauto
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ blimsup u f p ≤ blimsup u f fun (x : β) ↦ p x ∨ q x

Tactic:
le_sup_left.trans blimsup_sup_le_or

Premises used: le_sup_left, Filter.blimsup_sup_le_or, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ blimsup u f q ≤ blimsup u f fun (x : β) ↦ p x ∨ q x

Tactic:
le_sup_right.trans blimsup_sup_le_or

Premises used: le_sup_right, Filter.blimsup_sup_le_or, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (bliminf u f fun (x : β) ↦ p x ∨ q x) ≤ bliminf u f p ⊓ bliminf u f q

Tactic:
blimsup_sup_le_or (α := αᵒᵈ)

Premises used: setOf, Filter.bliminf, Filter.blimsup_sup_le_or, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (bliminf u f fun (x : β) ↦ p x ∨ q x) ≤ bliminf u f p

Tactic:
bliminf_or_le_inf.trans inf_le_left

Premises used: Filter.bliminf_or_le_inf, inf_le_left, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (bliminf u f fun (x : β) ↦ p x ∨ q x) ≤ bliminf u f q

Tactic:
bliminf_or_le_inf.trans inf_le_right

Premises used: Filter.bliminf_or_le_inf, inf_le_right, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst_1 : CompleteLattice γ
e : α ≃o γ
⊢ Eq.{u_3 + 1} (α := γ) ((e : (a : α) → γ) (blimsup u f p) : γ) (blimsup ((⇑e : (a : α) → γ) ∘ u) f p : γ)

Tactic:
simp only [blimsup_eq, map_sInf, Function.comp_apply, e.image_eq_preimage_symm,
    Set.preimage_setOf_eq, e.le_symm_apply]

Premises used: sInfHomClass.map_sInf, Filter.blimsup_eq, Set.preimage_setOf_eq, OrderIso.le_symm_apply, Function.comp_apply, OrderIso.image_eq_preimage_symm
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst_1 : CompleteLattice γ
e : α ≃o γ
⊢ Eq.{u_3 + 1} (α := γ) ((e : (a : α) → γ) (bliminf u f p) : γ) (bliminf ((⇑e : (a : α) → γ) ∘ u) f p : γ)

Tactic:
e.dual.apply_blimsup

Premises used: setOf, Filter.bliminf, OrderIso.dual, OrderIso.apply_blimsup, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst_1 : CompleteLattice γ
g : sSupHom α γ
simp :
  LE.le.{u_3} (α := γ) ((g : (a : α) → γ) (⨅ s ∈ f, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), u b) : γ)
    (⨅ s ∈ f, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), (g : (a : α) → γ) (u b) : γ)
⊢ LE.le.{u_3} (α := γ) ((g : (a : α) → γ) (blimsup u f p) : γ) (blimsup ((⇑g : (a : α) → γ) ∘ u) f p : γ)

Tactic:
simp only [blimsup_eq_iInf_biSup, Function.comp]

Premises used: Function.comp, Filter.blimsup_eq_iInf_biSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst_1 : CompleteLattice γ
g : sSupHom α γ
⊢ LE.le.{u_3} (α := γ) ((g : (a : α) → γ) (⨅ s ∈ f, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), u b) : γ)
    (⨅ s ∈ f, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), (g : (a : α) → γ) (u b) : γ)

Tactic:
((OrderHomClass.mono g).map_iInf₂_le _).trans ?_

Premises used: OrderHomClass.mono, LE.le.trans, Monotone.map_iInf₂_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst_1 : CompleteLattice γ
g : sSupHom α γ
refine :
  LE.le.{u_3} (α := γ) (⨅ i ∈ f, (g : (a : α) → γ) (⨆ (b : β), ⨆ (_ : p b ∧ b ∈ i), u b))
    (⨅ s ∈ f, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), (g : (a : α) → γ) (u b))
⊢ LE.le.{u_3} (α := γ) ((g : (a : α) → γ) (⨅ s ∈ f, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), u b) : γ)
    (⨅ s ∈ f, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), (g : (a : α) → γ) (u b) : γ)

Tactic:
refine ((OrderHomClass.mono g).map_iInf₂_le _).trans ?_

Premises used: OrderHomClass.mono, LE.le.trans, Monotone.map_iInf₂_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst_1 : CompleteLattice γ
g : sSupHom α γ
⊢ LE.le.{u_3} (α := γ) (⨅ i ∈ f, (g : (a : α) → γ) (⨆ (b : β), ⨆ (_ : p b ∧ b ∈ i), u b))
    (⨅ s ∈ f, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), (g : (a : α) → γ) (u b))

Tactic:
simp only [_root_.map_iSup, le_refl]

Premises used: le_refl, map_iSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst_1 : CompleteLattice γ
g : sInfHom α γ
⊢ LE.le.{u_3} (α := γ) (bliminf ((⇑g : (a : α) → γ) ∘ u) f p : γ) ((g : (a : α) → γ) (bliminf u f p) : γ)

Tactic:
(sInfHom.dual g).apply_blimsup_le

Premises used: sInfHom.dual, setOf, Filter.blimsup, Filter.bliminf, OrderDual, sSupHom.apply_blimsup_le, DFunLike.coe
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ limsup u (f ⊔ g) = limsup u f ⊔ limsup u g

Tactic:
le_antisymm ?_
    (sup_le (limsup_le_limsup_of_le le_sup_left) (limsup_le_limsup_of_le le_sup_right))

Premises used: le_sup_left, le_sup_right, le_antisymm, sup_le, Filter.limsup_le_limsup_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
refine : limsup u (f ⊔ g) ≤ limsup u f ⊔ limsup u g
⊢ limsup u (f ⊔ g) = limsup u f ⊔ limsup u g

Tactic:
refine le_antisymm ?_
    (sup_le (limsup_le_limsup_of_le le_sup_left) (limsup_le_limsup_of_le le_sup_right))

Premises used: le_sup_left, le_sup_right, le_antisymm, sup_le, Filter.limsup_le_limsup_of_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
simp_rw :
  ∀ (i : α) (j : ∀ᶠ (n : β) in f, u n ≤ i) (i_1 : α) (j : ∀ᶠ (n : β) in g, u n ≤ i_1),
    sInf {a : α | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ i ⊔ i_1
⊢ limsup u (f ⊔ g) ≤ limsup u f ⊔ limsup u g

Tactic:
simp_rw [limsup_eq, sInf_sup_eq, sup_sInf_eq, mem_setOf_eq, le_iInf₂_iff]

Premises used: Set.mem_setOf_eq, le_iInf₂_iff, sInf_sup_eq, sup_sInf_eq, Filter.limsup_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
a : α
ha : ∀ᶠ (n : β) in f, u n ≤ a
b : α
hb : ∀ᶠ (n : β) in g, u n ≤ b
⊢ sInf {a : α | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ a ⊔ b

Tactic:
sInf_le ⟨ha.mono fun _ h ↦ h.trans le_sup_left, hb.mono fun _ h ↦ h.trans le_sup_right⟩

Premises used: le_sup_left, le_sup_right, Filter.Eventually.mono, sInf_le, And.intro, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
a : α
ha : ∀ᶠ (n : β) in f, u n ≤ a
b : α
hb : ∀ᶠ (n : β) in g, u n ≤ b
⊢ sInf {a : α | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ a ⊔ b

Tactic:
exact sInf_le ⟨ha.mono fun _ h ↦ h.trans le_sup_left, hb.mono fun _ h ↦ h.trans le_sup_right⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ liminf u (f ⊔ g) = liminf u f ⊓ liminf u g

Tactic:
limsup_sup_filter (α := αᵒᵈ)

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.limsup_sup_filter, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
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

Tactic:
simp only [blimsup_eq_limsup, ← limsup_sup_filter, ← inf_sup_left, sup_principal, setOf_or]

Premises used: Filter.sup_principal, Filter.blimsup_eq_limsup, Filter.limsup_sup_filter, inf_sup_left, Set.setOf_or
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (bliminf u f fun (x : β) ↦ p x ∨ q x) = bliminf u f p ⊓ bliminf u f q

Tactic:
blimsup_or_eq_sup (α := αᵒᵈ)

Premises used: setOf, Filter.bliminf, OrderDual, Filter.blimsup_or_eq_sup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
simp_rw : (blimsup u f fun (x : β) ↦ p x ∨ ¬p x) = limsup u f
simp_rw₁ : (blimsup u f fun (x : β) ↦ True) = limsup u f
⊢ (blimsup u f p ⊔ blimsup u f fun (x : β) ↦ ¬p x) = limsup u f

Tactic:
simp_rw [← blimsup_or_eq_sup, or_not, blimsup_true]

Premises used: Filter.blimsup_true, or_not, Filter.blimsup_or_eq_sup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (bliminf u f p ⊓ bliminf u f fun (x : β) ↦ ¬p x) = liminf u f

Tactic:
blimsup_sup_not (α := αᵒᵈ)

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.bliminf, Filter.blimsup_sup_not, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (blimsup u f fun (x : β) ↦ ¬p x) ⊔ blimsup u f p = limsup u f

Tactic:
simpa only [not_not] using blimsup_sup_not (p := (¬p ·))

Premises used: Classical.not_not, Filter.blimsup_sup_not
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (bliminf u f fun (x : β) ↦ ¬p x) ⊓ bliminf u f p = liminf u f

Tactic:
blimsup_not_sup (α := αᵒᵈ)

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.bliminf, Filter.blimsup_not_sup, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst_1 : DecidablePred fun (x : β) ↦ x ∈ s
v : (i : β) → α
rw :
  ((blimsup (s.piecewise (β := fun (a : β) ↦ α) u v) f fun (x : β) ↦ x ∈ s) ⊔
      blimsup (s.piecewise (β := fun (a : β) ↦ α) u v) f fun (x : β) ↦ x ∉ s) =
    (blimsup u f fun (x : β) ↦ x ∈ s) ⊔ blimsup v f fun (x : β) ↦ x ∉ s
⊢ limsup (s.piecewise (β := fun (a : β) ↦ α) u v) f =
    (blimsup u f fun (x : β) ↦ x ∈ s) ⊔ blimsup v f fun (x : β) ↦ x ∉ s

Tactic:
rw [← blimsup_sup_not (p := (· ∈ s))]

Premises used: Filter.blimsup_sup_not
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst_1 : DecidablePred fun (x : β) ↦ x ∈ s
v : (i : β) → α
⊢ ((blimsup (s.piecewise (β := fun (a : β) ↦ α) u v) f fun (x : β) ↦ x ∈ s) ⊔
      blimsup (s.piecewise (β := fun (a : β) ↦ α) u v) f fun (x : β) ↦ x ∉ s) =
    (blimsup u f fun (x : β) ↦ x ∈ s) ⊔ blimsup v f fun (x : β) ↦ x ∉ s

Tactic:
congr_arg₂ _ (blimsup_congr ?_) (blimsup_congr ?_)

Premises used: Filter.blimsup_congr, congr_arg₂
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst_1 : DecidablePred fun (x : β) ↦ x ∈ s
v : (i : β) → α
refine_1 : ∀ᶠ (a : β) in f, a ∈ s → s.piecewise (β := fun (a : β) ↦ α) u v a = u a
refine_2 : ∀ᶠ (a : β) in f, a ∉ s → s.piecewise (β := fun (a : β) ↦ α) u v a = v a
⊢ ((blimsup (s.piecewise (β := fun (a : β) ↦ α) u v) f fun (x : β) ↦ x ∈ s) ⊔
      blimsup (s.piecewise (β := fun (a : β) ↦ α) u v) f fun (x : β) ↦ x ∉ s) =
    (blimsup u f fun (x : β) ↦ x ∈ s) ⊔ blimsup v f fun (x : β) ↦ x ∉ s

Tactic:
refine congr_arg₂ _ (blimsup_congr ?_) (blimsup_congr ?_)

Premises used: Filter.blimsup_congr, congr_arg₂
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst_1 : DecidablePred fun (x : β) ↦ x ∈ s
v : (i : β) → α
a : β
h : a ∈ s
⊢ s.piecewise (β := fun (a : β) ↦ α) u v a = u a

Tactic:
simp [h]
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst_1 : DecidablePred fun (x : β) ↦ x ∈ s
v : (i : β) → α
refine_1 :
  ∀ (a : β),
    Membership.mem (γ := Set β) {x : β | (fun (a : β) ↦ a ∈ s → s.piecewise (β := fun (a : β) ↦ α) u v a = u a) x} a
refine_1₁ refine_1₂ : ∀ (a : β) (h : a ∈ s), s.piecewise (β := fun (a : β) ↦ α) u v a = u a
⊢ ∀ᶠ (a : β) in f, a ∈ s → s.piecewise (β := fun (a : β) ↦ α) u v a = u a

Tactic:
filter_upwards with _ h using by simp [h]
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst_1 : DecidablePred fun (x : β) ↦ x ∈ s
v : (i : β) → α
a : β
h : a ∉ s
⊢ s.piecewise (β := fun (a : β) ↦ α) u v a = v a

Tactic:
simp [h]