awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : NoZeroDivisors k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h_1 : Nontrivial k
w : (↑Set.univ : Type) → Fin 3 → k :=
  fun (i : (↑Set.univ : Type)) ↦
    Finset.affineCombinationLineMapWeights ((↑i : Fin 3) + 1) ((↑i : Fin 3) + 2) (r (↑i : Fin 3))
hw : ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1
w' : Fin (HAdd.hAdd (α := ℕ) 2 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ j : Fin (2 + 1), w' j) 1
h :
  ∀ (i : (↑Set.univ : Type)),
    ∃ (r : k),
      ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
        r * Set.indicator {(↑i : Fin (2 + 1))}ᶜ (w i) j = Set.indicator {(↑i : Fin (2 + 1))}ᶜ w' j
hp' :
  ∀ (i : Fin 3),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
hp'w :
  ∀ (i : (↑Set.univ : Type)),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points (↑i : Fin 3))
          (singleton (α := P)
            ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) (w i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
h' :
  ∀ (i : Fin 3),
    ∃ (c : k), ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k :=
  fun (i : Fin 3) ↦
    ⋯.choose (p := fun (c : k) ↦
      ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j)
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
i : Fin 3
⊢ i + 2 ≠ i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : NoZeroDivisors k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h_1 : Nontrivial k
w : (↑Set.univ : Type) → Fin 3 → k :=
  fun (i : (↑Set.univ : Type)) ↦
    Finset.affineCombinationLineMapWeights ((↑i : Fin 3) + 1) ((↑i : Fin 3) + 2) (r (↑i : Fin 3))
hw : ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1
w' : Fin (HAdd.hAdd (α := ℕ) 2 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ j : Fin (2 + 1), w' j) 1
h :
  ∀ (i : (↑Set.univ : Type)),
    ∃ (r : k),
      ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
        r * Set.indicator {(↑i : Fin (2 + 1))}ᶜ (w i) j = Set.indicator {(↑i : Fin (2 + 1))}ᶜ w' j
hp' :
  ∀ (i : Fin 3),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
hp'w :
  ∀ (i : (↑Set.univ : Type)),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points (↑i : Fin 3))
          (singleton (α := P)
            ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) (w i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
h' :
  ∀ (i : Fin 3),
    ∃ (c : k), ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k :=
  fun (i : Fin 3) ↦
    ⋯.choose (p := fun (c : k) ↦
      ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j)
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
i : Fin 3
rw : c i * r i = c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) (i + 2)
⊢ c i * r i = w' (i + 2)

Tactic:
rw [← hc i (i + 2) (by simp)]

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : NoZeroDivisors k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h_1 : Nontrivial k
w : (↑Set.univ : Type) → Fin 3 → k :=
  fun (i : (↑Set.univ : Type)) ↦
    Finset.affineCombinationLineMapWeights ((↑i : Fin 3) + 1) ((↑i : Fin 3) + 2) (r (↑i : Fin 3))
hw : ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1
w' : Fin (HAdd.hAdd (α := ℕ) 2 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ j : Fin (2 + 1), w' j) 1
h :
  ∀ (i : (↑Set.univ : Type)),
    ∃ (r : k),
      ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
        r * Set.indicator {(↑i : Fin (2 + 1))}ᶜ (w i) j = Set.indicator {(↑i : Fin (2 + 1))}ᶜ w' j
hp' :
  ∀ (i : Fin 3),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
hp'w :
  ∀ (i : (↑Set.univ : Type)),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points (↑i : Fin 3))
          (singleton (α := P)
            ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) (w i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
h' :
  ∀ (i : Fin 3),
    ∃ (c : k), ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k :=
  fun (i : Fin 3) ↦
    ⋯.choose (p := fun (c : k) ↦
      ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j)
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
i : Fin 3
⊢ c i * r i = c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) (i + 2)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : NoZeroDivisors k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h_1 : Nontrivial k
w : (↑Set.univ : Type) → Fin 3 → k :=
  fun (i : (↑Set.univ : Type)) ↦
    Finset.affineCombinationLineMapWeights ((↑i : Fin 3) + 1) ((↑i : Fin 3) + 2) (r (↑i : Fin 3))
hw : ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1
w' : Fin (HAdd.hAdd (α := ℕ) 2 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ j : Fin (2 + 1), w' j) 1
h :
  ∀ (i : (↑Set.univ : Type)),
    ∃ (r : k),
      ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
        r * Set.indicator {(↑i : Fin (2 + 1))}ᶜ (w i) j = Set.indicator {(↑i : Fin (2 + 1))}ᶜ w' j
hp' :
  ∀ (i : Fin 3),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
hp'w :
  ∀ (i : (↑Set.univ : Type)),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points (↑i : Fin 3))
          (singleton (α := P)
            ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) (w i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
h' :
  ∀ (i : Fin 3),
    ∃ (c : k), ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k :=
  fun (i : Fin 3) ↦
    ⋯.choose (p := fun (c : k) ↦
      ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j)
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
⊢ ∀ (i : Fin 3), c i * r i = w' (i + 2)

Tactic:
have hc2 (i : Fin 3) : c i * r i = w' (i + 2) := by
    rw [← hc i (i + 2) (by simp)]
    simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : NoZeroDivisors k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h_1 : Nontrivial k
w : (↑Set.univ : Type) → Fin 3 → k :=
  fun (i : (↑Set.univ : Type)) ↦
    Finset.affineCombinationLineMapWeights ((↑i : Fin 3) + 1) ((↑i : Fin 3) + 2) (r (↑i : Fin 3))
hw : ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1
w' : Fin (HAdd.hAdd (α := ℕ) 2 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ j : Fin (2 + 1), w' j) 1
h :
  ∀ (i : (↑Set.univ : Type)),
    ∃ (r : k),
      ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
        r * Set.indicator {(↑i : Fin (2 + 1))}ᶜ (w i) j = Set.indicator {(↑i : Fin (2 + 1))}ᶜ w' j
hp' :
  ∀ (i : Fin 3),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
hp'w :
  ∀ (i : (↑Set.univ : Type)),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points (↑i : Fin 3))
          (singleton (α := P)
            ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) (w i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
h' :
  ∀ (i : Fin 3),
    ∃ (c : k), ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k :=
  fun (i : Fin 3) ↦
    ⋯.choose (p := fun (c : k) ↦
      ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j)
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
simp_rw : Eq.{u_1 + 1} (α := k) (∏ x : Fin 3, w' (x + 2)) (∏ x : Fin 3, w' (x + 1))
⊢ HMul.hMul (α := k) (∏ i : Fin 3, c i) (∏ i : Fin 3, r i) =
    HMul.hMul (α := k) (∏ i : Fin 3, c i) (∏ i : Fin 3, (1 - r i))

Tactic:
simp_rw [← Finset.prod_mul_distrib, Finset.prod_congr rfl (fun _ _ ↦ hc1 _),
      Finset.prod_congr rfl (fun _ _ ↦ hc2 _)]

Premises used: Finset.prod_mul_distrib, Finset.prod_congr, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : NoZeroDivisors k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h_1 : Nontrivial k
w : (↑Set.univ : Type) → Fin 3 → k :=
  fun (i : (↑Set.univ : Type)) ↦
    Finset.affineCombinationLineMapWeights ((↑i : Fin 3) + 1) ((↑i : Fin 3) + 2) (r (↑i : Fin 3))
hw : ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1
w' : Fin (HAdd.hAdd (α := ℕ) 2 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ j : Fin (2 + 1), w' j) 1
h :
  ∀ (i : (↑Set.univ : Type)),
    ∃ (r : k),
      ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
        r * Set.indicator {(↑i : Fin (2 + 1))}ᶜ (w i) j = Set.indicator {(↑i : Fin (2 + 1))}ᶜ w' j
hp' :
  ∀ (i : Fin 3),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
hp'w :
  ∀ (i : (↑Set.univ : Type)),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points (↑i : Fin 3))
          (singleton (α := P)
            ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) (w i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
h' :
  ∀ (i : Fin 3),
    ∃ (c : k), ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k :=
  fun (i : Fin 3) ↦
    ⋯.choose (p := fun (c : k) ↦
      ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j)
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
this :
  Eq.{u_1 + 1} (α := k) (∏ i : Fin (2 + 1), (w' ∘ (⇑(Equiv.addRight 2) : (a : Fin (2 + 1)) → Fin (2 + 1))) i)
    (∏ i : Fin (2 + 1), (w' ∘ (⇑(Equiv.addRight 1) : (a : Fin (2 + 1)) → Fin (2 + 1))) i)
⊢ Eq.{u_1 + 1} (α := k) (∏ x : Fin 3, w' (x + 2)) (∏ x : Fin 3, w' (x + 1))

Tactic:
simpa using this
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : NoZeroDivisors k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h_1 : Nontrivial k
w : (↑Set.univ : Type) → Fin 3 → k :=
  fun (i : (↑Set.univ : Type)) ↦
    Finset.affineCombinationLineMapWeights ((↑i : Fin 3) + 1) ((↑i : Fin 3) + 2) (r (↑i : Fin 3))
hw : ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1
w' : Fin (HAdd.hAdd (α := ℕ) 2 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ j : Fin (2 + 1), w' j) 1
h :
  ∀ (i : (↑Set.univ : Type)),
    ∃ (r : k),
      ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
        r * Set.indicator {(↑i : Fin (2 + 1))}ᶜ (w i) j = Set.indicator {(↑i : Fin (2 + 1))}ᶜ w' j
hp' :
  ∀ (i : Fin 3),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
hp'w :
  ∀ (i : (↑Set.univ : Type)),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points (↑i : Fin 3))
          (singleton (α := P)
            ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) (w i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
h' :
  ∀ (i : Fin 3),
    ∃ (c : k), ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k :=
  fun (i : Fin 3) ↦
    ⋯.choose (p := fun (c : k) ↦
      ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j)
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
suffices :
  Eq.{u_1 + 1} (α := k) (∏ i : Fin (2 + 1), (w' ∘ (⇑(Equiv.addRight 2) : (a : Fin (2 + 1)) → Fin (2 + 1))) i)
    (∏ i : Fin (2 + 1), (w' ∘ (⇑(Equiv.addRight 1) : (a : Fin (2 + 1)) → Fin (2 + 1))) i)
⊢ Eq.{u_1 + 1} (α := k) (∏ x : Fin 3, w' (x + 2)) (∏ x : Fin 3, w' (x + 1))

Tactic:
suffices ∏ i, (w' ∘ Equiv.addRight 2) i = ∏ i, (w' ∘ Equiv.addRight 1) i by
      simpa using this
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : NoZeroDivisors k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h_1 : Nontrivial k
w : (↑Set.univ : Type) → Fin 3 → k :=
  fun (i : (↑Set.univ : Type)) ↦
    Finset.affineCombinationLineMapWeights ((↑i : Fin 3) + 1) ((↑i : Fin 3) + 2) (r (↑i : Fin 3))
hw : ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1
w' : Fin (HAdd.hAdd (α := ℕ) 2 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ j : Fin (2 + 1), w' j) 1
h :
  ∀ (i : (↑Set.univ : Type)),
    ∃ (r : k),
      ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
        r * Set.indicator {(↑i : Fin (2 + 1))}ᶜ (w i) j = Set.indicator {(↑i : Fin (2 + 1))}ᶜ w' j
hp' :
  ∀ (i : Fin 3),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
hp'w :
  ∀ (i : (↑Set.univ : Type)),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points (↑i : Fin 3))
          (singleton (α := P)
            ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) (w i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
h' :
  ∀ (i : Fin 3),
    ∃ (c : k), ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k :=
  fun (i : Fin 3) ↦
    ⋯.choose (p := fun (c : k) ↦
      ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j)
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
simp_rw :
  Finset.prod (Finset.map (Equiv.toEmbedding (Equiv.addRight 2)) Finset.univ) w' =
    Finset.prod (Finset.map (Equiv.toEmbedding (Equiv.addRight 1)) Finset.univ) w'
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin (2 + 1), (w' ∘ (⇑(Equiv.addRight 2) : (a : Fin (2 + 1)) → Fin (2 + 1))) i)
    (∏ i : Fin (2 + 1), (w' ∘ (⇑(Equiv.addRight 1) : (a : Fin (2 + 1)) → Fin (2 + 1))) i)

Tactic:
simp_rw [Finset.prod_comp_equiv]

Premises used: Finset.prod_comp_equiv
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : NoZeroDivisors k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h_1 : Nontrivial k
w : (↑Set.univ : Type) → Fin 3 → k :=
  fun (i : (↑Set.univ : Type)) ↦
    Finset.affineCombinationLineMapWeights ((↑i : Fin 3) + 1) ((↑i : Fin 3) + 2) (r (↑i : Fin 3))
hw : ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1
w' : Fin (HAdd.hAdd (α := ℕ) 2 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ j : Fin (2 + 1), w' j) 1
h :
  ∀ (i : (↑Set.univ : Type)),
    ∃ (r : k),
      ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
        r * Set.indicator {(↑i : Fin (2 + 1))}ᶜ (w i) j = Set.indicator {(↑i : Fin (2 + 1))}ᶜ w' j
hp' :
  ∀ (i : Fin 3),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
hp'w :
  ∀ (i : (↑Set.univ : Type)),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points (↑i : Fin 3))
          (singleton (α := P)
            ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) (w i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
h' :
  ∀ (i : Fin 3),
    ∃ (c : k), ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k :=
  fun (i : Fin 3) ↦
    ⋯.choose (p := fun (c : k) ↦
      ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j)
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
⊢ Finset.prod (Finset.map (Equiv.toEmbedding (Equiv.addRight 2)) Finset.univ) w' =
    Finset.prod (Finset.map (Equiv.toEmbedding (Equiv.addRight 1)) Finset.univ) w'

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : NoZeroDivisors k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h_1 : Nontrivial k
w : (↑Set.univ : Type) → Fin 3 → k :=
  fun (i : (↑Set.univ : Type)) ↦
    Finset.affineCombinationLineMapWeights ((↑i : Fin 3) + 1) ((↑i : Fin 3) + 2) (r (↑i : Fin 3))
hw : ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1
w' : Fin (HAdd.hAdd (α := ℕ) 2 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ j : Fin (2 + 1), w' j) 1
h :
  ∀ (i : (↑Set.univ : Type)),
    ∃ (r : k),
      ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
        r * Set.indicator {(↑i : Fin (2 + 1))}ᶜ (w i) j = Set.indicator {(↑i : Fin (2 + 1))}ᶜ w' j
hp' :
  ∀ (i : Fin 3),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
hp'w :
  ∀ (i : (↑Set.univ : Type)),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points (↑i : Fin 3))
          (singleton (α := P)
            ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) (w i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
h' :
  ∀ (i : Fin 3),
    ∃ (c : k), ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k :=
  fun (i : Fin 3) ↦
    ⋯.choose (p := fun (c : k) ↦
      ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j)
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
⊢ HMul.hMul (α := k) (∏ i : Fin 3, c i) (∏ i : Fin 3, r i) =
    HMul.hMul (α := k) (∏ i : Fin 3, c i) (∏ i : Fin 3, (1 - r i))

Tactic:
have hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i) := by
    simp_rw [← Finset.prod_mul_distrib, Finset.prod_congr rfl (fun _ _ ↦ hc1 _),
      Finset.prod_congr rfl (fun _ _ ↦ hc2 _)]
    suffices ∏ i, (w' ∘ Equiv.addRight 2) i = ∏ i, (w' ∘ Equiv.addRight 1) i by
      simpa using this
    simp_rw [Finset.prod_comp_equiv]
    simp