awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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)
⊢ Eq.{u_2 + 1} (α := V)
    (∑ x ∈ d.weights.support,
      HMul.hMul (α := R) (β := R) ((f.weights : (a : StdSimplex R P) → R) d : R) ((d.weights : (a : P) → R) x : R) •
        (x -ᵥ b))
    (∑ x ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support,
      h x
        (HMul.hMul (α := R) (β := R) ((f.weights : (a : StdSimplex R P) → R) d : R) ((d.weights : (a : P) → R) x : R)))
have neg : d.weights.support = (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support
Tactic: refine Finset.sum_congr ?_ (fun _ _ => rfl)
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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)
⊢ d.weights.support = (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support
have neg : ∀ (p : P),
  p ∈ d.weights.support ↔ p ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support
Tactic: ext p
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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
⊢ p ∈ d.weights.support ↔ p ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support
have 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)
Tactic: simp only [Finsupp.mem_support_iff, ne_eq]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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
⊢ ¬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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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)
⊢ ¬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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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 ⋯
⊢ iConvexComb s f = (Finset.affineCombination R s.weights.support f : (a : I → R) → P) (⇑s.weights : (a : I) → R)
have 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)
Tactic: simp only [iConvexComb, sConvexComb_eq_affineCombination]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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_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)
have 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
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)]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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 ⋯
⊢ 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
have 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))
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
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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
⊢ convexCombPair s t hs ht h x y = (AffineMap.lineMap y x : (a : R) → P) s
have 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
Tactic: simp only [convexCombPair, AddTorsor.sConvexComb_eq_affineCombination, StdSimplex.duple,
    AffineMap.lineMap_apply]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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
⊢ (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
have 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
Tactic: rw [Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ id (b := y)]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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
⊢ (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
have 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
Tactic: rw [Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ id (b := y)]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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)
    (∑ 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
have 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)
Tactic: trans (Finsupp.single x s + Finsupp.single y t).sum fun _ r => r
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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)
⊢ 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
have trans₁ : Eq (α := R) ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (x : P) (r : R) ↦ r) 1
Tactic: trans (Finsupp.single x s + Finsupp.single y t).sum fun _ r => r
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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 (α := 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)
have 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)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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 (α := R) ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (x : P) (r : R) ↦ r) 1
have 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
Tactic: rw [Finsupp.sum_add_index (by simp) (by simp), Finsupp.sum_single_index (by simp),
        Finsupp.sum_single_index (by simp), h]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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
⊢ Eq (α := R) ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (x : P) (r : R) ↦ r) 1
have rw₁ : (s + Finsupp.sum (Finsupp.single y t) 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]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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
⊢ Eq (α := R) ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (x : P) (r : R) ↦ r) 1
have rw₃ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [Finsupp.sum_add_index (by simp) (by simp), Finsupp.sum_single_index (by simp),
        Finsupp.sum_single_index (by simp), h]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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
⊢ 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
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
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
⊢ ((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)
have 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)
Tactic: rw [Finset.weightedVSubOfPoint_apply]