-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem nth_of_bisim [Inhabited (M F)] (bisim : IsBisimulation R) (s₁ s₂) (ps : Path F) :
    (R s₁ s₂) →
      IsPath ps s₁ ∨ IsPath ps s₂ →
        iselect ps s₁ = iselect ps s₂ ∧
          ∃ (a : _) (f f' : F.B a → M F),
            isubtree ps s₁ = M.mk ⟨a, f⟩ ∧
              isubtree ps s₂ = M.mk ⟨a, f'⟩ ∧ ∀ i : F.B a, f i ~ f' i

Proof state:
case f.f.cons.mk.f.f
F : PFunctor.{u}
R : F.M → F.M → Prop
inst✝ : Inhabited F.M
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
h₁ : R (f i) (f' i)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
a₁ : F.A
f₁ : F.B a₁ → F.M
h' : f' i = M.mk ⟨a₁, f₁⟩
⊢ (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)

Tactic:
simp only [h, h', isubtree_cons] at ps_ih ⊢

Result:
case f.f.cons.mk.f.f
F : PFunctor.{u}
R : F.M → F.M → Prop
inst✝ : Inhabited F.M
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
h₁ : R (f i) (f' i)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
a₁ : F.A
f₁ : F.B a₁ → F.M
h' : f' i = M.mk ⟨a₁, f₁⟩
⊢ (isubtree ps (M.mk ⟨a₀, f₀⟩)).head = (isubtree ps (M.mk ⟨a₁, f₁⟩)).head ∧
    ∃ a f f',
      isubtree ps (M.mk ⟨a₀, f₀⟩) = M.mk ⟨a, f⟩ ∧
        isubtree ps (M.mk ⟨a₁, f₁⟩) = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)

Proof state:
case f.f.cons.mk.f.f
F : PFunctor.{u}
R : F.M → F.M → Prop
inst✝ : Inhabited F.M
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
a₁ : F.A
f₁ : F.B a₁ → F.M
h₁ : R (M.mk ⟨a₀, f₀⟩) (M.mk ⟨a₁, f₁⟩)
h' : f' i = M.mk ⟨a₁, f₁⟩
⊢ (isubtree ps (M.mk ⟨a₀, f₀⟩)).head = (isubtree ps (M.mk ⟨a₁, f₁⟩)).head ∧
    ∃ a f f',
      isubtree ps (M.mk ⟨a₀, f₀⟩) = M.mk ⟨a, f⟩ ∧
        isubtree ps (M.mk ⟨a₁, f₁⟩) = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)

Tactic:
obtain rfl : a₀ = a₁ := bisim.head h₁

Result:
case f.f.cons.mk.f.f
F : PFunctor.{u}
R : F.M → F.M → Prop
inst✝ : Inhabited F.M
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
f₁ : F.B a₀ → F.M
h₁ : R (M.mk ⟨a₀, f₀⟩) (M.mk ⟨a₀, f₁⟩)
h' : f' i = M.mk ⟨a₀, f₁⟩
⊢ (isubtree ps (M.mk ⟨a₀, f₀⟩)).head = (isubtree ps (M.mk ⟨a₀, f₁⟩)).head ∧
    ∃ a f f',
      isubtree ps (M.mk ⟨a₀, f₀⟩) = M.mk ⟨a, f⟩ ∧
        isubtree ps (M.mk ⟨a₀, f₁⟩) = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)

Proof state:
case f.f.cons.mk
F : PFunctor.{u}
R : F.M → F.M → Prop
inst✝ : Inhabited F.M
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
a' : F.A
i : F.B a'
hh : IsPath (⟨a', i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a', i⟩ :: ps) (M.mk ⟨a, f'⟩)
⊢ iselect (⟨a', i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect (⟨a', i⟩ :: ps) (M.mk ⟨a, f'⟩) ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a', i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a', i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)

Tactic:
obtain rfl : a = a' := by rcases hh with hh|hh <;> cases isPath_cons hh <;> rfl

Result:
case f.f.cons.mk
F : PFunctor.{u}
R : F.M → F.M → Prop
inst✝ : Inhabited F.M
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
⊢ iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)

Proof state:
case f
F : PFunctor.{u}
R : F.M → F.M → Prop
inst✝ : Inhabited F.M
bisim : IsBisimulation R
s₂ : F.M
ps : Path F
a : F.A
f : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) s₂
hh : IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps s₂
⊢ iselect ps (M.mk ⟨a, f⟩) = iselect ps s₂ ∧
    ∃ a_1 f_1 f',
      isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree ps s₂ = M.mk ⟨a_1, f'⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f' i)

Tactic:
induction' s₂ using PFunctor.M.casesOn' with a' f'

Result:
case f.f
F : PFunctor.{u}
R : F.M → F.M → Prop
inst✝ : Inhabited F.M
bisim : IsBisimulation R
ps : Path F
a : F.A
f : F.B a → F.M
a' : F.A
f' : F.B a' → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
hh : IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a', f'⟩)
⊢ iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a', f'⟩) ∧
    ∃ a_1 f_1 f'_1,
      isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree ps (M.mk ⟨a', f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)