Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: case snd.refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
⊢ ∀ x ∈ {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)},
    (f.bilin m₁) m * x m = Q m • x m₁

pp: case snd.refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
⊢ (f.bilin m₁) m * 0 m = Q m • 0 m₁

pp: case snd.refine_3
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
⊢ ∀ (x y : M →ₗ[R] A),
    x ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)} →
      y ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)} →
        (f.bilin m₁) m * x m = Q m • x m₁ →
          (f.bilin m₁) m * y m = Q m • y m₁ → (f.bilin m₁) m * (x + y) m = Q m • (x + y) m₁

pp: case snd.refine_4
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
⊢ ∀ (a : R),
    ∀ x ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)},
      (f.bilin m₁) m * x m = Q m • x m₁ → (f.bilin m₁) m * (a • x) m = Q m • (a • x) m₁

Tactic:
· rintro _ ⟨b, m₃, rfl⟩
      change f.bilin _ _ * (f.bilin _ _ * b) = Q m • (f.bilin _ _ * b)
      rw [← smul_mul_assoc, ← mul_assoc, f.contract_mid]

Goal state after:
case snd.refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
⊢ (f.bilin m₁) m * 0 m = Q m • 0 m₁

case snd.refine_3
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
⊢ ∀ (x y : M →ₗ[R] A),
    x ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)} →
      y ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)} →
        (f.bilin m₁) m * x m = Q m • x m₁ →
          (f.bilin m₁) m * y m = Q m • y m₁ → (f.bilin m₁) m * (x + y) m = Q m • (x + y) m₁

case snd.refine_4
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
⊢ ∀ (a : R),
    ∀ x ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)},
      (f.bilin m₁) m * x m = Q m • x m₁ → (f.bilin m₁) m * (a • x) m = Q m • (a • x) m₁