awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)))
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)))
⊢ closure[instTopologicalSpaceProd] (Prod.swap '' (↑f.graph : Set (E × F))) ⊆
    Prod.swap '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
have 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)))
Tactic: simp only [LinearEquiv.coe_toEquiv, LinearEquiv.prodComm_apply] at h1 h2
Cleared hypotheses: h1, h2
-- 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)))
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)))
⊢ closure[instTopologicalSpaceProd] (Prod.swap '' (↑f.graph : Set (E × F))) ⊆
    Prod.swap '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
have 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)))
Tactic: simp only [LinearEquiv.coe_toEquiv, LinearEquiv.prodComm_apply] at h1 h2
Cleared hypotheses: 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
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)))
⊢ closure[instTopologicalSpaceProd] (Prod.swap '' (↑f.graph : Set (E × F))) ⊆
    Prod.swap '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
have 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)))
Tactic: rw [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
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.inverse.IsClosable ↔ f.closure.toFun.ker = ⊥
have mp : f.inverse.IsClosable → f.closure.toFun.ker = ⊥
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
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 = ⊥
⊢ f.inverse.IsClosable ↔ f.closure.toFun.ker = ⊥
have mpr : f.closure.toFun.ker = ⊥ → f.inverse.IsClosable
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
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
⊢ f.closure.toFun.ker = ⊥
have mp : ∀ (m : ↥f.closure.domain), Eq.{u_3 + 1} (α := F) ((f.closure.toFun : (a : ↥f.closure.domain) → F) m : F) (0 : F) → m = 0
Tactic: rw [LinearMap.ker_eq_bot']
-- 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
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)
⊢ Subtype.mk (p := fun (x : E) ↦ x ∈ f.closure.domain) x hx = 0
have mp : x = 0
Tactic: simp only [Submodule.mk_eq_zero]
-- 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
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
have hx'₁ : (x, 0) ∈ f.closure.graph
Tactic: rw [toFun_eq_coe, eq_comm, image_iff] at hx'
Cleared hypotheses: hx'
-- 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
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
have rw : (0, x) ∈ (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).topologicalClosure
Tactic: rw [← h, inverse_graph 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
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) ∈ (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).topologicalClosure
have hx'₁ : (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'
Cleared hypotheses: hx'
-- 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
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))
⊢ (0, x) ∈ (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).topologicalClosure
have a : (0, x) ∈ Prod.swap '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
Tactic: apply image_closure_subset_closure_image continuous_swap
-- 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
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))
⊢ (0, x) ∈ Prod.swap '' closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F))
have a : ∃ (a : E) (b : F), (a, b) ∈ closure[instTopologicalSpaceProd] (↑f.graph : Set (E × F)) ∧ b = 0 ∧ a = x
Tactic: simp only [Set.mem_image, Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]
-- 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
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
have this : (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⟩
-- 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
h : f.closure.toFun.ker = ⊥
⊢ f.inverse.IsClosable
have h₁ : f.inverse.graph.topologicalClosure = f.closure.inverse.graph
Tactic: use f.closure.inverse
-- 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.inverse.closure = f.closure.inverse
have h : f.inverse.closure.graph = f.closure.inverse.graph
Tactic: apply 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
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.inverse.closure.graph = f.closure.inverse.graph
have h : f.inverse.closure.graph = f.inverse.graph.topologicalClosure
Tactic: rw [closure_inverse_graph hf hf' hcf,
    ((inverse_isClosable_iff hf hf').mpr hcf).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 = ⊥
h : f.inverse.closure.graph = f.inverse.graph.topologicalClosure
⊢ f.inverse.closure.graph = f.closure.inverse.graph
have h₁ : f.inverse.closure.graph = f.inverse.closure.graph
Tactic: rw [closure_inverse_graph hf hf' hcf,
    ((inverse_isClosable_iff hf hf').mpr hcf).graph_closure_eq_closure_graph]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
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
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
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} (ι := ι) (𝓝 x) ((fun (x : E) ↦ p) x)
    ((fun (x : E) (i : ι) ↦ ((fun (x_1 : E) ↦ x + x_1) '' b i : Set E)) x)
have 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)
Tactic: rw [← map_add_left_nhds_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
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)
have 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
Tactic: refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨t, ht⟩ ↦ mem_of_superset ht.1.1 ht.2⟩⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
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
⊢ ∃ (i : Set (↑S : Type u_2)), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
have 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
Tactic: let ⟨t, ht⟩ := (mem_nhds_subtype S x s).mp hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
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
⊢ ∃ (i : Set (↑S : Type u_2)), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
have 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
Tactic: let ⟨t', ht'⟩ := (LocallyConvexSpace.convex_basis (𝕜 := ℝ) x.1).mem_iff.mp ht.1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
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
have refine_1 : Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t' ∈ 𝓝 x
Tactic: refine ⟨(↑) ⁻¹' t', ⟨?_, ?_⟩, (preimage_mono ht'.2).trans ht.2⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
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
⊢ ∃ (i : Set (↑S : Type u_2)), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
have refine_2 : IsPathConnected (X := (↑S : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t')
Tactic: refine ⟨(↑) ⁻¹' t', ⟨?_, ?_⟩, (preimage_mono ht'.2).trans ht.2⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
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')
have refine_2 : IsPathConnected (S ∩ t')
Tactic: refine Subtype.preimage_coe_self_inter _ _ ▸ IsPathConnected.preimage_coe ?_ inter_subset_left
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst_5] t
this : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
⊢ ∃ (u : Set E) (v : Set E),
    IsOpen[inst_5] u ∧ IsOpen[inst_5] v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
have this₁ : IsUniformAddGroup E
Tactic: haveI : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst_5] t
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ ∃ (u : Set E) (v : Set E),
    IsOpen[inst_5] u ∧ IsOpen[inst_5] v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
have this₁ : HasBasis (α := E × E) (comap (β := E) (fun (x : E × E) ↦ x.2 - x.1) (𝓝 0))
  (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_5] s ∧ Convex 𝕜 s) fun (i : Set E) ↦ (fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id i
Tactic: have := (LocallyConvexSpace.convex_open_basis_zero 𝕜 E).comap fun x : E × E => x.2 - x.1