-- Module: Mathlib.Data.PFunctor.Multivariate.M
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
f₁ f₂ : P.mp.B a₁ ⟹ α
r :
  R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₁ f₁) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₁ f₂)
i : Fin2 n
p : P.mp.B a₁ i
e_snd :
  ∀ (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 : Fin2 n) (c : P.drop.B a i)
    (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₂)),
    f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
e_snd₁ :
  ∀ (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 : Fin2 n) (c : P.drop.B a i)
    (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₂))
    (e₁' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a 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 ⟹ α) (f x_1) (pathDestRight P (α := α) e₁' f₁ x_1))))
    (e₂' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f)
    (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 ⟹ α) (f 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 ⟹ α) (f 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 ⟹ α) (f x_1) (pathDestRight P (α := α) e₂' f₂ x_1) :
                (a : P.mp.A) × P.mp.B a ⟹ α))
            i)),
    f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
e_snd₂ :
  ∀ (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₂)),
    f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
e_snd₃ :
  ∀ (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₂))
    (e₁' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a 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 ⟹ α) (f x_1) (pathDestRight P (α := α) e₁' f₁ x_1))))
    (e₂' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f)
    (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 ⟹ α) (f 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 ⟹ α) (f 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 ⟹ α) (f 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)
⊢ f₁ i p = f₂ i p

Tactic:
induction p with (
    obtain ⟨a', f', f₁', f₂', e₁, e₂, h''⟩ := h _ _ r
    obtain ⟨g₁', e₁', rfl, rfl⟩ := M.bisim_lemma P e₁
    obtain ⟨g₂', e₂', e₃, rfl⟩ := M.bisim_lemma P e₂
    cases h'.symm.trans e₁'
    cases h'.symm.trans e₂')
  | root x a f h' i c =>
    exact congr_fun (congr_fun e₃ i) c
  | child x a f h' i c p IH =>
    exact IH _ _ (h'' _)

Premises used: rfl