awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
t : Finset ι
w : ι → R
z : ι → V
hs : StrictConvex R s
empty :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ w i) →
    ∀ (i j : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        Membership.mem (γ := Finset ι) ∅ j →
          z i ≠ z j →
            w i ≠ 0 →
              w j ≠ 0 → (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → z i ∈ s) → centerMass ∅ w z ∈ interior s
⊢ (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
have insert : ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
  (ht :
    (∀ i ∈ t, 0 ≤ w i) →
      ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s),
  (∀ i_1 ∈ insert i t, 0 ≤ w i_1) →
    ∀ (i_1 j : ι),
      i_1 ∈ insert i t →
        j ∈ insert i t →
          z i_1 ≠ z j → w i_1 ≠ 0 → w j ≠ 0 → (∀ i_2 ∈ insert i t, z i_2 ∈ s) → (insert i t).centerMass w z ∈ interior s
Tactic: classical
  induction t using Finset.induction with
  | empty => simp
  | insert i t hi ht =>
    intro h₀ i' j' hi' hj' hi'j' hi'0 hj'0 hmem
    have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
    have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
    by_cases hsum_t : ∑ j ∈ t, w j = 0
    · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
      have h : i' ∈ t ∨ j' ∈ t := by grind
      exfalso
      rcases h with h | h
      · exact hi'0 (ws _ h)
      · exact hj'0 (ws _ h)
    rw [Finset.centerMass_insert _ _ _ hi hsum_t]
    by_cases hi : w i = 0
    · simp only [hi, zero_add, zero_div, zero_smul, ne_eq, hsum_t, not_false_eq_true, div_self,
        one_smul]
      grind
    by_cases hzi : z i = t.centerMass w z
    · have hwi : w i + ∑ j ∈ t, w j ≠ 0 := by
        refine LT.lt.ne' ?_
        have hwi : 0 < w i := by grind
        grw [hwi]
        simp only [lt_add_iff_pos_right, gt_iff_lt]
        exact (sum_nonneg hs₀).lt_of_ne' hsum_t
      simp only [hzi, ← add_smul, ← add_div, ne_eq, hwi, not_false_eq_true, div_self, one_smul]
      by_cases! hijt : ∃ i'' j'', i'' ∈ t ∧ j'' ∈ t ∧ z i'' ≠ z j'' ∧ w i'' ≠ 0 ∧ w j'' ≠ 0
      · grind
      · exfalso
        obtain ⟨i'', hi'', hwi''⟩ : ∃ i'' ∈ t, w i'' ≠ 0 := by grind
        have hijt' : ∀ j'', j'' ∈ t → w j'' ≠ 0 → z j'' = Function.const _ (z i'') j'' := by
          grind
        have hi : i = i' ∨ i = j' := by grind
        have hzi'' : t.centerMass w z = z i'' := by
          rw [t.centerMass_congr_fun hijt', t.centerMass_const hsum_t]
        grind
    · exact strictConvex_iff_div.1 hs zi
        (hs.convex.centerMass_mem hs₀ (lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t))
          (fun j hj ↦ hmem j (mem_insert_of_mem hj))) hzi (by grind)
        ((sum_nonneg hs₀).lt_of_ne' hsum_t)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
t : Finset ι
w : ι → R
z : ι → V
hs : StrictConvex R s
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq.{u_1 + 1} (α := R) (∑ 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 ∈ s
⊢ ∑ k ∈ t, w k • z k ∈ interior s
have rw : t.centerMass w z ∈ interior s
Tactic: rw [← t.centerMass_eq_of_sum_1 _ h1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
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 ∈ closedBall p r
⊢ t.centerMass w z ∈ ball p r
have inl : ∀ (hz : ∀ i ∈ t, z i ∈ closedBall p 0), t.centerMass w z ∈ ball p 0
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
Cleared hypotheses: r, hz
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
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 ∈ closedBall p r
inl : ∀ (hz : ∀ i ∈ t, z i ∈ closedBall p 0), t.centerMass w z ∈ ball p 0
⊢ t.centerMass w z ∈ ball p r
have inr : ∀ (hr : r ≠ 0), t.centerMass w z ∈ ball p r
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
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 ∈ closedBall p r
hr : r ≠ 0
⊢ t.centerMass w z ∈ ball p r
have inr : t.centerMass w z ∈ interior (closedBall p r)
Tactic: rw [← interior_closedBall _ hr]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
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, z i ∈ closedBall p r
⊢ ∑ k ∈ t, w k • z k ∈ ball p r
have rw : t.centerMass w z ∈ ball p r
Tactic: rw [← t.centerMass_eq_of_sum_1 _ h1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (hypothesis)
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, ‖z i‖ ≤ r
⊢ norm.{u_2} (E := V) (∑ k ∈ t, w k • z k) < r
have hz₁ : ∀ i ∈ t, Membership.mem (γ := Set V) (closedBall 0 r) (z i)
Tactic: simp_rw [← mem_closedBall_zero_iff] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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)
⊢ norm.{u_2} (E := V) (∑ k ∈ t, w k • z k) < r
have rw : Membership.mem (γ := Set V) (ball 0 r) (∑ k ∈ t, w k • z k)
Tactic: rw [← mem_ball_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ dist ((affineCombination ℝ t p : (a : ι → ℝ) → P) w) p₀ < r
have rw : norm.{u_2} (E := V) (∑ i ∈ t, w i • (p i -ᵥ p₀)) < r
Tactic: rw [affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ h1 p₀,
    weightedVSubOfPoint_apply, dist_vadd_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (hypothesis)
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
⊢ norm.{u_2} (E := V) (∑ i ∈ t, w i • (p i -ᵥ p₀)) < r
have hp₁ : ∀ i ∈ t, ‖p i -ᵥ p₀‖ ≤ r
Tactic: simp_rw [dist_eq_norm_vsub] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ dist p p₀ < r
have 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
Tactic: rcases hp with ⟨w, hw, hw01, rfl⟩
Cleared hypotheses: p, hp, hp'
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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)), w i ≠ 0
have by_contra! : ∀ (hij : ∀ (i : Fin (n + 1)), w i = 0), False
Tactic: by_contra! hij
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ dist ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w) p₀ < r
have obtain : ∀ (i : Fin (n + 1)) (hi : w i ≠ 0), 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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)), i ≠ j ∧ w j ≠ 0
have by_contra! : ∀ (hij : ∀ (j : Fin (n + 1)) (_ : i ≠ j), w j = 0), False
Tactic: by_contra! hij
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ False
have apply : (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.points i
Tactic: apply hp' i
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ (affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.points i
have 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)
Tactic: rw [← Finset.univ.affineCombination_piSingle ℝ s.points (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ 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)
have h : w = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ w = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1
have h : ∀ (j : Fin (n + 1)), w j = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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)
⊢ w j = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j
have h : w i = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 i
Tactic: obtain rfl | hj := eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ w j = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j
have h₁ : ∀ (hj : i ≠ j), w j = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j
Tactic: obtain rfl | hj := eq_or_ne i j
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ w i = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 i
have h : w i = 1
Tactic: simp only [Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ w i = 1
have h : ∑ i : Fin (n + 1), w i = w i
Tactic: rw [← hw, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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 = Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j
have h : w j = 0
Tactic: rw [Pi.single_eq_of_ne' hj]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ dist ((affineCombination ℝ univ s.points : (a : Fin (n + 1) → ℝ) → P) w) p₀ < r
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
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₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
have hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
Tactic: have hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p := by simpa using h.left_ne_right
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
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
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
have h₁ : (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
Cleared hypotheses: h, hp₁p₃
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
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
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
have inl : ∀ (h : p₂ -ᵥ p = p₁ -ᵥ p) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃), dist p₂ p < max (dist p₁ p) (dist p₃ p)
Tactic: rcases h with ⟨h | h | h, hp₂p₁, hp₂p₃⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
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)
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
have inr : ∀ (h : p₂ -ᵥ p = p₃ -ᵥ p) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃), dist p₂ p < max (dist p₁ p) (dist p₃ p)
Tactic: rcases h with ⟨h | h | h, hp₂p₁, hp₂p₃⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (goal)
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)
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
have 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)
Tactic: rcases h with ⟨h | h | h, hp₂p₁, hp₂p₃⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexBetween (hypothesis)
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
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₁ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
have h₁ : p₂ = p₁
Tactic: rw [vsub_left_cancel_iff] at h
Cleared hypotheses: h, hp₂p₁, hp₂p₃