case h
R : Type u_3
inst✝² : CommSemiring R
X : Type u_1
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ (↑(↑(lift R) f) ∘ ι R) x✝ = f x✝
R : Type u_3
inst✝² : CommSemiring R
X : Type u_1
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ ↑(↑(lift R) f) ∘ ι R = f
ext
case h
R : Type u_3
inst✝² : CommSemiring R
X : Type u_1
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ ↑(↑{ 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) }
          f)
      (Quot.mk (Rel R X) (Pre.of x✝)) =
    f x✝
case h
R : Type u_3
inst✝² : CommSemiring R
X : Type u_1
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ (↑(↑(lift R) f) ∘ ι R) x✝ = f x✝
rw [Function.comp_apply, ι_def, lift]
no goals
case h
R : Type u_3
inst✝² : CommSemiring R
X : Type u_1
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ ↑(↑{ 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) }
          f)
      (Quot.mk (Rel R X) (Pre.of x✝)) =
    f x✝
rfl