-- 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₁_1 : P.mp.A
f₁_1 : P.mp.B a₁_1 ⟹ α
a₂_1 : P.mp.A
f₂_1 : P.mp.B a₂_1 ⟹ α
r_1 :
  R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₁_1 f₁_1)
    (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₂_1 f₂_1)
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) 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₁ = 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.mp.A) ↦ P.mp.B a ⟹ α) a₂ 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 : P.last.B a') ↦
          (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x) :
            (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.mp.A) ↦ P.mp.B a ⟹ α) a₁ 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 : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)))
rcases :
  ∀ (g₂' : P.last.B a' → P.last.M)
    (e₂' : PFunctor.M.dest a₂ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₂'),
    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.mp.A) ↦ P.mp.B a ⟹ α) a₂ 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 : P.last.B a') ↦
                Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₂' x) (pathDestRight P (α := α) e₂' f₂ x))))
        (h' :
          ∀ (i : (P.B a').last),
            R
              ((fun (x : P.last.B a') ↦
                  (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x) :
                    (a : P.mp.A) × P.mp.B a ⟹ α))
                i)
              ((fun (x : P.last.B a') ↦
                  (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₂' x) (pathDestRight P (α := α) e₂' f₂ x) :
                    (a : P.mp.A) × P.mp.B a ⟹ α))
                i)),
        ∃ (a : P.last.A) (f : P.last.B a → P.last.M) (f' : P.last.B a → P.last.M),
          PFunctor.M.dest
                (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                  (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁)) =
              Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f ∧
            PFunctor.M.dest
                  (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                    (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₂ f₂)) =
                Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f' ∧
              ∀ (i : P.last.B a),
                (fun (a₁ a₂ : P.last.M) ↦
                    ∃ (x : P.M α) (y : P.M α),
                      R x y ∧
                        x.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) = a₁ ∧
                          y.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) = a₂)
                  (f i) (f' i)
⊢ ∃ (a : P.last.A) (f : P.last.B a → P.last.M) (f' : P.last.B a → P.last.M),
    PFunctor.M.dest
          (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁)) =
        Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f ∧
      PFunctor.M.dest
            (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₂ f₂)) =
          Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f' ∧
        ∀ (i : P.last.B a),
          (fun (a₁ a₂ : P.last.M) ↦
              ∃ (x : P.M α) (y : P.M α),
                R x y ∧
                  x.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) = a₁ ∧ y.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) = a₂)
            (f i) (f' i)

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

Premises used: MvPFunctor.M.bisim_lemma, rfl