case intro
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ NeBot (𝓝[{x}ᶜ] x)
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x : M
⊢ NeBot (𝓝[{x}ᶜ] x)
rcases exists_ne (0 : M) with ⟨y, hy⟩
case intro
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
this : Tendsto (fun c => x + c • y) (𝓝[{0}ᶜ] 0) (𝓝[{x}ᶜ] x)
⊢ NeBot (𝓝[{x}ᶜ] x)

case this
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c => x + c • y) (𝓝[{0}ᶜ] 0) (𝓝[{x}ᶜ] x)
case intro
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ NeBot (𝓝[{x}ᶜ] x)
suffices : Tendsto (fun c : R => x + c • y) (𝓝[≠] 0) (𝓝[≠] x)
case this
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c => x + c • y) (𝓝[{0}ᶜ] 0) (𝓝[{x}ᶜ] x)
case intro
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
this : Tendsto (fun c => x + c • y) (𝓝[{0}ᶜ] 0) (𝓝[{x}ᶜ] x)
⊢ NeBot (𝓝[{x}ᶜ] x)

case this
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c => x + c • y) (𝓝[{0}ᶜ] 0) (𝓝[{x}ᶜ] x)
exact this.neBot
case this.refine'_1
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c => x + c • y) (𝓝 0) (𝓝 x)

case this.refine'_2
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ ∀ (a : R), a ∈ {0}ᶜ → x + a • y ∈ {x}ᶜ
case this
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c => x + c • y) (𝓝[{0}ᶜ] 0) (𝓝[{x}ᶜ] x)
refine' Tendsto.inf _ (tendsto_principal_principal.2 <| _)
case h.e'_5.h.e'_3
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ x = x + 0 • y
case this.refine'_1
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c => x + c • y) (𝓝 0) (𝓝 x)
convert tendsto_const_nhds.add ((@tendsto_id R _).smul_const y)
no goals
case h.e'_5.h.e'_3
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ x = x + 0 • y
rw [zero_smul, add_zero]
case this.refine'_2
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
c : R
hc : c ∈ {0}ᶜ
⊢ x + c • y ∈ {x}ᶜ
case this.refine'_2
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ ∀ (a : R), a ∈ {0}ᶜ → x + a • y ∈ {x}ᶜ
intro c hc
no goals
case this.refine'_2
R : Type u_2
M : Type u_1
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : ContinuousAdd M
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Nontrivial M
inst✝¹ : NeBot (𝓝[{0}ᶜ] 0)
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
c : R
hc : c ∈ {0}ᶜ
⊢ x + c • y ∈ {x}ᶜ
simpa [hy] using hc