awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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
e_f : x ∈ f.domain → x ∈ f.closure.domain
⊢ x ∈ (f.closure.domRestrict f.domain).domain ↔ x ∈ f.domain

Tactic:
simp only [domRestrict_domain, Submodule.mem_inf, and_iff_left_iff_imp]

Premises used: Submodule.mem_inf, LinearPMap.domRestrict_domain, and_iff_left_iff_imp
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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
hx : x ∈ f.domain
⊢ x ∈ f.closure.domain

Tactic:
f.le_closure.1 hx

Premises used: And.left, LinearPMap.le_closure
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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
hx : x ∈ f.domain
⊢ x ∈ f.closure.domain

Tactic:
exact f.le_closure.1 hx

Premises used: And.left, LinearPMap.le_closure
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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 ⋯
⊢ x = (↑z : E)

Tactic:
have hyz : x = z := rfl
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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)
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
⊢ (↑(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:
rw [f.le_closure.2 hyz]

Premises used: And.right, LinearPMap.le_closure
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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.closure : ↥f.closure.domain → F) z

Tactic:
domRestrict_apply hyz

Premises used: LinearPMap.domRestrict_apply
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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.closure : ↥f.closure.domain → F) z

Tactic:
exact domRestrict_apply hyz

Premises used: LinearPMap.domRestrict_apply
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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 = ⊥
rw :
  IsClosed[instTopologicalSpaceProd]
      (↑(Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) : Set (F × E)) ↔
    f.IsClosed
⊢ f.inverse.IsClosed ↔ f.IsClosed

Tactic:
rw [IsClosed, inverse_graph hf]

Premises used: LinearPMap.inverse_graph, LinearPMap.IsClosed
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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 = ⊥
⊢ IsClosed[instTopologicalSpaceProd]
      (↑(Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) : Set (F × E)) ↔
    f.IsClosed

Tactic:
(ContinuousLinearEquiv.prodComm R E F).isClosed_image

Premises used: LinearPMap.IsClosed, setOf, ContinuousLinearEquiv.prodComm, ContinuousLinearEquiv.isClosed_image, Set.image
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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 = ⊥
⊢ IsClosed[instTopologicalSpaceProd]
      (↑(Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) : Set (F × E)) ↔
    f.IsClosed

Tactic:
exact (ContinuousLinearEquiv.prodComm R E F).isClosed_image

Premises used: ContinuousLinearEquiv.prodComm, ContinuousLinearEquiv.isClosed_image
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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 = ⊥
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
⊢ f.closure.inverse.graph = f.inverse.graph.topologicalClosure

Tactic:
rw [inverse_graph hf, inverse_graph hcf, ← hf'.graph_closure_eq_closure_graph]

Premises used: LinearPMap.inverse_graph, LinearPMap.IsClosable.graph_closure_eq_closure_graph
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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 = ⊥
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))
⊢ 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:
apply SetLike.ext'

Premises used: SetLike.ext'
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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 = ⊥
h :
  closure[instTopologicalSpaceProd] (Prod.swap '' (↑f.graph : Set (E × F))) ⊆
    Prod.swap '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
⊢ 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))))

Tactic:
apply (image_closure_subset_closure_image continuous_swap).antisymm

Premises used: continuous_swap, HasSubset.Subset.antisymm, image_closure_subset_closure_image
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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))
    ((⇑(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
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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)))
⊢ 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)
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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)))
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)))
⊢ Eq (α := Set (F × E)) ((fun (a : E × F) ↦ a.swap) '' (↑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:
simp only [LinearEquiv.coe_toEquiv, LinearEquiv.prodComm_apply] at h1 h2

Premises used: LinearEquiv.coe_toEquiv, LinearEquiv.prodComm_apply
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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)))
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)))
h1₁ :
  Eq (α := Set (F × E)) ((fun (a : E × F) ↦ a.swap) '' (↑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)))
⊢ Eq (α := Set (F × E)) ((fun (a : E × F) ↦ a.swap) '' 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:
simp only [LinearEquiv.coe_toEquiv, LinearEquiv.prodComm_apply] at h1 h2

Premises used: LinearEquiv.coe_toEquiv, LinearEquiv.prodComm_apply
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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)) ((fun (a : E × F) ↦ a.swap) '' (↑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)))
h2 :
  Eq (α := Set (F × E)) ((fun (a : E × F) ↦ a.swap) '' 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)))
h :
  Subset (α := Set (F × E))
    (closure[instTopologicalSpaceProd]
      ((⇑(LinearEquiv.toEquiv (modM := Prod.instModule) (LinearEquiv.prodComm R E F)).symm : (a : F × E) → E × F) ⁻¹'
        (↑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)))
⊢ closure[instTopologicalSpaceProd] (Prod.swap '' (↑f.graph : Set (E × F))) ⊆
    Prod.swap '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))

Tactic:
rw [h1, h2]
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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)) ((fun (a : E × F) ↦ a.swap) '' (↑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)))
h2 :
  Eq (α := Set (F × E)) ((fun (a : E × F) ↦ a.swap) '' 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)))
⊢ Subset (α := Set (F × E))
    (closure[instTopologicalSpaceProd]
      ((⇑(LinearEquiv.toEquiv (modM := Prod.instModule) (LinearEquiv.prodComm R E F)).symm : (a : F × E) → E × F) ⁻¹'
        (↑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:
apply continuous_swap.closure_preimage_subset

Premises used: continuous_swap, Continuous.closure_preimage_subset
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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
mp : f.inverse.IsClosable → f.closure.toFun.ker = ⊥
mpr : f.closure.toFun.ker = ⊥ → f.inverse.IsClosable
⊢ f.inverse.IsClosable ↔ f.closure.toFun.ker = ⊥

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
mp :
  ∀ (m : ↥f.closure.domain),
    Eq.{u_3 + 1} (α := F) ((f.closure.toFun : (a : ↥f.closure.domain) → F) m : F) (0 : F) → m = 0
⊢ f.closure.toFun.ker = ⊥

Tactic:
rw [LinearMap.ker_eq_bot']

Premises used: LinearMap.ker_eq_bot'
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' :
  Eq.{u_3 + 1} (α := F)
    ((f.closure.toFun : (a : ↥f.closure.domain) → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.closure.domain) x hx) : F)
    (0 : F)
mp : x = 0
⊢ Subtype.mk (p := fun (x : E) ↦ x ∈ f.closure.domain) x hx = 0

Tactic:
simp only [Submodule.mk_eq_zero]

Premises used: Submodule.mk_eq_zero
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' :
  Eq.{u_3 + 1} (α := F)
    ((f.closure.toFun : (a : ↥f.closure.domain) → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.closure.domain) x hx) : F)
    (0 : F)
⊢ (x, 0) ∈ f.closure.graph

Tactic:
rw [toFun_eq_coe, eq_comm, image_iff] at hx'

Premises used: eq_comm, LinearPMap.toFun_eq_coe, LinearPMap.image_iff
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' : (x, 0) ∈ f.closure.graph
rw : (0, x) ∈ (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).topologicalClosure
⊢ (0, x) ∈ f'.graph

Tactic:
rw [← h, inverse_graph hf]

Premises used: LinearPMap.inverse_graph
-- Module: Mathlib.Topology.Algebra.Module.LinearPMap
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
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' : (x, 0) ∈ f.closure.graph
⊢ (x, 0) ∈ closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))

Tactic:
rw [← hf'.graph_closure_eq_closure_graph, ← SetLike.mem_coe,
        Submodule.topologicalClosure_coe] at hx'

Premises used: Submodule.topologicalClosure_coe, SetLike.mem_coe, LinearPMap.IsClosable.graph_closure_eq_closure_graph