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
ι : 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'
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
i : (↑s : Type u_4)
refine_3 :
  ∀ (r : k)
    (hr :
      ∀ (j : ι),
        r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j),
    ∃ (r : k),
      ∀ (j : ι), r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j
⊢ ∃ (r : k),
    ∀ (j : ι), r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j

Tactic:
obtain ⟨r, hr⟩ := hi i
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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'
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
i : (↑s : Type u_4)
r : k
hr :
  ∀ (j : ι),
    r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
⊢ ∃ (r : k),
    ∀ (j : ι), r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j

Tactic:
⟨r, fun j ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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'
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
i : (↑s : Type u_4)
r : k
hr :
  ∀ (j : ι),
    r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
refine_3 :
  ∀ (j : ι), r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j
⊢ ∃ (r : k),
    ∀ (j : ι), r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j

Tactic:
refine ⟨r, fun j ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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'
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
i : (↑s : Type u_4)
r : k
hr :
  ∀ (j : ι),
    r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
j : ι
⊢ r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j

Tactic:
hr j
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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'
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
i : (↑s : Type u_4)
r : k
hr :
  ∀ (j : ι),
    r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
j : ι
h : r * Set.indicator {(↑i : ι)}ᶜ (w i) j = r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j
h₁ : Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
⊢ r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j

Tactic:
convert! hr j using 1
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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'
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
i : (↑s : Type u_4)
r : k
hr :
  ∀ (j : ι),
    r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
j : ι
⊢ r * Set.indicator {(↑i : ι)}ᶜ (w i) j = r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j

Tactic:
simp [Set.indicator_apply]

Premises used: Set.indicator_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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'
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
i : (↑s : Type u_4)
r : k
hr :
  ∀ (j : ι),
    r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
j : ι
pos :
  ∀ (hj : j = (↑i : ι)),
    Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
neg :
  ∀ (hj : ¬j = (↑i : ι)),
    Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
⊢ Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j

Tactic:
by_cases hj : j = (i : ι)

Premises used: Subtype.val
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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'
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
i : (↑s : Type u_4)
r : k
hr :
  ∀ (j : ι),
    r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
j : ι
hj : j = (↑i : ι)
⊢ Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j

Tactic:
simp [Set.indicator_apply, hj]

Premises used: Set.indicator_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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'
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
i : (↑s : Type u_4)
r : k
hr :
  ∀ (j : ι),
    r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
j : ι
hj : ¬j = (↑i : ι)
⊢ Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j

Tactic:
simp [Set.indicator_apply, hj]

Premises used: Set.indicator_apply
-- 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
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))
inr : Nontrivial 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))

Tactic:
rcases subsingleton_or_nontrivial k

Premises used: subsingleton_or_nontrivial
-- 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
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 : Subsingleton k
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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
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 : Subsingleton k
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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
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))
⊢ ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1

Tactic:
simp [w]
-- 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
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))
⊢ ∀ (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]
-- 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
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
⊢ ∀ (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:
simpa [w] using hp'
-- 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
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
⊢ ∀ (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'
-- 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
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'
⊢ Set.Nonempty (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) Set.univ

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
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'
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))
⊢ 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

Premises used: AffineIndependent.exists_affineCombination_eq_smul_eq_of_fintype, Affine.Simplex.independent, 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)
i : Fin 3
c : k
j : Fin 3
⊢ Membership.mem (γ := Set (Fin 3)) Set.univ i

Tactic:
simp