[GOAL]
⊢ ConcreteCategory SemiRingCat
[PROOFSTEP]
dsimp [SemiRingCat]
[GOAL]
⊢ ConcreteCategory (Bundled Semiring)
[PROOFSTEP]
infer_instance
[GOAL]
X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget SemiRingCat).map f)
[GOAL]
X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
i : (forget SemiRingCat).obj X ≅ (forget SemiRingCat).obj Y := asIso ((forget SemiRingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let ff : X →+* Y := f
[GOAL]
X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
i : (forget SemiRingCat).obj X ≅ (forget SemiRingCat).obj Y := asIso ((forget SemiRingCat).map f)
ff : ↑X →+* ↑Y := f
⊢ IsIso f
[PROOFSTEP]
let e : X ≃+* Y := { ff, i.toEquiv with }
[GOAL]
X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
i : (forget SemiRingCat).obj X ≅ (forget SemiRingCat).obj Y := asIso ((forget SemiRingCat).map f)
ff : ↑X →+* ↑Y := f
e : ↑X ≃+* ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := ff.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 (↑↑ff) (x * y) = OneHom.toFun (↑↑ff) x * OneHom.toFun (↑↑ff) y),
    map_add' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑ff) (x + y) = OneHom.toFun (↑↑ff) x + OneHom.toFun (↑↑ff) y) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toSemiRingCatIso).1⟩
[GOAL]
⊢ ConcreteCategory RingCat
[PROOFSTEP]
dsimp [RingCat]
[GOAL]
⊢ ConcreteCategory (Bundled Ring)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ ConcreteCategory CommSemiRingCat
[PROOFSTEP]
dsimp [CommSemiRingCat]
[GOAL]
⊢ ConcreteCategory (Bundled CommSemiring)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ ∀ {X Y : CommSemiRingCat} {f : X ⟶ Y},
    HEq ((forget CommMonCat).map ((fun {R₁ R₂} f => ↑f) f)) ((forget CommSemiRingCat).map f)
[PROOFSTEP]
rfl
[GOAL]
X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget CommSemiRingCat).map f)
[GOAL]
X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
i : (forget CommSemiRingCat).obj X ≅ (forget CommSemiRingCat).obj Y := asIso ((forget CommSemiRingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let ff : X →+* Y := f
[GOAL]
X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
i : (forget CommSemiRingCat).obj X ≅ (forget CommSemiRingCat).obj Y := asIso ((forget CommSemiRingCat).map f)
ff : ↑X →+* ↑Y := f
⊢ IsIso f
[PROOFSTEP]
let e : X ≃+* Y := { ff, i.toEquiv with }
[GOAL]
X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
i : (forget CommSemiRingCat).obj X ≅ (forget CommSemiRingCat).obj Y := asIso ((forget CommSemiRingCat).map f)
ff : ↑X →+* ↑Y := f
e : ↑X ≃+* ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := ff.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 (↑↑ff) (x * y) = OneHom.toFun (↑↑ff) x * OneHom.toFun (↑↑ff) y),
    map_add' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑ff) (x + y) = OneHom.toFun (↑↑ff) x + OneHom.toFun (↑↑ff) y) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toSemiRingCatIso).1⟩
[GOAL]
⊢ ConcreteCategory CommRingCat
[PROOFSTEP]
dsimp [CommRingCat]
[GOAL]
⊢ ConcreteCategory (Bundled CommRing)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ ∀ {X Y : CommRingCat} {f : X ⟶ Y},
    HEq ((forget CommSemiRingCat).map ((fun {R₁ R₂} f => f) f)) ((forget CommRingCat).map f)
[PROOFSTEP]
rfl
[GOAL]
R S : CommRingCat
i : R ⟶ S
r : ↑R
h : r = 0
⊢ ↑i r = 0
[PROOFSTEP]
simp [h]
[GOAL]
X Y : RingCat
i : X ≅ Y
x : ↑X
⊢ ↑(i.hom ≫ i.inv) x = x
[PROOFSTEP]
rw [i.hom_inv_id]
[GOAL]
X Y : RingCat
i : X ≅ Y
x : ↑X
⊢ ↑(𝟙 X) x = x
[PROOFSTEP]
rfl
[GOAL]
X Y : RingCat
i : X ≅ Y
x : ↑Y
⊢ ↑(i.inv ≫ i.hom) x = x
[PROOFSTEP]
rw [i.inv_hom_id]
[GOAL]
X Y : RingCat
i : X ≅ Y
x : ↑Y
⊢ ↑(𝟙 Y) x = x
[PROOFSTEP]
rfl
[GOAL]
X Y : CommRingCat
i : X ≅ Y
x : ↑X
⊢ ↑(i.hom ≫ i.inv) x = x
[PROOFSTEP]
rw [i.hom_inv_id]
[GOAL]
X Y : CommRingCat
i : X ≅ Y
x : ↑X
⊢ ↑(𝟙 X) x = x
[PROOFSTEP]
rfl
[GOAL]
X Y : CommRingCat
i : X ≅ Y
x : ↑Y
⊢ ↑(i.inv ≫ i.hom) x = x
[PROOFSTEP]
rw [i.inv_hom_id]
[GOAL]
X Y : CommRingCat
i : X ≅ Y
x : ↑Y
⊢ ↑(𝟙 Y) x = x
[PROOFSTEP]
rfl
[GOAL]
X Y : CommRingCat
i : X ≅ Y
⊢ RingEquiv.toRingHom (commRingCatIsoToRingEquiv i) = i.hom
[PROOFSTEP]
ext
[GOAL]
case a
X Y : CommRingCat
i : X ≅ Y
x✝ : ↑X
⊢ ↑(RingEquiv.toRingHom (commRingCatIsoToRingEquiv i)) x✝ = ↑i.hom x✝
[PROOFSTEP]
rfl
[GOAL]
X Y : CommRingCat
i : X ≅ Y
⊢ RingEquiv.toRingHom (RingEquiv.symm (commRingCatIsoToRingEquiv i)) = i.inv
[PROOFSTEP]
ext
[GOAL]
case a
X Y : CommRingCat
i : X ≅ Y
x✝ : ↑Y
⊢ ↑(RingEquiv.toRingHom (RingEquiv.symm (commRingCatIsoToRingEquiv i))) x✝ = ↑i.inv x✝
[PROOFSTEP]
rfl
[GOAL]
X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget RingCat).map f)
[GOAL]
X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
i : (forget RingCat).obj X ≅ (forget RingCat).obj Y := asIso ((forget RingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let ff : X →+* Y := f
[GOAL]
X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
i : (forget RingCat).obj X ≅ (forget RingCat).obj Y := asIso ((forget RingCat).map f)
ff : ↑X →+* ↑Y := f
⊢ IsIso f
[PROOFSTEP]
let e : X ≃+* Y := { ff, i.toEquiv with }
[GOAL]
X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
i : (forget RingCat).obj X ≅ (forget RingCat).obj Y := asIso ((forget RingCat).map f)
ff : ↑X →+* ↑Y := f
e : ↑X ≃+* ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := ff.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 (↑↑ff) (x * y) = OneHom.toFun (↑↑ff) x * OneHom.toFun (↑↑ff) y),
    map_add' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑ff) (x + y) = OneHom.toFun (↑↑ff) x + OneHom.toFun (↑↑ff) y) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toRingCatIso).1⟩
[GOAL]
X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget CommRingCat).map f)
[GOAL]
X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
i : (forget CommRingCat).obj X ≅ (forget CommRingCat).obj Y := asIso ((forget CommRingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let ff : X →+* Y := f
[GOAL]
X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
i : (forget CommRingCat).obj X ≅ (forget CommRingCat).obj Y := asIso ((forget CommRingCat).map f)
ff : ↑X →+* ↑Y := f
⊢ IsIso f
[PROOFSTEP]
let e : X ≃+* Y := { ff, i.toEquiv with }
[GOAL]
X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
i : (forget CommRingCat).obj X ≅ (forget CommRingCat).obj Y := asIso ((forget CommRingCat).map f)
ff : ↑X →+* ↑Y := f
e : ↑X ≃+* ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := ff.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 (↑↑ff) (x * y) = OneHom.toFun (↑↑ff) x * OneHom.toFun (↑↑ff) y),
    map_add' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑ff) (x + y) = OneHom.toFun (↑↑ff) x + OneHom.toFun (↑↑ff) y) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toCommRingCatIso).1⟩
[GOAL]
⊢ ReflectsIsomorphisms (forget₂ RingCat AddCommGroupCat)
[PROOFSTEP]
infer_instance
