-- Mathlib/Data/PFunctor/Multivariate/M.lean
theorem M.bisim_lemma {α : TypeVec n} {a₁ : (mp P).A} {f₁ : (mp P).B a₁ ⟹ α} {a' : P.A}
    {f' : (P.B a').drop ⟹ α} {f₁' : (P.B a').last → M P α}
    (e₁ : M.dest P ⟨a₁, f₁⟩ = ⟨a', splitFun f' f₁'⟩) :
    ∃ (g₁' : _)(e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = M.pathDestLeft P e₁' f₁ ∧
        f₁' = fun x : (last P).B a' => ⟨g₁' x, M.pathDestRight P e₁' f₁ x⟩

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', splitFun f' f₁'⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Tactic:
generalize ef : @splitFun n _ (append1 α (M P α)) f' f₁' = ff at e₁

Result:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', ff⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', ff⟩
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Tactic:
rcases e₁' : he₁' with ⟨a₁', g₁'⟩

Result:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', ff⟩
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = ⟨a₁', g₁'⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Proof state:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', ff⟩
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = ⟨a₁', g₁'⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Tactic:
rw [M.dest_eq_dest' _ e₁'] at e₁

Result:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = ⟨a₁', g₁'⟩
e₁ : dest' P e₁' f₁ = ⟨a', ff⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', ff⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Tactic:
let he₁' := PFunctor.M.dest a₁

Result:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', ff⟩
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Proof state:
case mk.refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
g₁' : P.last.B a' → P.last.M
e₁' : he₁' = ⟨a', g₁'⟩
ef : splitFun f' f₁' = splitFun (pathDestLeft P e₁' f₁) fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Tactic:
exact ⟨_, e₁', splitFun_inj ef⟩

Result:
no goals

Proof state:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = ⟨a₁', g₁'⟩
e₁ : dest' P e₁' f₁ = ⟨a', ff⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Tactic:
cases e₁

Result:
case mk.refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
g₁' : P.last.B a' → P.last.M
e₁' : he₁' = ⟨a', g₁'⟩
ef : splitFun f' f₁' = splitFun (pathDestLeft P e₁' f₁) fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩