-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
c : Cone (pair A B)
j : Discrete WalkingPair
x : (↑c.pt : Type u)
hf :
  Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    (((Hom.hom
              (CategoryStruct.comp (Y := (A.prodFan B).pt)
                (ofHom
                    (RingHom.prod (Hom.hom (c.π.app { as := WalkingPair.left }))
                      (Hom.hom (c.π.app { as := WalkingPair.right }))) :
                  of (↑c.1 : Type u) ⟶ of ((↑A : Type u) × (↑B : Type u)))
                ((A.prodFan B).π.app { as := WalkingPair.left } :
                  Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (A.prodFan B).pt)
                      { as := WalkingPair.left : Discrete WalkingPair } ⟶
                    Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair })) :
            (↑c.pt : Type u) →+*
              (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u)) :
          (a : (↑c.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((Hom.hom (c.π.app { as := WalkingPair.left }) :
          (a : (↑c.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
⊢ Eq (α := (↑(Functor.obj (pair A B) j) : Type u))
    (((Hom.hom
              (ofHom
                  (RingHom.prod (Hom.hom (c.π.app { as := WalkingPair.left }))
                    (Hom.hom (c.π.app { as := WalkingPair.right }))) ≫
                (A.prodFan B).π.app j) :
            (↑c.pt : Type u) →+* (↑(Functor.obj (pair A B) j) : Type u)) :
          (a : (↑c.pt : Type u)) → (↑((pair A B).obj j) : Type u))
        x :
      (↑(Functor.obj (pair A B) j) : Type u))
    ((Hom.hom (c.π.app j) : (a : (↑c.pt : Type u)) → (↑((pair A B).obj j) : Type u)) x :
      (↑(Functor.obj (pair A B) j) : Type u))
have hf₁ : Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
  (((Hom.hom
            (CategoryStruct.comp (Y := (A.prodFan B).pt)
              (ofHom
                  (RingHom.prod (Hom.hom (c.π.app { as := WalkingPair.left }))
                    (Hom.hom (c.π.app { as := WalkingPair.right }))) :
                of (↑c.1 : Type u) ⟶ of ((↑A : Type u) × (↑B : Type u)))
              ((A.prodFan B).π.app { as := WalkingPair.right } :
                Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (A.prodFan B).pt)
                    { as := WalkingPair.right : Discrete WalkingPair } ⟶
                  Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :
          (↑c.pt : Type u) →+*
            (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u)) :
        (a : (↑c.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
      x :
    (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
  ((Hom.hom (c.π.app { as := WalkingPair.right }) :
        (a : (↑c.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
      x :
    (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j