gistfile1.txt

app_builder_exception, more information can be obtained using command `set_option trace.app_builder true`
state:
R S : Ring.{u},
i :
  @category_theory.iso.{u u+1} Ring.{u}
    (@category_theory.concrete_category.to_category.{u} Ring.{u} Ring.category_theory.concrete_category.{u})
    R
    S,
r : @coe_sort.{u+2 u+2} Ring.{u} Ring.has_coe_to_sort.{u} R,
x :
  @category_theory.functor.obj.{u u u+1 u+1} Ring.{u}
    (@category_theory.concrete_category.to_category.{u} Ring.{u} Ring.category_theory.concrete_category.{u})
    (Type u)
    category_theory.types.{u}
    (@category_theory.forget.{u} Ring.{u} Ring.category_theory.concrete_category.{u})
    S,
z :
  @eq.{u+1} (@coe_sort.{u+2 u+2} Ring.{u} Ring.has_coe_to_sort.{u} R) r
    (@coe_fn.{(max 1 (u+1)) u+1}
       (equiv.{u+1 u+1}
          (@category_theory.functor.obj.{u u u+1 u+1} Ring.{u}
             (@category_theory.concrete_category.to_category.{u} Ring.{u} Ring.category_theory.concrete_category.{u})
             (Type u)
             category_theory.types.{u}
             (@category_theory.forget.{u} Ring.{u} Ring.category_theory.concrete_category.{u})
             S)
          (@coe_sort.{u+2 u+2} Ring.{u} Ring.has_coe_to_sort.{u} R))
       (@equiv.has_coe_to_fun.{u+1 u+1}
          (@category_theory.functor.obj.{u u u+1 u+1} Ring.{u}
             (@category_theory.concrete_category.to_category.{u} Ring.{u} Ring.category_theory.concrete_category.{u})
             (Type u)
             category_theory.types.{u}
             (@category_theory.forget.{u} Ring.{u} Ring.category_theory.concrete_category.{u})
             S)
          (@coe_sort.{u+2 u+2} Ring.{u} Ring.has_coe_to_sort.{u} R))
       (@equiv.symm.{u+1 u+1} (@coe_sort.{u+2 u+2} Ring.{u} Ring.has_coe_to_sort.{u} R)
          (@category_theory.functor.obj.{u u u+1 u+1} Ring.{u}
             (@category_theory.concrete_category.to_category.{u} Ring.{u} Ring.category_theory.concrete_category.{u})
             (Type u)
             category_theory.types.{u}
             (@category_theory.forget.{u} Ring.{u} Ring.category_theory.concrete_category.{u})
             S)
          (@category_theory.iso.to_equiv.{u} (@coe_sort.{u+2 u+2} Ring.{u} Ring.has_coe_to_sort.{u} R)
             (@category_theory.functor.obj.{u u u+1 u+1} Ring.{u}
                (@category_theory.concrete_category.to_category.{u} Ring.{u} Ring.category_theory.concrete_category.{u})
                (Type u)
                category_theory.types.{u}
                (@category_theory.forget.{u} Ring.{u} Ring.category_theory.concrete_category.{u})
                S)
             (@category_theory.map_iso.{u u u+1 u+1} Ring.{u}
                (@category_theory.concrete_category.to_category.{u} Ring.{u} Ring.category_theory.concrete_category.{u})
                (Type u)
                category_theory.types.{u}
                (@category_theory.functor.obj.{u u u+1 u+1} Ring.{u}
                   (@category_theory.concrete_category.to_category.{u} Ring.{u}
                      Ring.category_theory.concrete_category.{u})
                   (Type u)
                   category_theory.types.{u}
                   (@category_theory.forget.{u} Ring.{u} Ring.category_theory.concrete_category.{u}))
                (@category_theory.category_theory.functorial.{u u u+1 u+1} Ring.{u}
                   (@category_theory.concrete_category.to_category.{u} Ring.{u}
                      Ring.category_theory.concrete_category.{u})
                   (Type u)
                   category_theory.types.{u}
                   (@category_theory.forget.{u} Ring.{u} Ring.category_theory.concrete_category.{u}))
                R
                S
                i)))
       x)
⊢ @coe_sort.{u+2 u+2} Ring.{u} Ring.has_coe_to_sort.{u} S