awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.LiminfLimsup
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
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 : ℕ
hj0 :
  BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑(Exists.choose (p := Surjective) ⋯ n) : ι')) : Type u_4)) ↦ f (↑i : ι))
⊢ ∃ (n : ℕ),
    Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) ⋯ n : Subtype p) ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
exact ⟨n, Or.inl hj0⟩
-- Module: Mathlib.Order.LiminfLimsup
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

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⟩
-- Module: Mathlib.Order.LiminfLimsup
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
hZ :
  Membership.mem (α := Subtype p) m
    (Exists.choose (p := Surjective) ⋯
        (Nat.find (p := fun (n : ℕ) ↦
          Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) ⋯ 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 : ι))}
    (⋯.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 : ι))})
        ⋯))

Tactic:
hZ

Premises used: Set.Mem, setOf
-- Module: Mathlib.Order.LiminfLimsup
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
hZ :
  Membership.mem (α := Subtype p) m
    (Exists.choose (p := Surjective) ⋯
        (Nat.find (p := fun (n : ℕ) ↦
          Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) ⋯ 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 : ι))}
    (⋯.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 : ι))})
        ⋯))

Tactic:
exact hZ
-- Module: Mathlib.Order.LiminfLimsup
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
hZ : ∀ (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 : ι))})
        ⋯))

Tactic:
(hZ j0 hj0).elim

Premises used: False.elim
-- Module: Mathlib.Order.LiminfLimsup
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
hZ : ∀ (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 : ι))})
        ⋯))

Tactic:
exact (hZ j0 hj0).elim

Premises used: False.elim
-- Module: Mathlib.Order.LiminfLimsup
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 : ι)))

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
-- Module: Mathlib.Order.LiminfLimsup
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 : ι))
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 : ι))
⊢ liminf f v = ⨆ (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]

Premises used: Filter.HasBasis.liminf_eq_sSup_iUnion_iInter, sSup_iUnion_Iic
-- Module: Mathlib.Order.LiminfLimsup
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 : ι)
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 : ι)
⊢ 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 = ∅

Premises used: Subtype
-- Module: Mathlib.Order.LiminfLimsup
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 : liminf f v = sSup univ
⊢ 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:
rw [if_pos H]

Premises used: if_pos
-- Module: Mathlib.Order.LiminfLimsup
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 : ∀ (j : Subtype p) (hj : s (↑j : ι') = ∅), liminf f v = sSup univ
⊢ liminf f v = sSup univ

Tactic:
rcases H with ⟨j, hj⟩
-- Module: Mathlib.Order.LiminfLimsup
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 : ι → α
j : Subtype p
hj : s (↑j : ι') = ∅
⊢ liminf f v = sSup univ

Tactic:
simp [hv.liminf_eq_sSup_univ_of_empty j j.2 hj]

Premises used: Filter.HasBasis.liminf_eq_sSup_univ_of_empty, Subtype.val, Subtype.property
-- Module: Mathlib.Order.LiminfLimsup
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 : ι') = ∅
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 : ι)
⊢ 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:
rw [if_neg H]

Premises used: if_neg
-- Module: Mathlib.Order.LiminfLimsup
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 : ι)
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 : ι)
⊢ 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))
-- Module: Mathlib.Order.LiminfLimsup
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' simp_rw : ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))
⊢ ∀ (j : Subtype p), Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι))) ∅

Tactic:
simp_rw [← not_nonempty_iff_eq_empty, nonempty_iInter_Iic_iff]

Premises used: Set.nonempty_iInter_Iic_iff, Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Order.LiminfLimsup
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 : ι))
⊢ ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))

Tactic:
H'
-- Module: Mathlib.Order.LiminfLimsup
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 : ι))
⊢ ∀ (j : Subtype p), ¬BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))

Tactic:
exact H'
-- Module: Mathlib.Order.LiminfLimsup
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 : ι))
⊢ ∀ (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'
-- Module: Mathlib.Order.LiminfLimsup
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 ∅)
pos₂ : Eq.{u_1 + 1} (α := α) (sSup (⋃ (j : Subtype p), ∅)) (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 : ι)

Tactic:
simp_rw [if_pos H', hv.liminf_eq_sSup_iUnion_iInter, A, iUnion_empty]

Premises used: if_pos, Filter.HasBasis.liminf_eq_sSup_iUnion_iInter, Set.iUnion_empty
-- Module: Mathlib.Order.LiminfLimsup
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 : liminf f v = ⨆ (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 : ι)

Tactic:
rw [if_neg H']

Premises used: if_neg
-- Module: Mathlib.Order.LiminfLimsup
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
neg₁ : ∃ (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 : ι)

Tactic:
apply hv.liminf_eq_ciSup_ciInf

Premises used: Filter.HasBasis.liminf_eq_ciSup_ciInf