-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem corec_unique (g : α → P α) (f : α → M P) (hyp : ∀ x, M.dest (f x) = P.map f (g x)) :
    f = M.corec g

Proof state:
case mk
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
have h₁ : M.dest (M.corec g x) = ⟨a, M.corec g ∘ f'⟩ := by rw [dest_corec, gxeq, PFunctor.map_eq]

Result:
case mk
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Proof state:
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
⊢ f = M.corec g

Tactic:
ext x

Result:
case h
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
⊢ f x = M.corec g x

Proof state:
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
⊢ ∀ (x : α),
    (fun x => True) x →
      ∃ a f_1 f',
        (f x).dest = ⟨a, f_1⟩ ∧
          (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
clear x

Result:
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
⊢ ∀ (x : α),
    (fun x => True) x →
      ∃ a f_1 f',
        (f x).dest = ⟨a, f_1⟩ ∧
          (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Proof state:
case h
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
⊢ f x = M.corec g x

Tactic:
apply bisim' (fun _ => True) _ _ _ _ trivial

Result:
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
⊢ ∀ (x : α),
    (fun x => True) x →
      ∃ a f_1 f',
        (f x).dest = ⟨a, f_1⟩ ∧
          (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Proof state:
case mk
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
have h₀ : M.dest (f x) = ⟨a, f ∘ f'⟩ := by rw [hyp, gxeq, PFunctor.map_eq]

Result:
case mk
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Proof state:
case mk
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
refine ⟨_, _, _, h₀, h₁, ?_⟩

Result:
case mk
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩
⊢ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'

Proof state:
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
⊢ (f x).dest = ⟨a, f ∘ f'⟩

Tactic:
rw [hyp, gxeq, PFunctor.map_eq]

Result:
no goals

Proof state:
case mk
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩
⊢ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'

Tactic:
intro i

Result:
case mk
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩
i : P.B a
⊢ ∃ x', (fun x => True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'

Proof state:
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
⊢ ∀ (x : α),
    (fun x => True) x →
      ∃ a f_1 f',
        (f x).dest = ⟨a, f_1⟩ ∧
          (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
intro x _

Result:
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Proof state:
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
rcases gxeq : g x with ⟨a, f'⟩

Result:
case mk
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Proof state:
case mk
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩
i : P.B a
⊢ ∃ x', (fun x => True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'

Tactic:
exact ⟨f' i, trivial, rfl, rfl⟩

Result:
no goals

Proof state:
P : PFunctor.{u}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
⊢ (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩

Tactic:
rw [dest_corec, gxeq, PFunctor.map_eq]

Result:
no goals