awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
⊢ limsup (fun (a : α) ↦ max (u a) (v a)) f = max (limsup u f) (limsup v f)
have cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
Tactic: have cobddmax := isCoboundedUnder_le_max (v := v) (Or.inl h₁)
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
⊢ limsup (fun (a : α) ↦ max (u a) (v a)) f = max (limsup u f) (limsup v f)
have a : limsup (fun (a : α) ↦ max (u a) (v a)) f ≤ max (limsup u f) (limsup v f)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
a : limsup (fun (a : α) ↦ max (u a) (v a)) f ≤ max (limsup u f) (limsup v f)
⊢ limsup (fun (a : α) ↦ max (u a) (v a)) f = max (limsup u f) (limsup v f)
have a₁ : max (limsup u f) (limsup v f) ≤ limsup (fun (a : α) ↦ max (u a) (v a)) f
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
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
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
⊢ limsup (fun (a : α) ↦ max (u a) (v a)) f ≤ max (limsup u f) (limsup v f)
have a : ∀ (b : β) (hb : b > max (limsup u f) (limsup v f)), ∀ᶠ (a : α) in f, max (u a) (v a) < b
Tactic: refine (limsup_le_iff cobddmax bddmax).2 (fun b hb ↦ ?_)
-- 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
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
b : β
hb : b > max (limsup u f) (limsup v f)
⊢ ∀ᶠ (a : α) in f, max (u a) (v a) < b
have hu : ∀ᶠ (a : α) in f, u a < b
Tactic: have hu := eventually_lt_of_limsup_lt (lt_of_le_of_lt (le_max_left _ _) hb) h₃
-- 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
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
b : β
hb : b > max (limsup u f) (limsup v f)
hu : ∀ᶠ (a : α) in f, u a < b
⊢ ∀ᶠ (a : α) in f, max (u a) (v a) < b
have hv : ∀ᶠ (a : α) in f, v a < b
Tactic: have hv := eventually_lt_of_limsup_lt (lt_of_le_of_lt (le_max_right _ _) hb) h₄
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
⊢ Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f)
    (s.sup' hs fun (i : ι) ↦ limsup (F i) f)
have bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
Tactic: have bddsup := isBoundedUnder_le_finset_sup' hs h₂
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
⊢ Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f)
    (s.sup' hs fun (i : ι) ↦ limsup (F i) f)
have a : LE.le.{u_2} (α := β) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f) (s.sup' hs fun (i : ι) ↦ limsup (F i) f)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
a :
  LE.le.{u_2} (α := β) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f) (s.sup' hs fun (i : ι) ↦ limsup (F i) f)
⊢ Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f)
    (s.sup' hs fun (i : ι) ↦ limsup (F i) f)
have a₁ : LE.le.{u_2} (α := β) (s.sup' hs fun (i : ι) ↦ limsup (F i) f) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
⊢ ∃ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
have rcases : ∀ (i : ι) (i_s : i ∈ s)
  (bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' sorry fun (i : ι) ↦ F i a),
  ∃ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
Tactic: rcases hs with ⟨i, i_s⟩
Cleared hypotheses: hs, bddsup
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
i : ι
i_s : i ∈ s
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' ⋯ fun (i : ι) ↦ F i a
⊢ ∃ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
have right : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
Tactic: use i, i_s
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
⊢ LE.le.{u_2} (α := β) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f) (s.sup' hs fun (i : ι) ↦ limsup (F i) f)
have h₃ : ∃ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
Tactic: have h₃ : ∃ i ∈ s, f.IsCoboundedUnder (· ≤ ·) (F i) := by
      rcases hs with ⟨i, i_s⟩
      use i, i_s
      exact h₁ i i_s
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
⊢ LE.le.{u_2} (α := β) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f) (s.sup' hs fun (i : ι) ↦ limsup (F i) f)
have cobddsup : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
Tactic: have cobddsup := isCoboundedUnder_le_finset_sup' hs h₃
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
cobddsup : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
⊢ LE.le.{u_2} (α := β) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f) (s.sup' hs fun (i : ι) ↦ limsup (F i) f)
have a : ∀ (b : β) (hb : b > s.sup' hs fun (i : ι) ↦ limsup (F i) f), ∀ᶠ (a : α) in f, (s.sup' hs fun (i : ι) ↦ F i a) < b
Tactic: refine (limsup_le_iff cobddsup bddsup).2 (fun b hb ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
cobddsup : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
b : β
hb : b > s.sup' hs fun (i : ι) ↦ limsup (F i) f
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun (i : ι) ↦ F i a) < b
have a : ∀ (hb : ∀ i ∈ s, limsup (F i) f < b), ∀ i ∈ s, ∀ᶠ (x : α) in f, F i x < b
Tactic: simp only [gt_iff_lt, sup'_lt_iff, eventually_all_finset] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
⊢ LE.le.{u_2} (α := β) (s.sup' hs fun (i : ι) ↦ limsup (F i) f) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f)
have a : ∀ b ∈ s, limsup (F b) f ≤ limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f
Tactic: apply Finset.sup'_le hs (fun i ↦ limsup (F i) f)
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
⊢ ∀ b ∈ s, limsup (F b) f ≤ limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f
have a : ∀ (i : ι) (i_s : i ∈ s) (a : α), F i a ≤ (fun (a : α) ↦ (s.sup' hs fun (i : ι) ↦ F i a : β)) a
Tactic: refine fun i i_s ↦ limsup_le_limsup (Eventually.of_forall (fun a ↦ ?_)) (h₁ i i_s) bddsup
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
i : ι
i_s : i ∈ s
a : α
⊢ F i a ≤ (fun (a : α) ↦ (s.sup' hs fun (i : ι) ↦ F i a : β)) a
have a₁ : ∃ b ∈ s, F i a ≤ F b a
Tactic: simp only [le_sup'_iff]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
i : ι
i_s : i ∈ s
a : α
w : ι
left : i ∈ s
⊢ ∃ b ∈ s, F i a ≤ F b a
have right : F i a ≤ F i a
Tactic: use i, i_s
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
⊢ Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f) (s.sup fun (i : ι) ↦ limsup (F i) f)
have inl : ∀ (h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ (F i))
  (h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ (F i)),
  Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) ⊥) (s.sup fun (i : ι) ↦ limsup (F i) ⊥)
Tactic: rcases eq_or_neBot f with (rfl | _)
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
inl :
  ∀ (h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ (F i))
    (h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ (F i)),
    Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) ⊥) (s.sup fun (i : ι) ↦ limsup (F i) ⊥)
⊢ Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f) (s.sup fun (i : ι) ↦ limsup (F i) f)
have inr : f.NeBot →
  Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f) (s.sup fun (i : ι) ↦ limsup (F i) f)
Tactic: rcases eq_or_neBot f with (rfl | _)
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h : f.NeBot
⊢ Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f) (s.sup fun (i : ι) ↦ limsup (F i) f)
have inr : ∀ (h₁ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i))
  (h₂ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)),
  Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ sup ∅ fun (i : ι) ↦ F i a) f) (sup ∅ fun (i : ι) ↦ limsup (F i) f)
Tactic: rcases Finset.eq_empty_or_nonempty s with (rfl | s_nemp)
Cleared hypotheses: s, h₁, h₂
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h : f.NeBot
inr :
  ∀ (h₁ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i))
    (h₂ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)),
    Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ sup ∅ fun (i : ι) ↦ F i a) f) (sup ∅ fun (i : ι) ↦ limsup (F i) f)
⊢ Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f) (s.sup fun (i : ι) ↦ limsup (F i) f)
have inr₁ : ∀ (s_nemp : s.Nonempty),
  Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f) (s.sup fun (i : ι) ↦ limsup (F i) f)
Tactic: rcases Finset.eq_empty_or_nonempty s with (rfl | s_nemp)
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h : f.NeBot
s_nemp : s.Nonempty
⊢ Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f) (s.sup fun (i : ι) ↦ limsup (F i) f)
have inr : Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f)
  (limsup (fun (a : α) ↦ s.sup' s_nemp fun (i : ι) ↦ F i a) f)
Tactic: rw [← Finset.sup'_eq_sup s_nemp fun i ↦ limsup (F i) f, ← limsup_finset_sup' s_nemp h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h : f.NeBot
s_nemp : s.Nonempty
⊢ Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f)
    (limsup (fun (a : α) ↦ s.sup' s_nemp fun (i : ι) ↦ F i a) f)
have inr : Eq (α := α → β) (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) fun (a : α) ↦ s.sup' s_nemp fun (i : ι) ↦ F i a
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h : f.NeBot
s_nemp : s.Nonempty
⊢ Eq (α := α → β) (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) fun (a : α) ↦ s.sup' s_nemp fun (i : ι) ↦ F i a
have inr : ∀ (a : α), Eq.{u_2 + 1} (α := β) (s.sup fun (i : ι) ↦ F i a) (s.sup' s_nemp fun (i : ι) ↦ F i a)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.Max (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMinOrder α
x : α × β
a : α
b : β
⊢ ∃ (b_1 : α × β), b_1 < (a, b)
have obtain : ∀ (c : α) (h : c < a), ∃ (b_1 : α × β), b_1 < (a, b)
Tactic: obtain ⟨c, h⟩ := exists_lt a
-- Lean 4 proof step from Mathlib.Order.Max (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMinOrder β
x : α × β
a : α
b : β
⊢ ∃ (b_1 : α × β), b_1 < (a, b)
have obtain : ∀ (c : β) (h : c < b), ∃ (b_1 : α × β), b_1 < (a, b)
Tactic: obtain ⟨c, h⟩ := exists_lt b
-- Lean 4 proof step from Mathlib.Order.Max (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst : Nonempty ι
inst_1 : (i : ι) → Preorder (π i)
inst_2 : ∀ (i : ι), NoMinOrder.{u_3} (π i)
a : (i : ι) → π i
⊢ ∃ (b : (i : ι) → π i), b < a
have obtain : ∀ (b : π (Classical.arbitrary ι)) (hb : b < a (Classical.arbitrary ι)), ∃ (b : (i : ι) → π i), b < a
Tactic: obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)
-- Lean 4 proof step from Mathlib.Order.Max (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst : Nonempty ι
inst_1 : (i : ι) → Preorder (π i)
inst_2 : ∀ (i : ι), NoMinOrder.{u_3} (π i)
a : (i : ι) → π i
⊢ ∃ (b : (i : ι) → π i), b < a
have obtain : ∀ (b : π (Classical.arbitrary ι)) (hb : b < a (Classical.arbitrary ι)), ∃ (b : (i : ι) → π i), b < a
Tactic: classical
    obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)
    exact ⟨_, update_lt_self_iff.2 hb⟩
-- Lean 4 proof step from Mathlib.Order.Max (goal)
Goal:
α : Type u_1
inst : LE α
⊢ NoBotOrder α ↔ ∀ (x : α), ¬IsBot x
have simp_rw : (∀ (a : α), ∃ (b : α), ¬a ≤ b) ↔ ∀ (x : α), ¬IsBot x
Tactic: simp_rw [noBotOrder_iff', IsBot, not_forall]
-- Lean 4 proof step from Mathlib.Order.Max (goal)
Goal:
α : Type u_1
inst : LE α
simp_rw : (∀ (a : α), ∃ (b : α), ¬a ≤ b) ↔ ∀ (x : α), ¬IsBot x
⊢ NoBotOrder α ↔ ∀ (x : α), ¬IsBot x
have simp_rw₁ : (∀ (a : α), ∃ (b : α), ¬a ≤ b) ↔ ∀ (x : α), ¬∀ (b : α), x ≤ b
Tactic: simp_rw [noBotOrder_iff', IsBot, not_forall]
-- Lean 4 proof step from Mathlib.Order.Max (goal)
Goal:
α : Type u_3
inst : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j = i
have simp_rw : IsMin j ↔ j ≤ i
Tactic: simp_rw [le_antisymm_iff, h j, and_true]
-- Lean 4 proof step from Mathlib.Order.Max (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : Nontrivial α
ha : IsBot a
ha' : IsMax a
⊢ False
have obtain : ∀ (b : α) (hb : b ≠ a), False
Tactic: obtain ⟨b, hb⟩ := exists_ne a
-- Lean 4 proof step from Mathlib.Order.MinMax (goal)
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ min (min a b) c = min (min a c) b
have rw : min a (min b c) = min (min a c) b
Tactic: rw [min_assoc, min_comm b, ← min_assoc]
-- Lean 4 proof step from Mathlib.Order.MinMax (goal)
Goal:
α : Type u
inst : LinearOrder α
a b c : α
rw : min a (min b c) = min (min a c) b
⊢ min (min a b) c = min (min a c) b
have rw₁ : min a (min c b) = min (min a c) b
Tactic: rw [min_assoc, min_comm b, ← min_assoc]
-- Lean 4 proof step from Mathlib.Order.MinMax (goal)
Goal:
α : Type u
inst : LinearOrder α
a b c : α
rw : min a (min b c) = min (min a c) b
rw₁ : min a (min c b) = min (min a c) b
⊢ min (min a b) c = min (min a c) b
have rw₂ : min (min a c) b = min (min a c) b
Tactic: rw [min_assoc, min_comm b, ← min_assoc]
-- Lean 4 proof step from Mathlib.Order.MinMax (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
⊢ f (max a b) = max (f a) (f b)
have inl : ∀ (h : a ≤ b), f (max a b) = max (f a) (f b)
Tactic: rcases le_total a b with h | h
-- Lean 4 proof step from Mathlib.Order.MinMax (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
inl : ∀ (h : a ≤ b), f (max a b) = max (f a) (f b)
⊢ f (max a b) = max (f a) (f b)
have inr : ∀ (h : b ≤ a), f (max a b) = max (f a) (f b)
Tactic: rcases le_total a b with h | h
-- Lean 4 proof step from Mathlib.Order.MinMax (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b : α
hf : Monotone f
⊢ f (max a b) = max (f a) (f b)
have inl : ∀ (h : a ≤ b), f (max a b) = max (f a) (f b)
Tactic: rcases le_total a b with h | h
-- Lean 4 proof step from Mathlib.Order.MinMax (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b : α
hf : Monotone f
inl : ∀ (h : a ≤ b), f (max a b) = max (f a) (f b)
⊢ f (max a b) = max (f a) (f b)
have inr : ∀ (h : b ≤ a), f (max a b) = max (f a) (f b)
Tactic: rcases le_total a b with h | h