awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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)
rw : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

Tactic:
rw [hf.eq_induced]

Premises used: Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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

Tactic:
.induced f

Premises used: LocallyConvexSpace.induced
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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

Tactic:
exact .induced f
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
ι : Sort u_1
𝕜 : 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 E
inst_7 : LocallyConvexSpace 𝕜 E
S : Submodule 𝕜 E
⊢ LocallyConvexSpace.{u_2, u_3} 𝕜 ↥S

Tactic:
IsInducing.locallyConvexSpace (f := S.subtype) .subtypeVal

Premises used: Topology.IsInducing.locallyConvexSpace, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
ι_1 : Sort u_1
𝕜 : 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
ι : Type u_5
X : ι → Type u_6
inst_6 : (i : ι) → AddCommMonoid (X i)
inst_7 : (i : ι) → TopologicalSpace (X i)
inst_8 : (i : ι) → Module.{u_2, u_6} 𝕜 (X i)
inst_9 : ∀ (i : ι), LocallyConvexSpace.{u_2, u_6} 𝕜 (X i)
⊢ LocallyConvexSpace 𝕜 ((i : ι) → X i)

Tactic:
.iInf fun i => .induced (LinearMap.proj i)

Premises used: LocallyConvexSpace.iInf, LinearMap.proj, LocallyConvexSpace.induced
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
ι : Sort u_1
𝕜 : 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 E
inst_7 : TopologicalSpace F
inst_8 : LocallyConvexSpace 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 F
⊢ LocallyConvexSpace 𝕜 (E × F)

Tactic:
.inf (.induced (LinearMap.fst _ _ _)) (.induced (LinearMap.snd _ _ _))

Premises used: LinearMap.fst, LocallyConvexSpace.inf, LinearMap.snd, setOf, LocallyConvexSpace.induced
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
inr : ∀ (hl : ∃ (b : R), b < 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

Tactic:
obtain hl | hl := isBot_or_exists_lt x

Premises used: isBot_or_exists_lt
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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

Tactic:
hl.rec ?_ _

Premises used: IsBot.rec
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
inl : ∀ [inst_5 : OrderBot R], HasBasis (𝓝 ⊥) (fun (s : Set R) ↦ Membership.mem (γ := Filter R) (𝓝 ⊥) s ∧ Convex R s) id
⊢ (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id

Tactic:
refine hl.rec ?_ _
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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

Tactic:
nhds_bot_basis.to_hasBasis' ?_ ?_

Premises used: nhds_bot_basis, Filter.HasBasis.to_hasBasis'
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
inl₁ :
  ∀ (i' : Set R), Membership.mem (γ := Filter R) (𝓝 ⊥) i' ∧ Convex R i' → Membership.mem (γ := Filter R) (𝓝 ⊥) (id i')
⊢ HasBasis (𝓝 ⊥) (fun (s : Set R) ↦ Membership.mem (γ := Filter R) (𝓝 ⊥) s ∧ Convex R s) id

Tactic:
refine nhds_bot_basis.to_hasBasis' ?_ ?_

Premises used: nhds_bot_basis, Filter.HasBasis.to_hasBasis'
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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

Tactic:
⟨Set.Iio _, ?_, .rfl⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro, Set.Iio
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
inl : Membership.mem (γ := Filter R) (𝓝 ⊥) (Iio i) ∧ Convex R (Iio i)
⊢ ∃ (i' : Set R), (Membership.mem (γ := Filter R) (𝓝 ⊥) i' ∧ Convex R i') ∧ id i' ⊆ Iio i

Tactic:
refine ⟨Set.Iio _, ?_, .rfl⟩
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
⊢ Membership.mem (γ := Filter R) (𝓝 ⊥) (Iio i) ∧ Convex R (Iio i)

Tactic:
simp_all [Iio_mem_nhds, convex_Iio]

Premises used: Iio_mem_nhds, convex_Iio
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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' : Set R), Membership.mem (γ := Filter R) (𝓝 ⊥) i' ∧ Convex R i' → Membership.mem (γ := Filter R) (𝓝 ⊥) (id i')

Tactic:
simp +contextual
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
inr₁ : ∀ (hu : ∃ (b : R), x < b), (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id
⊢ (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id

Tactic:
obtain hu | hu := isTop_or_exists_gt x

Premises used: isTop_or_exists_gt
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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

Tactic:
hu.rec ?_ _

Premises used: IsTop.rec
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
inr : ∀ [inst_5 : OrderTop R], HasBasis (𝓝 ⊤) (fun (s : Set R) ↦ Membership.mem (γ := Filter R) (𝓝 ⊤) s ∧ Convex R s) id
⊢ (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id

Tactic:
refine hu.rec ?_ _
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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

Tactic:
nhds_top_basis.to_hasBasis' ?_ ?_

Premises used: Filter.HasBasis.to_hasBasis', nhds_top_basis
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
inr₁ :
  ∀ (i' : Set R), Membership.mem (γ := Filter R) (𝓝 ⊤) i' ∧ Convex R i' → Membership.mem (γ := Filter R) (𝓝 ⊤) (id i')
⊢ HasBasis (𝓝 ⊤) (fun (s : Set R) ↦ Membership.mem (γ := Filter R) (𝓝 ⊤) s ∧ Convex R s) id

Tactic:
refine nhds_top_basis.to_hasBasis' ?_ ?_

Premises used: Filter.HasBasis.to_hasBasis', nhds_top_basis
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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

Tactic:
⟨Set.Ioi _, ?_, subset_rfl⟩

Premises used: Set.Ioi, And.intro, Exists.intro, subset_rfl
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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 < ⊤
inr : Membership.mem (γ := Filter R) (𝓝 ⊤) (Ioi i) ∧ Convex R (Ioi i)
⊢ ∃ (i' : Set R), (Membership.mem (γ := Filter R) (𝓝 ⊤) i' ∧ Convex R i') ∧ id i' ⊆ Ioi i

Tactic:
refine ⟨Set.Ioi _, ?_, subset_rfl⟩
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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 < ⊤
⊢ Membership.mem (γ := Filter R) (𝓝 ⊤) (Ioi i) ∧ Convex R (Ioi i)

Tactic:
simp_all
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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' : Set R), Membership.mem (γ := Filter R) (𝓝 ⊤) i' ∧ Convex R i' → Membership.mem (γ := Filter R) (𝓝 ⊤) (id i')

Tactic:
simp +contextual
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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

Tactic:
(nhds_basis_Ioo' hl hu).to_hasBasis' ?_ ?_

Premises used: nhds_basis_Ioo', Filter.HasBasis.to_hasBasis'
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
inr₁ : ∀ (i' : Set R), i' ∈ 𝓝 x ∧ Convex R i' → id i' ∈ 𝓝 x
⊢ (𝓝 x).HasBasis (fun (s : Set R) ↦ s ∈ 𝓝 x ∧ Convex R s) id

Tactic:
refine (nhds_basis_Ioo' hl hu).to_hasBasis' ?_ ?_

Premises used: nhds_basis_Ioo', Filter.HasBasis.to_hasBasis'
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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 : ∀ (a b : R), a < x → x < b → ∃ (i' : Set R), (i' ∈ 𝓝 x ∧ Convex R i') ∧ i' ⊆ Ioo a 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

Tactic:
simp only [id_eq, and_imp, Prod.forall]

Premises used: and_imp, Prod.forall, id_eq
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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_1 x_2 : R
h₁ : x_1 < x
h₂ : x < x_2
⊢ Ioo x_1 x_2 ∈ 𝓝 x ∧ Convex R (Ioo x_1 x_2)

Tactic:
simp [h₁, h₂, Ioo_mem_nhds, convex_Ioo]

Premises used: convex_Ioo, Ioo_mem_nhds
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
⊢ ∀ (a b : R), a < x → x < b → ∃ (i' : Set R), (i' ∈ 𝓝 x ∧ Convex R i') ∧ i' ⊆ Ioo a b

Tactic:
exact fun _ _ h₁ h₂ ↦ ⟨_, by simp [h₁, h₂, Ioo_mem_nhds, convex_Ioo], subset_rfl⟩
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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' : Set R), i' ∈ 𝓝 x ∧ Convex R i' → id i' ∈ 𝓝 x

Tactic:
simp +contextual
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
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
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ∀ y ∈ [x₀ -[𝕜] x], p y

Tactic:
rw [eventually_nhdsWithin_iff, (LocallyConvexSpace.convex_basis (𝕜 := 𝕜) x₀).eventually_iff]
    at h ⊢

Premises used: eventually_nhdsWithin_iff, Filter.HasBasis.eventually_iff, LocallyConvexSpace.convex_basis
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
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
⊢ ∃ (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
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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

Tactic:
⟨u, ⟨hu_nhds, hu_convex⟩, fun x hxu hxs y hy ↦ h ?_ (hs.segment_subset hx₀s hxs hy)⟩

Premises used: And.intro, Exists.intro, Convex.segment_subset
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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
refine : ∀ (x : E) (hxu : x ∈ id u) (hxs : x ∈ s) (y : E) (hy : y ∈ [x₀ -[𝕜] x]), y ∈ id u
⊢ ∃ (i : Set E), (i ∈ 𝓝 x₀ ∧ Convex 𝕜 i) ∧ ∀ ⦃x : E⦄, x ∈ id i → x ∈ s → ∀ y ∈ [x₀ -[𝕜] x], p y

Tactic:
refine ⟨u, ⟨hu_nhds, hu_convex⟩, fun x hxu hxs y hy ↦ h ?_ (hs.segment_subset hx₀s hxs hy)⟩
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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]
suffices : [x₀ -[𝕜] x] ⊆ u
⊢ y ∈ id u

Tactic:
suffices segment 𝕜 x₀ x ⊆ u from this hy
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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]
⊢ [x₀ -[𝕜] x] ⊆ u

Tactic:
hu_convex.segment_subset (mem_of_mem_nhds hu_nhds) hxu

Premises used: mem_of_mem_nhds, Convex.segment_subset
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
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]
⊢ [x₀ -[𝕜] x] ⊆ u

Tactic:
exact hu_convex.segment_subset (mem_of_mem_nhds hu_nhds) hxu

Premises used: mem_of_mem_nhds, Convex.segment_subset
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
A : Type u_2
inst_1 : Add A
inst_2 : SMul R A
τA : TopologicalSpace A
inst_3 : IsModuleTopology R A
⊢ τA = moduleTopology R A

Tactic:
IsModuleTopology.eq_moduleTopology' (R := R) (A := A)

Premises used: IsModuleTopology.eq_moduleTopology'
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R_1 : Type u_1
inst : TopologicalSpace R_1
A_1 : Type u_2
inst_1 : Add A_1
inst_2 : SMul R_1 A_1
R : Type u_3
inst_3 : TopologicalSpace R
A : Type u_4
inst_4 : Add A
inst_5 : SMul R A
⊢ IsModuleTopology R A

Tactic:
letI := moduleTopology R A; ⟨rfl⟩

Premises used: IsModuleTopology.mk, rfl
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
A : Type u_2
inst_1 : Add A
inst_2 : SMul R A
⊢ ContinuousSMul R A

Tactic:
continuousSMul_sInf fun _ h ↦ h.1

Premises used: continuousSMul_sInf, And.left
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
A : Type u_2
inst_1 : Add A
inst_2 : SMul R A
⊢ ContinuousAdd A

Tactic:
continuousAdd_sInf fun _ h ↦ h.2

Premises used: continuousAdd_sInf, And.right
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
A : Type u_2
inst_1 : Add A
inst_2 : SMul R A
inst_3 : TopologicalSpace A
inst_4 : IsModuleTopology R A
⊢ ContinuousSMul R A

Tactic:
eq_moduleTopology R A ▸ ModuleTopology.continuousSMul R A

Premises used: ModuleTopology.continuousSMul, Eq.rec, eq_moduleTopology, Eq.symm
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
A : Type u_2
inst_1 : Add A
inst_2 : SMul R A
inst_3 : TopologicalSpace A
inst_4 : IsModuleTopology R A
⊢ ContinuousAdd A

Tactic:
eq_moduleTopology R A ▸ ModuleTopology.continuousAdd R A

Premises used: Eq.rec, eq_moduleTopology, ModuleTopology.continuousAdd, Eq.symm
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
A : Type u_2
inst_1 : Add A
inst_2 : SMul R A
τA : TopologicalSpace A
inst_3 : ContinuousSMul R A
inst_4 : ContinuousAdd A
⊢ moduleTopology R A ≤ τA

Tactic:
sInf_le ⟨inferInstance, inferInstance⟩

Premises used: inferInstance, sInf_le, And.intro
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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)
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'})
⊢ τB' = moduleTopology S B'

Tactic:
simp_rw [e.toHomeomorph.symm.isInducing.1, eq_moduleTopology R A, moduleTopology, induced_sInf]

Premises used: Homeomorph.isInducing, induced_sInf, moduleTopology, eq_moduleTopology, Homeomorph.symm, ContinuousLinearEquiv.toHomeomorph, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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)
h₁ :
  Eq.{u_5 + 1} (α := Set (TopologicalSpace B'))
    (Set.image.{u_3, u_5} (α := TopologicalSpace A) (TopologicalSpace.induced (⇑e.toHomeomorph.symm : (a : B') → A))
      {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A})
    {t : TopologicalSpace B' | ContinuousSMul S B' ∧ ContinuousAdd B'}
⊢ 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:
apply congr_arg

Premises used: congr_arg