-- Mathlib/Data/PFunctor/Multivariate/M.lean
theorem M.bisim' {α : TypeVec n} (R : P.M α → P.M α → Prop)
    (h : ∀ x y, R x y → (id ::: Quot.mk R) <$$> M.dest _ x = (id ::: Quot.mk R) <$$> M.dest _ y)
    (x y) (r : R x y) : x = y

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ x = y

Tactic:
have := M.bisim₀ P (Relation.EqvGen R) ?_ ?_

Result:
case refine_3
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
this : ∀ (x y : P.M α), Relation.EqvGen R x y → x = y
⊢ x = y

case refine_1
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ Equivalence (Relation.EqvGen R)

case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ ∀ (x y : P.M α),
    Relation.EqvGen R x y →
      (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
        (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y

Proof state:
case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
Hr : Relation.EqvGen R x y
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y

Tactic:
have : ∀ x y, R x y → Relation.EqvGen R x y := @Relation.EqvGen.rel _ R

Result:
case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
Hr : Relation.EqvGen R x y
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y

Proof state:
case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∀ (x y : P.M α),
    Relation.EqvGen R x y →
      (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
        (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y

Tactic:
introv Hr

Result:
case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
Hr : Relation.EqvGen R x y
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y

Proof state:
case refine_3
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
this : ∀ (x y : P.M α), Relation.EqvGen R x y → x = y
⊢ x = y

Tactic:
solve_by_elim [Relation.EqvGen.rel]

Result:
no goals

Proof state:
case refine_1
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ Equivalence (Relation.EqvGen R)

Tactic:
apply Relation.EqvGen.is_equivalence

Result:
no goals

Proof state:
case refine_2.rel
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.factor R (Relation.EqvGen R) this ∘ Quot.mk R) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.factor R (Relation.EqvGen R) this ∘ Quot.mk R) <$$> dest P y✝

Tactic:
rwa [appendFun_comp_id, ← MvFunctor.map_map, ← MvFunctor.map_map, h]

Result:
no goals