-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem bisim (R : M P → M P → Prop)
    (h : ∀ x y, R x y → ∃ a f f', M.dest x = ⟨a, f⟩ ∧ M.dest y = ⟨a, f'⟩ ∧ ∀ i, R (f i) (f' i)) :
    ∀ x y, R x y → x = y

Proof state:
P : PFunctor.{u}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
x y : P.M
h' : R x y
this : Inhabited P.A
⊢ x = y

Tactic:
apply eq_of_bisim R _ _ _ h'

Result:
P : PFunctor.{u}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
x y : P.M
h' : R x y
this : Inhabited P.A
⊢ IsBisimulation R

Proof state:
P : PFunctor.{u}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
x y : P.M
h' : R x y
this : Inhabited P.A
⊢ IsBisimulation R

Tactic:
clear h' x y

Result:
P : PFunctor.{u}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
⊢ IsBisimulation R

Proof state:
case tail.intro.intro.intro.intro.intro.refl.refl
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
h₂ : ∀ (i : P.B a), R (f i) (f' i)
⊢ R (f i) (f' i)

Tactic:
apply h₂

Result:
no goals

Proof state:
case head.intro.intro.intro.intro.intro
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a', f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ a = a'

Tactic:
replace h₀ := congr_arg Sigma.fst h₀

Result:
case head.intro.intro.intro.intro.intro
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₁ : (M.mk ⟨a', f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ : (M.mk ⟨a, f⟩).dest.fst = ⟨a'', g⟩.fst
⊢ a = a'

Proof state:
case head.intro.intro.intro.intro.intro
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₁ : (M.mk ⟨a', f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ : (M.mk ⟨a, f⟩).dest.fst = ⟨a'', g⟩.fst
⊢ a = a'

Tactic:
replace h₁ := congr_arg Sigma.fst h₁

Result:
case head.intro.intro.intro.intro.intro
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ : (M.mk ⟨a, f⟩).dest.fst = ⟨a'', g⟩.fst
h₁ : (M.mk ⟨a', f'⟩).dest.fst = ⟨a'', g'⟩.fst
⊢ a = a'

Proof state:
P : PFunctor.{u}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
⊢ IsBisimulation R

Tactic:
constructor <;> introv ih <;> rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩ <;> clear h

Result:
case head.intro.intro.intro.intro.intro
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a', f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ a = a'

case tail.intro.intro.intro.intro.intro
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a, f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)

Proof state:
case tail.intro.intro.intro.intro.intro
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ : ⟨a, f⟩ = ⟨a'', g⟩
h₁ : ⟨a, f'⟩ = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)

Tactic:
cases h₀

Result:
case tail.intro.intro.intro.intro.intro.refl
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
g' : P.B a → P.M
h₁ : ⟨a, f'⟩ = ⟨a, g'⟩
h₂ : ∀ (i : P.B a), R (f i) (g' i)
⊢ R (f i) (f' i)

Proof state:
case tail.intro.intro.intro.intro.intro.refl
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
g' : P.B a → P.M
h₁ : ⟨a, f'⟩ = ⟨a, g'⟩
h₂ : ∀ (i : P.B a), R (f i) (g' i)
⊢ R (f i) (f' i)

Tactic:
cases h₁

Result:
case tail.intro.intro.intro.intro.intro.refl.refl
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
h₂ : ∀ (i : P.B a), R (f i) (f' i)
⊢ R (f i) (f' i)

Proof state:
case tail.intro.intro.intro.intro.intro
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a, f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)

Tactic:
simp only [dest_mk] at h₀ h₁

Result:
case tail.intro.intro.intro.intro.intro
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ : ⟨a, f⟩ = ⟨a'', g⟩
h₁ : ⟨a, f'⟩ = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)

Proof state:
case head.intro.intro.intro.intro.intro
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ : a = a''
h₁ : a' = a''
⊢ a = a'

Tactic:
rw [h₀, h₁]

Result:
no goals

Proof state:
P : PFunctor.{u}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
⊢ ∀ (x y : P.M), R x y → x = y

Tactic:
introv h'

Result:
P : PFunctor.{u}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
x y : P.M
h' : R x y
⊢ x = y

Proof state:
P : PFunctor.{u}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
x y : P.M
h' : R x y
⊢ x = y

Tactic:
haveI := Inhabited.mk x.head

Result:
P : PFunctor.{u}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
x y : P.M
h' : R x y
this : Inhabited P.A
⊢ x = y

Proof state:
case head.intro.intro.intro.intro.intro
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ : (M.mk ⟨a, f⟩).dest.fst = ⟨a'', g⟩.fst
h₁ : (M.mk ⟨a', f'⟩).dest.fst = ⟨a'', g'⟩.fst
⊢ a = a'

Tactic:
simp only [dest_mk] at h₀ h₁

Result:
case head.intro.intro.intro.intro.intro
P : PFunctor.{u}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ : a = a''
h₁ : a' = a''
⊢ a = a'