awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ s.closure = { toSubmodule := s, isClosed' := hs : ClosedSubmodule R M }
have carrier : ∀ (x : M),
  x ∈ (↑s.closure : Submodule R M).carrier ↔
    x ∈ (↑{ toSubmodule := s, isClosed' := hs : ClosedSubmodule R M } : Submodule R M).carrier
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ (↑s : Submodule R N).closure = s
have carrier : ∀ (x : N), x ∈ (↑(↑s : Submodule R N).closure : Submodule R N).carrier ↔ x ∈ (↑s : Submodule R N).carrier
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ map f s ≤ t ↔ s ≤ comap f t
have simp : (↑s : Submodule R M) ≤ Submodule.comap (↑f : M →ₗ[R] N) (↑t : Submodule R N) ↔ s ≤ comap f t
Tactic: simp [map, Submodule.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ Eq.{u_4 + 1} (α := Submodule R N) (↑(⨆ (i : ι), f i) : Submodule R N)
    (↑(Submodule.closure (⨆ (i : ι), (↑(f i) : Submodule R N))) : Submodule R N)
have 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)
Tactic: rw [iSup, toSubmodule_sSup, iSup_range]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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)
⊢ Eq.{u_4 + 1} (α := Submodule R N) (↑(⨆ (i : ι), f i) : Submodule R N)
    (↑(Submodule.closure (⨆ (i : ι), (↑(f i) : Submodule R N))) : Submodule R N)
have 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)
Tactic: rw [iSup, toSubmodule_sSup, iSup_range]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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)
⊢ Eq.{u_4 + 1} (α := Submodule R N) (↑(⨆ (i : ι), f i) : Submodule R N)
    (↑(Submodule.closure (⨆ (i : ι), (↑(f i) : Submodule R N))) : Submodule R N)
have 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)
Tactic: rw [iSup, toSubmodule_sSup, iSup_range]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ (↑(⨆ (i : ι), f i) : Set N) =
    closure
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_2, u_4} (R := R) (⨆ (i : ι), (↑(f i) : Submodule R N)))))
have simp : (↑(↑(Submodule.closure (⨆ (i : ι), (↑(f i) : Submodule R N))) : Submodule R N) : Set N) =
  closure (↑(⨆ (i : ι), (↑(f i) : Submodule R N)) : Set N)
Tactic: simp only [← coe_toSubmodule, toSubmodule_iSup, Submodule.carrier_eq_coe]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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)
have refine_1 : ∀ (a : ClosedSubmodule R N) (ha : a ∈ x_1) (x : N) (hx : x ∈ a), x ∈ sSup x_1
Tactic: refine ⟨fun a ha x hx ↦ ?_, fun a h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ IsLUB x_1 (sSup x_1)
have refine_2 : ∀ (a : ClosedSubmodule R N) (h : a ∈ upperBounds x_1), ∀ x ∈ sSup x_1, x ∈ a
Tactic: refine ⟨fun a ha x hx ↦ ?_, fun a h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ x ∈ sSup x_2 → x ∈ a
have refine_2 : x ∈ sSup x_2 → Membership.mem (γ := ClosedSubmodule R N) (↑a : Submodule R N).closure x
Tactic: rw [← ClosedSubmodule.closure_toSubmodule_eq (s := a)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ x ∈ sSup x_2 → Membership.mem (γ := ClosedSubmodule R N) (↑a : Submodule R N).closure x
have 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)
Tactic: apply closure_mono
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (hypothesis)
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)
⊢ y ∈ (↑a : Set N)
have hy₁ : ∀ (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
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ (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
have 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' := sorry : ClosedSubmodule R M })
                  ((fun (s : ClosedSubmodule R M) ↦
                      { toSubmodule := Submodule.map (↑(↑f : M ≃ₗ[R] N) : M →ₗ[R] N) (↑s : Submodule R M),
                        isClosed' := sorry : ClosedSubmodule R N })
                    x)) :
              Submodule R M))))
      x_1 ↔
    x_1 ∈ (↑x : Submodule R M).carrier
Tactic: ext _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ (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
have 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' := sorry : ClosedSubmodule R N })
                  ((fun (t : ClosedSubmodule R N) ↦
                      { toSubmodule := Submodule.map (↑(↑f.symm : N ≃ₗ[R] M) : N →ₗ[R] M) (↑t : Submodule R N),
                        isClosed' := sorry : ClosedSubmodule R M })
                    x)) :
              Submodule R N))))
      x_1 ↔
    x_1 ∈ (↑x : Submodule R N).carrier
Tactic: ext _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ Eq.{u_4 + 1} (α := ClosedSubmodule R N) ((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) ⊥) ⊥
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ Eq.{u_4 + 1} (α := ClosedSubmodule R N) ((mapEquiv f : (a : ClosedSubmodule R M) → ClosedSubmodule R N) ⊤) ⊤
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ 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)
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ 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)
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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) (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
have 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
Tactic: rw [← ContinuousLinearEquiv.image_closure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ 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)
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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
⊢ 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
have 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)
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (hypothesis)
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
⊢ (∃ 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)
have this : (↑(↑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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
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 ∈ 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)
have 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
Tactic: rw [← this, ← Submodule.coe_closure, ← Submodule.map_sup, Submodule.map_coe]