awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderTop α
a : α
x y : (↑(Ici a) : Type u_1)
⊢ IsCompl x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)
have rw : Disjoint x y ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)
Tactic: rw [_root_.isCompl_iff, Ici.disjoint_iff, Ici.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderTop α
a : α
x y : (↑(Ici a) : Type u_1)
rw : Disjoint x y ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)
⊢ IsCompl x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)
have rw₁ : (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)
Tactic: rw [_root_.isCompl_iff, Ici.disjoint_iff, Ici.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderTop α
a : α
x y : (↑(Ici a) : Type u_1)
rw : Disjoint x y ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)
rw₁ : (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)
⊢ IsCompl x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)
have rw₂ : (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α) ↔ (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint (↑x : α) (↑y : α)
Tactic: rw [_root_.isCompl_iff, Ici.disjoint_iff, Ici.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
Goal:
α : Type u_1
a b : α
inst : Lattice α
inst_1 : Fact (a ≤ b)
x y : (↑(Icc a b) : Type u_1)
⊢ IsCompl x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b
have rw : Disjoint x y ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b
Tactic: rw [_root_.isCompl_iff, Icc.disjoint_iff, Icc.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
Goal:
α : Type u_1
a b : α
inst : Lattice α
inst_1 : Fact (a ≤ b)
x y : (↑(Icc a b) : Type u_1)
rw : Disjoint x y ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b
⊢ IsCompl x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b
have rw₁ : (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b
Tactic: rw [_root_.isCompl_iff, Icc.disjoint_iff, Icc.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.LatticeIntervals (goal)
Goal:
α : Type u_1
a b : α
inst : Lattice α
inst_1 : Fact (a ≤ b)
x y : (↑(Icc a b) : Type u_1)
rw : Disjoint x y ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b
rw₁ : (↑x : α) ⊓ (↑y : α) = a ∧ Codisjoint x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b
⊢ IsCompl x y ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b
have rw₂ : (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b ↔ (↑x : α) ⊓ (↑y : α) = a ∧ (↑x : α) ⊔ (↑y : α) = b
Tactic: rw [_root_.isCompl_iff, Icc.disjoint_iff, Icc.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
have rw : limsup u (f ⊓ 𝓟 {x : β | p x}) =
  limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
    (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
    (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
Tactic: rw [blimsup_eq_limsup, limsup, limsup, ← map_map, map_comap_setCoe_val]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
rw :
  limsup u (f ⊓ 𝓟 {x : β | p x}) =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
⊢ blimsup u f p =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
have rw₁ : (map u (f ⊓ 𝓟 {x : β | p x})).limsSup =
  limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
    (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
    (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
Tactic: rw [blimsup_eq_limsup, limsup, limsup, ← map_map, map_comap_setCoe_val]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
rw :
  limsup u (f ⊓ 𝓟 {x : β | p x}) =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
rw₁ :
  (map u (f ⊓ 𝓟 {x : β | p x})).limsSup =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
⊢ blimsup u f p =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
have rw₂ : (map u (f ⊓ 𝓟 {x : β | p x})).limsSup =
  (map (α := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)).limsSup
Tactic: rw [blimsup_eq_limsup, limsup, limsup, ← map_map, map_comap_setCoe_val]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
rw :
  limsup u (f ⊓ 𝓟 {x : β | p x}) =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
rw₁ :
  (map u (f ⊓ 𝓟 {x : β | p x})).limsSup =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
rw₂ :
  (map u (f ⊓ 𝓟 {x : β | p x})).limsSup =
    (map (α := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
        (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
        (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)).limsSup
⊢ blimsup u f p =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
have rw₃ : (map u (f ⊓ 𝓟 {x : β | p x})).limsSup =
  (map u
      (map (α := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
        (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
        (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f))).limsSup
Tactic: rw [blimsup_eq_limsup, limsup, limsup, ← map_map, map_comap_setCoe_val]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
rw :
  limsup u (f ⊓ 𝓟 {x : β | p x}) =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
rw₁ :
  (map u (f ⊓ 𝓟 {x : β | p x})).limsSup =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
rw₂ :
  (map u (f ⊓ 𝓟 {x : β | p x})).limsSup =
    (map (α := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
        (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
        (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)).limsSup
rw₃ :
  (map u (f ⊓ 𝓟 {x : β | p x})).limsSup =
    (map u
        (map (α := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
          (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
          (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f))).limsSup
⊢ blimsup u f p =
    limsup (β := { x : β // Membership.mem (γ := Set β) {x : β | p x} x })
      (u ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x))
      (comap (Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | p x} x)) f)
have rw₄ : (map u (f ⊓ 𝓟 {x : β | p x})).limsSup = (map u (f ⊓ 𝓟 {x : β | p x})).limsSup
Tactic: rw [blimsup_eq_limsup, limsup, limsup, ← map_map, map_comap_setCoe_val]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
ι : Type u_6
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice β
v : ι → α
u : α → β
f : Filter ι
g : Filter α
hv : Tendsto v f g
hvf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (map v f) u
hg : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) g u
⊢ limsup (u ∘ v) f ≤ limsup u g
have rw : limsup u (map v f) ≤ limsup u g
Tactic: rw [limsup_comp]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : s.Nonempty
⊢ (𝓟 s).limsSup = sSup s
have simp : sInf {a : α | ∀ x ∈ s, x ≤ a} = sSup s
Tactic: simp only [limsSup, eventually_principal]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
u : β → α
inst_1 : Nonempty β
hu : BddAbove (range u)
⊢ limsup u ⊤ = ⨆ (i : β), u i
have rw : (map u ⊤).limsSup = ⨆ (i : β), u i
Tactic: rw [limsup, map_top, limsSup_principal_eq_csSup hu (range_nonempty _), sSup_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
u : β → α
inst_1 : Nonempty β
hu : BddAbove (range u)
rw : (map u ⊤).limsSup = ⨆ (i : β), u i
⊢ limsup u ⊤ = ⨆ (i : β), u i
have rw₁ : (𝓟 (range u)).limsSup = ⨆ (i : β), u i
Tactic: rw [limsup, map_top, limsSup_principal_eq_csSup hu (range_nonempty _), sSup_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
u : β → α
inst_1 : Nonempty β
hu : BddAbove (range u)
rw : (map u ⊤).limsSup = ⨆ (i : β), u i
rw₁ : (𝓟 (range u)).limsSup = ⨆ (i : β), u i
⊢ limsup u ⊤ = ⨆ (i : β), u i
have rw₂ : sSup (range u) = ⨆ (i : β), u i
Tactic: rw [limsup, map_top, limsSup_principal_eq_csSup hu (range_nonempty _), sSup_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
u : β → α
inst_1 : Nonempty β
hu : BddAbove (range u)
rw : (map u ⊤).limsSup = ⨆ (i : β), u i
rw₁ : (𝓟 (range u)).limsSup = ⨆ (i : β), u i
rw₂ : sSup (range u) = ⨆ (i : β), u i
⊢ limsup u ⊤ = ⨆ (i : β), u i
have rw₃ : iSup u = ⨆ (i : β), u i
Tactic: rw [limsup, map_top, limsSup_principal_eq_csSup hu (range_nonempty _), sSup_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
u : β → α
inst_1 : Nonempty β
hu : BddBelow (range u)
⊢ liminf u ⊤ = ⨅ (i : β), u i
have rw : (map u ⊤).limsInf = ⨅ (i : β), u i
Tactic: rw [liminf, map_top, limsInf_principal_eq_csSup hu (range_nonempty _), sInf_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
u : β → α
inst_1 : Nonempty β
hu : BddBelow (range u)
rw : (map u ⊤).limsInf = ⨅ (i : β), u i
⊢ liminf u ⊤ = ⨅ (i : β), u i
have rw₁ : (𝓟 (range u)).limsInf = ⨅ (i : β), u i
Tactic: rw [liminf, map_top, limsInf_principal_eq_csSup hu (range_nonempty _), sInf_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
u : β → α
inst_1 : Nonempty β
hu : BddBelow (range u)
rw : (map u ⊤).limsInf = ⨅ (i : β), u i
rw₁ : (𝓟 (range u)).limsInf = ⨅ (i : β), u i
⊢ liminf u ⊤ = ⨅ (i : β), u i
have rw₂ : sInf (range u) = ⨅ (i : β), u i
Tactic: rw [liminf, map_top, limsInf_principal_eq_csSup hu (range_nonempty _), sInf_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
u : β → α
inst_1 : Nonempty β
hu : BddBelow (range u)
rw : (map u ⊤).limsInf = ⨅ (i : β), u i
rw₁ : (𝓟 (range u)).limsInf = ⨅ (i : β), u i
rw₂ : sInf (range u) = ⨅ (i : β), u i
⊢ liminf u ⊤ = ⨅ (i : β), u i
have rw₃ : iInf u = ⨅ (i : β), u i
Tactic: rw [liminf, map_top, limsInf_principal_eq_csSup hu (range_nonempty _), sInf_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
β : Type u_2
α : Type u_6
inst : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ limsup u f = limsup v f
have rw : sInf {a : β | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f
Tactic: rw [limsup_eq]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
β : Type u_2
α : Type u_6
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
have e_a : ∀ (b : β), (∀ᶠ (n : α) in f, u n ≤ b) ↔ ∀ᶠ (n : β) in map v f, n ≤ b
Tactic: congr with b
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ liminf f v = sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι)))
have simp_rw : Eq.{u_1 + 1} (α := α) (sSup {a : α | ∃ (i : ι'), p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x})
  (sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι))))
Tactic: simp_rw [liminf_eq, hv.eventually_iff]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ Eq.{u_1 + 1} (α := α) (sSup {a : α | ∃ (i : ι'), p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x})
    (sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι))))
have e_a : Eq.{u_1 + 1} (α := Set α) {a : α | ∃ (i : ι'), p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x}
  (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ Eq.{u_1 + 1} (α := Set α) {a : α | ∃ (i : ι'), p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x}
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι)))
have e_a : ∀ (x : α),
  Membership.mem (γ := Set α) {a : α | ∃ (i : ι'), p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} x ↔
    Membership.mem (γ := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_6)), Iic (f (↑i : ι))) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
⊢ liminf (fun (i : ℕ) ↦ f (i + k)) atTop = liminf f atTop
have rw : liminf (β := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop = liminf f atTop
Tactic: rw [← Function.comp_def, liminf, liminf, ← map_map, map_add_atTop_eq_nat]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
rw : liminf (β := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop = liminf f atTop
⊢ liminf (fun (i : ℕ) ↦ f (i + k)) atTop = liminf f atTop
have rw₁ : (map (α := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop).limsInf = liminf f atTop
Tactic: rw [← Function.comp_def, liminf, liminf, ← map_map, map_add_atTop_eq_nat]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
rw : liminf (β := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop = liminf f atTop
rw₁ : (map (α := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop).limsInf = liminf f atTop
⊢ liminf (fun (i : ℕ) ↦ f (i + k)) atTop = liminf f atTop
have rw₂ : (map (α := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop).limsInf = (map f atTop).limsInf
Tactic: rw [← Function.comp_def, liminf, liminf, ← map_map, map_add_atTop_eq_nat]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
rw : liminf (β := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop = liminf f atTop
rw₁ : (map (α := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop).limsInf = liminf f atTop
rw₂ : (map (α := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop).limsInf = (map f atTop).limsInf
⊢ liminf (fun (i : ℕ) ↦ f (i + k)) atTop = liminf f atTop
have rw₃ : (map f (map (fun (i : ℕ) ↦ i + k) atTop)).limsInf = (map f atTop).limsInf
Tactic: rw [← Function.comp_def, liminf, liminf, ← map_map, map_add_atTop_eq_nat]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
rw : liminf (β := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop = liminf f atTop
rw₁ : (map (α := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop).limsInf = liminf f atTop
rw₂ : (map (α := ℕ) (f ∘ fun (i : ℕ) ↦ i + k) atTop).limsInf = (map f atTop).limsInf
rw₃ : (map f (map (fun (i : ℕ) ↦ i + k) atTop)).limsInf = (map f atTop).limsInf
⊢ liminf (fun (i : ℕ) ↦ f (i + k)) atTop = liminf f atTop
have rw₄ : (map f atTop).limsInf = (map f atTop).limsInf
Tactic: rw [← Function.comp_def, liminf, liminf, ← map_map, map_add_atTop_eq_nat]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, a ≤ u i
hu_le : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
⊢ a ≤ limsup u f
have refine : ∀ (b : α) (hb : ∀ᶠ (n : ι) in f, u n ≤ b), a ≤ b
Tactic: refine le_limsup_of_le hu_le fun b hb ↦ ?_
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, a ≤ u i
hu_le : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
b : α
hb : ∀ᶠ (n : ι) in f, u n ≤ b
⊢ a ≤ b
have obtain : ∀ (n : ι) (han : a ≤ u n) (hnb : u n ≤ b), a ≤ b
Tactic: obtain ⟨n, han, hnb⟩ := (hu.and_eventually hb).exists
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, u i ≤ a
hu_le : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
⊢ liminf u f ≤ a
have refine : ∀ (b : α) (hb : ∀ᶠ (n : ι) in f, b ≤ u n), b ≤ a
Tactic: refine liminf_le_of_le hu_le fun b hb ↦ ?_
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, u i ≤ a
hu_le : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
b : α
hb : ∀ᶠ (n : ι) in f, b ≤ u n
⊢ b ≤ a
have obtain : ∀ (n : ι) (hna : u n ≤ a) (hbn : b ≤ u n), b ≤ a
Tactic: obtain ⟨n, hna, hbn⟩ := (hu.and_eventually hb).exists
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Filter β
⊢ Eq.{u_1 + 1} (α := α) (limsup (fun (x : β) ↦ ⊥) f) ⊥
have rw : LE.le.{u_1} (α := α) (sInf {a : α | ∀ᶠ (n : β) in f, ⊥ ≤ a}) ⊥
Tactic: rw [limsup_eq, eq_bot_iff]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨅ (_ : True), sSup (u '' Ici i)) (⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i)
have simp : Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨆ a ∈ Ici i, u a) (⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i)
Tactic: simp only [sSup_image, iInf_const]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
u : β → α
⊢ limsup u ⊤ = ⨆ (i : β), u i
have rw : (map u ⊤).limsSup = ⨆ (i : β), u i
Tactic: rw [limsup, map_top, limsSup_principal_eq_sSup, sSup_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
u : β → α
rw : (map u ⊤).limsSup = ⨆ (i : β), u i
⊢ limsup u ⊤ = ⨆ (i : β), u i
have rw₁ : (𝓟 (range u)).limsSup = ⨆ (i : β), u i
Tactic: rw [limsup, map_top, limsSup_principal_eq_sSup, sSup_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
u : β → α
rw : (map u ⊤).limsSup = ⨆ (i : β), u i
rw₁ : (𝓟 (range u)).limsSup = ⨆ (i : β), u i
⊢ limsup u ⊤ = ⨆ (i : β), u i
have rw₂ : sSup (range u) = ⨆ (i : β), u i
Tactic: rw [limsup, map_top, limsSup_principal_eq_sSup, sSup_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
u : β → α
rw : (map u ⊤).limsSup = ⨆ (i : β), u i
rw₁ : (𝓟 (range u)).limsSup = ⨆ (i : β), u i
rw₂ : sSup (range u) = ⨆ (i : β), u i
⊢ limsup u ⊤ = ⨆ (i : β), u i
have rw₃ : iSup u = ⨆ (i : β), u i
Tactic: rw [limsup, map_top, limsSup_principal_eq_sSup, sSup_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
u : β → α
⊢ liminf u ⊤ = ⨅ (i : β), u i
have rw : (map u ⊤).limsInf = ⨅ (i : β), u i
Tactic: rw [liminf, map_top, limsInf_principal_eq_sInf, sInf_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
u : β → α
rw : (map u ⊤).limsInf = ⨅ (i : β), u i
⊢ liminf u ⊤ = ⨅ (i : β), u i
have rw₁ : (𝓟 (range u)).limsInf = ⨅ (i : β), u i
Tactic: rw [liminf, map_top, limsInf_principal_eq_sInf, sInf_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
u : β → α
rw : (map u ⊤).limsInf = ⨅ (i : β), u i
rw₁ : (𝓟 (range u)).limsInf = ⨅ (i : β), u i
⊢ liminf u ⊤ = ⨅ (i : β), u i
have rw₂ : sInf (range u) = ⨅ (i : β), u i
Tactic: rw [liminf, map_top, limsInf_principal_eq_sInf, sInf_range]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
u : β → α
rw : (map u ⊤).limsInf = ⨅ (i : β), u i
rw₁ : (𝓟 (range u)).limsInf = ⨅ (i : β), u i
rw₂ : sInf (range u) = ⨅ (i : β), u i
⊢ liminf u ⊤ = ⨅ (i : β), u i
have rw₃ : iInf u = ⨅ (i : β), u i
Tactic: rw [liminf, map_top, limsInf_principal_eq_sInf, sInf_range]
-- 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)
⊢ blimsup u f p = blimsup u f q
have simp : Eq.{u_1 + 1} (α := α) (sInf {a : α | ∀ᶠ (x : β) in f, p x → u x ≤ a}) (sInf {a : α | ∀ᶠ (x : β) in f, q x → u x ≤ a})
Tactic: simp only [blimsup_eq]