awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)
have rw : Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
  ((Finset.affineCombination R s p : (a : ι → R) → P) (r • (w₂ - w₁) + w₁) : P)
  ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)
Tactic: rw [s.affineCombination_congr hr fun _ _ => rfl]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) (r • (w₂ - w₁) + w₁) : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)
have rw : Ne.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
Tactic: rw [← s.weightedVSub_vadd_affineCombination, s.weightedVSub_const_smul,
    ← s.affineCombination_vsub, ← lineMap_apply, sbtw_lineMap_iff, and_iff_left hs.2,
    ← @vsub_ne_zero V, s.affineCombination_vsub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
have simp_rw : Eq.{u_1 + 1} (α := R) (∑ x ∈ s, (w₁ x - w₂ x)) 0
Tactic: simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
simp_rw : Eq.{u_1 + 1} (α := R) (∑ x ∈ s, (w₁ x - w₂ x)) 0
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
have simp_rw₁ : HSub.hSub (α := R) (∑ x ∈ s, w₁ x) (∑ x ∈ s, w₂ x) = 0
Tactic: simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
simp_rw : Eq.{u_1 + 1} (α := R) (∑ x ∈ s, (w₁ x - w₂ x)) 0
simp_rw₁ : HSub.hSub (α := R) (∑ x ∈ s, w₁ x) (∑ x ∈ s, w₂ x) = 0
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
have simp_rw₂ : HSub.hSub (α := R) 1 (∑ x ∈ s, w₂ x) = 0
Tactic: simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
simp_rw : Eq.{u_1 + 1} (α := R) (∑ x ∈ s, (w₁ x - w₂ x)) 0
simp_rw₁ : HSub.hSub (α := R) (∑ x ∈ s, w₁ x) (∑ x ∈ s, w₂ x) = 0
simp_rw₂ : HSub.hSub (α := R) 1 (∑ x ∈ s, w₂ x) = 0
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
have simp_rw₃ : HSub.hSub (α := R) 1 1 = 0
Tactic: simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
⊢ False
have hw₁w₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
Tactic: have hw₁w₂ : (∑ i ∈ s, (w₁ - w₂) i) = 0 := by
    simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
hw₁w₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
⊢ False
have refine : w₁ i = w₂ i
Tactic: refine hs.1 ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
hw₁w₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
⊢ w₁ i = w₂ i
have ha' : (w₁ - w₂) i = 0
Tactic: have ha' := ha s (w₁ - w₂) hw₁w₂ hz i his
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
hw₁w₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
ha' : (w₁ - w₂) i = 0
⊢ w₁ i = w₂ i
have rwa : ∀ (ha' : w₁ i - w₂ i = 0), w₁ i = w₂ i
Tactic: rwa [Pi.sub_apply, sub_eq_zero] at ha'
Cleared hypotheses: ha'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
hw₁w₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
ha' : (w₁ - w₂) i = 0
rwa : ∀ (ha' : w₁ i - w₂ i = 0), w₁ i = w₂ i
⊢ w₁ i = w₂ i
have rwa₁ : ∀ (ha' : w₁ i = w₂ i), w₁ i = w₂ i
Tactic: rwa [Pi.sub_apply, sub_eq_zero] at ha'
Cleared hypotheses: ha'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
⊢ s.closedInterior = affineSegment R (s.points 0) (s.points 1)
have h : ∀ (p : P), p ∈ s.closedInterior ↔ p ∈ affineSegment R (s.points 0) (s.points 1)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
p : P
⊢ p ∈ s.closedInterior ↔ p ∈ affineSegment R (s.points 0) (s.points 1)
have h : p ∈ s.closedInterior → p ∈ affineSegment R (s.points 0) (s.points 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
p : P
h : p ∈ s.closedInterior → p ∈ affineSegment R (s.points 0) (s.points 1)
⊢ p ∈ s.closedInterior ↔ p ∈ affineSegment R (s.points 0) (s.points 1)
have h₁ : p ∈ affineSegment R (s.points 0) (s.points 1) → p ∈ s.closedInterior
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (1 + 1), w i) 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Icc 0 1) (w i)
⊢ w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
have hw₁ : w 0 + w 1 = 1
Tactic: rw [Fin.sum_univ_two] at hw
Cleared hypotheses: hw, h01
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : w 0 + w 1 = 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Icc 0 1) (w i)
⊢ w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
have h : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), w i = Finset.affineCombinationLineMapWeights 0 1 (w 1) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : w 0 + w 1 = 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Icc 0 1) (w i)
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ w i = Finset.affineCombinationLineMapWeights 0 1 (w 1) i
have h : w ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
  Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 (w 1)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : w 0 + w 1 = 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Icc 0 1) (w i)
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  w ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
    Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 (w 1)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩)
⊢ w i = Finset.affineCombinationLineMapWeights 0 1 (w 1) i
have h₁ : w ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
  Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 (w 1)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (1 + 1), w i) 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Icc 0 1) (w i)
⊢ Membership.mem (α := P) (affineSegment R (s.points 0) (s.points 1))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (1 + 1) → R) → P) w : P)
have h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
Tactic: have h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1) := by
      rw [Fin.sum_univ_two] at hw
      ext i
      fin_cases i <;> simp [← hw]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (1 + 1), w i) 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Icc 0 1) (w i)
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
⊢ Membership.mem (α := P) (affineSegment R (s.points 0) (s.points 1))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (1 + 1) → R) → P) w : P)
have h₁ : Membership.mem (α := P) (affineSegment R (s.points 0) (s.points 1))
  ((lineMap (s.points 0) (s.points 1) : (a : R) → P) (w 1) : P)
Tactic: rw [h, Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 ≤ r
h1 : r ≤ 1
⊢ Membership.mem (α := P) s.closedInterior ((lineMap (s.points 0) (s.points 1) : (a : R) → P) r : P)
have h : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)),
  Membership.mem (γ := Set R) (Set.Icc 0 1) (Finset.affineCombinationLineMapWeights 0 1 r i)
Tactic: rw [← Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _), affineCombination_mem_closedInterior_iff
        (Finset.sum_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _) _)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 ≤ r
h1 : r ≤ 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) (Finset.affineCombinationLineMapWeights 0 1 r i)
have h : Membership.mem (γ := Set R) (Set.Icc 0 1)
  (Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 r
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 ≤ r
h1 : r ≤ 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  Membership.mem (γ := Set R) (Set.Icc 0 1)
    (Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 r
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))))
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) (Finset.affineCombinationLineMapWeights 0 1 r i)
have h₁ : Membership.mem (γ := Set R) (Set.Icc 0 1)
  (Finset.affineCombinationLineMapWeights (ι := Fin (HAdd.hAdd (α := ℕ) 1 1)) 0 1 r
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
p : P
⊢ p ∈ s.closedInterior ↔ Wbtw R (s.points 0) p (s.points 1)
have rw : p ∈ affineSegment R (s.points 0) (s.points 1) ↔ Wbtw R (s.points 0) p (s.points 1)
Tactic: rw [closedInterior_eq_affineSegment, Wbtw]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
p : P
rw : p ∈ affineSegment R (s.points 0) (s.points 1) ↔ Wbtw R (s.points 0) p (s.points 1)
⊢ p ∈ s.closedInterior ↔ Wbtw R (s.points 0) p (s.points 1)
have rw₁ : p ∈ affineSegment R (s.points 0) (s.points 1) ↔ p ∈ affineSegment R (s.points 0) (s.points 1)
Tactic: rw [closedInterior_eq_affineSegment, Wbtw]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
have inl : ∀ (hij : i < j), affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
Tactic: rcases h.lt_or_gt with hij | hji
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
inl :
  ∀ (hij : i < j), affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
have inr : ∀ (hji : j < i), affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
Tactic: rcases h.lt_or_gt with hij | hji
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
hji : j < i
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
have inr : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (max i j)) (s.points (min i j))
Tactic: nth_rw 2 [affineSegment_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
⊢ (s.face (fs := {i, j}) ⋯).closedInterior = affineSegment R (s.points i) (s.points j)
have h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
Tactic: have h' : affineSegment R (s.points i) (s.points j) =
      affineSegment R (s.points (min i j)) (s.points (max i j)) := by
    rcases h.lt_or_gt with hij | hji
    · simp [min_eq_left hij.le, max_eq_right hij.le]
    · nth_rw 2 [affineSegment_comm]
      simp [max_eq_left hji.le, min_eq_right hji.le]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
⊢ (s.face (fs := {i, j}) ⋯).closedInterior = affineSegment R (s.points i) (s.points j)
have rw : affineSegment R (s.points ((Finset.orderEmbOfFin {i, j} sorry : (a : Fin (1 + 1)) → Fin (n + 1)) 0))
    (s.points ((Finset.orderEmbOfFin {i, j} sorry : (a : Fin (1 + 1)) → Fin (n + 1)) 1)) =
  affineSegment R (s.points (min i j)) (s.points (max i j))
Tactic: rw [h', (s.face (Finset.card_pair h)).closedInterior_eq_affineSegment, face_points, face_points]