F : PFunctor
X : Type ?u.72703
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
x y : M P
h' : R x y
⊢ x = y
F : PFunctor
X : Type ?u.72703
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
⊢ ∀ (x y : M P), R x y → x = y
introv h'
F : PFunctor
X : Type ?u.72703
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
x y : M P
h' : R x y
this : Inhabited P.A
⊢ x = y
F : PFunctor
X : Type ?u.72703
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
x y : M P
h' : R x y
⊢ x = y
haveI := Inhabited.mk x.head
F : PFunctor
X : Type ?u.72703
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
x y : M P
h' : R x y
this : Inhabited P.A
⊢ IsBisimulation R
F : PFunctor
X : Type ?u.72703
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
x y : M P
h' : R x y
this : Inhabited P.A
⊢ x = y
apply eq_of_bisim R _ _ _ h'
F : PFunctor
X : Type ?u.72703
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
this : Inhabited P.A
⊢ IsBisimulation R
F : PFunctor
X : Type ?u.72703
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
x y : M P
h' : R x y
this : Inhabited P.A
⊢ IsBisimulation R
clear h' x y
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₀ : dest (M.mk { fst := a, snd := f }) = { fst := a'', snd := g }
h₁ : dest (M.mk { fst := a', snd := f' }) = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
⊢ a = a'

case tail.intro.intro.intro.intro.intro
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
a'' : P.A
g g' : B P a'' → M P
h₀ : dest (M.mk { fst := a, snd := f }) = { fst := a'', snd := g }
h₁ : dest (M.mk { fst := a, snd := f' }) = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
⊢ R (f i) (f' i)
F : PFunctor
X : Type ?u.72703
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
this : Inhabited P.A
⊢ IsBisimulation R
constructor <;> introv ih <;> rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩ <;> clear h
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₁ : dest (M.mk { fst := a', snd := f' }) = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
h₀ : (dest (M.mk { fst := a, snd := f })).fst = { fst := a'', snd := g }.fst
⊢ a = a'
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₀ : dest (M.mk { fst := a, snd := f }) = { fst := a'', snd := g }
h₁ : dest (M.mk { fst := a', snd := f' }) = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
⊢ a = a'
replace h₀ := congr_arg Sigma.fst h₀
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₂ : ∀ (i : B P a''), R (g i) (g' i)
h₀ : (dest (M.mk { fst := a, snd := f })).fst = { fst := a'', snd := g }.fst
h₁ : (dest (M.mk { fst := a', snd := f' })).fst = { fst := a'', snd := g' }.fst
⊢ a = a'
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₁ : dest (M.mk { fst := a', snd := f' }) = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
h₀ : (dest (M.mk { fst := a, snd := f })).fst = { fst := a'', snd := g }.fst
⊢ a = a'
replace h₁ := congr_arg Sigma.fst h₁
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₂ : ∀ (i : B P a''), R (g i) (g' i)
h₀ : a = a''
h₁ : a' = a''
⊢ a = a'
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₂ : ∀ (i : B P a''), R (g i) (g' i)
h₀ : (dest (M.mk { fst := a, snd := f })).fst = { fst := a'', snd := g }.fst
h₁ : (dest (M.mk { fst := a', snd := f' })).fst = { fst := a'', snd := g' }.fst
⊢ a = a'
simp only [dest_mk] at h₀ h₁
no goals
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₂ : ∀ (i : B P a''), R (g i) (g' i)
h₀ : a = a''
h₁ : a' = a''
⊢ a = a'
rw [h₀, h₁]
case tail.intro.intro.intro.intro.intro
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
a'' : P.A
g g' : B P a'' → M P
h₀ : { fst := a, snd := f } = { fst := a'', snd := g }
h₁ : { fst := a, snd := f' } = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
⊢ R (f i) (f' i)
case tail.intro.intro.intro.intro.intro
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
a'' : P.A
g g' : B P a'' → M P
h₀ : dest (M.mk { fst := a, snd := f }) = { fst := a'', snd := g }
h₁ : dest (M.mk { fst := a, snd := f' }) = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
⊢ R (f i) (f' i)
simp only [dest_mk] at h₀ h₁
case tail.intro.intro.intro.intro.intro.refl
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
g' : B P a → M P
h₁ : { fst := a, snd := f' } = { fst := a, snd := g' }
h₂ : ∀ (i : B P a), R (f i) (g' i)
⊢ R (f i) (f' i)
case tail.intro.intro.intro.intro.intro
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
a'' : P.A
g g' : B P a'' → M P
h₀ : { fst := a, snd := f } = { fst := a'', snd := g }
h₁ : { fst := a, snd := f' } = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
⊢ R (f i) (f' i)
cases h₀
case tail.intro.intro.intro.intro.intro.refl.refl
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
h₂ : ∀ (i : B P a), R (f i) (f' i)
⊢ R (f i) (f' i)
case tail.intro.intro.intro.intro.intro.refl
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
g' : B P a → M P
h₁ : { fst := a, snd := f' } = { fst := a, snd := g' }
h₂ : ∀ (i : B P a), R (f i) (g' i)
⊢ R (f i) (f' i)
cases h₁
no goals
case tail.intro.intro.intro.intro.intro.refl.refl
F : PFunctor
X : Type ?u.72703
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
h₂ : ∀ (i : B P a), R (f i) (f' i)
⊢ R (f i) (f' i)
apply h₂