awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
rw : s * s' + s * t' + t = 1
rw₁ : s * (s' + t') + t = 1
⊢ s * s' + (s * t' + t) = 1
have rw₂ : s * 1 + t = 1
Tactic: rw [← add_assoc, ← mul_add, h', mul_one, h]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
rw : s * s' + s * t' + t = 1
rw₁ : s * (s' + t') + t = 1
rw₂ : s * 1 + t = 1
rw₃ : s + t = 1
⊢ s * s' + (s * t' + t) = 1
have rw₄ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [← add_assoc, ← mul_add, h', mul_one, h]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ convexCombPair s t hs ht h (convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
have rw : sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)) =
  sConvexComb (convexCombPair (s * s') (s * t' + t) sorry sorry sorry (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h''))
Tactic: rw [convexCombPair_convexCombPair_left_eq_sConvexComb,
    convexCombPair_convexCombPair_right_eq_sConvexComb]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)) =
    sConvexComb (convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h''))
have e_f : convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃) =
  convexCombPair (s * s') (s * t' + t) sorry sorry sorry (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h'')
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃) =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h'')
have e_f : (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)).weights =
  (convexCombPair (s * s') (s * t' + t) sorry sorry sorry (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h'')).weights
Tactic: ext1
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ s * (t' * t'') + t * t'' = t
have rw : s * t' * t'' + t * t'' = t
Tactic: rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
rw : s * t' * t'' + t * t'' = t
⊢ s * (t' * t'') + t * t'' = t
have rw₁ : t * s'' + t * t'' = t
Tactic: rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
rw : s * t' * t'' + t * t'' = t
rw₁ : t * s'' + t * t'' = t
⊢ s * (t' * t'') + t * t'' = t
have rw₂ : t * (s'' + t'') = t
Tactic: rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
rw : s * t' * t'' + t * t'' = t
rw₁ : t * s'' + t * t'' = t
rw₂ : t * (s'' + t'') = t
⊢ s * (t' * t'') + t * t'' = t
have rw₃ : t * 1 = t
Tactic: rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
rw : s * t' * t'' + t * t'' = t
rw₁ : t * s'' + t * t'' = t
rw₂ : t * (s'' + t'') = t
rw₃ : t * 1 = t
⊢ s * (t' * t'') + t * t'' = t
have rw₄ : t = t
Tactic: rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)).weights =
    (convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h'')).weights
have this : s * (t' * t'') + t * t'' = t
Tactic: have : s * (t' * t'') + t * t'' = t := by rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ convexCombPair s t hs ht h (convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
have rw : sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)) =
  convexCombPair (s * s') (s * t' + t) sorry sorry sorry m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
Tactic: classical
  rw [convexCombPair_convexCombPair_left_eq_sConvexComb,
    convexCombPair_convexCombPair_right_eq_sConvexComb]
  congr 1
  ext1
  have : s * (t' * t'') + t * t'' = t := by rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]
  simp [convexCombPair, sum_add_index, add_smul, ← single_add, H, mul_assoc, ← mul_add, h'',
    add_assoc, this]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
rw :
  sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)) =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
⊢ convexCombPair s t hs ht h (convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
have rw₁ : sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)) =
  sConvexComb (convexCombPair (s * s') (s * t' + t) sorry sorry sorry (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h''))
Tactic: classical
  rw [convexCombPair_convexCombPair_left_eq_sConvexComb,
    convexCombPair_convexCombPair_right_eq_sConvexComb]
  congr 1
  ext1
  have : s * (t' * t'') + t * t'' = t := by rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]
  simp [convexCombPair, sum_add_index, add_smul, ← single_add, H, mul_assoc, ← mul_add, h'',
    add_assoc, this]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
rw :
  sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)) =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
rw₁ rw₂ rw₃ :
  sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)) =
    sConvexComb (convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h''))
⊢ convexCombPair s t hs ht h (convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
have e_f : convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃) =
  convexCombPair (s * s') (s * t' + t) sorry sorry sorry (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h'')
Tactic: classical
  rw [convexCombPair_convexCombPair_left_eq_sConvexComb,
    convexCombPair_convexCombPair_right_eq_sConvexComb]
  congr 1
  ext1
  have : s * (t' * t'') + t * t'' = t := by rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]
  simp [convexCombPair, sum_add_index, add_smul, ← single_add, H, mul_assoc, ← mul_add, h'',
    add_assoc, this]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
rw :
  sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)) =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
rw₁ rw₂ rw₃ :
  sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)) =
    sConvexComb (convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h''))
e_f :
  convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃) =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h'')
⊢ convexCombPair s t hs ht h (convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
have e_f₁ : (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)).weights =
  (convexCombPair (s * s') (s * t' + t) sorry sorry sorry (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h'')).weights
Tactic: classical
  rw [convexCombPair_convexCombPair_left_eq_sConvexComb,
    convexCombPair_convexCombPair_right_eq_sConvexComb]
  congr 1
  ext1
  have : s * (t' * t'') + t * t'' = t := by rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]
  simp [convexCombPair, sum_add_index, add_smul, ← single_add, H, mul_assoc, ← mul_add, h'',
    add_assoc, this]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
rw :
  sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)) =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
rw₁ rw₂ rw₃ :
  sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)) =
    sConvexComb (convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h''))
e_f :
  convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃) =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h'')
e_f₁ :
  (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)).weights =
    (convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h'')).weights
⊢ convexCombPair s t hs ht h (convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
have e_f₂ : ∀ (this : s * (t' * t'') + t * t'' = t),
  (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)).weights =
    (convexCombPair (s * s') (s * t' + t) sorry sorry sorry (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h'')).weights
Tactic: classical
  rw [convexCombPair_convexCombPair_left_eq_sConvexComb,
    convexCombPair_convexCombPair_right_eq_sConvexComb]
  congr 1
  ext1
  have : s * (t' * t'') + t * t'' = t := by rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]
  simp [convexCombPair, sum_add_index, add_smul, ← single_add, H, mul_assoc, ← mul_add, h'',
    add_assoc, this]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
⊢ s + t * s' + t * t' = 1
have rw : s + (t * s' + t * t') = 1
Tactic: rw [add_assoc, ← mul_add, h', mul_one, h]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
rw : s + (t * s' + t * t') = 1
⊢ s + t * s' + t * t' = 1
have rw₁ : s + t * (s' + t') = 1
Tactic: rw [add_assoc, ← mul_add, h', mul_one, h]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
rw : s + (t * s' + t * t') = 1
rw₁ : s + t * (s' + t') = 1
⊢ s + t * s' + t * t' = 1
have rw₂ : s + t * 1 = 1
Tactic: rw [add_assoc, ← mul_add, h', mul_one, h]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
rw : s + (t * s' + t * t') = 1
rw₁ : s + t * (s' + t') = 1
rw₂ : s + t * 1 = 1
rw₃ : s + t = 1
⊢ s + t * s' + t * t' = 1
have rw₄ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [add_assoc, ← mul_add, h', mul_one, h]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
⊢ convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    convexCombPair (s + t * s') (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
have simp : convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
  convexCombPair (t * s' + s) (t * t') sorry sorry sorry (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
Tactic: simp only [add_comm s]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
⊢ convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
have rw : convexCombPair t s ht hs sorry (convexCombPair s' t' hs' ht' h' m₂ m₃) m₁ =
  convexCombPair (t * s' + s) (t * t') sorry sorry sorry (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
Tactic: rw [convexCombPair_symm, convexCombPair_symm (x := m₂),
    convexCombPair_convexCombPair_assoc_left (hs'' := ht'') (ht'' := hs'')
      (h'' := (add_comm _ _).trans h'') (H := H),
    convexCombPair_symm, convexCombPair_symm (x := m₂)]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
rw :
  convexCombPair t s ht hs ⋯ (convexCombPair s' t' hs' ht' h' m₂ m₃) m₁ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
⊢ convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
have rw₁ : convexCombPair t s ht hs sorry (convexCombPair t' s' ht' hs' sorry m₃ m₂) m₁ =
  convexCombPair (t * s' + s) (t * t') sorry sorry sorry (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
Tactic: rw [convexCombPair_symm, convexCombPair_symm (x := m₂),
    convexCombPair_convexCombPair_assoc_left (hs'' := ht'') (ht'' := hs'')
      (h'' := (add_comm _ _).trans h'') (H := H),
    convexCombPair_symm, convexCombPair_symm (x := m₂)]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
rw :
  convexCombPair t s ht hs ⋯ (convexCombPair s' t' hs' ht' h' m₂ m₃) m₁ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
rw₁ :
  convexCombPair t s ht hs ⋯ (convexCombPair t' s' ht' hs' ⋯ m₃ m₂) m₁ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
⊢ convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
have rw₂ : convexCombPair (t * t') (t * s' + s) sorry sorry sorry m₃ (convexCombPair t'' s'' ht'' hs'' sorry m₂ m₁) =
  convexCombPair (t * s' + s) (t * t') sorry sorry sorry (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
Tactic: rw [convexCombPair_symm, convexCombPair_symm (x := m₂),
    convexCombPair_convexCombPair_assoc_left (hs'' := ht'') (ht'' := hs'')
      (h'' := (add_comm _ _).trans h'') (H := H),
    convexCombPair_symm, convexCombPair_symm (x := m₂)]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
rw :
  convexCombPair t s ht hs ⋯ (convexCombPair s' t' hs' ht' h' m₂ m₃) m₁ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
rw₁ :
  convexCombPair t s ht hs ⋯ (convexCombPair t' s' ht' hs' ⋯ m₃ m₂) m₁ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
rw₂ :
  convexCombPair (t * t') (t * s' + s) ⋯ ⋯ ⋯ m₃ (convexCombPair t'' s'' ht'' hs'' ⋯ m₂ m₁) =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
⊢ convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
have rw₃ : convexCombPair (t * s' + s) (t * t') sorry sorry sorry (convexCombPair t'' s'' ht'' hs'' sorry m₂ m₁) m₃ =
  convexCombPair (t * s' + s) (t * t') sorry sorry sorry (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
Tactic: rw [convexCombPair_symm, convexCombPair_symm (x := m₂),
    convexCombPair_convexCombPair_assoc_left (hs'' := ht'') (ht'' := hs'')
      (h'' := (add_comm _ _).trans h'') (H := H),
    convexCombPair_symm, convexCombPair_symm (x := m₂)]