-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
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
x y : FreeTensorAlgebra R A
r : rel R A x y
id :
  ∀ {i : 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 : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (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)
⊢ 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)
        x :
      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)
        y :
      B)
have prod : ∀ {i : I} {a₁ a₂ : A 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)
        ((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 : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₁
          | 1 => ((DirectSum.lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (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 : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) (a₁ * a₂)) :
          TensorAlgebra R (⨁ (i : I), A i)) :
      B)
Tactic: cases r with
          | id => simp
          | prod => simp
Cleared hypotheses: x, y, r