awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
F : Type u_3
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousSMul 𝕜 F
inst_14 : FiniteDimensional 𝕜 F
inst_15 : T2Space F
G : Type u_4
inst_16 : AddCommGroup G
inst_17 : Module 𝕜 G
inst_18 : TopologicalSpace G
inst_19 : IsTopologicalAddGroup G
inst_20 : ContinuousSMul 𝕜 G
f : E →ₗ[𝕜] F →ₗ[𝕜] G
map_add :
  ∀ (x y : E),
    ((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
        ((f : (a : E) → F →ₗ[𝕜] G) (x + y)) =
      HAdd.hAdd (α := F →L[𝕜] G) (β := F →L[𝕜] G)
        (((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
            ((f : (a : E) → F →ₗ[𝕜] G) x) :
          F →L[𝕜] G)
        (((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
            ((f : (a : E) → F →ₗ[𝕜] G) y) :
          F →L[𝕜] G)
⊢ IsLinearMap 𝕜 (M₂ := F →L[𝕜] G) fun (x : E) ↦
    ((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G) ((f : (a : E) → F →ₗ[𝕜] G) x)
have map_smul : ∀ (c : 𝕜) (x : E),
  ((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
      ((f : (a : E) → F →ₗ[𝕜] G) (c • x)) =
    HSMul.hSMul (β := F →L[𝕜] G) c
      (((toContinuousLinearMap : (F →ₗ[𝕜] G) ≃ₗ[𝕜] F →L[𝕜] G) : (a : F →ₗ[𝕜] G) → F →L[𝕜] G)
          ((f : (a : E) → F →ₗ[𝕜] G) x) :
        F →L[𝕜] G)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f g : E →ₗ.[R] F
hf : f.IsClosable
hfg : g ≤ f
⊢ g.IsClosable
have obtain : ∀ (f' : E →ₗ.[R] F) (hf : f.graph.topologicalClosure = f'.graph), g.IsClosable
Tactic: obtain ⟨f', hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
⊢ g.graph.topologicalClosure ≤ f'.graph
have rw : g.graph.topologicalClosure ≤ f.graph.topologicalClosure
Tactic: rw [← hf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (hypothesis)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
⊢ g.IsClosable
have this : g.graph.topologicalClosure ≤ f'.graph
Tactic: have : g.graph.topologicalClosure ≤ f'.graph := by
    rw [← hf]
    exact Submodule.topologicalClosure_mono (le_graph_of_le hfg)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
this : g.graph.topologicalClosure ≤ f'.graph
⊢ g.IsClosable
have h : g.graph.topologicalClosure = g.graph.topologicalClosure.toLinearPMap.graph
Tactic: use g.graph.topologicalClosure.toLinearPMap
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
this : g.graph.topologicalClosure ≤ f'.graph
⊢ g.graph.topologicalClosure = g.graph.topologicalClosure.toLinearPMap.graph
have h : ∀ (x : E × F) (_hx : x ∈ g.graph.topologicalClosure) (_hx' : x.1 = 0), x.2 = 0
Tactic: rw [Submodule.toLinearPMap_graph_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ ∃! f' : E →ₗ.[R] F, f.graph.topologicalClosure = f'.graph
have refine : ∀ (x x_1 : E →ₗ.[R] F) (hy₁ : f.graph.topologicalClosure = x.graph) (hy₂ : f.graph.topologicalClosure = x_1.graph),
  x.graph = x_1.graph
Tactic: refine existsUnique_of_exists_of_unique hf fun _ _ hy₁ hy₂ => eq_of_eq_graph ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
x x_1 : E →ₗ.[R] F
hy₁ : f.graph.topologicalClosure = x.graph
hy₂ : f.graph.topologicalClosure = x_1.graph
rw : f.graph.topologicalClosure = x_1.graph
⊢ x.graph = x_1.graph
have rw₁ : f.graph.topologicalClosure = f.graph.topologicalClosure
Tactic: rw [← hy₁, ← hy₂]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.graph.topologicalClosure = f.closure.graph
have rw : f.graph.topologicalClosure =
  (Exists.choose (p := fun (f' : E →ₗ.[R] F) ↦ f.graph.topologicalClosure = f'.graph) hf).graph
Tactic: rw [closure_def hf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ f ≤ f.closure
have pos : ∀ (hf : f.IsClosable), f ≤ f.closure
Tactic: by_cases hf : f.IsClosable
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
pos : ∀ (hf : f.IsClosable), f ≤ f.closure
⊢ f ≤ f.closure
have neg : ∀ (hf : ¬f.IsClosable), f ≤ f.closure
Tactic: by_cases hf : f.IsClosable
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f ≤ f.closure
have pos : f.graph ≤ f.closure.graph
Tactic: refine le_of_le_graph ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.graph ≤ f.closure.graph
have pos : f.graph ≤ f.graph.topologicalClosure
Tactic: rw [← hf.graph_closure_eq_closure_graph]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
hf : ¬f.IsClosable
⊢ f ≤ f.closure
have neg : f ≤ f
Tactic: rw [closure_def' hf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : g.IsClosable
h : f ≤ g
⊢ f.closure ≤ g.closure
have refine : f.closure.graph ≤ g.closure.graph
Tactic: refine le_of_le_graph ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : g.IsClosable
h : f ≤ g
⊢ f.closure.graph ≤ g.closure.graph
have rw : f.graph.topologicalClosure ≤ g.closure.graph
Tactic: rw [← (hg.leIsClosable h).graph_closure_eq_closure_graph]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : g.IsClosable
h : f ≤ g
⊢ f.graph.topologicalClosure ≤ g.closure.graph
have rw : f.graph.topologicalClosure ≤ g.graph.topologicalClosure
Tactic: rw [← hg.graph_closure_eq_closure_graph]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.closure.IsClosed
have rw : IsClosed[instTopologicalSpaceProd] (↑f.graph.topologicalClosure : Set (E × F))
Tactic: rw [IsClosed, ← hf.graph_closure_eq_closure_graph]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ f.closure.HasCore f.domain
have refine : (f.closure.domRestrict f.domain).closure = f.closure
Tactic: refine ⟨f.le_closure.1, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ (f.closure.domRestrict f.domain).closure = f.closure
have e_f : f.closure.domRestrict f.domain = f
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ f.closure.domRestrict f.domain = f
have e_f : ∀ (x : E), x ∈ (f.closure.domRestrict f.domain).domain ↔ x ∈ f.domain
Tactic: ext x h1 h2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
e_f : ∀ (x : E), x ∈ (f.closure.domRestrict f.domain).domain ↔ x ∈ f.domain
⊢ f.closure.domRestrict f.domain = f
have e_f₁ : ∀ ⦃x : E⦄ ⦃h1 : x ∈ (f.closure.domRestrict f.domain).domain⦄ ⦃h2 : x ∈ f.domain⦄,
  (↑(f.closure.domRestrict f.domain) : ↥(f.closure.domRestrict f.domain).domain → F)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.closure.domRestrict f.domain).domain) x h1) =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x h2)
Tactic: ext x h1 h2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
⊢ x ∈ (f.closure.domRestrict f.domain).domain ↔ x ∈ f.domain
have e_f : x ∈ f.domain → x ∈ f.closure.domain
Tactic: simp only [domRestrict_domain, Submodule.mem_inf, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (hypothesis)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
h1 : x ∈ (f.closure.domRestrict f.domain).domain
h2 : x ∈ f.domain
z : ↥f.closure.domain := Subtype.mk (p := fun (x : E) ↦ x ∈ f.closure.domain) x ⋯
⊢ (↑(f.closure.domRestrict f.domain) : ↥(f.closure.domRestrict f.domain).domain → F)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.closure.domRestrict f.domain).domain) x h1) =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x h2)
have hyz : x = (↑z : E)
Tactic: have hyz : x = z := rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
h1 : x ∈ (f.closure.domRestrict f.domain).domain
h2 : x ∈ f.domain
z : ↥f.closure.domain := Subtype.mk (p := fun (x : E) ↦ x ∈ f.closure.domain) x ⋯
hyz : x = (↑z : E)
⊢ (↑(f.closure.domRestrict f.domain) : ↥(f.closure.domRestrict f.domain).domain → F)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.closure.domRestrict f.domain).domain) x h1) =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x h2)
have e_f : (↑(f.closure.domRestrict f.domain) : ↥(f.closure.domRestrict f.domain).domain → F)
    (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.closure.domRestrict f.domain).domain) x h1) =
  (↑f.closure : ↥f.closure.domain → F) z
Tactic: rw [f.le_closure.2 hyz]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
⊢ f.inverse.IsClosed ↔ f.IsClosed
have rw : IsClosed[instTopologicalSpaceProd]
    (↑(Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) : Set (F × E)) ↔
  f.IsClosed
Tactic: rw [IsClosed, inverse_graph hf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
f : E →ₗ.[R] F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
⊢ f.closure.inverse.graph = f.inverse.graph.topologicalClosure
have rw : Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph.topologicalClosure =
  (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).topologicalClosure
Tactic: rw [inverse_graph hf, inverse_graph hcf, ← hf'.graph_closure_eq_closure_graph]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
f : E →ₗ.[R] F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
⊢ Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph.topologicalClosure =
    (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).topologicalClosure
have h : (↑(Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph.topologicalClosure) : Set (F × E)) =
  (↑(Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).topologicalClosure : Set (F × E))
Tactic: apply SetLike.ext'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
f : E →ₗ.[R] F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
⊢ Eq (α := Set (F × E)) ((fun (a : E × F) ↦ a.swap) '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F)))
    (closure[instTopologicalSpaceProd] ((fun (a : E × F) ↦ a.swap) '' (↑f.graph : Set (E × F))))
have h : closure[instTopologicalSpaceProd] (Prod.swap '' (↑f.graph : Set (E × F))) ⊆
  Prod.swap '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
Tactic: apply (image_closure_subset_closure_image continuous_swap).antisymm
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (hypothesis)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
f : E →ₗ.[R] F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
⊢ closure[instTopologicalSpaceProd] (Prod.swap '' (↑f.graph : Set (E × F))) ⊆
    Prod.swap '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
have h1 : Eq (α := Set (F × E))
  ((⇑(LinearEquiv.toEquiv (modM := Prod.instModule) (LinearEquiv.prodComm R E F)) : (a : E × F) → F × E) ''
    (↑f.graph : Set (E × F)))
  ((⇑(LinearEquiv.toEquiv (modM := Prod.instModule) (LinearEquiv.prodComm R E F)).symm : (a : F × E) → E × F) ⁻¹'
    (↑f.graph : Set (E × F)))
Tactic: have h1 := (LinearEquiv.prodComm R E F).toEquiv.image_eq_preimage_symm f.graph
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LinearPMap (hypothesis)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : CommRing R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
f : E →ₗ.[R] F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R E
inst_11 : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
h1 :
  Eq (α := Set (F × E))
    ((⇑(LinearEquiv.toEquiv (modM := Prod.instModule) (LinearEquiv.prodComm R E F)) : (a : E × F) → F × E) ''
      (↑f.graph : Set (E × F)))
    ((⇑(LinearEquiv.toEquiv (modM := Prod.instModule) (LinearEquiv.prodComm R E F)).symm : (a : F × E) → E × F) ⁻¹'
      (↑f.graph : Set (E × F)))
⊢ closure[instTopologicalSpaceProd] (Prod.swap '' (↑f.graph : Set (E × F))) ⊆
    Prod.swap '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
have h2 : Eq (α := Set (F × E))
  ((⇑(LinearEquiv.toEquiv (modM := Prod.instModule) (LinearEquiv.prodComm R E F)) : (a : E × F) → F × E) ''
    closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F)))
  ((⇑(LinearEquiv.toEquiv (modM := Prod.instModule) (LinearEquiv.prodComm R E F)).symm : (a : F × E) → E × F) ⁻¹'
    closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F)))
Tactic: have h2 := (LinearEquiv.prodComm R E F).toEquiv.image_eq_preimage_symm (_root_.closure f.graph)