awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
rw :
  Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) Aᵀ ↔
    Aᵀ * J l R * A = J l R
rw₁ : Aᵀ * J l R * Aᵀᵀ = J l R ↔ Aᵀ * J l R * A = J l R
rw₂ rw₃ : Aᵀ * J l R * A = J l R ↔ Aᵀ * J l R * A = J l R
⊢ Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A ↔
    Aᵀ * J l R * A = J l R

Tactic:
rw [← transpose_mem_iff, mem_iff, transpose_transpose]

Premises used: SymplecticGroup.transpose_mem_iff, Matrix.transpose_transpose, SymplecticGroup.mem_iff
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
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) = -J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R)ᵀ * J l R

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
⊢ -(J l R * Aᵀ * J l R * A) = -J l R * (Aᵀ * J l R * A)

Tactic:
simp only [Matrix.mul_assoc, Matrix.neg_mul]

Premises used: Matrix.mul_assoc, Matrix.neg_mul
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
⊢ Aᵀ * J l R * A = J l R

Tactic:
rw [mem_iff'] at hA

Premises used: SymplecticGroup.mem_iff'
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Aᵀ * J l R * A = J l R
rw rw₁ : -J l R * J l R = -J l R * J l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R

Tactic:
rw [hA]
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
⊢ -J l R * J l R = HSMul.hSMul (α := R) (-1) (J l R * J l R)

Tactic:
simp only [Matrix.neg_mul, neg_smul, one_smul]

Premises used: neg_smul, one_smul, Matrix.neg_mul
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
rw rw₁ :
  HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (-1) (-1) =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (-1) (-1)
⊢ HSMul.hSMul (α := R) (-1) (J l R * J l R) =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (-1) (-1)

Tactic:
rw [J_squared]

Premises used: Matrix.J_squared
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
⊢ HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (-1) (-1) = 1

Tactic:
simp only [neg_smul_neg, one_smul]

Premises used: neg_smul_neg, one_smul
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
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)⁻¹

Tactic:
(coe_inv A).trans (inv_eq_left_inv ?_).symm

Premises used: SymplecticGroup.coe_inv, Matrix.inv_eq_left_inv, Eq.symm, Eq.trans
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : ↥(symplecticGroup l R)
refine : -J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R)ᵀ * J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R) = 1
⊢ (↑A⁻¹ : Matrix (l ⊕ l) (l ⊕ l) R) = (↑A : Matrix (l ⊕ l) (l ⊕ l) R)⁻¹

Tactic:
refine (coe_inv A).trans (inv_eq_left_inv ?_).symm

Premises used: SymplecticGroup.coe_inv, Matrix.inv_eq_left_inv, Eq.symm, Eq.trans
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : ↥(symplecticGroup l R)
⊢ -J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R)ᵀ * J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R) = 1

Tactic:
simp [inv_left_mul_aux]

Premises used: SymplecticGroup.inv_left_mul_aux
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
⊢ -J l R * Aᵀ * J l R * A = 1

Tactic:
simp only [Matrix.neg_mul, inv_left_mul_aux hA]

Premises used: SymplecticGroup.inv_left_mul_aux, Matrix.neg_mul
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
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⁻¹ * A) : Matrix (l ⊕ l) (l ⊕ l) R) = (↑1 : Matrix (l ⊕ l) (l ⊕ l) R)
⊢ A⁻¹ * A = 1

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
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 : -(J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R)ᵀ * J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R)) = 1
⊢ (↑(A⁻¹ * A) : Matrix (l ⊕ l) (l ⊕ l) R) = (↑1 : Matrix (l ⊕ l) (l ⊕ l) R)

Tactic:
simp only [Submonoid.coe_one, Submonoid.coe_mul, Matrix.neg_mul, coe_inv]

Premises used: SymplecticGroup.coe_inv, Submonoid.coe_one, Matrix.neg_mul, Submonoid.coe_mul
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
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)
⊢ -(J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R)ᵀ * J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R)) = 1

Tactic:
inv_left_mul_aux A.2

Premises used: SymplecticGroup.inv_left_mul_aux, Subtype.property
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
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)
⊢ -(J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R)ᵀ * J l R * (↑A : Matrix (l ⊕ l) (l ⊕ l) R)) = 1

Tactic:
exact inv_left_mul_aux A.2

Premises used: SymplecticGroup.inv_left_mul_aux, Subtype.property
-- 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 (α := Algebra ℕ (TensorAlgebra R M)) Semiring.toNatAlgebra instAlgebra

Tactic:
rfl

Premises used: RingQuot.smul, instSemiringTensorAlgebra._aux_7, TensorAlgebra, instSemiringTensorAlgebra._aux_2, instSemiringTensorAlgebra._aux_1, RingQuot.natCast, instSemiringTensorAlgebra._aux_6, rfl
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 : Type u_2
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
R : Type u_3
S : Type u_4
A : Type u_5
M : Type u_6
inst_3 : CommSemiring R
inst_4 : CommSemiring S
inst_5 : AddCommMonoid M
inst_6 : CommSemiring A
inst_7 : Algebra R A
inst_8 : Algebra S A
inst_9 : Module R M
inst_10 : Module S M
inst_11 : Module A M
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower S A M
⊢ SMulCommClass R S (TensorAlgebra A M)

Tactic:
inferInstanceAs <| SMulCommClass R S (RingQuot _)

Premises used: _private.0.instSMulCommClassTensorAlgebra._proof_1
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 : Type u_2
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
R : Type u_3
S : Type u_4
A : Type u_5
M : Type u_6
inst_3 : CommSemiring R
inst_4 : CommSemiring S
inst_5 : AddCommMonoid M
inst_6 : CommSemiring A
inst_7 : SMul R S
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : Module R M
inst_11 : Module S M
inst_12 : Module A M
inst_13 : IsScalarTower R A M
inst_14 : IsScalarTower S A M
inst_15 : IsScalarTower R S A
⊢ IsScalarTower R S (TensorAlgebra A M)

Tactic:
inferInstanceAs <| IsScalarTower R S (RingQuot _)

Premises used: _private.0.instIsScalarTowerTensorAlgebra._proof_1
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M_1 : Type u_2
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
S M : Type
inst_3 : CommRing S
inst_4 : AddCommGroup M
inst_5 : Module S M
⊢ Eq (α := Algebra ℤ (TensorAlgebra S M)) (Ring.toIntAlgebra (TensorAlgebra S M)) instAlgebra

Tactic:
rfl

Premises used: RingQuot.smul, RingQuot.intCast, instSemiringTensorAlgebra._aux_7, TensorAlgebra, instSemiringTensorAlgebra._aux_2, instSemiringTensorAlgebra._aux_1, instSemiringTensorAlgebra._aux_6, 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
x y : M
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))
⊢ (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))

Tactic:
rw [← map_add (RingQuot.mkAlgHom R (Rel R M))]

Premises used: map_add, RingQuot.mkAlgHom, TensorAlgebra.Rel
-- 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)
    ((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:
RingQuot.mkAlgHom_rel R Rel.add

Premises used: TensorAlgebra, TensorAlgebra.Rel.add, RingQuot.mkAlgHom_rel
-- 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)
    ((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:
exact RingQuot.mkAlgHom_rel R Rel.add

Premises used: TensorAlgebra.Rel.add, RingQuot.mkAlgHom_rel
-- 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
x : M
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))
⊢ (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))

Tactic:
rw [← map_smul (RingQuot.mkAlgHom R (Rel R M))]

Premises used: RingQuot.mkAlgHom, TensorAlgebra.Rel, map_smul
-- 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
x : M
⊢ 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:
RingQuot.mkAlgHom_rel R Rel.smul

Premises used: TensorAlgebra.Rel.smul, TensorAlgebra, RingQuot.mkAlgHom_rel
-- 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
x : M
⊢ 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:
exact RingQuot.mkAlgHom_rel R Rel.smul

Premises used: TensorAlgebra.Rel.smul, RingQuot.mkAlgHom_rel
-- 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
m : M
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' := ⋯, map_smul' := ⋯ } :
          (a : M) → TensorAlgebra R M)
        m :
      TensorAlgebra R 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)

Tactic:
rw [ι]

Premises used: TensorAlgebra.ι
-- 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
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))
    (({
            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' := ⋯ } :
          (a : M) → TensorAlgebra R M)
        m :
      TensorAlgebra R M)

Tactic:
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
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)
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)
⊢ 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)

Tactic:
induction h
-- 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
x y : FreeAlgebra R M
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:
simp only [Algebra.smul_def, FreeAlgebra.lift_ι_apply, map_smulₛₗ, RingHom.id_apply,
              map_mul, AlgHom.commutes, map_add]

Premises used: RingHom.id_apply, FreeAlgebra.lift_ι_apply, map_add, MulActionSemiHomClass.map_smulₛₗ, map_mul, AlgHom.commutes, Algebra.smul_def
-- 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
x y : FreeAlgebra R M
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:
simp only [Algebra.smul_def, FreeAlgebra.lift_ι_apply, map_smulₛₗ, RingHom.id_apply,
              map_mul, AlgHom.commutes, map_add]

Premises used: RingHom.id_apply, FreeAlgebra.lift_ι_apply, map_add, MulActionSemiHomClass.map_smulₛₗ, map_mul, AlgHom.commutes, Algebra.smul_def
-- 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
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' := ⋯, 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
⊢ (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

Tactic:
rw [ι]

Premises used: TensorAlgebra.ι