-- Mathlib/Data/PFunctor/Multivariate/M.lean
theorem M.bisim {α : TypeVec n} (R : P.M α → P.M α → Prop)
    (h :
      ∀ x y,
        R x y →
          ∃ a f f₁ f₂,
            M.dest P x = ⟨a, splitFun f f₁⟩ ∧
              M.dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ i, R (f₁ i) (f₂ i))
    (x y) (r : R x y) : x = y

Proof state:
case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨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 ⟨f i, f₁⟩ ⟨f i, f₂⟩ → f₁ c p = f₂ c p
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
a' : P.A
f₂' : (P.B a').last → (α ::: P.M α).last
g₁' : P.last.B a' → P.last.M
e₁' : x.dest = ⟨a', g₁'⟩
e₂ : dest P ⟨x, f₂⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) f₂'⟩
h'' : ∀ (i : (P.B a').last), R ((fun x_1 => ⟨g₁' x_1, pathDestRight P e₁' f₁ x_1⟩) i) (f₂' i)
e₁ : dest P ⟨x, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x_1 => ⟨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)

Tactic:
rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', e₃, rfl⟩

Result:
case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨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 ⟨f i, f₁⟩ ⟨f i, f₂⟩ → f₁ c p = f₂ c p
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
a' : P.A
g₁' : P.last.B a' → P.last.M
e₁' : x.dest = ⟨a', g₁'⟩
e₁ : dest P ⟨x, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x_1 => ⟨g₁' x_1, pathDestRight P e₁' f₁ x_1⟩⟩
g₂' : P.last.B a' → P.last.M
e₂' : x.dest = ⟨a', g₂'⟩
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨x, f₂⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x_1 => ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩⟩
h'' :
  ∀ (i : (P.B a').last),
    R ((fun x_1 => ⟨g₁' x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 => ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩) i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)

Proof state:
case intro.mk.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁✝ : P.mp.A
f₁✝ : P.mp.B a₁✝ ⟹ α
a₂✝ : P.mp.A
f₂✝ : P.mp.B a₂✝ ⟹ α
r✝ : R ⟨a₁✝, f₁✝⟩ ⟨a₂✝, f₂✝⟩
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
a' : P.A
g₁' : P.last.B a' → P.last.M
e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩⟩
g₂' : P.last.B a' → P.last.M
e₂' : PFunctor.M.dest a₂ = ⟨a', g₂'⟩
left✝ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨a₂, f₂⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x => ⟨g₂' x, pathDestRight P e₂' f₂ x⟩⟩
h' :
  ∀ (i : (P.B a').last),
    R ((fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩) i) ((fun x => ⟨g₂' x, pathDestRight P e₂' f₂ x⟩) i)
⊢ ∃ a f f',
    PFunctor.M.dest ⟨a₁, f₁⟩.fst = ⟨a, f⟩ ∧
      PFunctor.M.dest ⟨a₂, f₂⟩.fst = ⟨a, f'⟩ ∧
        ∀ (i : P.last.B a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)

Tactic:
rw [e₁', e₂']

Result:
case intro.mk.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁✝ : P.mp.A
f₁✝ : P.mp.B a₁✝ ⟹ α
a₂✝ : P.mp.A
f₂✝ : P.mp.B a₂✝ ⟹ α
r✝ : R ⟨a₁✝, f₁✝⟩ ⟨a₂✝, f₂✝⟩
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
a' : P.A
g₁' : P.last.B a' → P.last.M
e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩⟩
g₂' : P.last.B a' → P.last.M
e₂' : PFunctor.M.dest a₂ = ⟨a', g₂'⟩
left✝ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨a₂, f₂⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x => ⟨g₂' x, pathDestRight P e₂' f₂ x⟩⟩
h' :
  ∀ (i : (P.B a').last),
    R ((fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩) i) ((fun x => ⟨g₂' x, pathDestRight P e₂' f₂ x⟩) i)
⊢ ∃ a f f',
    ⟨a', g₁'⟩ = ⟨a, f⟩ ∧
      ⟨a', g₂'⟩ = ⟨a, f'⟩ ∧ ∀ (i : P.last.B a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)

Proof state:
case mk.mk.e_snd.a.h
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
f₁ f₂ : P.mp.B a₁ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₁, f₂⟩
i : Fin2 n
p : P.mp.B a₁ i
⊢ f₁ i p = f₂ i p

Tactic:
induction' p with x a f h' i c x a f h' i c p IH <;>
  try
    rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h''⟩
    rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
    rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', e₃, rfl⟩
    cases h'.symm.trans e₁'
    cases h'.symm.trans e₂'

Result:
case mk.mk.e_snd.a.h.root.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl.refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
i : Fin2 n
c : P.drop.B a i
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
e₁' : x.dest = ⟨a, f⟩
e₁ : dest P ⟨x, f₁⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 => ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩⟩
e₂' : x.dest = ⟨a, f⟩
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨x, f₂⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 => ⟨f x_1, pathDestRight P e₂' f₂ x_1⟩⟩
h'' :
  ∀ (i : (P.B a).last),
    R ((fun x_1 => ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 => ⟨f x_1, pathDestRight P e₂' f₂ x_1⟩) i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)

case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl.refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨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 ⟨f i, f₁⟩ ⟨f i, f₂⟩ → f₁ c p = f₂ c p
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
e₁' : x.dest = ⟨a, f⟩
e₁ : dest P ⟨x, f₁⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 => ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩⟩
e₂' : x.dest = ⟨a, f⟩
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨x, f₂⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 => ⟨f x_1, pathDestRight P e₂' f₂ x_1⟩⟩
h'' :
  ∀ (i : (P.B a).last),
    R ((fun x_1 => ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 => ⟨f x_1, pathDestRight P e₂' f₂ x_1⟩) i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)