-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst_2 : CommRing P
g : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g j : (a : G j) → P) (f i j hij x) : P) ((g i : (a : G i) → P) x : P)
x : FreeCommRing ((i : ι) × G i)
hx :
  Membership.mem (γ := Set (FreeCommRing ((i : ι) × G i)))
    {a : FreeCommRing ((i : ι) × G i) |
      (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j H x)) -
              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) =
            a) ∨
        (∃ (i : ι),
            HSub.hSub (α := FreeCommRing ((i : ι) × G i)) (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) 1 =
              a) ∨
          (∃ (i : ι) (x : G i) (y : G i),
              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x + y)) -
                  (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) +
                    FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y)) =
                a) ∨
            ∃ (i : ι) (x : G i) (y : G i),
              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)) -
                  FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) *
                    FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y) =
                a}
    x
inl :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P)
      (((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
              (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) :
            (a : FreeCommRing ((i : ι) × G i)) → P)
          (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j hij x)) -
            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x)) :
        P)
      (0 : P)
inr :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α := P)
      (((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
              (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) :
            (a : FreeCommRing ((i : ι) × G i)) → P)
          (HSub.hSub (α := FreeCommRing ((i : ι) × G i)) (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) 1) :
        P)
      (0 : P)
inr₁ :
  ∀ (i : ι) (x y : G i),
    Eq.{u_3 + 1} (α := P)
      (((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
              (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) :
            (a : FreeCommRing ((i : ι) × G i)) → P)
          (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x + y)) -
            (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) +
              FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y))) :
        P)
      (0 : P)
⊢ Eq.{u_3 + 1} (α := P)
    (((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) :
          (a : FreeCommRing ((i : ι) × G i)) → P)
        x :
      P)
    (0 : P)
have inr₂ : ∀ (i : ι) (x y : G i),
  Eq.{u_3 + 1} (α := P)
    (((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) :
          (a : FreeCommRing ((i : ι) × G i)) → P)
        (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)) -
          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) *
            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y)) :
      P)
    (0 : P)
Tactic: rcases hx with (⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩)
Cleared hypotheses: x, hx