awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ceva (goal)
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)
hcr :
  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))
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
hw'i2 : w' (i + 2) = 0
hw'i0 : w' i = 1
hi1 : c (i + 1) * r (i + 1) = 1
hi1' : c (i + 1) * (1 - r (i + 1)) = 0
hci1 : c (i + 1) = 1
hri1 : r (i + 1) = 1
hi2 : c (i + 2) * (1 - r (i + 2)) = 1
hi2' : c (i + 2) * r (i + 2) = 0
rw : c (i + 2) * r (i + 2) + c (i + 2) * (1 - r (i + 2)) = HAdd.hAdd (α := k) 0 1
⊢ c (i + 2) * (r (i + 2) + (1 - r (i + 2))) = HAdd.hAdd (α := k) 0 1
have rw₁ : c (i + 2) * r (i + 2) + 1 = HAdd.hAdd (α := k) 0 1
Tactic: rw [mul_add, hi2, hi2']
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ceva (goal)
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)
hcr :
  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))
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
hw'i2 : w' (i + 2) = 0
hw'i0 : w' i = 1
hi1 : c (i + 1) * r (i + 1) = 1
hi1' : c (i + 1) * (1 - r (i + 1)) = 0
hci1 : c (i + 1) = 1
hri1 : r (i + 1) = 1
hi2 : c (i + 2) * (1 - r (i + 2)) = 1
hi2' : c (i + 2) * r (i + 2) = 0
rw : c (i + 2) * r (i + 2) + c (i + 2) * (1 - r (i + 2)) = HAdd.hAdd (α := k) 0 1
rw₁ : c (i + 2) * r (i + 2) + 1 = HAdd.hAdd (α := k) 0 1
⊢ c (i + 2) * (r (i + 2) + (1 - r (i + 2))) = HAdd.hAdd (α := k) 0 1
have rw₂ : HAdd.hAdd (α := k) 0 1 = HAdd.hAdd (α := k) 0 1
Tactic: rw [mul_add, hi2, hi2']
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ceva (hypothesis)
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)
hcr :
  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))
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
hw'i2 : w' (i + 2) = 0
hw'i0 : w' i = 1
hi1 : c (i + 1) * r (i + 1) = 1
hi1' : c (i + 1) * (1 - r (i + 1)) = 0
hci1 : c (i + 1) = 1
hri1 : r (i + 1) = 1
hi2 : c (i + 2) * (1 - r (i + 2)) = 1
hi2' : c (i + 2) * r (i + 2) = 0
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
have hci2 : c (i + 2) = 1
Tactic: have hci2 : c (i + 2) = 1 := by
      suffices c (i + 2) * (r (i + 2) + (1 - r (i + 2))) = 0 + 1 by simpa using this
      rw [mul_add, hi2, hi2']
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ceva (hypothesis)
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)
hcr :
  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))
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
hw'i2 : w' (i + 2) = 0
hw'i0 : w' i = 1
hi1 : c (i + 1) * r (i + 1) = 1
hi1' : c (i + 1) * (1 - r (i + 1)) = 0
hci1 : c (i + 1) = 1
hri1 : r (i + 1) = 1
hi2 : c (i + 2) * (1 - r (i + 2)) = 1
hi2' : c (i + 2) * r (i + 2) = 0
hci2 : c (i + 2) = 1
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
have hri2 : r (i + 2) = 0
Tactic: have hri2 : r (i + 2) = 0 := by simpa [hci2] using hi2'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ceva (goal)
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)
hcr :
  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))
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
hw'i2 : w' (i + 2) = 0
hw'i0 : w' i = 1
hi1 : c (i + 1) * r (i + 1) = 1
hi1' : c (i + 1) * (1 - r (i + 1)) = 0
hci1 : c (i + 1) = 1
hri1 : r (i + 1) = 1
hi2 : c (i + 2) * (1 - r (i + 2)) = 1
hi2' : c (i + 2) * r (i + 2) = 0
hci2 : c (i + 2) = 1
hri2 : r (i + 2) = 0
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
have pos : Eq.{u_1 + 1} (α := k) 0 (∏ i : Fin 3, (1 - r i))
Tactic: rw [Finset.prod_eq_zero (by simp) hri2,
      Finset.prod_eq_zero (i := i + 1) (by simp) (by simp [hri1])]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ceva (goal)
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)
hcr :
  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))
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
hw'i2 : w' (i + 2) = 0
hw'i0 : w' i = 1
hi1 : c (i + 1) * r (i + 1) = 1
hi1' : c (i + 1) * (1 - r (i + 1)) = 0
hci1 : c (i + 1) = 1
hri1 : r (i + 1) = 1
hi2 : c (i + 2) * (1 - r (i + 2)) = 1
hi2' : c (i + 2) * r (i + 2) = 0
hci2 : c (i + 2) = 1
hri2 : r (i + 2) = 0
pos : Eq.{u_1 + 1} (α := k) 0 (∏ i : Fin 3, (1 - r i))
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
have pos₁ : Eq.{u_1 + 1} (α := k) 0 0
Tactic: rw [Finset.prod_eq_zero (by simp) hri2,
      Finset.prod_eq_zero (i := i + 1) (by simp) (by simp [hri1])]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ceva (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
hr0 : ∀ (i : Fin 3), r i ≠ 0
p' : P
hp' :
  ∀ (i : Fin 3),
    Membership.mem (γ := 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))))
      p'
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i / (1 - r i)) 1
have rw : Ne.{u_1 + 1} (α := k) (∏ x : Fin 3, r x) 0
Tactic: rw [Finset.prod_div_distrib, ← prod_eq_prod_one_sub_of_mem_line_point_lineMap hp', div_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p b : P
⊢ (s.weightedVSubOfPoint (fun (x : ι) ↦ p) b : (a : ι → k) → V) w =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ b)
have rw : ∑ i ∈ s, w i • (p -ᵥ b) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ b)
Tactic: rw [weightedVSubOfPoint_apply, sum_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p b : P
rw : ∑ i ∈ s, w i • (p -ᵥ b) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ b)
⊢ (s.weightedVSubOfPoint (fun (x : ι) ↦ p) b : (a : ι → k) → V) w =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ b)
have rw₁ : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p -ᵥ b)) (∑ i ∈ s, w i • (p -ᵥ b))
Tactic: rw [weightedVSubOfPoint_apply, sum_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w₁ : V)
    ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w₂ : V)
have simp_rw : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • (p₁ i -ᵥ b)) (∑ i ∈ s, w₂ i • (p₂ i -ᵥ b))
Tactic: simp_rw [weightedVSubOfPoint_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • (p₁ i -ᵥ b)) (∑ i ∈ s, w₂ i • (p₂ i -ᵥ b))
have refine : ∀ (i : ι) (hi : i ∈ s), w₁ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
Tactic: refine sum_congr rfl fun i hi => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
i : ι
hi : i ∈ s
⊢ w₁ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
have rw : w₂ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
Tactic: rw [hw i hi, hp i hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
i : ι
hi : i ∈ s
rw : w₂ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
⊢ w₁ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
have rw₁ : w₂ i • (p₂ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
Tactic: rw [hw i hi, hp i hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w₁ : V)
    ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w₂ : V)
have simp : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • (p i -ᵥ p j)) (∑ i ∈ s, w₂ i • (p i -ᵥ p j))
Tactic: simp only [Finset.weightedVSubOfPoint_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • (p i -ᵥ p j)) (∑ i ∈ s, w₂ i • (p i -ᵥ p j))
have e_f : Eq (α := ι → V) (fun (i : ι) ↦ w₁ i • (p i -ᵥ p j)) fun (i : ι) ↦ w₂ i • (p i -ᵥ p j)
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ Eq (α := ι → V) (fun (i : ι) ↦ w₁ i • (p i -ᵥ p j)) fun (i : ι) ↦ w₂ i • (p i -ᵥ p j)
have e_f : ∀ (i : ι), w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
i : ι
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
have e_f : ∀ (h : i = j), w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
Tactic: rcases eq_or_ne i j with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
i : ι
e_f : ∀ (h : i = j), w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
have e_f₁ : ∀ (h : i ≠ j), w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
Tactic: rcases eq_or_ne i j with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
b₁ b₂ : P
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint p b₁ : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p b₂ : (a : ι → k) → V) w : V)
have h₁ : HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p b₁ : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p b₂ : (a : ι → k) → V) w : V) =
  0
Tactic: apply eq_of_sub_eq_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
b₁ b₂ : P
⊢ HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p b₁ : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint p b₂ : (a : ι → k) → V) w : V) =
    0
have h₁ : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))) 0
Tactic: rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_sub_distrib]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
b₁ b₂ : P
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have s₁ : s
Tactic: congr