awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (hypothesis)
Goal:
I : Type u_6
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
w : StdSimplex K I
s : Set I
hs : ∃ x ∈ s, Ne.{u_8 + 1} (α := K) ((w.weights : (a : I) → K) x : K) (0 : K)
hs' : ∃ x ∈ sᶜ, Ne.{u_8 + 1} (α := K) ((w.weights : (a : I) → K) x : K) (0 : K)
inst_3 : DecidablePred fun (x : I) ↦ x ∈ s
⊢ (convexCombPair ((filter (fun (x : I) ↦ x ∈ s) w.weights).sum fun (_x : I) (k : K) ↦ k)
        ((filter (fun (x : I) ↦ x ∉ s) w.weights).sum fun (_x : I) (k : K) ↦ k) ⋯ ⋯ ⋯ (w.restrict s hs)
        (w.restrict sᶜ hs')).weights =
    w.weights
have hs'₁ : ∃ x ∉ s, Ne.{u_8 + 1} (α := K) ((w.weights : (a : I) → K) x : K) (0 : K)
Tactic: simp only [Set.mem_compl_iff] at hs'
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
w : StdSimplex R I
f g : I → M
hfg : ∀ (i : I), Ne.{u_1 + 1} (α := R) ((w.weights : (a : I) → R) i : R) (0 : R) → f i = g i
⊢ iConvexComb w f = iConvexComb w g
have refine : map f w = map g w
Tactic: refine congr(sConvexComb $(?_))
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
w : StdSimplex R I
f g : I → M
hfg : ∀ (i : I), Ne.{u_1 + 1} (α := R) ((w.weights : (a : I) → R) i : R) (0 : R) → f i = g i
⊢ map f w = map g w
have a : ∀ (i : M), Eq.{u_1 + 1} (α := R) (((map f w).weights : (a : M) → R) i : R) (((map g w).weights : (a : M) → R) i : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
w : StdSimplex R I
f g : I → M
hfg : ∀ (i : I), Ne.{u_1 + 1} (α := R) ((w.weights : (a : I) → R) i : R) (0 : R) → f i = g i
i : M
⊢ Eq.{u_1 + 1} (α := R) (((map f w).weights : (a : M) → R) i : R) (((map g w).weights : (a : M) → R) i : R)
have a : Eq.{u_1 + 1} (α := R) ((mapDomain f w.weights : (a : M) → R) i : R) ((mapDomain g w.weights : (a : M) → R) i : R)
Tactic: simp only [weights_map]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
w : StdSimplex R I
f g : I → M
hfg : ∀ (i : I), Ne.{u_1 + 1} (α := R) ((w.weights : (a : I) → R) i : R) (0 : R) → f i = g i
i : M
⊢ Eq.{u_1 + 1} (α := R) ((mapDomain f w.weights : (a : M) → R) i : R) ((mapDomain g w.weights : (a : M) → R) i : R)
have a : mapDomain f w.weights = mapDomain g w.weights
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
w : StdSimplex R I
f g : I → M
hfg : ∀ (i : I), Ne.{u_1 + 1} (α := R) ((w.weights : (a : I) → R) i : R) (0 : R) → f i = g i
i : M
⊢ mapDomain f w.weights = mapDomain g w.weights
have a : ∀ (i : I) (hi : i ∈ w.weights.support), f i = g i
Tactic: refine Finsupp.mapDomain_congr fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
J : I → Type u_9
s : StdSimplex R I
f : (i : I) → StdSimplex.{u_1, u_9} R (J i)
g : (i : I) → J i → M
⊢ (iConvexComb s fun (i : I) ↦ iConvexComb (f i) (g i)) =
    iConvexComb (R := R) (iConvexComb s fun (i : I) ↦ map (fun (x : J i) ↦ Sigma.mk (β := J) i x) (f i))
      (Sigma.uncurry (β := J) (γ := fun (x : I) (y : J x) ↦ M) g)
have simp : sConvexComb (map (fun (i : I) ↦ sConvexComb (map (g i) (f i))) s) =
  sConvexComb.{u_1, u_3} (R := R)
    (map (Sigma.uncurry (β := J) (γ := fun (x : I) (y : J x) ↦ M) g)
      (sConvexComb (map (fun (i : I) ↦ map (fun (x : J i) ↦ Sigma.mk (β := J) i x) (f i)) s)))
Tactic: simp only [iConvexComb]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
J : I → Type u_9
s : StdSimplex R I
f : (i : I) → StdSimplex.{u_1, u_9} R (J i)
g : (i : I) → J i → M
⊢ sConvexComb (map (fun (i : I) ↦ sConvexComb (map (g i) (f i))) s) =
    sConvexComb.{u_1, u_3} (R := R)
      (map (Sigma.uncurry (β := J) (γ := fun (x : I) (y : J x) ↦ M) g)
        (sConvexComb (map (fun (i : I) ↦ map (fun (x : J i) ↦ Sigma.mk (β := J) i x) (f i)) s)))
have rw : sConvexComb.{u_1, u_3} (R := R) (sConvexComb (map (fun (i : I) ↦ map (g i) (f i)) s)) =
  sConvexComb.{u_1, u_3} (R := R)
    (map (Sigma.uncurry (β := J) (γ := fun (x : I) (y : J x) ↦ M) g)
      (sConvexComb (map (fun (i : I) ↦ map (fun (x : J i) ↦ Sigma.mk (β := J) i x) (f i)) s)))
Tactic: rw [← map_map, ← sConvexComb_sConvexComb]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
J : I → Type u_9
s : StdSimplex R I
f : (i : I) → StdSimplex.{u_1, u_9} R (J i)
g : (i : I) → J i → M
⊢ sConvexComb.{u_1, u_3} (R := R) (sConvexComb (map (fun (i : I) ↦ map (g i) (f i)) s)) =
    sConvexComb.{u_1, u_3} (R := R)
      (map (Sigma.uncurry (β := J) (γ := fun (x : I) (y : J x) ↦ M) g)
        (sConvexComb (map (fun (i : I) ↦ map (fun (x : J i) ↦ Sigma.mk (β := J) i x) (f i)) s)))
have e_f : Eq (α := StdSimplex R M) (sConvexComb (map (fun (i : I) ↦ map (g i) (f i)) s))
  (map (Sigma.uncurry (β := J) (γ := fun (x : I) (y : J x) ↦ M) g)
    (sConvexComb (map (fun (i : I) ↦ map (fun (x : J i) ↦ Sigma.mk (β := J) i x) (f i)) s)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : I → J → M
⊢ (iConvexComb s fun (i : I) ↦ iConvexComb (f i) (g i)) =
    iConvexComb (R := R) (iConvexComb s fun (i : I) ↦ map (fun (x : J) ↦ (i, x)) (f i)) (Function.uncurry g)
have simp : sConvexComb (map (fun (i : I) ↦ sConvexComb (map (g i) (f i))) s) =
  sConvexComb.{u_1, u_3} (R := R)
    (map (Function.uncurry g) (sConvexComb (map (fun (i : I) ↦ map (fun (x : J) ↦ (i, x)) (f i)) s)))
Tactic: simp only [iConvexComb]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : I → J → M
⊢ sConvexComb (map (fun (i : I) ↦ sConvexComb (map (g i) (f i))) s) =
    sConvexComb.{u_1, u_3} (R := R)
      (map (Function.uncurry g) (sConvexComb (map (fun (i : I) ↦ map (fun (x : J) ↦ (i, x)) (f i)) s)))
have rw : sConvexComb.{u_1, u_3} (R := R) (sConvexComb (map (fun (i : I) ↦ map (g i) (f i)) s)) =
  sConvexComb.{u_1, u_3} (R := R)
    (map (Function.uncurry g) (sConvexComb (map (fun (i : I) ↦ map (fun (x : J) ↦ (i, x)) (f i)) s)))
Tactic: rw [← map_map, ← sConvexComb_sConvexComb]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : I → J → M
⊢ sConvexComb.{u_1, u_3} (R := R) (sConvexComb (map (fun (i : I) ↦ map (g i) (f i)) s)) =
    sConvexComb.{u_1, u_3} (R := R)
      (map (Function.uncurry g) (sConvexComb (map (fun (i : I) ↦ map (fun (x : J) ↦ (i, x)) (f i)) s)))
have e_f : Eq (α := StdSimplex R M) (sConvexComb (map (fun (i : I) ↦ map (g i) (f i)) s))
  (map (Function.uncurry g) (sConvexComb (map (fun (i : I) ↦ map (fun (x : J) ↦ (i, x)) (f i)) s)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : J → M
⊢ (iConvexComb s fun (i : I) ↦ iConvexComb (f i) g) = iConvexComb (iConvexComb s f) g
have simp : sConvexComb (map (fun (i : I) ↦ sConvexComb (map g (f i))) s) = sConvexComb (map g (sConvexComb (map f s)))
Tactic: simp only [iConvexComb]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
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
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : J → M
⊢ sConvexComb (map (fun (i : I) ↦ sConvexComb (map g (f i))) s) = sConvexComb (map g (sConvexComb (map f s)))
have rw : sConvexComb.{u_1, u_3} (R := R) (sConvexComb (map (fun (i : I) ↦ map g (f i)) s)) =
  sConvexComb (map g (sConvexComb (map f s)))
Tactic: rw [← map_map, ← sConvexComb_sConvexComb]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
J : Type u_12
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
f : StdSimplex R I
g : StdSimplex R J
e : I → J → M
⊢ Eq.{u_10 + 1} (α := M) (iConvexComb f fun (i : I) ↦ iConvexComb g (e i))
    (iConvexComb g fun (j : J) ↦ iConvexComb f fun (i : I) ↦ e i j)
have rw : iConvexComb (R := R) (I := J × I)
    (map (M := I × J) (⇑(Equiv.prodComm I J) : (a : I × J) → J × I)
      (iConvexComb f fun (i : I) ↦ map (fun (x : J) ↦ (i, x)) g))
    (Function.uncurry e ∘ (⇑(Equiv.prodComm I J).symm : (a : J × I) → I × J)) =
  iConvexComb (R := R) (I := J × I) (iConvexComb g fun (i : J) ↦ map (fun (x : I) ↦ (i, x)) f)
    (Function.uncurry fun (j : J) (i : I) ↦ e i j)
Tactic: rw [iConvexComb_assoc', iConvexComb_assoc', iConvexComb_reindex _ (.prodComm ..)]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
J : Type u_12
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
f : StdSimplex R I
g : StdSimplex R J
e : I → J → M
⊢ iConvexComb (R := R) (I := J × I)
      (map (M := I × J) (⇑(Equiv.prodComm I J) : (a : I × J) → J × I)
        (iConvexComb f fun (i : I) ↦ map (fun (x : J) ↦ (i, x)) g))
      (Function.uncurry e ∘ (⇑(Equiv.prodComm I J).symm : (a : J × I) → I × J)) =
    iConvexComb (R := R) (I := J × I) (iConvexComb g fun (i : J) ↦ map (fun (x : I) ↦ (i, x)) f)
      (Function.uncurry fun (j : J) (i : I) ↦ e i j)
have e_s : Eq (α := StdSimplex R (J × I))
  (map (M := I × J) (⇑(Equiv.prodComm I J) : (a : I × J) → J × I)
    (iConvexComb f fun (i : I) ↦ map (fun (x : J) ↦ (i, x)) g))
  (iConvexComb g fun (i : J) ↦ map (fun (x : I) ↦ (i, x)) f)
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
J : Type u_12
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
f : StdSimplex R I
g : StdSimplex R J
e : I → J → M
⊢ Eq (α := StdSimplex R (J × I))
    (map (M := I × J) (⇑(Equiv.prodComm I J) : (a : I × J) → J × I)
      (iConvexComb f fun (i : I) ↦ map (fun (x : J) ↦ (i, x)) g))
    (iConvexComb g fun (i : J) ↦ map (fun (x : I) ↦ (i, x)) f)
have e_s : Eq (α := StdSimplex R (J × I)) (sConvexComb (map (fun (x : I) ↦ map (fun (x_1 : J) ↦ (x_1, x)) g) f))
  (sConvexComb (map ((fun (g : I → J × I) ↦ map g f) ∘ Prod.mk) g))
Tactic: suffices (f.map fun x ↦ g.map (Prod.mk · x)).sConvexComb =
      (g.map (f.map ∘ Prod.mk)).sConvexComb by
    simpa [iConvexComb, map_sConvexComb, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
J : Type u_12
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
f : StdSimplex R I
g : StdSimplex R J
e : I → J → M
⊢ Eq (α := StdSimplex R (J × I)) (sConvexComb (map (fun (x : I) ↦ map (fun (x_1 : J) ↦ (x_1, x)) g) f))
    (sConvexComb (map ((fun (g : I → J × I) ↦ map g f) ∘ Prod.mk) g))
have e_s : Eq (α := J × I →₀ R) (weights (sConvexComb (map (fun (x : I) ↦ map (fun (x_1 : J) ↦ (x_1, x)) g) f)))
  (weights (sConvexComb (map ((fun (g : I → J × I) ↦ map g f) ∘ Prod.mk) g)))
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
x : M
⊢ convexCombPair s t hs ht h x x = x
have unfold : sConvexComb (duple x x hs ht h) = x
Tactic: unfold convexCombPair
-- 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
x : M
⊢ sConvexComb (duple x x hs ht h) = x
have h₁ : duple x x hs ht h = StdSimplex.single x
Tactic: convert sConvexComb_single x
-- 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
x y : M
⊢ convexCombPair s t hs ht h x y = convexCombPair t s ht hs ⋯ y x
have unfold : sConvexComb (duple x y hs ht h) = sConvexComb (duple y x ht hs sorry)
Tactic: unfold convexCombPair
-- 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
x y : M
⊢ sConvexComb (duple x y hs ht h) = sConvexComb (duple y x ht hs ⋯)
have e_f : duple x y hs ht h = duple y x ht hs sorry
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
x y : M
⊢ duple x y hs ht h = duple y x ht hs ⋯
have e_f : (duple x y hs ht h).weights = (duple y x ht hs sorry).weights
Tactic: ext1
-- 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
J₁ : Type u₁
J₂ : Type u₂
g₁ : StdSimplex R J₁
g₂ : StdSimplex R J₂
m₁ : J₁ → M
m₂ : J₂ → M
⊢ 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₂))
have 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))))
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))
-- 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
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))))
⊢ 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₂))
have 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)))
Tactic: simp [iConvexComb, map_sConvexComb, map_map, Sigma.uncurry] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (hypothesis)
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) ↦ 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) ⋯ ⋯ ⋯))
have this : Eq.{u_3 + 1} (α := M) (iConvexComb f fun (i : I) ↦ iConvexComb (duple 0 1 sorry sorry sorry) ![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 sorry sorry sorry))
    (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])
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (hypothesis)
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) (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) ⋯ ⋯ ⋯))
have this₁ : Eq.{u_3 + 1} (α := M) (sConvexComb (map (fun (i : I) ↦ sConvexComb (duple (m₁ i) (m₂ i) sorry sorry sorry)) f))
  (sConvexComb.{u_1, u_3} (R := R) (sConvexComb (map (fun (x : I) ↦ duple (m₁ x) (m₂ x) sorry sorry sorry) f)))
Tactic: simp [iConvexComb, map_sConvexComb, map_map] at this
Cleared hypotheses: 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 : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ s * s' + (s * t' + t) = 1
have rw : s * s' + 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 : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
rw : s * s' + s * t' + t = 1
⊢ s * s' + (s * t' + t) = 1
have rw₁ : s * (s' + t') + t = 1
Tactic: rw [← add_assoc, ← mul_add, h', mul_one, h]