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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ∧ y -ᵥ p ≠ x -ᵥ p ∧ y -ᵥ p ≠ z -ᵥ p ↔ Sbtw R x y z

Tactic:
Sbtw,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ∧ y -ᵥ p ≠ x -ᵥ p ∧ y -ᵥ p ≠ z -ᵥ p ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s.Nonempty
𝓕 : Set (↑s → ℝ) := {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c}
hl : IsLUB 𝓕 (s.domRestrict φ)
f : ↑s → ℝ
hf : f ∈ 𝓕
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
⊢ Continuous (s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c)

Tactic:
fun_prop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : PartialOrder R
x : R
⊢ Sbtw R 0 x 1 ↔ x ∈ Set.Ioo 0 1

Tactic:
Sbtw,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : PartialOrder R
x : R
⊢ Wbtw R 0 x 1 ∧ x ≠ 0 ∧ x ≠ 1 ↔ x ∈ Set.Ioo 0 1
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ #s ≤ #(s.biUnion t)

Tactic:
rw [← card_image_of_injective s hf₁]

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ #(image f s) ≤ #(s.biUnion t)
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
x✝ : (j : J) → ↑(F.obj j)
⊢ x✝ ∈ partialSections F H ↔
    x✝ ∈ ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}

Tactic:
simp only [Set.mem_iInter, Set.mem_ofPred_eq]

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
x✝ : (j : J) → ↑(F.obj j)
⊢ x✝ ∈ partialSections F H ↔ ∀ i ∈ H, (ConcreteCategory.hom (F.map i.snd.snd.snd.snd)) (x✝ i.fst) = x✝ i.snd.fst
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: case hf
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
f : FiniteDiagramArrow G
a✝ : f ∈ ↑H
⊢ Continuous fun y ↦ (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (y f.fst)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: case hg
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
f : FiniteDiagramArrow G
a✝ : f ∈ ↑H
⊢ Continuous fun y ↦ y f.snd.fst

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) := {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c}
hl : IsLUB 𝓕 φ
f : E → ℝ
hf : f ∈ 𝓕
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = ⇑re ∘ ⇑l + const E c
⊢ Continuous (⇑re ∘ ⇑l + const E c)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
⊢ a ∈ (ofSet s) a ↔ a ∈ s

Tactic:
dsimp [ofSet]

Goal state after:
α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
⊢ (a ∈ if a ∈ s then some a else none) ↔ a ∈ s
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a b : α
⊢ a ∈ (ofSet s) b ↔ a = b ∧ a ∈ s

Tactic:
dsimp [ofSet]

Goal state after:
α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a b : α
⊢ (a ∈ if b ∈ s then some b else none) ↔ a = b ∧ a ∈ s
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AffineSpace V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
hji : j < i
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))

Tactic:
nth_rw 2 [sbtw_comm]

Goal state after:
case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AffineSpace V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
hji : j < i
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (max i j)) p (s.points (min i j))
Module: Mathlib.Analysis.Convex.Cone.Closure

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
E : Type u_2
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : SMul 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
K : ConvexCone 𝕜 E
c : 𝕜
hc : 0 < c
x✝ : E
h₁ : x✝ ∈ closure ↑K
⊢ Continuous (HSMul.hSMul c)

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁹ : AddCommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Semifield 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : DenselyOrdered 𝕜
inst✝¹ : NoMaxOrder 𝕜
inst✝ : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed ↑C
x : E
hx : x ∈ ↑C
f : 𝕜 → E := fun x_1 ↦ x_1 • x
hfS : closure (f '' Ioi 0) ⊆ ↑C
⊢ ContinuousWithinAt f (Ioi 0) 0

Tactic:
fun_prop

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 ∘ ⇑{ toFun := ![i, j, k], inj' := h })
⊢ ¬Wbtw R (T i) (T j) (T k)

Tactic:
affineIndependent_iff_not_collinear

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
ι : Type u_6
i j k : ι
h : Function.Injective ![i, j, k]
T : ι → P
hT : ¬Collinear R (Set.range (T ∘ ⇑{ toFun := ![i, j, k], inj' := h }))
⊢ ¬Wbtw R (T i) (T j) (T k)
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
hp : Injective ⇑p.flip
⊢ dual p univ = 0

Tactic:
by
  refine le_antisymm (fun y hy ↦ (map_eq_zero_iff p.flip hp).1 ?_) (by simp)
  ext x
  exact (hy <| mem_univ x).antisymm' <| by simpa using hy <| mem_univ (-x)

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : PartialOrder β
inst✝⁷ : TopologicalSpace β
inst✝⁶ : OrderClosedTopology β
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : SMul 𝕜 α
inst✝² : SMul 𝕜 β
inst✝¹ : ContinuousConstSMul 𝕜 β
inst✝ : ContinuousAdd β
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Continuous[Pi.topologicalSpace, inst✝⁷] fun x_1 ↦ x_1 (a • x + b • y)

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : PartialOrder β
inst✝⁷ : TopologicalSpace β
inst✝⁶ : OrderClosedTopology β
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : SMul 𝕜 α
inst✝² : SMul 𝕜 β
inst✝¹ : ContinuousConstSMul 𝕜 β
inst✝ : ContinuousAdd β
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Continuous[Pi.topologicalSpace, inst✝⁷] fun x_1 ↦ a • x_1 x + b • x_1 y

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : 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 B C : Set E
hB : IsExposed 𝕜 A B
hC : IsExposed 𝕜 A C
⊢ IsExposed 𝕜 A (B ∩ C)

Tactic:
rintro ⟨w, hwB, hwC⟩
  obtain ⟨l₁, rfl⟩ := hB ⟨w, hwB⟩
  obtain ⟨l₂, rfl⟩ := hC ⟨w, hwC⟩
  refine ⟨l₁ + l₂, Subset.antisymm ?_ ?_⟩
  · rintro x ⟨⟨hxA, hxB⟩, ⟨-, hxC⟩⟩
    exact ⟨hxA, fun z hz => add_le_add (hxB z hz) (hxC z hz)⟩
  rintro x ⟨hxA, hx⟩
  refine ⟨⟨hxA, fun y hy => ?_⟩, hxA, fun y hy => ?_⟩
  · exact
      (add_le_add_iff_right (l₂ x)).1 ((add_le_add (hwB.2 y hy) (hwC.2 x hxA)).trans (hx w hwB.1))
  · exact
      (add_le_add_iff_left (l₁ x)).1 (le_trans (add_le_add (hwB.2 x hxA) (hwC.2 y hy)) (hx w hwB.1))

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
x : E
hx : x ∈ s
⊢ x ∈ interior ((convexHull ℝ) (range ⇑b)) + {x}

Tactic:
by simpa using hb₁

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
this : s.Nonempty
⊢ x ∈ s

Tactic:
Subsingleton.mem_iff_nonempty

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
this : s.Nonempty
⊢ s.Nonempty
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ s ⊆ interior ((convexHull ℝ) (range ⇑b + ↑u))

Tactic:
convexHull_add

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ s ⊆ interior ((convexHull ℝ) (range ⇑b) + (convexHull ℝ) ↑u)
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ (convexHull ℝ) (range ⇑b + ↑u) ⊆ t

Tactic:
convexHull_add

Goal state after:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ (convexHull ℝ) (range ⇑b) + (convexHull ℝ) ↑u ⊆ t
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun x1 x2 ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C

Tactic:
have h : ContinuousAt (fun δ : ℝ ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0 := by
        fun_prop (disch := norm_num)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun x1 x2 ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
h : ContinuousAt (fun δ ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
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
hAconv : Convex ℝ s
⊢ s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))

Tactic:
by_contra hs

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
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))
⊢ False
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed[instTopologicalSpaceSubtype]
    (Subtype.val ⁻¹' Subtype.val '' closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s))

Tactic:
preimage_image_eq _ Subtype.coe_injective

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed[instTopologicalSpaceSubtype] (closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s))
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht : f t ∈ Set.Ioo 0 1
⊢ Continuous fun i ↦ ⟨f ↑i, ⋯⟩

Tactic:
fun_prop

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
⊢ IsAffineMap R fun x ↦ x.1 + x.2

Tactic:
fun_prop

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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x : M
s : Set M
hs : IsStarConvexSet R x s
⊢ IsStarConvexSet R (-x) (-s)

Tactic:
← Set.image_neg_eq_neg

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x : M
s : Set M
hs : IsStarConvexSet R x s
⊢ IsStarConvexSet R (-x) ((fun x ↦ -x) '' s)
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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x : M
s : Set M
hs : IsStarConvexSet R x s
⊢ IsAffineMap R Neg.neg

Tactic:
fun_prop

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✝³ : AddCommGroup 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
⊢ IsAffineMap R fun x ↦ x.1 - x.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
hs' : s ∈ K.faces → ∃ t ∈ K.faces, s ⊆ t ∧ s ≠ t
t : Finset E
ht : t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t ∈ K.faces, s ⊂ t

Tactic:
exact ⟨t, ht.1, ⟨ht.2.1, fun hts => ht.2.2 (Subset.antisymm ht.2.1 hts)⟩⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v w : V
e : Sym2 V
ι✝ : Type u
κ✝ : ι✝ → Type u
f : (a : ι✝) → κ✝ a → SimpleGraph V
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
by ext; simp [Classical.skolem]

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

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder 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 : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ s.WOppSide y x

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩

Goal state after:
case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder 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 : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R (y -ᵥ p₂) (p₁ -ᵥ x)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder 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 : SameRay R (y -ᵥ p₁) (p₂ -ᵥ x)
⊢ s.WOppSide x y

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩

Goal state after:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder 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 : SameRay R (y -ᵥ p₁) (p₂ -ᵥ x)
⊢ 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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ s.WSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ SameRay R ((t • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (x -ᵥ p₁)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t ≤ 0
⊢ SameRay R ((t • (x -ᵥ p₁) +ᵥ p₂) -ᵥ p₂) (p₁ -ᵥ x)
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
Sbtw,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃ ∧ p₂ ≠ p₁ ∧ p₂ ≠ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)