-- Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
theorem GradedAlgebra.lift_ι_eq (i' : ZMod 2) (x' : evenOdd Q i') :
    -- Porting note: added a second `by apply`
    lift Q ⟨by apply GradedAlgebra.ι Q, by apply GradedAlgebra.ι_sq_scalar Q⟩ x' =
      DirectSum.of (fun i => evenOdd Q i) i' x'

Proof state:
case mk.zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ 0 = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨0, ⋯⟩

Tactic:
apply Eq.symm

Result:
case mk.zero.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨0, ⋯⟩ = 0

Proof state:
case mk.mem.mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
hx : x ∈ LinearMap.range (ι Q) ^ ↑⟨i, ⋯⟩
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩

Tactic:
dsimp only [Subtype.coe_mk] at hx

Result:
case mk.mem.mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
hx : x ∈ LinearMap.range (ι Q) ^ i
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩

Proof state:
case mk.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' x y : CliffordAlgebra Q
hx : x ∈ ⨆ i, LinearMap.range (ι Q) ^ ↑i
hy : y ∈ ⨆ i, LinearMap.range (ι Q) ^ ↑i
ihx : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨x, hx⟩
ihy : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) y = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨y, hy⟩
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) (x + y) = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨x + y, ⋯⟩

Tactic:
rw [map_add, ihx, ihy, ← AddMonoidHom.map_add]

Result:
case mk.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' x y : CliffordAlgebra Q
hx : x ∈ ⨆ i, LinearMap.range (ι Q) ^ ↑i
hy : y ∈ ⨆ i, LinearMap.range (ι Q) ^ ↑i
ihx : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨x, hx⟩
ihy : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) y = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨y, hy⟩
⊢ (DirectSum.of (fun i => ↥(evenOdd Q i)) i') (⟨x, hx⟩ + ⟨y, hy⟩) =
    (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨x + y, ⋯⟩

Proof state:
case mk.zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) 0 = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨0, ⋯⟩

Tactic:
rw [map_zero]

Result:
case mk.zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ 0 = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨0, ⋯⟩

Proof state:
case mk.mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
i : { n // ↑n = i' }
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ ↑i
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨x, ⋯⟩

Tactic:
obtain ⟨i, rfl⟩ := i

Result:
case mk.mem.mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
hx : x ∈ LinearMap.range (ι Q) ^ ↑⟨i, ⋯⟩
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
hx' : x' ∈ evenOdd Q i'
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ↑⟨x', hx'⟩ = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨x', hx'⟩

Tactic:
dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
hx' : x' ∈ evenOdd Q i'
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x' = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨x', hx'⟩

Proof state:
case mk.mem.mk.mem_mul.intro.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ ↑(GradedMonoid.GMul.mul ⟨(ι Q) w✝, ⋯⟩ ⟨x, ⋯⟩) = (ι Q) w✝ * x

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mem.mk.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
r : R
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ((algebraMap R (CliffordAlgebra Q)) r) =
    (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑0) ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩

Tactic:
rw [AlgHom.commutes, DirectSum.algebraMap_apply]

Result:
case mk.mem.mk.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
r : R
⊢ (DirectSum.of (fun i => ↥(evenOdd Q i)) 0) (DirectSum.GAlgebra.toFun r) =
    (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑0) ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩

Proof state:
case mk.mem.mk.mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ : ℕ
m : CliffordAlgebra Q
hm : m ∈ LinearMap.range (ι Q)
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) (m * x) = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i.succ) ⟨m * x, ⋯⟩

Tactic:
obtain ⟨_, rfl⟩ := hm

Result:
case mk.mem.mk.mem_mul.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ((ι Q) w✝ * x) = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i.succ) ⟨(ι Q) w✝ * x, ⋯⟩

Proof state:
case mk.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' x y : CliffordAlgebra Q
hx : x ∈ ⨆ i, LinearMap.range (ι Q) ^ ↑i
hy : y ∈ ⨆ i, LinearMap.range (ι Q) ^ ↑i
ihx : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨x, hx⟩
ihy : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) y = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨y, hy⟩
⊢ (DirectSum.of (fun i => ↥(evenOdd Q i)) i') (⟨x, hx⟩ + ⟨y, hy⟩) =
    (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨x + y, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mk.zero.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨0, ⋯⟩ = 0

Tactic:
apply DFinsupp.single_eq_zero.mpr

Result:
case mk.zero.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ ⟨0, ⋯⟩ = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : ↥(evenOdd Q i')
⊢ M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)

Tactic:
apply GradedAlgebra.ι Q

Result:
no goals