mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ innerDual ∅ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ innerDual 0 = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
hx : x ∈ innerDual univ
⊢ x ∈ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ ⊥ ≤ innerDual univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ innerDual {x} = comap ((innerSL ℝ) x) (positive ℝ ℝ)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
s : Set E
⊢ innerDual (insert x s) = innerDual {x} ⊓ innerDual s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
ι : Sort u_4
f : ι → Set E
⊢ innerDual (⋃ i, f i) = ⨅ i, innerDual (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
S : Set (Set E)
⊢ innerDual (⋃₀ S) = sInf (innerDual '' S)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x₀ : E
C : ProperCone ℝ E
hx₀ : x₀ ∉ C
⊢ ∃ y, (∀ x ∈ C, 0 ≤ ⟪x, y⟫) ∧ ⟪x₀, y⟫ < 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
C : ProperCone ℝ E
⊢ innerDual ↑(innerDual ↑C) = C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → E
hmem : ∀ (x : ℕ), seq x ∈ C
y : F
hinner : ∀ ⦃x : E⦄, x ∈ C → 0 ≤ ⟪f x, y⟫_ℝ
hx : ∀ (x : ℕ), f (seq x) = (⇑f ∘ seq) x
htends : Filter.Tendsto (⇑f ∘ seq) Filter.atTop (nhds b)
n : ℕ
⊢ 0 ≤ ⟪f (seq n), y⟫_ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
⊢ b ∈ map f C → ∀ (y : F), (ContinuousLinearMap.adjoint f) y ∈ innerDual ↑C → 0 ≤ ⟪b, y⟫_ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ∀ (y : F), (ContinuousLinearMap.adjoint f) y ∈ innerDual ↑C → 0 ≤ ⟪b, y⟫_ℝ
⊢ b ∈ map f C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : PartialOrder R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : ClosedIciTopology R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hp : ∀ (x : M), Continuous ⇑(p x)
⊢ IsClosed ↑(dual p s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : IsOrderedRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ClosedIciTopology R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsContPerfPair
⊢ dual p ∅ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj : b ∉ map f K
⊢ ∃ y, (ContinuousLinearMap.adjoint f) y ∈ innerDual ↑K ∧ ⟪b, y⟫_ℝ < 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : IsOrderedRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ClosedIciTopology R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsContPerfPair
⊢ dual p 0 = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsOrderedRing R
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : ClosedIciTopology R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝² : p.IsContPerfPair
inst✝¹ : IsTopologicalRing R
inst✝ : T1Space N
⊢ ⊥ ≤ dual p univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsOrderedRing R
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : ClosedIciTopology R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝² : p.IsContPerfPair
inst✝¹ : IsTopologicalRing R
inst✝ : T1Space N
y : N
hy : y ∈ dual p univ
x : M
⊢ (p x) y ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsOrderedRing R
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : ClosedIciTopology R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝² : p.IsContPerfPair
inst✝¹ : IsTopologicalRing R
inst✝ : T1Space N
⊢ dual p univ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsOrderedRing R
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : ClosedIciTopology R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝² : p.IsContPerfPair
inst✝¹ : IsTopologicalRing R
inst✝ : OrderClosedTopology R
x : M
⊢ dual p {x} = comap (p.toContPerfPair x) (positive R R)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : IsOrderedRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ClosedIciTopology R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsContPerfPair
s t : Set M
⊢ dual p (s ∪ t) = dual p s ⊓ dual p t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : IsOrderedRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ClosedIciTopology R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsContPerfPair
x : M
s : Set M
⊢ dual p (insert x s) = dual p {x} ⊓ dual p s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : IsOrderedRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ClosedIciTopology R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsContPerfPair
ι : Sort u_4
f : ι → Set M
⊢ dual p (⋃ i, f i) = ⨅ i, dual p (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Collinear R {x, y, z}
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : IsOrderedRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ClosedIciTopology R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsContPerfPair
S : Set (Set M)
⊢ dual p (⋃₀ S) = sInf (dual p '' S)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
⊢ Wbtw R x y z ↔ SameRay R (y -ᵥ x) (z -ᵥ y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
C : ProperCone ℝ E
hKconv : Convex ℝ ∅
hKcomp : IsCompact ∅
hKC : Disjoint ∅ ↑C
⊢ (∀ x ∈ C, 0 ≤ 0 x) ∧ ∀ x ∈ ∅, 0 x < 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
z : G ⊗[R] H
⊢ z ∈ C₁.maxTensorProduct C₂ ↔
    ∀ φ ∈ dual (Dual.eval R G) ↑C₁, ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K ↑C
x₀ : E
hx₀ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, f a < u
huv : u < v
hv : ∀ b ∈ ↑C, v < f b
⊢ v < 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s✝ t : Set M
y : N
s : Set M
u v : N
hu : u ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}
hv : v ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}
x : M
hx : x ∈ s
⊢ 0 ≤ (p x) (u + v)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
x : G
y : H
C₁ : PointedCone R G
C₂ : PointedCone R H
hx : x ∈ C₁
hy : y ∈ C₂
⊢ x ⊗ₜ[R] y ∈ C₁.maxTensorProduct C₂

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s✝ t : Set M
y : N
s : Set M
⊢ 0 ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
⊢ C₁.minTensorProduct C₂ ≤ C₁.maxTensorProduct C₂

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
⊢ map (↑(TensorProduct.comm R G H)) (C₁.minTensorProduct C₂) = C₂.minTensorProduct C₁

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K ↑C
⊢ ∃ f, (∀ x ∈ C, 0 ≤ f x) ∧ ∀ x ∈ K, f x < 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
hr : r₂ ≤ r₁
⊢ y = r₁⁻¹ • r₂ • (z -ᵥ x) +ᵥ x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s✝ t : Set M
y✝ : N
s : Set M
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : N
hy : y ∈ {y | ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y}
x : M
hx : x ∈ s
⊢ 0 ≤ (p x) (c • y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
x₀ : E
C : ProperCone ℝ E
hx₀ : x₀ ∉ C
⊢ ∃ f, (∀ x ∈ C, 0 ≤ f x) ∧ f x₀ < 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
⊢ dual p ∅ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : SameRay R (y -ᵥ x) (z -ᵥ x)
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
⊢ dual p 0 = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module ℝ E
inst✝³ : ContinuousSMul ℝ E
inst✝² : LocallyConvexSpace ℝ E
inst✝¹ : Module ℝ F
p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ
inst✝ : p.IsContPerfPair
C : ProperCone ℝ E
⊢ dual p.flip ↑(dual p ↑C) = C

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
⊢ dual p ↑p.ker = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
ι : Type u_6
i j k : ι
h : Function.Injective ![i, j, k]
T : ι → P
hT : AffineIndependent R T
⊢ ¬Wbtw R (T i) (T j) (T k)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
x : M
⊢ dual p {x} = comap (p x) (positive R R)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ 0 ≤ 2⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ 2⁻¹ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s t : Set M
⊢ dual p (s ∪ t) = dual p s ⊓ dual p t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ Wbtw R y x ((pointReflection R x) y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.TopDualPairing

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : T2Space E
⊢ Continuous fun x ↦
    match x with
    | (x, y) => ((topDualPairing 𝕜 E) x) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ Sbtw R y x ((pointReflection R x) y)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
⊢ map (↑(TensorProduct.comm R G H)) (C₁.maxTensorProduct C₂) = C₂.maxTensorProduct C₁

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ Wbtw R x (midpoint R x y) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ midpoint R x y ≠ x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.TopDualPairing

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : T2Space E
⊢ Function.Bijective fun y ↦ { toLinearMap := (topDualPairing 𝕜 E).flip y, cont := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
x : M
s : Set M
⊢ dual p (insert x s) = dual p {x} ⊓ dual p s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ Sbtw R x (midpoint R x y) y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
ι : Sort u_4
f : ι → Set M
⊢ dual p (⋃ i, f i) = ⨅ i, dual p (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
S : Set (Set M)
⊢ dual p (⋃₀ S) = sInf (dual p '' S)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
⊢ ↑(dual p s) = ⋂ i, ↑(dual p {↑i})

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
t : Set N
⊢ s ⊆ ↑(dual p.flip t) ↔ t ⊆ ↑(dual p s)

Tactic:
by

Goal state after: