awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : IsUniformAddGroup E
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
⊢ ∃ (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₁ : (uniformity E).HasBasis (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: rw [← uniformity_eq_comap_nhds_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
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_2 : IsUniformAddGroup E
this :
  (uniformity E).HasBasis (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
⊢ ∃ (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 rcases : ∀ (V : Set E)
  (hV :
    Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
      (⋃ x ∈ t, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V)))
  (hV0 : 0 ∈ V) (hVopen : IsOpen[inst_5] V) (hVconvex : Convex 𝕜 V),
  ∃ (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
Tactic: rcases disj.exists_uniform_thickening_of_basis this hs₂ ht₂ with ⟨V, ⟨hV0, hVopen, hVconvex⟩, hV⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
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_2 : IsUniformAddGroup E
this :
  (uniformity E).HasBasis (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
V : Set E
hV :
  Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
    (⋃ x ∈ t, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen[inst_5] V
hVconvex : Convex 𝕜 V
⊢ ∃ (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 refine : Disjoint (s + V) (t + V)
Tactic: refine ⟨s + V, t + V, hVopen.add_left, hVopen.add_left, hs₁.add hVconvex, ht₁.add hVconvex,
    subset_add_left _ hV0, subset_add_left _ hV0, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
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_2 : IsUniformAddGroup E
this :
  (uniformity E).HasBasis (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
V : Set E
hV :
  Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
    (⋃ x ∈ t, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen[inst_5] V
hVconvex : Convex 𝕜 V
⊢ Disjoint (s + V) (t + V)
have simp_rw : Disjoint.{u_2} (α := Set E) (⋃ a ∈ s, (fun (x : E) ↦ -a + x) ⁻¹' V) (⋃ a ∈ t, (fun (x : E) ↦ -a + x) ⁻¹' V)
Tactic: simp_rw [← iUnion_add_left_image, image_add_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_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this :
  (uniformity E).HasBasis (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
V : Set E
hV :
  Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
    (⋃ x ∈ t, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen[inst_5] V
hVconvex : Convex 𝕜 V
⊢ Disjoint.{u_2} (α := Set E) (⋃ a ∈ s, (fun (x : E) ↦ -a + x) ⁻¹' V) (⋃ a ∈ t, (fun (x : E) ↦ -a + x) ⁻¹' V)
have hV₁ : Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, (fun (x : E × E) ↦ -x.1 + x.2) ∘ Prod.mk x ⁻¹' id V)
  (⋃ x ∈ t, (fun (x : E × E) ↦ -x.1 + x.2) ∘ Prod.mk x ⁻¹' id V)
Tactic: simp_rw [UniformSpace.ball, ← preimage_comp, sub_eq_neg_add] at hV
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
⊢ LocallyConvexSpace 𝕜 E
have refine : ∀ (x : E),
  (𝓝 x).HasBasis (ι := Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E))
    ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦
        If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i))
      x)
    ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦ (⋂ i ∈ If.1, If.2 i : Set E)) x)
Tactic: refine .ofBases 𝕜 E (fun _ => fun If : Set ts × (ts → Set E) => ⋂ i ∈ If.1, If.2 i)
      (fun x => fun If : Set ts × (ts → Set E) =>
        If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ @nhds _ (↑i) x ∧ Convex 𝕜 (If.2 i))
      (fun x => ?_) fun x If hif => convex_iInter fun i => convex_iInter fun hi => (hif.2 i hi).2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ (𝓝 x).HasBasis (ι := Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E))
    ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦
        If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i))
      x)
    ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦ (⋂ i ∈ If.1, If.2 i : Set E)) x)
have rw : HasBasis.{u_3, u_3 + 1} (α := E) (ι := Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E))
  (⨅ (i : (↑ts : Type u_3)), 𝓝 x)
  ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i))
    x)
  ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦ (⋂ i ∈ If.1, If.2 i : Set E)) x)
Tactic: rw [nhds_sInf, ← iInf_subtype'']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
have rw : LocallyConvexSpace 𝕜 E
Tactic: rw [inf_eq_iInf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
have refine : ∀ (b : Bool), LocallyConvexSpace 𝕜 E
Tactic: refine .iInf fun b => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
b : Bool
⊢ LocallyConvexSpace 𝕜 E
have false : LocallyConvexSpace 𝕜 E
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
b : Bool
false : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
have true : LocallyConvexSpace 𝕜 E
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
t : TopologicalSpace F
inst_6 : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f : (a : E) → F) t
⊢ LocallyConvexSpace 𝕜 E
have refine : ∀ (x : E),
  HasBasis.{u_3, u_4 + 1} (ι := Set F) (𝓝 x)
    ((fun (x : E) (s : Set F) ↦ Membership.mem (γ := Filter F) (𝓝 ((f : (a : E) → F) x) : Filter F) s ∧ Convex 𝕜 s) x)
    ((fun (x : E) ↦ (preimage (⇑f : (a : E) → F) : (s : Set F) → Set E)) x)
Tactic: refine LocallyConvexSpace.ofBases 𝕜 E (fun _ => preimage f)
    (fun x => fun s : Set F => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) (fun x => ?_) fun x s ⟨_, hs⟩ =>
    hs.linear_preimage f
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
t : TopologicalSpace F
inst_6 : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f : (a : E) → F) t
x : E
⊢ HasBasis.{u_3, u_4 + 1} (ι := Set F) (𝓝 x)
    ((fun (x : E) (s : Set F) ↦ Membership.mem (γ := Filter F) (𝓝 ((f : (a : E) → F) x) : Filter F) s ∧ Convex 𝕜 s) x)
    ((fun (x : E) ↦ (preimage (⇑f : (a : E) → F) : (s : Set F) → Set E)) x)
have rw : HasBasis.{u_3, u_4 + 1} (α := E) (ι := Set F)
  (comap.{u_3, u_4} (β := F) ((⇑f : (a : E) → F) : (a : E) → F) (𝓝 ((f : (a : E) → F) x) : Filter F))
  ((fun (x : E) (s : Set F) ↦ Membership.mem (γ := Filter F) (𝓝 ((f : (a : E) → F) x) : Filter F) s ∧ Convex 𝕜 s) x)
  ((fun (x : E) ↦ (preimage (⇑f : (a : E) → F) : (s : Set F) → Set E)) x)
Tactic: rw [nhds_induced]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : LocallyConvexSpace 𝕜 F
inst_8 : TopologicalSpace E
f : E →ₗ[𝕜] F
hf : IsInducing.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F)
⊢ LocallyConvexSpace 𝕜 E
have rw : LocallyConvexSpace 𝕜 E
Tactic: rw [hf.eq_induced]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
⊢ (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
have inl : ∀ (hl : IsBot x), (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
Tactic: obtain hl | hl := isBot_or_exists_lt x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
inl : ∀ (hl : IsBot x), (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
⊢ (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
have inr : ∀ (hl : ∃ (b : R), b < x), (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
Tactic: obtain hl | hl := isBot_or_exists_lt x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : IsBot x
⊢ (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
have inl : ∀ [inst_5 : OrderBot R], HasBasis (𝓝 ⊥) (fun (s : Set R) ↦ Membership.mem (γ := Filter R) (𝓝 ⊥) s ∧ Convex R s) id
Tactic: refine hl.rec ?_ _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : IsBot x
inst_5 : OrderBot R
⊢ HasBasis (𝓝 ⊥) (fun (s : Set R) ↦ Membership.mem (γ := Filter R) (𝓝 ⊥) s ∧ Convex R s) id
have inl : ∀ (i : R), ⊥ < i → ∃ (i' : Set R), (Membership.mem (γ := Filter R) (𝓝 ⊥) i' ∧ Convex R i') ∧ id i' ⊆ Iio i
Tactic: refine nhds_bot_basis.to_hasBasis' ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : IsBot x
inst_5 : OrderBot R
inl : ∀ (i : R), ⊥ < i → ∃ (i' : Set R), (Membership.mem (γ := Filter R) (𝓝 ⊥) i' ∧ Convex R i') ∧ id i' ⊆ Iio i
⊢ HasBasis (𝓝 ⊥) (fun (s : Set R) ↦ Membership.mem (γ := Filter R) (𝓝 ⊥) s ∧ Convex R s) id
have inl₁ : ∀ (i' : Set R), Membership.mem (γ := Filter R) (𝓝 ⊥) i' ∧ Convex R i' → Membership.mem (γ := Filter R) (𝓝 ⊥) (id i')
Tactic: refine nhds_bot_basis.to_hasBasis' ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : IsBot x
inst_5 : OrderBot R
i : R
h : ⊥ < i
⊢ ∃ (i' : Set R), (Membership.mem (γ := Filter R) (𝓝 ⊥) i' ∧ Convex R i') ∧ id i' ⊆ Iio i
have inl : Membership.mem (γ := Filter R) (𝓝 ⊥) (Iio i) ∧ Convex R (Iio i)
Tactic: refine ⟨Set.Iio _, ?_, .rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : ∃ (b : R), b < x
⊢ (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
have inr : ∀ (hu : IsTop x), (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
Tactic: obtain hu | hu := isTop_or_exists_gt x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : ∃ (b : R), b < x
inr : ∀ (hu : IsTop x), (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
⊢ (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
have inr₁ : ∀ (hu : ∃ (b : R), x < b), (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
Tactic: obtain hu | hu := isTop_or_exists_gt x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : ∃ (b : R), b < x
hu : IsTop x
⊢ (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
have inr : ∀ [inst_5 : OrderTop R], HasBasis (𝓝 ⊤) (fun (s : Set R) ↦ Membership.mem (γ := Filter R) (𝓝 ⊤) s ∧ Convex R s) id
Tactic: refine hu.rec ?_ _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : ∃ (b : R), b < x
hu : IsTop x
inst_5 : OrderTop R
⊢ HasBasis (𝓝 ⊤) (fun (s : Set R) ↦ Membership.mem (γ := Filter R) (𝓝 ⊤) s ∧ Convex R s) id
have inr : ∀ i < ⊤, ∃ (i' : Set R), (Membership.mem (γ := Filter R) (𝓝 ⊤) i' ∧ Convex R i') ∧ id i' ⊆ Ioi i
Tactic: refine nhds_top_basis.to_hasBasis' ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : ∃ (b : R), b < x
hu : IsTop x
inst_5 : OrderTop R
inr : ∀ i < ⊤, ∃ (i' : Set R), (Membership.mem (γ := Filter R) (𝓝 ⊤) i' ∧ Convex R i') ∧ id i' ⊆ Ioi i
⊢ HasBasis (𝓝 ⊤) (fun (s : Set R) ↦ Membership.mem (γ := Filter R) (𝓝 ⊤) s ∧ Convex R s) id
have inr₁ : ∀ (i' : Set R), Membership.mem (γ := Filter R) (𝓝 ⊤) i' ∧ Convex R i' → Membership.mem (γ := Filter R) (𝓝 ⊤) (id i')
Tactic: refine nhds_top_basis.to_hasBasis' ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : ∃ (b : R), b < x
hu : IsTop x
inst_5 : OrderTop R
i : R
h : i < ⊤
⊢ ∃ (i' : Set R), (Membership.mem (γ := Filter R) (𝓝 ⊤) i' ∧ Convex R i') ∧ id i' ⊆ Ioi i
have inr : Membership.mem (γ := Filter R) (𝓝 ⊤) (Ioi i) ∧ Convex R (Ioi i)
Tactic: refine ⟨Set.Ioi _, ?_, subset_rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : ∃ (b : R), b < x
hu : ∃ (b : R), x < b
⊢ (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
have inr : ∀ (i : R × R), i.1 < x ∧ x < i.2 → ∃ (i' : Set R), (i' ∈ 𝓝 x ∧ Convex R i') ∧ id i' ⊆ Ioo i.1 i.2
Tactic: refine (nhds_basis_Ioo' hl hu).to_hasBasis' ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : ∃ (b : R), b < x
hu : ∃ (b : R), x < b
inr : ∀ (i : R × R), i.1 < x ∧ x < i.2 → ∃ (i' : Set R), (i' ∈ 𝓝 x ∧ Convex R i') ∧ id i' ⊆ Ioo i.1 i.2
⊢ (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
have inr₁ : ∀ (i' : Set R), i' ∈ 𝓝 x ∧ Convex R i' → id i' ∈ 𝓝 x
Tactic: refine (nhds_basis_Ioo' hl hu).to_hasBasis' ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
x : R
hl : ∃ (b : R), b < x
hu : ∃ (b : R), x < b
⊢ ∀ (i : R × R), i.1 < x ∧ x < i.2 → ∃ (i' : Set R), (i' ∈ 𝓝 x ∧ Convex R i') ∧ id i' ⊆ Ioo i.1 i.2
have inr : ∀ (a b : R), a < x → x < b → ∃ (i' : Set R), (i' ∈ 𝓝 x ∧ Convex R i') ∧ i' ⊆ Ioo a b
Tactic: simp only [id_eq, and_imp, Prod.forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
s : Set E
hs : Convex 𝕜 s
x₀ : E
hx₀s : x₀ ∈ s
p : E → Prop
h : ∀ᶠ (x : E) in 𝓝[s] x₀, p x
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ∀ y ∈ [x₀ -[𝕜] x], p y
have rw : ∀ (h : ∃ (i : Set E), (i ∈ 𝓝 x₀ ∧ Convex 𝕜 i) ∧ ∀ ⦃x : E⦄, x ∈ id i → x ∈ s → p x),
  ∃ (i : Set E), (i ∈ 𝓝 x₀ ∧ Convex 𝕜 i) ∧ ∀ ⦃x : E⦄, x ∈ id i → x ∈ s → ∀ y ∈ [x₀ -[𝕜] x], p y
Tactic: rw [eventually_nhdsWithin_iff, (LocallyConvexSpace.convex_basis (𝕜 := 𝕜) x₀).eventually_iff]
    at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
s : Set E
hs : Convex 𝕜 s
x₀ : E
hx₀s : x₀ ∈ s
p : E → Prop
h : ∃ (i : Set E), (i ∈ 𝓝 x₀ ∧ Convex 𝕜 i) ∧ ∀ ⦃x : E⦄, x ∈ id i → x ∈ s → p x
⊢ ∃ (i : Set E), (i ∈ 𝓝 x₀ ∧ Convex 𝕜 i) ∧ ∀ ⦃x : E⦄, x ∈ id i → x ∈ s → ∀ y ∈ [x₀ -[𝕜] x], p y
have obtain : ∀ (u : Set E) (h : ∀ ⦃x : E⦄, x ∈ id u → x ∈ s → p x) (hu_nhds : u ∈ 𝓝 x₀) (hu_convex : Convex 𝕜 u),
  ∃ (i : Set E), (i ∈ 𝓝 x₀ ∧ Convex 𝕜 i) ∧ ∀ ⦃x : E⦄, x ∈ id i → x ∈ s → ∀ y ∈ [x₀ -[𝕜] x], p y
Tactic: obtain ⟨u, ⟨hu_nhds, hu_convex⟩, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
s : Set E
hs : Convex 𝕜 s
x₀ : E
hx₀s : x₀ ∈ s
p : E → Prop
u : Set E
h : ∀ ⦃x : E⦄, x ∈ id u → x ∈ s → p x
hu_nhds : u ∈ 𝓝 x₀
hu_convex : Convex 𝕜 u
⊢ ∃ (i : Set E), (i ∈ 𝓝 x₀ ∧ Convex 𝕜 i) ∧ ∀ ⦃x : E⦄, x ∈ id i → x ∈ s → ∀ y ∈ [x₀ -[𝕜] x], p y
have refine : ∀ (x : E) (hxu : x ∈ id u) (hxs : x ∈ s) (y : E) (hy : y ∈ [x₀ -[𝕜] x]), y ∈ id u
Tactic: refine ⟨u, ⟨hu_nhds, hu_convex⟩, fun x hxu hxs y hy ↦ h ?_ (hs.segment_subset hx₀s hxs hy)⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.LocallyConvex (goal)
Goal:
E : Type u_1
𝕜 : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
s : Set E
hs : Convex 𝕜 s
x₀ : E
hx₀s : x₀ ∈ s
p : E → Prop
u : Set E
h : ∀ ⦃x : E⦄, x ∈ id u → x ∈ s → p x
hu_nhds : u ∈ 𝓝 x₀
hu_convex : Convex 𝕜 u
x : E
hxu : x ∈ id u
hxs : x ∈ s
y : E
hy : y ∈ [x₀ -[𝕜] x]
⊢ y ∈ id u
have suffices : [x₀ -[𝕜] x] ⊆ u
Tactic: suffices segment 𝕜 x₀ x ⊆ u from this hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
A : Type u_3
inst_4 : AddCommMonoid A
inst_5 : Module R A
τA : TopologicalSpace A
inst_6 : IsModuleTopology R A
B' : Type u_5
inst_7 : AddCommMonoid B'
inst_8 : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
hσ' : Continuous.{u_2, u_1} (X := S) (Y := R) (⇑σ' : (a : S) → R)
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := (↑(↑e : A ≃ₛₗ[σ] B') : A →ₛₗ[σ] B')
g' : B' →ₛₗ[σ'] A := (↑(↑e.symm : B' ≃ₛₗ[σ'] A) : B' →ₛₗ[σ'] A)
h : A →+ B' := (↑e : A →+ B')
h' : B' →+ A := (↑e.symm : B' →+ A)
⊢ τB' = moduleTopology S B'
have simp_rw : Eq.{u_5 + 1} (α := TopologicalSpace B')
  (sInf
    (Set.image.{u_3, u_5} (α := TopologicalSpace A) (TopologicalSpace.induced (⇑e.toHomeomorph.symm : (a : B') → A))
      {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A}))
  (sInf {t : TopologicalSpace B' | ContinuousSMul S B' ∧ ContinuousAdd B'})
Tactic: simp_rw [e.toHomeomorph.symm.isInducing.1, eq_moduleTopology R A, moduleTopology, induced_sInf]