awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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) ι)
    ⋯
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:
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 := ι)

Premises used: CliffordAlgebra.ι, Subalgebra.toSubmodule, LinearMap.codRestrict_apply, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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)

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 := ι)
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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)
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)
⊢ C a

Tactic:
rw [← AlgHom.id_apply (R := R) a, ← of_id]

Premises used: AlgHom.id_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
    ((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:
(lift Q of a).prop

Premises used: Set.Mem, CliffordAlgebra.lift, Subtype.prop, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
    ((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:
exact (lift Q of a).prop

Premises used: CliffordAlgebra.lift, Subtype.prop, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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))) ⊤

Tactic:
top_unique fun x hx => ?_

Premises used: top_unique
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
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
⊢ Eq (α := Subalgebra R (CliffordAlgebra Q))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))) ⊤

Tactic:
refine top_unique fun x hx => ?_

Premises used: top_unique
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
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:
algebraMap_mem _ _

Premises used: Set.Mem, algebraMap_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
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:
exact algebraMap_mem _ _

Premises used: algebraMap_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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 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:
add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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 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:
exact add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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 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:
mul_mem hx hy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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 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:
exact mul_mem hx hy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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 : 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:
Algebra.subset_adjoin (Set.mem_range_self _)

Premises used: Set.mem_range_self, Algebra.subset_adjoin
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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 : 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:
exact Algebra.subset_adjoin (Set.mem_range_self _)

Premises used: Set.mem_range_self, Algebra.subset_adjoin
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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) (⇑(CliffordAlgebra.ι 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) (⇑(CliffordAlgebra.ι Q) : (a : M) → CliffordAlgebra Q))) x)
    (hy :
      Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(CliffordAlgebra.ι Q) : (a : M) → CliffordAlgebra Q))) y),
    Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(CliffordAlgebra.ι 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) (⇑(CliffordAlgebra.ι Q) : (a : M) → CliffordAlgebra Q))) x)
    (hy :
      Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(CliffordAlgebra.ι Q) : (a : M) → CliffordAlgebra Q))) y),
    Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(CliffordAlgebra.ι Q) : (a : M) → CliffordAlgebra Q))) (x * y)
ι :
  ∀ (x : M),
    Membership.mem (α := CliffordAlgebra Q) (γ := Subalgebra R (CliffordAlgebra Q))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(CliffordAlgebra.ι Q) : (a : M) → CliffordAlgebra Q)))
      ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
⊢ Membership.mem (γ := Subalgebra R (CliffordAlgebra Q))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(CliffordAlgebra.ι Q) : (a : M) → CliffordAlgebra Q))) x

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 _)

Premises used: Set.mem_range_self, CliffordAlgebra.ι, Algebra.algebraMap, Algebra.subset_adjoin, algebraMap_mem
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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 :
  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)
⊢ 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)

Tactic:
rw [f.map_add, mul_add, add_mul, add_mul]

Premises used: add_mul, LinearMap.map_add, mul_add
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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 : 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:
abel