awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
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)
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:
simp [of_apply]
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
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)

Tactic:
have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp (lift R of) := by
    ext
    simp [of_apply]
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
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)
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)
⊢ C a

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

Premises used: AlgHom.id_apply
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
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
    ((s.val.comp ((lift R : (a : M →ₗ[R] ↥s) → TensorAlgebra R M →ₐ[R] ↥s) of) :
        (a : TensorAlgebra R M) → TensorAlgebra R M)
      a)

Tactic:
Subtype.prop (lift R of a)

Premises used: Set.Mem, setOf, Subtype.prop, TensorAlgebra.lift, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
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
    ((s.val.comp ((lift R : (a : M →ₗ[R] ↥s) → TensorAlgebra R M →ₐ[R] ↥s) of) :
        (a : TensorAlgebra R M) → TensorAlgebra R M)
      a)

Tactic:
exact Subtype.prop (lift R of a)

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

Tactic:
top_unique fun x hx => ?_

Premises used: top_unique
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
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
⊢ Eq (α := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))) ⊤

Tactic:
refine top_unique fun x hx => ?_

Premises used: top_unique
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
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:
algebraMap_mem _ _

Premises used: Set.Mem, algebraMap_mem
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
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:
exact algebraMap_mem _ _

Premises used: algebraMap_mem
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
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:
add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
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:
exact add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
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:
mul_mem hx hy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
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:
exact mul_mem hx hy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Membership.mem (α := TensorAlgebra R M) (γ := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M)))
    ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)

Tactic:
Algebra.subset_adjoin (Set.mem_range_self _)

Premises used: Set.mem_range_self, Algebra.subset_adjoin
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Membership.mem (α := TensorAlgebra R M) (γ := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M)))
    ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)

Tactic:
exact Algebra.subset_adjoin (Set.mem_range_self _)

Premises used: Set.mem_range_self, Algebra.subset_adjoin
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
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) (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M)))
      ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
add :
  ∀ (x y : TensorAlgebra R M)
    (hx :
      Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M))) x)
    (hy :
      Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M))) y),
    Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M))) (x + y)
mul :
  ∀ (x y : TensorAlgebra R M)
    (hx :
      Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M))) x)
    (hy :
      Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
        (Algebra.adjoin R (Set.range (ι := M) (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M))) y),
    Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M))) (x * y)
ι :
  ∀ (x : M),
    Membership.mem (α := TensorAlgebra R M) (γ := Subalgebra R (TensorAlgebra R M))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M)))
      ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
⊢ Membership.mem (γ := Subalgebra R (TensorAlgebra R M))
    (Algebra.adjoin R (Set.range (ι := M) (⇑(TensorAlgebra.ι R) : (a : M) → TensorAlgebra R M))) 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, Algebra.algebraMap, Algebra.subset_adjoin, TensorAlgebra.ι, algebraMap_mem
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
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
simp_rw :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.map (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) ⊤)
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₁ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.map (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f)
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₂ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Algebra.adjoin R
      (Set.image (α := TensorAlgebra R M)
        (⇑((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f : TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        (Set.range (ι := M) (⇑(ι R) : (a : M) → TensorAlgebra R M))))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₃ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Algebra.adjoin R
      (Set.range.{u_3, u_2 + 1} (ι := M)
        (Function.comp (β := TensorAlgebra R M)
          (⇑((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))))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₄ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Algebra.adjoin R
      (Set.range fun (x : M) ↦
        (((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)))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
⊢ Eq.{u_3 + 1} (α := Subalgebra R A)
    (AlgHom.range (A := TensorAlgebra R M) ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f))
    (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]

Premises used: Set.range_comp, TensorAlgebra.adjoin_range_ι, TensorAlgebra.lift_ι_apply, AlgHom.map_adjoin, Function.comp_def, Algebra.map_top
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : R
⊢ (algebraMapInv : (a : TensorAlgebra R M) → R)
      ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) x : TensorAlgebra R M) =
    x

Tactic:
simp [algebraMapInv]

Premises used: TensorAlgebra.algebraMapInv
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : R
⊢ Eq (α := TensorAlgebra R M) ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) x : TensorAlgebra R M)
      ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) y : TensorAlgebra R M) ↔
    x = y

Tactic:
(algebraMap_leftInverse M).injective.eq_iff

Premises used: Function.LeftInverse.injective, Function.Injective.eq_iff, TensorAlgebra.algebraMap_leftInverse
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : R
⊢ Eq (α := TensorAlgebra R M) ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) x : TensorAlgebra R M)
      (0 : TensorAlgebra R M) ↔
    x = 0

Tactic:
map_eq_zero_iff (algebraMap _ _) (algebraMap_leftInverse _).injective

Premises used: Function.LeftInverse.injective, Algebra.algebraMap, map_eq_zero_iff, TensorAlgebra.algebraMap_leftInverse
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : R
⊢ Eq (α := TensorAlgebra R M) ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) x : TensorAlgebra R M)
      (1 : TensorAlgebra R M) ↔
    x = 1

Tactic:
map_eq_one_iff (algebraMap _ _) (algebraMap_leftInverse _).injective

Premises used: Function.LeftInverse.injective, Algebra.algebraMap, map_eq_one_iff, TensorAlgebra.algebraMap_leftInverse
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
⊢ Nontrivial (TensorAlgebra R M)

Tactic:
(algebraMap_leftInverse M).injective.nontrivial

Premises used: Function.LeftInverse.injective, Function.Injective.nontrivial, TensorAlgebra.algebraMap_leftInverse
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
⊢ Eq (α := TrivSqZeroExt R M)
    ((toTrivSqZeroExt : (a : TensorAlgebra R M) → TrivSqZeroExt R M) ((ι R : (a : M) → TensorAlgebra R M) x) :
      TrivSqZeroExt R M)
    (TrivSqZeroExt.inr x : TrivSqZeroExt R M)

Tactic:
lift_ι_apply _ _

Premises used: TrivSqZeroExt.inr, TensorAlgebra.lift_ι_apply
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
this : Module.{u_1, u_2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
⊢ IsCentralScalar R M

Tactic:
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
this_1 : Module.{u_1, u_2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R M
⊢ TensorAlgebra R M →ₗ[R] M

Tactic:
exact (TrivSqZeroExt.sndHom R M).comp toTrivSqZeroExt.toLinearMap

Premises used: AlgHom.toLinearMap, LinearMap.comp, TrivSqZeroExt.sndHom, TensorAlgebra.toTrivSqZeroExt
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ (ιInv : (a : TensorAlgebra R M) → M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) = x

Tactic:
simp [ιInv]

Premises used: TensorAlgebra.ιInv
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
⊢ Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
      ((ι R : (a : M) → TensorAlgebra R M) y : TensorAlgebra R M) ↔
    x = y

Tactic:
ι_leftInverse.injective.eq_iff

Premises used: Function.LeftInverse.injective, Function.Injective.eq_iff, TensorAlgebra.ι_leftInverse
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
rw :
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) (0 : TensorAlgebra R M) ↔
    Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
      ((ι R : (a : M) → TensorAlgebra R M) 0 : TensorAlgebra R M)
rw₁ rw₂ :
  Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) (0 : TensorAlgebra R M) ↔
    Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) (0 : TensorAlgebra R M)
⊢ Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) (0 : TensorAlgebra R M) ↔
    x = 0

Tactic:
rw [← ι_inj R x 0, map_zero]

Premises used: map_zero, TensorAlgebra.ι_inj, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
r : R
⊢ Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
      ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M) ↔
    x = 0 ∧ r = 0

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
r : R
refine_1 :
  ∀
    (h :
      Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
        ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)),
    x = 0 ∧ r = 0
refine_2 :
  x = 0 ∧ r = 0 →
    Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
      ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M)
⊢ Eq (α := TensorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
      ((algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r : TensorAlgebra R M) ↔
    x = 0 ∧ r = 0

Tactic:
refine ⟨fun h => ?_, ?_⟩