-- Mathlib/Analysis/Normed/Group/AddTorsor.lean
theorem IsClosed.vadd_right_of_isCompact {s : Set V} {t : Set P} (hs : IsClosed s)
    (ht : IsCompact t) : IsClosed (s +ᵥ t)

Proof state:
case intro.intro.intro.intro
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
hup : Tendsto u atTop (𝓝 p)
a : ℕ → V
ha : ∀ (n : ℕ), a n ∈ s
v : ℕ → P
hv : ∀ (n : ℕ), v n ∈ t
hav : ∀ (n : ℕ), (fun x1 x2 => x1 +ᵥ x2) (a n) (v n) = u n
q : P
hqt : q ∈ t
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφq : Tendsto (v ∘ φ) atTop (𝓝 q)
n : ℕ
⊢ (u ∘ φ -ᵥ v ∘ φ) n ∈ s

Tactic:
convert ha (φ n) using 1

Result:
case h.e'_5
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
hup : Tendsto u atTop (𝓝 p)
a : ℕ → V
ha : ∀ (n : ℕ), a n ∈ s
v : ℕ → P
hv : ∀ (n : ℕ), v n ∈ t
hav : ∀ (n : ℕ), (fun x1 x2 => x1 +ᵥ x2) (a n) (v n) = u n
q : P
hqt : q ∈ t
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφq : Tendsto (v ∘ φ) atTop (𝓝 q)
n : ℕ
⊢ (u ∘ φ -ᵥ v ∘ φ) n = a (φ n)

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
⊢ IsClosed (s +ᵥ t)

Tactic:
refine IsSeqClosed.isClosed (fun u p husv hup ↦ ?_)

Result:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
husv : ∀ (n : ℕ), u n ∈ s +ᵥ t
hup : Tendsto u atTop (𝓝 p)
⊢ p ∈ s +ᵥ t

Proof state:
case intro.intro.intro.intro
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
hup : Tendsto u atTop (𝓝 p)
a : ℕ → V
ha : ∀ (n : ℕ), a n ∈ s
v : ℕ → P
hv : ∀ (n : ℕ), v n ∈ t
hav : ∀ (n : ℕ), (fun x1 x2 => x1 +ᵥ x2) (a n) (v n) = u n
q : P
hqt : q ∈ t
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφq : Tendsto (v ∘ φ) atTop (𝓝 q)
⊢ p ∈ s +ᵥ t

Tactic:
refine ⟨p -ᵥ q, hs.mem_of_tendsto ((hup.comp φ_mono.tendsto_atTop).vsub hφq)
  (Eventually.of_forall fun n ↦ ?_), q, hqt, vsub_vadd _ _⟩

Result:
case intro.intro.intro.intro
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
hup : Tendsto u atTop (𝓝 p)
a : ℕ → V
ha : ∀ (n : ℕ), a n ∈ s
v : ℕ → P
hv : ∀ (n : ℕ), v n ∈ t
hav : ∀ (n : ℕ), (fun x1 x2 => x1 +ᵥ x2) (a n) (v n) = u n
q : P
hqt : q ∈ t
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφq : Tendsto (v ∘ φ) atTop (𝓝 q)
n : ℕ
⊢ (u ∘ φ -ᵥ v ∘ φ) n ∈ s

Proof state:
case h.e'_5
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
hup : Tendsto u atTop (𝓝 p)
a : ℕ → V
ha : ∀ (n : ℕ), a n ∈ s
v : ℕ → P
hv : ∀ (n : ℕ), v n ∈ t
hav : ∀ (n : ℕ), (fun x1 x2 => x1 +ᵥ x2) (a n) (v n) = u n
q : P
hqt : q ∈ t
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφq : Tendsto (v ∘ φ) atTop (𝓝 q)
n : ℕ
⊢ (u ∘ φ -ᵥ v ∘ φ) n = a (φ n)

Tactic:
exact (eq_vadd_iff_vsub_eq _ _ _).mp (hav (φ n)).symm

Result:
no goals

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
husv : ∀ (n : ℕ), u n ∈ s +ᵥ t
hup : Tendsto u atTop (𝓝 p)
⊢ p ∈ s +ᵥ t

Tactic:
choose! a ha v hv hav using husv

Result:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
hup : Tendsto u atTop (𝓝 p)
a : ℕ → V
ha : ∀ (n : ℕ), a n ∈ s
v : ℕ → P
hv : ∀ (n : ℕ), v n ∈ t
hav : ∀ (n : ℕ), (fun x1 x2 => x1 +ᵥ x2) (a n) (v n) = u n
⊢ p ∈ s +ᵥ t

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
hup : Tendsto u atTop (𝓝 p)
a : ℕ → V
ha : ∀ (n : ℕ), a n ∈ s
v : ℕ → P
hv : ∀ (n : ℕ), v n ∈ t
hav : ∀ (n : ℕ), (fun x1 x2 => x1 +ᵥ x2) (a n) (v n) = u n
⊢ p ∈ s +ᵥ t

Tactic:
rcases ht.isSeqCompact hv with ⟨q, hqt, φ, φ_mono, hφq⟩

Result:
case intro.intro.intro.intro
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
hup : Tendsto u atTop (𝓝 p)
a : ℕ → V
ha : ∀ (n : ℕ), a n ∈ s
v : ℕ → P
hv : ∀ (n : ℕ), v n ∈ t
hav : ∀ (n : ℕ), (fun x1 x2 => x1 +ᵥ x2) (a n) (v n) = u n
q : P
hqt : q ∈ t
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφq : Tendsto (v ∘ φ) atTop (𝓝 q)
⊢ p ∈ s +ᵥ t