awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
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'
⊢ ∃ (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'' : ∀ (i : (↑s : Type u_4)),
  ∃ (r : k),
    (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
        ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
          (j : ι) → k) =
      p'
Tactic: have hp'' : ∀ i : s, ∃ r : k, (fs i).affineCombination k p
      (AffineMap.lineMap (Pi.single (i : ι) 1) (w i) r) = p' := by
    intro i
    simp_rw [mem_affineSpan_pair_iff_exists_lineMap_eq] at hp'
    obtain ⟨r, rfl⟩ := hp' i
    exact ⟨r, by simp [hfs]⟩
-- 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 ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
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'
hp'' :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
            (j : ι) → k) =
        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 : ∀ (i' : ι) (hi' : i' ∈ s),
  ∃ (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 ⟨i', hi'⟩ := hs
Cleared hypotheses: hs
-- 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 ι
fs : (↑s : Type u_4) → Finset ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
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'
hp'' :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
            (j : ι) → k) =
        p'
i' : ι
hi' : i' ∈ s
⊢ ∃ (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 : ∀ (ri' : k)
  (hri' :
    (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
        ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
                (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
              (a : k) → (j : ι) → k)
            ri' :
          (j : ι) → k) =
      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
Tactic: obtain ⟨ri', hri'⟩ := hp'' ⟨i', hi'⟩
-- 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 ι
fs : (↑s : Type u_4) → Finset ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
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'
hp'' :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
            (j : ι) → k) =
        p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
      ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
              (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
            (a : k) → (j : ι) → k)
          ri' :
        (j : ι) → k) =
    p'
w' : ι → k :=
  (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
      (a : k) → (j : ι) → k)
    ri'
⊢ ∃ (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_1 : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi'), w' j) 1
Tactic: refine ⟨w', fs ⟨i', hi'⟩, ?_, ?_, ?_⟩
-- 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 ι
fs : (↑s : Type u_4) → Finset ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
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'
hp'' :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
            (j : ι) → k) =
        p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
      ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
              (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
            (a : k) → (j : ι) → k)
          ri' :
        (j : ι) → k) =
    p'
w' : ι → k :=
  (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
      (a : k) → (j : ι) → k)
    ri'
refine_1 : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi'), w' 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 refine_2 : (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P) w' = p'
Tactic: refine ⟨w', fs ⟨i', hi'⟩, ?_, ?_, ?_⟩
-- 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 ι
fs : (↑s : Type u_4) → Finset ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
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'
hp'' :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
            (j : ι) → k) =
        p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
      ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
              (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
            (a : k) → (j : ι) → k)
          ri' :
        (j : ι) → k) =
    p'
w' : ι → k :=
  (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
      (a : k) → (j : ι) → k)
    ri'
refine_1 : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi'), w' j) 1
refine_2 : (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P) w' = 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 refine_3 : ∀ (i : (↑s : Type u_4)),
  ∃ (r : k),
    ∀ (j : ι),
      r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j =
        ((↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) : Set ι) \ {(↑i : ι)}).indicator w' j
Tactic: refine ⟨w', fs ⟨i', hi'⟩, ?_, ?_, ?_⟩
-- 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 ι
fs : (↑s : Type u_4) → Finset ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
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'
hp'' :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
            (j : ι) → k) =
        p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
      ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
              (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
            (a : k) → (j : ι) → k)
          ri' :
        (j : ι) → k) =
    p'
w' : ι → k :=
  (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
      (a : k) → (j : ι) → k)
    ri'
i : (↑s : Type u_4)
⊢ ∃ (r : k),
    ∀ (j : ι),
      r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j =
        ((↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) : Set ι) \ {(↑i : ι)}).indicator w' j
have refine_3 : ∀ (r : k)
  (hr :
    (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
        ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
          (j : ι) → k) =
      p'),
  ∃ (r : k),
    ∀ (j : ι),
      r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j =
        ((↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) : Set ι) \ {(↑i : ι)}).indicator w' j
Tactic: obtain ⟨r, hr⟩ := hp'' 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 ι
fs : (↑s : Type u_4) → Finset ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
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'
hp'' :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
            (j : ι) → k) =
        p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
      ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
              (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
            (a : k) → (j : ι) → k)
          ri' :
        (j : ι) → k) =
    p'
w' : ι → k :=
  (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
      (a : k) → (j : ι) → k)
    ri'
i : (↑s : Type u_4)
r : k
hr :
  (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
      ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
        (j : ι) → k) =
    p'
⊢ ∃ (r : k),
    ∀ (j : ι),
      r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j =
        ((↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) : Set ι) \ {(↑i : ι)}).indicator w' j
have refine_3 : ∀ (j : ι),
  r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j =
    ((↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) : Set ι) \ {(↑i : ι)}).indicator w' j
Tactic: refine ⟨r, ?_⟩
-- 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 ι
fs : (↑s : Type u_4) → Finset ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
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'
hp'' :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
            (j : ι) → k) =
        p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
      ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
              (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
            (a : k) → (j : ι) → k)
          ri' :
        (j : ι) → k) =
    p'
w' : ι → k :=
  (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
      (a : k) → (j : ι) → k)
    ri'
i : (↑s : Type u_4)
r : k
hr :
  (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
      ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
        (j : ι) → k) =
    p'
⊢ ∀ (j : ι),
    r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j =
      ((↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) : Set ι) \ {(↑i : ι)}).indicator w' j
have hr₁ : Eq.{u_3 + 1} (α := P)
  ((Finset.affineCombination k (fs i) p : (a : ι → k) → P)
      ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
        (j : ι) → k) :
    P)
  ((Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
      ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
              (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
            (a : k) → (j : ι) → k)
          ri' :
        (j : ι) → k) :
    P)
Tactic: rw [← hri'] at hr
Cleared hypotheses: hr
-- 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 ι
fs : (↑s : Type u_4) → Finset ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
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'
hp'' :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
            (j : ι) → k) =
        p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
      ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
              (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
            (a : k) → (j : ι) → k)
          ri' :
        (j : ι) → k) =
    p'
w' : ι → k :=
  (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
      (a : k) → (j : ι) → k)
    ri'
i : (↑s : Type u_4)
r : k
hr :
  Eq.{u_3 + 1} (α := P)
    ((Finset.affineCombination k (fs i) p : (a : ι → k) → P)
        ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
          (j : ι) → k) :
      P)
    ((Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
        ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
                (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
              (a : k) → (j : ι) → k)
            ri' :
          (j : ι) → k) :
      P)
⊢ ∀ (j : ι),
    r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j =
      ((↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) : Set ι) \ {(↑i : ι)}).indicator w' j
have hr₁ : Eq.{u_3 + 1} (α := P)
  ((Finset.affineCombination k (fs i) p : (a : ι → k) → P)
      (HSMul.hSMul (β := ι → k) (1 - r) (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) + r • w i) :
    P)
  ((Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
      (HSMul.hSMul (β := ι → k) (1 - ri') (Pi.single (M := fun (j : ι) ↦ k) i' 1) +
        ri' • w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
    P)
Tactic: simp only [AffineMap.lineMap_apply_module] at hr
Cleared hypotheses: hr
-- 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 ι
fs : (↑s : Type u_4) → Finset ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
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'
hp'' :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
            (j : ι) → k) =
        p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
      ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
              (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
            (a : k) → (j : ι) → k)
          ri' :
        (j : ι) → k) =
    p'
w' : ι → k :=
  (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
      (a : k) → (j : ι) → k)
    ri'
i : (↑s : Type u_4)
r : k
hr :
  Eq.{u_3 + 1} (α := P)
    ((Finset.affineCombination k (fs i) p : (a : ι → k) → P)
        (HSMul.hSMul (β := ι → k) (1 - r) (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) + r • w i) :
      P)
    ((Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
        (HSMul.hSMul (β := ι → k) (1 - ri') (Pi.single (M := fun (j : ι) ↦ k) i' 1) +
          ri' • w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
      P)
⊢ ∀ (j : ι),
    r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j =
      ((↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) : Set ι) \ {(↑i : ι)}).indicator w' j
have refine_3 : ∀
  (hind :
    (↑(fs i) : Set ι).indicator
        (HSMul.hSMul (β := ι → k) (1 - r) (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) + r • w i) =
      (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) : Set ι).indicator
        (HSMul.hSMul (β := ι → k) (1 - ri') (Pi.single (M := fun (j : ι) ↦ k) i' 1) +
          ri' • w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')))
  (j : ι),
  r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j =
    ((↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) : Set ι) \ {(↑i : ι)}).indicator w' j
Tactic: have hind := hp.indicator_eq_of_affineCombination_eq _ _ _ _ ?_ ?_ hr