-- 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
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 : ι)
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 : ι)
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))
    (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 : ι)
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))
    (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 : ι)
⊢ 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]

Premises used: Filter.HasBasis.liminf_eq_sSup_iUnion_iInter, sSup_iUnion_Iic