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

Goal state before:
pp: case mp.inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
⊢ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
· refine ⟨-r₁ / r₂, div_neg_of_neg_of_pos (Left.neg_neg_iff.2 hr₁) hr₂, p₂, hp₂, ?_⟩
      rw [div_eq_inv_mul, ← smul_smul, neg_smul, h, smul_neg, smul_smul,
        inv_mul_cancel₀ hr₂.ne.symm, one_smul, neg_vsub_eq_vsub_rev, vsub_vadd]

Goal state after:
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 | s.SOppSide x y} = Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) ↑s

Tactic:
by

Goal state after:
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
hx : x ∈ s
hy : y ∉ s
⊢ s.SOppSide y ((pointReflection R x) y)

Tactic:
by

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

Goal state before:
pp: V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
⊢ IsConnected {y | s.WSameSide x y}

Tactic:
by

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

Goal state before:
pp: V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
⊢ IsPreconnected {y | s.WSameSide x y}

Tactic:
by

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

Goal state before:
pp: V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
h : (↑s).Nonempty
⊢ IsConnected {y | s.SSameSide x y}

Tactic:
by

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

Goal state before:
pp: case pos
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
hx : x ∈ s
⊢ IsPreconnected {y | s.SSameSide x y}

Tactic:
simp only [hx, SSameSide, not_true, false_and, and_false]

Goal state after:
case pos
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
hx : x ∈ s
⊢ IsPreconnected {y | False}
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
⊢ IsPreconnected {y | s.SSameSide x y}

Tactic:
by

Goal state after:
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
⊢ Wbtw 𝕜 ((lineMap x (a i)) ε) ((lineMap x (∑ j ∈ t, w j • a j)) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)))
    (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j)

Tactic:
by

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

Goal state before:
pp: V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
⊢ IsConnected {y | s.WOppSide x y}

Tactic:
by

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

Goal state before:
pp: V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
⊢ IsPreconnected {y | s.WOppSide x y}

Tactic:
by

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

Goal state before:
pp: V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
h : (↑s).Nonempty
⊢ IsConnected {y | s.SOppSide x y}

Tactic:
by

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

Goal state before:
pp: V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
⊢ IsPreconnected {y | s.SOppSide x y}

Tactic:
by

Goal state after:
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✝¹ : 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)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
⊢ w₂ i ≠ 0

Tactic:
by

Goal state after:
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✝¹ : 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)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
⊢ s.points j ∈ affineSpan R (Set.range (s.faceOpposite i).points)

Tactic:
by

Goal state after:
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✝¹ : 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)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : s.points j ∈ affineSpan R (Set.range (s.faceOpposite i).points)
w₃ : Fin (n + 1) → R := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single j 1)
⊢ ∑ k, w₃ k = 1

Tactic:
by

Goal state after:
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✝¹ : 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)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : s.points j ∈ affineSpan R (Set.range (s.faceOpposite i).points)
w₃ : Fin (n + 1) → R := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single j 1)
hw₃1 : ∑ k, w₃ k = 1
⊢ w₃ i = 0

Tactic:
by

Goal state after:
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
⊢ 0 < (1 - ε) / ε

Tactic:
by

Goal state after:
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
⊢ IsVisible 𝕜 ((convexHull 𝕜) s) x (a i)

Tactic:
by

Goal state after:
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 y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
h : ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False
⊢ False

Tactic:
by

Goal state after:
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 y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
⊢ s ∈ 𝓝 ((lineMap y x) 0)

Tactic:
by

Goal state after:
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) =ᵐ[μ] fun x ↦ (B (↑↑f x)) (↑↑g x)

Tactic:
by

Goal state after:
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 y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
hmem✝ : ∀ᶠ (δ : 𝕜) in 𝓝[>] 0, (lineMap y x) δ ∈ s
δ : 𝕜
hmem : (lineMap y x) δ ∈ s
hsbt : δ ∈ Set.Ioo 0 1
⊢ Sbtw 𝕜 y ((lineMap y x) δ) x

Tactic:
by

Goal state after:
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 y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
⊢ x = y

Tactic:
by

Goal state after:
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 y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hs : IsOpen[inst✝²] s
hsxy : IsVisible 𝕜 s x y
hy : y ∈ s
⊢ y ∈ interior s

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x : V
hx : x ∉ (convexHull ℝ) s
ι : Type
w✝ : Fintype ι
w : ι → ℝ
a : ι → V
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
ha : ∀ (i : ι), a i ∈ s
hy : ∑ i, w i • a i ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x (∑ i, w i • a i)
⊢ ∑ i with w i ≠ 0, w i = 1

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x : V
hx : x ∉ (convexHull ℝ) s
ι : Type
w✝ : Fintype ι
w : ι → ℝ
a : ι → V
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
ha : ∀ (i : ι), a i ∈ s
hy : ∑ i, w i • a i ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x (∑ i, w i • a i)
i : ι
hi : i ∈ {i | w i ≠ 0}
⊢ ∀ i ∈ Finset.univ, a i ∈ s

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x y : V
hx : x ∉ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x y
⊢ y ∈ (convexHull ℝ) {z | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
⊢ 1 ∈ t

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ₀ : 0 ≤ δ
hδ : (lineMap x y) δ ∈ s
ε : ℝ
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hε : (lineMap x ((lineMap x y) δ)) ε ∈ s
h : (lineMap x ((lineMap x y) δ)) ε ≠ (lineMap x y) δ
⊢ δ ≠ 0

Tactic:
by

Goal state after:
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✝¹ : 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)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)

Tactic:
by

Goal state after:
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✝¹ : 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)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂) (w₁ i / (w₁ i - w₂ i))
⊢ 0 < w₁ i - w₂ i

Tactic:
by

Goal state after:
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✝¹ : 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)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
⊢ ∑ j, w₃ j = 1

Tactic:
by

Goal state after:
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₁ f₂ : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ holder r B (f₁ + f₂) g = holder r B f₁ g + holder r B f₂ g

Tactic:
by

Goal state after:
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✝¹ : 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)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : ∑ j, w₃ j = 1
⊢ w₁ ≠ w₂

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ : (lineMap x y) δ ∈ s
ε : ℝ
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hε : (lineMap x ((lineMap x y) δ)) ε ∈ s
h : (lineMap x ((lineMap x y) δ)) ε ≠ (lineMap x y) δ
hδ₀ : 0 < δ
⊢ ε ≠ 1

Tactic:
by

Goal state after:
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✝¹ : 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)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : ∑ j, w₃ j = 1
⊢ w₁ i < w₁ i - w₂ i

Tactic:
by

Goal state after:
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✝¹ : 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)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : ∑ j, w₃ j = 1
h : Sbtw R w₁ w₃ w₂
⊢ Sbtw R ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₃)
    ((Finset.affineCombination R Finset.univ s.points) w₂)

Tactic:
by

Goal state after:
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₁ g₂ : ↥(Lp F q μ)
⊢ holder r B f (g₁ + g₂) = holder r B f g₁ + holder r B f g₂

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] s
hy : y ∈ s
x : V
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
x : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] ((convexHull ℝ) s)
hx : x ∉ (convexHull ℝ) s
⊢ (convexHull ℝ) s ⊆ ↑(affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))

Tactic:
by

Goal state after:
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✝¹ : 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)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
⊢ (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₂)

Tactic:
by

Goal state after:
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
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ holder r B (c • f) g = c • holder r B f g

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
x : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] ((convexHull ℝ) s)
hx : x ∉ (convexHull ℝ) s
⊢ Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
    Module.rank ℝ ↥(span ℝ ↑(-x +ᵥ affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y})))

Tactic:
by

Goal state after:
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
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ holder r B f (c • g) = c • holder r B f g

Tactic:
by

Goal state after:
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 : ℝ≥0∞
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
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : Fact (1 ≤ q)
inst✝³ : p.HolderConjugate q
inst✝² : NormedSpace ℝ G
inst✝¹ : SMulCommClass ℝ 𝕜 G
inst✝ : CompleteSpace G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ ((lpPairing μ p q B) f) g = ∫ (x : α), (B (↑↑f x)) (↑↑g x) ∂μ

Tactic:
by

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

Goal state before:
pp: V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
x : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] ((convexHull ℝ) s)
hx : x ∉ (convexHull ℝ) s
h :
  -x +ᵥ ↑(affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y})) =
    ↑(span ℝ (-x +ᵥ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))
⊢ Module.rank ℝ ↥(span ℝ ↑(-x +ᵥ affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))) =
    Module.rank ℝ ↥(span ℝ (-x +ᵥ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))

Tactic:
by

Goal state after: