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)
g : CliffordAlgebra Q →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι Q = f ↔
    g =
      (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)
have h : g.toLinearMap ∘ₗ ι Q = f ↔
  Eq (α :=
    { 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) })
    ((Equiv.symm (lift Q) :
          (a : CliffordAlgebra Q →ₐ[R] 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) })
        g :
      { 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) })
    (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 :
      { 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) })
Tactic: convert! (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).symm_apply_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
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)
g : CliffordAlgebra Q →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι Q = f ↔
    Eq (α :=
      { 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) })
      ((Equiv.symm (lift Q) :
            (a : CliffordAlgebra Q →ₐ[R] 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) })
          g :
        { 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) })
      (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 :
        { 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) })
have h : g.toLinearMap ∘ₗ ι Q = f ↔
  Eq (α :=
    { 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) })
    (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))
      (g.toLinearMap ∘ₗ ι Q) sorry)
    (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)
Tactic: rw [lift_symm_apply, Subtype.mk_eq_mk]
-- 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)
g : CliffordAlgebra Q →ₐ[R] A
h :
  g.toLinearMap ∘ₗ ι Q = f ↔
    Eq (α :=
      { 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) })
      (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))
        (g.toLinearMap ∘ₗ ι Q) ⋯)
      (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)
⊢ g.toLinearMap ∘ₗ ι Q = f ↔
    Eq (α :=
      { 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) })
      ((Equiv.symm (lift Q) :
            (a : CliffordAlgebra Q →ₐ[R] 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) })
          g :
        { 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) })
      (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 :
        { 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) })
have h₁ : g.toLinearMap ∘ₗ ι Q = f ↔ g.toLinearMap ∘ₗ ι Q = f
Tactic: rw [lift_symm_apply, Subtype.mk_eq_mk]
-- 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 : Semiring A
inst_4 : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
⊢ f = g
have a : Eq (α :=
  { 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) })
  ((Equiv.symm (lift Q) :
        (a : CliffordAlgebra Q →ₐ[R] 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) })
      f :
    { 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) })
  ((Equiv.symm (lift Q) :
        (a : CliffordAlgebra Q →ₐ[R] 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) })
      g :
    { 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) })
Tactic: apply (lift Q).symm.injective
-- 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
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
of : { f : M →ₗ[R] ↥s //
  ∀ (m : M),
    HMul.hMul (α := ↥s) (β := ↥s) ((f : (a : M) → ↥s) m : ↥s) ((f : (a : M) → ↥s) m : ↥s) =
      (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m) } :=
  Subtype.mk (p := fun (f : M →ₗ[R] ↥s) ↦
    ∀ (m : M),
      HMul.hMul (α := ↥s) (β := ↥s) ((f : (a : M) → ↥s) m : ↥s) ((f : (a : M) → ↥s) m : ↥s) =
        (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m))
    (LinearMap.codRestrict
      ((Subalgebra.toSubmodule : (a : Subalgebra R (CliffordAlgebra Q)) → Submodule R (CliffordAlgebra Q)) s)
      (CliffordAlgebra.ι Q) ι)
    ⋯
⊢ s.val.comp
      ((lift Q :
          (a :
              { f : M →ₗ[R] ↥s //
                ∀ (m : M),
                  (f : (a : M) → ↥s) m * (f : (a : M) → ↥s) m =
                    (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m) }) →
            CliffordAlgebra Q →ₐ[R] ↥s)
        of) =
    AlgHom.id R (CliffordAlgebra Q)
have a₁ : ∀ (x : M),
  Eq (α := CliffordAlgebra Q)
    ((AlgHom.toLinearMap
              (s.val.comp
                ((lift Q :
                    (a :
                        { f : M →ₗ[R] ↥s //
                          ∀ (m : M),
                            (f : (a : M) → ↥s) m * (f : (a : M) → ↥s) m =
                              (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m) }) →
                      CliffordAlgebra Q →ₐ[R] ↥s)
                  of)) ∘ₗ
            CliffordAlgebra.ι Q :
          (a : M) → CliffordAlgebra Q)
        x :
      CliffordAlgebra Q)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q)) ∘ₗ CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x :
      CliffordAlgebra Q)
Tactic: ext 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
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
of : { f : M →ₗ[R] ↥s //
  ∀ (m : M),
    HMul.hMul (α := ↥s) (β := ↥s) ((f : (a : M) → ↥s) m : ↥s) ((f : (a : M) → ↥s) m : ↥s) =
      (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m) } :=
  Subtype.mk (p := fun (f : M →ₗ[R] ↥s) ↦
    ∀ (m : M),
      HMul.hMul (α := ↥s) (β := ↥s) ((f : (a : M) → ↥s) m : ↥s) ((f : (a : M) → ↥s) m : ↥s) =
        (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m))
    (LinearMap.codRestrict
      ((Subalgebra.toSubmodule : (a : Subalgebra R (CliffordAlgebra Q)) → Submodule R (CliffordAlgebra Q)) s)
      (CliffordAlgebra.ι Q) ι)
    ⋯
⊢ C a
have of_id : s.val.comp
    ((lift Q :
        (a :
            { f : M →ₗ[R] ↥s //
              ∀ (m : M),
                (f : (a : M) → ↥s) m * (f : (a : M) → ↥s) m =
                  (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m) }) →
          CliffordAlgebra Q →ₐ[R] ↥s)
      of) =
  AlgHom.id R (CliffordAlgebra Q)
Tactic: have of_id : s.val.comp (lift Q of) = AlgHom.id R (CliffordAlgebra Q) := by
    ext x
    simpa [of, -LinearMap.codRestrict_apply]
      -- This `@[simp]` lemma applies to `coeSort s.subModule`, but the goal contains
      -- a plain `coeSort s`. So we remove it from the `simp` arguments, and add it to
      -- the term that `simpa` will simplify before applying.
      using LinearMap.codRestrict_apply s.toSubmodule (CliffordAlgebra.ι Q) x (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
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
of : { f : M →ₗ[R] ↥s //
  ∀ (m : M),
    HMul.hMul (α := ↥s) (β := ↥s) ((f : (a : M) → ↥s) m : ↥s) ((f : (a : M) → ↥s) m : ↥s) =
      (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m) } :=
  Subtype.mk (p := fun (f : M →ₗ[R] ↥s) ↦
    ∀ (m : M),
      HMul.hMul (α := ↥s) (β := ↥s) ((f : (a : M) → ↥s) m : ↥s) ((f : (a : M) → ↥s) m : ↥s) =
        (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m))
    (LinearMap.codRestrict
      ((Subalgebra.toSubmodule : (a : Subalgebra R (CliffordAlgebra Q)) → Submodule R (CliffordAlgebra Q)) s)
      (CliffordAlgebra.ι Q) ι)
    ⋯
of_id :
  s.val.comp
      ((lift Q :
          (a :
              { f : M →ₗ[R] ↥s //
                ∀ (m : M),
                  (f : (a : M) → ↥s) m * (f : (a : M) → ↥s) m =
                    (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m) }) →
            CliffordAlgebra Q →ₐ[R] ↥s)
        of) =
    AlgHom.id R (CliffordAlgebra Q)
⊢ C a
have rw : C
  ((s.val.comp
        ((lift Q :
            (a :
                { f : M →ₗ[R] ↥s //
                  ∀ (m : M),
                    (f : (a : M) → ↥s) m * (f : (a : M) → ↥s) m =
                      (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m) }) →
              CliffordAlgebra Q →ₐ[R] ↥s)
          of) :
      (a : CliffordAlgebra Q) → CliffordAlgebra Q)
    a)
Tactic: rw [← AlgHom.id_apply (R := R) a, ← of_id]
-- 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
⊢ Eq (α := Subalgebra R (CliffordAlgebra Q))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) ⊤
have refine : ∀ (x : CliffordAlgebra Q) (hx : Membership.mem (γ := Subalgebra R (CliffordAlgebra Q)) ⊤ x),
  Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) x
Tactic: refine top_unique fun x hx => ?_
-- 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
x : CliffordAlgebra Q
⊢ Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) x
have algebraMap : ∀ (r : R),
  Membership.mem (α := CliffordAlgebra Q) (γ := Subalgebra R (CliffordAlgebra Q))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q)))
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
Tactic: induction x using induction with
  | algebraMap => exact algebraMap_mem _ _
  | add x y hx hy => exact add_mem hx hy
  | mul x y hx hy => exact mul_mem hx hy
  | ι x => exact Algebra.subset_adjoin (Set.mem_range_self _)
Cleared hypotheses: x
-- 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
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : R),
    Membership.mem (α := CliffordAlgebra Q) (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q)))
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
⊢ Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) x
have add : ∀ (x y : CliffordAlgebra Q)
  (hx :
    Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) x)
  (hy :
    Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) y),
  Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) (x + y)
Tactic: induction x using induction with
  | algebraMap => exact algebraMap_mem _ _
  | add x y hx hy => exact add_mem hx hy
  | mul x y hx hy => exact mul_mem hx hy
  | ι x => exact Algebra.subset_adjoin (Set.mem_range_self _)
Cleared hypotheses: x
-- 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
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : R),
    Membership.mem (α := CliffordAlgebra Q) (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q)))
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
add :
  ∀ (x y : CliffordAlgebra Q)
    (hx :
      Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) x)
    (hy :
      Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) y),
    Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) (x + y)
⊢ Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) x
have mul : ∀ (x y : CliffordAlgebra Q)
  (hx :
    Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) x)
  (hy :
    Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) y),
  Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) (x * y)
Tactic: induction x using induction with
  | algebraMap => exact algebraMap_mem _ _
  | add x y hx hy => exact add_mem hx hy
  | mul x y hx hy => exact mul_mem hx hy
  | ι x => exact Algebra.subset_adjoin (Set.mem_range_self _)
Cleared hypotheses: x
-- 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
x : CliffordAlgebra Q
algebraMap :
  ∀ (r : R),
    Membership.mem (α := CliffordAlgebra Q) (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q)))
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
add :
  ∀ (x y : CliffordAlgebra Q)
    (hx :
      Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) x)
    (hy :
      Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) y),
    Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) (x + y)
mul :
  ∀ (x y : CliffordAlgebra Q)
    (hx :
      Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) x)
    (hy :
      Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) y),
    Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) (x * y)
⊢ Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) x
have ι : ∀ (x : M),
  Membership.mem (α := CliffordAlgebra Q) (γ := Subalgebra R (CliffordAlgebra Q))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q)))
    ((ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
Tactic: induction x using induction with
  | algebraMap => exact algebraMap_mem _ _
  | add x y hx hy => exact add_mem hx hy
  | mul x y hx hy => exact mul_mem hx hy
  | ι x => exact Algebra.subset_adjoin (Set.mem_range_self _)
Cleared hypotheses: x
-- 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)
⊢ 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.{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]