-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
q : P
v : V
rw :
  HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (v + (q -ᵥ (b : (a : ι) → P) i)) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₁ :
  1 -
      HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
        (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₂ :
  1 -
      HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
        (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
    HAdd.hAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₃ :
  1 -
      HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
        (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
    HAdd.hAdd (α := k) (-((b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₄ :
  HSub.hSub (β := k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
      (((b.basisOf i).sumCoords : (a : V) → k) v : k) =
    HAdd.hAdd (α := k) (-((b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₅ :
  HSub.hSub (β := k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
      (((b.basisOf i).sumCoords : (a : V) → k) v : k) =
    HAdd.hAdd (β := k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
      (-((b.basisOf i).sumCoords : (a : V) → k) v : k)
⊢ HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) ((v +ᵥ q) -ᵥ (b : (a : ι) → P) i) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
have rw₆ : HAdd.hAdd (β := k)
    (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
    (-((b.basisOf i).sumCoords : (a : V) → k) v : k) =
  HAdd.hAdd (β := k)
    (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
    (-((b.basisOf i).sumCoords : (a : V) → k) v : k)
Tactic: rw [vadd_vsub_assoc, map_add, vadd_eq_add, LinearMap.neg_apply, sub_add_eq_sub_sub_swap,
      add_comm, sub_eq_add_neg]