R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
g : FreeAlgebra R X →ₐ[R] A
⊢ ↑g ∘ ι R = f ↔
    ↑{ toFun := FreeAlgebra.liftAux R, invFun := fun F => ↑F ∘ ι R,
              left_inv := (_ : ∀ (f : X → A), (fun F => ↑F ∘ ι R) (FreeAlgebra.liftAux R f) = f),
              right_inv :=
                (_ : ∀ (F : FreeAlgebra R X →ₐ[R] A), FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F) = F) }.symm
        g =
      f
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
g : FreeAlgebra R X →ₐ[R] A
⊢ ↑g ∘ ι R = f ↔ g = ↑(lift R) f
rw [← (lift R).symm_apply_eq, lift]
no goals
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
g : FreeAlgebra R X →ₐ[R] A
⊢ ↑g ∘ ι R = f ↔
    ↑{ toFun := FreeAlgebra.liftAux R, invFun := fun F => ↑F ∘ ι R,
              left_inv := (_ : ∀ (f : X → A), (fun F => ↑F ∘ ι R) (FreeAlgebra.liftAux R f) = f),
              right_inv :=
                (_ : ∀ (F : FreeAlgebra R X →ₐ[R] A), FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F) = F) }.symm
        g =
      f
rfl