awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : Type u
inst : Semiring R
⊢ (↑(of R) : Type u) = R

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : SemiRingCat
r : (↑R : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{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 : SemiRingCat
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 : SemiRingCat
f : R ⟶ S
g : S ⟶ T
r : (↑R : Type u_1)
⊢ Eq (α := (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{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 : SemiRingCat.{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 : SemiRingCat.{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 : SemiRingCat
f g : R ⟶ S
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : Type u
inst : Semiring 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 : Semiring R
inst_1 : Semiring S
inst_2 : Semiring 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 : Semiring R
inst_1 : Semiring S
f : R →+* S
r : R
⊢ Eq (α := (↑(of S) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{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 : SemiRingCat
e : R ≅ S
r : (↑R : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{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 : SemiRingCat.{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 : SemiRingCat
e : R ≅ S
s : (↑S : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{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 : SemiRingCat.{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:
R S : SemiRingCat
f : R ⟶ S
x :
  (↑(Functor.obj
        (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD := MonCat.carrier))
        R) :
    Type u_1)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
            MonCat.carrier))
          S) :
      Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            MonCat.carrier) (X :=
            Functor.obj
              (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                carrier) MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
                MonCat.carrier))
              R)
            (CategoryTheory.Functor.map
              (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                carrier) MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
                MonCat.carrier))
              f) :
          (a : (↑((forget₂ SemiRingCat MonCat).obj R) : Type u_1)) → (↑((forget₂ SemiRingCat MonCat).obj S) : Type u_1))
        x :
      (↑(Functor.obj
            (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              carrier) MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
              MonCat.carrier))
            S) :
        Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{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 : SemiRingCat
f : R ⟶ S
x :
  (↑(Functor.obj
        (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CD :=
          AddCommMonCat.carrier))
        R) :
    Type u_1)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1))
            (CD := AddCommMonCat.carrier))
          S) :
      Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
            AddCommMonCat.carrier) (X :=
            Functor.obj
              (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1))
                (CD := AddCommMonCat.carrier))
              R)
            (CategoryTheory.Functor.map
              (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1))
                (CD := AddCommMonCat.carrier))
              f) :
          (a : (↑((forget₂ SemiRingCat AddCommMonCat).obj R) : Type u_1)) →
            (↑((forget₂ SemiRingCat AddCommMonCat).obj S) : Type u_1))
        x :
      (↑(Functor.obj
            (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1))
              (CD := AddCommMonCat.carrier))
            S) :
        Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{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:
X Y : SemiRingCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
      f)
i : Functor.obj
    (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)) X ≅
  Functor.obj
    (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget SemiRingCat (FC := fun (R S : SemiRingCat.{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.toSemiRingCatIso.isIso_hom

Premises used: RingEquiv.toSemiRingCatIso, MonoidHomClass.toMonoidHom, CategoryTheory.Iso.isIso_hom, RingHomClass.toRingHom
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
X Y : SemiRingCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
      f)
i : Functor.obj
    (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)) X ≅
  Functor.obj
    (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget SemiRingCat (FC := fun (R S : SemiRingCat.{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.toSemiRingCatIso.isIso_hom

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : RingCat
r : (↑R : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : RingCat.{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 : RingCat
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 : RingCat
f : R ⟶ S
g : S ⟶ T
r : (↑R : Type u_1)
⊢ Eq (α := (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{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 : RingCat.{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 : RingCat.{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 : RingCat
f g : R ⟶ S
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : Type u
inst : Ring 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 : Ring R
inst_1 : Ring S
inst_2 : Ring 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 : Ring R
inst_1 : Ring S
f : R →+* S
r : R
⊢ Eq (α := (↑(of S) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{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 : RingCat
e : R ≅ S
r : (↑R : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : RingCat.{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 : RingCat.{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 : RingCat
e : R ≅ S
s : (↑S : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : RingCat.{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 : RingCat.{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:
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)
          SemiRingCat (FD := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CD :=
          SemiRingCat.carrier))
        R) :
    Type u_1)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ RingCat (FC := fun (R S : RingCat.{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))
          S) :
      Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            SemiRingCat.carrier) (X :=
            Functor.obj
              (forget₂ RingCat (FC := fun (R S : RingCat.{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))
              R)
            (CategoryTheory.Functor.map
              (forget₂ RingCat (FC := fun (R S : RingCat.{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))
              f) :
          (a : (↑((forget₂ RingCat SemiRingCat).obj R) : Type u_1)) →
            (↑((forget₂ RingCat SemiRingCat).obj S) : 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)
              SemiRingCat (FD := fun (R S : SemiRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CD :=
              SemiRingCat.carrier))
            S) :
        Type u_1))
    ((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:
⊢ Functor.Full
    (forget₂ RingCat (FC := fun (R S : RingCat.{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: RingCat.fullyFaithfulForget₂ToSemiRingCat, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
X Y : RingCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget RingCat (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget RingCat (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)) f)
i : Functor.obj (forget RingCat (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
    X ≅
  Functor.obj (forget RingCat (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget RingCat (FC := fun (R S : RingCat.{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.toRingCatIso.isIso_hom

Premises used: MonoidHomClass.toMonoidHom, CategoryTheory.Iso.isIso_hom, RingHomClass.toRingHom, RingEquiv.toRingCatIso
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
X Y : RingCat
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget RingCat (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget RingCat (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)) f)
i : Functor.obj (forget RingCat (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
    X ≅
  Functor.obj (forget RingCat (FC := fun (R S : RingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget RingCat (FC := fun (R S : RingCat.{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.toRingCatIso.isIso_hom

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : CommSemiRingCat
r : (↑R : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommSemiRingCat.{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 : CommSemiRingCat
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 : CommSemiRingCat
f : R ⟶ S
g : S ⟶ T
r : (↑R : Type u_1)
⊢ Eq (α := (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommSemiRingCat.{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 : CommSemiRingCat.{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 : CommSemiRingCat.{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 : CommSemiRingCat
f g : R ⟶ S
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Basic
Goal:
R : Type u
inst : CommSemiring 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 : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring 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 : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
r : R
⊢ Eq (α := (↑(of S) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommSemiRingCat.{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 : CommSemiRingCat
e : R ≅ S
r : (↑R : 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))
      ((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))
          r :
        (↑S : Type u_1)) =
    r

Tactic:
simp