awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι → α
hs : ∀ (j : Subtype p), (s (↑j : ι')).Nonempty
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : 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 : ι)
have A : Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
  (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
Tactic: 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)
-- 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
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
j : Subtype p
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (Iic (⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)))
have apply : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)) ↦ f (↑i : ι))
Tactic: apply (Iic_ciInf _).symm
-- 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
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
j : Subtype p
⊢ BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)) ↦ f (↑i : ι))
have change : liminf_reparam f s p j ∈ m
Tactic: change liminf_reparam f s p j ∈ m
-- 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
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
j : Subtype p
⊢ liminf_reparam f s p j ∈ m
have pos : ∀ (Hj : j ∈ m), liminf_reparam f s p j ∈ m
Tactic: by_cases Hj : j ∈ m
-- 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
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
j : Subtype p
pos : ∀ (Hj : j ∈ m), liminf_reparam f s p j ∈ m
⊢ liminf_reparam f s p j ∈ m
have neg : ∀ (Hj : j ∉ m), liminf_reparam f s p j ∈ m
Tactic: by_cases Hj : j ∈ m
-- 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
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
j : Subtype p
Hj : j ∉ m
⊢ liminf_reparam f s p j ∈ m
have neg : Membership.mem (γ := Set (Subtype p))
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
  (sorry.choose (p := Surjective)
    (Nat.find (p := fun (n : ℕ) ↦
      Membership.mem (γ := Set (Subtype p))
          {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
          (sorry.choose (p := Surjective) n) ∨
        ∀ (j : Subtype p),
          j ∉ {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))})
      sorry))
Tactic: simp only [m, liminf_reparam, if_neg Hj]
-- 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
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
j : Subtype p
Hj : j ∉ m
⊢ ∃ (n : ℕ),
    Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) ⋯ n : Subtype p) ∨ ∀ (j : Subtype p), j ∉ m
have rcases : ∀ (n : ℕ)
  (hj0 :
    BddBelow.{u_1} (α := α)
      (range fun (i : (↑(s (↑(Exists.choose (p := Surjective) sorry n) : ι')) : Type u_4)) ↦ f (↑i : ι))),
  ∃ (n : ℕ),
    Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) sorry n : Subtype p) ∨ ∀ (j : Subtype p), j ∉ m
Tactic: rcases (exists_surjective_nat (Subtype p)).choose_spec j0 with ⟨n, rfl⟩
Cleared hypotheses: j0, hj0
-- 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 : ι → α
hs : ∀ (j : Subtype p), (s (↑j : ι')).Nonempty
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
j : Subtype p
Hj : j ∉ m
⊢ Membership.mem (γ := Set (Subtype p))
    {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
    (⋯.choose (p := Surjective)
      (Nat.find (p := fun (n : ℕ) ↦
        Membership.mem (γ := Set (Subtype p))
            {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
            (⋯.choose (p := Surjective) n) ∨
          ∀ (j : Subtype p),
            j ∉ {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))})
        ⋯))
have Z : ∃ (n : ℕ),
  Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) sorry n : Subtype p) ∨ ∀ (j : Subtype p), j ∉ m
Tactic: 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⟩
-- 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
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
j : Subtype p
Hj : j ∉ m
Z :
  ∃ (n : ℕ),
    Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) ⋯ n : Subtype p) ∨ ∀ (j : Subtype p), j ∉ m
⊢ Membership.mem (γ := Set (Subtype p))
    {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
    (⋯.choose (p := Surjective)
      (Nat.find (p := fun (n : ℕ) ↦
        Membership.mem (γ := Set (Subtype p))
            {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
            (⋯.choose (p := Surjective) n) ∨
          ∀ (j : Subtype p),
            j ∉ {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))})
        ⋯))
have neg : ∀
  (hZ :
    Membership.mem (α := Subtype p) m
      (Exists.choose (p := Surjective) sorry
          (Nat.find (p := fun (n : ℕ) ↦
            Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) sorry n : Subtype p) ∨
              ∀ (j : Subtype p), j ∉ m)
            Z) :
        Subtype p)),
  Membership.mem (γ := Set (Subtype p))
    {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
    (sorry.choose (p := Surjective)
      (Nat.find (p := fun (n : ℕ) ↦
        Membership.mem (γ := Set (Subtype p))
            {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
            (sorry.choose (p := Surjective) n) ∨
          ∀ (j : Subtype p),
            j ∉ {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))})
        sorry))
Tactic: rcases Nat.find_spec Z with hZ | hZ
-- 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 : ι → α
hs : ∀ (j : Subtype p), (s (↑j : ι')).Nonempty
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
⊢ liminf f v = ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have B : ∀ (j : Subtype p),
  Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (Iic (⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)))
Tactic: 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
-- 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
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
B :
  ∀ (j : Subtype p),
    Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
      (Iic (⨅ (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 simp_rw : Eq.{u_1 + 1} (α := α) (sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι))))
  (⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι))
Tactic: simp_rw [hv.liminf_eq_sSup_iUnion_iInter, A, B, sSup_iUnion_Iic]
-- 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
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
B :
  ∀ (j : Subtype p),
    Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
      (Iic (⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)))
simp_rw :
  Eq.{u_1 + 1} (α := α) (sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι))))
    (⨆ (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 simp_rw₁ : Eq.{u_1 + 1} (α := α)
  (sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι))))
  (⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι))
Tactic: simp_rw [hv.liminf_eq_sSup_iUnion_iInter, A, B, sSup_iUnion_Iic]
-- 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
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
B :
  ∀ (j : Subtype p),
    Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
      (Iic (⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)))
simp_rw :
  Eq.{u_1 + 1} (α := α) (sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι))))
    (⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι))
simp_rw₁ :
  Eq.{u_1 + 1} (α := α)
    (sSup (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι))))
    (⨆ (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 simp_rw₂ : Eq.{u_1 + 1} (α := α)
  (sSup (⋃ (j : Subtype p), Iic (⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι))))
  (⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι))
Tactic: simp_rw [hv.liminf_eq_sSup_iUnion_iInter, A, B, sSup_iUnion_Iic]
-- 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 : ι))
⊢ 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 : ι))),
  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