-- 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.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, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mem.mk.add
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✝ : ℕ
x y : CliffordAlgebra Q
i : ℕ
hx : x ∈ LinearMap.range (ι Q) ^ i
hy : y ∈ LinearMap.range (ι Q) ^ i
ihx : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
ihy : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) y = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨y, ⋯⟩
⊢ ((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.mem.mk.add
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✝ : ℕ
x y : CliffordAlgebra Q
i : ℕ
hx : x ∈ LinearMap.range (ι Q) ^ i
hy : y ∈ LinearMap.range (ι Q) ^ i
ihx : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
ihy : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) y = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨y, ⋯⟩
⊢ (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) (⟨x, ⋯⟩ + ⟨y, ⋯⟩) = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨x + y, ⋯⟩

Proof state:
case mk.mem.mk.mem_mul.intro.refine_1
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
⊢ 1 + ↑i = ↑i.succ

Tactic:
rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]

Result:
no goals

Proof state:
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, ⋯⟩

Tactic:
rw [map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]

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
⊢ (DirectSum.of (fun i => ↥(evenOdd Q i)) (1 + ↑i)) (GradedMonoid.GMul.mul ⟨(ι Q) w✝, ⋯⟩ ⟨x, ⋯⟩) =
    (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i.succ) ⟨(ι Q) w✝ * x, ⋯⟩

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
⊢ ⟨0, ⋯⟩ = 0

Tactic:
rfl

Result:
no goals

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 : M), (GradedAlgebra.ι Q) m * (GradedAlgebra.ι Q) m = (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i))) (Q m)

Tactic:
apply GradedAlgebra.ι_sq_scalar Q

Result:
no goals

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')
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ↑x' = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') x'

Tactic:
obtain ⟨x', hx'⟩ := x'

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', hx'⟩ = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨x', hx'⟩

Proof state:
case mk.mem.mk.add
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✝ : ℕ
x y : CliffordAlgebra Q
i : ℕ
hx : x ∈ LinearMap.range (ι Q) ^ i
hy : y ∈ LinearMap.range (ι Q) ^ i
ihx : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
ihy : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) y = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨y, ⋯⟩
⊢ (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) (⟨x, ⋯⟩ + ⟨y, ⋯⟩) = (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i) ⟨x + y, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
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
⊢ (DirectSum.of (fun i => ↥(evenOdd Q i)) (1 + ↑i)) (GradedMonoid.GMul.mul ⟨(ι Q) w✝, ⋯⟩ ⟨x, ⋯⟩) =
    (DirectSum.of (fun i => ↥(evenOdd Q i)) ↑i.succ) ⟨(ι Q) w✝ * x, ⋯⟩

Tactic:
refine DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext ?_ ?_) <;>
  dsimp only [GradedMonoid.mk, Subtype.coe_mk]

Result:
case mk.mem.mk.mem_mul.intro.refine_1
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
⊢ 1 + ↑i = ↑i.succ

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