awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
x : M
h₁ : duple x x hs ht h = StdSimplex.single x
⊢ sConvexComb (duple x x hs ht h) = x

Tactic:
convert sConvexComb_single x

Premises used: Convexity.ConvexSpace.sConvexComb_single
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
x : M
⊢ duple x x hs ht h = StdSimplex.single x

Tactic:
simp only [StdSimplex.duple, StdSimplex.single, ← single_add, h]

Premises used: Convexity.StdSimplex.duple, Convexity.StdSimplex.single, Finsupp.single_add
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
x y : M
unfold : sConvexComb (duple x y hs ht h) = sConvexComb (duple y x ht hs ⋯)
⊢ convexCombPair s t hs ht h x y = convexCombPair t s ht hs ⋯ y x

Tactic:
unfold convexCombPair

Premises used: Convexity.convexCombPair
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
x y : M
e_f : duple x y hs ht h = duple y x ht hs ⋯
⊢ sConvexComb (duple x y hs ht h) = sConvexComb (duple y x ht hs ⋯)

Tactic:
congr 1
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
x y : M
e_f : (duple x y hs ht h).weights = (duple y x ht hs ⋯).weights
⊢ duple x y hs ht h = duple y x ht hs ⋯

Tactic:
ext1
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
x y : M
⊢ (duple x y hs ht h).weights = (duple y x ht hs ⋯).weights

Tactic:
simp [StdSimplex.duple, add_comm]

Premises used: Convexity.StdSimplex.duple, add_comm
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
f : M → N
hf : IsAffineMap R f
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : M
⊢ f (convexCombPair s t hs ht h x y) = convexCombPair s t hs ht h (f x) (f y)

Tactic:
simp [hf.map_sConvexComb, convexCombPair]

Premises used: Convexity.IsAffineMap.map_sConvexComb, Convexity.convexCombPair
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
J₁ : Type u₁
J₂ : Type u₂
g₁ : StdSimplex R J₁
g₂ : StdSimplex R J₂
m₁ : J₁ → M
m₂ : J₂ → M
⊢ Eq.{u_3 + 1} (α := M)
    (iConvexComb (duple 0 1 hs ht h) fun (i : Fin 2) ↦
      iConvexComb (R := R) (I := ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i)
        (Fin.cons (α := fun (i : Fin 2) ↦ StdSimplex R (![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i))
          (map ULift.up g₁)
          (Fin.cons (α := fun (i : Fin 1) ↦ StdSimplex R (![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i.succ))
            (map ULift.up g₂) fun (a : Fin 0) ↦ nomatch a)
          i)
        (Fin.cons (α := fun (i : Fin 2) ↦ ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i → M) (m₁ ∘ ULift.down)
          (Fin.cons (α := fun (i : Fin 1) ↦ ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i.succ → M)
            (m₂ ∘ ULift.down)
            fun (a : Fin 0) (a_1 : ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] a.succ.succ) ↦ nomatch a, a_1)
          i))
    (iConvexComb (R := R) (I := Sigma ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂])
      (iConvexComb (duple 0 1 hs ht h) fun (i : Fin 2) ↦
        map
          (fun (x : ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i) ↦
            Sigma.mk (β := ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂]) i x)
          (Fin.cons (α := fun (i : Fin 2) ↦ StdSimplex R (![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i))
            (map ULift.up g₁)
            (Fin.cons (α := fun (i : Fin 1) ↦
              StdSimplex R (![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i.succ)) (map ULift.up g₂)
              fun (a : Fin 0) ↦ nomatch a)
            i))
      (Sigma.uncurry (β := ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂]) (γ :=
        fun (x : Fin 2) (y : ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] x) ↦ M)
        (Fin.cons (α := fun (i : Fin 2) ↦ ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i → M) (m₁ ∘ ULift.down)
          (Fin.cons (α := fun (i : Fin 1) ↦ ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i.succ → M)
            (m₂ ∘ ULift.down)
            fun (a : Fin 0) (a_1 : ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] a.succ.succ) ↦
            nomatch a, a_1))))

Tactic:
have := iConvexComb_assoc'' (I := Fin 2) (.duple 0 1 hs ht h)
    (J := ![ULift.{max u₁ u₂} J₁, ULift.{max u₁ u₂} J₂])
    (M := M) (Fin.cons (g₁.map ULift.up) (Fin.cons (g₂.map ULift.up) nofun))
    (Fin.cons (m₁ ∘ ULift.down) (Fin.cons (m₂ ∘ ULift.down) nofun))
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
J₁ : Type u₁
J₂ : Type u₂
g₁ : StdSimplex R J₁
g₂ : StdSimplex R J₂
m₁ : J₁ → M
m₂ : J₂ → M
this :
  Eq.{u_3 + 1} (α := M)
    (iConvexComb (duple 0 1 hs ht h) fun (i : Fin 2) ↦
      iConvexComb (R := R) (I := ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i)
        (Fin.cons (α := fun (i : Fin 2) ↦ StdSimplex R (![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i))
          (map ULift.up g₁)
          (Fin.cons (α := fun (i : Fin 1) ↦ StdSimplex R (![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i.succ))
            (map ULift.up g₂) fun (a : Fin 0) ↦ nomatch a)
          i)
        (Fin.cons (α := fun (i : Fin 2) ↦ ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i → M) (m₁ ∘ ULift.down)
          (Fin.cons (α := fun (i : Fin 1) ↦ ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i.succ → M)
            (m₂ ∘ ULift.down)
            fun (a : Fin 0) (a_1 : ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] a.succ.succ) ↦ nomatch a, a_1)
          i))
    (iConvexComb (R := R) (I := Sigma ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂])
      (iConvexComb (duple 0 1 hs ht h) fun (i : Fin 2) ↦
        map
          (fun (x : ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i) ↦
            Sigma.mk (β := ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂]) i x)
          (Fin.cons (α := fun (i : Fin 2) ↦ StdSimplex R (![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i))
            (map ULift.up g₁)
            (Fin.cons (α := fun (i : Fin 1) ↦
              StdSimplex R (![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i.succ)) (map ULift.up g₂)
              fun (a : Fin 0) ↦ nomatch a)
            i))
      (Sigma.uncurry (β := ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂]) (γ :=
        fun (x : Fin 2) (y : ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] x) ↦ M)
        (Fin.cons (α := fun (i : Fin 2) ↦ ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i → M) (m₁ ∘ ULift.down)
          (Fin.cons (α := fun (i : Fin 1) ↦ ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] i.succ → M)
            (m₂ ∘ ULift.down)
            fun (a : Fin 0) (a_1 : ![ULift.{max u₁ u₂, u₁} J₁, ULift.{max u₁ u₂, u₂} J₂] a.succ.succ) ↦
            nomatch a, a_1))))
⊢ Eq.{u_3 + 1} (α := M)
    (sConvexComb
      (duple (sConvexComb (map (fun (x : J₁) ↦ m₁ x) g₁)) (sConvexComb (map (fun (x : J₂) ↦ m₂ x) g₂)) hs ht h))
    (sConvexComb (sConvexComb (duple (map (fun (x : J₁) ↦ m₁ x) g₁) (map (fun (x : J₂) ↦ m₂ x) g₂) hs ht h)))

Tactic:
simp [iConvexComb, map_sConvexComb, map_map, Sigma.uncurry] at this

Premises used: Sigma.uncurry, Convexity.StdSimplex.map_map, Convexity.iConvexComb, Convexity.StdSimplex.map_sConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
J₁ : Type u₁
J₂ : Type u₂
g₁ : StdSimplex R J₁
g₂ : StdSimplex R J₂
m₁ : J₁ → M
m₂ : J₂ → M
this :
  Eq.{u_3 + 1} (α := M)
    (sConvexComb
      (duple (sConvexComb (map (fun (x : J₁) ↦ m₁ x) g₁)) (sConvexComb (map (fun (x : J₂) ↦ m₂ x) g₂)) hs ht h))
    (sConvexComb (sConvexComb (duple (map (fun (x : J₁) ↦ m₁ x) g₁) (map (fun (x : J₂) ↦ m₂ x) g₂) hs ht h)))
⊢ convexCombPair s t hs ht h (iConvexComb g₁ m₁) (iConvexComb g₂ m₂) =
    sConvexComb (convexCombPair s t hs ht h (map m₁ g₁) (map m₂ g₂))

Tactic:
simpa [convexCombPair, ← convexCombPair_def]

Premises used: Convexity.convexCombPair_def, Convexity.convexCombPair
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
I : Type u_6
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : I → R
hs : ∀ (i : I), 0 ≤ s i
ht : ∀ (i : I), 0 ≤ t i
h : ∀ (i : I), s i + t i = 1
f : StdSimplex R I
m₁ m₂ : I → M
⊢ Eq.{u_3 + 1} (α := M) (iConvexComb f fun (i : I) ↦ iConvexComb (duple 0 1 ⋯ ⋯ ⋯) ![m₁ i, m₂ i])
    (iConvexComb.{u_1, u_3, u_6} (R := R) (I := I × Fin 2)
      (iConvexComb f fun (i : I) ↦ map (fun (x : Fin 2) ↦ (i, x)) (duple 0 1 ⋯ ⋯ ⋯))
      (Function.uncurry fun (i : I) ↦ ![m₁ i, m₂ i]))

Tactic:
have := iConvexComb_assoc' (I := I) (J := Fin 2) (R := R) (M := M) f
    (fun i ↦ .duple 0 1 (hs i) (ht i) (h i)) (fun i ↦ ![m₁ i, m₂ i])
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
I : Type u_6
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : I → R
hs : ∀ (i : I), 0 ≤ s i
ht : ∀ (i : I), 0 ≤ t i
h : ∀ (i : I), s i + t i = 1
f : StdSimplex R I
m₁ m₂ : I → M
this :
  Eq.{u_3 + 1} (α := M) (iConvexComb f fun (i : I) ↦ iConvexComb (duple 0 1 ⋯ ⋯ ⋯) ![m₁ i, m₂ i])
    (iConvexComb.{u_1, u_3, u_6} (R := R) (I := I × Fin 2)
      (iConvexComb f fun (i : I) ↦ map (fun (x : Fin 2) ↦ (i, x)) (duple 0 1 ⋯ ⋯ ⋯))
      (Function.uncurry fun (i : I) ↦ ![m₁ i, m₂ i]))
⊢ Eq.{u_3 + 1} (α := M) (sConvexComb (map (fun (i : I) ↦ sConvexComb (duple (m₁ i) (m₂ i) ⋯ ⋯ ⋯)) f))
    (sConvexComb.{u_1, u_3} (R := R) (sConvexComb (map (fun (x : I) ↦ duple (m₁ x) (m₂ x) ⋯ ⋯ ⋯) f)))

Tactic:
simp [iConvexComb, map_sConvexComb, map_map] at this

Premises used: Convexity.StdSimplex.map_map, Convexity.iConvexComb, Convexity.StdSimplex.map_sConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
I : Type u_6
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : I → R
hs : ∀ (i : I), 0 ≤ s i
ht : ∀ (i : I), 0 ≤ t i
h : ∀ (i : I), s i + t i = 1
f : StdSimplex R I
m₁ m₂ : I → M
this :
  Eq.{u_3 + 1} (α := M) (iConvexComb f fun (i : I) ↦ convexCombPair (s i) (t i) ⋯ ⋯ ⋯ (m₁ i) (m₂ i))
    (sConvexComb.{u_1, u_3} (R := R) (iConvexComb f fun (x : I) ↦ duple (m₁ x) (m₂ x) ⋯ ⋯ ⋯))
⊢ Eq.{u_3 + 1} (α := M) (iConvexComb f fun (i : I) ↦ convexCombPair (s i) (t i) ⋯ ⋯ ⋯ (m₁ i) (m₂ i))
    (sConvexComb.{u_1, u_3} (R := R) (iConvexComb f fun (i : I) ↦ duple (m₁ i) (m₂ i) ⋯ ⋯ ⋯))

Tactic:
simpa [convexCombPair, ← convexCombPair_def]

Premises used: Convexity.convexCombPair_def, Convexity.convexCombPair
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
J : Type u_7
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
g : StdSimplex R J
e : J → M
m : M
⊢ convexCombPair s t hs ht h (iConvexComb g e) m =
    sConvexComb (convexCombPair s t hs ht h (map e g) (StdSimplex.single m))

Tactic:
simpa using convexCombPair_iConvexComb_iConvexComb hs ht h g g e (fun _ ↦ m)

Premises used: Convexity.convexCombPair_iConvexComb_iConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
J : Type u_7
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
m : M
g : StdSimplex R J
e : J → M
⊢ convexCombPair s t hs ht h m (iConvexComb g e) =
    sConvexComb (convexCombPair s t hs ht h (StdSimplex.single m) (map e g))

Tactic:
simpa using convexCombPair_iConvexComb_iConvexComb hs ht h g g (fun _ ↦ m) e

Premises used: Convexity.convexCombPair_iConvexComb_iConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
m₁ m₂ m₃ : M
⊢ convexCombPair s t hs ht h (convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ =
    sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃))

Tactic:
simpa using convexCombPair_iConvexComb_left hs ht h (.duple m₁ m₂ hs' ht' h') id m₃

Premises used: Convexity.StdSimplex.duple, id, Convexity.convexCombPair_iConvexComb_left
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
m₁ m₂ m₃ : M
⊢ convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    sConvexComb (convexCombPair s t hs ht h (StdSimplex.single m₁) (duple m₂ m₃ hs' ht' h'))

Tactic:
simpa using convexCombPair_iConvexComb_right hs ht h m₁ (.duple m₂ m₃ hs' ht' h') id

Premises used: Convexity.StdSimplex.duple, id, Convexity.convexCombPair_iConvexComb_right
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
⊢ 0 ≤ s * s'

Tactic:
positivity
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
⊢ 0 ≤ s * t' + t

Tactic:
positivity
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
rw₄ rw₅ : Eq.{u_1 + 1} (α := R) 1 1
⊢ s * s' + (s * t' + t) = 1

Tactic:
rw [← add_assoc, ← mul_add, h', mul_one, h]

Premises used: add_assoc, mul_add, mul_one
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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₃)) =
    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₃)

Tactic:
rw [convexCombPair_convexCombPair_left_eq_sConvexComb,
    convexCombPair_convexCombPair_right_eq_sConvexComb]

Premises used: Convexity.convexCombPair_convexCombPair_left_eq_sConvexComb, Convexity.convexCombPair_convexCombPair_right_eq_sConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
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'')
⊢ 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''))

Tactic:
congr 1
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
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 (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃) =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h'')

Tactic:
ext1
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
rw₄ rw₅ : t = t
⊢ s * (t' * t'') + t * t'' = t

Tactic:
rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]

Premises used: mul_assoc, mul_add, mul_one
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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

Tactic:
have : s * (t' * t'') + t * t'' = t := by rw [← mul_assoc, ← H, ← mul_add, h'', mul_one]
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
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) ⋯ ⋯ ⋯ (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h'')).weights

Tactic:
simp [convexCombPair, sum_add_index, add_smul, ← single_add, H, mul_assoc, ← mul_add, h'',
    add_assoc, this]

Premises used: add_assoc, mul_assoc, add_smul, Finsupp.single_add, mul_add, Finsupp.sum_add_index, Convexity.convexCombPair
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
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) ⋯ ⋯ ⋯ (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₃)

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]

Premises used: add_assoc, mul_assoc, Convexity.convexCombPair_convexCombPair_left_eq_sConvexComb, add_smul, Finsupp.single_add, mul_add, Finsupp.sum_add_index, Convexity.convexCombPair, Convexity.convexCombPair_convexCombPair_right_eq_sConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
⊢ 0 ≤ s + t * s'

Tactic:
positivity
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
⊢ 0 ≤ t * t'

Tactic:
positivity