-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
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'
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : ExteriorAlgebra R M
h :
  ∀ (r : R) (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')
          ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
            CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
        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)
              ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
                CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
            N) :
        N')
h₁ :
  ∀ (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),
    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')
h₂ :
  ∀ (x : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) (m : M)
    (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'))
    (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')
          (HMul.hMul (α := CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
            ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
            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)
              (HMul.hMul (α := CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
                ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
                x) :
            N) :
        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')
        v :
      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)
            v :
          N) :
      N')

Tactic:
induction v using CliffordAlgebra.left_induction generalizing f with
  | algebraMap =>
    rw [liftAlternating_algebraMap, liftAlternating_algebraMap, map_smul,
      LinearMap.compAlternatingMap_apply]
  | add _ _ hx hy => rw [map_add, map_add, map_add, hx, hy]
  | ι_mul _ _ hx =>
    rw [liftAlternating_ι_mul, liftAlternating_ι_mul, ← hx]
    simp_rw [AlternatingMap.curryLeft_compAlternatingMap]

Premises used: LinearMap.compAlternatingMap_apply, ExteriorAlgebra.liftAlternating_ι_mul, Algebra.algebraMap, map_add, AlternatingMap.curryLeft_compAlternatingMap, ExteriorAlgebra.liftAlternating_algebraMap, map_smul