awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
refine_1 : ∀ (i : ι) (hi : i ∈ s), w i = r * (w₁ i - w₂ i)
⊢ ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)

Tactic:
refine ⟨r, fun i hi => ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
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)
⊢ w i = r * (w₁ i - w₂ i)

Tactic:
rw [s.affineCombination_vsub, ← s.weightedVSub_const_smul, ← sub_eq_zero, ← map_sub] at hr

Premises used: Finset.affineCombination_vsub, map_sub, sub_eq_zero, Finset.weightedVSub_const_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
simp_rw₈ : HSMul.hSMul (β := k) r 1 - HSMul.hSMul (β := k) r 1 - 0 = 0
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, (r • (w₁ - w₂) - w) j) 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]

Premises used: sub_self, smul_sub, Finset.sum_sub_distrib, Finset.smul_sum, Pi.sub_apply, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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

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]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
⊢ (r • (w₁ - w₂) - w) i = 0

Tactic:
have hr' := h s _ hw' hr i hi
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
refine_1 : r • (w₁ i - w₂ i) - w i = 0
⊢ w i = r * (w₁ i - w₂ i)

Tactic:
rw [eq_comm, ← sub_eq_zero, ← smul_eq_mul]

Premises used: sub_eq_zero, eq_comm, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
⊢ r • (w₁ i - w₂ i) - w i = 0

Tactic:
hr'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
⊢ r • (w₁ i - w₂ i) - w i = 0

Tactic:
exact hr'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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)
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
⊢ ∃ (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⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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

Tactic:
⟨r, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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)
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
⊢ ∃ (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 ⟨r, ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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)
w' : (i : ι) → k := fun (i : ι) ↦ r * (w₁ i - w₂ i)
⊢ ∀ i ∈ s, w i = w' i

Tactic:
change ∀ i ∈ s, w i = w' i at hr
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
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)
⊢ 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:
rw [s.weightedVSub_congr hr fun _ _ => rfl, s.affineCombination_vsub, ←
      s.weightedVSub_const_smul]

Premises used: Finset.affineCombination_vsub, Finset.weightedVSub_const_smul, Finset.weightedVSub_congr, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (r • (w₁ - w₂)) : V)
    ((s.weightedVSub p : (a : ι → k) → V) w' : V)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
rw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, (w - w₁) i) 0
⊢ 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

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₁]

Premises used: Finset.affineCombination_vsub, direction_affineSpan, Finset.affineCombination, left_mem_affineSpan_pair, AffineSubspace.vadd_mem_iff_mem_direction, vsub_vadd, weightedVSub_mem_vectorSpan_pair, DFunLike.coe, Set.pair_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
⊢ (∃ (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:
simp only [Pi.sub_apply, sub_eq_iff_eq_add]

Premises used: sub_eq_iff_eq_add, Pi.sub_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, (w - w₁) i) 0

Tactic:
simp_all only [Pi.sub_apply, Finset.sum_sub_distrib, sub_self]

Premises used: sub_self, Finset.sum_sub_distrib, Pi.sub_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ha : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : 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
c : k
rw :
  (∀ i ∈ s, w i = (AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) c i) ↔
    ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i) : (a : k) → k) c
rw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, (AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) c i) 1
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) w : P)
      (((AffineMap.lineMap ((affineCombination k s p : (a : ι → k) → P) w₁)
                ((affineCombination k s p : (a : ι → k) → P) w₂) :
              k →ᵃ[k] P) :
            (a : k) → P)
          c :
        P) ↔
    ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i) : (a : k) → k) c

Tactic:
rw [← AffineMap.apply_lineMap, ha.affineCombination_eq_iff_eq hw]

Premises used: AffineIndependent.affineCombination_eq_iff_eq, AffineMap.apply_lineMap
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ha : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : 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
c : k
⊢ (∀ i ∈ s, w i = (AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) c i) ↔
    ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i) : (a : k) → k) c

Tactic:
simp [AffineMap.lineMap_apply]

Premises used: AffineMap.lineMap_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
ha : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : 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
c : k
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, (AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) c i) 1

Tactic:
simp [AffineMap.lineMap_apply, sum_add_distrib, ← mul_sum, hw₁, hw₂]

Premises used: Finset.mul_sum, Finset.sum_add_distrib, AffineMap.lineMap_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
inl :
  ∃ t ⊆ ∅,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k ∅) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))
inr :
  ∀ (p : P) (hp : p ∈ s),
    ∃ t ⊆ s,
      Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
        AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
          (Subtype.val (p := fun (x : P) ↦ x ∈ t))
⊢ ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
⊢ ∃ t ⊆ ∅,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k ∅) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))

Tactic:
⟨∅, Set.empty_subset ∅, rfl, affineIndependent_of_subsingleton k _⟩

Premises used: And.intro, Set.empty_subset, Exists.intro, affineIndependent_of_subsingleton, EmptyCollection.emptyCollection, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
⊢ ∃ t ⊆ ∅,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k ∅) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))

Tactic:
exact ⟨∅, Set.empty_subset ∅, rfl, affineIndependent_of_subsingleton k _⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
inr :
  ∀ (b : Set V) (hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s)
    (hb₂ :
      Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k ((⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s)))
    (hb₃ : LinearIndependent.{u_2, u_1, u_2} (ι := { x : V // x ∈ b }) k (Subtype.val (p := fun (x : V) ↦ x ∈ b))),
    ∃ t ⊆ s,
      Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
        AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
          (Subtype.val (p := fun (x : P) ↦ x ∈ t))
⊢ ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))

Tactic:
obtain ⟨b, hb₁, hb₂, hb₃⟩ := exists_linearIndependent k ((Equiv.vaddConst p).symm '' s)

Premises used: Equiv.vaddConst, exists_linearIndependent, Set.image, Equiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k ((⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s))
hb₃ : LinearIndependent.{u_2, u_1, u_2} (ι := { x : V // x ∈ b }) k (Subtype.val (p := fun (x : V) ↦ x ∈ b))
⊢ ∀ v ∈ b, v ≠ 0

Tactic:
have hb₀ : ∀ v : V, v ∈ b → v ≠ 0 := fun v hv => hb₃.ne_zero (⟨v, hv⟩ : b)
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k ((⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s))
hb₃ : LinearIndependent.{u_2, u_1, u_2} (ι := { x : V // x ∈ b }) k (Subtype.val (p := fun (x : V) ↦ x ∈ b))
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)

Tactic:
rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k hb₀ p] at hb₃

Premises used: linearIndependent_set_iff_affineIndependent_vadd_union_singleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k ((⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s))
hb₃ : LinearIndependent.{u_2, u_1, u_2} (ι := { x : V // x ∈ b }) k (Subtype.val (p := fun (x : V) ↦ x ∈ b))
hb₀ : ∀ v ∈ b, v ≠ 0
hb₄ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
⊢ ∀ v ∈ b, v ≠ 0

Tactic:
rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k hb₀ p] at hb₃

Premises used: linearIndependent_set_iff_affineIndependent_vadd_union_singleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k ((⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s))
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))

Tactic:
⟨{p} ∪ Equiv.vaddConst p '' b, ?_, ?_, hb₃⟩

Premises used: Equiv.vaddConst, And.intro, Exists.intro, Set.image, Union.union, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k ((⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s))
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
inr : {p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b ⊆ s
inr₁ : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) (affineSpan k s)
⊢ ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))

Tactic:
refine ⟨{p} ∪ Equiv.vaddConst p '' b, ?_, ?_, hb₃⟩