awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq (α := ℝ) (∑ 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, Membership.mem (γ := Set V) (closedBall 0 r) (z i)
⊢ Membership.mem (γ := Set V) (ball 0 r) (∑ k ∈ t, w k • z k)

Tactic:
sum_mem_ball_of_strictConvexSpace h0 h1 hi hj hij hi0 hj0 hz

Premises used: Set.Mem, sum_mem_ball_of_strictConvexSpace
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq (α := ℝ) (∑ 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, Membership.mem (γ := Set V) (closedBall 0 r) (z i)
⊢ Membership.mem (γ := Set V) (ball 0 r) (∑ k ∈ t, w k • z k)

Tactic:
exact sum_mem_ball_of_strictConvexSpace h0 h1 hi hj hij hi0 hj0 hz

Premises used: sum_mem_ball_of_strictConvexSpace
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq (α := ℝ) (∑ 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
rw : norm.{u_2} (E := V) (∑ i ∈ t, w i • (p i -ᵥ p₀)) < r
⊢ dist ((affineCombination ℝ t p : (a : ι → ℝ) → P) w) p₀ < r

Tactic:
rw [affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ h1 p₀,
    weightedVSubOfPoint_apply, dist_vadd_left]

Premises used: Finset.weightedVSubOfPoint_apply, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, dist_vadd_left
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq (α := ℝ) (∑ 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, ‖p i -ᵥ p₀‖ ≤ r

Tactic:
simp_rw [dist_eq_norm_vsub] at hp

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq (α := ℝ) (∑ 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, ‖p i -ᵥ p₀‖ ≤ r
⊢ p i -ᵥ p₀ ≠ p j -ᵥ p₀

Tactic:
simpa using hij
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq (α := ℝ) (∑ 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, ‖p i -ᵥ p₀‖ ≤ r
⊢ norm.{u_2} (E := V) (∑ i ∈ t, w i • (p i -ᵥ p₀)) < r

Tactic:
exact norm_sum_lt_of_strictConvexSpace h0 h1 hi hj (by simpa using hij) hi0 hj0 hp

Premises used: norm_sum_lt_of_strictConvexSpace
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ p : P
hp : p ∈ s.closedInterior
hp' : ∀ (i : Fin (n + 1)), p ≠ s.points i
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
rcases :
  ∀ (w : Fin (n + 1) → ℝ) (hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1)
    (hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i))
    (hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i),
    dist ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w) p₀ < r
⊢ dist p p₀ < r

Tactic:
rcases hp with ⟨w, hw, hw01, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
by_contra! : ∀ (hij : ∀ (i : Fin (n + 1)), w i = 0), False
⊢ ∃ (i : Fin (n + 1)), w i ≠ 0

Tactic:
by_contra! hij
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
hij : ∀ (i : Fin (n + 1)), w i = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
obtain :
  ∀ (i : Fin (n + 1)) (hi : w i ≠ 0), dist ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w) p₀ < r
⊢ dist ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w) p₀ < r

Tactic:
obtain ⟨i, hi⟩ : ∃ i, w i ≠ 0 := by
    by_contra! hij
    simp_all
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
by_contra! : ∀ (hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0), False
⊢ ∃ (j : Fin (n + 1)), i ≠ j ∧ w j ≠ 0

Tactic:
by_contra! hij
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0
apply : (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.points i
⊢ False

Tactic:
apply hp' i
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0
rw :
  Eq.{u_3 + 1} (α := P) ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
    ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) :
      P)
⊢ (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.points i

Tactic:
rw [← Finset.univ.affineCombination_piSingle ℝ s.points (Finset.mem_univ i)]

Premises used: Finset.mem_univ, Affine.Simplex.points, Real, Finset.univ, Finset.affineCombination_piSingle
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0
h : w = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
    ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) :
      P)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0
h : ∀ (j : Fin (n + 1)), w j = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j
⊢ w = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1

Tactic:
ext j
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0
j : Fin (n + 1)
h : w i = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 i
h₁ : ∀ (hj : i ≠ j), w j = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j
⊢ w j = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j

Tactic:
obtain rfl | hj := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0
h : w i = 1
⊢ w i = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 i

Tactic:
simp only [Pi.single_eq_same]

Premises used: Pi.single_eq_same
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0
h : ∑ i : Fin (n + 1), w i = w i
⊢ w i = 1

Tactic:
rw [← hw, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0
⊢ i ∉ univ → w i = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0
⊢ ∑ i : Fin (n + 1), w i = w i

Tactic:
exact sum_eq_single i (fun k _ hk ↦ hij k hk.symm) (by simp)

Premises used: Ne.symm, Finset.sum_eq_single
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0
j : Fin (n + 1)
hj : i ≠ j
h : w j = 0
⊢ w j = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j

Tactic:
rw [Pi.single_eq_of_ne' hj]

Premises used: Pi.single_eq_of_ne'
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0
j : Fin (n + 1)
hj : i ≠ j
⊢ w j = 0

Tactic:
hij j hj
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0
j : Fin (n + 1)
hj : i ≠ j
⊢ w j = 0

Tactic:
exact hij j hj
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
obtain :
  ∀ (j : Fin (n + 1)) (hij : i ≠ j) (hj : w j ≠ 0),
    dist ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w) p₀ < r
⊢ dist ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w) p₀ < r

Tactic:
obtain ⟨j, hij, hj⟩ : ∃ j, i ≠ j ∧ w j ≠ 0 := by
    by_contra! hij
    apply hp' i
    rw [← Finset.univ.affineCombination_piSingle ℝ s.points (Finset.mem_univ i)]
    congr 1
    ext j
    obtain rfl | hj := eq_or_ne i j
    · simp only [Pi.single_eq_same]
      rw [← hw, eq_comm]
      exact sum_eq_single i (fun k _ hk ↦ hij k hk.symm) (by simp)
    · rw [Pi.single_eq_of_ne' hj]
      exact hij j hj
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
j : Fin (n + 1)
hij : i ≠ j
hj : w j ≠ 0
⊢ dist ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w) p₀ < r

Tactic:
dist_affineCombination_lt_of_strictConvexSpace (fun k _ ↦ (hw01 k).1) hw
    (Finset.mem_univ i) (Finset.mem_univ j) (s.independent.injective.ne hij) hi hj (fun k _ ↦ hr k)

Premises used: Finset.mem_univ, dist_affineCombination_lt_of_strictConvexSpace, Function.Injective.ne, AffineIndependent.injective, And.left, Affine.Simplex.independent
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (w i)
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
j : Fin (n + 1)
hij : i ≠ j
hj : w j ≠ 0
⊢ dist ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w) p₀ < r

Tactic:
exact dist_affineCombination_lt_of_strictConvexSpace (fun k _ ↦ (hw01 k).1) hw
    (Finset.mem_univ i) (Finset.mem_univ j) (s.independent.injective.ne hij) hi hj (fun k _ ↦ hr k)

Premises used: Finset.mem_univ, dist_affineCombination_lt_of_strictConvexSpace, Function.Injective.ne, AffineIndependent.injective, And.left, Affine.Simplex.independent
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ p : P
hp : p ∈ s.interior
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
⊢ dist p p₀ < r

Tactic:
s.dist_lt_of_mem_closedInterior_of_strictConvexSpace
    (Set.mem_of_mem_of_subset hp s.interior_subset_closedInterior)
    (fun i h ↦ s.point_notMem_interior i (h ▸ hp)) hr

Premises used: Affine.Simplex.interior_subset_closedInterior, Eq.rec, Affine.Simplex.point_notMem_interior, Set.mem_of_mem_of_subset, Affine.Simplex.dist_lt_of_mem_closedInterior_of_strictConvexSpace
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ p₁ -ᵥ p ≠ p₃ -ᵥ p

Tactic:
simpa using h.left_ne_right

Premises used: Sbtw.left_ne_right
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ p₁ -ᵥ p ≠ p₃ -ᵥ p

Tactic:
have hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p := by simpa using h.left_ne_right
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
⊢ (p₂ -ᵥ p = p₁ -ᵥ p ∨ p₂ -ᵥ p = p₃ -ᵥ p ∨ p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)) ∧ p₂ ≠ p₁ ∧ p₂ ≠ p₃

Tactic:
rw [Sbtw, ← wbtw_vsub_const_iff p, Wbtw, affineSegment_eq_segment, ← insert_endpoints_openSegment,
    Set.mem_insert_iff, Set.mem_insert_iff] at h

Premises used: Wbtw, insert_endpoints_openSegment, affineSegment_eq_segment, wbtw_vsub_const_iff, Set.mem_insert_iff, Sbtw
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h₁ : (p₂ -ᵥ p = p₁ -ᵥ p ∨ p₂ -ᵥ p = p₃ -ᵥ p ∨ p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)) ∧ p₂ ≠ p₁ ∧ p₂ ≠ p₃
⊢ p₁ -ᵥ p ≠ p₃ -ᵥ p

Tactic:
rw [Sbtw, ← wbtw_vsub_const_iff p, Wbtw, affineSegment_eq_segment, ← insert_endpoints_openSegment,
    Set.mem_insert_iff, Set.mem_insert_iff] at h

Premises used: Wbtw, insert_endpoints_openSegment, affineSegment_eq_segment, wbtw_vsub_const_iff, Set.mem_insert_iff, Sbtw
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
inst_3 : PseudoMetricSpace P
inst_4 : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : (p₂ -ᵥ p = p₁ -ᵥ p ∨ p₂ -ᵥ p = p₃ -ᵥ p ∨ p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)) ∧ p₂ ≠ p₁ ∧ p₂ ≠ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
inl : ∀ (h : p₂ -ᵥ p = p₁ -ᵥ p) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃), dist p₂ p < max (dist p₁ p) (dist p₃ p)
inr : ∀ (h : p₂ -ᵥ p = p₃ -ᵥ p) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃), dist p₂ p < max (dist p₁ p) (dist p₃ p)
inr₁ :
  ∀ (h : p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃),
    dist p₂ p < max (dist p₁ p) (dist p₃ p)
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
rcases h with ⟨h | h | h, hp₂p₁, hp₂p₃⟩