-- 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:
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
this : (f.bilin m₁) m * 0 = Q m • 0
⊢ (f.bilin m₁) m * 0 m = Q m • 0 m₁

Tactic:
simp

Result:
no goals

Proof state:
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
x : A × ↥(CliffordAlgebra.even.lift.S f)
⊢ ((CliffordAlgebra.even.lift.fFold f) m) (((CliffordAlgebra.even.lift.fFold f) m) x) = Q m • x

Tactic:
obtain ⟨a, ⟨g, hg⟩⟩ := x

Result:
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⟩)

Proof state:
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

Tactic:
ext 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
⊢ ↑(((CliffordAlgebra.even.lift.fFold f) m) (((CliffordAlgebra.even.lift.fFold f) m) (a, ⟨g, hg⟩))).2 m₁ =
    ↑(Q m • (a, ⟨g, hg⟩)).2 m₁

Proof state:
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

Tactic:
change f.bilin m m * a = Q m • a

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
⊢ (f.bilin m) m * a = Q m • a

Proof state:
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
⊢ (f.bilin m) m * a = Q m • a

Tactic:
rw [Algebra.smul_def, f.contract]

Result:
no goals

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
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₁

Tactic:
rw [LinearMap.smul_apply, LinearMap.smul_apply, mul_smul_comm, ihx, smul_comm]

Result:
no goals

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 m = Q m • 0 m₁

Tactic:
suffices f.bilin m₁ m * 0 = Q m • (0 : A) by simp

Result:
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

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 * ((f.bilin m) m₃ * b) = Q m • ((f.bilin m₁) m₃ * b)

Tactic:
rw [← smul_mul_assoc, ← mul_assoc, f.contract_mid]

Result:
no goals

Proof state:
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
_hx : x ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
_hy : y ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
ihx : (f.bilin m₁) m * x m = Q m • x m₁
ihy : (f.bilin m₁) m * y m = Q m • y m₁
⊢ (f.bilin m₁) m * (x + y) m = Q m • (x + y) m₁

Tactic:
rw [LinearMap.add_apply, LinearMap.add_apply, mul_add, smul_add, ihx, ihy]

Result:
no goals

Proof state:
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₁

Tactic:
rintro _ ⟨b, m₃, rfl⟩

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 * ((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₁

Proof state:
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₁

Tactic:
rintro x y _hx _hy ihx ihy

Result:
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
_hx : x ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
_hy : y ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
ihx : (f.bilin m₁) m * x m = Q m • x m₁
ihy : (f.bilin m₁) m * y m = Q m • y m₁
⊢ (f.bilin m₁) m * (x + y) m = Q m • (x + y) m₁