-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Inhabited F.M
inst_1 : DecidableEq F.A
bisim : IsBisimulation R
ps : Path F
a : F.A
f f' : F.B a → F.M
h₀ :
  R (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))
hh :
  IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨
    IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))
f₁ :
  ∀ (i : F.Idx) (ps : List F.Idx)
    (ps_ih :
      ∀ (a : F.A) (f f' : F.B a → F.M)
        (h₀ :
          R (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f))
            (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f')))
        (hh :
          IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨
            IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))),
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
            iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f')) ∧
          ∃ (a_1 : F.A) (f_1 : F.B a_1 → F.M) (f'_1 : F.B a_1 → F.M),
            isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
                M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1) ∧
              isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f')) =
                  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) 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 (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f))
        (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f')))
    (hh :
      IsPath (i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨
        IsPath (i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))),
    iselect (i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
        iselect (i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f')) ∧
      ∃ (a_1 : F.A) (f_1 : F.B a_1 → F.M) (f'_1 : F.B a_1 → F.M),
        isubtree (i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
            M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1) ∧
          isubtree (i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f')) =
              M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f'_1) ∧
            ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
⊢ iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f')) ∧
    ∃ (a_1 : F.A) (f_1 : F.B a_1 → F.M) (f'_1 : F.B a_1 → F.M),
      isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
          M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1) ∧
        isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f')) =
            M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f'_1) ∧
          ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)

Tactic:
induction ps generalizing a f f' with
  | nil =>
    exists rfl, a, f, f', rfl, rfl
    apply bisim.tail h₀
  | cons i ps ps_ih => ?_

Premises used: PFunctor.M.IsBisimulation.tail, List.cons, rfl, List.nil