awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommSemiRingCat
e : R ≅ S
s : (↑S : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          e.hom :
        (a : (↑R : Type u_1)) → (↑S : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              carrier) e.inv :
            (a : (↑S : Type u_1)) → (↑R : Type u_1))
          s :
        (↑R : Type u_1)) =
    s

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
⊢ Functor.Full
    (forget₂ CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      carrier) SemiRingCat (FD := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CD :=
      SemiRingCat.carrier))

Tactic:
fullyFaithfulForget₂ToSemiRingCat.full

Premises used: CommSemiRingCat.fullyFaithfulForget₂ToSemiRingCat, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
X Y : CommSemiRingCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        carrier))
      X)
    (CategoryTheory.Functor.map
      (forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        carrier))
      f)
i : Functor.obj
    (forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      carrier))
    X ≅
  Functor.obj
    (forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        carrier))
      f)
ff : (↑X : Type u_1) →+* (↑Y : Type u_1) := Hom.hom f
e : (↑X : Type u_1) ≃+* (↑Y : Type u_1) :=
  let __src := i.toEquiv;
  { toFun := (↑(↑ff : (↑X : Type u_1) →* (↑Y : Type u_1)) : OneHom (↑X : Type u_1) (↑Y : Type u_1)).toFun,
    invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ IsIso f

Tactic:
e.toCommSemiRingCatIso.isIso_hom

Premises used: RingEquiv.toCommSemiRingCatIso, MonoidHomClass.toMonoidHom, CategoryTheory.Iso.isIso_hom, RingHomClass.toRingHom
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
X Y : CommSemiRingCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        carrier))
      X)
    (CategoryTheory.Functor.map
      (forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        carrier))
      f)
i : Functor.obj
    (forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      carrier))
    X ≅
  Functor.obj
    (forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        carrier))
      f)
ff : (↑X : Type u_1) →+* (↑Y : Type u_1) := Hom.hom f
e : (↑X : Type u_1) ≃+* (↑Y : Type u_1) :=
  let __src := i.toEquiv;
  { toFun := (↑(↑ff : (↑X : Type u_1) →* (↑Y : Type u_1)) : OneHom (↑X : Type u_1) (↑Y : Type u_1)).toFun,
    invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toCommSemiRingCatIso.isIso_hom

Premises used: RingEquiv.toCommSemiRingCatIso, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : Type u
inst : CommRing R
⊢ (↑(of R) : Type u) = R

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : CommRingCat
⊢ of (↑R : Type u) = R

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : CommRingCat
⊢ Hom.hom (𝟙 R) = RingHom.id (↑R : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : CommRingCat
r : (↑R : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          (𝟙 R) :
        (a : (↑R : Type u_1)) → (↑R : Type u_1))
      r =
    r

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
r : (↑R : Type u_1)
⊢ Eq (α := (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
            (f ≫ g) :
          (a : (↑R : Type u_1)) → (↑T : Type u_1))
        r :
      (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
            g :
          (a : (↑S : Type u_1)) → (↑T : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                carrier) f :
              (a : (↑R : Type u_1)) → (↑S : Type u_1))
            r :
          (↑S : Type u_1)) :
      (↑T : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommRingCat
f g : R ⟶ S
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: CommRingCat.Hom.ext
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : Type u
inst : CommRing R
⊢ ofHom (RingHom.id R) = 𝟙 (of R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
⊢ Eq (α := (↑(of S) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (ofHom f) :
          (a : (↑(of R) : Type u)) → (↑(of S) : Type u))
        r :
      (↑(of S) : Type u))
    ((f : (a : R) → S) r : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommRingCat
e : R ≅ S
r : (↑R : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          e.inv :
        (a : (↑S : Type u_1)) → (↑R : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
              e.hom :
            (a : (↑R : Type u_1)) → (↑S : Type u_1))
          r :
        (↑S : Type u_1)) =
    r

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommRingCat
e : R ≅ S
s : (↑S : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          e.hom :
        (a : (↑R : Type u_1)) → (↑S : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
              e.inv :
            (a : (↑S : Type u_1)) → (↑R : Type u_1))
          s :
        (↑R : Type u_1)) =
    s

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
⊢ Functor.Full
    (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
      RingCat (FD := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CD := RingCat.carrier))

Tactic:
fullyFaithfulForget₂ToRingCat.full

Premises used: CommRingCat.fullyFaithfulForget₂ToRingCat, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ RingCat.Hom.hom
      (CategoryTheory.Functor.map
        (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          RingCat (FD := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CD := RingCat.carrier))
        f) =
    Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : CommRingCat
⊢ (↑(Functor.obj
          (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier))
          R) :
      Type u) =
    (↑R : Type u)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
X Y : CommRingCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
      f)
i : Functor.obj
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)) X ≅
  Functor.obj
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
      f)
ff : (↑X : Type u_1) →+* (↑Y : Type u_1) := Hom.hom f
e : (↑X : Type u_1) ≃+* (↑Y : Type u_1) :=
  let __src := i.toEquiv;
  { toFun := (↑(↑ff : (↑X : Type u_1) →* (↑Y : Type u_1)) : OneHom (↑X : Type u_1) (↑Y : Type u_1)).toFun,
    invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ IsIso f

Tactic:
e.toCommRingCatIso.isIso_hom

Premises used: RingEquiv.toCommRingCatIso, MonoidHomClass.toMonoidHom, CategoryTheory.Iso.isIso_hom, RingHomClass.toRingHom
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
X Y : CommRingCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
      f)
i : Functor.obj
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)) X ≅
  Functor.obj
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
      f)
ff : (↑X : Type u_1) →+* (↑Y : Type u_1) := Hom.hom f
e : (↑X : Type u_1) ≃+* (↑Y : Type u_1) :=
  let __src := i.toEquiv;
  { toFun := (↑(↑ff : (↑X : Type u_1) →* (↑Y : Type u_1)) : OneHom (↑X : Type u_1) (↑Y : Type u_1)).toFun,
    invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toCommRingCatIso.isIso_hom

Premises used: RingEquiv.toCommRingCatIso, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : SemiRingCat
e : R ≅ S
a :
  ∀ (x : (↑S : Type u)),
    Eq (α := (↑S : Type u))
      (((SemiRingCat.Hom.hom e.hom).comp (SemiRingCat.Hom.hom e.inv) : (a : (↑S : Type u)) → (↑S : Type u)) x :
        (↑S : Type u))
      ((RingHom.id (↑S : Type u) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))
⊢ (SemiRingCat.Hom.hom e.hom).comp (SemiRingCat.Hom.hom e.inv) = RingHom.id (↑S : Type u)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : SemiRingCat
e : R ≅ S
x : (↑S : Type u)
⊢ Eq (α := (↑S : Type u))
    (((SemiRingCat.Hom.hom e.hom).comp (SemiRingCat.Hom.hom e.inv) : (a : (↑S : Type u)) → (↑S : Type u)) x :
      (↑S : Type u))
    ((RingHom.id (↑S : Type u) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : SemiRingCat
e : R ≅ S
a :
  ∀ (x : (↑R : Type u)),
    Eq (α := (↑R : Type u))
      (((SemiRingCat.Hom.hom e.inv).comp (SemiRingCat.Hom.hom e.hom) : (a : (↑R : Type u)) → (↑R : Type u)) x :
        (↑R : Type u))
      ((RingHom.id (↑R : Type u) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))
⊢ (SemiRingCat.Hom.hom e.inv).comp (SemiRingCat.Hom.hom e.hom) = RingHom.id (↑R : Type u)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : SemiRingCat
e : R ≅ S
x : (↑R : Type u)
⊢ Eq (α := (↑R : Type u))
    (((SemiRingCat.Hom.hom e.inv).comp (SemiRingCat.Hom.hom e.hom) : (a : (↑R : Type u)) → (↑R : Type u)) x :
      (↑R : Type u))
    ((RingHom.id (↑R : Type u) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : RingCat
e : R ≅ S
a :
  ∀ (x : (↑S : Type u)),
    Eq (α := (↑S : Type u))
      (((RingCat.Hom.hom e.hom).comp (RingCat.Hom.hom e.inv) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))
      ((RingHom.id (↑S : Type u) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))
⊢ (RingCat.Hom.hom e.hom).comp (RingCat.Hom.hom e.inv) = RingHom.id (↑S : Type u)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : RingCat
e : R ≅ S
x : (↑S : Type u)
⊢ Eq (α := (↑S : Type u))
    (((RingCat.Hom.hom e.hom).comp (RingCat.Hom.hom e.inv) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))
    ((RingHom.id (↑S : Type u) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : RingCat
e : R ≅ S
a :
  ∀ (x : (↑R : Type u)),
    Eq (α := (↑R : Type u))
      (((RingCat.Hom.hom e.inv).comp (RingCat.Hom.hom e.hom) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))
      ((RingHom.id (↑R : Type u) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))
⊢ (RingCat.Hom.hom e.inv).comp (RingCat.Hom.hom e.hom) = RingHom.id (↑R : Type u)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : RingCat
e : R ≅ S
x : (↑R : Type u)
⊢ Eq (α := (↑R : Type u))
    (((RingCat.Hom.hom e.inv).comp (RingCat.Hom.hom e.hom) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))
    ((RingHom.id (↑R : Type u) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommSemiRingCat
e : R ≅ S
a :
  ∀ (x : (↑S : Type u)),
    Eq (α := (↑S : Type u))
      (((CommSemiRingCat.Hom.hom e.hom).comp (CommSemiRingCat.Hom.hom e.inv) : (a : (↑S : Type u)) → (↑S : Type u)) x :
        (↑S : Type u))
      ((RingHom.id (↑S : Type u) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))
⊢ (CommSemiRingCat.Hom.hom e.hom).comp (CommSemiRingCat.Hom.hom e.inv) = RingHom.id (↑S : Type u)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommSemiRingCat
e : R ≅ S
x : (↑S : Type u)
⊢ Eq (α := (↑S : Type u))
    (((CommSemiRingCat.Hom.hom e.hom).comp (CommSemiRingCat.Hom.hom e.inv) : (a : (↑S : Type u)) → (↑S : Type u)) x :
      (↑S : Type u))
    ((RingHom.id (↑S : Type u) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommSemiRingCat
e : R ≅ S
a :
  ∀ (x : (↑R : Type u)),
    Eq (α := (↑R : Type u))
      (((CommSemiRingCat.Hom.hom e.inv).comp (CommSemiRingCat.Hom.hom e.hom) : (a : (↑R : Type u)) → (↑R : Type u)) x :
        (↑R : Type u))
      ((RingHom.id (↑R : Type u) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))
⊢ (CommSemiRingCat.Hom.hom e.inv).comp (CommSemiRingCat.Hom.hom e.hom) = RingHom.id (↑R : Type u)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommSemiRingCat
e : R ≅ S
x : (↑R : Type u)
⊢ Eq (α := (↑R : Type u))
    (((CommSemiRingCat.Hom.hom e.inv).comp (CommSemiRingCat.Hom.hom e.hom) : (a : (↑R : Type u)) → (↑R : Type u)) x :
      (↑R : Type u))
    ((RingHom.id (↑R : Type u) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommRingCat
e : R ≅ S
a :
  ∀ (x : (↑S : Type u)),
    Eq (α := (↑S : Type u))
      (((CommRingCat.Hom.hom e.hom).comp (CommRingCat.Hom.hom e.inv) : (a : (↑S : Type u)) → (↑S : Type u)) x :
        (↑S : Type u))
      ((RingHom.id (↑S : Type u) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))
⊢ (CommRingCat.Hom.hom e.hom).comp (CommRingCat.Hom.hom e.inv) = RingHom.id (↑S : Type u)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommRingCat
e : R ≅ S
x : (↑S : Type u)
⊢ Eq (α := (↑S : Type u))
    (((CommRingCat.Hom.hom e.hom).comp (CommRingCat.Hom.hom e.inv) : (a : (↑S : Type u)) → (↑S : Type u)) x :
      (↑S : Type u))
    ((RingHom.id (↑S : Type u) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommRingCat
e : R ≅ S
a :
  ∀ (x : (↑R : Type u)),
    Eq (α := (↑R : Type u))
      (((CommRingCat.Hom.hom e.inv).comp (CommRingCat.Hom.hom e.hom) : (a : (↑R : Type u)) → (↑R : Type u)) x :
        (↑R : Type u))
      ((RingHom.id (↑R : Type u) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))
⊢ (CommRingCat.Hom.hom e.inv).comp (CommRingCat.Hom.hom e.hom) = RingHom.id (↑R : Type u)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommRingCat
e : R ≅ S
x : (↑R : Type u)
⊢ Eq (α := (↑R : Type u))
    (((CommRingCat.Hom.hom e.inv).comp (CommRingCat.Hom.hom e.hom) : (a : (↑R : Type u)) → (↑R : Type u)) x :
      (↑R : Type u))
    ((RingHom.id (↑R : Type u) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : SemiRingCat
e : R ≅ S
⊢ (↑e.semiRingCatIsoToRingEquiv : (↑R : Type u) →+* (↑S : Type u)) = SemiRingCat.Hom.hom e.hom

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : RingCat
e : R ≅ S
⊢ (↑e.ringCatIsoToRingEquiv : (↑R : Type u) →+* (↑S : Type u)) = RingCat.Hom.hom e.hom

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommSemiRingCat
e : R ≅ S
⊢ (↑e.commSemiRingCatIsoToRingEquiv : (↑R : Type u) →+* (↑S : Type u)) = CommSemiRingCat.Hom.hom e.hom

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommRingCat
e : R ≅ S
⊢ (↑e.commRingCatIsoToRingEquiv : (↑R : Type u) →+* (↑S : Type u)) = CommRingCat.Hom.hom e.hom

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : RingCat
f : R ⟶ S
x :
  Functor.obj (forget RingCat (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)) R
⊢ Eq (α :=
    (fun (X : Type u_1) ↦ X)
      (Functor.obj
        (forget RingCat (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)) S))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (forget RingCat (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
              f) :
          (a : (fun (X : Type u_1) ↦ X) ((forget RingCat).obj R)) → (fun (X : Type u_1) ↦ X) ((forget RingCat).obj S))
        x :
      (fun (X : Type u_1) ↦ X)
        (Functor.obj
          (forget RingCat (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)) S))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier) f :
          (a : (↑R : Type u_1)) → (↑S : Type u_1))
        x :
      (↑S : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R S : CommRingCat
f : R ⟶ S
x :
  Functor.obj
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)) R
⊢ Eq (α :=
    (fun (X : Type u_1) ↦ X)
      (Functor.obj
        (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
        S))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                carrier))
              f) :
          (a : (fun (X : Type u_1) ↦ X) ((forget CommRingCat).obj R)) →
            (fun (X : Type u_1) ↦ X) ((forget CommRingCat).obj S))
        x :
      (fun (X : Type u_1) ↦ X)
        (Functor.obj
          (forget CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            carrier))
          S))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
            f :
          (a : (↑R : Type u_1)) → (↑S : Type u_1))
        x :
      (↑S : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
x_1 y_1 z_1 : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
      (Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y))
      (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z) =
    Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
      (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
      (Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z))

Tactic:
Quot.sound (Relation.mul_assoc _ _ _)

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, RingCat.Colimits.Relation.mul_assoc, Quotient, RingCat.Colimits.ColimitType