mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case inr.inl
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht₁ : Convex ℝ ∅
ht₃ : IsOpen ∅
disj : Disjoint s ∅
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ ∅, u < f b

pp: case inr.inr
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u < f b

Tactic:
·

Goal state after:
case inr.inl
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht₁ : Convex ℝ ∅
ht₃ : IsOpen ∅
disj : Disjoint s ∅
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ ∅, u < f b
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ gauge (ball 0 r) x = ‖x‖ / r

Tactic:
·

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ gauge (ball 0 r) x = ‖x‖ / r
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ gauge (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 0) x = 0 x

Tactic:
simp only [← singleton_zero, gauge_def', mem_closure_zero_iff_norm, norm_smul, mul_eq_zero,
    norm_eq_zero, inv_eq_zero]

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x

pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : 0 < ‖x‖
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x

Tactic:
·

Goal state after:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : 0 < ‖x‖
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x

Tactic:
·

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : 0 < ‖x‖
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hr : 0 ≤ 0
⊢ gauge (closedBall 0 0) x = ‖x‖ / 0

pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ gauge (closedBall 0 r) x = ‖x‖ / r

Tactic:
·

Goal state after:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hr : 0 ≤ 0
⊢ gauge (closedBall 0 0) x = ‖x‖ / 0
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ gauge (closedBall 0 r) x = ‖x‖ / r

Tactic:
·

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ gauge (closedBall 0 r) x = ‖x‖ / r
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr.a
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ gauge (closedBall 0 r) x ≤ ‖x‖ / r

pp: case a
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ ‖x‖ / r ≤ gauge (closedBall 0 r) x

Tactic:
·

Goal state after:
case inr.a
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ gauge (closedBall 0 r) x ≤ ‖x‖ / r
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case a
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ ‖x‖ / r ≤ gauge (closedBall 0 r) x

Tactic:
·

Goal state after:
case a
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ ‖x‖ / r ≤ gauge (closedBall 0 r) x
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : r ≤ 0
⊢ r * gauge s x ≤ ‖x‖

pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : 0 < r
⊢ r * gauge s x ≤ ‖x‖

Tactic:
·

Goal state after:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : r ≤ 0
⊢ r * gauge s x ≤ ‖x‖
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case refine_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, f a < u
hfB : ∀ b ∈ t, u ≤ f b
⊢ f ≠ 0

pp: case refine_2
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, f a < u
hfB : ∀ b ∈ t, u ≤ f b
a : E
ha : a ∈ s
⊢ f a ≤ u

Tactic:
·

Goal state after:
case refine_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, f a < u
hfB : ∀ b ∈ t, u ≤ f b
⊢ f ≠ 0
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 ↑r ⊆ s
this : Absorbent ℝ (ball 0 ↑r)
x y : E
⊢ gauge s y + gauge s (x - y) ≤ gauge s y + ‖x - y‖ / ↑r

Tactic:
gauge_mono this hs (x - y),

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 ↑r ⊆ s
this : Absorbent ℝ (ball 0 ↑r)
x y : E
⊢ gauge s y + gauge (ball 0 ↑r) (x - y) ≤ gauge s y + ‖x - y‖ / ↑r
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case refine_2
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, f a < u
hfB : ∀ b ∈ t, u ≤ f b
a : E
ha : a ∈ s
⊢ f a ≤ u

Tactic:
·

Goal state after:
case refine_2
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, f a < u
hfB : ∀ b ∈ t, u ≤ f b
a : E
ha : a ∈ s
⊢ f a ≤ u
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case pos
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
⊢ ∃ f u, (∀ a ∈ s, f a ≤ u) ∧ ∀ b ∈ t, u ≤ f b

pp: case neg
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : ¬t.Nonempty
⊢ ∃ f u, (∀ a ∈ s, f a ≤ u) ∧ ∀ b ∈ t, u ≤ f b

Tactic:
·

Goal state after:
case pos
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
⊢ ∃ f u, (∀ a ∈ s, f a ≤ u) ∧ ∀ b ∈ t, u ≤ f b
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
inst✝⁹ : Field R
inst✝⁸ : AddCommGroup V
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : Module R V
inst✝³ : SeparatingDual R V
W : Type u_3
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : FiniteDimensional R W
f : W →ₗ[R] V
hf : Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap)
⊢ Injective ⇑f

pp: case mpr
R : Type u_1
V : Type u_2
inst✝⁹ : Field R
inst✝⁸ : AddCommGroup V
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : Module R V
inst✝³ : SeparatingDual R V
W : Type u_3
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : FiniteDimensional R W
f : W →ₗ[R] V
hf : Injective ⇑f
⊢ Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap)

Tactic:
·

Goal state after:
case mp
R : Type u_1
V : Type u_2
inst✝⁹ : Field R
inst✝⁸ : AddCommGroup V
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : Module R V
inst✝³ : SeparatingDual R V
W : Type u_3
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : FiniteDimensional R W
f : W →ₗ[R] V
hf : Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap)
⊢ Injective ⇑f
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case neg
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : ¬t.Nonempty
⊢ ∃ f u, (∀ a ∈ s, f a ≤ u) ∧ ∀ b ∈ t, u ≤ f b

Tactic:
·

Goal state after:
case neg
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : ¬t.Nonempty
⊢ ∃ f u, (∀ a ∈ s, f a ≤ u) ∧ ∀ b ∈ t, u ≤ f b
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: case inl
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y ≠ 0
⊢ ∃ f, f x = 1 ∧ f y ≠ 0

pp: case inr
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y = 0
⊢ ∃ f, f x = 1 ∧ f y ≠ 0

Tactic:
·

Goal state after:
case inl
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y ≠ 0
⊢ ∃ f, f x = 1 ∧ f y ≠ 0
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case inl
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
t : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
ht₁ : Convex ℝ t
ht₂ : IsClosed t
hs₁ : Convex ℝ ∅
hs₂ : IsCompact ∅
disj : Disjoint ∅ t
⊢ ∃ f u v, (∀ a ∈ ∅, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b

pp: case inr
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
⊢ ∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b

Tactic:
·

Goal state after:
case inl
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
t : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
ht₁ : Convex ℝ t
ht₂ : IsClosed t
hs₁ : Convex ℝ ∅
hs₂ : IsCompact ∅
disj : Disjoint ∅ t
⊢ ∃ f u v, (∀ a ∈ ∅, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: case inr.inl
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y = 0
v : StrongDual R V
vy : v y = 1
vx : v x ≠ 0
⊢ ∃ f, f x = 1 ∧ f y ≠ 0

pp: case inr.inr
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y = 0
v : StrongDual R V
vy : v y = 1
vx : v x = 0
⊢ ∃ f, f x = 1 ∧ f y ≠ 0

Tactic:
·

Goal state after:
case inr.inl
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y = 0
v : StrongDual R V
vy : v y = 1
vx : v x ≠ 0
⊢ ∃ f, f x = 1 ∧ f y ≠ 0
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: case inr.inr
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y = 0
v : StrongDual R V
vy : v y = 1
vx : v x = 0
⊢ ∃ f, f x = 1 ∧ f y ≠ 0

Tactic:
·

Goal state after:
case inr.inr
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y = 0
v : StrongDual R V
vy : v y = 1
vx : v x = 0
⊢ ∃ f, f x = 1 ∧ f y ≠ 0
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case inr.inl
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
hs : s.Nonempty
ht₁ : Convex ℝ ∅
ht₂ : IsClosed ∅
disj : Disjoint s ∅
⊢ ∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ ∅, v < f b

pp: case inr.inr
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
⊢ ∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b

Tactic:
·

Goal state after:
case inr.inl
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
hs : s.Nonempty
ht₁ : Convex ℝ ∅
ht₂ : IsClosed ∅
disj : Disjoint s ∅
⊢ ∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ ∅, v < f b
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
h𝕜 : SecondCountableTopology 𝕜
⊢ StronglyMeasurable (deriv f)

pp: case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hF : SecondCountableTopology F
⊢ StronglyMeasurable (deriv f)

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
h𝕜 : SecondCountableTopology 𝕜
⊢ StronglyMeasurable (deriv f)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hF : SecondCountableTopology F
⊢ StronglyMeasurable (deriv f)

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hF : SecondCountableTopology F
⊢ StronglyMeasurable (deriv f)
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
⊢ ∀ (m : R) (x_1 : V), m • x_1 + G (m • x_1) • (y - x) = (RingHom.id R) m • (x_1 + G x_1 • (y - x))

Tactic:
simp [smul_smul]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, f a ≤ u
hB' : ∀ b ∈ t, u ≤ f b
hzero : StrongDual.extendRCLikeₗ f = 0
⊢ False

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, f a ≤ u
hB' : ∀ b ∈ t, u ≤ f b
⊢ ∀ a ∈ s, re ((StrongDual.extendRCLikeₗ f) a) ≤ u

pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, f a ≤ u
hB' : ∀ b ∈ t, u ≤ f b
⊢ ∀ b ∈ t, u ≤ re ((StrongDual.extendRCLikeₗ f) b)

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, f a ≤ u
hB' : ∀ b ∈ t, u ≤ f b
hzero : StrongDual.extendRCLikeₗ f = 0
⊢ False
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + G z • (y - x) + ((G y)⁻¹ * (G z * G y)) • (x - y) = z

Tactic:
rw [mul_comm (G z), ← mul_assoc, inv_mul_cancel₀ Gy]

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + G z • (y - x) + (1 * G z) • (x - y) = z
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, f a ≤ u
hB' : ∀ b ∈ t, u ≤ f b
⊢ ∀ a ∈ s, re ((StrongDual.extendRCLikeₗ f) a) ≤ u

pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, f a ≤ u
hB' : ∀ b ∈ t, u ≤ f b
⊢ ∀ b ∈ t, u ≤ re ((StrongDual.extendRCLikeₗ f) b)

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, f a ≤ u
hB' : ∀ b ∈ t, u ≤ f b
⊢ ∀ a ∈ s, re ((StrongDual.extendRCLikeₗ f) a) ≤ u