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
inst_7 : ContinuousAdd N
inst_8 : ContinuousConstSMul R N
f : M →L[R] N
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ ↦ map_le_iff_le_comap

Premises used: ClosedSubmodule.map_le_iff_le_comap, GaloisConnection
-- 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 t : ClosedSubmodule R N
⊢ (↑(s ⊔ t) : Submodule R N) = (↑((↑s : Submodule R N) ⊔ (↑t : Submodule R N)).closure : Submodule R N)

Tactic:
rfl

Premises used: rfl
-- 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 t : ClosedSubmodule R N
⊢ (↑(↑((↑s : Submodule R N) ⊔ (↑t : Submodule R N)).closure : Submodule R N) : Set N) =
    closure ((↑s : Submodule R N) ⊔ (↑t : Submodule R N)).carrier

Tactic:
simp only [coe_toSubmodule, Submodule.coe_closure, Submodule.carrier_eq_coe]

Premises used: Submodule.coe_closure, Submodule.carrier_eq_coe, ClosedSubmodule.coe_toSubmodule
-- 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 t : ClosedSubmodule R N
x : N
⊢ x ∈ s ⊔ t ↔ x ∈ closure ((↑s : Submodule R N) ⊔ (↑t : Submodule R N)).carrier

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, closure, Set.sInter
-- 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 : Set (ClosedSubmodule R N)
⊢ (↑(sSup S) : Submodule R N) = (↑(Submodule.closure (⨆ s ∈ S, (↑s : Submodule R N))) : Submodule R N)

Tactic:
rfl

Premises used: Submodule.topologicalClosure, rfl
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
ι : Sort u_1
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
f : ι → ClosedSubmodule R N
rw :
  Eq.{u_4 + 1} (α := Submodule R N) (↑(sSup (Set.range fun (i : ι) ↦ f i)) : Submodule R N)
    (↑(Submodule.closure (⨆ (i : ι), (↑(f i) : Submodule R N))) : Submodule R N)
rw₁ :
  Eq.{u_4 + 1} (α := Submodule R N)
    (↑(Submodule.closure
          (⨆ (s : ClosedSubmodule R N),
            ⨆ (_ : Membership.mem (γ := Set (ClosedSubmodule R N)) (Set.range fun (i : ι) ↦ f i) s),
              (↑s : Submodule R N))) :
      Submodule R N)
    (↑(Submodule.closure (⨆ (i : ι), (↑(f i) : Submodule R N))) : Submodule R N)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := Submodule R N) (↑(Submodule.closure (⨆ (i : ι), (↑(f i) : Submodule R N))) : Submodule R N)
    (↑(Submodule.closure (⨆ (i : ι), (↑(f i) : Submodule R N))) : Submodule R N)
⊢ Eq.{u_4 + 1} (α := Submodule R N) (↑(⨆ (i : ι), f i) : Submodule R N)
    (↑(Submodule.closure (⨆ (i : ι), (↑(f i) : Submodule R N))) : Submodule R N)

Tactic:
rw [iSup, toSubmodule_sSup, iSup_range]

Premises used: iSup, iSup_range, ClosedSubmodule.toSubmodule_sSup
-- 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 : Set (ClosedSubmodule R N)
⊢ (↑(↑(Submodule.closure (⨆ s ∈ S, (↑s : Submodule R N))) : Submodule R N) : Set N) =
    closure
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u_2, u_4} (R := R) (⨆ s ∈ S, (↑s : Submodule R N)))))

Tactic:
simp only [coe_toSubmodule, Submodule.coe_closure, Submodule.carrier_eq_coe]

Premises used: Submodule.coe_closure, Submodule.carrier_eq_coe, ClosedSubmodule.coe_toSubmodule
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
ι : Sort u_1
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
f : ι → ClosedSubmodule R N
simp :
  (↑(↑(Submodule.closure (⨆ (i : ι), (↑(f i) : Submodule R N))) : Submodule R N) : Set N) =
    closure (↑(⨆ (i : ι), (↑(f i) : Submodule R N)) : Set N)
⊢ (↑(⨆ (i : ι), f i) : Set N) =
    closure
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_2, u_4} (R := R) (⨆ (i : ι), (↑(f i) : Submodule R N)))))

Tactic:
simp only [← coe_toSubmodule, toSubmodule_iSup, Submodule.carrier_eq_coe]

Premises used: ClosedSubmodule.toSubmodule_iSup, Submodule.carrier_eq_coe, ClosedSubmodule.coe_toSubmodule
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
ι : Sort u_1
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
f : ι → ClosedSubmodule R N
⊢ (↑(↑(Submodule.closure (⨆ (i : ι), (↑(f i) : Submodule R N))) : Submodule R N) : Set N) =
    closure (↑(⨆ (i : ι), (↑(f i) : Submodule R N)) : Set N)

Tactic:
rfl
-- 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
x : N
S : Set (ClosedSubmodule R N)
⊢ x ∈ sSup S ↔
    Membership.mem (γ := Set N)
      (closure
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_2, u_4} (R := R) (⨆ s ∈ S, (↑s : Submodule R N))))))
      x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule
Goal:
ι : Sort u_1
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
x : N
f : ι → ClosedSubmodule R N
⊢ Membership.mem (γ := ClosedSubmodule R N) (⨆ (i : ι), f i) x ↔
    Membership.mem (γ := Set N)
      (closure
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_2, u_4} (R := R) (⨆ (i : ι), (↑(f i) : Submodule R N))))))
      x

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
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
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
f : M →L[R] N
s t : ClosedSubmodule R N
x : N
x_1 : Set (ClosedSubmodule R N)
⊢ IsLUB x_1 (sSup x_1)

Tactic:
⟨fun a ha x hx ↦ ?_, fun a h x ↦ ?_⟩

Premises used: IsLeast, And.intro, IsLUB
-- 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
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
f : M →L[R] N
s t : ClosedSubmodule R N
x : N
x_1 : Set (ClosedSubmodule R N)
refine_1 : ∀ (a : ClosedSubmodule R N) (ha : a ∈ x_1) (x : N) (hx : x ∈ a), x ∈ sSup x_1
refine_2 : ∀ (a : ClosedSubmodule R N) (h : a ∈ upperBounds x_1), ∀ x ∈ sSup x_1, x ∈ a
⊢ IsLUB x_1 (sSup x_1)

Tactic:
refine ⟨fun a ha x hx ↦ ?_, fun a h x ↦ ?_⟩
-- 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
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
f : M →L[R] N
s t : ClosedSubmodule R N
x_1 : N
x_2 : Set (ClosedSubmodule R N)
a : ClosedSubmodule R N
ha : a ∈ x_2
x : N
hx : x ∈ a
⊢ x ∈ sSup x_2

Tactic:
subset_closure <| Submodule.mem_iSup_of_mem _ <| Submodule.mem_iSup_of_mem ha hx

Premises used: Set.Mem, subset_closure, setOf, closure, Submodule.mem_iSup_of_mem, Set.sInter
-- 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
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
f : M →L[R] N
s t : ClosedSubmodule R N
x_1 : N
x_2 : Set (ClosedSubmodule R N)
a : ClosedSubmodule R N
ha : a ∈ x_2
x : N
hx : x ∈ a
⊢ x ∈ sSup x_2

Tactic:
exact subset_closure <| Submodule.mem_iSup_of_mem _ <| Submodule.mem_iSup_of_mem ha hx

Premises used: subset_closure, Submodule.mem_iSup_of_mem
-- 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
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
f : M →L[R] N
s t : ClosedSubmodule R N
x_1 : N
x_2 : Set (ClosedSubmodule R N)
a : ClosedSubmodule R N
h : a ∈ upperBounds x_2
x : N
refine_2 : x ∈ sSup x_2 → Membership.mem (γ := ClosedSubmodule R N) (↑a : Submodule R N).closure x
⊢ x ∈ sSup x_2 → x ∈ a

Tactic:
rw [← ClosedSubmodule.closure_toSubmodule_eq (s := a)]

Premises used: ClosedSubmodule.closure_toSubmodule_eq
-- 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
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
f : M →L[R] N
s t : ClosedSubmodule R N
x_1 : N
x_2 : Set (ClosedSubmodule R N)
a : ClosedSubmodule R N
h : a ∈ upperBounds x_2
x : N
refine_2 :
  (↑(Submodule.toAddSubmonoid.{u_2, u_4} (R := R) (⨆ s ∈ x_2, (↑s : Submodule R N))) : Set N) ⊆
    (↑(↑a : Submodule R N).toAddSubmonoid : Set N)
⊢ x ∈ sSup x_2 → Membership.mem (γ := ClosedSubmodule R N) (↑a : Submodule R N).closure x

Tactic:
apply closure_mono

Premises used: closure_mono
-- 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
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
f : M →L[R] N
s t : ClosedSubmodule R N
x_1 : N
x_2 : Set (ClosedSubmodule R N)
a : ClosedSubmodule R N
h : a ∈ upperBounds x_2
x y : N
hy : y ∈ (↑(⨆ s ∈ x_2, (↑s : Submodule R N)) : Set N)
⊢ ∀ (N_1 : Submodule R N), (∀ (i : ClosedSubmodule R N), ⨆ (_ : i ∈ x_2), (↑i : Submodule R N) ≤ N_1) → y ∈ N_1

Tactic:
simp only [SetLike.mem_coe, Submodule.mem_iSup] at hy

Premises used: SetLike.mem_coe, Submodule.mem_iSup
-- 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
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
f : M →L[R] N
s t : ClosedSubmodule R N
x_1 : N
x_2 : Set (ClosedSubmodule R N)
a : ClosedSubmodule R N
h : a ∈ upperBounds x_2
x y : N
hy : ∀ (N_1 : Submodule R N), (∀ (i : ClosedSubmodule R N), ⨆ (_ : i ∈ x_2), (↑i : Submodule R N) ≤ N_1) → y ∈ N_1
⊢ y ∈ (↑a : Set N)

Tactic:
hy a fun b _ hz ↦ Submodule.mem_iSup _ |>.mp hz _ <| fun hb ↦ h hb

Premises used: Set.Mem, ClosedSubmodule.toSubmodule, Iff.mp, Submodule.mem_iSup
-- 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
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
f : M →L[R] N
s t : ClosedSubmodule R N
x_1 : N
x_2 : Set (ClosedSubmodule R N)
a : ClosedSubmodule R N
h : a ∈ upperBounds x_2
x y : N
hy : ∀ (N_1 : Submodule R N), (∀ (i : ClosedSubmodule R N), ⨆ (_ : i ∈ x_2), (↑i : Submodule R N) ≤ N_1) → y ∈ N_1
⊢ y ∈ (↑a : Set N)

Tactic:
exact hy a fun b _ hz ↦ Submodule.mem_iSup _ |>.mp hz _ <| fun hb ↦ h hb

Premises used: ClosedSubmodule.toSubmodule, Iff.mp, Submodule.mem_iSup
-- 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
f : M ≃L[R] N
s : ClosedSubmodule R M
⊢ IsClosed (Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑s : Submodule R M)).carrier

Tactic:
simpa using s.isClosed

Premises used: 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
f : M ≃L[R] N
t : ClosedSubmodule R N
⊢ IsClosed (Submodule.map (↑(↑f.symm : N ≃ₗ[R] M) : N →ₗ[R] M) (↑t : Submodule R N)).carrier

Tactic:
simpa using t.isClosed

Premises used: 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
f : M ≃L[R] N
x : ClosedSubmodule R M
carrier :
  ∀ (x_1 : M),
    Membership.mem (γ := Set M)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_2, u_3} (R := R)
              (↑((fun (t : ClosedSubmodule R N) ↦
                      { toSubmodule := Submodule.map (↑(↑f.symm : N ≃ₗ[R] M) : N →ₗ[R] M) (↑t : Submodule R N),
                        isClosed' := ⋯ : ClosedSubmodule R M })
                    ((fun (s : ClosedSubmodule R M) ↦
                        { toSubmodule := Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑s : Submodule R M),
                          isClosed' := ⋯ : ClosedSubmodule R N })
                      x)) :
                Submodule R M))))
        x_1 ↔
      x_1 ∈ (↑x : Submodule R M).carrier
⊢ (fun (t : ClosedSubmodule R N) ↦
        { toSubmodule := Submodule.map (↑(↑f.symm : N ≃ₗ[R] M) : N →ₗ[R] M) (↑t : Submodule R N), isClosed' := ⋯ :
          ClosedSubmodule R M })
      ((fun (s : ClosedSubmodule R M) ↦
          { toSubmodule := Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑s : Submodule R M), isClosed' := ⋯ :
            ClosedSubmodule R N })
        x) =
    x

Tactic:
ext _
-- 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
f : M ≃L[R] N
x : ClosedSubmodule R M
x_1 : M
⊢ Membership.mem (γ := Set M)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_2, u_3} (R := R)
            (↑((fun (t : ClosedSubmodule R N) ↦
                    { toSubmodule := Submodule.map (↑(↑f.symm : N ≃ₗ[R] M) : N →ₗ[R] M) (↑t : Submodule R N),
                      isClosed' := ⋯ : ClosedSubmodule R M })
                  ((fun (s : ClosedSubmodule R M) ↦
                      { toSubmodule := Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑s : Submodule R M),
                        isClosed' := ⋯ : ClosedSubmodule R N })
                    x)) :
              Submodule R M))))
      x_1 ↔
    x_1 ∈ (↑x : Submodule R M).carrier

Tactic:
simp
-- 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
f : M ≃L[R] N
x : ClosedSubmodule R N
carrier :
  ∀ (x_1 : N),
    Membership.mem (γ := Set N)
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
              (↑((fun (s : ClosedSubmodule R M) ↦
                      { toSubmodule := Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑s : Submodule R M),
                        isClosed' := ⋯ : ClosedSubmodule R N })
                    ((fun (t : ClosedSubmodule R N) ↦
                        { toSubmodule := Submodule.map (↑(↑f.symm : N ≃ₗ[R] M) : N →ₗ[R] M) (↑t : Submodule R N),
                          isClosed' := ⋯ : ClosedSubmodule R M })
                      x)) :
                Submodule R N))))
        x_1 ↔
      x_1 ∈ (↑x : Submodule R N).carrier
⊢ (fun (s : ClosedSubmodule R M) ↦
        { toSubmodule := Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑s : Submodule R M), isClosed' := ⋯ :
          ClosedSubmodule R N })
      ((fun (t : ClosedSubmodule R N) ↦
          { toSubmodule := Submodule.map (↑(↑f.symm : N ≃ₗ[R] M) : N →ₗ[R] M) (↑t : Submodule R N), isClosed' := ⋯ :
            ClosedSubmodule R M })
        x) =
    x

Tactic:
ext _
-- 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
f : M ≃L[R] N
x : ClosedSubmodule R N
x_1 : N
⊢ Membership.mem (γ := Set N)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_2, u_4} (R := R)
            (↑((fun (s : ClosedSubmodule R M) ↦
                    { toSubmodule := Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑s : Submodule R M),
                      isClosed' := ⋯ : ClosedSubmodule R N })
                  ((fun (t : ClosedSubmodule R N) ↦
                      { toSubmodule := Submodule.map (↑(↑f.symm : N ≃ₗ[R] M) : N →ₗ[R] M) (↑t : Submodule R N),
                        isClosed' := ⋯ : ClosedSubmodule R M })
                    x)) :
              Submodule R N))))
      x_1 ↔
    x_1 ∈ (↑x : Submodule R N).carrier

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 : ClosedSubmodule R M
⊢ (↑((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) s) : Submodule R N) =
    Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑s : Submodule R M)

Tactic:
rfl

Premises used: Submodule.map, 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
f : M ≃L[R] N
⊢ mapEquiv f.symm = (mapEquiv f).symm

Tactic:
rfl

Premises used: ClosedSubmodule.mapEquiv, Equiv.symm, 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
f : M ≃L[R] N
s : ClosedSubmodule R M
x : N
⊢ Membership.mem (γ := ClosedSubmodule R N)
      ((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) s : ClosedSubmodule R N) x ↔
    Membership.mem (α := M) s ((f.symm : (a : N) → M) x : M)

Tactic:
Submodule.mem_map_equiv (e := f.toLinearEquiv) s.toSubmodule

Premises used: Set.Mem, ClosedSubmodule.toSubmodule, Submodule.mem_map_equiv
-- 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 M
x : M
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := ClosedSubmodule R N)
      ((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) s : ClosedSubmodule R N)
      ((f : (a : M) → N) x : N) ↔
    x ∈ s

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
inst_7 : T1Space M
inst_8 : T1Space 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
inst_7 : T1Space M
inst_8 : T1Space 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