-- 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 : 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'))),
    (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f))).head =
        (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))).head ∧
      ∃ (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'))
i : F.B a
hh :
  IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨
    IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₀ f₀)
a₁ : F.A
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₁))
h' : f' i = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₁ f₁)
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₁)))
    (h' : f' i = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₀ f₁)),
    (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₀ f₀))).head =
        (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₀ f₁))).head ∧
      ∃ (a : F.A) (f : F.B a → F.M) (f' : F.B a → 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 f) ∧
          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 f') ∧
            ∀ (i : F.B a), R (f i) (f' i)
⊢ (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₀ f₀))).head =
      (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₁ f₁))).head ∧
    ∃ (a : F.A) (f : F.B a → F.M) (f' : F.B a → 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 f) ∧
        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 f') ∧
          ∀ (i : F.B a), R (f i) (f' i)

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

Premises used: PFunctor.M.IsBisimulation.head, rfl