awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen[inst_3] s
h's : s.Nonempty
rcases : ∀ (x : E) (hx : x ∈ s), #(↑s : Type u_1) = #E
⊢ #(↑s : Type u_1) = #E

Tactic:
rcases h's with ⟨x, hx⟩
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen[inst_3] s
x : E
hx : x ∈ s
⊢ #(↑s : Type u_1) = #E

Tactic:
cardinal_eq_of_mem_nhds 𝕜 (hs.mem_nhds hx)

Premises used: IsOpen.mem_nhds, cardinal_eq_of_mem_nhds
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddGroup E
inst_2 : MulActionWithZero 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen[inst_3] s
x : E
hx : x ∈ s
⊢ #(↑s : Type u_1) = #E

Tactic:
exact cardinal_eq_of_mem_nhds 𝕜 (hs.mem_nhds hx)

Premises used: IsOpen.mem_nhds, cardinal_eq_of_mem_nhds
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
E : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen[inst_5] s
h's : s.Nonempty
⊢ 𝔠 ≤ #(↑s : Type u_1)

Tactic:
simpa [cardinal_eq_of_isOpen 𝕜 hs h's] using continuum_le_cardinal_of_module 𝕜 E

Premises used: cardinal_eq_of_isOpen, continuum_le_cardinal_of_module
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
E : Type u
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
rw : interior s = ∅
⊢ Dense sᶜ

Tactic:
rw [← interior_eq_empty_iff_dense_compl]

Premises used: interior_eq_empty_iff_dense_compl
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
E : Type u
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
by_contra : ∀ (H : ¬interior s = ∅), False
⊢ interior s = ∅

Tactic:
by_contra H
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
E : Type u
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
H : ¬interior s = ∅
apply : ℵ₀ < ℵ₀
⊢ False

Tactic:
apply lt_irrefl (ℵ₀ : Cardinal.{u})
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
E : Type u
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
H : ¬interior s = ∅
⊢ ℵ₀ < 𝔠

Tactic:
aleph0_lt_continuum

Premises used: Cardinal.aleph0_lt_continuum
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
E : Type u
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
H : ¬interior s = ∅
⊢ 𝔠 ≤ #(↑(interior s) : Type u)

Tactic:
continuum_le_cardinal_of_isOpen 𝕜 isOpen_interior (notMem_singleton_empty.1 H)

Premises used: isOpen_interior, Set.notMem_singleton_empty, Iff.mp, continuum_le_cardinal_of_isOpen
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
E : Type u
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
H : ¬interior s = ∅
⊢ #(↑(interior s) : Type u) ≤ #(↑s : Type u)

Tactic:
mk_le_mk_of_subset interior_subset

Premises used: interior_subset, Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
E : Type u
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
H : ¬interior s = ∅
⊢ #(↑s : Type u) ≤ ℵ₀

Tactic:
le_aleph0 hs

Premises used: Set.Countable.le_aleph0
-- Module: Mathlib.Topology.Algebra.Module.Cardinality
Goal:
E : Type u
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nontrivial E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Countable
H : ¬interior s = ∅
⊢ ℵ₀ < ℵ₀

Tactic:
calc
    (ℵ₀ : Cardinal.{u}) < 𝔠 := aleph0_lt_continuum
    _ ≤ #(interior s) :=
      continuum_le_cardinal_of_isOpen 𝕜 isOpen_interior (notMem_singleton_empty.1 H)
    _ ≤ #s := mk_le_mk_of_subset interior_subset
    _ ≤ ℵ₀ := le_aleph0 hs

Premises used: interior_subset, isOpen_interior, Set.Countable.le_aleph0, Cardinal.mk_le_mk_of_subset, interior, Set.notMem_singleton_empty, Iff.mp, Cardinal.aleph0_lt_continuum, continuum_le_cardinal_of_isOpen
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
s t : ClosedSubmodule R M
h : (↑s : Submodule R M) = (↑t : Submodule R M)
mk :
  ∀ (toSubmodule : Submodule R M) (isClosed' : IsClosed toSubmodule.carrier)
    (h :
      (↑{ toSubmodule := toSubmodule, isClosed' := isClosed' : ClosedSubmodule R M } : Submodule R M) =
        (↑t : Submodule R M)),
    { toSubmodule := toSubmodule, isClosed' := isClosed' : ClosedSubmodule R M } = t
⊢ s = t

Tactic:
cases s
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
t : ClosedSubmodule R M
toSubmodule : Submodule R M
isClosed' : IsClosed toSubmodule.carrier
h :
  (↑{ toSubmodule := toSubmodule, isClosed' := isClosed' : ClosedSubmodule R M } : Submodule R M) = (↑t : Submodule R M)
⊢ { toSubmodule := toSubmodule, isClosed' := isClosed' : ClosedSubmodule R M } = t

Tactic:
congr!
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
⊢ Injective.{u_3 + 1, u_3 + 1} (α := ClosedSubmodule R M) toCloseds

Tactic:
fun _s _t h ↦ SetLike.coe_injective congr(($h : Set M))

Premises used: congrArg, id, SetLike.coe_injective, SetLike.coe, Function.Injective
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
s : ClosedSubmodule R M
⊢ (↑s : Submodule R M).carrier = (↑s : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
x : M
s : Submodule R M
hs : IsClosed s.carrier
⊢ x ∈ { toSubmodule := s, isClosed' := hs : ClosedSubmodule R M } ↔ x ∈ s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
s : ClosedSubmodule R M
⊢ (↑(↑s : Submodule R M) : Set M) = (↑s : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
x : M
s : ClosedSubmodule R M
⊢ x ∈ (↑s : Submodule R M) ↔ x ∈ s

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
s : ClosedSubmodule R M
⊢ (↑(↑s : Closeds M) : Set M) = (↑s : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
s : ClosedSubmodule R M
⊢ IsClosed (↑s : Set M)

Tactic:
s.isClosed'

Premises used: ClosedSubmodule.isClosed'
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
s t : ClosedSubmodule R M
⊢ (↑s : Submodule R M) ≤ (↑t : Submodule R M) ↔ s ≤ t

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
ι : Sort u_1
R : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
inst_6 : Module R N
inst_7 : AddCommMonoid O
inst_8 : TopologicalSpace O
inst_9 : Module R O
s_1 t : ClosedSubmodule R M
x : M
f : M →L[R] N
s : ClosedSubmodule R N
⊢ IsClosed (Submodule.comap (↑f : M →ₗ[R] N) (↑s : Submodule R N)).carrier

Tactic:
simpa using s.isClosed.preimage f.continuous

Premises used: ContinuousLinearMap.continuous, ClosedSubmodule.isClosed, IsClosed.preimage
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
inst_6 : Module R N
f : M →L[R] N
s : ClosedSubmodule R N
x : M
⊢ x ∈ comap f s ↔ Membership.mem (α := N) s ((f : (a : M) → N) x : N)

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
inst_6 : Module R N
f : M →L[R] N
s : ClosedSubmodule R N
⊢ (↑(comap f s) : Submodule R M) = Submodule.comap (↑f : M →ₗ[R] N) (↑s : Submodule R N)

Tactic:
rfl

Premises used: Submodule.comap, rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
s : ClosedSubmodule R M
⊢ comap (ContinuousLinearMap.id R M) s = s

Tactic:
rfl

Premises used: Set.Mem, setOf, ClosedSubmodule.comap, Submodule.comap, Set.preimage, rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
inst_6 : Module R N
inst_7 : AddCommMonoid O
inst_8 : TopologicalSpace O
inst_9 : Module R O
g : N →L[R] O
f : M →L[R] N
s : ClosedSubmodule R O
⊢ comap f (comap g s) = comap (g ∘SL f) s

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, Set.Mem, setOf, ClosedSubmodule.comap, Submodule.comap, Set.preimage, rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
ι : Sort u_1
R : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
inst_6 : Module R N
inst_7 : AddCommMonoid O
inst_8 : TopologicalSpace O
inst_9 : Module R O
s t : ClosedSubmodule R M
x : M
S : Set (ClosedSubmodule R M)
⊢ IsClosed.{u_3} (X := M)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_2, u_3} (R := R) (⨅ s ∈ S, (↑s : Submodule R M)))))

Tactic:
simpa using isClosed_biInter fun x hx ↦ x.isClosed

Premises used: isClosed_biInter
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
S : Set (ClosedSubmodule R M)
⊢ (↑(sInf S) : Submodule R M) = ⨅ s ∈ S, (↑s : Submodule R M)

Tactic:
rfl

Premises used: iInf, rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
ι : Sort u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
f : ι → ClosedSubmodule R M
rw :
  Eq.{u_3 + 1} (α := Submodule R M) (↑(sInf (Set.range fun (i : ι) ↦ f i)) : Submodule R M)
    (⨅ (i : ι), (↑(f i) : Submodule R M))
rw₁ :
  Eq.{u_3 + 1} (α := Submodule R M)
    (⨅ (s : ClosedSubmodule R M),
      ⨅ (_ : Membership.mem (γ := Set (ClosedSubmodule R M)) (Set.range fun (i : ι) ↦ f i) s), (↑s : Submodule R M))
    (⨅ (i : ι), (↑(f i) : Submodule R M))
rw₂ rw₃ : Eq.{u_3 + 1} (α := Submodule R M) (⨅ (i : ι), (↑(f i) : Submodule R M)) (⨅ (i : ι), (↑(f i) : Submodule R M))
⊢ Eq.{u_3 + 1} (α := Submodule R M) (↑(⨅ (i : ι), f i) : Submodule R M) (⨅ (i : ι), (↑(f i) : Submodule R M))

Tactic:
rw [iInf, toSubmodule_sInf, iInf_range]

Premises used: iInf, iInf_range, ClosedSubmodule.toSubmodule_sInf
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
S : Set (ClosedSubmodule R M)
⊢ (↑(sInf S) : Set M) = ⨅ s ∈ S, (↑s : Set M)

Tactic:
simp [← coe_toSubmodule]

Premises used: ClosedSubmodule.coe_toSubmodule
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
ι : Sort u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
f : ι → ClosedSubmodule R M
⊢ (↑(⨅ (i : ι), f i) : Set M) = ⨅ (i : ι), (↑(f i) : Set M)

Tactic:
simp [← coe_toSubmodule]

Premises used: ClosedSubmodule.coe_toSubmodule
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
x : M
S : Set (ClosedSubmodule R M)
⊢ x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s

Tactic:
simp [← SetLike.mem_coe]

Premises used: SetLike.mem_coe
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
ι : Sort u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
x : M
f : ι → ClosedSubmodule R M
⊢ Membership.mem (γ := ClosedSubmodule R M) (⨅ (i : ι), f i) x ↔ ∀ (i : ι), x ∈ f i

Tactic:
simp [← SetLike.mem_coe]

Premises used: SetLike.mem_coe
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
s t : ClosedSubmodule R M
⊢ (↑(s ⊓ t) : Submodule R M) = (↑s : Submodule R M) ⊓ (↑t : Submodule R M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
s t : ClosedSubmodule R M
⊢ (↑(s ⊓ t) : Set M) = (↑s : Set M) ⊓ (↑t : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
s t : ClosedSubmodule R M
x : M
⊢ x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
⊢ Eq.{u_3 + 1} (α := Submodule R M) (↑⊤ : Submodule R M) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
⊢ (↑⊤ : Set M) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
x : M
⊢ Membership.mem (γ := ClosedSubmodule R M) ⊤ x

Tactic:
trivial

Premises used: trivial, Set.Mem, Set.univ, setOf
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : T1Space M
⊢ Eq.{u_3 + 1} (α := Submodule R M) (↑⊥ : Submodule R M) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : T1Space M
⊢ (↑⊥ : Set M) = {0}

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
x : M
inst_4 : T1Space M
⊢ Membership.mem (γ := ClosedSubmodule R M) ⊥ x ↔ x = 0

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
s : Submodule R M
t : ClosedSubmodule R M
⊢ s.closure ≤ t ↔ s ≤ (↑t : Submodule R M)

Tactic:
t.isClosed.closure_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, IsClosed.closure_subset_iff, closure, ClosedSubmodule.isClosed, Set.sInter
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
x : M
s : Submodule R M
⊢ Membership.mem (γ := ClosedSubmodule R M) s.closure x ↔ x ∈ s.topologicalClosure

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
s : ClosedSubmodule R M
carrier : ∀ (x : M), x ∈ (↑(↑s : Submodule R M).closure : Submodule R M).carrier ↔ x ∈ (↑s : Submodule R M).carrier
⊢ (↑s : Submodule R M).closure = s

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
s : ClosedSubmodule R M
x : M
carrier : x ∈ (↑s : Set M) ↔ x ∈ s
carrier₁ : IsClosed (↑s : Set M)
⊢ x ∈ closure (↑s : Set M) ↔ x ∈ s

Tactic:
rw [closure_eq_iff_isClosed.mpr]

Premises used: Iff.mpr, closure_eq_iff_isClosed
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
s : ClosedSubmodule R M
x : M
⊢ x ∈ (↑s : Set M) ↔ x ∈ s

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
s : ClosedSubmodule R M
x : M
⊢ IsClosed (↑s : Set M)

Tactic:
s.isClosed'

Premises used: ClosedSubmodule.isClosed'
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
s : ClosedSubmodule R M
x : M
⊢ IsClosed (↑s : Set M)

Tactic:
exact s.isClosed'

Premises used: ClosedSubmodule.isClosed'
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
s : Submodule R M
hs : IsClosed s.carrier
carrier :
  ∀ (x : M),
    x ∈ (↑s.closure : Submodule R M).carrier ↔
      x ∈ (↑{ toSubmodule := s, isClosed' := hs : ClosedSubmodule R M } : Submodule R M).carrier
⊢ s.closure = { toSubmodule := s, isClosed' := hs : ClosedSubmodule R M }

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
s : Submodule R M
hs : IsClosed s.carrier
x : M
⊢ x ∈ (↑s.closure : Submodule R M).carrier ↔
    x ∈ (↑{ toSubmodule := s, isClosed' := hs : ClosedSubmodule R M } : Submodule R M).carrier

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : TopologicalSpace N
inst_3 : Module R N
inst_4 : ContinuousAdd N
inst_5 : ContinuousConstSMul R N
s : ClosedSubmodule R N
carrier : ∀ (x : N), x ∈ (↑(↑s : Submodule R N).closure : Submodule R N).carrier ↔ x ∈ (↑s : Submodule R N).carrier
⊢ (↑s : Submodule R N).closure = s

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : TopologicalSpace N
inst_3 : Module R N
inst_4 : ContinuousAdd N
inst_5 : ContinuousConstSMul R N
s : ClosedSubmodule R N
x : N
⊢ x ∈ (↑(↑s : Submodule R N).closure : Submodule R N).carrier ↔ x ∈ (↑s : Submodule R N).carrier

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
s : ClosedSubmodule R M
⊢ (↑(map (ContinuousLinearMap.id R M) s) : Set M) = (↑s : Set M)

Tactic:
simp [map]

Premises used: ClosedSubmodule.map
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
inst_6 : Module R N
inst_7 : ContinuousAdd N
inst_8 : ContinuousConstSMul R N
f : M →L[R] N
s : ClosedSubmodule R M
t : ClosedSubmodule R N
simp : (↑s : Submodule R M) ≤ Submodule.comap (↑f : M →ₗ[R] N) (↑t : Submodule R N) ↔ s ≤ comap f t
⊢ map f s ≤ t ↔ s ≤ comap f t

Tactic:
simp [map, Submodule.map_le_iff_le_comap]

Premises used: Submodule.map_le_iff_le_comap, ClosedSubmodule.map
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
inst_6 : Module R N
inst_7 : ContinuousAdd N
inst_8 : ContinuousConstSMul R N
f : M →L[R] N
s : ClosedSubmodule R M
t : ClosedSubmodule R N
⊢ (↑s : Submodule R M) ≤ Submodule.comap (↑f : M →ₗ[R] N) (↑t : Submodule R N) ↔ s ≤ comap f t

Tactic:
simp [← toSubmodule_le_toSubmodule]

Premises used: ClosedSubmodule.toSubmodule_le_toSubmodule