-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
have have₁ have₂ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₃ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1), finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₄ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1) (hn : (Finset.image p s).Nonempty),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₅ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1) (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₆ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1) (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s) (hp₁' : p₁ ∈ p '' (↑s : Set ι)),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₇ :
  ∀ (hc' : #(Finset.image p s) = n + 1) (p₁ : P)
    (hi' :
      LinearIndependent k (M := V)
        fun (v : (↑(↑(Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V) : Type u_2)) ↦
        (↑v : V))
    (hp₁ : p₁ ∈ Finset.image p s) (hp₁' : p₁ ∈ p '' (↑s : Set ι)),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₈ :
  ∀ (hc' : #(Finset.image p s) = n + 1) (p₁ : P)
    (hi' :
      LinearIndependent k (M := V)
        fun (v : (↑(↑(Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V) : Type u_2)) ↦
        (↑v : V))
    (hp₁ : p₁ ∈ Finset.image p s) (hp₁' : p₁ ∈ p '' (↑s : Set ι))
    (hc : Finset.card.{u_2} (α := V) (Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n

Tactic:
classical
  have hi' := hi.range.mono (Set.image_subset_range p ↑s)
  have hc' : #(s.image p) = n + 1 := by rwa [s.card_image_of_injective hi.injective]
  have hn : (s.image p).Nonempty := by simp [hc', ← Finset.card_pos]
  rcases hn with ⟨p₁, hp₁⟩
  have hp₁' : p₁ ∈ p '' s := by simpa using hp₁
  rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁', ← Finset.coe_singleton,
    ← Finset.coe_image, ← Finset.coe_sdiff, Finset.sdiff_singleton_eq_erase, ← Finset.coe_image]
    at hi'
  have hc : #(((s.image p).erase p₁).image (· -ᵥ p₁)) = n := by
    rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
    exact Nat.pred_eq_of_eq_succ hc'
  rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, hc]

Premises used: finrank_span_finset_eq_card, Finset.sdiff_singleton_eq_erase, Finset.coe_singleton, Finset.coe_sdiff, Finset.coe_image