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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
i : (↑s : Type u_4)
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
have simp_rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ insert (↑i : ι) (fs i), (↑(fs i) : Set ι).indicator (w i) x) (∑ j ∈ fs i, w i j)
Tactic: simp_rw [← hw i, fsx, wx]
-- 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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
i : (↑s : Type u_4)
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ insert (↑i : ι) (fs i), (↑(fs i) : Set ι).indicator (w i) x) (∑ j ∈ fs i, w i j)
have pos : ∀ (hi : (↑i : ι) ∈ fs i),
  Eq.{u_1 + 1} (α := k) (∑ x ∈ insert (↑i : ι) (fs i), (↑(fs i) : Set ι).indicator (w i) x) (∑ j ∈ fs i, w i j)
Tactic: by_cases hi : (i : ι) ∈ fs i
-- 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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
i : (↑s : Type u_4)
pos :
  ∀ (hi : (↑i : ι) ∈ fs i),
    Eq.{u_1 + 1} (α := k) (∑ x ∈ insert (↑i : ι) (fs i), (↑(fs i) : Set ι).indicator (w i) x) (∑ j ∈ fs i, w i j)
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ insert (↑i : ι) (fs i), (↑(fs i) : Set ι).indicator (w i) x) (∑ j ∈ fs i, w i j)
have neg : ∀ (hi : (↑i : ι) ∉ fs i),
  Eq.{u_1 + 1} (α := k) (∑ x ∈ insert (↑i : ι) (fs i), (↑(fs i) : Set ι).indicator (w i) x) (∑ j ∈ fs i, w i j)
Tactic: by_cases hi : (i : ι) ∈ fs i
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ceva (hypothesis)
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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
⊢ ∃ (w' : ι → k) (fs' : Finset ι),
    Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
      (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k),
            ∀ (j : ι),
              r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
have hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
Tactic: have hwx : ∀ i, ∑ j ∈ fsx i, wx i j = 1 := by
    intro i
    simp_rw [← hw i, fsx, wx]
    by_cases hi : (i : ι) ∈ fs i <;> simpa [hi] using Finset.sum_congr rfl (by aesop)
-- 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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
i : (↑s : Type u_4)
⊢ Membership.mem (γ := AffineSubspace k P)
    (affineSpan k
      (insert (p (↑i : ι)) (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
    p'
have h : Eq.{u_3 + 1} (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P)
  ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i) : P)
Tactic: convert! hp' i using 4
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ceva (hypothesis)
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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
⊢ ∃ (w' : ι → k) (fs' : Finset ι),
    Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
      (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k),
            ∀ (j : ι),
              r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
have hp'x : ∀ (i : (↑s : Type u_4)),
  Membership.mem (γ := AffineSubspace k P)
    (affineSpan k
      (insert (p (↑i : ι)) (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
    p'
Tactic: have hp'x : ∀ i : s, p' ∈ line[k, p i, (fsx i).affineCombination k p (wx i)] := by
    intro i
    convert! hp' i using 4
    simp_rw [fsx, wx]
    exact (Finset.affineCombination_indicator_subset _ _ (by simp)).symm
-- 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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
⊢ ∃ (w' : ι → k) (fs' : Finset ι),
    Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
      (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k),
            ∀ (j : ι),
              r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
have obtain : ∀ (w' : ι → k) (fs' : Finset ι)
  (h :
    Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
      (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k),
            ∀ (j : ι),
              r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j),
  ∃ (w' : ι → k) (fs' : Finset ι),
    Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
      (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k),
            ∀ (j : ι),
              r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
Tactic: obtain ⟨w', fs', h⟩ := hp.exists_affineCombination_eq_smul_eq_aux hs hfsx hwx hp'x
-- 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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
w' : ι → k
fs' : Finset ι
h :
  Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
    (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
⊢ ∃ (w' : ι → k) (fs' : Finset ι),
    Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
      (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k),
            ∀ (j : ι),
              r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
have refine : ∀ (i : (↑s : Type u_4)),
  ∃ (r : k),
    ∀ (j : ι), r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
Tactic: refine ⟨w', fs', h.1, h.2.1, fun i ↦ ?_⟩
-- 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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
w' : ι → k
fs' : Finset ι
h :
  Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
    (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
i : (↑s : Type u_4)
⊢ ∃ (r : k),
    ∀ (j : ι), r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
have obtain : ∀ (r : k)
  (hr :
    ∀ (j : ι), r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j),
  ∃ (r : k),
    ∀ (j : ι), r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
Tactic: obtain ⟨r, hr⟩ := h.2.2 i
-- 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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
w' : ι → k
fs' : Finset ι
h :
  Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
    (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
i : (↑s : Type u_4)
r : k
hr : ∀ (j : ι), r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
⊢ ∃ (r : k),
    ∀ (j : ι), r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
have refine : ∀ (j : ι), r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
Tactic: refine ⟨r, fun j ↦ ?_⟩
-- 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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
w' : ι → k
fs' : Finset ι
h :
  Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
    (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
i : (↑s : Type u_4)
r : k
hr : ∀ (j : ι), r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
j : ι
⊢ r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
have h₁ : ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j
Tactic: convert! hr j using 2
-- 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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
w' : ι → k
fs' : Finset ι
h :
  Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
    (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
i : (↑s : Type u_4)
r : k
hr : ∀ (j : ι), r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
j : ι
⊢ ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j
have h₁ : (if j ∈ fs i ∧ ¬j = (↑i : ι) then w i j else 0) = if j ∈ fs i ∧ ¬j = (↑i : ι) then if j ∈ fs i then w i j else 0 else 0
Tactic: simp only [Set.indicator_apply, Set.mem_diff, SetLike.mem_coe, Set.mem_singleton_iff,
    Finset.coe_insert, Set.insert_diff_of_mem, fsx, wx]
-- 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
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, 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 (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
let let₁ let₂ :
  ∃ (w' : ι → k) (fs' : Finset ι),
    Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
      (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k),
            ∀ (j : ι),
              r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
⊢ ∃ (w' : ι → k) (fs' : Finset ι),
    Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
      (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k),
            ∀ (j : ι),
              r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
have let₃ : let fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i);
∀ (hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i),
  ∃ (w' : ι → k) (fs' : Finset ι),
    Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
      (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k),
            ∀ (j : ι),
              r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
Tactic: classical
  let fsx : s → Finset ι := fun i ↦ insert (i : ι) (fs i)
  have hfsx : ∀ i, (i : ι) ∈ fsx i := by simp [fsx]
  let wx : s → ι → k := fun i ↦ Set.indicator (fs i) (w i)
  have hwx : ∀ i, ∑ j ∈ fsx i, wx i j = 1 := by
    intro i
    simp_rw [← hw i, fsx, wx]
    by_cases hi : (i : ι) ∈ fs i <;> simpa [hi] using Finset.sum_congr rfl (by aesop)
  have hp'x : ∀ i : s, p' ∈ line[k, p i, (fsx i).affineCombination k p (wx i)] := by
    intro i
    convert! hp' i using 4
    simp_rw [fsx, wx]
    exact (Finset.affineCombination_indicator_subset _ _ (by simp)).symm
  obtain ⟨w', fs', h⟩ := hp.exists_affineCombination_eq_smul_eq_aux hs hfsx hwx hp'x
  refine ⟨w', fs', h.1, h.2.1, fun i ↦ ?_⟩
  obtain ⟨r, hr⟩ := h.2.2 i
  refine ⟨r, fun j ↦ ?_⟩
  convert! hr j using 2
  simp only [Set.indicator_apply, Set.mem_diff, SetLike.mem_coe, Set.mem_singleton_iff,
    Finset.coe_insert, Set.insert_diff_of_mem, fsx, wx]
  grind