-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem affineIndependent_set_iff_linearIndependent_vsub {s : Set P} {p₁ : P} (hp₁ : p₁ ∈ s) :
    AffineIndependent k (fun p => p : s → P) ↔
      LinearIndependent k (fun v => v : (fun p => (p -ᵥ p₁ : V)) '' (s \ {p₁}) → V)

Proof state:
case mpr
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 P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
f : { x // x ≠ ⟨p₁, hp₁⟩ } → ↑((fun p => p -ᵥ p₁) '' (s \ {p₁})) := fun x => ⟨↑↑x -ᵥ p₁, ⋯⟩
⊢ LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩

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

Result:
no goals

Proof state:
case mp
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 P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
⊢ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v

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)

Result:
case mp
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 P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
hv : ∀ (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))), ↑v +ᵥ p₁ ∈ s \ {p₁}
⊢ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v

Proof state:
case h.e'_4.h.h.e.h
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 P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
hv : ∀ (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))), ↑v +ᵥ p₁ ∈ s \ {p₁}
f : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁})) → { x // x ≠ ⟨p₁, hp₁⟩ } := fun x => ⟨⟨↑x +ᵥ p₁, ⋯⟩, ⋯⟩
x✝ : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))
v : { x // x ∈ (fun p => p -ᵥ p₁) '' (s \ {p₁}) }
⊢ ↑v = ((fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) ∘ f) v

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

Result:
no goals

Proof state:
case mpr
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 P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
⊢ LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩

Tactic:
let f : { x : s // x ≠ ⟨p₁, hp₁⟩ } → (fun p : P => (p -ᵥ p₁ : V)) '' (s \ {p₁}) := fun x =>
  ⟨((x : s) : P) -ᵥ p₁, ⟨x, ⟨⟨(x : s).property, fun hx => x.property (Subtype.ext hx)⟩, rfl⟩⟩⟩

Result:
case mpr
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 P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
f : { x // x ≠ ⟨p₁, hp₁⟩ } → ↑((fun p => p -ᵥ p₁) '' (s \ {p₁})) := fun x => ⟨↑↑x -ᵥ p₁, ⋯⟩
⊢ LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩

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 P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (AffineIndependent k fun p => ↑p) ↔ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v

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

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 P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) ↔
    LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v

Proof state:
case mp
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 P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
hv : ∀ (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))), ↑v +ᵥ p₁ ∈ s \ {p₁}
⊢ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v

Tactic:
let f : (fun p : P => (p -ᵥ p₁ : V)) '' (s \ {p₁}) → { x : s // x ≠ ⟨p₁, hp₁⟩ } := fun x =>
  ⟨⟨(x : V) +ᵥ p₁, Set.mem_of_mem_diff (hv x)⟩, fun hx =>
    Set.not_mem_of_mem_diff (hv x) (Subtype.ext_iff.1 hx)⟩

Result:
case mp
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 P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
hv : ∀ (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))), ↑v +ᵥ p₁ ∈ s \ {p₁}
f : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁})) → { x // x ≠ ⟨p₁, hp₁⟩ } := fun x => ⟨⟨↑x +ᵥ p₁, ⋯⟩, ⋯⟩
⊢ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v

Proof state:
case mpr
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 P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v) →
    LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩

Tactic:
intro h

Result:
case mpr
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 P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
⊢ LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩

Proof state:
case mp
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 P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
hv : ∀ (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))), ↑v +ᵥ p₁ ∈ s \ {p₁}
f : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁})) → { x // x ≠ ⟨p₁, hp₁⟩ } := fun x => ⟨⟨↑x +ᵥ p₁, ⋯⟩, ⋯⟩
⊢ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑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)))

Result:
case h.e'_4.h.h.e
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 P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
hv : ∀ (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))), ↑v +ᵥ p₁ ∈ s \ {p₁}
f : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁})) → { x // x ≠ ⟨p₁, hp₁⟩ } := fun x => ⟨⟨↑x +ᵥ p₁, ⋯⟩, ⋯⟩
x✝ : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))
⊢ Subtype.val = (fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) ∘ f

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 P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) ↔
    LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v

Tactic:
constructor

Result:
case mp
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 P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) →
    LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v

case mpr
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 P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v) →
    LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩