-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_eq_sInf_sSup {ι R : Type*} (F : Filter ι) [CompleteLattice R] (a : ι → R) :
    limsup a F = sInf ((fun I => sSup (a '' I)) '' F.sets)

Proof state:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1} ≤ sInf ((fun I => sSup (a '' I)) '' F.sets)

Tactic:
refine sInf_le_sInf fun x hx => ?_

Result:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I => sSup (a '' I)) '' F.sets
⊢ x ∈ {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1}

Proof state:
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F = sInf ((fun I => sSup (a '' I)) '' F.sets)

Tactic:
apply le_antisymm

Result:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F ≤ sInf ((fun I => sSup (a '' I)) '' F.sets)

case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I => sSup (a '' I)) '' F.sets) ≤ limsup a F

Proof state:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I => sSup (a '' I)) '' F.sets) ≤ limsup a F

Tactic:
refine le_sInf fun b hb => sInf_le_of_le (mem_image_of_mem _ hb) <| sSup_le ?_

Result:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
b : R
hb : b ∈ {a_1 | ∀ᶠ (n : R) in map a F, n ≤ a_1}
⊢ ∀ b_1 ∈ a '' (a ⁻¹' {x | (fun n => n ≤ b) x}), b_1 ≤ b

Proof state:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I => sSup (a '' I)) '' F.sets
⊢ x ∈ {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1}

Tactic:
rcases (mem_image _ F.sets x).mp hx with ⟨I, ⟨I_mem_F, hI⟩⟩

Result:
case a.intro.intro
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I => sSup (a '' I)) '' F.sets
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
⊢ x ∈ {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1}

Proof state:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
b : R
hb : b ∈ {a_1 | ∀ᶠ (n : R) in map a F, n ≤ a_1}
⊢ ∀ b_1 ∈ a '' (a ⁻¹' {x | (fun n => n ≤ b) x}), b_1 ≤ b

Tactic:
rintro _ ⟨_, h, rfl⟩

Result:
case a.intro.intro
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
b : R
hb : b ∈ {a_1 | ∀ᶠ (n : R) in map a F, n ≤ a_1}
w✝ : ι
h : w✝ ∈ a ⁻¹' {x | (fun n => n ≤ b) x}
⊢ a w✝ ≤ b

Proof state:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F ≤ sInf ((fun I => sSup (a '' I)) '' F.sets)

Tactic:
rw [limsup_eq]

Result:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1} ≤ sInf ((fun I => sSup (a '' I)) '' F.sets)

Proof state:
case a.intro.intro
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
b : R
hb : b ∈ {a_1 | ∀ᶠ (n : R) in map a F, n ≤ a_1}
w✝ : ι
h : w✝ ∈ a ⁻¹' {x | (fun n => n ≤ b) x}
⊢ a w✝ ≤ b

Tactic:
exact h

Result:
no goals

Proof state:
case h
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I => sSup (a '' I)) '' F.sets
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
i : ι
hi : i ∈ I
⊢ a i ≤ x

Tactic:
exact hI ▸ le_sSup (mem_image_of_mem _ hi)

Result:
no goals

Proof state:
case a.intro.intro
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I => sSup (a '' I)) '' F.sets
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
⊢ x ∈ {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1}

Tactic:
filter_upwards [I_mem_F] with i hi

Result:
case h
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I => sSup (a '' I)) '' F.sets
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
i : ι
hi : i ∈ I
⊢ a i ≤ x