awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
cond :
  ∀ (m : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)
simp_rw :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.map (A := CliffordAlgebra Q)
      ((lift Q :
          (a :
              { f : M →ₗ[R] A //
                ∀ (m : M),
                  (f : (a : M) → A) m * (f : (a : M) → A) m = (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) }) →
            CliffordAlgebra Q →ₐ[R] A)
        (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
          f cond))
      ⊤)
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
⊢ Eq.{u_3 + 1} (α := Subalgebra R A)
    (AlgHom.range (A := CliffordAlgebra Q)
      ((lift Q :
          (a :
              { f : M →ₗ[R] A //
                ∀ (m : M),
                  (f : (a : M) → A) m * (f : (a : M) → A) m = (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) }) →
            CliffordAlgebra Q →ₐ[R] A)
        (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
          f cond)))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
have simp_rw₁ : Eq.{u_3 + 1} (α := Subalgebra R A)
  (Subalgebra.map (A := CliffordAlgebra Q)
    ((lift Q :
        (a :
            { f : M →ₗ[R] A //
              ∀ (m : M),
                (f : (a : M) → A) m * (f : (a : M) → A) m = (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) }) →
          CliffordAlgebra Q →ₐ[R] A)
      (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
        ∀ (m : M),
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
        f cond))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))))
  (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
Tactic: simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
f : M →ₗ[R] A
hf :
  ∀ (x : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)
a b : M
⊢ HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) b : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) a : A) =
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a + b) : A) ((f : (a : M) → A) (a + b) : A) -
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) a : A) -
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A)
have rw : HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) b : A) +
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) a : A) =
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) a : A) +
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) a : A) +
        (HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) b : A) +
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A)) -
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) a : A) -
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A)
Tactic: rw [f.map_add, mul_add, add_mul, add_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
f : M →ₗ[R] A
hf :
  ∀ (x : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)
a b : M
⊢ HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a + b) : A) ((f : (a : M) → A) (a + b) : A) -
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) a : A) -
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A) =
    HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)
have rw : HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
      (HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) a : A)) -
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A) =
  HSub.hSub (β := A)
    (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)
Tactic: rw [hf, hf, hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
f : M →ₗ[R] A
hf :
  ∀ (x : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)
a b : M
rw :
  HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        (HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) a : A)) -
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A) =
    HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)
⊢ HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a + b) : A) ((f : (a : M) → A) (a + b) : A) -
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) a : A) -
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A) =
    HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)
have rw₁ : HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A) -
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A) =
  HSub.hSub (β := A)
    (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)
Tactic: rw [hf, hf, hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
f : M →ₗ[R] A
hf :
  ∀ (x : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)
a b : M
rw :
  HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        (HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) a : A)) -
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A) =
    HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)
rw₁ :
  HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A) -
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A) =
    HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)
⊢ HMul.hMul (α := A) (β := A) ((f : (a : M) → A) (a + b) : A) ((f : (a : M) → A) (a + b) : A) -
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) a : A) ((f : (a : M) → A) a : A) -
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) b : A) ((f : (a : M) → A) b : A) =
    HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)
have rw₂ : HSub.hSub (β := A)
    (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A) =
  HSub.hSub (β := A)
    (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A)
Tactic: rw [hf, hf, hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
f : M →ₗ[R] A
hf :
  ∀ (x : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)
a b : M
⊢ HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A) =
    (algebraMap R A : (a : R) → A)
      (HSub.hSub (β := R) (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R))
        ((Q : (a : M) → R) b : R))
have rw : HSub.hSub (α := A) (β := A)
    ((algebraMap R A : (a : R) → A)
        (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R)) :
      A)
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A) =
  (algebraMap R A : (a : R) → A)
    (HSub.hSub (β := R) (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R))
      ((Q : (a : M) → R) b : R))
Tactic: rw [← map_sub, ← map_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
f : M →ₗ[R] A
hf :
  ∀ (x : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)
a b : M
rw :
  HSub.hSub (α := A) (β := A)
      ((algebraMap R A : (a : R) → A)
          (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R)) :
        A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A) =
    (algebraMap R A : (a : R) → A)
      (HSub.hSub (β := R) (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R))
        ((Q : (a : M) → R) b : R))
⊢ HSub.hSub (β := A)
      (HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) (a + b) : R) : A)
        ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) a : R) : A))
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) b : R) : A) =
    (algebraMap R A : (a : R) → A)
      (HSub.hSub (β := R) (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R))
        ((Q : (a : M) → R) b : R))
have rw₁ : Eq.{u_4 + 1} (α := A)
  ((algebraMap R A : (a : R) → A)
      (HSub.hSub (β := R) (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R))
        ((Q : (a : M) → R) b : R)) :
    A)
  ((algebraMap R A : (a : R) → A)
      (HSub.hSub (β := R) (HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) (a + b) : R) ((Q : (a : M) → R) a : R))
        ((Q : (a : M) → R) b : R)) :
    A)
Tactic: rw [← map_sub, ← map_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
⊢ (∀ (x : M),
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
        (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)) ↔
    LinearMap.compl₂ (LinearMap.mul R A) f ∘ₗ f + LinearMap.compl₂ (LinearMap.flip (LinearMap.mul R A)) f ∘ₗ f =
      LinearMap.compr₂ (Pₗ := R) (QuadraticMap.polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q)
        (Algebra.linearMap R A)
have simp_rw : (∀ (x : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)) ↔
  ∀ (x x_1 : M),
    Eq.{u_4 + 1} (α := A)
      ((((LinearMap.compl₂ (LinearMap.mul R A) f ∘ₗ f + LinearMap.compl₂ (LinearMap.flip (LinearMap.mul R A)) f ∘ₗ f :
                  (a : M) → M →ₗ[R] A)
                x :
              M →ₗ[R] A) :
            (a : M) → A)
          x_1 :
        A)
      ((((LinearMap.compr₂ (Pₗ := R) (QuadraticMap.polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q)
                    (Algebra.linearMap R A) :
                  (a : M) → M →ₗ[R] A)
                x :
              M →ₗ[R] A) :
            (a : M) → A)
          x_1 :
        A)
Tactic: simp_rw [DFunLike.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
⊢ (∀ (x : M),
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
        (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)) ↔
    ∀ (x x_1 : M),
      Eq.{u_4 + 1} (α := A)
        ((((LinearMap.compl₂ (LinearMap.mul R A) f ∘ₗ f + LinearMap.compl₂ (LinearMap.flip (LinearMap.mul R A)) f ∘ₗ f :
                    (a : M) → M →ₗ[R] A)
                  x :
                M →ₗ[R] A) :
              (a : M) → A)
            x_1 :
          A)
        ((((LinearMap.compr₂ (Pₗ := R) (QuadraticMap.polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q)
                      (Algebra.linearMap R A) :
                    (a : M) → M →ₗ[R] A)
                  x :
                M →ₗ[R] A) :
              (a : M) → A)
            x_1 :
          A)
have refine : ∀
  (h :
    ∀ (x x_1 : M),
      Eq.{u_4 + 1} (α := A)
        ((((LinearMap.compl₂ (LinearMap.mul R A) f ∘ₗ f + LinearMap.compl₂ (LinearMap.flip (LinearMap.mul R A)) f ∘ₗ f :
                    (a : M) → M →ₗ[R] A)
                  x :
                M →ₗ[R] A) :
              (a : M) → A)
            x_1 :
          A)
        ((((LinearMap.compr₂ (Pₗ := R) (QuadraticMap.polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q)
                      (Algebra.linearMap R A) :
                    (a : M) → M →ₗ[R] A)
                  x :
                M →ₗ[R] A) :
              (a : M) → A)
            x_1 :
          A))
  (x : M),
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)
Tactic: refine ⟨mul_add_swap_eq_polar_of_forall_mul_self_eq _, fun h x => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (hypothesis)
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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
h :
  ∀ (x x_1 : M),
    Eq.{u_4 + 1} (α := A)
      ((((LinearMap.compl₂ (LinearMap.mul R A) f ∘ₗ f + LinearMap.compl₂ (LinearMap.flip (LinearMap.mul R A)) f ∘ₗ f :
                  (a : M) → M →ₗ[R] A)
                x :
              M →ₗ[R] A) :
            (a : M) → A)
          x_1 :
        A)
      ((((LinearMap.compr₂ (Pₗ := R) (QuadraticMap.polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q)
                    (Algebra.linearMap R A) :
                  (a : M) → M →ₗ[R] A)
                x :
              M →ₗ[R] A) :
            (a : M) → A)
          x_1 :
        A)
x : M
⊢ HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)
have h₁ : ∀ (x y : M),
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) y : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((f : (a : M) → A) x : A) =
    (algebraMap R A : (a : R) → A) (QuadraticMap.polar (⇑Q : (a : M) → R) x y)
Tactic: change ∀ x y : M, f x * f y + f y * f x = algebraMap R A (QuadraticMap.polar Q x y) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
x : M
h :
  ∀ (x y : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) y : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) (QuadraticMap.polar (⇑Q : (a : M) → R) x y)
⊢ HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R)
have apply : 2 * HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
  HMul.hMul (α := A) (β := A) (2 : A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
Tactic: apply h2.mul_left_cancel
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
x : M
h :
  ∀ (x y : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) y : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) (QuadraticMap.polar (⇑Q : (a : M) → R) x y)
⊢ 2 * HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    HMul.hMul (α := A) (β := A) (2 : A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
have rw : HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) +
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
  HMul.hMul (α := A) (β := A) (2 : A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
Tactic: rw [two_mul, two_mul, h x x, QuadraticMap.polar_self, two_smul, map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
x : M
h :
  ∀ (x y : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) y : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) (QuadraticMap.polar (⇑Q : (a : M) → R) x y)
rw :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    HMul.hMul (α := A) (β := A) (2 : A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
⊢ 2 * HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    HMul.hMul (α := A) (β := A) (2 : A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
have rw₁ : HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) +
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
  HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
Tactic: rw [two_mul, two_mul, h x x, QuadraticMap.polar_self, two_smul, map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (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
A : Type u_4
inst_3 : Ring A
inst_4 : Algebra R A
h2 : IsUnit.{u_4} (M := A) 2
f : M →ₗ[R] A
x : M
h :
  ∀ (x y : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) y : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) y : A) ((f : (a : M) → A) x : A) =
      (algebraMap R A : (a : R) → A) (QuadraticMap.polar (⇑Q : (a : M) → R) x y)
rw :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    HMul.hMul (α := A) (β := A) (2 : A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
rw₁ :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
      ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
⊢ 2 * HMul.hMul (α := A) (β := A) ((f : (a : M) → A) x : A) ((f : (a : M) → A) x : A) =
    HMul.hMul (α := A) (β := A) (2 : A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
have rw₂ : (algebraMap R A : (a : R) → A) (QuadraticMap.polar (⇑Q : (a : M) → R) x x) =
  HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
    ((algebraMap R A : (a : R) → A) ((Q : (a : M) → R) x : R) : A)
Tactic: rw [two_mul, two_mul, h x x, QuadraticMap.polar_self, two_smul, map_add]