-- Mathlib/LinearAlgebra/FreeProduct/Basic.lean
theorem lift_unique
    (f : FreeProduct R A →ₐ[R] B) (h : ∀ i, f ∘ₐ ι R A i = maps) :
    f = lift R A maps

Proof state:
case w.w.H.h
I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
f : FreeProduct R A →ₐ[R] B
i : I
a : A i
h : ∀ (i : I) (x : A i), (f ∘ₐ ι R A i) x = maps x
⊢ (((f ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a =
    (((((lift R A) fun {i} => maps) ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ
        DirectSum.lof R I A i)
      a

Tactic:
specialize h i a

Result:
case w.w.H.h
I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
f : FreeProduct R A →ₐ[R] B
i : I
a : A i
h : (f ∘ₐ ι R A i) a = maps a
⊢ (((f ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a =
    (((((lift R A) fun {i} => maps) ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ
        DirectSum.lof R I A i)
      a

Proof state:
case w.w.H.h
I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
f : FreeProduct R A →ₐ[R] B
i : I
a : A i
h : (f ∘ₐ ι R A i) a = maps a
⊢ (((f ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a =
    (((((lift R A) fun {i} => maps) ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ
        DirectSum.lof R I A i)
      a

Tactic:
simp [h.symm, ι]

Result:
no goals

Proof state:
case w.w.H.h
I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
f : FreeProduct R A →ₐ[R] B
h : ∀ (i : I), f ∘ₐ ι R A i = maps
i : I
a : A i
⊢ (((f ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a =
    (((((lift R A) fun {i} => maps) ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ
        DirectSum.lof R I A i)
      a

Tactic:
simp_rw [AlgHom.ext_iff] at h

Result:
case w.w.H.h
I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
f : FreeProduct R A →ₐ[R] B
i : I
a : A i
h : ∀ (i : I) (x : A i), (f ∘ₐ ι R A i) x = maps x
⊢ (((f ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a =
    (((((lift R A) fun {i} => maps) ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ
        DirectSum.lof R I A i)
      a

Proof state:
I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
f : FreeProduct R A →ₐ[R] B
h : ∀ (i : I), f ∘ₐ ι R A i = maps
⊢ f = (lift R A) fun {i} => maps

Tactic:
ext i a

Result:
case w.w.H.h
I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
f : FreeProduct R A →ₐ[R] B
h : ∀ (i : I), f ∘ₐ ι R A i = maps
i : I
a : A i
⊢ (((f ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a =
    (((((lift R A) fun {i} => maps) ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ
        DirectSum.lof R I A i)
      a