-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
x y : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    Eq.{u_4 + 1} (α := N')
      (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
              g.compAlternatingMap (f i) :
            (a : ExteriorAlgebra R M) → N')
          x :
        N')
      ((g : (a : N) → N')
          ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                  ExteriorAlgebra R M →ₗ[R] N) :
                (a : ExteriorAlgebra R M) → N)
              x :
            N) :
        N')
hy :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    Eq.{u_4 + 1} (α := N')
      (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
              g.compAlternatingMap (f i) :
            (a : ExteriorAlgebra R M) → N')
          y :
        N')
      ((g : (a : N) → N')
          ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                  ExteriorAlgebra R M →ₗ[R] N) :
                (a : ExteriorAlgebra R M) → N)
              y :
            N) :
        N')
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
h :
  HAdd.hAdd (α := N') (β := N')
      (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
              g.compAlternatingMap (f i) :
            (a : ExteriorAlgebra R M) → N')
          x :
        N')
      (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
              g.compAlternatingMap (f i) :
            (a : ExteriorAlgebra R M) → N')
          y :
        N') =
    (g : (a : N) → N')
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          (x + y) :
        N)
h₁ :
  HAdd.hAdd (α := N') (β := N')
      (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
              g.compAlternatingMap (f i) :
            (a : ExteriorAlgebra R M) → N')
          x :
        N')
      (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
              g.compAlternatingMap (f i) :
            (a : ExteriorAlgebra R M) → N')
          y :
        N') =
    (g : (a : N) → N')
      (HAdd.hAdd (α := N) (β := N)
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            x :
          N)
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            y :
          N))
⊢ Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        (x + y) :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            (x + y) :
          N) :
      N')
have h₂ : HAdd.hAdd (α := N') (β := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        x :
      N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        y :
      N') =
  HAdd.hAdd (α := N') (β := N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            x :
          N) :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            y :
          N) :
      N')
Tactic: rw [map_add, map_add, map_add, hx, hy]