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
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) ∈ closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
a : (0, x) ∈ Prod.swap '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
⊢ (0, x) ∈ (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).topologicalClosure

Tactic:
apply image_closure_subset_closure_image continuous_swap

Premises used: continuous_swap, 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
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' : (x, 0) ∈ closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
a : ∃ (a : E) (b : F), (a, b) ∈ closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F)) ∧ b = 0 ∧ a = x
⊢ (0, x) ∈ Prod.swap '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))

Tactic:
simp only [Set.mem_image, Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]

Premises used: Set.mem_image, Prod.swap_prod_mk, Prod.mk.injEq, Prod.exists
-- 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) ∈ closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
⊢ ∃ (a : E) (b : F), (a, b) ∈ closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F)) ∧ b = 0 ∧ a = x

Tactic:
⟨x, 0, hx', rfl, rfl⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat, 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
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) ∈ closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
⊢ ∃ (a : E) (b : F), (a, b) ∈ closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F)) ∧ b = 0 ∧ a = x

Tactic:
exact ⟨x, 0, hx', rfl, 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
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
⊢ (0, x) ∈ f'.graph

Tactic:
have : (0, x) ∈ graph f' := by
      rw [← h, inverse_graph hf]
      rw [← hf'.graph_closure_eq_closure_graph, ← SetLike.mem_coe,
        Submodule.topologicalClosure_coe] at hx'
      apply image_closure_subset_closure_image continuous_swap
      simp only [Set.mem_image, Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]
      exact ⟨x, 0, hx', rfl, 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
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
this : (0, x) ∈ f'.graph
⊢ x = 0

Tactic:
graph_fst_eq_zero_snd f' this rfl

Premises used: LinearPMap.graph_fst_eq_zero_snd, 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
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
this : (0, x) ∈ f'.graph
⊢ x = 0

Tactic:
exact graph_fst_eq_zero_snd f' this rfl

Premises used: LinearPMap.graph_fst_eq_zero_snd, 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
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
h : f.closure.toFun.ker = ⊥
h₁ : f.inverse.graph.topologicalClosure = f.closure.inverse.graph
⊢ f.inverse.IsClosable

Tactic:
use f.closure.inverse

Premises used: LinearPMap.inverse, 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
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
h : f.closure.toFun.ker = ⊥
⊢ f.inverse.graph.topologicalClosure = f.closure.inverse.graph

Tactic:
(closure_inverse_graph hf hf' h).symm

Premises used: LinearPMap.closure_inverse_graph, Eq.symm
-- 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
h : f.closure.toFun.ker = ⊥
⊢ f.inverse.graph.topologicalClosure = f.closure.inverse.graph

Tactic:
exact (closure_inverse_graph hf hf' h).symm

Premises used: LinearPMap.closure_inverse_graph, Eq.symm
-- 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 : f.inverse.closure.graph = f.closure.inverse.graph
⊢ f.inverse.closure = f.closure.inverse

Tactic:
apply eq_of_eq_graph

Premises used: LinearPMap.eq_of_eq_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 : f.inverse.closure.graph = f.inverse.graph.topologicalClosure
h₁ h₂ : f.inverse.closure.graph = f.inverse.closure.graph
⊢ f.inverse.closure.graph = f.closure.inverse.graph

Tactic:
rw [closure_inverse_graph hf hf' hcf,
    ((inverse_isClosable_iff hf hf').mpr hcf).graph_closure_eq_closure_graph]

Premises used: Iff.mpr, LinearPMap.inverse_isClosable_iff, LinearPMap.closure_inverse_graph, LinearPMap.IsClosable.graph_closure_eq_closure_graph
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
⊢ LocallyConvexSpace 𝕜 E ↔ ∀ (x : E), (𝓝 x).HasBasis (fun (s : Set E) ↦ s ∈ 𝓝 x ∧ Convex 𝕜 s) id

Tactic:
⟨fun _ ↦ LocallyConvexSpace.convex_basis, LocallyConvexSpace.mk⟩

Premises used: LocallyConvexSpace.mk, Iff.intro, LocallyConvexSpace.convex_basis
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
ι : Type u_3
b : E → ι → Set E
p : E → ι → Prop
hbasis : ∀ (x : E), (𝓝 x).HasBasis (p x) (b x)
hconvex : ∀ (x : E) (i : ι), p x i → Convex 𝕜 (b x i)
⊢ LocallyConvexSpace 𝕜 E

Tactic:
⟨fun x =>
    (hbasis x).to_hasBasis
      (fun i hi => ⟨b x i, ⟨⟨(hbasis x).mem_of_mem hi, hconvex x i hi⟩, le_refl (b x i)⟩⟩)
      fun s hs =>
      ⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩⟩

Premises used: LocallyConvexSpace.mk, le_refl, Filter.HasBasis.index, Filter.HasBasis.property_index, Filter.HasBasis.set_index_subset, And.left, And.intro, Exists.intro, Subtype.val, Filter.HasBasis.to_hasBasis, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
⊢ HasBasis (𝓝 0) (fun (s : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s) id

Tactic:
LocallyConvexSpace.convex_basis 0

Premises used: LocallyConvexSpace.convex_basis, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
⊢ LocallyConvexSpace 𝕜 E ↔ ∀ (x : E), ∀ U ∈ 𝓝 x, ∃ S ∈ 𝓝 x, Convex 𝕜 S ∧ S ⊆ U

Tactic:
(locallyConvexSpace_iff 𝕜 E).trans (forall_congr' fun _ => hasBasis_self)

Premises used: locallyConvexSpace_iff, Filter.hasBasis_self, forall_congr', Iff.trans
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : HasBasis (𝓝 0) p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
⊢ LocallyConvexSpace 𝕜 E

Tactic:
LocallyConvexSpace.ofBases 𝕜 E (fun (x : E) (i : ι) => (x + ·) '' b i) (fun _ => p)
    (fun x => ?_) fun x i hi => (hconvex i hi).translate x

Premises used: LocallyConvexSpace.ofBases, Convex.translate, HAdd.hAdd, Set.image
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : HasBasis (𝓝 0) p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
refine :
  ∀ (x : E),
    HasBasis.{u_2, u_3 + 1} (ι := ι) (𝓝 x) ((fun (x : E) ↦ p) x)
      ((fun (x : E) (i : ι) ↦ ((fun (x_1 : E) ↦ x + x_1) '' b i : Set E)) x)
⊢ LocallyConvexSpace 𝕜 E

Tactic:
refine LocallyConvexSpace.ofBases 𝕜 E (fun (x : E) (i : ι) => (x + ·) '' b i) (fun _ => p)
    (fun x => ?_) fun x i hi => (hconvex i hi).translate x

Premises used: LocallyConvexSpace.ofBases, Convex.translate, HAdd.hAdd, Set.image
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : HasBasis (𝓝 0) p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
x : E
rw :
  HasBasis.{u_2, u_3 + 1} (α := E) (ι := ι) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0)) ((fun (x : E) ↦ p) x)
    ((fun (x : E) (i : ι) ↦ ((fun (x_1 : E) ↦ x + x_1) '' b i : Set E)) x)
⊢ HasBasis.{u_2, u_3 + 1} (ι := ι) (𝓝 x) ((fun (x : E) ↦ p) x)
    ((fun (x : E) (i : ι) ↦ ((fun (x_1 : E) ↦ x + x_1) '' b i : Set E)) x)

Tactic:
rw [← map_add_left_nhds_zero]

Premises used: map_add_left_nhds_zero
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : HasBasis (𝓝 0) p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
x : E
⊢ HasBasis.{u_2, u_3 + 1} (α := E) (ι := ι) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0)) ((fun (x : E) ↦ p) x)
    ((fun (x : E) (i : ι) ↦ ((fun (x_1 : E) ↦ x + x_1) '' b i : Set E)) x)

Tactic:
hbasis.map _

Premises used: Filter.HasBasis.map
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : HasBasis (𝓝 0) p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
x : E
⊢ HasBasis.{u_2, u_3 + 1} (α := E) (ι := ι) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0)) ((fun (x : E) ↦ p) x)
    ((fun (x : E) (i : ι) ↦ ((fun (x_1 : E) ↦ x + x_1) '' b i : Set E)) x)

Tactic:
exact hbasis.map _

Premises used: Filter.HasBasis.map
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
⊢ LocallyConvexSpace 𝕜 E ↔ HasBasis (𝓝 0) (fun (s : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s) id

Tactic:
⟨fun _ => LocallyConvexSpace.convex_basis 0, fun h =>
    LocallyConvexSpace.ofBasisZero 𝕜 E _ _ h fun _ => And.right⟩

Premises used: Membership.mem, nhds, id, And, And.right, Convex, Iff.intro, LocallyConvexSpace.convex_basis, LocallyConvexSpace.ofBasisZero, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
⊢ LocallyConvexSpace 𝕜 E ↔
    ∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (S : Set E), Membership.mem (γ := Filter E) (𝓝 0) S ∧ Convex 𝕜 S ∧ S ⊆ U

Tactic:
(locallyConvexSpace_iff_zero 𝕜 E).trans hasBasis_self

Premises used: Filter.hasBasis_self, Iff.trans, locallyConvexSpace_iff_zero
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : Module ℝ E
inst_7 : ContinuousSMul ℝ E
inst_8 : LocallyConvexSpace ℝ E
⊢ LocPathConnectedSpace E

Tactic:
.of_bases (fun x ↦ convex_basis (𝕜 := ℝ) x)
    fun _ _ hs ↦ hs.2.isPathConnected <| nonempty_of_mem <| mem_of_mem_nhds hs.1

Premises used: Convex.isPathConnected, mem_of_mem_nhds, And.right, And.left, Set.nonempty_of_mem, LocallyConvexSpace.convex_basis, LocPathConnectedSpace.of_bases
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
⊢ LocPathConnectedSpace.{u_2} (↑S : Type u_2)

Tactic:
⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨t, ht⟩ ↦ mem_of_superset ht.1.1 ht.2⟩⟩⟩

Premises used: _private.0.Convex.locPathConnectedSpace.match_1, Membership.mem, nhds, LocPathConnectedSpace.mk, And.right, And.left, Filter.HasBasis.mk, Iff.intro, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
refine :
  ∀ (x : (↑S : Type u_2)) (s : Set (↑S : Type u_2)) (hs : s ∈ 𝓝 x),
    ∃ (i : Set (↑S : Type u_2)), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
⊢ LocPathConnectedSpace.{u_2} (↑S : Type u_2)

Tactic:
refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨t, ht⟩ ↦ mem_of_superset ht.1.1 ht.2⟩⟩⟩
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : (↑S : Type u_2)
s : Set (↑S : Type u_2)
hs : s ∈ 𝓝 x
let :
  ∀ (t : Set E) (ht : t ∈ 𝓝 (↑x : E) ∧ Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t ⊆ s),
    ∃ (i : Set (↑S : Type u_2)), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
⊢ ∃ (i : Set (↑S : Type u_2)), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
let ⟨t, ht⟩ := (mem_nhds_subtype S x s).mp hs
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : (↑S : Type u_2)
s : Set (↑S : Type u_2)
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 (↑x : E) ∧ Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t ⊆ s
let :
  ∀ (t' : Set E) (ht' : (t' ∈ 𝓝 (↑x : E) ∧ Convex ℝ t') ∧ id t' ⊆ t),
    ∃ (i : Set (↑S : Type u_2)), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
⊢ ∃ (i : Set (↑S : Type u_2)), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
let ⟨t', ht'⟩ := (LocallyConvexSpace.convex_basis (𝕜 := ℝ) x.1).mem_iff.mp ht.1
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : (↑S : Type u_2)
s : Set (↑S : Type u_2)
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 (↑x : E) ∧ Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 (↑x : E) ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ ∃ (i : Set (↑S : Type u_2)), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
⟨(↑) ⁻¹' t', ⟨?_, ?_⟩, (preimage_mono ht'.2).trans ht.2⟩

Premises used: HasSubset.Subset.trans, Set.preimage_mono, And.right, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : (↑S : Type u_2)
s : Set (↑S : Type u_2)
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 (↑x : E) ∧ Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 (↑x : E) ∧ Convex ℝ t') ∧ id t' ⊆ t
refine_1 : Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t' ∈ 𝓝 x
refine_2 : IsPathConnected (X := (↑S : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t')
⊢ ∃ (i : Set (↑S : Type u_2)), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
refine ⟨(↑) ⁻¹' t', ⟨?_, ?_⟩, (preimage_mono ht'.2).trans ht.2⟩
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : (↑S : Type u_2)
s : Set (↑S : Type u_2)
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 (↑x : E) ∧ Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 (↑x : E) ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t' ∈ 𝓝 x

Tactic:
continuousAt_subtype_val.preimage_mem_nhds ht'.1.1

Premises used: continuousAt_subtype_val, Set.Mem, ContinuousAt.preimage_mem_nhds, And.left
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : (↑S : Type u_2)
s : Set (↑S : Type u_2)
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 (↑x : E) ∧ Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 (↑x : E) ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t' ∈ 𝓝 x

Tactic:
exact continuousAt_subtype_val.preimage_mem_nhds ht'.1.1

Premises used: continuousAt_subtype_val, ContinuousAt.preimage_mem_nhds, And.left
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : (↑S : Type u_2)
s : Set (↑S : Type u_2)
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 (↑x : E) ∧ Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 (↑x : E) ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ IsPathConnected (X := (↑S : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t')

Tactic:
Subtype.preimage_coe_self_inter _ _ ▸ IsPathConnected.preimage_coe ?_ inter_subset_left

Premises used: Eq.rec, Set.inter_subset_left, Subtype.preimage_coe_self_inter, IsPathConnected.preimage_coe
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : (↑S : Type u_2)
s : Set (↑S : Type u_2)
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 (↑x : E) ∧ Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 (↑x : E) ∧ Convex ℝ t') ∧ id t' ⊆ t
refine_2 : IsPathConnected (S ∩ t')
⊢ IsPathConnected (X := (↑S : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t')

Tactic:
refine Subtype.preimage_coe_self_inter _ _ ▸ IsPathConnected.preimage_coe ?_ inter_subset_left
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : (↑S : Type u_2)
s : Set (↑S : Type u_2)
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 (↑x : E) ∧ Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 (↑x : E) ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ IsPathConnected (S ∩ t')

Tactic:
(hS.inter ht'.1.2).isPathConnected ⟨x, x.2, mem_of_mem_nhds ht'.1.1⟩

Premises used: Convex.isPathConnected, mem_of_mem_nhds, Convex.inter, And.right, And.left, And.intro, Exists.intro, Subtype.val, Subtype.property