-- Mathlib/Analysis/Normed/Order/UpperLower.lean
protected lemma IsClosed.upperClosure_pi (hs : IsClosed s) (hs' : BddBelow s) :
    IsClosed (upperClosure s : Set (ι → ℝ))

Proof state:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val✝ : Fintype ι
⊢ IsClosed ↑(upperClosure s)

Tactic:
refine IsSeqClosed.isClosed fun f x hf hx ↦ ?_

Result:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val✝ : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hf : ∀ (n : ℕ), f n ∈ ↑(upperClosure s)
hx : Filter.Tendsto f Filter.atTop (nhds x)
⊢ x ∈ ↑(upperClosure s)

Proof state:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val✝ : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hf : ∀ (n : ℕ), f n ∈ ↑(upperClosure s)
hx : Filter.Tendsto f Filter.atTop (nhds x)
⊢ x ∈ ↑(upperClosure s)

Tactic:
choose g hg hgf using hf

Result:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val✝ : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : ℕ → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hgf : ∀ (n : ℕ), g n ≤ f n
⊢ x ∈ ↑(upperClosure s)

Proof state:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val✝ : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : ℕ → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hgf : ∀ (n : ℕ), g n ≤ f n
⊢ x ∈ ↑(upperClosure s)

Tactic:
obtain ⟨a, ha⟩ := hx.bddAbove_range

Result:
case intro.intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val✝ : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : ℕ → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hgf : ∀ (n : ℕ), g n ≤ f n
a : ι → ℝ
ha : a ∈ upperBounds (range f)
⊢ x ∈ ↑(upperClosure s)

Proof state:
case intro.intro.intro.intro.intro.intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val✝ : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : ℕ → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hgf : ∀ (n : ℕ), g n ≤ f n
a : ι → ℝ
ha : a ∈ upperBounds (range f)
b : ι → ℝ
hb : b ∈ closure (s ∩ Iic a)
φ : ℕ → ℕ
hφ : StrictMono φ
hbf : Filter.Tendsto (g ∘ φ) Filter.atTop (nhds b)
⊢ x ∈ ↑(upperClosure s)

Tactic:
exact ⟨b, closure_minimal inter_subset_left hs hb,
  le_of_tendsto_of_tendsto' hbf (hx.comp hφ.tendsto_atTop) fun _ ↦ hgf _⟩

Result:
no goals

Proof state:
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
⊢ IsClosed ↑(upperClosure s)

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val✝ : Fintype ι
⊢ IsClosed ↑(upperClosure s)

Proof state:
case intro.intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val✝ : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : ℕ → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hgf : ∀ (n : ℕ), g n ≤ f n
a : ι → ℝ
ha : a ∈ upperBounds (range f)
⊢ x ∈ ↑(upperClosure s)

Tactic:
obtain ⟨b, hb, φ, hφ, hbf⟩ := tendsto_subseq_of_bounded (hs'.isBounded_inter bddAbove_Iic) fun n ↦
  ⟨hg n, (hgf _).trans <| ha <| mem_range_self _⟩

Result:
case intro.intro.intro.intro.intro.intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val✝ : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : ℕ → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hgf : ∀ (n : ℕ), g n ≤ f n
a : ι → ℝ
ha : a ∈ upperBounds (range f)
b : ι → ℝ
hb : b ∈ closure (s ∩ Iic a)
φ : ℕ → ℕ
hφ : StrictMono φ
hbf : Filter.Tendsto (g ∘ φ) Filter.atTop (nhds b)
⊢ x ∈ ↑(upperClosure s)