awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
m : M
hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
ι_mul :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
                ((0 : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
ι_mul₁ :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
                ((0 : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          x :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
ι_mul₂ :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
      (((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) 0 :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          x :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
ι_mul₃ :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
      ((0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
have ι_mul₄ : HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x - 0 =
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
Tactic: rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
      sub_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
m : M
hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
ι_mul :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
                ((0 : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
ι_mul₁ :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
                ((0 : (a : M) → M →ₗ[R] R) m) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          x :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
ι_mul₂ :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
      (((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) 0 :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          x :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
ι_mul₃ :
  HSub.hSub (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)
      ((0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
ι_mul₄ :
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x - 0 =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
have ι_mul₅ : HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x =
  HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
Tactic: rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
      sub_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
have algebraMap : ∀ (r : R),
  Eq (α := CliffordAlgebra Q)
    ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
Tactic: induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp_rw [changeForm_algebraMap]
  | add _ _ hx hy => rw [map_add, hx, hy]
  | ι_mul _ _ hx => rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
      sub_zero]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q)
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
have add : ∀ (x y : CliffordAlgebra Q) (hx : (changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x)
  (hy : (changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y),
  (changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y
Tactic: induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp_rw [changeForm_algebraMap]
  | add _ _ hx hy => rw [map_add, hx, hy]
  | ι_mul _ _ hx => rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
      sub_zero]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q)
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
add :
  ∀ (x y : CliffordAlgebra Q) (hx : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x)
    (hy : (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y),
    (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
have ι_mul : ∀ (x : CliffordAlgebra Q) (m : M) (hx : (changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x),
  (changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) =
    HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x
Tactic: induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp_rw [changeForm_algebraMap]
  | add _ _ hx hy => rw [map_add, hx, hy]
  | ι_mul _ _ hx => rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
      sub_zero]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x y : CliffordAlgebra Q
hx :
  Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') x : CliffordAlgebra Q'')
hy :
  Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') y : CliffordAlgebra Q'')
⊢ Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') (x + y)) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') (x + y) : CliffordAlgebra Q'')
have add : Eq (α := CliffordAlgebra Q'')
  ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
      (HAdd.hAdd (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y : CliffordAlgebra Q')) :
    CliffordAlgebra Q'')
  ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') (x + y) : CliffordAlgebra Q'')
Tactic: rw [map_add, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x y : CliffordAlgebra Q
hx :
  Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') x : CliffordAlgebra Q'')
hy :
  Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') y : CliffordAlgebra Q'')
add :
  Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        (HAdd.hAdd (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y : CliffordAlgebra Q')) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') (x + y) : CliffordAlgebra Q'')
⊢ Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') (x + y)) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') (x + y) : CliffordAlgebra Q'')
have add₁ : HAdd.hAdd (α := CliffordAlgebra Q'') (β := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
      CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y) :
      CliffordAlgebra Q'') =
  (changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') (x + y)
Tactic: rw [map_add, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x y : CliffordAlgebra Q
hx :
  Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') x : CliffordAlgebra Q'')
hy :
  Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') y : CliffordAlgebra Q'')
add :
  Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        (HAdd.hAdd (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x : CliffordAlgebra Q')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y : CliffordAlgebra Q')) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') (x + y) : CliffordAlgebra Q'')
add₁ :
  HAdd.hAdd (α := CliffordAlgebra Q'') (β := CliffordAlgebra Q'')
      ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
        CliffordAlgebra Q'')
      ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y) :
        CliffordAlgebra Q'') =
    (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') (x + y)
⊢ Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') (x + y)) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') (x + y) : CliffordAlgebra Q'')
have add₂ : HAdd.hAdd (α := CliffordAlgebra Q'') (β := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
      CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y) :
      CliffordAlgebra Q'') =
  HAdd.hAdd (α := CliffordAlgebra Q'') (β := CliffordAlgebra Q'')
    ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') x : CliffordAlgebra Q'')
    ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') y : CliffordAlgebra Q'')
Tactic: rw [map_add, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q
⊢ Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') x : CliffordAlgebra Q'')
have algebraMap : ∀ (r : R),
  Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
      CliffordAlgebra Q'')
    ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q'')
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
      CliffordAlgebra Q'')
Tactic: induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp_rw [changeForm_algebraMap]
  | add _ _ hx hy => rw [map_add, map_add, map_add, hx, hy]
  | ι_mul _ _ hx => rw [changeForm_ι_mul, map_sub, changeForm_ι_mul, changeForm_ι_mul, hx, sub_sub,
      LinearMap.add_apply, map_add, LinearMap.add_apply, changeForm_contractLeft, hx,
      add_comm (_ : CliffordAlgebra Q'')]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q'')
      ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
            ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
        CliffordAlgebra Q'')
      ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'')
          ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q'')
⊢ Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
      CliffordAlgebra Q'')
    ((changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') x : CliffordAlgebra Q'')
have add : ∀ (x y : CliffordAlgebra Q)
  (hx :
    Eq (α := CliffordAlgebra Q'')
      ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') x) :
        CliffordAlgebra Q'')
      ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') x : CliffordAlgebra Q''))
  (hy :
    Eq (α := CliffordAlgebra Q'')
      ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') y) :
        CliffordAlgebra Q'')
      ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') y : CliffordAlgebra Q'')),
  Eq (α := CliffordAlgebra Q'')
    ((changeForm h' : (a : CliffordAlgebra Q') → CliffordAlgebra Q'')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') (x + y)) :
      CliffordAlgebra Q'')
    ((changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q'') (x + y) : CliffordAlgebra Q'')
Tactic: induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp_rw [changeForm_algebraMap]
  | add _ _ hx hy => rw [map_add, map_add, map_add, hx, hy]
  | ι_mul _ _ hx => rw [changeForm_ι_mul, map_sub, changeForm_ι_mul, changeForm_ι_mul, hx, sub_sub,
      LinearMap.add_apply, map_add, LinearMap.add_apply, changeForm_contractLeft, hx,
      add_comm (_ : CliffordAlgebra Q'')]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
have simp_rw : (changeForm sorry : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
Tactic: simp_rw [(add_neg_cancel B), changeForm_self_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q'
⊢ (changeForm ⋯ : (a : CliffordAlgebra Q') → CliffordAlgebra Q') x = x
have simp_rw : (changeForm sorry : (a : CliffordAlgebra Q') → CliffordAlgebra Q') x = x
Tactic: simp_rw [(neg_add_cancel B), changeForm_self_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
y x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ (x₁ + x₂) * y = y * (x₁ + x₂)
have add : (x₁ + x₂) * y = y * x₁ + y * x₂
Tactic: rw [mul_add, add_mul, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
y x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
add : (x₁ + x₂) * y = y * x₁ + y * x₂
⊢ (x₁ + x₂) * y = y * (x₁ + x₂)
have add₁ : x₁ * y + x₂ * y = y * x₁ + y * x₂
Tactic: rw [mul_add, add_mul, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
y x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
add : (x₁ + x₂) * y = y * x₁ + y * x₂
add₁ : x₁ * y + x₂ * y = y * x₁ + y * x₂
⊢ (x₁ + x₂) * y = y * (x₁ + x₂)
have add₂ : y * x₁ + x₂ * y = y * x₁ + y * x₂
Tactic: rw [mul_add, add_mul, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
y x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
add : (x₁ + x₂) * y = y * x₁ + y * x₂
add₁ : x₁ * y + x₂ * y = y * x₁ + y * x₂
add₂ : y * x₁ + x₂ * y = y * x₁ + y * x₂
⊢ (x₁ + x₂) * y = y * (x₁ + x₂)
have add₃ : y * x₁ + y * x₂ = y * x₁ + y * x₂
Tactic: rw [mul_add, add_mul, hx₁, hx₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
y x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ x₁ * x₂ * y = y * (x₁ * x₂)
have mul : x₁ * (x₂ * y) = y * (x₁ * x₂)
Tactic: rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Equivs (goal)
Goal:
R : Type u_1
inst : CommRing R
y x₁ x₂ : CliffordAlgebra (R := R) (M := Unit) 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
mul : x₁ * (x₂ * y) = y * (x₁ * x₂)
⊢ x₁ * x₂ * y = y * (x₁ * x₂)
have mul₁ : x₁ * (y * x₂) = y * (x₁ * x₂)
Tactic: rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]