[GOAL]
⊢ ConcreteCategory BoolRingCat
[PROOFSTEP]
dsimp [BoolRingCat]
[GOAL]
⊢ ConcreteCategory (Bundled BooleanRing)
[PROOFSTEP]
infer_instance
  -- Porting note: disabled `simps`
  --   Invalid simp lemma BoolRingCat.hasForgetToCommRing_forget₂_obj_str_add.
  --   The given definition is not a constructor application:
  --     inferInstance.1
  -- @[simps]
[GOAL]
α β : BoolRingCat
e : ↑α ≃+* ↑β
⊢ ↑e ≫ ↑(RingEquiv.symm e) = 𝟙 α
[PROOFSTEP]
ext
[GOAL]
case w
α β : BoolRingCat
e : ↑α ≃+* ↑β
x✝ : (forget BoolRingCat).obj α
⊢ ↑(↑e ≫ ↑(RingEquiv.symm e)) x✝ = ↑(𝟙 α) x✝
[PROOFSTEP]
exact e.symm_apply_apply _
[GOAL]
α β : BoolRingCat
e : ↑α ≃+* ↑β
⊢ ↑(RingEquiv.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext
[GOAL]
case w
α β : BoolRingCat
e : ↑α ≃+* ↑β
x✝ : (forget BoolRingCat).obj β
⊢ ↑(↑(RingEquiv.symm e) ≫ ↑e) x✝ = ↑(𝟙 β) x✝
[PROOFSTEP]
exact e.apply_symm_apply _
