mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G H : SimpleGraph V
⊢ (∀ (v : V), Disjoint (G.incidenceSet v) (H.incidenceSet v)) ↔ Disjoint G H

Tactic:
[

Goal state after:
V : Type u
G H : SimpleGraph V
⊢ (∀ (v : V), Disjoint (G.incidenceSet v) (H.incidenceSet v)) ↔ Disjoint G H
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
⊢ G.incidenceSet a ∩ G.incidenceSet b = ∅

Tactic:
[

Goal state after:
V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
⊢ G.incidenceSet a ∩ G.incidenceSet b = ∅
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G H : SimpleGraph V
⊢ (∀ (v : V), Disjoint (G.neighborSet v) (H.neighborSet v)) ↔ Disjoint G H

Tactic:
[

Goal state after:
V : Type u
G H : SimpleGraph V
⊢ (∀ (v : V), Disjoint (G.neighborSet v) (H.neighborSet v)) ↔ Disjoint G H
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u
inst✝ : Nonempty ι
s : ι → SimpleGraph V
v x✝ : V
⊢ x✝ ∈ (⨅ i, s i).neighborSet v ↔ x✝ ∈ ⋂ i, (s i).neighborSet v

Tactic:
[

Goal state after:
ι : Sort u_1
V : Type u
inst✝ : Nonempty ι
s : ι → SimpleGraph V
v x✝ : V
⊢ x✝ ∈ (⨅ i, s i).neighborSet v ↔ x✝ ∈ ⋂ i, (s i).neighborSet v
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V}, G.Adj a b → a ≠ b
⊢ w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ w ∈ {v}ᶜ

Tactic:
[

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V}, G.Adj a b → a ≠ b
⊢ w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ w ∈ {v}ᶜ
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v ∪ Gᶜ.neighborSet v)
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1

Tactic:
[

Goal state after:
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v ∪ Gᶜ.neighborSet v)
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G H : SimpleGraph V
⊢ (∀ (u v : V), Disjoint (G.commonNeighbors u v) (H.commonNeighbors u v)) ↔ Disjoint G H

Tactic:
[

Goal state after:
V : Type u
G H : SimpleGraph V
⊢ (∀ (u v : V), Disjoint (G.commonNeighbors u v) (H.commonNeighbors u v)) ↔ Disjoint G H
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case inr.inr
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
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
[

Goal state after:
case inr.inr
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
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
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₂ : P
h : p₂ ∈ s
⊢ (y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
[

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₂ : P
h : p₂ ∈ s
⊢ (y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
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₂ : P
h : p₂ ∈ s
⊢ (x ∉ s ∧ y ∉ s ∧ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔
    x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
[

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₂ : P
h : p₂ ∈ s
⊢ (x ∉ s ∧ y ∉ s ∧ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔
    x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
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✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
this : dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a -[ℝ] c -ᵥ a]
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

Tactic:
[

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
this : dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a -[ℝ] c -ᵥ a]
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
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✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

Tactic:
dist_add_dist_eq_iff

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ Wbtw ℝ a b c ↔ Wbtw ℝ a b c
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
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : StrictConvexSpace ℝ E
inst✝³ : MetricSpace PE
inst✝² : MetricSpace PF
inst✝¹ : NormedAddTorsor E PE
inst✝ : NormedAddTorsor F PF
r : ℝ
f : PF → PE
x✝ y✝ z : PE
hi : Isometry f
x y : PF
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)

Tactic:
apply eq_midpoint_of_dist_eq_half
        · rw [hi.dist_eq, hi.dist_eq]
          simp only [dist_left_midpoint, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul]
        · rw [hi.dist_eq, hi.dist_eq]
          simp only [dist_midpoint_right, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul]

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

Goal state before:
pp: V : Type u_2
ι : Type u_4
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, ‖z i‖ ≤ r
⊢ ‖∑ k ∈ t, w k • z k‖ < r

Tactic:
[

Goal state after:
V : Type u_2
ι : Type u_4
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, ‖z i‖ ≤ r
⊢ ‖∑ k ∈ t, w k • z k‖ < r
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : p i ≠ p j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hp : ∀ i ∈ t, dist (p i) p₀ ≤ r
⊢ ‖∑ i ∈ t, w i • (p i -ᵥ p₀)‖ < r

Tactic:
[

Goal state after:
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : p i ≠ p j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hp : ∀ i ∈ t, dist (p i) p₀ ≤ r
⊢ ‖∑ i ∈ t, w i • (p i -ᵥ p₀)‖ < r
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case inr.inr.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✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
this : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)
⊢ ((r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁)) +ᵥ p₁ ∈ s

Tactic:
this

Goal state after:
case inr.inr.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✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
this : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)
⊢ (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.WSameSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s

Tactic:
[

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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.WSameSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
x✝² : Convex ℝ s
x : E
x✝¹ : x ∈ s
y : E
x✝ : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y - a * b * (m / 2 * ‖x - y‖ ^ 2) ↔
    f (a • x + b • y) - m / 2 * ‖a • x + b • y‖ ^ 2 ≤ a • (f x - m / 2 * ‖x‖ ^ 2) + b • (f y - m / 2 * ‖y‖ ^ 2)

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
x✝² : Convex ℝ s
x : E
x✝¹ : x ∈ s
y : E
x✝ : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y - a * b * (m / 2 * ‖x - y‖ ^ 2) ↔
    f (a • x + b • y) - m / 2 * ‖a • x + b • y‖ ^ 2 ≤ a • (f x - m / 2 * ‖x‖ ^ 2) + b • (f y - m / 2 * ‖y‖ ^ 2)
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
x✝² : Convex ℝ s
x : E
x✝¹ : x ∈ s
y : E
x✝ : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y + a * b * (m / 2 * ‖x - y‖ ^ 2) ≤ f (a • x + b • y) ↔
    a • (f x + m / 2 * ‖x‖ ^ 2) + b • (f y + m / 2 * ‖y‖ ^ 2) ≤ f (a • x + b • y) + m / 2 * ‖a • x + b • y‖ ^ 2

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
x✝² : Convex ℝ s
x : E
x✝¹ : x ∈ s
y : E
x✝ : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y + a * b * (m / 2 * ‖x - y‖ ^ 2) ≤ f (a • x + b • y) ↔
    a • (f x + m / 2 * ‖x‖ ^ 2) + b • (f y + m / 2 * ‖y‖ ^ 2) ≤ f (a • x + b • y) + m / 2 * ‖a • x + b • y‖ ^ 2
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.SSameSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s

Tactic:
[

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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.SSameSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.WOppSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) ↑s

Tactic:
[

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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.WOppSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) ↑s
Module: Mathlib.Analysis.Convex.Visible

Goal state before:
pp: case inr
𝕜 : 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 - ε
⊢ False

Tactic:
have hwi : 0 < 1 - w i := by linarith

Goal state after:
case inr
𝕜 : 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
⊢ 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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.SOppSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) ↑s

Tactic:
[

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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.SOppSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) ↑s
Module: Mathlib.Analysis.Convex.Visible

Goal state before:
pp: 𝕜 : 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
⊢ w i • a i + ∑ x ∈ t.erase i, (1 - w i) • (w x / (1 - w i)) • a x = ∑ j ∈ t, w j • a j

Tactic:
[

Goal state after:
𝕜 : 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
⊢ w i • a i + ∑ x ∈ t.erase i, (1 - w i) • (w x / (1 - w i)) • a x = ∑ j ∈ t, w j • a j
Module: Mathlib.Analysis.Convex.Visible

Goal state before:
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
this : w i • a i + (1 - w i) • ∑ j ∈ t.erase i, (w j / (1 - w i)) • a j = ∑ j ∈ t, w j • a j
⊢ (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:
[

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
this : w i • a i + (1 - w i) • ∑ j ∈ t.erase i, (w j / (1 - w i)) • a j = ∑ j ∈ t, w j • a j
⊢ (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.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:
[

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 μ)
⊢ ‖holder r B f g‖₊ ≤ ‖B‖₊ * ‖f‖₊ * ‖g‖₊
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ ∫⁻ (a : α), ∫⁻ (t : ℝ) in Ioc 0 (f a), ENNReal.ofReal (g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ ∫⁻ (a : α), ∫⁻ (t : ℝ) in Ioc 0 (f a), ENNReal.ofReal (g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) s) = fun x ↦
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f x)
⊢ ∫⁻ (x : α), (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) s ∂μ =
    (Ioi 0).indicator (fun t ↦ μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) s) = fun x ↦
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f x)
⊢ ∫⁻ (x : α), (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) s ∂μ =
    (Ioi 0).indicator (fun t ↦ μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s