awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : (↑s : Set M) ∈ 𝓝 y
x : M
⊢ Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 (y + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 x))

Tactic:
have : Tendsto (fun c : R => y + c • x) (𝓝[{ x : R | IsUnit x }] 0) (𝓝 (y + (0 : R) • x)) :=
    tendsto_const_nhds.add ((tendsto_nhdsWithin_of_tendsto_nhds tendsto_id).smul tendsto_const_nhds)
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : (↑s : Set M) ∈ 𝓝 y
x : M
this : Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 (y + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 x))
⊢ Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 y)

Tactic:
rw [zero_smul, add_zero] at this

Premises used: zero_smul, add_zero
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : (↑s : Set M) ∈ 𝓝 y
x : M
this : Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 y)
obtain : ∀ (u : Rˣ) (hu : y + (↑u : R) • x ∈ s), x ∈ s
⊢ x ∈ s

Tactic:
obtain ⟨_, hu : y + _ • _ ∈ s, u, rfl⟩ :=
    nonempty_of_mem (inter_mem (Filter.mem_map.1 (this hy)) self_mem_nhdsWithin)

Premises used: Filter.inter_mem, Filter.nonempty_of_mem, self_mem_nhdsWithin, Iff.mp, Filter.mem_map, rfl
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : (↑s : Set M) ∈ 𝓝 y
x : M
this : Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 y)
u : Rˣ
hu : y + (↑u : R) • x ∈ s
⊢ y ∈ s

Tactic:
have hy' : y ∈ ↑s := mem_of_mem_nhds hy
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : (↑s : Set M) ∈ 𝓝 y
x : M
this : Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 y)
u : Rˣ
hu : y + (↑u : R) • x ∈ s
hy' : y ∈ s
rwa : ∀ (hu : (↑u : R) • x ∈ s) (hy' : y ∈ s), x ∈ s
rwa₁ : ∀ (hu : u • x ∈ s) (hy' : y ∈ s), x ∈ s
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hu : x ∈ s) (hy' : y ∈ s), x ∈ s
⊢ x ∈ s

Tactic:
rwa [s.add_mem_iff_right hy', ← Units.smul_def, s.smul_mem_iff' u] at hu

Premises used: Submodule.smul_mem_iff', Units.smul_def, Submodule.add_mem_iff_right
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x : M
rcases : ∀ (y : M) (hy : y ≠ 0), (𝓝[≠] x).NeBot
⊢ (𝓝[≠] x).NeBot

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

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
suffices : Tendsto (fun (c : R) ↦ x + c • y) (𝓝[≠] 0) (𝓝[≠] x)
⊢ (𝓝[≠] x).NeBot

Tactic:
suffices Tendsto (fun c : R => x + c • y) (𝓝[≠] 0) (𝓝[≠] x) from this.neBot
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun (c : R) ↦ x + c • y) (𝓝[≠] 0) (𝓝[≠] x)

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

Premises used: Iff.mpr, nhdsWithin, Filter.Tendsto.inf, Filter.tendsto_principal_principal
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
refine_1 : Tendsto (fun (c : R) ↦ x + c • y) (𝓝 0) (𝓝 x)
refine_2 : ∀ (a : R), Membership.mem (γ := Set R) {0}ᶜ a → Membership.mem (γ := Set M) {x}ᶜ (x + a • y)
⊢ Tendsto (fun (c : R) ↦ x + c • y) (𝓝[≠] 0) (𝓝[≠] x)

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

Premises used: Iff.mpr, Filter.Tendsto.inf, Filter.tendsto_principal_principal
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun (x_1 : R) ↦ x + id x_1 • y) (𝓝 0) (𝓝 (x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 y))

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

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.smul_const, Filter.Tendsto.add
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
h : x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 y
⊢ Tendsto (fun (c : R) ↦ x + c • y) (𝓝 0) (𝓝 x)

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

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.smul_const, Filter.Tendsto.add
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
h : x = x + 0
h₁ h₂ : x = x
⊢ x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 y

Tactic:
rw [zero_smul, add_zero]

Premises used: zero_smul, add_zero
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsDomain R
inst_8 : Nontrivial M
inst_9 : NeBot (α := R) (𝓝[≠] 0)
inst_10 : IsTorsionFree R M
x y : M
hy : y ≠ 0
c : R
hc : Membership.mem (γ := Set R) {0}ᶜ c
⊢ Membership.mem (γ := Set M) {x}ᶜ (x + c • y)

Tactic:
simpa [hy] using hc
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂' : Type u_5
φ : R → S
inst : SMul R M₁
inst_1 : SMul S M₂'
u : TopologicalSpace R
u' : TopologicalSpace S
t' : TopologicalSpace M₂'
inst_2 : ContinuousSMul S M₂'
F' : Type u_7
inst_3 : FunLike F' M₁ M₂'
inst_4 : MulActionSemiHomClass F' φ M₁ M₂'
f' : F'
hφ : Continuous[u, u'] φ
⊢ ContinuousSMul R M₁

Tactic:
let _ : TopologicalSpace M₁ := t'.induced f'
  IsInducing.continuousSMul ⟨rfl⟩ hφ (map_smulₛₗ f' _ _)

Premises used: Topology.IsInducing.continuousSMul, MulActionSemiHomClass.map_smulₛₗ, TopologicalSpace.induced, Topology.IsInducing.mk, DFunLike.coe, rfl
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : SMul R M₁
inst_1 : SMul R M₂
u : TopologicalSpace R
t : TopologicalSpace M₂
inst_2 : ContinuousSMul R M₂
F : Type u_6
inst_3 : FunLike F M₁ M₂
inst_4 : MulActionHomClass F R M₁ M₂
f : F
⊢ ContinuousSMul R M₁

Tactic:
continuousSMul_inducedₛₗ f continuous_id

Premises used: continuous_id, continuousSMul_inducedₛₗ
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
rw :
  IsSeparable.{u_2} (α := M)
    (⋃ (n : ℕ),
      (fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s})
⊢ IsSeparable (↑(Submodule.span R s) : Set M)

Tactic:
rw [Submodule.span_eq_iUnion_nat]

Premises used: Submodule.span_eq_iUnion_nat
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
⊢ IsSeparable.{u_2} (α := M)
    (⋃ (n : ℕ),
      (fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s})

Tactic:
.iUnion fun n ↦ .image ?_ ?_

Premises used: TopologicalSpace.IsSeparable.iUnion, TopologicalSpace.IsSeparable.image
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
refine_1 : ∀ (n : ℕ), IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s}
refine_2 : ∀ (n : ℕ), Continuous[Pi.topologicalSpace, inst_3] fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2
⊢ IsSeparable.{u_2} (α := M)
    (⋃ (n : ℕ),
      (fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s})

Tactic:
refine .iUnion fun n ↦ .image ?_ ?_
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
⊢ IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ SProd.sprod (α := Set R) Set.univ s}

Tactic:
apply isSeparable_pi (fun i ↦ .prod (.of_separableSpace Set.univ) hs)

Premises used: Set.univ, TopologicalSpace.isSeparable_pi, TopologicalSpace.IsSeparable.of_separableSpace, TopologicalSpace.IsSeparable.prod
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
⊢ IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ SProd.sprod (α := Set R) Set.univ s}

Tactic:
have : IsSeparable {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ Set.univ ×ˢ s} := by
      apply isSeparable_pi (fun i ↦ .prod (.of_separableSpace Set.univ) hs)
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
this : IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ SProd.sprod (α := Set R) Set.univ s}
refine_1 refine_1₁ refine_1₂ refine_1₃ :
  ∀
    (this :
      IsSeparable (α := Fin n → R × M)
        {f : Fin n → R × M | ∀ (i : Fin n), Membership.mem (γ := Set (R × M)) (Prod.snd ⁻¹' s) (f i)}),
    IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s}
⊢ IsSeparable (α := Fin n → R × M) {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s}

Tactic:
rwa [Set.univ_prod] at this

Premises used: Set.univ_prod
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
apply :
  ∀ (i : Fin n),
    Membership.mem (γ := Finset (Fin n)) Finset.univ i →
      Continuous[Pi.topologicalSpace, inst_3] fun (a : Fin n → R × M) ↦ (a i).1 • (a i).2
⊢ Continuous[Pi.topologicalSpace, inst_3] fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2

Tactic:
apply continuous_finsetSum _ (fun i _ ↦ ?_)

Premises used: continuous_finsetSum
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
i : Fin n
h : Membership.mem (γ := Finset (Fin n)) Finset.univ i
⊢ Continuous[Pi.topologicalSpace, inst_3] fun (a : Fin n → R × M) ↦ (a i).1 • (a i).2

Tactic:
(continuous_fst.comp (continuous_apply i)).smul (continuous_snd.comp (continuous_apply i))

Premises used: Continuous.comp, continuous_snd, continuous_fst, Continuous.smul, continuous_apply
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : TopologicalSpace R
inst_5 : SeparableSpace R
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
i : Fin n
h : Membership.mem (γ := Finset (Fin n)) Finset.univ i
⊢ Continuous[Pi.topologicalSpace, inst_3] fun (a : Fin n → R × M) ↦ (a i).1 • (a i).2

Tactic:
exact (continuous_fst.comp (continuous_apply i)).smul (continuous_snd.comp (continuous_apply i))

Premises used: Continuous.comp, continuous_snd, continuous_fst, Continuous.smul
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
S : Submodule R M
⊢ IsTopologicalAddGroup.{u_2} ↥S

Tactic:
inferInstanceAs (IsTopologicalAddGroup S.toAddSubgroup)

Premises used: _private.0.Submodule.topologicalAddGroup._proof_1
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
s : Submodule R M
c : R
⊢ Set.MapsTo (fun (x : M) ↦ c • x) (closure[inst_1] (↑s : Set M)) (closure[inst_1] (↑s : Set M))

Tactic:
have : Set.MapsTo (c • ·) (s : Set M) s := fun _ h ↦ s.smul_mem c h
  this.closure (continuous_const_smul c)

Premises used: ContinuousConstSMul.continuous_const_smul, Set.MapsTo.closure, Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
s : Submodule R M
c : R
⊢ c • closure[inst_1] (↑s : Set M) ⊆ closure[inst_1] (↑s : Set M)

Tactic:
(s.mapsTo_smul_closure c).image_subset

Premises used: Submodule.mapsTo_smul_closure, Set.MapsTo.image_subset
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Submodule R M
⊢ (↑s.topologicalClosure : Set M) = closure[inst_1] (↑s : Set M)

Tactic:
rfl

Premises used: Set.Mem, setOf, closure, Set.sInter, rfl
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Submodule R M
⊢ s ≤ s.topologicalClosure

Tactic:
subset_closure

Premises used: Set.Mem, subset_closure, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Set M
⊢ closure[inst_1] s ⊆ closure[inst_1] (↑(span R s) : Set M)

Tactic:
closure_mono subset_span

Premises used: closure_mono, Submodule.subset_span
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Set M
⊢ closure[inst_1] s ⊆ closure[inst_1] (↑(span R s) : Set M)

Tactic:
exact closure_mono subset_span

Premises used: closure_mono, Submodule.subset_span
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Submodule R M
⊢ IsClosed[inst_1] (↑s.topologicalClosure : Set M)

Tactic:
isClosed_closure

Premises used: setOf, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s t : Submodule R M
h : s ≤ t
ht : IsClosed[inst_1] (↑t : Set M)
⊢ s.topologicalClosure ≤ t

Tactic:
closure_minimal h ht

Premises used: Set.Mem, closure_minimal, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s t : Submodule R M
h : s ≤ t
⊢ s.topologicalClosure ≤ t.topologicalClosure

Tactic:
closure_mono h

Premises used: Set.Mem, setOf, closure_mono, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Submodule R M
hs : IsClosed[inst_1] (↑s : Set M)
⊢ s.topologicalClosure = s

Tactic:
SetLike.ext' hs.closure_eq

Premises used: IsClosed.closure_eq, SetLike.ext'
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Submodule R M
rw : closure[inst_1] (↑s : Set M) = Set.univ ↔ (↑s.topologicalClosure : Set M) = (↑⊤ : Set M)
⊢ Dense (↑s : Set M) ↔ s.topologicalClosure = ⊤

Tactic:
rw [← SetLike.coe_set_eq, dense_iff_closure_eq]

Premises used: dense_iff_closure_eq, SetLike.coe_set_eq
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Submodule R M
⊢ closure[inst_1] (↑s : Set M) = Set.univ ↔ (↑s.topologicalClosure : Set M) = (↑⊤ : Set M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
M' : Type u_1
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : UniformSpace M'
inst_9 : ContinuousAdd M'
inst_10 : ContinuousConstSMul R M'
inst_11 : CompleteSpace M'
U : Submodule R M'
⊢ CompleteSpace.{u_1} ↥U.topologicalClosure

Tactic:
isClosed_closure.completeSpace_coe

Premises used: Set.Mem, setOf, closure, IsClosed.completeSpace_coe, Set.sInter
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Submodule R M
hs : IsCoatom s
⊢ IsClosed[inst_1] (↑s : Set M) ∨ Dense (↑s : Set M)

Tactic:
(hs.le_iff.mp s.le_topologicalClosure).symm.imp ?_ dense_iff_topologicalClosure_eq_top.mpr

Premises used: Iff.mpr, Submodule.dense_iff_topologicalClosure_eq_top, Submodule.le_topologicalClosure, Or.symm, IsCoatom.le_iff, Iff.mp, Or.imp
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Submodule R M
hs : IsCoatom s
refine : s.topologicalClosure = s → IsClosed[inst_1] (↑s : Set M)
⊢ IsClosed[inst_1] (↑s : Set M) ∨ Dense (↑s : Set M)

Tactic:
refine (hs.le_iff.mp s.le_topologicalClosure).symm.imp ?_ dense_iff_topologicalClosure_eq_top.mpr

Premises used: Iff.mpr, Submodule.dense_iff_topologicalClosure_eq_top, Submodule.le_topologicalClosure, Or.symm, IsCoatom.le_iff, Iff.mp, Or.imp
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Submodule R M
hs : IsCoatom s
⊢ s.topologicalClosure = s → IsClosed[inst_1] (↑s : Set M)

Tactic:
fun h ↦ h ▸ isClosed_closure

Premises used: Eq.rec, isClosed_closure
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : ContinuousConstSMul R M
inst_5 : ContinuousAdd M
s : Submodule R M
hs : IsCoatom s
⊢ s.topologicalClosure = s → IsClosed[inst_1] (↑s : Set M)

Tactic:
exact fun h ↦ h ▸ isClosed_closure
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : UniformSpace M
inst_3 : Module R M
inst_4 : CompleteSpace M
K : Submodule R M
c : IsClosed[inst_2.toTopologicalSpace] (↑K : Set M)
⊢ CompleteSpace.{u_2} ↥K

Tactic:
IsComplete.completeSpace_coe (c.isComplete)

Premises used: IsComplete.completeSpace_coe, IsClosed.isComplete
-- Module: Mathlib.Topology.Algebra.Module.Basic
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : (i : ι) → TopologicalSpace (M i)
inst_4 : DecidableEq ι
s : (i : ι) → Submodule R (M i)
rw :
  closure[Pi.topologicalSpace] (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i)) =
    closure[Pi.topologicalSpace] (Set.pi (α := M) Set.univ fun (i : ι) ↦ (↑(s i) : Set (M i)))
⊢ closure[Pi.topologicalSpace] (↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) : Set ((i : ι) → M i)) =
    Set.pi (α := M) Set.univ fun (i : ι) ↦ closure[inst_3 i] (↑(s i) : Set (M i))

Tactic:
rw [← closure_pi_set]

Premises used: closure_pi_set