-- Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean
theorem fFold_fFold (m : M) (x : A × S f) : fFold f m (fFold f m x) = Q m • x

Proof state:
case mk.mk.snd.a.h.refine_1.intro.intro
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
b : A
m₃ : M
⊢ (f.bilin m₁) m * ((LinearMap.lcomp R A (f.bilin.flip m₃)) (LinearMap.mulRight R b)) m =
    Q m • ((LinearMap.lcomp R A (f.bilin.flip m₃)) (LinearMap.mulRight R b)) m₁

Tactic:
change f.bilin _ _ * (f.bilin _ _ * b) = Q m • (f.bilin _ _ * b)

Result:
case mk.mk.snd.a.h.refine_1.intro.intro
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
b : A
m₃ : M
⊢ (f.bilin m₁) m * ((f.bilin m) m₃ * b) = Q m • ((f.bilin m₁) m₃ * b)

Proof state:
case mk.mk
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
⊢ ((CliffordAlgebra.even.lift.fFold f) m) (((CliffordAlgebra.even.lift.fFold f) m) (a, ⟨g, hg⟩)) = Q m • (a, ⟨g, hg⟩)

Tactic:
ext : 2

Result:
case mk.mk.fst
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
⊢ (((CliffordAlgebra.even.lift.fFold f) m) (((CliffordAlgebra.even.lift.fFold f) m) (a, ⟨g, hg⟩))).1 =
    (Q m • (a, ⟨g, hg⟩)).1

case mk.mk.snd.a
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
⊢ ↑(((CliffordAlgebra.even.lift.fFold f) m) (((CliffordAlgebra.even.lift.fFold f) m) (a, ⟨g, hg⟩))).2 =
    ↑(Q m • (a, ⟨g, hg⟩)).2

Proof state:
case mk.mk.snd.a.h.refine_4
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.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 x hx _c ihx

Result:
case mk.mk.snd.a.h.refine_4
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
x : R
hx : M →ₗ[R] A
_c : hx ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
ihx : (f.bilin m₁) m * hx m = Q m • hx m₁
⊢ (f.bilin m₁) m * (x • hx) m = Q m • (x • hx) m₁

Proof state:
case mk.mk.snd.a.h.refine_2
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ (f.bilin m₁) m * 0 = Q m • 0

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.snd.a.h
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ (f.bilin m₁) m * g m = Q m • g m₁

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hg

Result:
case mk.mk.snd.a.h.refine_1
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.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₁

case mk.mk.snd.a.h.refine_2
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ (f.bilin m₁) m * 0 m = Q m • 0 m₁

case mk.mk.snd.a.h.refine_3
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.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 mk.mk.snd.a.h.refine_4
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.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₁

Proof state:
case mk.mk.snd.a.h
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ↑(((CliffordAlgebra.even.lift.fFold f) m) (((CliffordAlgebra.even.lift.fFold f) m) (a, ⟨g, hg⟩))).2 m₁ =
    ↑(Q m • (a, ⟨g, hg⟩)).2 m₁

Tactic:
change f.bilin _ _ * g m = Q m • g m₁

Result:
case mk.mk.snd.a.h
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type uA
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ (f.bilin m₁) m * g m = Q m • g m₁