awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : P → R → V := fun (x : P) (w : R) ↦ w • (x -ᵥ b)
h_rhs :
  Eq.{u_2 + 1} (α := V)
    (∑
      a ∈
        Finsupp.support.{u_3, u_1} (M := R)
          (∑ d ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights),
      h a
        ((∑ d ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights :
            (a : P) → R)
          a))
    (∑ x ∈ f.weights.support,
      ∑ a ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights).support,
        h a ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights : (a : P) → R) a))
d : StdSimplex R P
hd : ¬Eq.{u_1 + 1} (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) (0 : R)
p : P
neg :
  ¬Eq.{u_1 + 1} (α := R) ((d.weights : (a : P) → R) p : R) (0 : R) →
    ¬Eq.{u_1 + 1} (α := R)
        ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights : (a : P) → R) p : R) (0 : R)
neg₁ :
  ¬Eq.{u_1 + 1} (α := R)
        ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights : (a : P) → R) p : R) (0 : R) →
    ¬Eq.{u_1 + 1} (α := R) ((d.weights : (a : P) → R) p : R) (0 : R)
⊢ ¬Eq.{u_1 + 1} (α := R) ((d.weights : (a : P) → R) p : R) (0 : R) ↔
    ¬Eq.{u_1 + 1} (α := R)
        ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights : (a : P) → R) p : R) (0 : R)

Tactic:
constructor
-- 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
h : P → R → V := fun (x : P) (w : R) ↦ w • (x -ᵥ b)
h_rhs :
  Eq.{u_2 + 1} (α := V)
    (∑
      a ∈
        Finsupp.support.{u_3, u_1} (M := R)
          (∑ d ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights),
      h a
        ((∑ d ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights :
            (a : P) → R)
          a))
    (∑ x ∈ f.weights.support,
      ∑ a ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights).support,
        h a ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights : (a : P) → R) a))
d : StdSimplex R P
hd : ¬Eq.{u_1 + 1} (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) (0 : R)
p : P
hp : ¬Eq.{u_1 + 1} (α := R) ((d.weights : (a : P) → R) p : R) (0 : R)
⊢ ¬Eq.{u_1 + 1} (α := R)
      ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights : (a : P) → R) p : R) (0 : R)

Tactic:
(mul_pos ((f.nonneg d).lt_of_ne' hd) ((d.nonneg p).lt_of_ne' hp)).ne'

Premises used: Convexity.StdSimplex.nonneg, LT.lt.ne', mul_pos, LE.le.lt_of_ne'
-- 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
h : P → R → V := fun (x : P) (w : R) ↦ w • (x -ᵥ b)
h_rhs :
  Eq.{u_2 + 1} (α := V)
    (∑
      a ∈
        Finsupp.support.{u_3, u_1} (M := R)
          (∑ d ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights),
      h a
        ((∑ d ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights :
            (a : P) → R)
          a))
    (∑ x ∈ f.weights.support,
      ∑ a ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights).support,
        h a ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights : (a : P) → R) a))
d : StdSimplex R P
hd : ¬Eq.{u_1 + 1} (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) (0 : R)
p : P
hp : ¬Eq.{u_1 + 1} (α := R) ((d.weights : (a : P) → R) p : R) (0 : R)
⊢ ¬Eq.{u_1 + 1} (α := R)
      ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights : (a : P) → R) p : R) (0 : R)

Tactic:
exact (mul_pos ((f.nonneg d).lt_of_ne' hd) ((d.nonneg p).lt_of_ne' hp)).ne'

Premises used: Convexity.StdSimplex.nonneg, LT.lt.ne', mul_pos, LE.le.lt_of_ne'
-- 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
h : P → R → V := fun (x : P) (w : R) ↦ w • (x -ᵥ b)
h_rhs :
  Eq.{u_2 + 1} (α := V)
    (∑
      a ∈
        Finsupp.support.{u_3, u_1} (M := R)
          (∑ d ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights),
      h a
        ((∑ d ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights :
            (a : P) → R)
          a))
    (∑ x ∈ f.weights.support,
      ∑ a ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights).support,
        h a ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights : (a : P) → R) a))
d : StdSimplex R P
hd : ¬Eq.{u_1 + 1} (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) (0 : R)
p : P
hp :
  ¬Eq.{u_1 + 1} (α := R)
      ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights : (a : P) → R) p : R) (0 : R)
hp' : Eq.{u_1 + 1} (α := R) ((d.weights : (a : P) → R) p : R) (0 : R)
⊢ False

Tactic:
simp only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, hp', mul_zero,
        not_true_eq_false] at hp

Premises used: not_true_eq_false, MulZeroClass.mul_zero, Finsupp.coe_smul, smul_eq_mul, Pi.smul_apply
-- 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
s : StdSimplex R P
⊢ sConvexComb s = (Finset.affineCombination R s.weights.support id : (a : P → R) → P) (⇑s.weights : (a : P) → R)

Tactic:
rfl
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
I : Type u_4
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
s : StdSimplex R I
f : I → P
p : P := Nonempty.some ⋯
simp :
  Eq.{u_3 + 1} (α := P)
    ((Finset.affineCombination R (StdSimplex.map f s).weights.support id : (a : P → R) → P)
        (⇑(StdSimplex.map f s).weights : (a : P) → R) :
      P)
    ((Finset.affineCombination R s.weights.support f : (a : I → R) → P) (⇑s.weights : (a : I) → R) : P)
⊢ iConvexComb s f = (Finset.affineCombination R s.weights.support f : (a : I → R) → P) (⇑s.weights : (a : I) → R)

Tactic:
simp only [iConvexComb, sConvexComb_eq_affineCombination]

Premises used: Convexity.iConvexComb, AddTorsor.sConvexComb_eq_affineCombination
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
I : Type u_4
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
s : StdSimplex R I
f : I → P
p : P := Nonempty.some ⋯
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((StdSimplex.map f s).weights.support.weightedVSubOfPoint id p : (a : P → R) → V) fun (i : P) ↦
          (fun (x : P) (r : R) ↦ r) i (((StdSimplex.map f s).weights : (a : P) → R) i) :
        V)
      p =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((s.weights.support.weightedVSubOfPoint f p : (a : I → R) → V) fun (i : I) ↦
          (fun (x : I) (r : R) ↦ r) i ((s.weights : (a : I) → R) i) :
        V)
      p
⊢ Eq.{u_3 + 1} (α := P)
    ((Finset.affineCombination R (StdSimplex.map f s).weights.support id : (a : P → R) → P)
        (⇑(StdSimplex.map f s).weights : (a : P) → R) :
      P)
    ((Finset.affineCombination R s.weights.support f : (a : I → R) → P) (⇑s.weights : (a : I) → R) : P)

Tactic:
rw [Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
    (b := p) (h := (s.map f).total),
    Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
    (b := p) (h := s.total)]

Premises used: Finsupp.support, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, Convexity.StdSimplex.weights, Convexity.StdSimplex.total, Convexity.StdSimplex.map, DFunLike.coe
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
I : Type u_4
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
s : StdSimplex R I
f : I → P
p : P := Nonempty.some ⋯
this :
  Eq.{u_2 + 1} (α := V) ((Finsupp.mapDomain f s.weights).sum fun (x : P) (r : R) ↦ r • (x -ᵥ p))
    (s.weights.sum fun (x : I) (r : R) ↦ r • (f x -ᵥ p))
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((StdSimplex.map f s).weights.support.weightedVSubOfPoint id p : (a : P → R) → V) fun (i : P) ↦
          (fun (x : P) (r : R) ↦ r) i (((StdSimplex.map f s).weights : (a : P) → R) i) :
        V)
      p =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((s.weights.support.weightedVSubOfPoint f p : (a : I → R) → V) fun (i : I) ↦
          (fun (x : I) (r : R) ↦ r) i ((s.weights : (a : I) → R) i) :
        V)
      p

Tactic:
simpa
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
I : Type u_4
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
s : StdSimplex R I
f : I → P
p : P := Nonempty.some ⋯
suffices :
  Eq.{u_2 + 1} (α := V) ((Finsupp.mapDomain f s.weights).sum fun (x : P) (r : R) ↦ r • (x -ᵥ p))
    (s.weights.sum fun (x : I) (r : R) ↦ r • (f x -ᵥ p))
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((StdSimplex.map f s).weights.support.weightedVSubOfPoint id p : (a : P → R) → V) fun (i : P) ↦
          (fun (x : P) (r : R) ↦ r) i (((StdSimplex.map f s).weights : (a : P) → R) i) :
        V)
      p =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((s.weights.support.weightedVSubOfPoint f p : (a : I → R) → V) fun (i : I) ↦
          (fun (x : I) (r : R) ↦ r) i ((s.weights : (a : I) → R) i) :
        V)
      p

Tactic:
suffices ((s.weights.mapDomain f).sum fun x r ↦ r • (x -ᵥ p)) =
    s.weights.sum fun x r ↦ r • (f x -ᵥ p) by simpa
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
I : Type u_4
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
s : StdSimplex R I
f : I → P
p : P := Nonempty.some ⋯
⊢ Eq.{u_2 + 1} (α := V) ((Finsupp.mapDomain f s.weights).sum fun (x : P) (r : R) ↦ r • (x -ᵥ p))
    (s.weights.sum fun (x : I) (r : R) ↦ r • (f x -ᵥ p))

Tactic:
simp [Finsupp.sum_mapDomain_index, add_smul]

Premises used: Finsupp.sum_mapDomain_index, add_smul
-- 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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
simp :
  (Finset.affineCombination R (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support id :
        (a : P → R) → P)
      (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) =
    s • (x -ᵥ y) +ᵥ y
⊢ convexCombPair s t hs ht h x y = (AffineMap.lineMap y x : (a : R) → P) s

Tactic:
simp only [convexCombPair, AddTorsor.sConvexComb_eq_affineCombination, StdSimplex.duple,
    AffineMap.lineMap_apply]

Premises used: Convexity.StdSimplex.duple, AffineMap.lineMap_apply, Convexity.convexCombPair, AddTorsor.sConvexComb_eq_affineCombination
-- 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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support.weightedVSubOfPoint id y :
            (a : P → R) → V)
          (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) :
        V)
      y =
    s • (x -ᵥ y) +ᵥ y
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i)
    1
⊢ (Finset.affineCombination R (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support id :
        (a : P → R) → P)
      (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) =
    s • (x -ᵥ y) +ᵥ y

Tactic:
rw [Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ id (b := y)]

Premises used: Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, id
-- 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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
trans :
  Eq (α := R)
    (∑ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i)
    ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (x : P) (r : R) ↦ r)
trans₁ : Eq (α := R) ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (x : P) (r : R) ↦ r) 1
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i)
    1

Tactic:
trans (Finsupp.single x s + Finsupp.single y t).sum fun _ r => r

Premises used: Finsupp.sum, HAdd.hAdd, Finsupp.single
-- 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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
apply :
  ∀ x_1 ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
    Eq.{u_1 + 1} (α := R) ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) x_1 : R)
      ((fun (x : P) (r : R) ↦ r) x_1
          ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) x_1) :
        R)
⊢ Eq (α := R)
    (∑ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i)
    ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (x : P) (r : R) ↦ r)

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- 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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y i : P
_ :
  i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support →
    Eq.{u_1 + 1} (α := R) ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i : R)
      ((fun (x : P) (r : R) ↦ r) i
          ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i) :
        R)
⊢ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support →
    Eq.{u_1 + 1} (α := R) ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i : R)
      ((fun (x : P) (r : R) ↦ r) i
          ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i) :
        R)

Tactic:
_
-- 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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y i : P
h_1 : i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support
⊢ Eq.{u_1 + 1} (α := R) ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i : R)
    ((fun (x : P) (r : R) ↦ r) i ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i) :
      R)

Tactic:
simp only [Finsupp.coe_add, Pi.add_apply]

Premises used: Pi.add_apply, Finsupp.coe_add
-- 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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ∀ a ∈ Finsupp.support (Finsupp.single x s) ∪ Finsupp.support (Finsupp.single y t), Eq.{u_1 + 1} (α := R) 0 0

Tactic:
simp
-- 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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ∀ a ∈ Finsupp.support (Finsupp.single x s) ∪ Finsupp.support (Finsupp.single y t), ∀ (b₁ b₂ : R), b₁ + b₂ = b₁ + b₂

Tactic:
simp
-- 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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
simp
-- 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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
rw :
  HAdd.hAdd (α := R) (Finsupp.sum (Finsupp.single x s) fun (x : P) (r : R) ↦ r)
      (Finsupp.sum (Finsupp.single y t) fun (x : P) (r : R) ↦ r) =
    1
rw₁ : (s + Finsupp.sum (Finsupp.single y t) fun (x : P) (r : R) ↦ r) = 1
rw₂ : s + t = 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq (α := R) ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (x : P) (r : R) ↦ r) 1

Tactic:
rw [Finsupp.sum_add_index (by simp) (by simp), Finsupp.sum_single_index (by simp),
        Finsupp.sum_single_index (by simp), h]

Premises used: Finsupp.sum_single_index, Finsupp.sum_add_index
-- 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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
e_a :
  ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support.weightedVSubOfPoint id y :
        (a : P → R) → V)
      (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) =
    s • (x -ᵥ y)
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support.weightedVSubOfPoint id y :
            (a : P → R) → V)
          (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) :
        V)
      y =
    s • (x -ᵥ y) +ᵥ y

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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
e_a :
  ∑ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i : R) (id i -ᵥ y) =
    s • (x -ᵥ y)
⊢ ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support.weightedVSubOfPoint id y :
        (a : P → R) → V)
      (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) =
    s • (x -ᵥ y)

Tactic:
rw [Finset.weightedVSubOfPoint_apply]

Premises used: Finset.weightedVSubOfPoint_apply