-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
H :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A)
      ((f : (a : ↥(even Q)) → A)
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) ⋯ :
            ↥(even Q)) :
        A)
      ((g : (a : ↥(even Q)) → A)
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) ⋯ :
            ↥(even Q)) :
        A)
H₁ :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) (hy : y ∈ evenOdd Q 0)
    (ihx :
      Eq.{u_3 + 1} (α := A)
        ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
        ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A))
    (ihy :
      Eq.{u_3 + 1} (α := A)
        ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy) : A)
        ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) y hy) : A)),
    Eq.{u_3 + 1} (α := A)
      ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) (x + y) ⋯) : A)
      ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) (x + y) ⋯) : A)
H₂ :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0)
    (ih :
      Eq.{u_3 + 1} (α := A)
        ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
        ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)),
    Eq.{u_3 + 1} (α := A)
      ((f : (a : ↥(even Q)) → A)
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
                ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
                ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
              x)
            ⋯) :
        A)
      ((g : (a : ↥(even Q)) → A)
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q)
            (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
                ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
                ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
              x)
            ⋯) :
        A)
⊢ Eq.{u_3 + 1} (α := A)
    ((f : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)
    ((g : (a : ↥(even Q)) → A) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ even Q) x hx) : A)

Tactic:
induction x, hx using even_induction with
  | algebraMap r =>
    exact (f.commutes r).trans (g.commutes r).symm
  | add x y hx hy ihx ihy =>
    have := congr_arg₂ (· + ·) ihx ihy
    exact (map_add f _ _).trans (this.trans <| (map_add g _ _).symm)
  | ι_mul_ι_mul m₁ m₂ x hx ih =>
    have := congr_arg₂ (· * ·) (LinearMap.congr_fun (LinearMap.congr_fun h m₁) m₂) ih
    exact (map_mul f _ _).trans (this.trans <| (map_mul g _ _).symm)

Premises used: Algebra.algebraMap