awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u
inst : CommSemiring R
A B : Type v
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A ≃ₐ[R] B
rel : A → A → Prop
b : B
⊢ Eq (α := RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
    ((AlgHom.comp (B := RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
            (AlgHom.comp (B := RingQuot rel)
              ((liftAlgHom R (s := rel) :
                  (a :
                      { f_1 : A →ₐ[R] RingQuot (rel on (⇑f.symm : (a : B) → A)) //
                        ∀ ⦃x y : A⦄,
                          rel x y →
                            (f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) x =
                              (f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) y }) →
                    RingQuot rel →ₐ[R] RingQuot (rel on (⇑f.symm : (a : B) → A)))
                (Subtype.mk (p := fun (f_1 : A →ₐ[R] RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A))) ↦
                  ∀ ⦃x y : A⦄,
                    rel x y →
                      Eq (α := RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
                        ((f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) x :
                          RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
                        ((f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) y :
                          RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A))))
                  (AlgHom.comp (mkAlgHom R (rel on (⇑f.symm : (a : B) → A))) (↑f : A →ₐ[R] B)) ⋯))
              ((liftAlgHom R (s := rel on (⇑f.symm : (a : B) → A)) :
                  (a :
                      { f_1 : B →ₐ[R] RingQuot rel //
                        ∀ ⦃x y : B⦄,
                          (rel on (⇑f.symm : (a : B) → A)) x y →
                            (f_1 : (a : B) → RingQuot rel) x = (f_1 : (a : B) → RingQuot rel) y }) →
                    RingQuot (rel on (⇑f.symm : (a : B) → A)) →ₐ[R] RingQuot rel)
                (Subtype.mk (p := fun (f_1 : B →ₐ[R] RingQuot rel) ↦
                  ∀ ⦃x y : B⦄,
                    (rel on (⇑f.symm : (a : B) → A)) x y →
                      Eq (α := RingQuot rel) ((f_1 : (a : B) → RingQuot rel) x : RingQuot rel)
                        ((f_1 : (a : B) → RingQuot rel) y : RingQuot rel))
                  (AlgHom.comp (mkAlgHom R rel) (↑f.symm : B →ₐ[R] A)) ⋯)))
            (mkAlgHom R (rel on (⇑f.symm : (a : B) → A))) :
          (a : B) → RingQuot (rel on (⇑f.symm : (a : B) → A)))
        b :
      RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
    ((AlgHom.comp (AlgHom.id R (RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A))))
            (mkAlgHom R (rel on (⇑f.symm : (a : B) → A))) :
          (a : B) → RingQuot (rel on (⇑f.symm : (a : B) → A)))
        b :
      RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u
inst : CommSemiring R
A B : Type v
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A ≃ₐ[R] B
rel : A → A → Prop
a : A
⊢ Eq (α := RingQuot rel)
    ((AlgHom.comp
            (AlgHom.comp (B := RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
              ((liftAlgHom R (s := rel on (⇑f.symm : (a : B) → A)) :
                  (a :
                      { f_1 : B →ₐ[R] RingQuot rel //
                        ∀ ⦃x y : B⦄,
                          (rel on (⇑f.symm : (a : B) → A)) x y →
                            (f_1 : (a : B) → RingQuot rel) x = (f_1 : (a : B) → RingQuot rel) y }) →
                    RingQuot (rel on (⇑f.symm : (a : B) → A)) →ₐ[R] RingQuot rel)
                (Subtype.mk (p := fun (f_1 : B →ₐ[R] RingQuot rel) ↦
                  ∀ ⦃x y : B⦄,
                    (rel on (⇑f.symm : (a : B) → A)) x y →
                      Eq (α := RingQuot rel) ((f_1 : (a : B) → RingQuot rel) x : RingQuot rel)
                        ((f_1 : (a : B) → RingQuot rel) y : RingQuot rel))
                  (AlgHom.comp (mkAlgHom R rel) (↑f.symm : B →ₐ[R] A)) ⋯))
              ((liftAlgHom R (s := rel) :
                  (a :
                      { f_1 : A →ₐ[R] RingQuot (rel on (⇑f.symm : (a : B) → A)) //
                        ∀ ⦃x y : A⦄,
                          rel x y →
                            (f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) x =
                              (f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) y }) →
                    RingQuot rel →ₐ[R] RingQuot (rel on (⇑f.symm : (a : B) → A)))
                (Subtype.mk (p := fun (f_1 : A →ₐ[R] RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A))) ↦
                  ∀ ⦃x y : A⦄,
                    rel x y →
                      Eq (α := RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
                        ((f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) x :
                          RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
                        ((f_1 : (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A))) y :
                          RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A))))
                  (AlgHom.comp (mkAlgHom R (rel on (⇑f.symm : (a : B) → A))) (↑f : A →ₐ[R] B)) ⋯)))
            (mkAlgHom R rel) :
          (a : A) → RingQuot rel)
        a :
      RingQuot rel)
    ((AlgHom.comp (AlgHom.id R (RingQuot rel)) (mkAlgHom R rel) : (a : A) → RingQuot rel) a : RingQuot rel)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
A B : Type v
inst : Semiring A
inst_1 : Semiring B
f : A ≃+* B
rel : A → A → Prop
n : ℕ
⊢ Eq (α := B) ((f : (a : A) → B) ((algebraMap ℕ A : (a : ℕ) → A) n : A) : B) ((algebraMap ℕ B : (a : ℕ) → B) n : B)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps : {i : I} → AlgHom.{v, w, w'} R (A i) B
⊢ Module R (⨁ (i : I), A i)

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
i : I
⊢ rel R A
    ((ι R : (a : ⨁ (i : I), A i) → TensorAlgebra R (⨁ (i : I), A i))
      (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) 1))
    1

Tactic:
rel.id

Premises used: LinearAlgebra.FreeProduct.rel.id
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps : {i : I} → AlgHom.{v, w, w'} R (A i) B
⊢ Semiring (FreeProduct R A)

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps : {i : I} → AlgHom.{v, w, w'} R (A i) B
⊢ Algebra R (FreeProduct R A)

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
x : ⨁ (i : I), A i
⊢ Eq (α := FreeProduct R A)
    (RingQuot.mk (r := rel R A)
      (Quot.mk (RingQuot.Rel (rel R A)) ((ι R : (a : ⨁ (i : I), A i) → TensorAlgebra R (⨁ (i : I), A i)) x)))
    ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A) x)

Tactic:
aesop (add simp [ι', mkAlgHom, RingQuot.mkAlgHom, mkRingHom])

Premises used: LinearAlgebra.FreeProduct.mkAlgHom, LinearAlgebra.FreeProduct.ι', RingQuot.mkAlgHom, RingQuot.mkRingHom
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
i : I
this :
  Eq (α := FreeProduct R A)
    ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
        (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) 1) :
      FreeProduct R A)
    ((mkAlgHom R A : (a : FreeTensorAlgebra R A) → FreeProduct R A) 1 : FreeProduct R A)
⊢ Eq (α := FreeProduct R A)
    ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
        (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) 1) :
      FreeProduct R A)
    (1 : FreeProduct R A)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
i : I
suffices :
  Eq (α := FreeProduct R A)
    ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
        (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) 1) :
      FreeProduct R A)
    ((mkAlgHom R A : (a : FreeTensorAlgebra R A) → FreeProduct R A) 1 : FreeProduct R A)
⊢ Eq (α := FreeProduct R A)
    ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
        (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) 1) :
      FreeProduct R A)
    (1 : FreeProduct R A)

Tactic:
suffices ι' R A (DirectSum.lof R I A i 1) = mkAlgHom R A 1 by simpa
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
i : I
⊢ Eq (α := FreeProduct R A)
    ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
        (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) 1) :
      FreeProduct R A)
    ((mkAlgHom R A : (a : FreeTensorAlgebra R A) → FreeProduct R A) 1 : FreeProduct R A)

Tactic:
RingQuot.mkAlgHom_rel R <| rel_id R A (i := i)

Premises used: LinearAlgebra.FreeProduct.rel_id, RingQuot.mkAlgHom_rel
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
i : I
⊢ Eq (α := FreeProduct R A)
    ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
        (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) 1) :
      FreeProduct R A)
    ((mkAlgHom R A : (a : FreeTensorAlgebra R A) → FreeProduct R A) 1 : FreeProduct R A)

Tactic:
exact RingQuot.mkAlgHom_rel R <| rel_id R A (i := i)

Premises used: LinearAlgebra.FreeProduct.rel_id, RingQuot.mkAlgHom_rel
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
a₁ a₂ : A i
⊢ Eq (α := RingQuot (R := TensorAlgebra R (⨁ (i : I), A i)) (rel R A))
    ((RingQuot.mkAlgHom R (rel R A) : (a : TensorAlgebra R (⨁ (i : I), A i)) → RingQuot (rel R A))
        ((tprod R (⨁ (i : I), A i) 2 : (a : (i : Fin 2) → ⨁ (i : I), A i) → TensorAlgebra R (⨁ (i : I), A i))
          fun (x : Fin 2) ↦
          match (motive := Fin 2 → ⨁ (i : I), A i) x with
          | 0 => ((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₁
          | 1 => ((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₂) :
      RingQuot (R := TensorAlgebra R (⨁ (i : I), A i)) (rel R A))
    ((RingQuot.mkAlgHom R (rel R A) : (a : TensorAlgebra R (⨁ (i : I), A i)) → RingQuot (rel R A))
        ((ι R : (a : ⨁ (i : I), A i) → TensorAlgebra R (⨁ (i : I), A i))
          (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) (a₁ * a₂))) :
      RingQuot (R := TensorAlgebra R (⨁ (i : I), A i)) (rel R A))

Tactic:
RingQuot.mkAlgHom_rel R <| rel.prod

Premises used: LinearAlgebra.FreeProduct.rel.prod, RingQuot.mkAlgHom_rel
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
a₁ a₂ : A i
h :
  HMul.hMul (α := FreeProduct R A) (β := FreeProduct R A)
      ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
          (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₁) :
        FreeProduct R A)
      ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
          (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₂) :
        FreeProduct R A) =
    (RingQuot.mkAlgHom R (rel R A) : (a : TensorAlgebra R (⨁ (i : I), A i)) → RingQuot (rel R A))
      ((tprod R (⨁ (i : I), A i) 2 : (a : (i : Fin 2) → ⨁ (i : I), A i) → TensorAlgebra R (⨁ (i : I), A i))
        fun (x : Fin 2) ↦
        match (motive := Fin 2 → ⨁ (i : I), A i) x with
        | 0 => ((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₁
        | 1 => ((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₂)
⊢ HMul.hMul (α := FreeProduct R A) (β := FreeProduct R A)
      ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
          (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₁) :
        FreeProduct R A)
      ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
          (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₂) :
        FreeProduct R A) =
    (ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
      (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) (a₁ * a₂))

Tactic:
convert! RingQuot.mkAlgHom_rel R <| rel.prod

Premises used: LinearAlgebra.FreeProduct.rel.prod, RingQuot.mkAlgHom_rel
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
a₁ a₂ : A i
⊢ HMul.hMul (α := FreeProduct R A) (β := FreeProduct R A)
      ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
          (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₁) :
        FreeProduct R A)
      ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
          (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₂) :
        FreeProduct R A) =
    (RingQuot.mkAlgHom R (rel R A) : (a : TensorAlgebra R (⨁ (i : I), A i)) → RingQuot (rel R A))
      ((tprod R (⨁ (i : I), A i) 2 : (a : (i : Fin 2) → ⨁ (i : I), A i) → TensorAlgebra R (⨁ (i : I), A i))
        fun (x : Fin 2) ↦
        match (motive := Fin 2 → ⨁ (i : I), A i) x with
        | 0 => ((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₁
        | 1 => ((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
i : I
⊢ Eq (α := FreeProduct R A)
    ((RingQuot.mkAlgHom R (rel R A) : (a : FreeTensorAlgebra R A) → FreeProduct R A)
        ((ι R : (a : ⨁ (i : I), A i) → FreeTensorAlgebra R A)
          (((DirectSum.lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) 1)) :
      FreeProduct R A)
    (1 : FreeProduct R A)

Tactic:
identify_one R A i

Premises used: LinearAlgebra.FreeProduct.identify_one
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
i : I
⊢ Eq (α := FreeProduct R A)
    ((RingQuot.mkAlgHom R (rel R A) : (a : FreeTensorAlgebra R A) → FreeProduct R A)
        ((ι R : (a : ⨁ (i : I), A i) → FreeTensorAlgebra R A)
          (((DirectSum.lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) 1)) :
      FreeProduct R A)
    (1 : FreeProduct R A)

Tactic:
exact identify_one R A i

Premises used: LinearAlgebra.FreeProduct.identify_one
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps_1 maps : {i : I} → AlgHom.{v, w, w'} R (A i) B
i_1 : I
⊢ Eq.{w' + 1} (α := B)
    ((((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
              (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps) :
            TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B) :
          (a : FreeTensorAlgebra R A) → B)
        ((TensorAlgebra.ι R : (a : ⨁ (i : I), A i) → TensorAlgebra R (⨁ (i : I), A i))
          (((DirectSum.lof R I A i_1 : A i_1 →ₗ[R] ⨁ (i : I), A i) : (a : A i_1) → ⨁ (i : I), A i) 1)) :
      B)
    ((((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
              (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps) :
            TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B) :
          (a : FreeTensorAlgebra R A) → B)
        1 :
      B)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps_1 maps : {i : I} → AlgHom.{v, w, w'} R (A i) B
i_1 : I
a₁ a₂ : A i_1
⊢ Eq.{w' + 1} (α := B)
    ((((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
              (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps) :
            TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B) :
          (a : FreeTensorAlgebra R A) → B)
        ((tprod R (⨁ (i : I), A i) 2 : (a : (i : Fin 2) → ⨁ (i : I), A i) → TensorAlgebra R (⨁ (i : I), A i))
          fun (x : Fin 2) ↦
          match (motive := Fin 2 → ⨁ (i : I), A i) x with
          | 0 => ((DirectSum.lof R I A i_1 : A i_1 →ₗ[R] ⨁ (i : I), A i) : (a : A i_1) → ⨁ (i : I), A i) a₁
          | 1 => ((DirectSum.lof R I A i_1 : A i_1 →ₗ[R] ⨁ (i : I), A i) : (a : A i_1) → ⨁ (i : I), A i) a₂) :
      B)
    ((((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
              (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps) :
            TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B) :
          (a : FreeTensorAlgebra R A) → B)
        ((TensorAlgebra.ι R : (a : ⨁ (i : I), A i) → TensorAlgebra R (⨁ (i : I), A i))
            (((DirectSum.lof R I A i_1 : A i_1 →ₗ[R] ⨁ (i : I), A i) : (a : A i_1) → ⨁ (i : I), A i) (a₁ * a₂)) :
          TensorAlgebra R (⨁ (i : I), A i)) :
      B)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps π : {i : I} → AlgHom.{v, w, w'} R (A i) B
h :
  ∀ (i : I) (aᵢ : A i),
    Eq.{w' + 1} (α := B)
      (((fun (π : FreeProduct R A →ₐ[R] B) (i : I) ↦ π ∘ₐ ι R A i)
              ((fun (maps : {i : I} → AlgHom.{v, w, w'} R (A i) B) ↦
                  ((liftAlgHom R (s := rel R A) :
                        (a :
                            { f : FreeTensorAlgebra R A →ₐ[R] B //
                              ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                                rel R A x y →
                                  (f : (a : FreeTensorAlgebra R A) → B) x = (f : (a : FreeTensorAlgebra R A) → B) y }) →
                          RingQuot (rel R A) →ₐ[R] B)
                      (Subtype.mk (p := fun (f : FreeTensorAlgebra R A →ₐ[R] B) ↦
                        ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                          rel R A x y →
                            Eq.{w' + 1} (α := B) ((f : (a : FreeTensorAlgebra R A) → B) x : B)
                              ((f : (a : FreeTensorAlgebra R A) → B) y : B))
                        ((TensorAlgebra.lift R :
                            (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
                          (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps))
                        ⋯) :
                    RingQuot (R := FreeTensorAlgebra R A) (rel R A) →ₐ[R] B))
                @π)
              i :
            (a : A i) → B)
          aᵢ :
        B)
      ((π : (a : A i) → B) aᵢ : B)
⊢ (fun (π : FreeProduct R A →ₐ[R] B) (i : I) ↦ π ∘ₐ ι R A i)
      ((fun (maps : {i : I} → AlgHom.{v, w, w'} R (A i) B) ↦
          ((liftAlgHom R (s := rel R A) :
                (a :
                    { f : FreeTensorAlgebra R A →ₐ[R] B //
                      ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                        rel R A x y →
                          (f : (a : FreeTensorAlgebra R A) → B) x = (f : (a : FreeTensorAlgebra R A) → B) y }) →
                  RingQuot (rel R A) →ₐ[R] B)
              (Subtype.mk (p := fun (f : FreeTensorAlgebra R A →ₐ[R] B) ↦
                ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                  rel R A x y →
                    Eq.{w' + 1} (α := B) ((f : (a : FreeTensorAlgebra R A) → B) x : B)
                      ((f : (a : FreeTensorAlgebra R A) → B) y : B))
                ((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
                  (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps))
                ⋯) :
            RingQuot (R := FreeTensorAlgebra R A) (rel R A) →ₐ[R] B))
        @π) =
    @π

Tactic:
ext i aᵢ
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
i_1 : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps π : {i : I} → AlgHom.{v, w, w'} R (A i) B
i : I
aᵢ : A i
⊢ Eq.{w' + 1} (α := B)
    (((fun (π : FreeProduct R A →ₐ[R] B) (i : I) ↦ π ∘ₐ ι R A i)
            ((fun (maps : {i : I} → AlgHom.{v, w, w'} R (A i) B) ↦
                ((liftAlgHom R (s := rel R A) :
                      (a :
                          { f : FreeTensorAlgebra R A →ₐ[R] B //
                            ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                              rel R A x y →
                                (f : (a : FreeTensorAlgebra R A) → B) x = (f : (a : FreeTensorAlgebra R A) → B) y }) →
                        RingQuot (rel R A) →ₐ[R] B)
                    (Subtype.mk (p := fun (f : FreeTensorAlgebra R A →ₐ[R] B) ↦
                      ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                        rel R A x y →
                          Eq.{w' + 1} (α := B) ((f : (a : FreeTensorAlgebra R A) → B) x : B)
                            ((f : (a : FreeTensorAlgebra R A) → B) y : B))
                      ((TensorAlgebra.lift R :
                          (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
                        (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps))
                      ⋯) :
                  RingQuot (R := FreeTensorAlgebra R A) (rel R A) →ₐ[R] B))
              @π)
            i :
          (a : A i) → B)
        aᵢ :
      B)
    ((π : (a : A i) → B) aᵢ : B)

Tactic:
aesop (add simp [ι, ι'])

Premises used: LinearAlgebra.FreeProduct.ι', LinearAlgebra.FreeProduct.ι