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 g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
⊢ g.graph.topologicalClosure ≤ f.graph.topologicalClosure

Tactic:
Submodule.topologicalClosure_mono (le_graph_of_le hfg)

Premises used: Set.Mem, Submodule.topologicalClosure_mono, LinearPMap.le_graph_of_le
-- 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 g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
⊢ g.graph.topologicalClosure ≤ f.graph.topologicalClosure

Tactic:
exact Submodule.topologicalClosure_mono (le_graph_of_le hfg)

Premises used: Submodule.topologicalClosure_mono, LinearPMap.le_graph_of_le
-- 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 g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
⊢ g.graph.topologicalClosure ≤ f'.graph

Tactic:
have : g.graph.topologicalClosure ≤ f'.graph := by
    rw [← hf]
    exact Submodule.topologicalClosure_mono (le_graph_of_le hfg)
-- 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 g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
this : g.graph.topologicalClosure ≤ f'.graph
h : g.graph.topologicalClosure = g.graph.topologicalClosure.toLinearPMap.graph
⊢ g.IsClosable

Tactic:
use g.graph.topologicalClosure.toLinearPMap

Premises used: LinearPMap.graph, Submodule.topologicalClosure, Submodule.toLinearPMap
-- 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 g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
this : g.graph.topologicalClosure ≤ f'.graph
h : ∀ (x : E × F) (_hx : x ∈ g.graph.topologicalClosure) (_hx' : x.1 = 0), x.2 = 0
⊢ g.graph.topologicalClosure = g.graph.topologicalClosure.toLinearPMap.graph

Tactic:
rw [Submodule.toLinearPMap_graph_eq]

Premises used: Submodule.toLinearPMap_graph_eq
-- 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 g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
this : g.graph.topologicalClosure ≤ f'.graph
⊢ ∀ (x : E × F) (_hx : x ∈ g.graph.topologicalClosure) (_hx' : x.1 = 0), x.2 = 0

Tactic:
fun _ hx hx' => f'.graph_fst_eq_zero_snd (this hx) hx'

Premises used: LinearPMap.graph_fst_eq_zero_snd
-- 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 g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
this : g.graph.topologicalClosure ≤ f'.graph
⊢ ∀ (x : E × F) (_hx : x ∈ g.graph.topologicalClosure) (_hx' : x.1 = 0), x.2 = 0

Tactic:
exact fun _ hx hx' => f'.graph_fst_eq_zero_snd (this hx) hx'

Premises used: LinearPMap.graph_fst_eq_zero_snd
-- 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
hf : f.IsClosable
⊢ ∃! f' : E →ₗ.[R] F, f.graph.topologicalClosure = f'.graph

Tactic:
existsUnique_of_exists_of_unique hf fun _ _ hy₁ hy₂ => eq_of_eq_graph ?_

Premises used: LinearPMap.eq_of_eq_graph, existsUnique_of_exists_of_unique
-- 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
hf : f.IsClosable
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
⊢ ∃! f' : E →ₗ.[R] F, f.graph.topologicalClosure = f'.graph

Tactic:
refine existsUnique_of_exists_of_unique hf fun _ _ hy₁ hy₂ => eq_of_eq_graph ?_

Premises used: LinearPMap.eq_of_eq_graph, existsUnique_of_exists_of_unique
-- 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
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
rw₁ rw₂ : f.graph.topologicalClosure = f.graph.topologicalClosure
⊢ x.graph = x_1.graph

Tactic:
rw [← hy₁, ← hy₂]
-- 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
hf : f.IsClosable
⊢ f.closure = Exists.choose (p := fun (f' : E →ₗ.[R] F) ↦ f.graph.topologicalClosure = f'.graph) hf

Tactic:
simp [closure, hf]

Premises used: LinearPMap.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
hf : ¬f.IsClosable
⊢ f.closure = f

Tactic:
simp [closure, hf]

Premises used: LinearPMap.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
hf : f.IsClosable
rw :
  f.graph.topologicalClosure =
    (Exists.choose (p := fun (f' : E →ₗ.[R] F) ↦ f.graph.topologicalClosure = f'.graph) hf).graph
⊢ f.graph.topologicalClosure = f.closure.graph

Tactic:
rw [closure_def hf]

Premises used: LinearPMap.closure_def
-- 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
hf : f.IsClosable
⊢ f.graph.topologicalClosure =
    (Exists.choose (p := fun (f' : E →ₗ.[R] F) ↦ f.graph.topologicalClosure = f'.graph) hf).graph

Tactic:
hf.choose_spec

Premises used: Exists.choose_spec
-- 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
hf : f.IsClosable
⊢ f.graph.topologicalClosure =
    (Exists.choose (p := fun (f' : E →ₗ.[R] F) ↦ f.graph.topologicalClosure = f'.graph) hf).graph

Tactic:
exact hf.choose_spec

Premises used: Exists.choose_spec
-- 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
pos : ∀ (hf : f.IsClosable), f ≤ f.closure
neg : ∀ (hf : ¬f.IsClosable), f ≤ f.closure
⊢ f ≤ f.closure

Tactic:
by_cases hf : f.IsClosable

Premises used: LinearPMap.IsClosable
-- 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
hf : f.IsClosable
⊢ f ≤ f.closure

Tactic:
le_of_le_graph ?_

Premises used: Set.Mem, LinearPMap.le_of_le_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
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
pos : f.graph ≤ f.closure.graph
⊢ f ≤ f.closure

Tactic:
refine le_of_le_graph ?_

Premises used: LinearPMap.le_of_le_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
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
pos : f.graph ≤ f.graph.topologicalClosure
⊢ f.graph ≤ f.closure.graph

Tactic:
rw [← hf.graph_closure_eq_closure_graph]

Premises used: 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
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.graph.topologicalClosure

Tactic:
(graph f).le_topologicalClosure

Premises used: Submodule.le_topologicalClosure, LinearPMap.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
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.graph.topologicalClosure

Tactic:
exact (graph f).le_topologicalClosure

Premises used: Submodule.le_topologicalClosure, LinearPMap.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
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
neg neg₁ : f ≤ f
⊢ f ≤ f.closure

Tactic:
rw [closure_def' hf]

Premises used: LinearPMap.closure_def'
-- 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 g : E →ₗ.[R] F
hg : g.IsClosable
h : f ≤ g
⊢ f.closure ≤ g.closure

Tactic:
le_of_le_graph ?_

Premises used: Set.Mem, LinearPMap.le_of_le_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
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
refine : f.closure.graph ≤ g.closure.graph
⊢ f.closure ≤ g.closure

Tactic:
refine le_of_le_graph ?_

Premises used: LinearPMap.le_of_le_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
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
rw : f.graph.topologicalClosure ≤ g.closure.graph
⊢ f.closure.graph ≤ g.closure.graph

Tactic:
rw [← (hg.leIsClosable h).graph_closure_eq_closure_graph]

Premises used: LinearPMap.IsClosable.leIsClosable, 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
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
rw : f.graph.topologicalClosure ≤ g.graph.topologicalClosure
⊢ f.graph.topologicalClosure ≤ g.closure.graph

Tactic:
rw [← hg.graph_closure_eq_closure_graph]

Premises used: 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
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.graph.topologicalClosure

Tactic:
Submodule.topologicalClosure_mono (le_graph_of_le h)

Premises used: Submodule.topologicalClosure_mono, LinearPMap.le_graph_of_le
-- 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 g : E →ₗ.[R] F
hg : g.IsClosable
h : f ≤ g
⊢ f.graph.topologicalClosure ≤ g.graph.topologicalClosure

Tactic:
exact Submodule.topologicalClosure_mono (le_graph_of_le h)

Premises used: Submodule.topologicalClosure_mono, LinearPMap.le_graph_of_le
-- 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
hf : f.IsClosable
rw : IsClosed[instTopologicalSpaceProd] (↑f.graph.topologicalClosure : Set (E × F))
⊢ f.closure.IsClosed

Tactic:
rw [IsClosed, ← hf.graph_closure_eq_closure_graph]

Premises used: LinearPMap.IsClosed, 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
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
⊢ IsClosed[instTopologicalSpaceProd] (↑f.graph.topologicalClosure : Set (E × F))

Tactic:
f.graph.isClosed_topologicalClosure

Premises used: Submodule.isClosed_topologicalClosure, LinearPMap.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
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
⊢ IsClosed[instTopologicalSpaceProd] (↑f.graph.topologicalClosure : Set (E × F))

Tactic:
exact f.graph.isClosed_topologicalClosure

Premises used: Submodule.isClosed_topologicalClosure, LinearPMap.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
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.IsClosable

Tactic:
hf.closure_isClosed.isClosable

Premises used: LinearPMap.IsClosed.isClosable, LinearPMap.IsClosable.closure_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
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.IsClosable ↔ ∃ (g : E →ₗ.[R] F), g.IsClosed ∧ f ≤ g

Tactic:
⟨fun h => ⟨f.closure, h.closure_isClosed, f.le_closure⟩, fun ⟨_, hg, h⟩ =>
    hg.isClosable.leIsClosable h⟩

Premises used: LinearPMap.closure, LinearPMap.IsClosable.leIsClosable, LinearPMap.IsClosed.isClosable, LinearPMap.IsClosable.closure_isClosed, And.intro, Iff.intro, Exists.intro, LinearPMap.le_closure, _private.0.LinearPMap.isClosable_iff_exists_closed_extension.match_1, LinearPMap.IsClosable
-- 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
S : Submodule R E
h : f.HasCore S
⊢ (f.domRestrict S).closure = f

Tactic:
h.2

Premises used: LinearPMap.HasCore.closure_eq
-- 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
⊢ f.closure.HasCore f.domain

Tactic:
⟨f.le_closure.1, ?_⟩

Premises used: LinearPMap.HasCore.mk, 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
refine : (f.closure.domRestrict f.domain).closure = f.closure
⊢ f.closure.HasCore f.domain

Tactic:
refine ⟨f.le_closure.1, ?_⟩
-- 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
e_f : f.closure.domRestrict f.domain = f
⊢ (f.closure.domRestrict f.domain).closure = f.closure

Tactic:
congr
-- 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
e_f : ∀ (x : E), x ∈ (f.closure.domRestrict f.domain).domain ↔ x ∈ f.domain
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)
⊢ f.closure.domRestrict f.domain = f

Tactic:
ext x h1 h2