awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : I
f : I → M
⊢ iConvexComb.{u_1, u_3, u_6} (R := R) (StdSimplex.single i) f = f i

Tactic:
simp [iConvexComb]

Premises used: Convexity.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
w : StdSimplex R M
⊢ iConvexComb w id = sConvexComb w

Tactic:
simp [iConvexComb]

Premises used: Convexity.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
w : StdSimplex R M
⊢ (iConvexComb w fun (x : M) ↦ x) = sConvexComb w

Tactic:
iConvexComb_id _

Premises used: Convexity.iConvexComb_id
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
I : Type u_6
J : Type u_7
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s : StdSimplex R I
f : I → J
g : J → M
⊢ iConvexComb (map f s) g = iConvexComb s fun (i : I) ↦ g (f i)

Tactic:
simp only [iConvexComb, map_map]

Premises used: Convexity.StdSimplex.map_map, Convexity.iConvexComb
-- 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
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

Tactic:
congr(sConvexComb $(?_))

Premises used: congrArg, id, Convexity.ConvexSpace.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
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
refine : map f w = map g w
⊢ iConvexComb w f = iConvexComb w g

Tactic:
refine congr(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
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
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)
⊢ map f w = map g w

Tactic:
ext 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
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
a : Eq.{u_1 + 1} (α := R) ((mapDomain f w.weights : (a : M) → R) i : R) ((mapDomain g w.weights : (a : M) → R) i : R)
⊢ Eq.{u_1 + 1} (α := R) (((map f w).weights : (a : M) → R) i : R) (((map g w).weights : (a : M) → R) i : R)

Tactic:
simp only [weights_map]

Premises used: Convexity.StdSimplex.weights_map
-- 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
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
a : mapDomain f w.weights = mapDomain g w.weights
⊢ Eq.{u_1 + 1} (α := R) ((mapDomain f w.weights : (a : M) → R) i : R) ((mapDomain g w.weights : (a : M) → R) i : R)

Tactic:
congr 1
-- 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
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

Tactic:
Finsupp.mapDomain_congr fun i hi ↦ ?_

Premises used: Finsupp.mapDomain_congr
-- 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
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
a : ∀ (i : I) (hi : i ∈ w.weights.support), f i = g i
⊢ mapDomain f w.weights = mapDomain g w.weights

Tactic:
refine Finsupp.mapDomain_congr fun i hi ↦ ?_

Premises used: Finsupp.mapDomain_congr
-- 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
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_1 : M
i : I
hi : i ∈ w.weights.support
⊢ Ne.{u_1 + 1} (α := R) ((w.weights : (a : I) → R) i : R) (0 : R)

Tactic:
simpa using hi
-- 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
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_1 : M
i : I
hi : i ∈ w.weights.support
⊢ f i = g i

Tactic:
exact hfg i (by simpa using hi)
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
I : Type u_6
J : Type u_7
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s : StdSimplex R I
f : I ≃ J
g : I → M
⊢ iConvexComb s g = iConvexComb.{u_1, u_3, u_7} (I := J) (map (⇑f : (a : I) → J) s) (g ∘ (⇑f.symm : (a : J) → I))

Tactic:
simp [iConvexComb_map]

Premises used: Convexity.iConvexComb_map
-- 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
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
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)))
⊢ (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)

Tactic:
simp only [iConvexComb]

Premises used: Convexity.iConvexComb
-- 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
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
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)))
⊢ 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:
rw [← map_map, ← sConvexComb_sConvexComb]

Premises used: Convexity.StdSimplex.map_map, Convexity.sConvexComb_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
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
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)))
⊢ 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:
congr 1
-- 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
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
⊢ 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:
simp [map_sConvexComb, map_map, Sigma.uncurry]

Premises used: Sigma.uncurry, Convexity.StdSimplex.map_map, 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
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : I → J → M
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)))
⊢ (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)

Tactic:
simp only [iConvexComb]

Premises used: Convexity.iConvexComb
-- 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
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : I → J → M
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)))
⊢ 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:
rw [← map_map, ← sConvexComb_sConvexComb]

Premises used: Convexity.StdSimplex.map_map, Convexity.sConvexComb_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
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : I → J → M
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)))
⊢ 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:
congr 1
-- 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
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : I → J → M
⊢ 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:
simp [map_sConvexComb, map_map, Function.uncurry]

Premises used: Convexity.StdSimplex.map_map, Function.uncurry, 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
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : J → M
simp : sConvexComb (map (fun (i : I) ↦ sConvexComb (map g (f i))) s) = sConvexComb (map g (sConvexComb (map f s)))
⊢ (iConvexComb s fun (i : I) ↦ iConvexComb (f i) g) = iConvexComb (iConvexComb s f) g

Tactic:
simp only [iConvexComb]

Premises used: Convexity.iConvexComb
-- 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
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : J → M
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)))
⊢ sConvexComb (map (fun (i : I) ↦ sConvexComb (map g (f i))) s) = sConvexComb (map g (sConvexComb (map f s)))

Tactic:
rw [← map_map, ← sConvexComb_sConvexComb]

Premises used: Convexity.StdSimplex.map_map, Convexity.sConvexComb_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
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : J → M
⊢ 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:
simp [map_sConvexComb, map_map]

Premises used: Convexity.StdSimplex.map_map, Convexity.StdSimplex.map_sConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
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)
⊢ 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)

Tactic:
rw [iConvexComb_assoc', iConvexComb_assoc', iConvexComb_reindex _ (.prodComm ..)]

Premises used: Equiv.prodComm, Convexity.iConvexComb_assoc', Convexity.iConvexComb_reindex
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
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)
⊢ 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:
congr
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
this :
  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))
⊢ 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:
simpa [iConvexComb, map_sConvexComb, map_map, Function.comp_def]

Premises used: Convexity.StdSimplex.map_map, Function.comp_def, Convexity.iConvexComb, Convexity.StdSimplex.map_sConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
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))
⊢ 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:
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]
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
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)))
⊢ 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:
ext1
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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 (α := 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:
simp [mapDomain, sum_sum_index, add_smul, smul_sum, mul_comm, sum_comm f.weights g.weights]

Premises used: Finsupp.sum_comm, Finsupp.mapDomain, Convexity.StdSimplex.weights, add_smul, mul_comm, Finsupp.smul_sum, Finsupp.sum_sum_index
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
I : Type u_6
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 : StdSimplex R I
g : I → M
⊢ f (iConvexComb s g) = iConvexComb s (f ∘ g)

Tactic:
simp [iConvexComb, hf.map_sConvexComb, map_comp]

Premises used: Convexity.StdSimplex.map_comp, Convexity.iConvexComb, Convexity.IsAffineMap.map_sConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
f : J → K
s : StdSimplex R I
g : I → StdSimplex R J
⊢ map f (iConvexComb s g) = iConvexComb s (map f ∘ g)

Tactic:
(isAffineMap_map R f).map_iConvexComb s g

Premises used: Convexity.IsAffineMap.map_iConvexComb, Convexity.StdSimplex.isAffineMap_map
-- 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
p q : M
⊢ convexCombPair s t hs ht h p q = iConvexComb (duple 0 1 hs ht h) ![p, q]

Tactic:
simp [StdSimplex.iConvexComb, convexCombPair]

Premises used: Convexity.iConvexComb, Convexity.convexCombPair
-- 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
x y : M
⊢ LE.le.{u_1} (α := R) 0 0

Tactic:
simp
-- 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
x y : M
⊢ LE.le.{u_1} (α := R) 0 1

Tactic:
simp
-- 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
x y : M
⊢ HAdd.hAdd (α := R) 0 1 = 1

Tactic:
simp
-- 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
x y : M
⊢ convexCombPair.{u_1, u_3} (R := R) 0 1 ⋯ ⋯ ⋯ x y = y

Tactic:
simp [convexCombPair, StdSimplex.duple, StdSimplex.mk_single]

Premises used: Convexity.StdSimplex.duple, Convexity.StdSimplex.mk_single, Convexity.convexCombPair
-- 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
x y : M
⊢ HAdd.hAdd (α := R) 1 0 = 1

Tactic:
simp
-- 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
x y : M
⊢ convexCombPair.{u_1, u_3} (R := R) 1 0 ⋯ ⋯ ⋯ x y = x

Tactic:
simp [convexCombPair, StdSimplex.duple, StdSimplex.mk_single]

Premises used: Convexity.StdSimplex.duple, Convexity.StdSimplex.mk_single, 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 : M
unfold : sConvexComb (duple x x hs ht h) = x
⊢ convexCombPair s t hs ht h x x = 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 : M
⊢ sConvexComb.{u_1, u_3} (R := R) (StdSimplex.single x) = x

Tactic:
sConvexComb_single x

Premises used: Convexity.ConvexSpace.sConvexComb_single