-- 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
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)
y : P.M α
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
r : R ⟨a₁, f₁⟩ y
⊢ ⟨a₁, f₁⟩ = y

Tactic:
obtain ⟨a₂, f₂⟩ := y

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₂⟩
⊢ ⟨a₁, f₁⟩ = ⟨a₂, f₂⟩

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

Tactic:
subst this

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₁ f₂ : P.mp.B a₁ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₁, f₂⟩
⊢ ⟨a₁, f₁⟩ = ⟨a₁, f₂⟩

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

Tactic:
exact ⟨_, _, _, rfl, rfl, fun b => ⟨_, _, h' b, rfl, rfl⟩⟩

Result:
no goals

Proof state:
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)

Tactic:
exact (congr_fun (congr_fun e₃ i) c :)

Result:
no goals

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₂⟩
⊢ ∀ (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)

Tactic:
rintro _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩

Result:
case intro.mk.intro.mk.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 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)
x y : P.M α
r : R x y
⊢ x = y

Tactic:
obtain ⟨a₁, f₁⟩ := x

Result:
case 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)
y : P.M α
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
r : R ⟨a₁, f₁⟩ y
⊢ ⟨a₁, f₁⟩ = y

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₁ f₂ : P.mp.B a₁ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₁, f₂⟩
⊢ ⟨a₁, f₁⟩ = ⟨a₁, f₂⟩

Tactic:
congr with (i p)

Result:
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

Proof state:
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)

Tactic:
exact IH _ _ (h'' _)

Result:
no goals