-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
        (P.B a).last → (α ::: P.M α).last),
        dest P (α := α) x =
            Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁) ∧
          dest P (α := α) y =
              Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂) ∧
            ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
i_1 : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
i : P.last.B a
c : Fin2 n
p : Path P (f i) c
IH :
  ∀ (f₁ f₂ : P.mp.B (f i) ⟹ α)
    (r :
      R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) (f i) f₁)
        (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) (f i) f₂)),
    f₁ c p = f₂ c p
f₁ f₂ : P.mp.B x ⟹ α
r : R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂)
a' : P.A
f₂' : (P.B a').last → (α ::: P.M α).last
g₁' : P.last.B a' → P.last.M
e₁' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'
e₂ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a'
      (splitFun (α := P.B a') (α' := α ::: P.M α) (pathDestLeft P (α := α) e₁' f₁) f₂'))
h'' :
  ∀ (i : (P.B a').last),
    R
      ((fun (x_1 : P.last.B a') ↦
          (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x_1) (pathDestRight P (α := α) e₁' f₁ x_1) :
            (a : P.mp.A) × P.mp.B a ⟹ α))
        i)
      (f₂' i)
e₁ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a'
      (splitFun (α := P.B a') (α' := α ::: P.M α) (pathDestLeft P (α := α) e₁' f₁) fun (x_1 : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x_1) (pathDestRight P (α := α) e₁' f₁ x_1)))
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
have e_snd : ∀ (g₂' : P.last.B a' → P.last.M) (e₂' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₂')
  (e₃ : pathDestLeft P (α := α) e₁' f₁ = pathDestLeft P (α := α) e₂' f₂)
  (e₂ :
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a'
        (splitFun (α := P.B a') (α' := α ::: P.M α) (pathDestLeft P (α := α) e₁' f₁) fun (x_1 : P.last.B a') ↦
          Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₂' x_1) (pathDestRight P (α := α) e₂' f₂ x_1))))
  (h'' :
    ∀ (i : (P.B a').last),
      R
        ((fun (x_1 : P.last.B a') ↦
            (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x_1) (pathDestRight P (α := α) e₁' f₁ x_1) :
              (a : P.mp.A) × P.mp.B a ⟹ α))
          i)
        ((fun (x_1 : P.last.B a') ↦
            (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₂' x_1) (pathDestRight P (α := α) e₂' f₂ x_1) :
              (a : P.mp.A) × P.mp.B a ⟹ α))
          i)),
  f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
Tactic: obtain ⟨g₂', e₂', e₃, rfl⟩ := M.bisim_lemma P e₂
Cleared hypotheses: f₂', e₂, h''