awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ Eq.{u_1 + 1} (α := α) (sInf {a : α | ∀ᶠ (x : β) in f, p x → u x ≤ a}) (sInf {a : α | ∀ᶠ (x : β) in f, q x → u x ≤ a})
have e_a : ∀ (a : α), (∀ᶠ (x : β) in f, p x → u x ≤ a) ↔ ∀ᶠ (x : β) in f, q x → u x ≤ a
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
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) ↔ ∀ᶠ (x : β) in f, q x → u x ≤ a
have e_a : ∀ (b : β) (hb : u b ≠ ⊥ → (p b ↔ q b)), p b → u b ≤ a ↔ q b → u b ≤ a
Tactic: refine eventually_congr (h.mono fun b hb => ?_)
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
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
have e_a : ∀ (hu : u b = ⊥), p b → u b ≤ a ↔ q b → u b ≤ a
Tactic: rcases eq_or_ne (u b) ⊥ with hu | hu
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
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)
e_a : ∀ (hu : u b = ⊥), p b → u b ≤ a ↔ q b → u b ≤ a
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
have e_a₁ : ∀ (hu : u b ≠ ⊥), p b → u b ≤ a ↔ q b → u b ≤ a
Tactic: rcases eq_or_ne (u b) ⊥ with hu | hu
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
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
have e_a : q b → u b ≤ a ↔ q b → u b ≤ a
Tactic: rw [hb hu]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
⊢ limsup a F = sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets)
have a₁ : limsup a F ≤ sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
a₁ : limsup a F ≤ sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets)
⊢ limsup a F = sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets)
have a₂ : sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
⊢ limsup a F ≤ sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets)
have a₁ : LE.le.{u_7} (α := R) (sInf {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1}) (sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets))
Tactic: rw [limsup_eq]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
⊢ LE.le.{u_7} (α := R) (sInf {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1})
    (sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets))
have a₁ : ∀ (x : R) (hx : Membership.mem (γ := Set R) ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) x),
  Membership.mem (γ := Set R) {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1} x
Tactic: refine sInf_le_sInf fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
x : R
hx : Membership.mem (γ := Set R) ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) x
⊢ Membership.mem (γ := Set R) {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1} x
have a₁ : ∀ (I : Set ι) (I_mem_F : I ∈ F.sets) (hI : sSup (a '' I) = x),
  Membership.mem (γ := Set R) {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1} x
Tactic: rcases (mem_image _ F.sets x).mp hx with ⟨I, ⟨I_mem_F, hI⟩⟩
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
x : R
hx : Membership.mem (γ := Set R) ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) x
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
⊢ Membership.mem (γ := Set R) {a_1 : R | ∀ᶠ (n : ι) in F, a n ≤ a_1} x
have h : ∀ (i : ι) (hi : i ∈ I), a i ≤ x
Tactic: filter_upwards [I_mem_F] with i hi
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
ι : Type u_6
R : Type u_7
F : Filter ι
inst : CompleteLattice R
a : ι → R
⊢ sInf ((fun (I : Set ι) ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F
have a₁ : ∀ (b : R) (hb : Membership.mem (γ := Set R) {a_1 : R | ∀ᶠ (n : R) in map a F, n ≤ a_1} b),
  ∀ b_1 ∈ a '' a ⁻¹' {x : R | (fun (n : R) ↦ n ≤ b) x}, b_1 ≤ b
Tactic: refine le_sInf fun b hb => sInf_le_of_le (mem_image_of_mem _ hb) <| sSup_le ?_
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ liminf u f ≤ x
have rw : sSup {a : β | ∀ᶠ (n : α) in f, a ≤ u n} ≤ x
Tactic: rw [liminf_eq]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ sSup {a : β | ∀ᶠ (n : α) in f, a ≤ u n} ≤ x
have refine : ∀ (b : β) (hb : Membership.mem (γ := Set β) {a : β | ∀ᶠ (n : α) in f, a ≤ u n} b), b ≤ x
Tactic: refine sSup_le fun b hb => ?_
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : Membership.mem (γ := Set β) {a : β | ∀ᶠ (n : α) in f, a ≤ u n} b
⊢ ∃ᶠ (x_1 : α) in f, b ≤ x
have contrapose! : ∀ (h : ∀ᶠ (x_1 : α) in f, ¬b ≤ x), ∀ᶠ (x_1 : α) in f, ¬u x_1 ≤ x
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
Goal:
α : Type u_6
β : Type u_7
inst : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : Membership.mem (γ := Set β) {a : β | ∀ᶠ (n : α) in f, a ≤ u n} b
⊢ b ≤ x
have hbx : ∃ᶠ (x_1 : α) in f, b ≤ x
Tactic: have hbx : ∃ᶠ _ in f, b ≤ x := by
    contrapose! h
    exact hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ Eq (α := α) ((f : (a : α) → α) (limsup (fun (n : ℕ) ↦ (⇑f : (a : α) → α)^[n] a) atTop) : α)
    (limsup (fun (n : ℕ) ↦ (⇑f : (a : α) → α)^[n] a) atTop : α)
have rw : Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), (f : (a : α) → α) (⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i] a))
  (⨅ (n : ℕ), ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i + n] a)
Tactic: rw [limsup_eq_iInf_iSup_of_nat', map_iInf]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), (f : (a : α) → α) (⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i] a))
    (⨅ (n : ℕ), ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i + n] a)
have simp_rw : Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i.succ] 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]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
| ⨅ (n : ℕ), ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i + n] a
have rw : (⨅ (i : ℕ), ⨅ (_ : 0 < i), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i] a) ⊓
  ⨅ (i : ℕ), ⨅ (_ : ¬0 < i), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i] a
Tactic: rw [iInf_split _ (0 < ·)]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i.succ] a)
    (⨅ (n : ℕ), ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i + n] a)
have 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)
Tactic: conv_rhs => rw [iInf_split _ (0 < ·)]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
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)
have simp : LE.le.{u_1} (α := α) (⨅ (i : ℕ), ⨆ (i_1 : ℕ), (⇑f : (a : α) → α)^[i_1 + i.succ] a) (⨆ (i : ℕ), (⇑f : (a : α) → α)^[i] a)
Tactic: simp only [not_lt, Nat.le_zero, iInf_iInf_eq_left, add_zero, iInf_nat_gt_zero_eq, left_eq_inf]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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)
have refine : LE.le.{u_1} (α := α) (⨆ (j : ℕ), (⇑f : (a : α) → α)^[j + HAdd.hAdd (α := ℕ) 0 1] a)
  (⨆ (i : ℕ), (⇑f : (a : α) → α)^[i] a)
Tactic: refine (iInf_le (fun i => ⨆ j, f^[j + (i + 1)] a) 0).trans ?_
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ LE.le.{u_1} (α := α) (⨆ (j : ℕ), (⇑f : (a : α) → α)^[j + HAdd.hAdd (α := ℕ) 0 1] a)
    (⨆ (i : ℕ), (⇑f : (a : α) → α)^[i] a)
have simp : ∀ (i : ℕ), (⇑f : (a : α) → α)^[i + 1] a ≤ ⨆ (i : ℕ), (⇑f : (a : α) → α)^[i] a
Tactic: simp only [zero_add, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∀ (x : β), (q x → u x ≤ a) → p x → u x ≤ a
have inl : ∀ (x : β), p x → ¬q x → u x ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∀ (x : β), (q x → u x ≤ a) → p x → u x ≤ a
have inr : ∀ (x : β), p x → u x ≤ a → u x ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∀ (x : β), (q x → a ≤ u x) → p x → a ≤ u x
have inl : ∀ (x : β), p x → ¬q x → a ≤ u x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∀ (x : β), (q x → a ≤ u x) → p x → a ≤ u x
have inr : ∀ (x : β), p x → a ≤ u x → a ≤ u x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∀ (x : β), p x ∧ q x → p x
have tauto₃ : ∀ (x : β), p x → q x → p x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∀ (x : β), p x ∧ q x → q x
have tauto₃ : ∀ (x : β), p x → q x → q x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∀ (x : β), p x → p x ∨ q x
have tauto₅ : ∀ (x : β), p x → ¬p x → q x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∀ (x : β), q x → p x ∨ q x
have tauto₅ : ∀ (x : β), q x → ¬p x → q x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : α) → γ) (blimsup u f p) : γ) (blimsup ((⇑g : (a : α) → γ) ∘ u) f p : γ)
have 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) : γ)
Tactic: simp only [blimsup_eq_iInf_biSup, Function.comp]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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) : γ)
have 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))
Tactic: refine ((OrderHomClass.mono g).map_iInf₂_le _).trans ?_
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ limsup u (f ⊔ g) = limsup u f ⊔ limsup u g
have refine : 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))
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ limsup u (f ⊔ g) ≤ limsup u f ⊔ limsup u g
have 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
Tactic: simp_rw [limsup_eq, sInf_sup_eq, sup_sInf_eq, mem_setOf_eq, le_iInf₂_iff]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (blimsup u f p ⊔ blimsup u f fun (x : β) ↦ ¬p x) = limsup u f
have simp_rw : (blimsup u f fun (x : β) ↦ p x ∨ ¬p x) = limsup u f
Tactic: simp_rw [← blimsup_or_eq_sup, or_not, blimsup_true]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ (blimsup u f p ⊔ blimsup u f fun (x : β) ↦ ¬p x) = limsup u f
have simp_rw₁ : (blimsup u f fun (x : β) ↦ True) = limsup u f
Tactic: simp_rw [← blimsup_or_eq_sup, or_not, blimsup_true]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst_1 : DecidablePred fun (x : β) ↦ x ∈ s
v : (i : β) → α
⊢ limsup (s.piecewise (β := fun (a : β) ↦ α) u v) f =
    (blimsup u f fun (x : β) ↦ x ∈ s) ⊔ blimsup v f fun (x : β) ↦ x ∉ s
have 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
Tactic: rw [← blimsup_sup_not (p := (· ∈ s))]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
have refine_1 : ∀ᶠ (a : β) in f, a ∈ s → s.piecewise (β := fun (a : β) ↦ α) u v a = u a
Tactic: refine congr_arg₂ _ (blimsup_congr ?_) (blimsup_congr ?_)
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ((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
have refine_2 : ∀ᶠ (a : β) in f, a ∉ s → s.piecewise (β := fun (a : β) ↦ α) u v a = v a
Tactic: refine congr_arg₂ _ (blimsup_congr ?_) (blimsup_congr ?_)
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst_1 : DecidablePred fun (x : β) ↦ x ∈ s
v : (i : β) → α
⊢ ∀ᶠ (a : β) in f, a ∈ s → s.piecewise (β := fun (a : β) ↦ α) u v a = u a
have refine_1 : ∀ (a : β),
  Membership.mem (γ := Set β) {x : β | (fun (a : β) ↦ a ∈ s → s.piecewise (β := fun (a : β) ↦ α) u v a = u a) x} a
Tactic: filter_upwards with _ h using by simp [h]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ ∀ᶠ (a : β) in f, a ∈ s → s.piecewise (β := fun (a : β) ↦ α) u v a = u a
have refine_1₁ : ∀ a ∈ s, s.piecewise (β := fun (a : β) ↦ α) u v a = u a
Tactic: filter_upwards with _ h using by simp [h]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst_1 : DecidablePred fun (x : β) ↦ x ∈ s
v : (i : β) → α
⊢ ∀ᶠ (a : β) in f, a ∉ s → s.piecewise (β := fun (a : β) ↦ α) u v a = v a
have refine_2 : ∀ (a : β),
  Membership.mem (γ := Set β) {x : β | (fun (a : β) ↦ a ∉ s → s.piecewise (β := fun (a : β) ↦ α) u v a = v a) x} a
Tactic: filter_upwards with _ h using by simp [h]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst_1 : DecidablePred fun (x : β) ↦ x ∈ s
v : (i : β) → α
refine_2 :
  ∀ (a : β),
    Membership.mem (γ := Set β) {x : β | (fun (a : β) ↦ a ∉ s → s.piecewise (β := fun (a : β) ↦ α) u v a = v a) x} a
⊢ ∀ᶠ (a : β) in f, a ∉ s → s.piecewise (β := fun (a : β) ↦ α) u v a = v a
have refine_2₁ : ∀ a ∉ s, s.piecewise (β := fun (a : β) ↦ α) u v a = v a
Tactic: filter_upwards with _ h using by simp [h]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
⊢ a ⊔ limsup u f = limsup (fun (x : β) ↦ a ⊔ u x) f
have simp : Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, a ⊔ ⨆ a ∈ i, u a) (⨅ s ∈ f, (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x)
Tactic: simp only [limsup_eq_iInf_iSup, iSup_sup_eq, sup_iInf₂_eq]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
⊢ Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, a ⊔ ⨆ a ∈ i, u a) (⨅ s ∈ f, (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x)
have e_s : Eq (α := Set β → α) (fun (i : Set β) ↦ ⨅ (_ : i ∈ f), a ⊔ ⨆ a ∈ i, u a) fun (s : Set β) ↦
  ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
⊢ Eq (α := Set β → α) (fun (i : Set β) ↦ ⨅ (_ : i ∈ f), a ⊔ ⨆ a ∈ i, u a) fun (s : Set β) ↦
    ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
have e_s : ∀ (s : Set β), Eq.{u_1 + 1} (α := α) (⨅ (_ : s ∈ f), a ⊔ ⨆ a ∈ s, u a) (⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
s : Set β
⊢ Eq.{u_1 + 1} (α := α) (⨅ (_ : s ∈ f), a ⊔ ⨆ a ∈ s, u a) (⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x)
have e_s : Eq.{u_1 + 1} (α := s ∈ f → α) (fun (j : s ∈ f) ↦ a ⊔ ⨆ a ∈ s, u a) fun (x : s ∈ f) ↦ (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
s : Set β
⊢ Eq.{u_1 + 1} (α := s ∈ f → α) (fun (j : s ∈ f) ↦ a ⊔ ⨆ a ∈ s, u a) fun (x : s ∈ f) ↦ (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
have e_s : ∀ (hs : s ∈ f), a ⊔ ⨆ a ∈ s, u a = (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
Tactic: ext hs
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
s : Set β
hs : s ∈ f
⊢ a ⊔ ⨆ a ∈ s, u a = (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
have e_s : a = ⨆ x ∈ s, a
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ a ⊔ liminf u f = liminf (fun (x : β) ↦ a ⊔ u x) f
have simp : a ⊔ ⨆ s ∈ f, ⨅ a ∈ s, u a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1
Tactic: simp only [liminf_eq_iSup_iInf]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ a ⊔ ⨆ s ∈ f, ⨅ a ∈ s, u a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1
have rw : Eq.{u_1 + 1} (α := α) (⨆ i ∈ f, (⨅ a ∈ i, u a) ⊔ a) (⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1)
Tactic: rw [sup_comm, biSup_sup (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f, (⨅ a ∈ i, u a) ⊔ a) (⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1)
have simp_rw : Eq.{u_1 + 1} (α := α) (⨆ i ∈ f, ⨅ i_1 ∈ i, u i_1 ⊔ a) (⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1)
Tactic: simp_rw [iInf₂_sup_eq, sup_comm (a := a)]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ limsup u f \ a = limsup (fun (b : β) ↦ u b \ a) f
have simp : (⨅ s ∈ f, ⨆ a ∈ s, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ
Tactic: simp only [limsup_eq_iInf_iSup, sdiff_eq]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (⨅ s ∈ f, ⨆ a ∈ s, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ
have rw : Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, (⨆ a ∈ i, u a) ⊓ aᶜ) (⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ)
Tactic: rw [biInf_inf (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, (⨆ a ∈ i, u a) ⊓ aᶜ) (⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ)
have simp_rw : Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, aᶜ ⊓ ⨆ a ∈ i, u a) (⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ)
Tactic: simp_rw [inf_comm, inf_iSup₂_eq, inf_comm]