-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem forall_mul_self_eq_iff {A : Type*} [Ring A] [Algebra R A] (h2 : IsUnit (2 : A))
    (f : M →ₗ[R] A) :
    (∀ x, f x * f x = algebraMap _ _ (Q x)) ↔
      (LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f =
        Q.polarBilin.compr₂ (Algebra.linearMap R A)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
x : M
h : ∀ (x y : M), f x * f y + f y * f x = (algebraMap R A) (QuadraticMap.polar (⇑Q) x y)
⊢ f x * f x = (algebraMap R A) (Q x)

Tactic:
apply h2.mul_left_cancel

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
x : M
h : ∀ (x y : M), f x * f y + f y * f x = (algebraMap R A) (QuadraticMap.polar (⇑Q) x y)
⊢ 2 * (f x * f x) = 2 * (algebraMap R A) (Q x)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
h :
  ∀ (x x_1 : M),
    (((LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f) x) x_1 =
      ((LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)) x) x_1
x : M
⊢ f x * f x = (algebraMap R A) (Q x)

Tactic:
change ∀ x y : M, f x * f y + f y * f x = algebraMap R A (QuadraticMap.polar Q x y) at h

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
x : M
h : ∀ (x y : M), f x * f y + f y * f x = (algebraMap R A) (QuadraticMap.polar (⇑Q) x y)
⊢ f x * f x = (algebraMap R A) (Q x)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
⊢ (∀ (x : M), f x * f x = (algebraMap R A) (Q x)) ↔
    ∀ (x x_1 : M),
      (((LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f) x) x_1 =
        ((LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)) x) x_1

Tactic:
refine ⟨mul_add_swap_eq_polar_of_forall_mul_self_eq _, fun h x => ?_⟩

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
h :
  ∀ (x x_1 : M),
    (((LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f) x) x_1 =
      ((LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)) x) x_1
x : M
⊢ f x * f x = (algebraMap R A) (Q x)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
⊢ (∀ (x : M), f x * f x = (algebraMap R A) (Q x)) ↔
    (LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f =
      LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)

Tactic:
simp_rw [DFunLike.ext_iff]

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
⊢ (∀ (x : M), f x * f x = (algebraMap R A) (Q x)) ↔
    ∀ (x x_1 : M),
      (((LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f) x) x_1 =
        ((LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)) x) x_1

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
x : M
h : ∀ (x y : M), f x * f y + f y * f x = (algebraMap R A) (QuadraticMap.polar (⇑Q) x y)
⊢ 2 * (f x * f x) = 2 * (algebraMap R A) (Q x)

Tactic:
rw [two_mul, two_mul, h x x, QuadraticMap.polar_self, two_smul, map_add]

Result:
no goals