awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
⊢ (ofProd Q₁ Q₂ : (a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (m₁, m₂)) =
    HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m₁ ᵍ⊗ₜ[R] 1 : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      (1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m₂ : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
have rw : (LinearMap.coprod
        (AlgHom.toLinearMap (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)) ∘ₗ
          (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) sorry)
        (AlgHom.toLinearMap (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)) ∘ₗ
          (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) sorry) :
      (a : M₁ × M₂) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
    (m₁, m₂) =
  HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
    ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m₁ ᵍ⊗ₜ[R] 1 : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
    (1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m₂ : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
Tactic: rw [ofProd, lift_ι_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ (toProd Q₁ Q₂).comp (ofProd Q₁ Q₂) = AlgHom.id R (CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
have a : ∀ (m : M₁),
  Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    (((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inl R M₁ M₂ :
          (a : M₁) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        m :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    (((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))) ∘ₗ
              ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        m :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
a :
  ∀ (m : M₁),
    Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
      (((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inl R M₁ M₂ :
            (a : M₁) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
          m :
        CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
      (((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))) ∘ₗ
                ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
          m :
        CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
⊢ (toProd Q₁ Q₂).comp (ofProd Q₁ Q₂) = AlgHom.id R (CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
have a₁ : ∀ (m : M₂),
  Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    (((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inr R M₁ M₂ :
          (a : M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        m :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    (((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))) ∘ₗ
              ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        m :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₁
⊢ Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    (((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inl R M₁ M₂ :
          (a : M₁) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        m :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    (((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))) ∘ₗ
              ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        m :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
have a : Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
  ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
      ((ofProd Q₁ Q₂ : (a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (m, 0))) :
    CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
  ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (m, 0) :
    CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₂
⊢ Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    (((((toProd Q₁ Q₂).comp (ofProd Q₁ Q₂)).toLinearMap ∘ₗ ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ LinearMap.inr R M₁ M₂ :
          (a : M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        m :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    (((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))) ∘ₗ
              ι (QuadraticMap.prod Q₁ Q₂)) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        m :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
have a : Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
  ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
      ((ofProd Q₁ Q₂ : (a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m))) :
    CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
  ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
    CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₂
⊢ Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        ((ofProd Q₁ Q₂ : (a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m))) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
have a : Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
  ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
      (HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) 0 ᵍ⊗ₜ[R] 1 : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        (1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) :
    CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
  ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
    CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
Tactic: rw [ofProd_ι_mk, map_add, toProd_one_tmul_ι, toProd_ι_tmul_one, Prod.mk_zero_zero,
      map_zero, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₂
a :
  Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        (HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) 0 ᵍ⊗ₜ[R] 1 : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          (1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
⊢ Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        ((ofProd Q₁ Q₂ : (a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m))) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
have a₁ : HAdd.hAdd (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂)) (β :=
    CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) 0 ᵍ⊗ₜ[R] 1) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        (1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂)) =
  (ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m)
Tactic: rw [ofProd_ι_mk, map_add, toProd_one_tmul_ι, toProd_ι_tmul_one, Prod.mk_zero_zero,
      map_zero, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₂
a :
  Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        (HAdd.hAdd (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) (β := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) 0 ᵍ⊗ₜ[R] 1 : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          (1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
a₁ :
  HAdd.hAdd (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂)) (β :=
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
      ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
          ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) 0 ᵍ⊗ₜ[R] 1) :
        CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
      ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
          (1 ᵍ⊗ₜ[R] (ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) m) :
        CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂)) =
    (ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m)
⊢ Eq (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        ((ofProd Q₁ Q₂ : (a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m))) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
have a₂ : HAdd.hAdd (α := CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂)) (β :=
    CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((toProd Q₁ Q₂ : (a : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
        ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) 0 ᵍ⊗ₜ[R] 1) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂))
    ((ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m) :
      CliffordAlgebra (R := R) (M := M₁ × M₂) (QuadraticMap.prod Q₁ Q₂)) =
  (ι (QuadraticMap.prod Q₁ Q₂) : (a : M₁ × M₂) → CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) (0, m)
Tactic: rw [ofProd_ι_mk, map_add, toProd_one_tmul_ι, toProd_ι_tmul_one, Prod.mk_zero_zero,
      map_zero, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ (ofProd Q₁ Q₂).comp (toProd Q₁ Q₂) = AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
have ha : ∀ (x : M₁),
  Eq (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
    (((((ofProd Q₁ Q₂).comp (toProd Q₁ Q₂)).comp
                (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
            ι Q₁ :
          (a : M₁) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        x :
      evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
    ((AlgHom.toLinearMap
              (AlgHom.comp (AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂))
                (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))) ∘ₗ
            ι Q₁ :
          (a : M₁) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        x :
      evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
ha :
  ∀ (x : M₁),
    Eq (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      (((((ofProd Q₁ Q₂).comp (toProd Q₁ Q₂)).comp
                  (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
              ι Q₁ :
            (a : M₁) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          x :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
      ((AlgHom.toLinearMap
                (AlgHom.comp (AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂))
                  (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))) ∘ₗ
              ι Q₁ :
            (a : M₁) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
          x :
        evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
⊢ (ofProd Q₁ Q₂).comp (toProd Q₁ Q₂) = AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
have hb : ∀ (x : M₂),
  Eq (α := evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
    (((((ofProd Q₁ Q₂).comp (toProd Q₁ Q₂)).comp
                (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
            ι Q₂ :
          (a : M₂) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        x :
      evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
    ((AlgHom.toLinearMap
              (AlgHom.comp (AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂))
                (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))) ∘ₗ
            ι Q₂ :
          (a : M₂) → evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
        x :
      evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx :
  Membership.mem (γ := Subgroup (CliffordAlgebra Q)ˣ)
    (Subgroup.closure (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) x
inst_3 : Invertible (α := R) 2
m : M
⊢ HSMul.hSMul (α := ConjAct (CliffordAlgebra Q)ˣ) (β := CliffordAlgebra Q)
      ((ConjAct.toConjAct : (a : (CliffordAlgebra Q)ˣ) → ConjAct (CliffordAlgebra Q)ˣ) x : ConjAct (CliffordAlgebra Q)ˣ)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) ∈
    (ι Q).range
have rw : HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
    (↑x⁻¹ : CliffordAlgebra Q) ∈
  (ι Q).range
Tactic: rw [ConjAct.units_smul_def, ConjAct.ofConjAct_toConjAct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x_1 : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
hx :
  Membership.mem (γ := Set (CliffordAlgebra Q)ˣ)
    (Units.val ⁻¹' Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q)) x
m : M
⊢ HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have mem : ∀ (a : M) (ha : (ι Q : (a : M) → CliffordAlgebra Q) a = (↑x : CliffordAlgebra Q)),
  HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
Tactic: obtain ⟨a, ha⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x_1 : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q : (a : M) → CliffordAlgebra Q) a = (↑x : CliffordAlgebra Q)
this_1 : Invertible (↑x : CliffordAlgebra Q) := x.invertible
this_2 : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) :=
  Eq.mpr ⋯ this_1
this : Invertible (α := R) ((Q : (a : M) → R) a : R) := invertibleOfInvertibleι Q a
⊢ HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have mem : HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
    @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑x : CliffordAlgebra Q) _ ∈
  (ι Q).range
Tactic: simp_rw [← invOf_units x, ← ha, ι_mul_ι_mul_invOf_ι, LinearMap.mem_range_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x_1 : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q : (a : M) → CliffordAlgebra Q) a = (↑x : CliffordAlgebra Q)
this_1 : Invertible (↑x : CliffordAlgebra Q) := x.invertible
this_2 : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) :=
  Eq.mpr ⋯ this_1
this : Invertible (α := R) ((Q : (a : M) → R) a : R) := invertibleOfInvertibleι Q a
mem :
  HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑x : CliffordAlgebra Q) _ ∈
    (ι Q).range
⊢ HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have mem₁ : HMul.hMul (β := CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
    (@Invertible.invOf _ MulOne.toMul MulOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) a) _ : CliffordAlgebra Q) ∈
  (ι Q).range
Tactic: simp_rw [← invOf_units x, ← ha, ι_mul_ι_mul_invOf_ι, LinearMap.mem_range_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x_1 : (CliffordAlgebra Q)ˣ
inst_3 : Invertible (α := R) 2
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q : (a : M) → CliffordAlgebra Q) a = (↑x : CliffordAlgebra Q)
this_1 : Invertible (↑x : CliffordAlgebra Q) := x.invertible
this_2 : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) :=
  Eq.mpr ⋯ this_1
this : Invertible (α := R) ((Q : (a : M) → R) a : R) := invertibleOfInvertibleι Q a
mem :
  HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑x : CliffordAlgebra Q) _ ∈
    (ι Q).range
mem₁ :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q))
      (@Invertible.invOf _ MulOne.toMul MulOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) a) _ : CliffordAlgebra Q) ∈
    (ι Q).range
⊢ HMul.hMul (β := CliffordAlgebra Q) (↑x : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) *
      (↑x⁻¹ : CliffordAlgebra Q) ∈
    (ι Q).range
have mem₂ : Membership.mem (α := CliffordAlgebra Q) (ι Q).range
  ((ι Q : (a : M) → CliffordAlgebra Q)
      (HMul.hMul (α := R) (β := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
            (QuadraticMap.polar (⇑Q : (a : M) → R) a m : R) •
          a -
        m) :
    CliffordAlgebra Q)
Tactic: simp_rw [← invOf_units x, ← ha, ι_mul_ι_mul_invOf_ι, LinearMap.mem_range_self]