-- 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
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₂⟩
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)

Tactic:
rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h''⟩

Result:
case mk.mk.e_snd.a.h.child.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').drop ⟹ (α ::: P.M α).drop
f₁' f₂' : (P.B a').last → (α ::: P.M α).last
e₁ : dest P ⟨x, f₁⟩ = ⟨a', splitFun f' f₁'⟩
e₂ : dest P ⟨x, f₂⟩ = ⟨a', splitFun f' f₂'⟩
h'' : ∀ (i : (P.B a').last), R (f₁' i) (f₂' 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 mk.mk
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₁, f₁⟩ = ⟨a₂, f₂⟩

Tactic:
have : a₁ = a₂ := by
  refine
    PFunctor.M.bisim (fun a₁ a₂ => ∃ x y, R x y ∧ x.1 = a₁ ∧ y.1 = a₂) ?_ _ _
      ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
  rintro _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
  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₂', _, rfl⟩
  rw [e₁', e₂']
  exact ⟨_, _, _, rfl, rfl, fun b => ⟨_, _, h' b, rfl, rfl⟩⟩

Result:
case mk.mk
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₂⟩
this : a₁ = a₂
⊢ ⟨a₁, f₁⟩ = ⟨a₂, f₂⟩

Proof state:
case intro.mk.intro.mk.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
f₂' : (P.B a').last → (α ::: P.M α).last
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₁) f₂'⟩
h' : ∀ (i : (P.B a').last), R ((fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩) i) (f₂' i)
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩⟩
⊢ ∃ 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:
rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', _, rfl⟩

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',
    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)

Proof state:
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₁ = a₂

Tactic:
refine
  PFunctor.M.bisim (fun a₁ a₂ => ∃ x y, R x y ∧ x.1 = a₁ ∧ y.1 = a₂) ?_ _ _
    ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩

Result:
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₂⟩
⊢ ∀ (x y : P.last.M),
    (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) x y →
      ∃ a f f',
        x.dest = ⟨a, f⟩ ∧
          y.dest = ⟨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)