case h
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
⊢ f x = M.corec g x
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
⊢ f = M.corec g
ext x
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
⊢ ∀ (x : α),
    (fun x => True) x →
      ∃ a f_1 f',
        dest (f x) = { fst := a, snd := f_1 } ∧
          dest (M.corec g x) = { fst := a, snd := f' } ∧
            ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
case h
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
⊢ f x = M.corec g x
apply bisim' (fun _ => True) _ _ _ _ trivial
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
⊢ ∀ (x : α),
    (fun x => True) x →
      ∃ a f_1 f',
        dest (f x) = { fst := a, snd := f_1 } ∧
          dest (M.corec g x) = { fst := a, snd := f' } ∧
            ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
⊢ ∀ (x : α),
    (fun x => True) x →
      ∃ a f_1 f',
        dest (f x) = { fst := a, snd := f_1 } ∧
          dest (M.corec g x) = { fst := a, snd := f' } ∧
            ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
clear x
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
⊢ ∃ a f_1 f',
    dest (f x) = { fst := a, snd := f_1 } ∧
      dest (M.corec g x) = { fst := a, snd := f' } ∧
        ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
⊢ ∀ (x : α),
    (fun x => True) x →
      ∃ a f_1 f',
        dest (f x) = { fst := a, snd := f_1 } ∧
          dest (M.corec g x) = { fst := a, snd := f' } ∧
            ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
intro x _
case mk
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
⊢ ∃ a f_1 f',
    dest (f x) = { fst := a, snd := f_1 } ∧
      dest (M.corec g x) = { fst := a, snd := f' } ∧
        ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
⊢ ∃ a f_1 f',
    dest (f x) = { fst := a, snd := f_1 } ∧
      dest (M.corec g x) = { fst := a, snd := f' } ∧
        ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
cases' gxeq : g x with a f'
case mk
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
⊢ ∃ a f_1 f',
    dest (f x) = { fst := a, snd := f_1 } ∧
      dest (M.corec g x) = { fst := a, snd := f' } ∧
        ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
case mk
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
⊢ ∃ a f_1 f',
    dest (f x) = { fst := a, snd := f_1 } ∧
      dest (M.corec g x) = { fst := a, snd := f' } ∧
        ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
have h₀ : M.dest (f x) = ⟨a, f ∘ f'⟩ := by rw [hyp, gxeq, PFunctor.map_eq]
case mk
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
h₁ : dest (M.corec g x) = { fst := a, snd := M.corec g ∘ f' }
⊢ ∃ a f_1 f',
    dest (f x) = { fst := a, snd := f_1 } ∧
      dest (M.corec g x) = { fst := a, snd := f' } ∧
        ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
case mk
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
⊢ ∃ a f_1 f',
    dest (f x) = { fst := a, snd := f_1 } ∧
      dest (M.corec g x) = { fst := a, snd := f' } ∧
        ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
have h₁ : M.dest (M.corec g x) = ⟨a, M.corec g ∘ f'⟩ := by rw [dest_corec, gxeq, PFunctor.map_eq]
case mk
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
h₁ : dest (M.corec g x) = { fst := a, snd := M.corec g ∘ f' }
⊢ ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'
case mk
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
h₁ : dest (M.corec g x) = { fst := a, snd := M.corec g ∘ f' }
⊢ ∃ a f_1 f',
    dest (f x) = { fst := a, snd := f_1 } ∧
      dest (M.corec g x) = { fst := a, snd := f' } ∧
        ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
refine' ⟨_, _, _, h₀, h₁, _⟩
case mk
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
h₁ : dest (M.corec g x) = { fst := a, snd := M.corec g ∘ f' }
i : B P a
⊢ ∃ x', (fun x => True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'
case mk
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
h₁ : dest (M.corec g x) = { fst := a, snd := M.corec g ∘ f' }
⊢ ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'
intro i
no goals
case mk
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
h₁ : dest (M.corec g x) = { fst := a, snd := M.corec g ∘ f' }
i : B P a
⊢ ∃ x', (fun x => True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'
exact ⟨f' i, trivial, rfl, rfl⟩
no goals
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
⊢ dest (f x) = { fst := a, snd := f ∘ f' }
rw [hyp, gxeq, PFunctor.map_eq]
no goals
F : PFunctor
X : Type ?u.75905
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
⊢ dest (M.corec g x) = { fst := a, snd := M.corec g ∘ f' }
rw [dest_corec, gxeq, PFunctor.map_eq]