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
i1 : ι
h :
  ∀ (s : Finset { x : ι // x ≠ i1 }) (g : { x : ι // x ≠ i1 } → k),
    Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) (∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1)) 0
i : ι
hi : i ∈ s
f : ι → V := fun (i : ι) ↦ w i • (p i -ᵥ p i1)
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1), f (↑i : ι)) 0

Tactic:
have hs2 : (∑ i ∈ (s.erase i1).subtype fun i => i ≠ i1, f i) = 0 := by
        rw [← hs]
        convert! Finset.sum_subtype_of_mem f fun x => Finset.ne_of_mem_erase
-- 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
i1 : ι
h :
  ∀ (s : Finset { x : ι // x ≠ i1 }) (g : { x : ι // x ≠ i1 } → k),
    Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) (∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1)) 0
i : ι
hi : i ∈ s
f : ι → V := fun (i : ι) ↦ w i • (p i -ᵥ p i1)
hs2 : Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1), f (↑i : ι)) 0
⊢ ∀ (i : { x : ι // x ≠ i1 }),
    Membership.mem (γ := Finset { x : ι // x ≠ i1 }) (Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1)) i →
      Eq.{u_1 + 1} (α := k) ((fun (x : { x : ι // x ≠ i1 }) ↦ w (↑x : ι)) i) 0

Tactic:
have h2 := h ((s.erase i1).subtype fun i => i ≠ i1) (fun x => w x) hs2
-- 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
i1 : ι
h :
  ∀ (s : Finset { x : ι // x ≠ i1 }) (g : { x : ι // x ≠ i1 } → k),
    Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) (∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1)) 0
i : ι
hi : i ∈ s
f : ι → V := fun (i : ι) ↦ w i • (p i -ᵥ p i1)
hs2 : Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1), f (↑i : ι)) 0
h2 :
  ∀ (i : { x : ι // x ≠ i1 }),
    Membership.mem (γ := Finset { x : ι // x ≠ i1 }) (Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1)) i →
      Eq.{u_1 + 1} (α := k) ((fun (x : { x : ι // x ≠ i1 }) ↦ w (↑x : ι)) i) 0
⊢ ∀ (i : { x : ι // x ≠ i1 }), (↑i : ι) ∈ s.erase i1 → w (↑i : ι) = 0

Tactic:
simp_rw [Finset.mem_subtype] at h2

Premises used: Finset.mem_subtype
-- 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
i1 : ι
h :
  ∀ (s : Finset { x : ι // x ≠ i1 }) (g : { x : ι // x ≠ i1 } → k),
    Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) (∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1)) 0
i : ι
hi : i ∈ s
f : ι → V := fun (i : ι) ↦ w i • (p i -ᵥ p i1)
hs2 : Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1), f (↑i : ι)) 0
h2 : ∀ (i : { x : ι // x ≠ i1 }), (↑i : ι) ∈ s.erase i1 → w (↑i : ι) = 0
⊢ ∀ i ∈ s, i ≠ i1 → w i = 0

Tactic:
have h2b : ∀ i ∈ s, i ≠ i1 → w i = 0 := fun i his hi =>
        h2 ⟨i, hi⟩ (Finset.mem_erase_of_ne_of_mem hi his)
-- 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
i1 : ι
h :
  ∀ (s : Finset { x : ι // x ≠ i1 }) (g : { x : ι // x ≠ i1 } → k),
    Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) (∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1)) 0
i : ι
hi : i ∈ s
f : ι → V := fun (i : ι) ↦ w i • (p i -ᵥ p i1)
hs2 : Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1), f (↑i : ι)) 0
h2 : ∀ (i : { x : ι // x ≠ i1 }), (↑i : ι) ∈ s.erase i1 → w (↑i : ι) = 0
h2b : ∀ i ∈ s, i ≠ i1 → w i = 0
⊢ w i = 0

Tactic:
Finset.eq_zero_of_sum_eq_zero hw h2b i hi

Premises used: Finset.eq_zero_of_sum_eq_zero
-- 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
i1 : ι
h :
  ∀ (s : Finset { x : ι // x ≠ i1 }) (g : { x : ι // x ≠ i1 } → k),
    Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) (∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1)) 0
i : ι
hi : i ∈ s
f : ι → V := fun (i : ι) ↦ w i • (p i -ᵥ p i1)
hs2 : Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1), f (↑i : ι)) 0
h2 : ∀ (i : { x : ι // x ≠ i1 }), (↑i : ι) ∈ s.erase i1 → w (↑i : ι) = 0
h2b : ∀ i ∈ s, i ≠ i1 → w i = 0
⊢ w i = 0

Tactic:
exact Finset.eq_zero_of_sum_eq_zero hw h2b i hi

Premises used: Finset.eq_zero_of_sum_eq_zero
-- 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
i1 : ι
mp :
  AffineIndependent k p →
    LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1
mpr mpr₁ :
  (LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1) →
    AffineIndependent k p
⊢ AffineIndependent k p ↔
    LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1

Tactic:
classical
    constructor
    · intro h
      rw [linearIndependent_iff']
      intro s g hg i hi
      set f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩ with hfdef
      let s2 : Finset ι := insert i1 (s.map (Embedding.subtype _))
      have hfg : ∀ x : { x // x ≠ i1 }, g x = f x := by grind
      rw [hfg]
      have hf : ∑ ι ∈ s2, f ι = 0 := by
        rw [Finset.sum_insert
            (Finset.notMem_map_subtype_of_not_property s (Classical.not_not.2 rfl)),
          Finset.sum_subtype_map_embedding fun x _ => (hfg x).symm]
        rw [hfdef]
        dsimp only
        rw [dif_pos rfl]
        exact neg_add_cancel _
      have hs2 : s2.weightedVSub p f = (0 : V) := by
        set f2 : ι → V := fun x => f x • (p x -ᵥ p i1) with hf2def
        set g2 : { x // x ≠ i1 } → V := fun x => g x • (p x -ᵥ p i1)
        have hf2g2 : ∀ x : { x // x ≠ i1 }, f2 x = g2 x := by
          simp only [g2, hf2def]
          refine fun x => ?_
          rw [hfg]
        rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s2 f p hf (p i1),
          Finset.weightedVSubOfPoint_insert, Finset.weightedVSubOfPoint_apply,
          Finset.sum_subtype_map_embedding fun x _ => hf2g2 x]
        exact hg
      exact h s2 f hf hs2 i (Finset.mem_insert_of_mem (Finset.mem_map.2 ⟨i, hi, rfl⟩))
    · intro h
      rw [linearIndependent_iff'] at h
      intro s w hw hs i hi
      rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p hw (p i1), ←
        s.weightedVSubOfPoint_erase w p i1, Finset.weightedVSubOfPoint_apply] at hs
      let f : ι → V := fun i => w i • (p i -ᵥ p i1)
      have hs2 : (∑ i ∈ (s.erase i1).subtype fun i => i ≠ i1, f i) = 0 := by
        rw [← hs]
        convert! Finset.sum_subtype_of_mem f fun x => Finset.ne_of_mem_erase
      have h2 := h ((s.erase i1).subtype fun i => i ≠ i1) (fun x => w x) hs2
      simp_rw [Finset.mem_subtype] at h2
      have h2b : ∀ i ∈ s, i ≠ i1 → w i = 0 := fun i his hi =>
        h2 ⟨i, hi⟩ (Finset.mem_erase_of_ne_of_mem hi his)
      exact Finset.eq_zero_of_sum_eq_zero hw h2b i hi

Premises used: Finset.weightedVSubOfPoint_apply, linearIndependent_iff', Finset.mem_subtype
-- 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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
rw :
  (LinearIndependent.{u_3, u_1, u_2} k (M := V)
      fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
      (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)) ↔
    LinearIndependent k (M := V) fun (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦ (↑v : V)
⊢ (AffineIndependent k (P := P) fun (p : (↑s : Type u_3)) ↦ (↑p : P)) ↔
    LinearIndependent k (M := V) fun (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦ (↑v : V)

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub k (fun p => p : s → P) ⟨p₁, hp₁⟩]

Premises used: Subtype.mk, affineIndependent_iff_linearIndependent_vsub, Subtype.val
-- 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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
mp :
  (LinearIndependent.{u_3, u_1, u_2} k (M := V)
      fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
      (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)) →
    LinearIndependent k (M := V) fun (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦ (↑v : V)
mpr :
  (LinearIndependent k (M := V) fun (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦ (↑v : V)) →
    LinearIndependent.{u_3, u_1, u_2} k (M := V)
      fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
      (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)
⊢ (LinearIndependent.{u_3, u_1, u_2} k (M := V)
      fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
      (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)) ↔
    LinearIndependent k (M := V) fun (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦ (↑v : V)

Tactic:
constructor
-- 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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h :
  LinearIndependent.{u_3, u_1, u_2} k (M := V)
    fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
    (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)
⊢ ∀ (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)), (↑v : V) +ᵥ p₁ ∈ s \ {p₁}

Tactic:
have hv : ∀ v : (fun p => (p -ᵥ p₁ : V)) '' (s \ {p₁}), (v : V) +ᵥ p₁ ∈ s \ {p₁} := fun v =>
      (vsub_left_injective p₁).mem_set_image.1 ((vadd_vsub (v : V) p₁).symm ▸ v.property)
-- 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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h :
  LinearIndependent.{u_3, u_1, u_2} k (M := V)
    fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
    (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)
hv : ∀ (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)), (↑v : V) +ᵥ p₁ ∈ s \ {p₁}
f : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2) →
  { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ } :=
  fun (x : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦
    Subtype.mk (p := fun (x : (↑s : Type u_3)) ↦ x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ s) ((↑x : V) +ᵥ p₁) ⋯) ⋯
⊢ LinearIndependent k (M := V)
    ((fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
        (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)) ∘
      f)

Tactic:
h.comp f fun x1 x2 hx =>
        Subtype.ext (vadd_right_cancel p₁ (Subtype.ext_iff.1 (Subtype.ext_iff.1 hx)))

Premises used: Subtype.ext_iff, vadd_right_cancel, Iff.mp, LinearIndependent.comp, Subtype.ext
-- 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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h :
  LinearIndependent.{u_3, u_1, u_2} k (M := V)
    fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
    (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)
hv : ∀ (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)), (↑v : V) +ᵥ p₁ ∈ s \ {p₁}
f : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2) →
  { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ } :=
  fun (x : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦
    Subtype.mk (p := fun (x : (↑s : Type u_3)) ↦ x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ s) ((↑x : V) +ᵥ p₁) ⋯) ⋯
h₁ :
  ∀ (x : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)),
    Subtype.val (p := fun (x : V) ↦ Membership.mem (γ := Set V) ((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) x) =
      (fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
          (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)) ∘
        f
⊢ LinearIndependent k (M := V) fun (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦ (↑v : V)

Tactic:
convert!
      h.comp f fun x1 x2 hx =>
        Subtype.ext (vadd_right_cancel p₁ (Subtype.ext_iff.1 (Subtype.ext_iff.1 hx)))

Premises used: Subtype.ext_iff, vadd_right_cancel, Iff.mp, LinearIndependent.comp, Subtype.ext
-- 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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h :
  LinearIndependent.{u_3, u_1, u_2} k (M := V)
    fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
    (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)
hv : ∀ (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)), (↑v : V) +ᵥ p₁ ∈ s \ {p₁}
f : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2) →
  { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ } :=
  fun (x : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦
    Subtype.mk (p := fun (x : (↑s : Type u_3)) ↦ x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ s) ((↑x : V) +ᵥ p₁) ⋯) ⋯
x : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)
h₁ :
  ∀ (v : { x : V // Membership.mem (γ := Set V) ((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) x }),
    (↑v : V) =
      ((fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
            (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)) ∘
          f)
        v
⊢ Subtype.val (p := fun (x : V) ↦ Membership.mem (γ := Set V) ((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) x) =
    (fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
        (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)) ∘
      f

Tactic:
ext v
-- 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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h :
  LinearIndependent.{u_3, u_1, u_2} k (M := V)
    fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
    (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)
hv : ∀ (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)), (↑v : V) +ᵥ p₁ ∈ s \ {p₁}
f : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2) →
  { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ } :=
  fun (x : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦
    Subtype.mk (p := fun (x : (↑s : Type u_3)) ↦ x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ s) ((↑x : V) +ᵥ p₁) ⋯) ⋯
x : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)
v : { x : V // Membership.mem (γ := Set V) ((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) x }
⊢ (↑v : V) =
    ((fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
          (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)) ∘
        f)
      v

Tactic:
(vadd_vsub (v : V) p₁).symm

Premises used: vadd_vsub, Eq.symm, Subtype.val
-- 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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h :
  LinearIndependent.{u_3, u_1, u_2} k (M := V)
    fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
    (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)
hv : ∀ (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)), (↑v : V) +ᵥ p₁ ∈ s \ {p₁}
f : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2) →
  { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ } :=
  fun (x : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦
    Subtype.mk (p := fun (x : (↑s : Type u_3)) ↦ x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ s) ((↑x : V) +ᵥ p₁) ⋯) ⋯
x : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)
v : { x : V // Membership.mem (γ := Set V) ((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) x }
⊢ (↑v : V) =
    ((fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
          (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)) ∘
        f)
      v

Tactic:
exact (vadd_vsub (v : V) p₁).symm

Premises used: vadd_vsub, Eq.symm, Subtype.val
-- 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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k (M := V) fun (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦ (↑v : V)
f : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ } →
  (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2) :=
  fun (x : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
    Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) ((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) x)
      ((↑(↑x : (↑s : Type u_3)) : P) -ᵥ p₁) ⋯
⊢ LinearIndependent k (M := V) ((fun (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦ (↑v : V)) ∘ f)

Tactic:
h.comp f fun x1 x2 hx => Subtype.ext (Subtype.ext (vsub_left_cancel (Subtype.ext_iff.1 hx)))

Premises used: Subtype.ext_iff, Iff.mp, LinearIndependent.comp, vsub_left_cancel, Subtype.ext
-- 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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k (M := V) fun (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2)) ↦ (↑v : V)
f : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ } →
  (↑((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) : Type u_2) :=
  fun (x : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
    Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) ((fun (p : P) ↦ p -ᵥ p₁) '' (s \ {p₁})) x)
      ((↑(↑x : (↑s : Type u_3)) : P) -ᵥ p₁) ⋯
⊢ LinearIndependent.{u_3, u_1, u_2} k (M := V)
    fun (i : { x : (↑s : Type u_3) // x ≠ Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁ }) ↦
    (↑(↑i : (↑s : Type u_3)) : P) -ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p₁ hp₁) : P)

Tactic:
convert!
      h.comp f fun x1 x2 hx => Subtype.ext (Subtype.ext (vsub_left_cancel (Subtype.ext_iff.1 hx)))

Premises used: Subtype.ext_iff, Iff.mp, LinearIndependent.comp, vsub_left_cancel, Subtype.ext
-- 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
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
rw :
  (LinearIndependent k (M := V) fun (v : (↑s : Type u_2)) ↦ (↑v : V)) ↔
    LinearIndependent k (M := V)
      fun (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun (v : V) ↦ v +ᵥ p₁) '' s) \ {p₁})) : Type u_2)) ↦ (↑v : V)
⊢ (LinearIndependent k (M := V) fun (v : (↑s : Type u_2)) ↦ (↑v : V)) ↔
    AffineIndependent k (P := P) fun (p : (↑({p₁} ∪ (fun (v : V) ↦ v +ᵥ p₁) '' s) : Type u_3)) ↦ (↑p : P)

Tactic:
rw [affineIndependent_set_iff_linearIndependent_vsub k
      (Set.mem_union_left _ (Set.mem_singleton p₁))]

Premises used: Set.mem_singleton, affineIndependent_set_iff_linearIndependent_vsub, Set.mem_union_left
-- 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
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
simp_rw : s \ {0} = s
⊢ (fun (p : P) ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun (v : V) ↦ v +ᵥ p₁) '' s) \ {p₁}) = s

Tactic:
simp_rw [Set.union_diff_left, Set.image_diff (vsub_left_injective p₁), Set.image_image,
      Set.image_singleton, vsub_self, vadd_vsub, Set.image_id']

Premises used: Set.image_image, Set.union_diff_left, Set.image_singleton, Set.image_id', Set.image_diff, vsub_left_injective, vadd_vsub, vsub_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
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ s \ {0} = s

Tactic:
Set.diff_singleton_eq_self fun h => hs 0 h rfl

Premises used: Set.diff_singleton_eq_self, OfNat.ofNat, 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
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ s \ {0} = s

Tactic:
exact Set.diff_singleton_eq_self fun h => hs 0 h rfl

Premises used: Set.diff_singleton_eq_self, OfNat.ofNat, 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
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ (fun (p : P) ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun (v : V) ↦ v +ᵥ p₁) '' s) \ {p₁}) = s

Tactic:
have h : (fun p => (p -ᵥ p₁ : V)) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}) = s := by
    simp_rw [Set.union_diff_left, Set.image_diff (vsub_left_injective p₁), Set.image_image,
      Set.image_singleton, vsub_self, vadd_vsub, Set.image_id']
    exact Set.diff_singleton_eq_self fun h => hs 0 h 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
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
h : (fun (p : P) ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun (v : V) ↦ v +ᵥ p₁) '' s) \ {p₁}) = s
rw rw₁ :
  (LinearIndependent k (M := V) fun (v : (↑s : Type u_2)) ↦ (↑v : V)) ↔
    LinearIndependent k (M := V) fun (v : (↑s : Type u_2)) ↦ (↑v : V)
⊢ (LinearIndependent k (M := V) fun (v : (↑s : Type u_2)) ↦ (↑v : V)) ↔
    LinearIndependent k (M := V)
      fun (v : (↑((fun (p : P) ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun (v : V) ↦ v +ᵥ p₁) '' s) \ {p₁})) : Type u_2)) ↦ (↑v : V)

Tactic:
rw [h]