-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem linearIndependent_set_iff_affineIndependent_vadd_union_singleton {s : Set V}
    (hs : ∀ v ∈ s, v ≠ (0 : V)) (p₁ : P) : LinearIndependent k (fun v => v : s → V) ↔
    AffineIndependent k (fun p => p : ({p₁} ∪ (fun v => v +ᵥ p₁) '' s : Set P) → P)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
h : (fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}) = s
⊢ (LinearIndependent k fun (v : ↑s) => ↑v) ↔
    LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}))) => ↑v

Tactic:
rw [h]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ (LinearIndependent k fun (v : ↑s) => ↑v) ↔
    LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}))) => ↑v

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

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
h : (fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}) = s
⊢ (LinearIndependent k fun (v : ↑s) => ↑v) ↔
    LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}))) => ↑v

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : 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

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ (LinearIndependent k fun (v : ↑s) => ↑v) ↔ AffineIndependent k fun p => ↑p

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

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ (LinearIndependent k fun (v : ↑s) => ↑v) ↔
    LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}))) => ↑v

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ (fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun 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']

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ s \ {0} = s