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

Goal state before:
pp: E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun x ↦ x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
l : StrongDual ℝ E
hl : l y < l x
z : E
hzt : z ∈ t
hz : IsMaxOn (⇑l) t z
h : IsExposed ℝ t {z | z ∈ t ∧ ∀ w ∈ t, l w ≤ l z}
⊢ False

Tactic:
rw [ht.eq_of_ge (y := ({ z ∈ t | ∀ w ∈ t, l w ≤ l z }))
      ⟨⟨z, hzt, hz⟩, h.isClosed htclos, hst.trans h.isExtreme⟩ (t.sep_subset _)] at hyB

Goal state after:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun x ↦ x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyx : ¬y = x
l : StrongDual ℝ E
hyB : y ∈ {z | z ∈ t ∧ ∀ w ∈ t, l w ≤ l z}
hl : l y < l x
z : E
hzt : z ∈ t
hz : IsMaxOn (⇑l) t z
h : IsExposed ℝ t {z | z ∈ t ∧ ∀ w ∈ t, l w ≤ l z}
⊢ False
Module: Mathlib.Analysis.Convex.KreinMilman

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw : f x ∈ ⇑f '' s ∧ ∀ x₁ ∈ ⇑f '' s, ∀ x₂ ∈ ⇑f '' s, f x ∈ openSegment ℝ x₁ x₂ → x₁ = f x ∧ x₂ = f x
ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}
ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty
hyt :
  ∀ ⦃x₁ : E⦄,
    x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} →
      ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this : (fun a ↦ f a) '' openSegment ℝ y z = openSegment ℝ (f y) (f z)
⊢ f x ∈ (fun a ↦ f a) '' openSegment ℝ y z

Tactic:
exact mem_image_of_mem _ hxyz

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x y : M
s t : Set M
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
⊢ IsStarConvexSet R (x + y) (s + t)

Tactic:
rw [← Set.add_image_prod]; exact (hs.prod ht).image (by fun_prop)

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ ∀ (I : Finset ↑F), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, ↑i).Nonempty

Tactic:
intro G _

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset ↑F
a✝ : #G ≤ finrank 𝕜 E + 1
⊢ (⋂ i ∈ G, ↑i).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
s : Set (Sym2 V)
⊢ (fromEdgeSet s).edgeSet = s \ Sym2.diagSet

Tactic:
ext e

Goal state after:
V : Type u
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ (fromEdgeSet s).edgeSet ↔ e ∈ s \ Sym2.diagSet
Module: Mathlib.Analysis.Convex.Strict.Extreme

Goal state before:
pp: a b : ℝ
hab : a ≤ b
⊢ extremePoints ℝ (closedBall ((a + b) / 2) ((b - a) / 2)) = {a, b}

Tactic:
StrictConvexSpace.extremePoints_closedBall_eq_sphere

Goal state after:
a b : ℝ
hab : a ≤ b
⊢ sphere ((a + b) / 2) ((b - a) / 2) = {a, b}
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.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
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x -ᵥ p₁' = 0
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
case mp.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
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.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
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x -ᵥ p₁' = 0
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
case mp.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
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Module: Mathlib.Analysis.Convex.Side

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
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)
h : y -ᵥ p₂ = 0
⊢ False

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
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
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)
h : y = p₂
⊢ False
Module: Mathlib.Analysis.Convex.Side

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
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
h : y -ᵥ p₂ = 0
⊢ False

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
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
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (y -ᵥ p₂) (p₃ -ᵥ z)
h : y = p₂
⊢ False
Module: Mathlib.Analysis.Convex.Side

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
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
h : p₂ -ᵥ y = 0
⊢ False

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
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
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
h : p₂ = y
⊢ False
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
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
s : AffineSubspace R P
x y : P
hs : s.WSameSide x y
ho : s.WOppSide y x
h : ¬(x ∈ s ∨ y ∈ s)
⊢ False

Tactic:
rw [not_or] at h

Goal state after:
case mp
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
s : AffineSubspace R P
x y : P
hs : s.WSameSide x y
ho : s.WOppSide y x
h : x ∉ s ∧ y ∉ s
⊢ False
Module: Mathlib.Analysis.Convex.Side

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
s : AffineSubspace R P
x y : P
h : s.WSameSide x y
⊢ ¬s.SOppSide x y

Tactic:
intro ho

Goal state after:
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
s : AffineSubspace R P
x y : P
h : s.WSameSide x y
ho : s.SOppSide x y
⊢ False
Module: Mathlib.Analysis.Convex.Side

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
s : AffineSubspace R P
x y : P
h : s.SSameSide x y
⊢ ¬s.WOppSide x y

Tactic:
intro ho

Goal state after:
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
s : AffineSubspace R P
x y : P
h : s.SSameSide x y
ho : s.WOppSide x y
⊢ False
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points) w ≠ s.points i
⊢ ∃ i, w i ≠ 0

Tactic:
by
    by_contra! hij
    simp_all

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

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
s : AffineSubspace R P
x y p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p₁ = 0
⊢ ∃ p ∈ s, Wbtw R x p y

Tactic:
vsub_eq_zero_iff_eq

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
s : AffineSubspace R P
x y p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : x = p₁
⊢ ∃ p ∈ s, Wbtw R x p y
Module: Mathlib.Analysis.Convex.Side

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
s : AffineSubspace R P
x y p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ -ᵥ y = 0
⊢ ∃ p ∈ s, Wbtw R x p y

Tactic:
vsub_eq_zero_iff_eq

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
s : AffineSubspace R P
x y p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ = y
⊢ ∃ p ∈ s, Wbtw R x p y
Module: Mathlib.Analysis.Convex.Side

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
s : AffineSubspace R P
x z : P
hx : x ∉ s
hz : z ∈ s
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
hy : 1 • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z) 1 ≠ x
hyz : (lineMap x z) 1 ≠ z
⊢ False

Tactic:
simp [lineMap_apply] at hyz

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

Goal state before:
pp: case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y -ᵥ p₂ = 0
⊢ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y = p₂
⊢ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : y -ᵥ p₂ = 0
⊢ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : y = p₂
⊢ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mpr
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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
t : R
ht : 0 < t
p' : P
hp' : p' ∈ ↑s
⊢ s.SSameSide x (t • (x -ᵥ p) +ᵥ p')

Tactic:
exact sSameSide_smul_vsub_vadd_right hx hp hp' ht

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

Goal state before:
pp: case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : p₂ -ᵥ y = 0
⊢ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : p₂ = y
⊢ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.Analysis.Convex.Visible

Goal state before:
pp: case refine_1
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this : 0 < 1 - ε
hwi : 0 < 1 - w i
⊢ (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1) ≤ 1

pp: case refine_2
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this : 0 < 1 - ε
hwi : 0 < 1 - w i
⊢ (lineMap ((lineMap x (a i)) ε) (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j))
      ((1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) =
    (lineMap x (∑ j ∈ t, w j • a j)) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹))

Tactic:
· refine (div_le_one <| by positivity).2 ?_
        calc
          (1 - w i) / w i = 0 + (1 - w i) / w i + 0 := by simp
          _ ≤ (1 - ε) / ε + (1 - w i) / w i + 1 := by gcongr <;> positivity

Goal state after:
case refine_2
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this : 0 < 1 - ε
hwi : 0 < 1 - w i
⊢ (lineMap ((lineMap x (a i)) ε) (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j))
      ((1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) =
    (lineMap x (∑ j ∈ t, w j • a j)) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹))
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ -ᵥ y = 0
⊢ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
vsub_eq_zero_iff_eq

Goal state after:
case mp.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
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ = y
⊢ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ ‖holder r B f g‖₊ ≤ ‖B‖₊ * ‖f‖₊ * ‖g‖₊

Tactic:
simp_rw [← ENNReal.coe_le_coe, ENNReal.coe_mul, ← enorm_eq_nnnorm, Lp.enorm_def]

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ eLpNorm (↑↑(holder r B f g)) r μ ≤ ‖B‖ₑ * eLpNorm (↑↑f) p μ * eLpNorm (↑↑g) q μ
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case refine_1
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✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
h :
  (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
⊢ SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∧ w₁ i ≠ 0

Tactic:
have h0 : w₁ i ≠ 0 :=
      (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.1 h.left_notMem

Goal state after:
case refine_1
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✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
h :
  (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
h0 : w₁ i ≠ 0
⊢ SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∧ w₁ i ≠ 0