-- Mathlib/Topology/Algebra/Module/LinearPMap.lean
theorem closure_inverse_graph (hf : LinearMap.ker f.toFun = ⊥) (hf' : f.IsClosable)
    (hcf : LinearMap.ker f.closure.toFun = ⊥) :
    f.closure.inverse.graph = f.inverse.graph.topologicalClosure

Proof state:
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : f.IsClosable
hcf : LinearMap.ker f.closure.toFun = ⊥
h1 : (fun a => a.swap) '' ↑f.graph = ⇑↑(LinearEquiv.prodComm R E F).symm ⁻¹' ↑f.graph
h2 : (fun a => a.swap) '' _root_.closure ↑f.graph = ⇑↑(LinearEquiv.prodComm R E F).symm ⁻¹' _root_.closure ↑f.graph
⊢ _root_.closure (Prod.swap '' ↑f.graph) ⊆ Prod.swap '' _root_.closure ↑f.graph

Tactic:
rw [h1, h2]

Result:
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : f.IsClosable
hcf : LinearMap.ker f.closure.toFun = ⊥
h1 : (fun a => a.swap) '' ↑f.graph = ⇑↑(LinearEquiv.prodComm R E F).symm ⁻¹' ↑f.graph
h2 : (fun a => a.swap) '' _root_.closure ↑f.graph = ⇑↑(LinearEquiv.prodComm R E F).symm ⁻¹' _root_.closure ↑f.graph
⊢ _root_.closure (⇑↑(LinearEquiv.prodComm R E F).symm ⁻¹' ↑f.graph) ⊆
    ⇑↑(LinearEquiv.prodComm R E F).symm ⁻¹' _root_.closure ↑f.graph

Proof state:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : f.IsClosable
hcf : LinearMap.ker f.closure.toFun = ⊥
⊢ f.closure.inverse.graph = f.inverse.graph.topologicalClosure

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

Result:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : f.IsClosable
hcf : LinearMap.ker f.closure.toFun = ⊥
⊢ Submodule.map (LinearEquiv.prodComm R E F) f.graph.topologicalClosure =
    (Submodule.map (LinearEquiv.prodComm R E F) f.graph).topologicalClosure

Proof state:
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : f.IsClosable
hcf : LinearMap.ker f.closure.toFun = ⊥
h1 : ⇑(LinearEquiv.prodComm R E F).toEquiv '' ↑f.graph = ⇑(LinearEquiv.prodComm R E F).toEquiv.symm ⁻¹' ↑f.graph
⊢ _root_.closure (Prod.swap '' ↑f.graph) ⊆ Prod.swap '' _root_.closure ↑f.graph

Tactic:
have h2 := Set.image_equiv_eq_preimage_symm (_root_.closure f.graph)
  (LinearEquiv.prodComm R E F).toEquiv

Result:
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : f.IsClosable
hcf : LinearMap.ker f.closure.toFun = ⊥
h1 : ⇑(LinearEquiv.prodComm R E F).toEquiv '' ↑f.graph = ⇑(LinearEquiv.prodComm R E F).toEquiv.symm ⁻¹' ↑f.graph
h2 :
  ⇑(LinearEquiv.prodComm R E F).toEquiv '' _root_.closure ↑f.graph =
    ⇑(LinearEquiv.prodComm R E F).toEquiv.symm ⁻¹' _root_.closure ↑f.graph
⊢ _root_.closure (Prod.swap '' ↑f.graph) ⊆ Prod.swap '' _root_.closure ↑f.graph