awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₁ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₂ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q) =
    1
have rw₃ : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
  1
Tactic: rw [map_smul, mul_smul_comm, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₁ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₂ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₃ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _) :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q) =
    1
have rw₄ : Eq (α := CliffordAlgebra Q)
  ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
      (HMul.hMul (α := R) (β := R)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((Q : (a : M) → R) m : R)) :
    CliffordAlgebra Q)
  (1 : CliffordAlgebra Q)
Tactic: rw [map_smul, mul_smul_comm, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₁ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₂ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₃ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _) :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₄ :
  Eq (α := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
        (HMul.hMul (α := R) (β := R)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
          ((Q : (a : M) → R) m : R)) :
      CliffordAlgebra Q)
    (1 : CliffordAlgebra Q)
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q) =
    1
have rw₅ : Eq (α := CliffordAlgebra Q) ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) 1
Tactic: rw [map_smul, mul_smul_comm, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
inst_3 : Invertible (α := R) ((Q : (a : M) → R) m : R)
rw :
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₁ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)) =
    1
rw₂ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₃ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _) :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m) : CliffordAlgebra Q) =
    1
rw₄ :
  Eq (α := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q)
        (HMul.hMul (α := R) (β := R)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R)
          ((Q : (a : M) → R) m : R)) :
      CliffordAlgebra Q)
    (1 : CliffordAlgebra Q)
rw₅ : Eq (α := CliffordAlgebra Q) ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 1) 1
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) m) _ : R) m) :
        CliffordAlgebra Q) =
    1
have rw₆ : Eq (α := CliffordAlgebra Q) 1 1
Tactic: rw [map_smul, mul_smul_comm, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
h : IsUnit.{u_1} (M := R) ((Q : (a : M) → R) m : R)
⊢ IsUnit (M := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
have intro : ∀ (val : Invertible (α := R) ((Q : (a : M) → R) m : R)),
  IsUnit (M := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
Tactic: cases h.nonempty_invertible
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
a b : M
inst_3 : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
inst_4 : Invertible (α := R) ((Q : (a : M) → R) a : R)
⊢ HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) a) _ :
        CliffordAlgebra Q) =
    (ι 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 b : R) •
          a -
        b)
have rw : HMul.hMul (β := CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
    ((ι Q : (a : M) → CliffordAlgebra Q)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R) a) :
      CliffordAlgebra Q) =
  (ι 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 b : R) •
        a -
      b)
Tactic: rw [invOf_ι, map_smul, mul_smul_comm, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul,
    invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
a b : M
inst_3 : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
inst_4 : Invertible (α := R) ((Q : (a : M) → R) a : R)
rw :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R) a) :
        CliffordAlgebra Q) =
    (ι 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 b : R) •
          a -
        b)
⊢ HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) a) _ :
        CliffordAlgebra Q) =
    (ι 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 b : R) •
          a -
        b)
have rw₁ : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
    HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
  (ι 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 b : R) •
        a -
      b)
Tactic: rw [invOf_ι, map_smul, mul_smul_comm, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul,
    invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
a b : M
inst_3 : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
inst_4 : Invertible (α := R) ((Q : (a : M) → R) a : R)
⊢ HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) a) _ :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
    (ι 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 b : R) •
          a -
        b)
have rw : HMul.hMul (β := CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R) a) :
        CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
    ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
  (ι 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 b : R) •
        a -
      b)
Tactic: rw [invOf_ι, map_smul, smul_mul_assoc, smul_mul_assoc, ι_mul_ι_mul_ι, ← map_smul, smul_sub,
    smul_smul, smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
a b : M
inst_3 : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
inst_4 : Invertible (α := R) ((Q : (a : M) → R) a : R)
rw :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
              (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R) a) :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
    (ι 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 b : R) •
          a -
        b)
⊢ HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) a) _ :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
    (ι 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 b : R) •
          a -
        b)
have rw₁ : HMul.hMul (β := CliffordAlgebra Q)
    (HMul.hMul (β := CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
    ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
  (ι 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 b : R) •
        a -
      b)
Tactic: rw [invOf_ι, map_smul, smul_mul_assoc, smul_mul_assoc, ι_mul_ι_mul_ι, ← map_smul, smul_sub,
    smul_smul, smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
inst_3 : Invertible (α := R) 2
m : M
h : IsUnit (M := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
⊢ IsUnit.{u_1} (M := R) ((Q : (a : M) → R) m : R)
have intro : ∀ (val : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)),
  IsUnit.{u_1} (M := R) ((Q : (a : M) → R) m : R)
Tactic: cases h.nonempty_invertible
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ ((f₁ : (a : M₁) → N) x) ((f₂ : (a : M₂) → N) y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
⊢ HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) 0 : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) 0 : CliffordAlgebra Qₙ)
have zero : HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
    ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
  HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
    HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
Tactic: rw [map_zero, zero_mul, mul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Prod (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ ((f₁ : (a : M₁) → N) x) ((f₂ : (a : M₂) → N) y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
zero :
  HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
⊢ HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) 0 : CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) =
    HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
      HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
        ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ)
        ((map f₁ : (a : CliffordAlgebra Q₁) → CliffordAlgebra Qₙ) 0 : CliffordAlgebra Qₙ)
have zero₁ : 0 =
  HPow.hPow (α := ℤˣ) (-1) (i₂ * i₁) •
    HMul.hMul (α := CliffordAlgebra Qₙ) (β := CliffordAlgebra Qₙ)
      ((map f₂ : (a : CliffordAlgebra Q₂) → CliffordAlgebra Qₙ) m₂ : CliffordAlgebra Qₙ) (0 : CliffordAlgebra Qₙ)
Tactic: rw [map_zero, zero_mul, mul_zero, smul_zero]