awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
carrier :
  ∀ (x : N),
    Membership.mem (γ := Set N)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
              (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) ⊤) : Submodule R N))))
        x ↔
      Membership.mem (γ := Set N)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_2, u_4} (R := R) (↑⊤ : Submodule R N))))
        x
⊢ Eq.{u_4 + 1} (α := ClosedSubmodule R N) ((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) ⊤) ⊤

Tactic:
ext x
-- 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
x : N
⊢ Membership.mem (γ := Set N)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
            (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) ⊤) : Submodule R N))))
      x ↔
    Membership.mem (γ := Set N)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_2, u_4} (R := R) (↑⊤ : Submodule R N))))
      x

Tactic:
simp
-- 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 t : ClosedSubmodule R M
carrier :
  ∀ (x : N),
    Membership.mem (γ := Set N)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
              (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) (s ⊓ t)) : Submodule R N))))
        x ↔
      Membership.mem (γ := Set N)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
              (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) s ⊓
                    (mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) t) :
                Submodule R N))))
        x
⊢ Eq.{u_4 + 1} (α := ClosedSubmodule R N)
    ((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) (s ⊓ t) : ClosedSubmodule R N)
    ((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) s ⊓
        (mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) t :
      ClosedSubmodule R N)

Tactic:
ext x
-- 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 t : ClosedSubmodule R M
x : N
⊢ Membership.mem (γ := Set N)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
            (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) (s ⊓ t)) : Submodule R N))))
      x ↔
    Membership.mem (γ := Set N)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
            (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) s ⊓
                  (mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) t) :
              Submodule R N))))
      x

Tactic:
simp only [Submodule.carrier_eq_coe, coe_toSubmodule, SetLike.mem_coe, toSubmodule_inf,
    Submodule.coe_inf, Set.mem_inter_iff, mem_mapEquiv_iff, mem_inf]

Premises used: Set.mem_inter_iff, ClosedSubmodule.mem_inf, Submodule.coe_inf, SetLike.mem_coe, ClosedSubmodule.mem_mapEquiv_iff, ClosedSubmodule.toSubmodule_inf, Submodule.carrier_eq_coe, ClosedSubmodule.coe_toSubmodule
-- 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
inst_7 : ContinuousAdd N
inst_8 : ContinuousConstSMul R N
inst_9 : ContinuousAdd M
inst_10 : ContinuousConstSMul R M
s : Submodule R M
carrier :
  ∀ (x : N),
    x ∈ (↑(Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) s).closure : Submodule R N).carrier ↔
      Membership.mem (γ := Set N)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
              (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) s.closure) : Submodule R N))))
        x
⊢ Eq (α := ClosedSubmodule R N) (Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) s).closure
    ((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) s.closure)

Tactic:
ext x
-- 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
inst_7 : ContinuousAdd N
inst_8 : ContinuousConstSMul R N
inst_9 : ContinuousAdd M
inst_10 : ContinuousConstSMul R M
s : Submodule R M
x : N
carrier :
  Membership.mem (γ := Set N) (closure ((fun (a : M) ↦ (f : (a : M) → N) a) '' (↑s : Set M))) x ↔
    ∃ x_1 ∈ closure (↑s : Set M), (f : (a : M) → N) x_1 = x
⊢ x ∈ (↑(Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) s).closure : Submodule R N).carrier ↔
    Membership.mem (γ := Set N)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
            (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) s.closure) : Submodule R N))))
      x

Tactic:
simp only [Submodule.carrier_eq_coe, coe_toSubmodule, Submodule.coe_closure, Submodule.map_coe,
    LinearEquiv.coe_coe, ContinuousLinearEquiv.coe_toLinearEquiv, mapEquiv_apply, Set.mem_image]

Premises used: Set.mem_image, ContinuousLinearEquiv.coe_toLinearEquiv, ClosedSubmodule.mapEquiv_apply, Submodule.coe_closure, Submodule.map_coe, Submodule.carrier_eq_coe, ClosedSubmodule.coe_toSubmodule, LinearEquiv.coe_coe
-- 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
inst_7 : ContinuousAdd N
inst_8 : ContinuousConstSMul R N
inst_9 : ContinuousAdd M
inst_10 : ContinuousConstSMul R M
s : Submodule R M
x : N
carrier :
  Membership.mem (γ := Set N) ((⇑f : (a : M) → N) '' closure (↑s : Set M)) x ↔
    ∃ x_1 ∈ closure (↑s : Set M), (f : (a : M) → N) x_1 = x
⊢ Membership.mem (γ := Set N) (closure ((fun (a : M) ↦ (f : (a : M) → N) a) '' (↑s : Set M))) x ↔
    ∃ x_1 ∈ closure (↑s : Set M), (f : (a : M) → N) x_1 = x

Tactic:
rw [← ContinuousLinearEquiv.image_closure]

Premises used: ContinuousLinearEquiv.image_closure
-- 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
inst_7 : ContinuousAdd N
inst_8 : ContinuousConstSMul R N
inst_9 : ContinuousAdd M
inst_10 : ContinuousConstSMul R M
s : Submodule R M
x : N
⊢ Membership.mem (γ := Set N) ((⇑f : (a : M) → N) '' closure (↑s : Set M)) x ↔
    ∃ x_1 ∈ closure (↑s : Set M), (f : (a : M) → N) x_1 = x

Tactic:
simp
-- 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
inst_9 : ContinuousAdd M
inst_10 : ContinuousConstSMul R M
f : M ≃L[R] N
s t : ClosedSubmodule R M
carrier :
  ∀ (x : N),
    Membership.mem (γ := Set N)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
              (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) (s ⊔ t)) : Submodule R N))))
        x ↔
      Membership.mem (γ := Set N)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
              (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) s ⊔
                    (mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) t) :
                Submodule R N))))
        x
⊢ Eq.{u_4 + 1} (α := ClosedSubmodule R N)
    ((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) (s ⊔ t) : ClosedSubmodule R N)
    ((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) s ⊔
        (mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) t :
      ClosedSubmodule R N)

Tactic:
ext x
-- 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
inst_9 : ContinuousAdd M
inst_10 : ContinuousConstSMul R M
f : M ≃L[R] N
s t : ClosedSubmodule R M
x : N
carrier :
  (∃ x_1 ∈ closure (↑((↑s : Submodule R M) ⊔ (↑t : Submodule R M)) : Set M), (f : (a : M) → N) x_1 = x) ↔
    x ∈
      closure
        (↑(Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑s : Submodule R M) ⊔
              Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑t : Submodule R M)) :
          Set N)
⊢ Membership.mem (γ := Set N)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
            (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) (s ⊔ t)) : Submodule R N))))
      x ↔
    Membership.mem (γ := Set N)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
            (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) s ⊔
                  (mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) t) :
              Submodule R N))))
      x

Tactic:
simp only [mapEquiv_apply, toSubmodule_sup, Submodule.carrier_eq_coe, Submodule.map_coe,
    LinearEquiv.coe_coe, ContinuousLinearEquiv.coe_toLinearEquiv, coe_toSubmodule,
    Submodule.coe_closure, Set.mem_image]

Premises used: ClosedSubmodule.toSubmodule_sup, Set.mem_image, ContinuousLinearEquiv.coe_toLinearEquiv, ClosedSubmodule.mapEquiv_apply, Submodule.coe_closure, Submodule.map_coe, Submodule.carrier_eq_coe, ClosedSubmodule.coe_toSubmodule, LinearEquiv.coe_coe
-- 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
inst_9 : ContinuousAdd M
inst_10 : ContinuousConstSMul R M
f : M ≃L[R] N
s t : ClosedSubmodule R M
x : N
⊢ (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) = (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N)

Tactic:
LinearMap.ext (congrFun rfl)

Premises used: LinearMap.ext, congrFun, rfl
-- 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
inst_9 : ContinuousAdd M
inst_10 : ContinuousConstSMul R M
f : M ≃L[R] N
s t : ClosedSubmodule R M
x : N
⊢ (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) = (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N)

Tactic:
exact LinearMap.ext (congrFun rfl)

Premises used: LinearMap.ext, congrFun, rfl
-- 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
inst_9 : ContinuousAdd M
inst_10 : ContinuousConstSMul R M
f : M ≃L[R] N
s t : ClosedSubmodule R M
x : N
⊢ (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) = (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N)

Tactic:
have : f = f.toLinearEquiv.toLinearMap := by
    exact LinearMap.ext (congrFun rfl)
-- 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
inst_9 : ContinuousAdd M
inst_10 : ContinuousConstSMul R M
f : M ≃L[R] N
s t : ClosedSubmodule R M
x : N
this : (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) = (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N)
carrier :
  (∃ x_1 ∈ (↑((↑s : Submodule R M) ⊔ (↑t : Submodule R M)).closure : Set M), (f : (a : M) → N) x_1 = x) ↔
    Membership.mem (γ := Set N)
      (closure
        ((⇑(↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) : (a : M) → N) '' (↑((↑s : Submodule R M) ⊔ (↑t : Submodule R M)) : Set M)))
      x
⊢ (∃ x_1 ∈ closure (↑((↑s : Submodule R M) ⊔ (↑t : Submodule R M)) : Set M), (f : (a : M) → N) x_1 = x) ↔
    x ∈
      closure
        (↑(Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑s : Submodule R M) ⊔
              Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑t : Submodule R M)) :
          Set N)

Tactic:
rw [← this, ← Submodule.coe_closure, ← Submodule.map_sup, Submodule.map_coe]

Premises used: Submodule.map_sup, Submodule.coe_closure, Submodule.map_coe
-- 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
inst_9 : ContinuousAdd M
inst_10 : ContinuousConstSMul R M
f : M ≃L[R] N
s t : ClosedSubmodule R M
x : N
this : (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) = (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N)
⊢ (∃ x_1 ∈ (↑((↑s : Submodule R M) ⊔ (↑t : Submodule R M)).closure : Set M), (f : (a : M) → N) x_1 = x) ↔
    Membership.mem (γ := Set N)
      (closure
        ((⇑(↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) : (a : M) → N) '' (↑((↑s : Submodule R M) ⊔ (↑t : Submodule R M)) : Set M)))
      x

Tactic:
simp [← ContinuousLinearEquiv.image_closure]

Premises used: ContinuousLinearEquiv.image_closure
-- 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
𝕜 : Type u_6
H : Type u_7
inst_10 : Semiring 𝕜
inst_11 : AddCommMonoid H
inst_12 : UniformSpace H
inst_13 : Module 𝕜 H
inst_14 : CompleteSpace H
K : ClosedSubmodule 𝕜 H
a : IsComplete (↑K : Set H)
⊢ CompleteSpace.{u_7} ↥K

Tactic:
apply IsComplete.completeSpace_coe

Premises used: IsComplete.completeSpace_coe
-- 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
𝕜 : Type u_6
H : Type u_7
inst_10 : Semiring 𝕜
inst_11 : AddCommMonoid H
inst_12 : UniformSpace H
inst_13 : Module 𝕜 H
inst_14 : CompleteSpace H
K : ClosedSubmodule 𝕜 H
⊢ IsComplete (↑K : Submodule 𝕜 H).carrier

Tactic:
K.isClosed'.isComplete

Premises used: IsClosed.isComplete, ClosedSubmodule.isClosed'
-- 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
𝕜 : Type u_6
H : Type u_7
inst_10 : Semiring 𝕜
inst_11 : AddCommMonoid H
inst_12 : UniformSpace H
inst_13 : Module 𝕜 H
inst_14 : CompleteSpace H
K : ClosedSubmodule 𝕜 H
⊢ IsComplete (↑K : Submodule 𝕜 H).carrier

Tactic:
exact K.isClosed'.isComplete

Premises used: IsClosed.isComplete, ClosedSubmodule.isClosed'
-- Module: Mathlib.Topology.Algebra.Module.Compact
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
hN : N.FG
obtain : ∀ (s : Finset M) (hs : span R (↑s : Set M) = N), IsCompact (↑N : Set M)
⊢ IsCompact (↑N : Set M)

Tactic:
obtain ⟨s, hs⟩ := hN
-- Module: Mathlib.Topology.Algebra.Module.Compact
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R (↑s : Set M) = N
⊢ LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N

Tactic:
simp [hs]
-- Module: Mathlib.Topology.Algebra.Module.Compact
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R (↑s : Set M) = N
⊢ LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N

Tactic:
have : LinearMap.range (Fintype.linearCombination R (α := s) Subtype.val) = N := by
    simp [hs]
-- Module: Mathlib.Topology.Algebra.Module.Compact
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R (↑s : Set M) = N
this : LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N
rw :
  IsCompact
    (↑(LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) : Set M)
⊢ IsCompact (↑N : Set M)

Tactic:
rw [← this]
-- Module: Mathlib.Topology.Algebra.Module.Compact
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R (↑s : Set M) = N
this : LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N
⊢ IsCompact
    (↑(LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) : Set M)

Tactic:
isCompact_range ?_

Premises used: setOf, isCompact_range, Set.range
-- Module: Mathlib.Topology.Algebra.Module.Compact
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R (↑s : Set M) = N
this : LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N
refine :
  Continuous (X := ↥s → R) (Y := M)
    (⇑(Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s → R) → M)
⊢ IsCompact
    (↑(LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) : Set M)

Tactic:
refine isCompact_range ?_

Premises used: isCompact_range
-- Module: Mathlib.Topology.Algebra.Module.Compact
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R (↑s : Set M) = N
this : LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N
simp : Continuous (Y := M) fun (f : ↥s → R) ↦ ∑ i ∈ s.attach, f i • (↑i : M)
⊢ Continuous (X := ↥s → R) (Y := M)
    (⇑(Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s → R) → M)

Tactic:
simp only [Fintype.linearCombination, Finset.univ_eq_attach, LinearMap.coe_mk,
    AddHom.coe_mk]

Premises used: LinearMap.coe_mk, Finset.univ_eq_attach, Fintype.linearCombination, AddHom.coe_mk
-- Module: Mathlib.Topology.Algebra.Module.Compact
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R (↑s : Set M) = N
this : LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N
⊢ Continuous (Y := M) fun (f : ↥s → R) ↦ ∑ i ∈ s.attach, f i • (↑i : M)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Module.Compact
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
inst_3 : CompactSpace R
I : Ideal R
hI : I.FG
⊢ IsCompact (↑I : Set R)

Tactic:
Submodule.isCompact_of_fg hI

Premises used: Submodule.isCompact_of_fg
-- Module: Mathlib.Topology.Algebra.Module.Compact
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
inst_8 : Module.Finite R M
⊢ CompactSpace M

Tactic:
⟨Submodule.isCompact_of_fg (Module.Finite.fg_top (R := R))⟩

Premises used: Module.Finite.fg_top, CompactSpace.mk, Submodule.isCompact_of_fg
-- Module: Mathlib.Topology.Algebra.Module.Compact
Goal:
R_1 : Type u_1
M : Type u_2
inst : CommSemiring R_1
inst_1 : TopologicalSpace R_1
inst_2 : AddCommMonoid M
inst_3 : Module R_1 M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R_1 M
R : Type u_3
inst_7 : CommRing R
inst_8 : TopologicalSpace R
inst_9 : IsTopologicalRing R
inst_10 : IsNoetherianRing R
inst_11 : CompactSpace R
inst_12 : T2Space R
I : Ideal R
⊢ IsClosed (↑I : Set R)

Tactic:
(Ideal.isCompact_of_fg (IsNoetherian.noetherian I)).isClosed

Premises used: IsNoetherian.noetherian, Ideal.isCompact_of_fg, IsCompact.isClosed
-- Module: Mathlib.Topology.Algebra.Module.Complement
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
p q : Submodule R M
h : IsCompl p q
⊢ IsTopCompl p q ↔ Continuous[inst_1, inst_1] (⇑(p.projection q h) : (a : M) → M)

Tactic:
⟨IsTopCompl.continuous_projection, fun h' ↦ ⟨h, h'⟩⟩

Premises used: Submodule.IsTopCompl.continuous_projection, Submodule.IsTopCompl.mk, Iff.intro