-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
i : ι
x : φv i
s₁ :
  Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
    ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
s₂ :
  (f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2)
s₃ :
  (g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
h₁ :
  ∀
    (s₁ :
      HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
          ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
          ((f : (a : (i : ι) → φv i) → P2) 0 : P2) =
        (g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x))
    (s₂ :
      (f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
        HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
          ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
          ((f : (a : (i : ι) → φv i) → P2) 0 : P2))
    (s₃ :
      (g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
        HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
          ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
          ((g : (a : (i : ι) → φv i) → P2) 0 : P2))
    (h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)),
    Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
      ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
⊢ Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
have h₃ : ∀
  (s₁ :
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
        ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
        ((f : (a : (i : ι) → φv i) → P2) 0 : P2) =
      HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
        ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
        ((g : (a : (i : ι) → φv i) → P2) 0 : P2))
  (s₂ :
    (f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
      HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
        ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
        ((f : (a : (i : ι) → φv i) → P2) 0 : P2))
  (s₃ :
    (g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
      HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
        ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
        ((g : (a : (i : ι) → φv i) → P2) 0 : P2))
  (h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)),
  Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
Tactic: rwa [s₂, s₃, h₂, vadd_right_cancel_iff] at s₁
Cleared hypotheses: s₁, s₂, s₃, h₂