awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))
u v : (P F).M α
cuv : Mcongr (F := F) (α := α) u v
a₁ : r (Quot.mk (Mcongr (F := F) (α := α)) v) (Quot.mk (Mcongr (F := F) (α := α)) v)
⊢ r (Quot.mk (Mcongr (F := F) (α := α)) u) (Quot.mk (Mcongr (F := F) (α := α)) v)

Tactic:
rw [Quot.sound cuv]

Premises used: Quot.sound
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))
u v : (P F).M α
cuv : Mcongr (F := F) (α := α) u v
⊢ r (Quot.mk (Mcongr (F := F) (α := α)) v) (Quot.mk (Mcongr (F := F) (α := α)) v)

Tactic:
apply h'
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))
⊢ ∀ (u v : (P F).M α), Mcongr (F := F) (α := α) u v → Quot.mk r' u = Quot.mk r' v

Tactic:
have h₁ : ∀ u v : q.P.M α, Mcongr u v → Quot.mk r' u = Quot.mk r' v := by
      intro u v cuv
      apply Quot.sound
      dsimp [r', hr']
      rw [Quot.sound cuv]
      apply h'
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))
h₁ : ∀ (u v : (P F).M α), Mcongr (F := F) (α := α) u v → Quot.mk r' u = Quot.mk r' v
c : Cofix F α
apply :
  ∀ (a : (P F).M α) (b : Cofix F α),
    r (Quot.mk (Mcongr (F := F) (α := α)) a) b →
      Quot.lift (r := Mcongr (F := F) (α := α)) (Quot.mk r') h₁ (Quot.mk (Mcongr (F := F) (α := α)) a) =
        Quot.lift (r := Mcongr (F := F) (α := α)) (Quot.mk r') h₁ b
⊢ ∀ (b : Cofix F α) (a : r c b),
    Quot.lift (r := Mcongr (F := F) (α := α)) (Quot.mk r') h₁ c =
      Quot.lift (r := Mcongr (F := F) (α := α)) (Quot.mk r') h₁ b

Tactic:
apply Quot.inductionOn
            (motive := fun c =>
              ∀ b, r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b) c

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))
h₁ : ∀ (u v : (P F).M α), Mcongr (F := F) (α := α) u v → Quot.mk r' u = Quot.mk r' v
c : (P F).M α
d : Cofix F α
apply :
  ∀ (a : (P F).M α),
    r (Quot.mk (Mcongr (F := F) (α := α)) c) (Quot.mk (Mcongr (F := F) (α := α)) a) →
      Quot.lift (r := Mcongr (F := F) (α := α)) (Quot.mk r') h₁ (Quot.mk (Mcongr (F := F) (α := α)) c) =
        Quot.lift (r := Mcongr (F := F) (α := α)) (Quot.mk r') h₁ (Quot.mk (Mcongr (F := F) (α := α)) a)
⊢ r (Quot.mk (Mcongr (F := F) (α := α)) c) d →
    Quot.lift (r := Mcongr (F := F) (α := α)) (Quot.mk r') h₁ (Quot.mk (Mcongr (F := F) (α := α)) c) =
      Quot.lift (r := Mcongr (F := F) (α := α)) (Quot.mk r') h₁ d

Tactic:
apply Quot.inductionOn
            (motive := fun d => r (Quot.mk Mcongr c) d →
              Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d) d

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))
h₁ : ∀ (u v : (P F).M α), Mcongr (F := F) (α := α) u v → Quot.mk r' u = Quot.mk r' v
c d : (P F).M α
rcd : r (Quot.mk (Mcongr (F := F) (α := α)) c) (Quot.mk (Mcongr (F := F) (α := α)) d)
a₁ : r' c d
⊢ Quot.lift (r := Mcongr (F := F) (α := α)) (Quot.mk r') h₁ (Quot.mk (Mcongr (F := F) (α := α)) c) =
    Quot.lift (r := Mcongr (F := F) (α := α)) (Quot.mk r') h₁ (Quot.mk (Mcongr (F := F) (α := α)) d)

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))
h₁ : ∀ (u v : (P F).M α), Mcongr (F := F) (α := α) u v → Quot.mk r' u = Quot.mk r' v
c d : (P F).M α
rcd : r (Quot.mk (Mcongr (F := F) (α := α)) c) (Quot.mk (Mcongr (F := F) (α := α)) d)
⊢ r' c d

Tactic:
apply rcd
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) b))
h₁ : ∀ (u v : (P F).M α), Mcongr (F := F) (α := α) u v → Quot.mk r' u = Quot.mk r' v
f : Quot r → Quot r' := Quot.lift (r := r) (Quot.lift (r := Mcongr (F := F) (α := α)) (Quot.mk r') h₁) ⋯
⊢ f ∘ Quot.mk r ∘ Quot.mk (Mcongr (F := F) (α := α)) = Quot.mk r'

Tactic:
have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
⊢ IsPrecongr (F := F) (α := α) r'

Tactic:
have : IsPrecongr r' := by
    intro a b r'ab
    have h₀ :
      appendFun id (Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest q.P a) =
        appendFun id (Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest q.P b) := by
      rw [appendFun_comp_id, comp_map, comp_map]; exact h _ _ r'ab
    have h₁ : ∀ u v : q.P.M α, Mcongr u v → Quot.mk r' u = Quot.mk r' v := by
      intro u v cuv
      apply Quot.sound
      dsimp [r', hr']
      rw [Quot.sound cuv]
      apply h'
    let f : Quot r → Quot r' :=
      Quot.lift (Quot.lift (Quot.mk r') h₁)
        (by
          intro c
          apply Quot.inductionOn
            (motive := fun c =>
              ∀ b, r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b) c
          clear c
          intro c d
          apply Quot.inductionOn
            (motive := fun d => r (Quot.mk Mcongr c) d →
              Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d) d
          clear d
          intro d rcd; apply Quot.sound; apply rcd)
    have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl
    rw [← this, appendFun_comp_id, q.P.comp_map, q.P.comp_map, abs_map, abs_map, abs_map, abs_map,
      h₀]
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
this : IsPrecongr (F := F) (α := α) r'
⊢ Mcongr (F := F) (α := α) x y

Tactic:
⟨r', this, rxy⟩

Premises used: MvQPF.Mcongr, And.intro, Exists.intro
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
x y : (P F).M α
rxy : r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
r' : (x y : (P F).M α) → Prop :=
  fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
hr' : r' = fun (x y : (P F).M α) ↦ r (Quot.mk (Mcongr (F := F) (α := α)) x) (Quot.mk (Mcongr (F := F) (α := α)) y)
this : IsPrecongr (F := F) (α := α) r'
⊢ Mcongr (F := F) (α := α) x y

Tactic:
exact ⟨r', this, rxy⟩
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x y : Cofix F α
rxy : r x y
h' : ∀ (x : Cofix F α), r' x x
h₁ :
  ∀ (x y : Cofix F α),
    r' x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r')
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r')) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r')
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r')) (y.dest (F := F) (α := α))
a : r' x y
⊢ x = y

Tactic:
apply Cofix.bisim_aux r'

Premises used: _private.0.MvQPF.Cofix.bisim_aux
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x_1 y : Cofix F α
rxy : r x_1 y
x : Cofix F α
h' : x = x
⊢ r' x x

Tactic:
left
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x_1 y : Cofix F α
rxy : r x_1 y
x : Cofix F α
⊢ x = x

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h_1 :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F α
rxy : r x_1 y_1
x y : Cofix F α
h : x = y
h₁ h₂ :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r')
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r')) (y.dest (F := F) (α := α)) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r')
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r')) (y.dest (F := F) (α := α))
⊢ MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r')
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r')) (x.dest (F := F) (α := α)) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r')
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r')) (y.dest (F := F) (α := α))

Tactic:
rw [h]
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h :
  ∀ (x y : Cofix F α),
    r x y →
      MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α)) =
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))
r' : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F α
rxy : r x_1 y_1
x y : Cofix F α
r'xy : r x y
⊢ ∀ (x y : Cofix F α), r x y → r' x y

Tactic:
have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h