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
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j : ι, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) (w i) : P))))
      p'
obtain :
  ∀ (w'' : ι → k) (fs'' : Finset ι) (hw'' : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs'', w'' j) 1)
    (hw''p' : (Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' = p')
    (hi :
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j =
              ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j),
    ∃ (w' : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ j : ι, w' j) 1 ∧
        (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w' = p' ∧
          ∀ (i : (↑s : Type u_4)),
            ∃ (r : k), ∀ (j : ι), r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ w' j
refine_1 :
  ∀ (w'' : ι → k) (fs'' : Finset ι) (hw'' : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs'', w'' j) 1)
    (hw''p' : (Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' = p')
    (hi :
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j =
              ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j),
    Eq.{u_1 + 1} (α := k) (∑ j : ι, (↑fs'' : Set ι).indicator w'' j) 1
⊢ ∃ (w' : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ j : ι, w' j) 1 ∧
      (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k), ∀ (j : ι), r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ w' j
have refine_2 : ∀ (w'' : ι → k) (fs'' : Finset ι) (hw'' : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs'', w'' j) 1)
  (hw''p' : (Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' = p')
  (hi :
    ∀ (i : (↑s : Type u_4)),
      ∃ (r : k),
        ∀ (j : ι),
          r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j),
  (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) ((↑fs'' : Set ι).indicator w'') = p'
Tactic: classical
  obtain ⟨w'', fs'', hw'', hw''p', hi⟩ := hp.exists_affineCombination_eq_smul_eq hs hw hp'
  refine ⟨Set.indicator fs'' w'', ?_, ?_, ?_⟩
  · rw [← hw'']
    exact Finset.sum_indicator_subset _ (by simp)
  · rw [← hw''p']
    exact (Finset.affineCombination_indicator_subset _ _ (by simp)).symm
  · intro i
    obtain ⟨r, hr⟩ := hi i
    refine ⟨r, fun j ↦ ?_⟩
    convert! hr j using 1
    · simp [Set.indicator_apply]
    · by_cases hj : j = (i : ι) <;> simp [Set.indicator_apply, hj]
-- 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
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) (∏ i : Fin 3, (1 - r i))
have inl : Subsingleton k → Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
Tactic: rcases subsingleton_or_nontrivial k
-- 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
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'
inl : Subsingleton k → Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
have inr : Nontrivial k → Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
Tactic: rcases subsingleton_or_nontrivial k
-- 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
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'
h : 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))
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
have hw : ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1
Tactic: have hw : ∀ i, ∑ j, w i j = 1 := by simp [w]
-- 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
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'
h : 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
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
have hp'w : ∀ (i : (↑Set.univ : Type)),
  Membership.mem (γ := 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))))
    p'
Tactic: have hp'w : ∀ i : ↑(Set.univ : Set (Fin 3)),
      p' ∈ line[k, t.points i, Finset.univ.affineCombination k t.points (w i)] := by
    simpa [w] using hp'
-- 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
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'
h : 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
hp'w :
  ∀ (i : (↑Set.univ : Type)),
    Membership.mem (γ := 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))))
      p'
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
have inr : ∀ (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)),
  Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
Tactic: obtain ⟨w', hw', rfl, h⟩ :=
    t.independent.exists_affineCombination_eq_smul_eq_of_fintype (by simp) hw hp'w
Cleared hypotheses: p', hp', hp'w
-- 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)
i : Fin 3
⊢ ∃ (c : k),
    ∀ (j : Fin 3),
      j ≠ i → c * w (Subtype.mk (p := fun (x : Fin 3) ↦ Membership.mem (γ := Set (Fin 3)) Set.univ x) i ⋯) j = w' j
have obtain : ∀ (c : k)
  (hc :
    ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
      c *
          Set.indicator
            {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                      Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) Set.univ x) i sorry) :
                  Fin (2 + 1))}ᶜ
            (w
              (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) Set.univ x) i sorry))
            j =
        Set.indicator
          {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                    Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) Set.univ x) i sorry) :
                Fin (2 + 1))}ᶜ
          w' j),
  ∃ (c : k),
    ∀ (j : Fin 3),
      j ≠ i → c * w (Subtype.mk (p := fun (x : Fin 3) ↦ Membership.mem (γ := Set (Fin 3)) Set.univ x) i sorry) j = w' j
Tactic: obtain ⟨c, hc⟩ := h ⟨i, by simp⟩
-- 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)
i : Fin 3
c : k
hc :
  ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
    c *
        Set.indicator
          {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                    Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) Set.univ x) i ⋯) :
                Fin (2 + 1))}ᶜ
          (w
            (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
              Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) Set.univ x) i ⋯))
          j =
      Set.indicator
        {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                  Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) Set.univ x) i ⋯) :
              Fin (2 + 1))}ᶜ
        w' j
⊢ ∃ (c : k),
    ∀ (j : Fin 3),
      j ≠ i → c * w (Subtype.mk (p := fun (x : Fin 3) ↦ Membership.mem (γ := Set (Fin 3)) Set.univ x) i ⋯) j = w' j
have refine : ∀ (j : Fin 3) (hj : j ≠ i),
  c * w (Subtype.mk (p := fun (x : Fin 3) ↦ Membership.mem (γ := Set (Fin 3)) Set.univ x) i sorry) j = w' j
Tactic: refine ⟨c, fun j hj ↦ ?_⟩
-- 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)
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
have h' : ∀ (i : Fin 3),
  ∃ (c : k),
    ∀ (j : Fin 3),
      j ≠ i → c * w (Subtype.mk (p := fun (x : Fin 3) ↦ Membership.mem (γ := Set (Fin 3)) Set.univ x) i sorry) j = w' j
Tactic: have h' : ∀ i : Fin 3, ∃ c : k, ∀ j ≠ i, c * w ⟨i, by simp⟩ j = w' j := by
    intro i
    obtain ⟨c, hc⟩ := h ⟨i, by simp⟩
    refine ⟨c, fun j hj ↦ ?_⟩
    simpa [hj] using hc j
-- 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)
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
have hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
Tactic: have hc (i : Fin 3) : ∀ j : Fin 3, j ≠ i →
    c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j :=
      (h' i).choose_spec
-- 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
i : Fin 3
⊢ c i * (1 - r i) = w' (i + 1)
have rw : c i * (1 - r i) = c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) (i + 1)
Tactic: rw [← hc i (i + 1) (by simp)]
-- 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
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))
have hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
Tactic: have hc1 (i : Fin 3) : c i * (1 - r i) = w' (i + 1) := by
    rw [← hc i (i + 1) (by simp)]
    simp