-- 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
0 :
  ∀ (hi : c ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) = 0)
    (hw'i1 : w' (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) 1) = 0)
    (hw'i2 : w' (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) 2) = 0),
    w' ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) = w' 0 + w' 1 + w' 2
1 :
  ∀ (hi : c ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) = 0)
    (hw'i1 : w' (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) 1) = 0)
    (hw'i2 : w' (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) 2) = 0),
    w' ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) = w' 0 + w' 1 + w' 2
⊢ w' i = w' 0 + w' 1 + w' 2
have 2 : ∀ (hi : c ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) = 0)
  (hw'i1 : w' (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) 1) = 0)
  (hw'i2 : w' (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) 2) = 0),
  w' ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) = w' 0 + w' 1 + w' 2
Tactic: fin_cases i
Cleared hypotheses: i, hi, hw'i1, hw'i2