awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
⊢ (∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a) → x ≤ limsup u f
have rw : (∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a) → ∀ ⦃c : β⦄, c < x → c < limsup u f
Tactic: rw [← forall_lt_iff_le]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a
y : β
y_x : y < x
⊢ y < limsup u f
have obtain : ∀ (z : β) (y_z : y < z) (z_x : z < x), y < limsup u f
Tactic: obtain ⟨z, y_z, z_x⟩ := exists_between y_x
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
⊢ liminf u f ≤ limsup v f
have inl : ∀ (h : ∃ᶠ (x : α) in ⊥, u x ≤ v x) (h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) ⊥ u)
  (h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ v), liminf u ⊥ ≤ limsup v ⊥
Tactic: rcases f.eq_or_neBot with rfl | _
Cleared hypotheses: f, h, h₁, h₂
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
inl :
  ∀ (h : ∃ᶠ (x : α) in ⊥, u x ≤ v x) (h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) ⊥ u)
    (h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ v), liminf u ⊥ ≤ limsup v ⊥
⊢ liminf u f ≤ limsup v f
have inr : f.NeBot → liminf u f ≤ limsup v f
Tactic: rcases f.eq_or_neBot with rfl | _
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
have obtain : ∀ (a : β) (ha : ∀ᶠ (x : α) in f, v x ≤ a), IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
Tactic: obtain ⟨a, ha⟩ := h₂.eventually_le
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
a : β
ha : ∀ᶠ (x : α) in f, v x ≤ a
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
have apply : ∃ᶠ (x : α) in f, u x ≤ a
Tactic: apply IsCoboundedUnder.of_frequently_le (a := a)
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
⊢ liminf u f ≤ limsup v f
have h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
Tactic: have h₃ : f.IsCoboundedUnder (· ≥ ·) u := by
    obtain ⟨a, ha⟩ := h₂.eventually_le
    apply IsCoboundedUnder.of_frequently_le (a := a)
    exact (h.and_eventually ha).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
have obtain : ∀ (a : β) (ha : ∀ᶠ (x : α) in f, a ≤ u x), IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
Tactic: obtain ⟨a, ha⟩ := h₁.eventually_ge
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
a : β
ha : ∀ᶠ (x : α) in f, a ≤ u x
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
have apply : ∃ᶠ (x : α) in f, a ≤ v x
Tactic: apply IsCoboundedUnder.of_frequently_ge (a := a)
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
⊢ liminf u f ≤ limsup v f
have h₄ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
Tactic: have h₄ : f.IsCoboundedUnder (· ≤ ·) v := by
    obtain ⟨a, ha⟩ := h₁.eventually_ge
    apply IsCoboundedUnder.of_frequently_ge (a := a)
    exact (ha.and_frequently h).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₄ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
⊢ liminf u f ≤ limsup v f
have inr : ∀ (y : β) (y_v : y < liminf u f), ∃ᶠ (a : α) in f, y < v a
Tactic: refine (le_limsup_iff h₄ h₂).2 fun y y_v ↦ ?_
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₄ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
y : β
y_v : y < liminf u f
⊢ ∃ᶠ (a : α) in f, y < v a
have this : ∀ᶠ (a : α) in f, y < u a
Tactic: have := (le_liminf_iff h₃ h₁).1 (le_refl (liminf u f)) y y_v
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder β
f_1 : Filter α
u : α → β
inst_1 : ConditionallyCompleteLinearOrder α
f_2 : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst_2 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_3 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
j : Subtype p
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
g : ℕ → Subtype p := Exists.choose (p := Surjective) ⋯
⊢ ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
have pos : ∀ (H : ∃ (j : Subtype p), j ∈ m), ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
Tactic: by_cases! H : ∃ j, j ∈ m
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder β
f_1 : Filter α
u : α → β
inst_1 : ConditionallyCompleteLinearOrder α
f_2 : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst_2 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_3 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
j : Subtype p
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
g : ℕ → Subtype p := Exists.choose (p := Surjective) ⋯
pos : ∀ (H : ∃ (j : Subtype p), j ∈ m), ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
⊢ ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
have neg : ∀ (H : ∀ (j : Subtype p), j ∉ m), ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
Tactic: by_cases! H : ∃ j, j ∈ m
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder β
f_1 : Filter α
u : α → β
inst_1 : ConditionallyCompleteLinearOrder α
f_2 : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst_2 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_3 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
j : Subtype p
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
g : ℕ → Subtype p := Exists.choose (p := Surjective) ⋯
H : ∃ (j : Subtype p), j ∈ m
⊢ ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
have pos : ∀ (j : Subtype p) (hj : j ∈ m), ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
Tactic: rcases H with ⟨j, hj⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder β
f_1 : Filter α
u : α → β
inst_1 : ConditionallyCompleteLinearOrder α
f_2 : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst_2 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_3 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
j_1 : Subtype p
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
g : ℕ → Subtype p := Exists.choose (p := Surjective) ⋯
j : Subtype p
hj : j ∈ m
⊢ ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
have pos : ∀ (n : ℕ) (hj : Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) sorry n : Subtype p)),
  ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
Tactic: rcases (exists_surjective_nat (Subtype p)).choose_spec j with ⟨n, rfl⟩
Cleared hypotheses: j, 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
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: rcases H with ⟨j0, hj0⟩
Cleared hypotheses: H
-- 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 : ι))}
⊢ liminf f v = ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
have this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
Tactic: have : ∀ (j : Subtype p), Nonempty (s j) := fun j ↦ Nonempty.coe_sort (hs 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)
⊢ 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 : ι)))
have h₁ : Subset.{u_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: apply Subset.antisymm
-- 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)
h₁ :
  Subset.{u_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 : ι)))
⊢ 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 : ι)))
have h₂ : Subset.{u_1} (α := Set α)
  (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
  (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
Tactic: apply Subset.antisymm
-- 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)
⊢ Subset.{u_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 : ι)))
have apply : ∀ (j : Subtype p),
  Subset.{u_1} (α := Set α) (⋂ (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: apply iUnion_subset (fun 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)
j : Subtype p
⊢ Subset.{u_1} (α := Set α) (⋂ (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 : ι)))
have pos : ∀ (hj : j ∈ m),
  Subset.{u_1} (α := Set α) (⋂ (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: 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)
j : Subtype p
pos :
  ∀ (hj : j ∈ m),
    Subset.{u_1} (α := Set α) (⋂ (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 : ι)))
⊢ Subset.{u_1} (α := Set α) (⋂ (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 : ι)))
have neg : ∀ (hj : j ∉ m),
  Subset.{u_1} (α := Set α) (⋂ (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: by_cases hj : j ∈ m
-- 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)
j : Subtype p
hj : j ∈ m
⊢ Subset.{u_1} (α := Set α) (⋂ (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 : ι)))
have this₁ : j = liminf_reparam f s p j
Tactic: have : j = liminf_reparam f s p j := by simp only [m, liminf_reparam, hj, ite_true]
-- 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_1 : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
j : Subtype p
hj : j ∈ m
this : j = liminf_reparam f s p j
| ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι))
have rw : ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι))
Tactic: rw [this]
-- 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_1 : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
j : Subtype p
hj : j ∈ m
this : j = liminf_reparam f s p j
⊢ Subset.{u_1} (α := Set α) (⋂ (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 : ι)))
have pos : Subset.{u_1} (α := Set α) (⋂ (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)), Iic (f (↑i : ι)))
Tactic: conv_lhs => rw [this]
-- 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)
j : Subtype p
hj : j ∉ m
⊢ Subset.{u_1} (α := Set α) (⋂ (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 : ι)))
have hj₁ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι))) ∅
Tactic: simp only [m, mem_setOf_eq, ← nonempty_iInter_Iic_iff, not_nonempty_iff_eq_empty] at hj
Cleared hypotheses: 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)
⊢ Subset.{u_1} (α := Set α)
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
have apply : ∀ (j : Subtype p),
  Subset.{u_1} (α := Set α) (⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
Tactic: apply iUnion_subset (fun j ↦ ?_)