[GOAL]
R : Type u
inst✝ : CommRing R
X✝ Y✝ : AlgebraCat R
a₁✝ a₂✝ : X✝ ⟶ Y✝
h :
  (CategoryTheory.Functor.mk { obj := fun R_1 => ↑R_1, map := fun {X Y} f => f.toFun }).map a₁✝ =
    (CategoryTheory.Functor.mk { obj := fun R_1 => ↑R_1, map := fun {X Y} f => f.toFun }).map a₂✝
⊢ ∀ (x : ↑X✝), ↑a₁✝ x = ↑a₂✝ x
[PROOFSTEP]
intros x
[GOAL]
R : Type u
inst✝ : CommRing R
X✝ Y✝ : AlgebraCat R
a₁✝ a₂✝ : X✝ ⟶ Y✝
h :
  (CategoryTheory.Functor.mk { obj := fun R_1 => ↑R_1, map := fun {X Y} f => f.toFun }).map a₁✝ =
    (CategoryTheory.Functor.mk { obj := fun R_1 => ↑R_1, map := fun {X Y} f => f.toFun }).map a₂✝
x : ↑X✝
⊢ ↑a₁✝ x = ↑a₂✝ x
[PROOFSTEP]
dsimp at h 
[GOAL]
R : Type u
inst✝ : CommRing R
X✝ Y✝ : AlgebraCat R
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : ↑a₁✝ = ↑a₂✝
x : ↑X✝
⊢ ↑a₁✝ x = ↑a₂✝ x
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
⊢ ∀ (X : Type u),
    { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
        (𝟙 X) =
      𝟙
        ({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.obj
          X)
[PROOFSTEP]
intro X
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X : Type u
⊢ { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.obj
        X)
[PROOFSTEP]
apply FreeAlgebra.hom_ext
[GOAL]
case w
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X : Type u
⊢ ↑({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
          (𝟙 X)) ∘
      FreeAlgebra.ι R =
    ↑(𝟙
          ({ obj := fun S => mk (FreeAlgebra R S),
                map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.obj
            X)) ∘
      FreeAlgebra.ι R
[PROOFSTEP]
simp only [FreeAlgebra.ι_comp_lift]
[GOAL]
case w
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X : Type u
⊢ FreeAlgebra.ι R ∘ 𝟙 X = ↑(𝟙 (mk (FreeAlgebra R X))) ∘ FreeAlgebra.ι R
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
⊢ ∀ {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
        (f ≫ g) =
      { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
          f ≫
        { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
          g
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
      (f✝ ≫ g✝) =
    { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map f✝ ≫
      { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map g✝
[PROOFSTEP]
apply FreeAlgebra.hom_ext
[GOAL]
case w
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ ↑({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
          (f✝ ≫ g✝)) ∘
      FreeAlgebra.ι R =
    ↑({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
            f✝ ≫
          { obj := fun S => mk (FreeAlgebra R S),
                map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
            g✝) ∘
      FreeAlgebra.ι R
[PROOFSTEP]
simp only [FreeAlgebra.ι_comp_lift]
[GOAL]
case w
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ FreeAlgebra.ι R ∘ (f✝ ≫ g✝) =
    ↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝) ≫ ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ g✝)) ∘ FreeAlgebra.ι R
[PROOFSTEP]
ext1
  -- Porting node: this ↓ `erw` used to be handled by the `simp` below it
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : X✝
⊢ (FreeAlgebra.ι R ∘ (f✝ ≫ g✝)) x✝ =
    (↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝) ≫ ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ g✝)) ∘ FreeAlgebra.ι R)
      x✝
[PROOFSTEP]
erw [CategoryTheory.coe_comp]
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : X✝
⊢ (FreeAlgebra.ι R ∘ (f✝ ≫ g✝)) x✝ =
    ((↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ g✝)) ∘ ↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝))) ∘
        FreeAlgebra.ι R)
      x✝
[PROOFSTEP]
simp only [CategoryTheory.coe_comp, Function.comp_apply, types_comp_apply]
  -- Porting node: this ↓ `erw` and `rfl` used to be handled by the `simp` above
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : X✝
⊢ FreeAlgebra.ι R (g✝ (f✝ x✝)) =
    ↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ g✝))
      (↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝)) (FreeAlgebra.ι R x✝))
[PROOFSTEP]
erw [FreeAlgebra.lift_ι_apply, FreeAlgebra.lift_ι_apply]
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : X✝
⊢ FreeAlgebra.ι R (g✝ (f✝ x✝)) = (FreeAlgebra.ι R ∘ g✝) (f✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
⊢ ∀ {X' X : Type u} {Y : AlgebraCat R} (f : X' ⟶ X) (g : X ⟶ (forget (AlgebraCat R)).obj Y),
    ↑((fun X A => (FreeAlgebra.lift R).symm) X' Y).symm (f ≫ g) =
      (free R).map f ≫ ↑((fun X A => (FreeAlgebra.lift R).symm) X Y).symm g
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X'✝ X✝ : Type u
Y✝ : AlgebraCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget (AlgebraCat R)).obj Y✝
⊢ ↑((fun X A => (FreeAlgebra.lift R).symm) X'✝ Y✝).symm (f✝ ≫ g✝) =
    (free R).map f✝ ≫ ↑((fun X A => (FreeAlgebra.lift R).symm) X✝ Y✝).symm g✝
[PROOFSTEP]
apply FreeAlgebra.hom_ext
[GOAL]
case w
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X'✝ X✝ : Type u
Y✝ : AlgebraCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget (AlgebraCat R)).obj Y✝
⊢ ↑(↑((fun X A => (FreeAlgebra.lift R).symm) X'✝ Y✝).symm (f✝ ≫ g✝)) ∘ FreeAlgebra.ι R =
    ↑((free R).map f✝ ≫ ↑((fun X A => (FreeAlgebra.lift R).symm) X✝ Y✝).symm g✝) ∘ FreeAlgebra.ι R
[PROOFSTEP]
simp only [FreeAlgebra.ι_comp_lift]
[GOAL]
case w
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X'✝ X✝ : Type u
Y✝ : AlgebraCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget (AlgebraCat R)).obj Y✝
⊢ ↑(↑(FreeAlgebra.lift R).symm.symm (f✝ ≫ g✝)) ∘ FreeAlgebra.ι R =
    ↑((free R).map f✝ ≫ ↑(FreeAlgebra.lift R).symm.symm g✝) ∘ FreeAlgebra.ι R
[PROOFSTEP]
ext1
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X'✝ X✝ : Type u
Y✝ : AlgebraCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget (AlgebraCat R)).obj Y✝
x✝ : X'✝
⊢ (↑(↑(FreeAlgebra.lift R).symm.symm (f✝ ≫ g✝)) ∘ FreeAlgebra.ι R) x✝ =
    (↑((free R).map f✝ ≫ ↑(FreeAlgebra.lift R).symm.symm g✝) ∘ FreeAlgebra.ι R) x✝
[PROOFSTEP]
simp only [free_map, Equiv.symm_symm, FreeAlgebra.lift_ι_apply, CategoryTheory.coe_comp, Function.comp_apply,
  types_comp_apply]
  -- Porting node: this ↓ `erw` and `rfl` used to be handled by the `simp` above
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X'✝ X✝ : Type u
Y✝ : AlgebraCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget (AlgebraCat R)).obj Y✝
x✝ : X'✝
⊢ ↑(↑(FreeAlgebra.lift R) (f✝ ≫ g✝)) (FreeAlgebra.ι R x✝) =
    ↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝) ≫ ↑(FreeAlgebra.lift R) g✝) (FreeAlgebra.ι R x✝)
[PROOFSTEP]
erw [FreeAlgebra.lift_ι_apply, CategoryTheory.comp_apply, FreeAlgebra.lift_ι_apply, Function.comp_apply,
  FreeAlgebra.lift_ι_apply]
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X'✝ X✝ : Type u
Y✝ : AlgebraCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget (AlgebraCat R)).obj Y✝
x✝ : X'✝
⊢ (f✝ ≫ g✝) x✝ = g✝ (f✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
⊢ ∀ {X : Type u} {Y Y' : AlgebraCat R} (f : (free R).obj X ⟶ Y) (g : Y ⟶ Y'),
    ↑((fun X A => (FreeAlgebra.lift R).symm) X Y') (f ≫ g) =
      ↑((fun X A => (FreeAlgebra.lift R).symm) X Y) f ≫ (forget (AlgebraCat R)).map g
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ : Type u
Y✝ Y'✝ : AlgebraCat R
f✝ : (free R).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
⊢ ↑((fun X A => (FreeAlgebra.lift R).symm) X✝ Y'✝) (f✝ ≫ g✝) =
    ↑((fun X A => (FreeAlgebra.lift R).symm) X✝ Y✝) f✝ ≫ (forget (AlgebraCat R)).map g✝
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ : Type u
Y✝ Y'✝ : AlgebraCat R
f✝ : (free R).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
a✝ : X✝
⊢ ↑((fun X A => (FreeAlgebra.lift R).symm) X✝ Y'✝) (f✝ ≫ g✝) a✝ =
    (↑((fun X A => (FreeAlgebra.lift R).symm) X✝ Y✝) f✝ ≫ (forget (AlgebraCat R)).map g✝) a✝
[PROOFSTEP]
simp only [CategoryTheory.coe_comp, Function.comp_apply, FreeAlgebra.lift_symm_apply, types_comp_apply]
  -- Porting note: proof used to be done after this ↑ `simp`; added ↓ two lines
[GOAL]
case h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ : Type u
Y✝ Y'✝ : AlgebraCat R
f✝ : (free R).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
a✝ : X✝
⊢ ↑(FreeAlgebra.lift R).symm (f✝ ≫ g✝) a✝ = (forget (AlgebraCat R)).map g✝ (↑(FreeAlgebra.lift R).symm f✝ a✝)
[PROOFSTEP]
erw [FreeAlgebra.lift_symm_apply, FreeAlgebra.lift_symm_apply]
[GOAL]
case h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ : Type u
Y✝ Y'✝ : AlgebraCat R
f✝ : (free R).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
a✝ : X✝
⊢ (↑(f✝ ≫ g✝) ∘ FreeAlgebra.ι R) a✝ = (forget (AlgebraCat R)).map g✝ ((↑f✝ ∘ FreeAlgebra.ι R) a✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
g₁ : Ring X₁
g₂ : Ring X₂
m₁ : Algebra R X₁
m₂ : Algebra R X₂
e : X₁ ≃ₐ[R] X₂
⊢ ↑e ≫ ↑(symm e) = 𝟙 (AlgebraCat.of R X₁)
[PROOFSTEP]
ext x
[GOAL]
case w
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
g₁ : Ring X₁
g₂ : Ring X₂
m₁ : Algebra R X₁
m₂ : Algebra R X₂
e : X₁ ≃ₐ[R] X₂
x : (forget (AlgebraCat R)).obj (AlgebraCat.of R X₁)
⊢ ↑(↑e ≫ ↑(symm e)) x = ↑(𝟙 (AlgebraCat.of R X₁)) x
[PROOFSTEP]
exact e.left_inv x
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
g₁ : Ring X₁
g₂ : Ring X₂
m₁ : Algebra R X₁
m₂ : Algebra R X₂
e : X₁ ≃ₐ[R] X₂
⊢ ↑(symm e) ≫ ↑e = 𝟙 (AlgebraCat.of R X₂)
[PROOFSTEP]
ext x
[GOAL]
case w
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
g₁ : Ring X₁
g₂ : Ring X₂
m₁ : Algebra R X₁
m₂ : Algebra R X₂
e : X₁ ≃ₐ[R] X₂
x : (forget (AlgebraCat R)).obj (AlgebraCat.of R X₂)
⊢ ↑(↑(symm e) ≫ ↑e) x = ↑(𝟙 (AlgebraCat.of R X₂)) x
[PROOFSTEP]
exact e.right_inv x
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
i : X ≅ Y
x : ↑X
⊢ ↑i.inv (↑i.hom x) = x
[PROOFSTEP]
change (i.hom ≫ i.inv) x = x
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
i : X ≅ Y
x : ↑X
⊢ ↑(i.hom ≫ i.inv) x = x
[PROOFSTEP]
simp only [hom_inv_id]
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
i : X ≅ Y
x : ↑X
⊢ ↑(𝟙 X) x = x
[PROOFSTEP]
rw [id_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
i : X ≅ Y
x : ↑Y
⊢ ↑i.hom (↑i.inv x) = x
[PROOFSTEP]
change (i.inv ≫ i.hom) x = x
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
i : X ≅ Y
x : ↑Y
⊢ ↑(i.inv ≫ i.hom) x = x
[PROOFSTEP]
simp only [inv_hom_id]
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
i : X ≅ Y
x : ↑Y
⊢ ↑(𝟙 Y) x = x
[PROOFSTEP]
rw [id_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
f : X ⟶ Y
x✝ : IsIso ((forget (AlgebraCat R)).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget (AlgebraCat.{u} R)).map f)
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
f : X ⟶ Y
x✝ : IsIso ((forget (AlgebraCat R)).map f)
i : (forget (AlgebraCat R)).obj X ≅ (forget (AlgebraCat R)).obj Y := asIso ((forget (AlgebraCat R)).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃ₐ[R] Y := { f, i.toEquiv with }
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
f : X ⟶ Y
x✝ : IsIso ((forget (AlgebraCat R)).map f)
i : (forget (AlgebraCat R)).obj X ≅ (forget (AlgebraCat R)).obj Y := asIso ((forget (AlgebraCat R)).map f)
e : ↑X ≃ₐ[R] ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := f.toFun, invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
        right_inv := (_ : Function.RightInverse src.invFun src.toFun) },
    map_mul' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑↑f) (x * y) = OneHom.toFun (↑↑↑f) x * OneHom.toFun (↑↑↑f) y),
    map_add' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑↑f) (x + y) = OneHom.toFun (↑↑↑f) x + OneHom.toFun (↑↑↑f) y),
    commutes' := (_ : ∀ (r : R), OneHom.toFun (↑↑↑f) (↑(algebraMap R ↑X) r) = ↑(algebraMap R ↑Y) r) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toAlgebraIso).1⟩
