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

Goal state before:
pp: case inr.inr.inr.inr
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 : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : 0 < ty
hz0 : 0 < tz
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
·

Goal state after:
case inr.inr.inr.inr
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 : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : 0 < ty
hz0 : 0 < tz
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: case inl
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
⊢ ∃ f, (∀ x ∈ C, 0 ≤ f x) ∧ ∀ x ∈ ∅, f x < 0

pp: case inr
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, (∀ x ∈ C, 0 ≤ f x) ∧ ∀ x ∈ K, f x < 0

Tactic:
·

Goal state after:
case inl
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
⊢ ∃ f, (∀ x ∈ C, 0 ≤ f x) ∧ ∀ x ∈ ∅, f x < 0
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inl
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 : y -ᵥ x = 0
⊢ Wbtw R x y z ∨ Wbtw R x z y

pp: case inr.inl
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 : z -ᵥ x = 0
⊢ Wbtw R x y z ∨ Wbtw R x z y

pp: case inr.inr
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)
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
·

Goal state after:
case inl
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 : y -ᵥ x = 0
⊢ Wbtw R x y z ∨ Wbtw R x z y
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inr.inl
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 : z -ᵥ x = 0
⊢ Wbtw R x y z ∨ Wbtw R x z y

pp: case inr.inr
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)
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
·

Goal state after:
case inr.inl
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 : z -ᵥ x = 0
⊢ Wbtw R x y z ∨ Wbtw R x z y
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inr.inr.inr
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)
this : ∀ {y z : P} (r₁ r₂ : R), 0 < r₁ → 0 < r₂ → r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x) → r₂ ≤ r₁ → Wbtw R x y z ∨ Wbtw R x z y
hr : ¬r₂ ≤ r₁
⊢ Wbtw R x y z ∨ Wbtw R x z y

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₁
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
·

Goal state after:
case inr.inr.inr
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)
this : ∀ {y z : P} (r₁ r₂ : R), 0 < r₁ → 0 < r₂ → r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x) → r₂ ≤ r₁ → Wbtw R x y z ∨ Wbtw R x z y
hr : ¬r₂ ≤ r₁
⊢ Wbtw R x y z ∨ Wbtw R x z y
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: case refine_1
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 : H ⊗[R] G
⊢ (∃ x,
      (∀ φ ∈ dual (Dual.eval R G) ↑C₁, ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) x) ∧
        ↑(TensorProduct.comm R G H) x = z) →
    ∀ φ ∈ dual (Dual.eval R H) ↑C₂, ∀ ψ ∈ dual (Dual.eval R G) ↑C₁, 0 ≤ ((dualDistrib R H G) (φ ⊗ₜ[R] ψ)) z

pp: case refine_2
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 : H ⊗[R] G
hz : ∀ φ ∈ dual (Dual.eval R H) ↑C₂, ∀ ψ ∈ dual (Dual.eval R G) ↑C₁, 0 ≤ ((dualDistrib R H G) (φ ⊗ₜ[R] ψ)) z
⊢ ∀ φ ∈ dual (Dual.eval R G) ↑C₁,
    ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) ((TensorProduct.comm R H G) z)

Tactic:
·

Goal state after:
case refine_1
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 : H ⊗[R] G
⊢ (∃ x,
      (∀ φ ∈ dual (Dual.eval R G) ↑C₁, ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) x) ∧
        ↑(TensorProduct.comm R G H) x = z) →
    ∀ φ ∈ dual (Dual.eval R H) ↑C₂, ∀ ψ ∈ dual (Dual.eval R G) ↑C₁, 0 ≤ ((dualDistrib R H G) (φ ⊗ₜ[R] ψ)) z
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: case refine_2
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 : H ⊗[R] G
hz : ∀ φ ∈ dual (Dual.eval R H) ↑C₂, ∀ ψ ∈ dual (Dual.eval R G) ↑C₁, 0 ≤ ((dualDistrib R H G) (φ ⊗ₜ[R] ψ)) z
⊢ ∀ φ ∈ dual (Dual.eval R G) ↑C₁,
    ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) ((TensorProduct.comm R H G) z)

Tactic:
·

Goal state after:
case refine_2
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 : H ⊗[R] G
hz : ∀ φ ∈ dual (Dual.eval R H) ↑C₂, ∀ ψ ∈ dual (Dual.eval R G) ↑C₁, 0 ≤ ((dualDistrib R H G) (φ ⊗ₜ[R] ψ)) z
⊢ ∀ φ ∈ dual (Dual.eval R G) ↑C₁,
    ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) ((TensorProduct.comm R H G) z)
Module: Mathlib.Analysis.Convex.Cone.TensorProduct

Goal state before:
pp: case refine_1
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
i : ↑s
x✝ : i ∈ Finset.univ
⊢ b i ∈ C₁

pp: case refine_2
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
i : ↑s
x✝ : i ∈ Finset.univ
⊢ ((equivFinsuppOfBasisLeft b) z) i ∈ ↑C₂

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
i : ↑s
x✝ : i ∈ Finset.univ
⊢ b i ∈ C₁
Module: Mathlib.Analysis.Convex.Cone.TensorProduct

Goal state before:
pp: case refine_2
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
i : ↑s
x✝ : i ∈ Finset.univ
⊢ ((equivFinsuppOfBasisLeft b) z) i ∈ ↑C₂

Tactic:
·

Goal state after:
case refine_2
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
i : ↑s
x✝ : i ∈ Finset.univ
⊢ ((equivFinsuppOfBasisLeft b) z) i ∈ ↑C₂
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E},
    s ∈ 𝓝 x → x = 0 → ∃ b, x ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s
hx : ¬x = 0
⊢ ∃ b, x ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s

pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x✝ : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
hx : x = 0
⊢ ∃ b, x ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s

Tactic:
·

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E},
    s ∈ 𝓝 x → x = 0 → ∃ b, x ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s
hx : ¬x = 0
⊢ ∃ b, x ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s
Module: Mathlib.Analysis.Convex.Extrema

Goal state before:
pp: case inl
β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
hc : a ∈ Icc a b
⊢ f a ≤ f a

pp: case inr
β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
⊢ f a ≤ f c

Tactic:
·

Goal state after:
case inl
β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
hc : a ∈ Icc a b
⊢ f a ≤ f a
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∃ l a, ∅ = {x | x ∈ A ∧ a ≤ l x}

pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : Nontrivial 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hB : B.Nonempty
⊢ ∃ l a, B = {x | x ∈ A ∧ a ≤ l x}

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∃ l a, ∅ = {x | x ∈ A ∧ a ≤ l x}
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
⊢ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x} ∩ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x} ⊆
    {x | x ∈ A ∧ ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x}

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
⊢ {x | x ∈ A ∧ ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x} ⊆
    {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x} ∩ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
⊢ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x} ∩ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x} ⊆
    {x | x ∈ A ∧ ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x}
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: case refine_2.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
x : E
hxA : x ∈ A
hx : ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x
y : E
hy : y ∈ A
⊢ l₁ y ≤ l₁ x

pp: case refine_2.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
x : E
hxA : x ∈ A
hx : ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x
y : E
hy : y ∈ A
⊢ l₂ y ≤ l₂ x

Tactic:
·

Goal state after:
case refine_2.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
x : E
hxA : x ∈ A
hx : ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x
y : E
hy : y ∈ A
⊢ l₁ y ≤ l₁ x
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: case refine_2.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
x : E
hxA : x ∈ A
hx : ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x
y : E
hy : y ∈ A
⊢ l₂ y ≤ l₂ x

Tactic:
·

Goal state after:
case refine_2.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
x : E
hxA : x ∈ A
hx : ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x
y : E
hy : y ∈ A
⊢ l₂ y ≤ l₂ x
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case refine_1
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
hcnorm : range ⇑c ⊆ closedBall 0 (cnorm + 1)
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
hdnorm : range ⇑d ⊆ closedBall 0 (ε / 2)
⊢ 0 ∈ interior ((convexHull ℝ) (range ⇑d))

pp: case refine_2
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
hcnorm : range ⇑c ⊆ closedBall 0 (cnorm + 1)
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
hdnorm : range ⇑d ⊆ closedBall 0 (ε / 2)
⊢ (convexHull ℝ) (range ⇑d) ⊆ s

Tactic:
·

Goal state after:
case refine_1
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
hcnorm : range ⇑c ⊆ closedBall 0 (cnorm + 1)
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
hdnorm : range ⇑d ⊆ closedBall 0 (ε / 2)
⊢ 0 ∈ interior ((convexHull ℝ) (range ⇑d))
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : gauge t x = 0
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x

pp: case neg
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : ¬gauge t x = 0
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : gauge t x = 0
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x