-- Mathlib/Topology/Order/Lattice.lean
lemma finset_sup'_nhds [SemilatticeSup L] [ContinuousSup L]
    (hne : s.Nonempty) (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) :
    Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))

Proof state:
case singleton
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a✝ : ι
hs : ∀ i ∈ {a✝}, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto ({a✝}.sup' ⋯ f) l (𝓝 ({a✝}.sup' ⋯ g))

Tactic:
simpa using hs

Result:
no goals

Proof state:
case cons
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s✝ : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
⊢ Tendsto (f a ⊔ s.sup' hne f) l (𝓝 (g a ⊔ s.sup' hne g))

Tactic:
exact hs.1.sup_nhds (ihs hs.2)

Result:
no goals

Proof state:
case cons
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s✝ : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : ∀ i ∈ cons a s ha, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto ((cons a s ha).sup' ⋯ f) l (𝓝 ((cons a s ha).sup' ⋯ g))

Tactic:
rw [forall_mem_cons] at hs

Result:
case cons
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s✝ : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
⊢ Tendsto ((cons a s ha).sup' ⋯ f) l (𝓝 ((cons a s ha).sup' ⋯ g))

Proof state:
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
hne : s.Nonempty
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))

Tactic:
induction hne using Finset.Nonempty.cons_induction with
| singleton => simpa using hs
| cons a s ha hne ihs =>
  rw [forall_mem_cons] at hs
  simp only [sup'_cons, hne]
  exact hs.1.sup_nhds (ihs hs.2)

Result:
no goals

Proof state:
case cons
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s✝ : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
⊢ Tendsto ((cons a s ha).sup' ⋯ f) l (𝓝 ((cons a s ha).sup' ⋯ g))

Tactic:
simp only [sup'_cons, hne]

Result:
case cons
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s✝ : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
⊢ Tendsto (f a ⊔ s.sup' hne f) l (𝓝 (g a ⊔ s.sup' hne g))