F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
⊢ ∀ (s₁ s₂ : M F), R s₁ s₂ → s₁ = s₂
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
⊢ ∀ (s₁ s₂ : M F), R s₁ s₂ → s₁ = s₂
inhabit M F
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
⊢ s₁ = s₂
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
⊢ ∀ (s₁ s₂ : M F), R s₁ s₂ → s₁ = s₂
introv Hr
case H
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
⊢ ∀ (ps : Path F), iselect ps s₁ = iselect ps s₂
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
⊢ s₁ = s₂
apply ext
case H
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
⊢ iselect ps s₁ = iselect ps s₂
case H
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
⊢ ∀ (ps : Path F), iselect ps s₁ = iselect ps s₂
introv
case pos
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂

case neg
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)
⊢ iselect ps s₁ = iselect ps s₂
case H
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
⊢ iselect ps s₁ = iselect ps s₂
by_cases h : IsPath ps s₁ ∨ IsPath ps s₂
case pos
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
H :
  iselect ps s₁ = iselect ps s₂ ∧
    ∃ a f f',
      isubtree ps s₁ = M.mk { fst := a, snd := f } ∧
        isubtree ps s₂ = M.mk { fst := a, snd := f' } ∧ ∀ (i : B F a), R (f i) (f' i)
⊢ iselect ps s₁ = iselect ps s₂
case pos
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
have H := nth_of_bisim R bisim _ _ ps Hr h
no goals
case pos
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
H :
  iselect ps s₁ = iselect ps s₂ ∧
    ∃ a f f',
      isubtree ps s₁ = M.mk { fst := a, snd := f } ∧
        isubtree ps s₂ = M.mk { fst := a, snd := f' } ∧ ∀ (i : B F a), R (f i) (f' i)
⊢ iselect ps s₁ = iselect ps s₂
exact H.left
case neg
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h : ¬IsPath ps s₁ ∧ ¬IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
case neg
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)
⊢ iselect ps s₁ = iselect ps s₂
rw [not_or] at h
case neg.intro
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h₀ : ¬IsPath ps s₁
h₁ : ¬IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
case neg
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h : ¬IsPath ps s₁ ∧ ¬IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
cases' h with h₀ h₁
no goals
case neg.intro
F : PFunctor
X : Type ?u.71783
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h₀ : ¬IsPath ps s₁
h₁ : ¬IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
simp only [iselect_eq_default, *, not_false_iff]