awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
z : H ⊗[R] G
hz :
  ∀ (φ : Dual R H),
    Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) φ →
      ∀ (ψ : Dual R G),
        Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) ψ →
          LE.le.{u_1} (α := R) (0 : R)
            ((((dualDistrib R H G : (a : Dual R H ⊗[R] Dual R G) → Dual R (H ⊗[R] G)) (φ ⊗ₜ[R] ψ) : Dual R (H ⊗[R] G)) :
                  (a : H ⊗[R] G) → R)
                z :
              R)
φ : Dual R G
hφ : Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) φ
ψ : Dual R H
hψ : Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) ψ
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) (φ ⊗ₜ[R] ψ) : Dual R (G ⊗[R] H)) :
          (a : G ⊗[R] H) → R)
        ((TensorProduct.comm R H G : (a : H ⊗[R] G) → G ⊗[R] H) z : G ⊗[R] H) :
      R)

Tactic:
simpa [dualDistrib_apply_comm] using hz ψ hψ φ hφ

Premises used: TensorProduct.dualDistrib_apply_comm
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
C₁ C₁' : PointedCone R G
C₂ C₂' : PointedCone R H
h₁ : C₁ ≤ C₁'
h₂ : C₂ ≤ C₂'
⊢ LE.le (α := PointedCone R (G ⊗[R] H)) (C₁.minTensorProduct C₂ : PointedCone R (G ⊗[R] H))
    (C₁'.minTensorProduct C₂' : PointedCone R (G ⊗[R] H))

Tactic:
Submodule.span_mono <| Set.image2_subset h₁ h₂

Premises used: Set.image2_subset, Set.Mem, Submodule.span_mono
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
C₁ C₁' : PointedCone R G
C₂ C₂' : PointedCone R H
h₁ : C₁ ≤ C₁'
h₂ : C₂ ≤ C₂'
⊢ LE.le (α := PointedCone R (G ⊗[R] H)) (C₁.maxTensorProduct C₂ : PointedCone R (G ⊗[R] H))
    (C₁'.maxTensorProduct C₂' : PointedCone R (G ⊗[R] H))

Tactic:
fun _ hz => mem_maxTensorProduct.mpr fun φ hφ ψ hψ =>
    mem_maxTensorProduct.mp hz φ (dual_le_dual h₁ hφ) ψ (dual_le_dual h₂ hψ)

Premises used: Iff.mpr, Set.Mem, PointedCone.dual_le_dual, Iff.mp, PointedCone.mem_maxTensorProduct
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
G' : Type u_4
H' : Type u_5
inst_7 : AddCommGroup G'
inst_8 : Module R G'
inst_9 : AddCommGroup H'
inst_10 : Module R H'
f : G →ₗ[R] G'
g : H →ₗ[R] H'
C₁ : PointedCone R G
C₂ : PointedCone R H
⊢ LE.le (α := PointedCone R (G' ⊗[R] H'))
    (map (TensorProduct.map f g) (C₁.minTensorProduct C₂) : PointedCone R (G' ⊗[R] H'))
    ((map f C₁).minTensorProduct (map g C₂) : PointedCone R (G' ⊗[R] H'))

Tactic:
(Submodule.map_span_le _ _ _).mpr fun _ ⟨x, hx, y, hy, h⟩ ↦
    h ▸ map_tmul f g x y ▸ tmul_mem_minTensorProduct ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩

Premises used: Iff.mpr, PointedCone.map, LinearMap.restrictScalars, Submodule.map_span_le, Set.Mem, PointedCone.minTensorProduct, setOf, Membership.mem, Eq.rec, Subtype, LE.le, TensorProduct.map, And.intro, _private.0.PointedCone.minTensorProduct_map_le.match_1, TensorProduct.map_tmul, Exists.intro, PointedCone.tmul_mem_minTensorProduct, OfNat.ofNat, Eq.symm, DFunLike.coe, rfl
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
G' : Type u_4
H' : Type u_5
inst_7 : AddCommGroup G'
inst_8 : Module R G'
inst_9 : AddCommGroup H'
inst_10 : Module R H'
f : G →ₗ[R] G'
g : H →ₗ[R] H'
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw :
  ∀ (φ : Dual R G),
    Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) φ →
      ∀ (ψ : Dual R H),
        Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) ψ →
          LE.le.{u_1} (α := R) (0 : R)
            ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) (φ ⊗ₜ[R] ψ) : Dual R (G ⊗[R] H)) :
                  (a : G ⊗[R] H) → R)
                w :
              R)
φ : Dual R G'
hφ : Membership.mem (γ := PointedCone R (Dual R G')) (dual (Dual.eval R G') (↑(map f C₁) : Set G')) φ
ψ : Dual R H'
hψ : Membership.mem (γ := PointedCone R (Dual R H')) (dual (Dual.eval R H') (↑(map g C₂) : Set H')) ψ
x : G
y : H
⊢ Eq.{u_1 + 1} (α := R)
    (((dualDistrib R G' H' : (a : Dual R G' ⊗[R] Dual R H') → Dual R (G' ⊗[R] H')) (φ ⊗ₜ[R] ψ) ∘ₗ
            TensorProduct.map f g :
          (a : G ⊗[R] H) → R)
        (x ⊗ₜ[R] y) :
      R)
    ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g)) :
            Dual R (G ⊗[R] H)) :
          (a : G ⊗[R] H) → R)
        (x ⊗ₜ[R] y) :
      R)

Tactic:
simp [map_tmul]

Premises used: TensorProduct.map_tmul
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
G' : Type u_4
H' : Type u_5
inst_7 : AddCommGroup G'
inst_8 : Module R G'
inst_9 : AddCommGroup H'
inst_10 : Module R H'
f : G →ₗ[R] G'
g : H →ₗ[R] H'
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw :
  ∀ (φ : Dual R G),
    Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) φ →
      ∀ (ψ : Dual R H),
        Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) ψ →
          LE.le.{u_1} (α := R) (0 : R)
            ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) (φ ⊗ₜ[R] ψ) : Dual R (G ⊗[R] H)) :
                  (a : G ⊗[R] H) → R)
                w :
              R)
φ : Dual R G'
hφ : Membership.mem (γ := PointedCone R (Dual R G')) (dual (Dual.eval R G') (↑(map f C₁) : Set G')) φ
ψ : Dual R H'
hψ : Membership.mem (γ := PointedCone R (Dual R H')) (dual (Dual.eval R H') (↑(map g C₂) : Set H')) ψ
⊢ Eq (α := G ⊗[R] H →ₗ[R] R)
    ((dualDistrib R G' H' : (a : Dual R G' ⊗[R] Dual R H') → Dual R (G' ⊗[R] H')) (φ ⊗ₜ[R] ψ) ∘ₗ TensorProduct.map f g)
    ((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g)))

Tactic:
have h_eq : ((dualDistrib R G' H') (φ ⊗ₜ[R] ψ)).comp (TensorProduct.map f g) =
      ((dualDistrib R G H) ((φ.comp f) ⊗ₜ[R] (ψ.comp g))) :=
    TensorProduct.ext' fun x y ↦ by simp [map_tmul]
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
G' : Type u_4
H' : Type u_5
inst_7 : AddCommGroup G'
inst_8 : Module R G'
inst_9 : AddCommGroup H'
inst_10 : Module R H'
f : G →ₗ[R] G'
g : H →ₗ[R] H'
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw :
  ∀ (φ : Dual R G),
    Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) φ →
      ∀ (ψ : Dual R H),
        Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) ψ →
          LE.le.{u_1} (α := R) (0 : R)
            ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) (φ ⊗ₜ[R] ψ) : Dual R (G ⊗[R] H)) :
                  (a : G ⊗[R] H) → R)
                w :
              R)
φ : Dual R G'
hφ : Membership.mem (γ := PointedCone R (Dual R G')) (dual (Dual.eval R G') (↑(map f C₁) : Set G')) φ
ψ : Dual R H'
hψ : Membership.mem (γ := PointedCone R (Dual R H')) (dual (Dual.eval R H') (↑(map g C₂) : Set H')) ψ
h_eq :
  Eq (α := G ⊗[R] H →ₗ[R] R)
    ((dualDistrib R G' H' : (a : Dual R G' ⊗[R] Dual R H') → Dual R (G' ⊗[R] H')) (φ ⊗ₜ[R] ψ) ∘ₗ TensorProduct.map f g)
    ((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g)))
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g)) :
            Dual R (G ⊗[R] H)) :
          (a : G ⊗[R] H) → R)
        w :
      R)

Tactic:
hw (φ.comp f) (fun x hx ↦ hφ ⟨x, hx, rfl⟩) (ψ.comp g) (fun y hy ↦ hψ ⟨y, hy, rfl⟩)

Premises used: LinearMap.comp, And.intro, Exists.intro, rfl
-- Module: Mathlib.Geometry.Convex.Cone.TensorProduct
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
G : Type u_2
inst_3 : AddCommGroup G
inst_4 : Module R G
H : Type u_3
inst_5 : AddCommGroup H
inst_6 : Module R H
G' : Type u_4
H' : Type u_5
inst_7 : AddCommGroup G'
inst_8 : Module R G'
inst_9 : AddCommGroup H'
inst_10 : Module R H'
f : G →ₗ[R] G'
g : H →ₗ[R] H'
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw :
  ∀ (φ : Dual R G),
    Membership.mem (γ := PointedCone R (Dual R G)) (dual (Dual.eval R G) (↑C₁ : Set G)) φ →
      ∀ (ψ : Dual R H),
        Membership.mem (γ := PointedCone R (Dual R H)) (dual (Dual.eval R H) (↑C₂ : Set H)) ψ →
          LE.le.{u_1} (α := R) (0 : R)
            ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) (φ ⊗ₜ[R] ψ) : Dual R (G ⊗[R] H)) :
                  (a : G ⊗[R] H) → R)
                w :
              R)
φ : Dual R G'
hφ : Membership.mem (γ := PointedCone R (Dual R G')) (dual (Dual.eval R G') (↑(map f C₁) : Set G')) φ
ψ : Dual R H'
hψ : Membership.mem (γ := PointedCone R (Dual R H')) (dual (Dual.eval R H') (↑(map g C₂) : Set H')) ψ
h_eq :
  Eq (α := G ⊗[R] H →ₗ[R] R)
    ((dualDistrib R G' H' : (a : Dual R G' ⊗[R] Dual R H') → Dual R (G' ⊗[R] H')) (φ ⊗ₜ[R] ψ) ∘ₗ TensorProduct.map f g)
    ((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g)))
⊢ Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R G' H' : (a : Dual R G' ⊗[R] Dual R H') → Dual R (G' ⊗[R] H')) (φ ⊗ₜ[R] ψ) : Dual R (G' ⊗[R] H')) :
          (a : G' ⊗[R] H') → R)
        (((↑{ c : R // 0 ≤ c } :
                  {S : Type u_1} →
                    {M : Type (max u_3 u_2)} →
                      {M₂ : Type (max u_5 u_4)} →
                        [inst_11 : Semiring { c : R // 0 ≤ c }] →
                          [inst_12 : Semiring S] →
                            [inst_13 : AddCommMonoid M] →
                              [inst_14 : AddCommMonoid M₂] →
                                [inst_15 : Module { c : R // 0 ≤ c } M] →
                                  [inst_16 : Module { c : R // 0 ≤ c } M₂] →
                                    [inst_17 : Module S M] →
                                      [inst_18 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ { c : R // 0 ≤ c } S] →
                                          (fₗ : M →ₗ[S] M₂) → M →ₗ[{ c : R // 0 ≤ c }] M₂)
                (TensorProduct.map f g) :
              (a : G ⊗[R] H) → G' ⊗[R] H')
            w :
          G' ⊗[R] H') :
      R)
    ((((dualDistrib R G H : (a : Dual R G ⊗[R] Dual R H) → Dual R (G ⊗[R] H)) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g)) :
            Dual R (G ⊗[R] H)) :
          (a : G ⊗[R] H) → R)
        w :
      R)

Tactic:
exact DFunLike.congr_fun h_eq w

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
x : P
simp :
  (Finset.affineCombination R (Finsupp.support.{u_3, u_1} (M := R) (Finsupp.single x 1)) id : (a : P → R) → P)
      (⇑(Finsupp.single x 1) : (a : P) → R) =
    x
⊢ convexCombination.{u_1, u_2, u_3} (R := R) (StdSimplex.single x) = x

Tactic:
simp only [convexCombination, StdSimplex.single]

Premises used: Convexity.StdSimplex.single, AddTorsor.convexCombination
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
x : P
rw : (Finset.affineCombination R {x} id : (a : P → R) → P) (⇑(Finsupp.single x 1) : (a : P) → R) = x
⊢ (Finset.affineCombination R (Finsupp.support.{u_3, u_1} (M := R) (Finsupp.single x 1)) id : (a : P → R) → P)
      (⇑(Finsupp.single x 1) : (a : P) → R) =
    x

Tactic:
rw [Finsupp.support_single _ one_ne_zero]

Premises used: Finsupp.support_single, one_ne_zero
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
x : P
⊢ (Finset.affineCombination R {x} id : (a : P → R) → P) (⇑(Finsupp.single x 1) : (a : P) → R) = x

Tactic:
({x} : Finset P).affineCombination_of_eq_one_of_eq_zero _ _
    (Finset.mem_singleton_self x) Finsupp.single_eq_same fun j _ hne => Finsupp.single_eq_of_ne hne

Premises used: Finset.mem_singleton_self, Finsupp.single_eq_same, Finsupp.single_eq_of_ne, Finset.affineCombination_of_eq_one_of_eq_zero, Singleton.singleton
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
x : P
⊢ (Finset.affineCombination R {x} id : (a : P → R) → P) (⇑(Finsupp.single x 1) : (a : P) → R) = x

Tactic:
exact ({x} : Finset P).affineCombination_of_eq_one_of_eq_zero _ _
    (Finset.mem_singleton_self x) Finsupp.single_eq_same fun j _ hne => Finsupp.single_eq_of_ne hne

Premises used: Finset.mem_singleton_self, Finsupp.single_eq_same, Finsupp.single_eq_of_ne, Finset.affineCombination_of_eq_one_of_eq_zero, Singleton.singleton
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
⊢ Nonempty P

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
obtain : ∀ (b : P), convexCombination (StdSimplex.map convexCombination f) = convexCombination f.join
⊢ convexCombination (StdSimplex.map convexCombination f) = convexCombination f.join

Tactic:
obtain ⟨b⟩ : Nonempty P := inferInstance

Premises used: Nonempty
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
⊢ (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id : (a : P → R) → P)
      (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
          (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
        V)
      b

Tactic:
have hL := Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
    (f.map convexCombination).weights.support (f.map convexCombination).weights id
    (f.map convexCombination).total b
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id : (a : P → R) → P)
      (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
          (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
        V)
      b
⊢ (Finset.affineCombination R f.join.weights.support id : (a : P → R) → P) (⇑f.join.weights : (a : P) → R) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((f.join.weights.support.weightedVSubOfPoint id b : (a : P → R) → V) (⇑f.join.weights : (a : P) → R) : V) b

Tactic:
have hR := Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
    f.join.weights.support f.join.weights id f.join.total b
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id : (a : P → R) → P)
      (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
          (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
        V)
      b
hR :
  (Finset.affineCombination R f.join.weights.support id : (a : P → R) → P) (⇑f.join.weights : (a : P) → R) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((f.join.weights.support.weightedVSubOfPoint id b : (a : P → R) → V) (⇑f.join.weights : (a : P) → R) : V) b
simp :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
          (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
        V)
      b =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((f.join.weights.support.weightedVSubOfPoint id b : (a : P → R) → V) (⇑f.join.weights : (a : P) → R) : V) b
⊢ convexCombination (StdSimplex.map convexCombination f) = convexCombination f.join

Tactic:
simp only [convexCombination, hL, hR]

Premises used: AddTorsor.convexCombination
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id : (a : P → R) → P)
      (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
          (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
        V)
      b
hR :
  (Finset.affineCombination R f.join.weights.support id : (a : P → R) → P) (⇑f.join.weights : (a : P) → R) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((f.join.weights.support.weightedVSubOfPoint id b : (a : P → R) → V) (⇑f.join.weights : (a : P) → R) : V) b
e_a :
  Eq.{u_2 + 1} (α := V)
    (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
        (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
      V)
    ((f.join.weights.support.weightedVSubOfPoint id b : (a : P → R) → V) (⇑f.join.weights : (a : P) → R) : V)
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
          (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
        V)
      b =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((f.join.weights.support.weightedVSubOfPoint id b : (a : P → R) → V) (⇑f.join.weights : (a : P) → R) : V) b

Tactic:
congr 1
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id : (a : P → R) → P)
      (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
          (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
        V)
      b
hR :
  (Finset.affineCombination R f.join.weights.support id : (a : P → R) → P) (⇑f.join.weights : (a : P) → R) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((f.join.weights.support.weightedVSubOfPoint id b : (a : P → R) → V) (⇑f.join.weights : (a : P) → R) : V) b
e_a :
  Eq.{u_2 + 1} (α := V)
    (∑ x ∈ (Finsupp.mapDomain convexCombination f.weights).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Finsupp.mapDomain convexCombination f.weights : (a : P) → R) x : R)
        (x -ᵥ b))
    (∑ x ∈ Finsupp.support.{u_3, u_1} (M := R) (f.weights.sum fun (d : StdSimplex R P) (r : R) ↦ r • d.weights),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((f.weights.sum fun (d : StdSimplex R P) (r : R) ↦ r • d.weights : (a : P) → R) x : R) (x -ᵥ b))
⊢ Eq.{u_2 + 1} (α := V)
    (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
        (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
      V)
    ((f.join.weights.support.weightedVSubOfPoint id b : (a : P → R) → V) (⇑f.join.weights : (a : P) → R) : V)

Tactic:
simp only [Finset.weightedVSubOfPoint_apply, StdSimplex.map, StdSimplex.join, id]

Premises used: Finset.weightedVSubOfPoint_apply, id, Convexity.StdSimplex.map, Convexity.StdSimplex.join