awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : ↥(symplecticGroup l R)
⊢ (↑A⁻¹ : Matrix (l ⊕ l) (l ⊕ l) R) = (↑A : Matrix (l ⊕ l) (l ⊕ l) R)⁻¹
have refine : -J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R)ᵀ * J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R) = 1
Tactic: refine (coe_inv A).trans (inv_eq_left_inv ?_).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A_1 : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
A : ↥(symplecticGroup l R)
⊢ A⁻¹ * A = 1
have a : (↑(A⁻¹ * A) : Matrix (l ⊕ l) (l ⊕ l) R) = (↑1 : Matrix (l ⊕ l) (l ⊕ l) R)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A_1 : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
A : ↥(symplecticGroup l R)
⊢ (↑(A⁻¹ * A) : Matrix (l ⊕ l) (l ⊕ l) R) = (↑1 : Matrix (l ⊕ l) (l ⊕ l) R)
have a : -(J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R)ᵀ * J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R)) = 1
Tactic: simp only [Submonoid.coe_one, Submonoid.coe_mul, Matrix.neg_mul, coe_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
⊢ (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R (x + y)) =
    HAdd.hAdd (α := TensorAlgebra R M) (β := TensorAlgebra R M)
      ((RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R x) :
        RingQuot (R := FreeAlgebra R M) (Rel R M))
      ((RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R y) :
        RingQuot (R := FreeAlgebra R M) (Rel R M))
have rw : Eq (α := TensorAlgebra R M)
  ((RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R (x + y)) :
    RingQuot (R := FreeAlgebra R M) (Rel R M))
  ((RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M))
      (HAdd.hAdd (α := FreeAlgebra R M) (FreeAlgebra.ι R x) (FreeAlgebra.ι R y)) :
    RingQuot (R := FreeAlgebra R M) (Rel R M))
Tactic: rw [← map_add (RingQuot.mkAlgHom R (Rel R M))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x : M
⊢ (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R (r • x)) =
    HSMul.hSMul (α := R) (β := TensorAlgebra R M) ((RingHom.id R : (a : R) → R) r : R)
      ((RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R x) :
        RingQuot (R := FreeAlgebra R M) (Rel R M))
have rw : Eq (α := TensorAlgebra R M)
  ((RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R (r • x)) :
    RingQuot (R := FreeAlgebra R M) (Rel R M))
  ((RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M))
      (HSMul.hSMul (α := R) (β := FreeAlgebra R M) ((RingHom.id R : (a : R) → R) r : R) (FreeAlgebra.ι R x)) :
    RingQuot (R := FreeAlgebra R M) (Rel R M))
Tactic: rw [← map_smul (RingQuot.mkAlgHom R (Rel R M))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
⊢ Eq (α := RingQuot (R := FreeAlgebra R M) (Rel R M))
    ((RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R m) :
      RingQuot (R := FreeAlgebra R M) (Rel R M))
    ((ι R : (a : M) → TensorAlgebra R M) m : TensorAlgebra R M)
have rw : Eq (α := RingQuot (R := FreeAlgebra R M) (Rel R M))
  ((RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R m) :
    RingQuot (R := FreeAlgebra R M) (Rel R M))
  (({
          toFun := fun (m : M) ↦
            (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R m),
          map_add' := sorry, map_smul' := sorry } :
        (a : M) → TensorAlgebra R M)
      m :
    TensorAlgebra R M)
Tactic: rw [ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
h : Rel R M x y
⊢ Eq.{u_3 + 1} (α := A)
    ((((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A) : FreeAlgebra R M →ₐ[R] A) :
          (a : FreeAlgebra R M) → A)
        x :
      A)
    ((((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A) : FreeAlgebra R M →ₐ[R] A) :
          (a : FreeAlgebra R M) → A)
        y :
      A)
have add : ∀ {a b : M},
  Eq.{u_3 + 1} (α := A)
    ((((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A) : FreeAlgebra R M →ₐ[R] A) :
          (a : FreeAlgebra R M) → A)
        (FreeAlgebra.ι R (a + b)) :
      A)
    ((((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A) : FreeAlgebra R M →ₐ[R] A) :
          (a : FreeAlgebra R M) → A)
        (HAdd.hAdd (α := FreeAlgebra R M) (FreeAlgebra.ι R a) (FreeAlgebra.ι R b)) :
      A)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
h : Rel R M x y
add :
  ∀ {a b : M},
    Eq.{u_3 + 1} (α := A)
      ((((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A) : FreeAlgebra R M →ₐ[R] A) :
            (a : FreeAlgebra R M) → A)
          (FreeAlgebra.ι R (a + b)) :
        A)
      ((((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A) : FreeAlgebra R M →ₐ[R] A) :
            (a : FreeAlgebra R M) → A)
          (HAdd.hAdd (α := FreeAlgebra R M) (FreeAlgebra.ι R a) (FreeAlgebra.ι R b)) :
        A)
⊢ Eq.{u_3 + 1} (α := A)
    ((((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A) : FreeAlgebra R M →ₐ[R] A) :
          (a : FreeAlgebra R M) → A)
        x :
      A)
    ((((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A) : FreeAlgebra R M →ₐ[R] A) :
          (a : FreeAlgebra R M) → A)
        y :
      A)
have smul : ∀ {r : R} {a : M},
  Eq.{u_3 + 1} (α := A)
    ((((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A) : FreeAlgebra R M →ₐ[R] A) :
          (a : FreeAlgebra R M) → A)
        (FreeAlgebra.ι R (r • a)) :
      A)
    ((((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A) : FreeAlgebra R M →ₐ[R] A) :
          (a : FreeAlgebra R M) → A)
        (HMul.hMul (α := FreeAlgebra R M) (β := FreeAlgebra R M)
          ((algebraMap R (FreeAlgebra R M) : (a : R) → FreeAlgebra R M) r : FreeAlgebra R M) (FreeAlgebra.ι R a)) :
      A)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
⊢ (fun (F : TensorAlgebra R M →ₐ[R] A) ↦ F.toLinearMap ∘ₗ ι R)
      (Function.comp (β :=
        { f : FreeAlgebra R M →ₐ[R] A //
          ∀ ⦃x y : FreeAlgebra R M⦄,
            Rel R M x y →
              Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A) ((f : (a : FreeAlgebra R M) → A) y : A) })
        (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
          (a :
              { f : FreeAlgebra R M →ₐ[R] A //
                ∀ ⦃x y : FreeAlgebra R M⦄,
                  Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
            RingQuot (Rel R M) →ₐ[R] A)
        (fun (f : M →ₗ[R] A) ↦
          Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
            ∀ ⦃x y : FreeAlgebra R M⦄,
              Rel R M x y →
                Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A) ((f : (a : FreeAlgebra R M) → A) y : A))
            ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) ⋯)
        f) =
    f
have rw : (fun (F : TensorAlgebra R M →ₐ[R] A) ↦
      (F.toLinearMap ∘ₗ
          {
            toFun := fun (m : M) ↦
              (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R m),
            map_add' := sorry, map_smul' := sorry } :
        M →ₗ[R] A))
    (Function.comp (β :=
      { f : FreeAlgebra R M →ₐ[R] A //
        ∀ ⦃x y : FreeAlgebra R M⦄,
          Rel R M x y →
            Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A) ((f : (a : FreeAlgebra R M) → A) y : A) })
      (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
        (a :
            { f : FreeAlgebra R M →ₐ[R] A //
              ∀ ⦃x y : FreeAlgebra R M⦄,
                Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
          RingQuot (Rel R M) →ₐ[R] A)
      (fun (f : M →ₗ[R] A) ↦
        Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
          ∀ ⦃x y : FreeAlgebra R M⦄,
            Rel R M x y →
              Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A) ((f : (a : FreeAlgebra R M) → A) y : A))
          ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) sorry)
      f) =
  f
Tactic: rw [ι]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
⊢ (fun (F : TensorAlgebra R M →ₐ[R] A) ↦
        (F.toLinearMap ∘ₗ
            {
              toFun := fun (m : M) ↦
                (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R m),
              map_add' := ⋯, map_smul' := ⋯ } :
          M →ₗ[R] A))
      (Function.comp (β :=
        { f : FreeAlgebra R M →ₐ[R] A //
          ∀ ⦃x y : FreeAlgebra R M⦄,
            Rel R M x y →
              Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A) ((f : (a : FreeAlgebra R M) → A) y : A) })
        (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
          (a :
              { f : FreeAlgebra R M →ₐ[R] A //
                ∀ ⦃x y : FreeAlgebra R M⦄,
                  Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
            RingQuot (Rel R M) →ₐ[R] A)
        (fun (f : M →ₗ[R] A) ↦
          Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
            ∀ ⦃x y : FreeAlgebra R M⦄,
              Rel R M x y →
                Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A) ((f : (a : FreeAlgebra R M) → A) y : A))
            ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) ⋯)
        f) =
    f
have h : ∀ (x : M),
  Eq.{u_3 + 1} (α := A)
    (((fun (F : TensorAlgebra R M →ₐ[R] A) ↦
              (F.toLinearMap ∘ₗ
                  {
                    toFun := fun (m : M) ↦
                      (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R m),
                    map_add' := sorry, map_smul' := sorry } :
                M →ₗ[R] A))
            (Function.comp (β :=
              { f : FreeAlgebra R M →ₐ[R] A //
                ∀ ⦃x y : FreeAlgebra R M⦄,
                  Rel R M x y →
                    Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                      ((f : (a : FreeAlgebra R M) → A) y : A) })
              (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
                (a :
                    { f : FreeAlgebra R M →ₐ[R] A //
                      ∀ ⦃x y : FreeAlgebra R M⦄,
                        Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
                  RingQuot (Rel R M) →ₐ[R] A)
              (fun (f : M →ₗ[R] A) ↦
                Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
                  ∀ ⦃x y : FreeAlgebra R M⦄,
                    Rel R M x y →
                      Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                        ((f : (a : FreeAlgebra R M) → A) y : A))
                  ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) sorry)
              f) :
          (a : M) → A)
        x :
      A)
    ((f : (a : M) → A) x : A)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
x : M
| ((f : (a : M) → A) x : A)
have rw : ((AlgHom.toLinearMap ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) ∘ₗ ι R : (a : M) → A) x : A)
Tactic: rw [← ι_comp_lift f]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
x : M
⊢ Eq.{u_3 + 1} (α := A)
    ((((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f : TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) :
      A)
    ((f : (a : M) → A) x : A)
have conv_rhs : Eq.{u_3 + 1} (α := A)
  ((((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f : TensorAlgebra R M →ₐ[R] A) :
        (a : TensorAlgebra R M) → A)
      ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) :
    A)
  ((AlgHom.toLinearMap ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) ∘ₗ ι R : (a : M) → A) x : A)
Tactic: conv_rhs => rw [← ι_comp_lift f]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι R = f ↔ g = (lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f
have rw : g.toLinearMap ∘ₗ ι R = f ↔ (Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) g = f
Tactic: rw [← (lift R).symm_apply_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ (lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (g.toLinearMap ∘ₗ ι R) = g
have rw : (lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A)
    ((Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) g) =
  g
Tactic: rw [← lift_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f g : TensorAlgebra R M →ₐ[R] A
w : f.toLinearMap ∘ₗ ι R = g.toLinearMap ∘ₗ ι R
⊢ f = g
have w₁ : Eq (α := M →ₗ[R] A) ((Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) f : M →ₗ[R] A)
  ((Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) g : M →ₗ[R] A)
Tactic: rw [← lift_symm_apply, ← lift_symm_apply] at w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a : TensorAlgebra R M | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s :=
  LinearMap.codRestrict
    ((Subalgebra.toSubmodule : (a : Subalgebra R (TensorAlgebra R M)) → Submodule R (TensorAlgebra R M)) s)
    (TensorAlgebra.ι R) ι
⊢ C a
have of_apply : ∀ {x : M},
  Eq (α := TensorAlgebra R M) ((↑((of : (a : M) → ↥s) x) : TensorAlgebra R M) : TensorAlgebra R M)
    ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
Tactic: have of_apply {x : M} : of x = (TensorAlgebra.ι R) x := by rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a : TensorAlgebra R M | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s :=
  LinearMap.codRestrict
    ((Subalgebra.toSubmodule : (a : Subalgebra R (TensorAlgebra R M)) → Submodule R (TensorAlgebra R M)) s)
    (TensorAlgebra.ι R) ι
of_apply :
  ∀ {x : M},
    Eq (α := TensorAlgebra R M) ((↑((of : (a : M) → ↥s) x) : TensorAlgebra R M) : TensorAlgebra R M)
      ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
⊢ AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R : (a : M →ₗ[R] ↥s) → TensorAlgebra R M →ₐ[R] ↥s) of)
have w : ∀ (x : M),
  Eq (α := TensorAlgebra R M)
    ((AlgHom.toLinearMap (AlgHom.id R (TensorAlgebra R M)) ∘ₗ TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x :
      TensorAlgebra R M)
    ((AlgHom.toLinearMap (s.val.comp ((lift R : (a : M →ₗ[R] ↥s) → TensorAlgebra R M →ₐ[R] ↥s) of)) ∘ₗ
            TensorAlgebra.ι R :
          (a : M) → TensorAlgebra R M)
        x :
      TensorAlgebra R M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a : TensorAlgebra R M | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s :=
  LinearMap.codRestrict
    ((Subalgebra.toSubmodule : (a : Subalgebra R (TensorAlgebra R M)) → Submodule R (TensorAlgebra R M)) s)
    (TensorAlgebra.ι R) ι
of_apply :
  ∀ {x : M},
    Eq (α := TensorAlgebra R M) ((↑((of : (a : M) → ↥s) x) : TensorAlgebra R M) : TensorAlgebra R M)
      ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
⊢ C a
have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R : (a : M →ₗ[R] ↥s) → TensorAlgebra R M →ₐ[R] ↥s) of)
Tactic: have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp (lift R of) := by
    ext
    simp [of_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a : TensorAlgebra R M | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s :=
  LinearMap.codRestrict
    ((Subalgebra.toSubmodule : (a : Subalgebra R (TensorAlgebra R M)) → Submodule R (TensorAlgebra R M)) s)
    (TensorAlgebra.ι R) ι
of_apply :
  ∀ {x : M},
    Eq (α := TensorAlgebra R M) ((↑((of : (a : M) → ↥s) x) : TensorAlgebra R M) : TensorAlgebra R M)
      ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R : (a : M →ₗ[R] ↥s) → TensorAlgebra R M →ₐ[R] ↥s) of)
⊢ C a
have rw : C
  ((s.val.comp ((lift R : (a : M →ₗ[R] ↥s) → TensorAlgebra R M →ₐ[R] ↥s) of) :
      (a : TensorAlgebra R M) → TensorAlgebra R M)
    a)
Tactic: rw [← AlgHom.id_apply (R := R) a, of_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) ⊤
have refine : ∀ (x : TensorAlgebra R M) (hx : Membership.mem (γ := Subalgebra R (TensorAlgebra R M)) ⊤ x),
  Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) x
Tactic: refine top_unique fun x hx => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : TensorAlgebra R M
⊢ Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) x
have algebraMap : ∀ (r : R),
  Membership.mem (α := TensorAlgebra R M) (γ := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M)))
    ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
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.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : TensorAlgebra R M
algebraMap :
  ∀ (r : R),
    Membership.mem (α := TensorAlgebra R M) (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M)))
      ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
⊢ Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) x
have add : ∀ (x y : TensorAlgebra R M)
  (hx :
    Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) x)
  (hy :
    Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) y),
  Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) (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