-- Mathlib/Topology/Algebra/Module/Basic.lean
theorem Module.punctured_nhds_neBot [Nontrivial M] [NeBot (𝓝[≠] (0 : R))] [NoZeroSMulDivisors R M]
    (x : M) : NeBot (𝓝[≠] x)

Proof state:
case intro.refine_2
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ ∀ a ∈ {0}ᶜ, x + a • y ∈ {x}ᶜ

Tactic:
intro c hc

Result:
case intro.refine_2
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
c : R
hc : c ∈ {0}ᶜ
⊢ x + c • y ∈ {x}ᶜ

Proof state:
case intro.refine_1
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c => x + c • y) (𝓝 0) (𝓝 x)

Tactic:
convert tendsto_const_nhds.add ((@tendsto_id R _).smul_const y)

Result:
case h.e'_5.h.e'_3
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ x = x + 0 • y

Proof state:
case intro.refine_2
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
c : R
hc : c ∈ {0}ᶜ
⊢ x + c • y ∈ {x}ᶜ

Tactic:
simpa [hy] using hc

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ (𝓝[≠] x).NeBot

Tactic:
suffices Tendsto (fun c : R => x + c • y) (𝓝[≠] 0) (𝓝[≠] x) from this.neBot

Result:
case intro
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c => x + c • y) (𝓝[≠] 0) (𝓝[≠] x)

Proof state:
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x : M
⊢ (𝓝[≠] x).NeBot

Tactic:
rcases exists_ne (0 : M) with ⟨y, hy⟩

Result:
case intro
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ (𝓝[≠] x).NeBot

Proof state:
case h.e'_5.h.e'_3
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ x = x + 0 • y

Tactic:
rw [zero_smul, add_zero]

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c => x + c • y) (𝓝[≠] 0) (𝓝[≠] x)

Tactic:
refine Tendsto.inf ?_ (tendsto_principal_principal.2 <| ?_)

Result:
case intro.refine_1
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c => x + c • y) (𝓝 0) (𝓝 x)

case intro.refine_2
R : Type u_1
M : Type u_2
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✝¹ : (𝓝[≠] 0).NeBot
inst✝ : NoZeroSMulDivisors R M
x y : M
hy : y ≠ 0
⊢ ∀ a ∈ {0}ᶜ, x + a • y ∈ {x}ᶜ