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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this : k ∈ (cons j (cons k u hk✝) ⋯).erase j
⊢ j ∈ cons j (cons k u hk✝) ⋯

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this : 0 < w j
⊢ k ∈ cons j (cons k u hk✝) ⋯

Tactic:
by

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

Goal state before:
pp: F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (‖x‖⁻¹ * ‖x‖) • x ∈ U
⊢ ‖x‖ ≠ 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
⊢ w j / c + w k / c = 1

Tactic:
by

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

Goal state before:
pp: F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
⊢ (convexHull ℝ) (sphere x r) = closedBall x r

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (Metric.thickening δ s)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (Metric.cthickening δ s)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
⊢ (convexHull R) ↑s = {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y : E
hx : x ∈ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) t
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
x : E
⊢ x ∈ (convexHull R) ↑s ↔ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
x : E
⊢ x ∈ (convexHull R) ↑s ↔ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
⊢ ediam ((convexHull ℝ) s) = ediam s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Set E
hs : s.Finite
⊢ (convexHull R) s = {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ hs.toFinset, w y = 1 ∧ hs.toFinset.centerMass w id = x}

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
⊢ diam ((convexHull ℝ) s) = diam s

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
⊢ Bornology.IsBounded ((convexHull ℝ) s) ↔ Bornology.IsBounded s

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ¬x = 0
⊢ ContinuousOn (fun r ↦ r • x) (Ici 0)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ IsConnected {y | SameRay ℝ x y}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ f (w j • p j + (w k • p k + ∑ x ∈ u, w x • p x)) = f (c • ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • p x)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : x ≠ 0
⊢ ContinuousOn (fun r ↦ r • x) (Ioi 0)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : x ≠ 0
⊢ IsConnected {y | SameRay ℝ x y ∧ y ≠ 0}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
i : ι
hi : i ∈ u
⊢ i ∈ cons j (cons k u hk✝) ⋯

Tactic:
by

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

Goal state before:
pp: case refine_1.refine_2.hz
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hz : ∀ i ∈ t, z i ∈ s
⊢ ∀ i ∈ t, z i ∈ ↑(Finset.image z t)

Tactic:
exact fun i hi => Finset.mem_coe.2 (Finset.mem_image_of_mem _ hi)

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y z : E
hy : y ∈ segment ℝ x z
⊢ ‖y - x‖ ≤ ‖z - x‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ c + ∑ i ∈ u, w i = 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ 0 ≤ c

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Set E
⊢ (convexHull R) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ j ∈ cons j (cons k u hk✝) ⋯

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
p₁ p₂ : E
⊢ vectorSpan R (segment R p₁ p₂) = R ∙ (p₂ -ᵥ p₁)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ k ∈ cons j (cons k u hk✝) ⋯

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ (w j / c) • p j + (w k / c) • p k ∈ s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module R E
inst✝² : Module R F
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i, v i • g i = y
⊢ ∑ i, w i.1 * v i.2 = 1

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝[s] x, r p.1 p.2
seg : ∀ᶠ (χ : α) in f, [y χ -[ℝ] z χ] ⊆ s
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.SeparationQuotient.Section

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul K E
f : SeparationQuotient E →ₗ[K] E
hf : mk ∘ ⇑f = id
⊢ Continuous (mk ∘ f.toFun)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.SeparationQuotient.Section

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul K E
⊢ ∃ f, mkCLM K E ∘SL f = ContinuousLinearMap.id K (SeparationQuotient E)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.SeparationQuotient.Section

Goal state before:
pp: case h
K : Type u_1
E : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module K E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul K E
L : Type u_3
inst✝³ : Semiring L
σ : L →+* K
F : Type u_4
inst✝² : AddCommMonoid F
inst✝¹ : Module L F
inst✝ : TopologicalSpace F
f : F →SL[σ] SeparationQuotient E
⊢ mkCLM K E ∘SL outCLM K E ∘SL f = f

Tactic:
← ContinuousLinearMap.comp_assoc,

Goal state after:
case h
K : Type u_1
E : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module K E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul K E
L : Type u_3
inst✝³ : Semiring L
σ : L →+* K
F : Type u_4
inst✝² : AddCommMonoid F
inst✝¹ : Module L F
inst✝ : TopologicalSpace F
f : F →SL[σ] SeparationQuotient E
⊢ (mkCLM K E ∘SL outCLM K E) ∘SL f = f
Module: Mathlib.Topology.Algebra.SeparationQuotient.Section

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module K E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul K E
L : Type u_3
inst✝³ : Semiring L
σ : L →+* K
F : Type u_4
inst✝² : AddCommMonoid F
inst✝¹ : Module L F
inst✝ : TopologicalSpace F
⊢ Function.Surjective (mkCLM K E).comp

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.SeparationQuotient.Section

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul K E
⊢ IsUniformInducing ⇑(outCLM K E)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup H
inst✝⁸ : Module 𝕜 H
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this : IsTopologicalAddGroup H
⊢ (𝓝 0).HasBasis (fun x ↦ x ∈ 𝓝 0) fun V ↦ {u | ∀ (x : α), φ u x ∈ V}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ c • f ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • f (p x) <
    c • ((w j / c) • f (p j) + (w k / c) • f (p k)) + ∑ x ∈ u, w x • f (p x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module R E
inst✝² : Module R F
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Set F
x : E
y : F
hx : x ∈ (convexHull R) s
hy : y ∈ (convexHull R) t
⊢ (x, y) ∈ (convexHull R) (s ×ˢ t)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ c • ((w j / c) • f (p j) + (w k / c) • f (p k)) + ∑ x ∈ u, w x • f (p x) =
    w j • f (p j) + w k • f (p k) + ∑ x ∈ u, w x • f (p x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s t : Set E
⊢ (convexHull R) (s + t) = (convexHull R) s + (convexHull R) t

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ w j • f (p j) + w k • f (p k) + ∑ x ∈ u, w x • f (p x) = w j • f (p j) + (w k • f (p k) + ∑ x ∈ u, w x • f (p x))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s t : Set E
⊢ (convexHull R) (s - t) = (convexHull R) s - (convexHull R) t

Tactic:
by

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
⊢ (convexHull R) (Set.range ⇑b) = {x | ∀ (i : ι), 0 ≤ (b.coord i) x}

Tactic:
convexHull_range_eq_exists_affineCombination

Goal state after:
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
⊢ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s ⇑b) w = x} = {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
Module: Mathlib.Topology.Algebra.Module.UniformConvergence

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup H
inst✝⁸ : Module 𝕜 H
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
⊢ ContinuousSMul 𝕜 H

Tactic:
by

Goal state after: