awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
⊢ Membership.mem (α := V) (γ := Submodule k V)
      (vectorSpan k (P := P)
        (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
          (singleton (α := P) ((affineCombination k s p : (a : ι → k) → P) w₂ : P))))
      ((s.weightedVSub p : (a : ι → k) → V) w : V) ↔
    ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
have rw : (∃ (r : k),
    r •
        VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
          ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
      (s.weightedVSub p : (a : ι → k) → V) w) ↔
  ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
Tactic: rw [mem_vectorSpan_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
⊢ (∃ (r : k),
      r •
          VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
        (s.weightedVSub p : (a : ι → k) → V) w) ↔
    ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
have refine_1 : ∀
  (h :
    ∃ (r : k),
      r •
          VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
        (s.weightedVSub p : (a : ι → k) → V) w),
  ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
refine_1 :
  ∀
    (h :
      ∃ (r : k),
        r •
            VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
              ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
          (s.weightedVSub p : (a : ι → k) → V) w),
    ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
⊢ (∃ (r : k),
      r •
          VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
        (s.weightedVSub p : (a : ι → k) → V) w) ↔
    ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
have refine_2 : ∀ (h : ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)),
  ∃ (r : k),
    r •
        VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
          ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
      (s.weightedVSub p : (a : ι → k) → V) w
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h_1 : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
h :
  ∃ (r : k),
    r •
        VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
          ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
      (s.weightedVSub p : (a : ι → k) → V) w
⊢ ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
have refine_1 : ∀ (r : k)
  (hr :
    r •
        VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
          ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
      (s.weightedVSub p : (a : ι → k) → V) w),
  ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
Tactic: rcases h with ⟨r, hr⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr :
  r •
      VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
        ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (s.weightedVSub p : (a : ι → k) → V) w
⊢ ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
have refine_1 : ∀ (i : ι) (hi : i ∈ s), w i = r * (w₁ i - w₂ i)
Tactic: refine ⟨r, fun i hi => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr :
  r •
      VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
        ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (s.weightedVSub p : (a : ι → k) → V) w
i : ι
hi : i ∈ s
⊢ w i = r * (w₁ i - w₂ i)
have refine_1 : ∀ (hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)) (i : ι)
  (hi : i ∈ s), w i = r * (w₁ i - w₂ i)
Tactic: rw [s.affineCombination_vsub, ← s.weightedVSub_const_smul, ← sub_eq_zero, ← map_sub] at hr
Cleared hypotheses: hr, i, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)
i : ι
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 0
have simp_rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, ((r • (w₁ - w₂)) x - w x)) 0
Tactic: simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)
i : ι
hi : i ∈ s
simp_rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, ((r • (w₁ - w₂)) x - w x)) 0
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 0
have simp_rw₁ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ - w₂) x - w x)) 0
Tactic: simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)
i : ι
hi : i ∈ s
simp_rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, ((r • (w₁ - w₂)) x - w x)) 0
simp_rw₁ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ - w₂) x - w x)) 0
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 0
have simp_rw₂ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ x - w₂ x) - w x)) 0
Tactic: simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)
i : ι
hi : i ∈ s
simp_rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, ((r • (w₁ - w₂)) x - w x)) 0
simp_rw₁ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ - w₂) x - w x)) 0
simp_rw₂ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ x - w₂ x) - w x)) 0
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 0
have simp_rw₃ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • w₁ x - r • w₂ x - w x)) 0
Tactic: simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)
i : ι
hi : i ∈ s
simp_rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, ((r • (w₁ - w₂)) x - w x)) 0
simp_rw₁ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ - w₂) x - w x)) 0
simp_rw₂ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ x - w₂ x) - w x)) 0
simp_rw₃ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • w₁ x - r • w₂ x - w x)) 0
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 0
have simp_rw₄ : HSub.hSub (α := k) (∑ x ∈ s, r • w₁ x) (∑ x ∈ s, r • w₂ x) - ∑ x ∈ s, w x = 0
Tactic: simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)
i : ι
hi : i ∈ s
simp_rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, ((r • (w₁ - w₂)) x - w x)) 0
simp_rw₁ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ - w₂) x - w x)) 0
simp_rw₂ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ x - w₂ x) - w x)) 0
simp_rw₃ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • w₁ x - r • w₂ x - w x)) 0
simp_rw₄ : HSub.hSub (α := k) (∑ x ∈ s, r • w₁ x) (∑ x ∈ s, r • w₂ x) - ∑ x ∈ s, w x = 0
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 0
have simp_rw₅ : HSMul.hSMul (β := k) r (∑ x ∈ s, w₁ x) - HSMul.hSMul (β := k) r (∑ x ∈ s, w₂ x) - ∑ x ∈ s, w x = 0
Tactic: simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)
i : ι
hi : i ∈ s
simp_rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, ((r • (w₁ - w₂)) x - w x)) 0
simp_rw₁ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ - w₂) x - w x)) 0
simp_rw₂ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ x - w₂ x) - w x)) 0
simp_rw₃ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • w₁ x - r • w₂ x - w x)) 0
simp_rw₄ : HSub.hSub (α := k) (∑ x ∈ s, r • w₁ x) (∑ x ∈ s, r • w₂ x) - ∑ x ∈ s, w x = 0
simp_rw₅ : HSMul.hSMul (β := k) r (∑ x ∈ s, w₁ x) - HSMul.hSMul (β := k) r (∑ x ∈ s, w₂ x) - ∑ x ∈ s, w x = 0
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 0
have simp_rw₆ : HSMul.hSMul (β := k) r (∑ x ∈ s, w₁ x) - HSMul.hSMul (β := k) r (∑ x ∈ s, w₂ x) - 0 = 0
Tactic: simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)
i : ι
hi : i ∈ s
simp_rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, ((r • (w₁ - w₂)) x - w x)) 0
simp_rw₁ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ - w₂) x - w x)) 0
simp_rw₂ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ x - w₂ x) - w x)) 0
simp_rw₃ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • w₁ x - r • w₂ x - w x)) 0
simp_rw₄ : HSub.hSub (α := k) (∑ x ∈ s, r • w₁ x) (∑ x ∈ s, r • w₂ x) - ∑ x ∈ s, w x = 0
simp_rw₅ : HSMul.hSMul (β := k) r (∑ x ∈ s, w₁ x) - HSMul.hSMul (β := k) r (∑ x ∈ s, w₂ x) - ∑ x ∈ s, w x = 0
simp_rw₆ : HSMul.hSMul (β := k) r (∑ x ∈ s, w₁ x) - HSMul.hSMul (β := k) r (∑ x ∈ s, w₂ x) - 0 = 0
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 0
have simp_rw₇ : HSMul.hSMul (β := k) r 1 - HSMul.hSMul (β := k) r (∑ x ∈ s, w₂ x) - 0 = 0
Tactic: simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)
i : ι
hi : i ∈ s
simp_rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, ((r • (w₁ - w₂)) x - w x)) 0
simp_rw₁ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ - w₂) x - w x)) 0
simp_rw₂ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • (w₁ x - w₂ x) - w x)) 0
simp_rw₃ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (r • w₁ x - r • w₂ x - w x)) 0
simp_rw₄ : HSub.hSub (α := k) (∑ x ∈ s, r • w₁ x) (∑ x ∈ s, r • w₂ x) - ∑ x ∈ s, w x = 0
simp_rw₅ : HSMul.hSMul (β := k) r (∑ x ∈ s, w₁ x) - HSMul.hSMul (β := k) r (∑ x ∈ s, w₂ x) - ∑ x ∈ s, w x = 0
simp_rw₆ : HSMul.hSMul (β := k) r (∑ x ∈ s, w₁ x) - HSMul.hSMul (β := k) r (∑ x ∈ s, w₂ x) - 0 = 0
simp_rw₇ : HSMul.hSMul (β := k) r 1 - HSMul.hSMul (β := k) r (∑ x ∈ s, w₂ x) - 0 = 0
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 0
have simp_rw₈ : HSMul.hSMul (β := k) r 1 - HSMul.hSMul (β := k) r 1 - 0 = 0
Tactic: simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)
i : ι
hi : i ∈ s
⊢ w i = r * (w₁ i - w₂ i)
have hw' : Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 0
Tactic: have hw' : (∑ j ∈ s, (r • (w₁ - w₂) - w) j) = 0 := by
      simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)
i : ι
hi : i ∈ s
hw' : Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 0
⊢ w i = r * (w₁ i - w₂ i)
have hr' : (r • (w₁ - w₂) - w) i = 0
Tactic: have hr' := h s _ hw' hr i hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂) - w) : V) (0 : V)
i : ι
hi : i ∈ s
hw' : Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 0
hr' : (r • (w₁ - w₂) - w) i = 0
⊢ w i = r * (w₁ i - w₂ i)
have refine_1 : r • (w₁ i - w₂ i) - w i = 0
Tactic: rw [eq_comm, ← sub_eq_zero, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h_1 : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
h : ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
⊢ ∃ (r : k),
    r •
        VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
          ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
      (s.weightedVSub p : (a : ι → k) → V) w
have refine_2 : ∀ (r : k) (hr : ∀ i ∈ s, w i = r * (w₁ i - w₂ i)),
  ∃ (r : k),
    r •
        VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
          ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
      (s.weightedVSub p : (a : ι → k) → V) w
Tactic: rcases h with ⟨r, hr⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr : ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
⊢ ∃ (r : k),
    r •
        VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
          ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
      (s.weightedVSub p : (a : ι → k) → V) w
have refine_2 : r •
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
  (s.weightedVSub p : (a : ι → k) → V) w
Tactic: refine ⟨r, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
w' : (i : ι) → k := fun (i : ι) ↦ r * (w₁ i - w₂ i)
hr : ∀ i ∈ s, w i = w' i
⊢ r •
      VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
        ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (s.weightedVSub p : (a : ι → k) → V) w
have refine_2 : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂)) : V)
  ((s.weightedVSub p : (a : ι → k) → V) w' : V)
Tactic: rw [s.weightedVSub_congr hr fun _ _ => rfl, s.affineCombination_vsub, ←
      s.weightedVSub_const_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
h_1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
⊢ Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
          (singleton (α := P) ((affineCombination k s p : (a : ι → k) → P) w₂ : P))))
      ((affineCombination k s p : (a : ι → k) → P) w : P) ↔
    ∃ (r : k), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
have rw : (∃ (r : k), ∀ i ∈ s, (w - w₁) i = r * (w₂ i - w₁ i)) ↔ ∃ (r : k), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
Tactic: rw [← vsub_vadd (s.affineCombination k p w) (s.affineCombination k p w₁),
    AffineSubspace.vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _),
    direction_affineSpan, s.affineCombination_vsub, Set.pair_comm,
    weightedVSub_mem_vectorSpan_pair h _ hw₂ hw₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
h_1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
rw : (∃ (r : k), ∀ i ∈ s, (w - w₁) i = r * (w₂ i - w₁ i)) ↔ ∃ (r : k), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
          (singleton (α := P) ((affineCombination k s p : (a : ι → k) → P) w₂ : P))))
      ((affineCombination k s p : (a : ι → k) → P) w : P) ↔
    ∃ (r : k), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
have rw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, (w - w₁) i) 0
Tactic: rw [← vsub_vadd (s.affineCombination k p w) (s.affineCombination k p w₁),
    AffineSubspace.vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _),
    direction_affineSpan, s.affineCombination_vsub, Set.pair_comm,
    weightedVSub_mem_vectorSpan_pair h _ hw₂ hw₁]