awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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), BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))
rcases :
  ∀ (j0 : Subtype p) (hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))),
    liminf f v = ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
rcases₁ :
  ∀ (j0 : Subtype p) (hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))),
    liminf f v = ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
⊢ liminf f v = ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have rcases₂ : ∀ (j0 : Subtype p) (hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι)))
  (this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)),
  liminf f v = ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
Tactic: classical
  rcases H with ⟨j0, hj0⟩
  let m : Set (Subtype p) := {j | BddBelow (range (fun (i : s j) ↦ f i))}
  have : ∀ (j : Subtype p), Nonempty (s j) := fun j ↦ Nonempty.coe_sort (hs j)
  have A : ⋃ (j : Subtype p), ⋂ (i : s j), Iic (f i) =
         ⋃ (j : Subtype p), ⋂ (i : s (liminf_reparam f s p j)), Iic (f i) := by
    apply Subset.antisymm
    · apply iUnion_subset (fun j ↦ ?_)
      by_cases hj : j ∈ m
      · have : j = liminf_reparam f s p j := by simp only [m, liminf_reparam, hj, ite_true]
        conv_lhs => rw [this]
        apply subset_iUnion _ j
      · simp only [m, mem_setOf_eq, ← nonempty_iInter_Iic_iff, not_nonempty_iff_eq_empty] at hj
        simp only [hj, empty_subset]
    · apply iUnion_subset (fun j ↦ ?_)
      exact subset_iUnion (fun (k : Subtype p) ↦ (⋂ (i : s k), Iic (f i))) (liminf_reparam f s p j)
  have B : ∀ (j : Subtype p), ⋂ (i : s (liminf_reparam f s p j)), Iic (f i) =
                                Iic (⨅ (i : s (liminf_reparam f s p j)), f i) := by
    intro j
    apply (Iic_ciInf _).symm
    change liminf_reparam f s p j ∈ m
    by_cases Hj : j ∈ m
    · simpa only [m, liminf_reparam, if_pos Hj] using Hj
    · simp only [m, liminf_reparam, if_neg Hj]
      have Z : ∃ n, (exists_surjective_nat (Subtype p)).choose n ∈ m ∨ ∀ j, j ∉ m := by
        rcases (exists_surjective_nat (Subtype p)).choose_spec j0 with ⟨n, rfl⟩
        exact ⟨n, Or.inl hj0⟩
      rcases Nat.find_spec Z with hZ | hZ
      · exact hZ
      · exact (hZ j0 hj0).elim
  simp_rw [hv.liminf_eq_sSup_iUnion_iInter, A, B, sSup_iUnion_Iic]
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι → α
⊢ liminf f v =
    if ∃ (j : Subtype p), s (↑j : ι') = ∅ then sSup univ
    else
      if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
        sSup ∅
      else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have pos : ∀ (H : ∃ (j : Subtype p), s (↑j : ι') = ∅),
  liminf f v =
    if ∃ (j : Subtype p), s (↑j : ι') = ∅ then sSup univ
    else
      if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
        sSup ∅
      else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
Tactic: by_cases H : ∃ (j : Subtype p), s j = ∅
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι → α
pos :
  ∀ (H : ∃ (j : Subtype p), s (↑j : ι') = ∅),
    liminf f v =
      if ∃ (j : Subtype p), s (↑j : ι') = ∅ then sSup univ
      else
        if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
          sSup ∅
        else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
⊢ liminf f v =
    if ∃ (j : Subtype p), s (↑j : ι') = ∅ then sSup univ
    else
      if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
        sSup ∅
      else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have neg : ∀ (H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅),
  liminf f v =
    if ∃ (j : Subtype p), s (↑j : ι') = ∅ then sSup univ
    else
      if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
        sSup ∅
      else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
Tactic: by_cases H : ∃ (j : Subtype p), s j = ∅
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι') = ∅
⊢ liminf f v =
    if ∃ (j : Subtype p), s (↑j : ι') = ∅ then sSup univ
    else
      if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
        sSup ∅
      else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have pos : liminf f v = sSup univ
Tactic: rw [if_pos H]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι') = ∅
⊢ liminf f v = sSup univ
have pos : ∀ (j : Subtype p) (hj : s (↑j : ι') = ∅), liminf f v = sSup univ
Tactic: rcases H with ⟨j, hj⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι') = ∅
⊢ liminf f v =
    if ∃ (j : Subtype p), s (↑j : ι') = ∅ then sSup univ
    else
      if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
        sSup ∅
      else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have neg : liminf f v =
  if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then sSup ∅
  else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
Tactic: rw [if_neg H]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι') = ∅
⊢ liminf f v =
    if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
      sSup ∅
    else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have pos : ∀ (H' : ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))),
  liminf f v =
    if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
      sSup ∅
    else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
Tactic: by_cases H' : ∀ (j : Subtype p), ¬BddBelow (range (fun (i : s j) ↦ f i))
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι') = ∅
pos :
  ∀ (H' : ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))),
    liminf f v =
      if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
        sSup ∅
      else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
⊢ liminf f v =
    if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
      sSup ∅
    else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have neg : ∀ (H' : ¬∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))),
  liminf f v =
    if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
      sSup ∅
    else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
Tactic: by_cases H' : ∀ (j : Subtype p), ¬BddBelow (range (fun (i : s j) ↦ f i))
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
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 : ι))
⊢ liminf f v =
    if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
      sSup ∅
    else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have A : ∀ (j : Subtype p), Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι))) ∅
Tactic: have A : ∀ (j : Subtype p), ⋂ (i : s j), Iic (f i) = ∅ := by
      simp_rw [← not_nonempty_iff_eq_empty, nonempty_iInter_Iic_iff]
      exact H'
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι))
A : ∀ (j : Subtype p), Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι))) ∅
⊢ liminf f v =
    if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
      sSup ∅
    else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have pos : liminf f v = sSup ∅
Tactic: simp_rw [if_pos H', hv.liminf_eq_sSup_iUnion_iInter, A, iUnion_empty]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι))
A : ∀ (j : Subtype p), Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι))) ∅
pos : liminf f v = sSup ∅
⊢ liminf f v =
    if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
      sSup ∅
    else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have pos₁ : Eq.{u_1 + 1} (α := α) (sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))) (sSup ∅)
Tactic: simp_rw [if_pos H', hv.liminf_eq_sSup_iUnion_iInter, A, iUnion_empty]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι))
A : ∀ (j : Subtype p), Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι))) ∅
pos : liminf f v = sSup ∅
pos₁ : Eq.{u_1 + 1} (α := α) (sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))) (sSup ∅)
⊢ liminf f v =
    if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
      sSup ∅
    else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have pos₂ : Eq.{u_1 + 1} (α := α) (sSup (⋃ (j : Subtype p), ∅)) (sSup ∅)
Tactic: simp_rw [if_pos H', hv.liminf_eq_sSup_iUnion_iInter, A, iUnion_empty]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι))
⊢ liminf f v =
    if ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι)) then
      sSup ∅
    else ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have neg : liminf f v = ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
Tactic: rw [if_neg H']
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι))
⊢ liminf f v = ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have neg : ∀ (j : Subtype p), (s (↑j : ι')).Nonempty
Tactic: apply hv.liminf_eq_ciSup_ciInf
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : ι))
neg : ∀ (j : Subtype p), (s (↑j : ι')).Nonempty
⊢ liminf f v = ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have neg₁ : ∃ (j : Subtype p), BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))
Tactic: apply hv.liminf_eq_ciSup_ciInf
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
have refine : ∀ (c : γ) (hc : ∀ᶠ (n : γ) in map (fun (x : α) ↦ l (v x)) f, n ≤ c), l (limsup v f) ≤ c
Tactic: refine le_limsSup_of_le hlv fun c hc => ?_
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
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
⊢ l (limsup v f) ≤ c
have hc₁ : ∀ᶠ (a : α) in f, l (v a) ≤ c
Tactic: rw [Filter.eventually_map] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
⊢ l (limsup v f) ≤ c
have simp_rw : ∀ (hc : ∀ᶠ (a : α) in f, v a ≤ u c), limsup v f ≤ u c
Tactic: simp_rw [gc _ _] at hc ⊢
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : γ)
have refine : LE.le.{u_6} (α := γ) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f : γ) ((g : (a : β) → γ) (limsup u f) : γ)
Tactic: refine le_antisymm ((OrderIso.to_galoisConnection g).l_limsup_le hgu hu_co) ?_
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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} (α := γ) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f : γ) ((g : (a : β) → γ) (limsup u f) : γ)
have rw : LE.le.{u_6} (α := γ)
  ((g : (a : β) → γ) ((g.symm : (a : γ) → β) (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]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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) : γ)
have refine : (g.symm : (a : γ) → β) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f) ≤ limsup u f
Tactic: refine g.monotone ?_
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
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)
⊢ (g.symm : (a : γ) → β) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f) ≤ limsup u f
have hf : 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
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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) : γ)
⊢ (g.symm : (a : γ) → β) (limsup (fun (x : α) ↦ (g : (a : β) → γ) (u x)) f) ≤ limsup u f
have 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 : β)
Tactic: nth_rw 2 [hf]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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 : β)
have refine : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (x : α) ↦ (g.symm : (a : γ) → β) ((g : (a : β) → γ) (u x) : γ)
Tactic: refine (OrderIso.to_galoisConnection g.symm).l_limsup_le ?_ hgu_co
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
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
⊢ limsup (fun (a : α) ↦ max (u a) (v a)) f = max (limsup u f) (limsup v f)
have bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
Tactic: have bddmax := IsBoundedUnder.sup h₃ h₄