k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.119726
s : Set V
hs : ∀ (v : V), v ∈ s → v ≠ 0
p₁ : P
⊢ (LinearIndependent k fun v => ↑v) ↔ LinearIndependent k fun v => ↑v
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.119726
s : Set V
hs : ∀ (v : V), v ∈ s → v ≠ 0
p₁ : P
⊢ (LinearIndependent k fun v => ↑v) ↔ AffineIndependent k fun p => ↑p
rw [affineIndependent_set_iff_linearIndependent_vsub k
    (Set.mem_union_left _ (Set.mem_singleton p₁))]
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.119726
s : Set V
hs : ∀ (v : V), v ∈ s → v ≠ 0
p₁ : P
h : (fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}) = s
⊢ (LinearIndependent k fun v => ↑v) ↔ LinearIndependent k fun v => ↑v
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.119726
s : Set V
hs : ∀ (v : V), v ∈ s → v ≠ 0
p₁ : P
⊢ (LinearIndependent k fun v => ↑v) ↔ LinearIndependent k fun v => ↑v
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
no goals
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.119726
s : Set V
hs : ∀ (v : V), v ∈ s → v ≠ 0
p₁ : P
h : (fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}) = s
⊢ (LinearIndependent k fun v => ↑v) ↔ LinearIndependent k fun v => ↑v
rw [h]
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.119726
s : Set V
hs : ∀ (v : V), v ∈ s → v ≠ 0
p₁ : P
⊢ s \ {0} = s
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.119726
s : Set V
hs : ∀ (v : V), v ∈ s → v ≠ 0
p₁ : P
⊢ (fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}) = s
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']
no goals
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.119726
s : Set V
hs : ∀ (v : V), v ∈ s → v ≠ 0
p₁ : P
⊢ s \ {0} = s
exact Set.diff_singleton_eq_self fun h => hs 0 h rfl