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)
rw :
  LinearMap.range
      (AlgHom.toLinearMap
          ((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)) ∘ₗ
        ι Q) =
    f.range
⊢ Submodule.map
      (AlgHom.toLinearMap
        ((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)))
      (ι Q).range =
    f.range
have rw₁ : f.range = f.range
Tactic: rw [← LinearMap.range_comp, ι_comp_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
Q₁ : QuadraticForm R M₁
⊢ map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁)
have a : ∀ (m : M₁),
  Eq (α := CliffordAlgebra Q₁)
    (((map (QuadraticMap.Isometry.id Q₁)).toLinearMap ∘ₗ ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m : CliffordAlgebra Q₁)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q₁)) ∘ₗ ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m :
      CliffordAlgebra Q₁)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
⊢ (map f).comp (map g) = map (f.comp g)
have a : ∀ (m : M₁),
  Eq (α := CliffordAlgebra Q₃)
    ((((map f).comp (map g)).toLinearMap ∘ₗ ι Q₁ : (a : M₁) → CliffordAlgebra Q₃) m : CliffordAlgebra Q₃)
    (((map (f.comp g)).toLinearMap ∘ₗ ι Q₁ : (a : M₁) → CliffordAlgebra Q₃) m : CliffordAlgebra Q₃)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ Eq (α := CliffordAlgebra Q₃)
    ((map f : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₃)
        ((map g : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m)) :
      CliffordAlgebra Q₃)
    ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₃)
have a : Eq (α := CliffordAlgebra Q₃)
  ((map f : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₃)
      ((ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) ((g : (a : M₁) → M₂) m)) :
    CliffordAlgebra Q₃)
  ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
    CliffordAlgebra Q₃)
Tactic: rw [map_apply_ι, map_apply_ι, map_apply_ι, QuadraticMap.Isometry.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
a :
  Eq (α := CliffordAlgebra Q₃)
    ((map f : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₃)
        ((ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) ((g : (a : M₁) → M₂) m)) :
      CliffordAlgebra Q₃)
    ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₃)
⊢ Eq (α := CliffordAlgebra Q₃)
    ((map f : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₃)
        ((map g : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m)) :
      CliffordAlgebra Q₃)
    ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₃)
have a₁ : Eq (α := CliffordAlgebra Q₃)
  ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) m : M₂)) : CliffordAlgebra Q₃)
  ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
    CliffordAlgebra Q₃)
Tactic: rw [map_apply_ι, map_apply_ι, map_apply_ι, QuadraticMap.Isometry.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
a :
  Eq (α := CliffordAlgebra Q₃)
    ((map f : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₃)
        ((ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) ((g : (a : M₁) → M₂) m)) :
      CliffordAlgebra Q₃)
    ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₃)
a₁ :
  Eq (α := CliffordAlgebra Q₃)
    ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) m : M₂)) : CliffordAlgebra Q₃)
    ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₃)
⊢ Eq (α := CliffordAlgebra Q₃)
    ((map f : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₃)
        ((map g : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m)) :
      CliffordAlgebra Q₃)
    ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₃)
have a₂ : Eq (α := CliffordAlgebra Q₃)
  ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) m : M₂)) : CliffordAlgebra Q₃)
  ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f.comp g : (a : M₁) → M₃) m) : CliffordAlgebra Q₃)
Tactic: rw [map_apply_ι, map_apply_ι, map_apply_ι, QuadraticMap.Isometry.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
a :
  Eq (α := CliffordAlgebra Q₃)
    ((map f : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₃)
        ((ι Q₂ : (a : M₂) → CliffordAlgebra Q₂) ((g : (a : M₁) → M₂) m)) :
      CliffordAlgebra Q₃)
    ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₃)
a₁ :
  Eq (α := CliffordAlgebra Q₃)
    ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) m : M₂)) : CliffordAlgebra Q₃)
    ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₃)
a₂ :
  Eq (α := CliffordAlgebra Q₃)
    ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) m : M₂)) : CliffordAlgebra Q₃)
    ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f.comp g : (a : M₁) → M₃) m) : CliffordAlgebra Q₃)
⊢ Eq (α := CliffordAlgebra Q₃)
    ((map f : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₃)
        ((map g : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m)) :
      CliffordAlgebra Q₃)
    ((map (f.comp g) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) ((ι Q₁ : (a : M₁) → CliffordAlgebra Q₁) m) :
      CliffordAlgebra Q₃)
have a₃ : Eq (α := CliffordAlgebra Q₃)
  ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) m : M₂)) : CliffordAlgebra Q₃)
  ((ι Q₃ : (a : M₃) → CliffordAlgebra Q₃) ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) m : M₂)) : CliffordAlgebra Q₃)
Tactic: rw [map_apply_ι, map_apply_ι, map_apply_ι, QuadraticMap.Isometry.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
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₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
h : LeftInverse.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑g : (a : M₂) → M₁) (⇑f : (a : M₁) → M₂)
⊢ LeftInverse (α := CliffordAlgebra Q₁) (β := CliffordAlgebra Q₂)
    (⇑(map g) : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁)
    (⇑(map f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂)
have refine : ∀ (x : CliffordAlgebra Q₁),
  (map g : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁) ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) x) =
    x
Tactic: refine fun x => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
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₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
h : LeftInverse.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑g : (a : M₂) → M₁) (⇑f : (a : M₁) → M₂)
x : CliffordAlgebra Q₁
⊢ (map g : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁) ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) x) =
    x
have h₁ : g.comp f = QuadraticMap.Isometry.id Q₁
Tactic: replace h : g.comp f = QuadraticMap.Isometry.id Q₁ := DFunLike.ext _ _ 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_4
M₂ : Type u_5
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₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
⊢ (map g : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁) ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) x) =
    x
have rw : ((map g).comp (map f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
Tactic: rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
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₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
rw : ((map g).comp (map f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
⊢ (map g : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁) ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) x) =
    x
have rw₁ : (map (g.comp f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
Tactic: rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
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₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
rw : ((map g).comp (map f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₁ : (map (g.comp f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
⊢ (map g : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁) ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) x) =
    x
have rw₂ : (map (QuadraticMap.Isometry.id Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
Tactic: rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
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₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
rw : ((map g).comp (map f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₁ : (map (g.comp f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₂ : (map (QuadraticMap.Isometry.id Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
⊢ (map g : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁) ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) x) =
    x
have rw₃ : (AlgHom.id R (CliffordAlgebra Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
Tactic: rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
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₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
rw : ((map g).comp (map f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₁ : (map (g.comp f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₂ : (map (QuadraticMap.Isometry.id Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₃ : (AlgHom.id R (CliffordAlgebra Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
⊢ (map g : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁) ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) x) =
    x
have rw₄ : id x = x
Tactic: rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
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₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
rw : ((map g).comp (map f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₁ : (map (g.comp f) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₂ : (map (QuadraticMap.Isometry.id Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₃ : (AlgHom.id R (CliffordAlgebra Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x = x
rw₄ : id x = x
⊢ (map g : (a : CliffordAlgebra Q₂) → CliffordAlgebra Q₁) ((map f : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₂) x) =
    x
have rw₅ : x = x
Tactic: rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]
-- 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
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
⊢ map (e.toIsometry.comp e.symm.toIsometry) = AlgHom.id R (CliffordAlgebra Q₂)
have h : e.toIsometry.comp e.symm.toIsometry = QuadraticMap.Isometry.id Q₂
Tactic: convert! map_id Q₂ using 2
-- 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
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
⊢ e.toIsometry.comp e.symm.toIsometry = QuadraticMap.Isometry.id Q₂
have h : ∀ (m : M₂),
  Eq (α := M₂) ((e.toIsometry.comp e.symm.toIsometry : (a : M₂) → M₂) m : M₂)
    ((QuadraticMap.Isometry.id Q₂ : (a : M₂) → M₂) m : M₂)
Tactic: ext m
-- 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
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
⊢ map (e.symm.toIsometry.comp e.toIsometry) = AlgHom.id R (CliffordAlgebra Q₁)
have h : e.symm.toIsometry.comp e.toIsometry = QuadraticMap.Isometry.id Q₁
Tactic: convert! map_id Q₁ using 2
-- 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
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_5 : AddCommGroup M₁
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
⊢ e.symm.toIsometry.comp e.toIsometry = QuadraticMap.Isometry.id Q₁
have h : ∀ (m : M₁),
  Eq (α := M₁) ((e.symm.toIsometry.comp e.toIsometry : (a : M₁) → M₁) m : M₁)
    ((QuadraticMap.Isometry.id Q₁ : (a : M₁) → M₁) m : M₁)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃
⊢ (equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) = equivOfIsometry (e₁₂.trans e₂₃)
have h : ∀ (x : CliffordAlgebra Q₁),
  Eq (α := CliffordAlgebra Q₃)
    (((equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) x :
      CliffordAlgebra Q₃)
    ((equivOfIsometry (e₁₂.trans e₂₃) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) x : CliffordAlgebra Q₃)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
Q₁ : QuadraticForm R M₁
⊢ equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) = AlgEquiv.refl
have h : ∀ (x : CliffordAlgebra Q₁),
  Eq (α := CliffordAlgebra Q₁)
    ((equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x :
      CliffordAlgebra Q₁)
    ((AlgEquiv.refl : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x : CliffordAlgebra Q₁)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory (goal)
Goal:
R : Type u
inst : CommRing R
_M _N _P : QuadraticModuleCat R
f : _M ⟶ _N
g : _N ⟶ _P
⊢ AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry (f ≫ g))) =
    AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry f)) ≫ AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry g))
have hf : ∀ (x : (↑_M.toModuleCat : Type u)),
  Eq (α := (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
    (((AlgCat.Hom.hom (AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry (f ≫ g))))).toLinearMap ∘ₗ
            CliffordAlgebra.ι _M.form :
          (a : (↑_M.toModuleCat : Type u)) → (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
        x :
      (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
    (((AlgCat.Hom.hom
                (AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry f)) ≫
                  AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry g)))).toLinearMap ∘ₗ
            CliffordAlgebra.ι _M.form :
          (a : (↑_M.toModuleCat : Type u)) → (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
        x :
      (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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
⊢ Eq (α := CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q) (AlgHom.comp involute involute) (AlgHom.id R (CliffordAlgebra Q))
have a : ∀ (x : M),
  Eq (α := CliffordAlgebra Q)
    ((AlgHom.toLinearMap (AlgHom.comp involute involute) ∘ₗ ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q)) ∘ₗ ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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
⊢ Eq (α := CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) (reverse ∘ₗ AlgHom.toLinearMap involute)
    (AlgHom.toLinearMap involute ∘ₗ reverse)
have h : ∀ (x : CliffordAlgebra Q),
  Eq (α := CliffordAlgebra Q)
    ((reverse ∘ₗ AlgHom.toLinearMap involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((AlgHom.toLinearMap involute ∘ₗ reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation (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
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) :
      CliffordAlgebra Q)
have h : ∀ (r : R),
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
      CliffordAlgebra Q)
Tactic: induction x using CliffordAlgebra.induction with
  | algebraMap => simp
  | ι => simp
  | mul a b ha hb => simp only [ha, hb, reverse.map_mul, map_mul]
  | add a b ha hb => simp only [ha, hb, reverse.map_add, map_add]
Cleared hypotheses: x