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
β : Type u
g : β → F (α ::: β)
x : β
rw :
  M.dest (P F) (α := α) (M.corec (P F) (α := α) (fun (x : β) ↦ repr (F := F) (α := α ::: β) (g x)) x) =
    MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: (P F).M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (M.corec (P F) (α := α) fun (x : β) ↦ repr (F := F) (α := α ::: β) (g x)))
      (repr (F := F) (α := α ::: β) (g x))
rw₁ rw₂ :
  Eq (α := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: (P F).M α))
    (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: (P F).M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (M.corec (P F) (α := α) fun (x : β) ↦ repr (F := F) (α := α ::: β) (g x)))
      (repr (F := F) (α := α ::: β) (g x)))
    (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: (P F).M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (M.corec (P F) (α := α) fun (x : β) ↦ repr (F := F) (α := α ::: β) (g x)))
      (repr (F := F) (α := α ::: β) (g x)))
⊢ M.dest (P F) (α := α) (corecF (F := F) (α := α) g x) =
    MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: (P F).M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corecF (F := F) (α := α) g))
      (repr (F := F) (α := α ::: β) (g x))

Tactic:
rw [corecF, M.dest_corec]

Premises used: MvQPF.corecF, MvPFunctor.M.dest_corec
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂ : r aa₁ aa₂
a :
  Mcongr (F := F) (α := β) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁)
    (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)
⊢ Eq.{u + 1} (α := Cofix F β)
    ((fun (x : (P F).M α) ↦
        (Quot.mk (Mcongr (F := F) (α := β)) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) :
          Quot (α := (P F).M β) (Mcongr (F := F) (α := β))))
      aa₁)
    ((fun (x : (P F).M α) ↦
        (Quot.mk (Mcongr (F := F) (α := β)) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) :
          Quot (α := (P F).M β) (Mcongr (F := F) (α := β))))
      aa₂)

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
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂ : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
h :
  IsPrecongr (F := F) (α := β) r' ∧
    r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)
⊢ Mcongr (F := F) (α := β) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁)
    (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)

Tactic:
use r'
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂ : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
h : IsPrecongr (F := F) (α := β) r'
h₁ : r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)
⊢ IsPrecongr (F := F) (α := β) r' ∧
    r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁_1 a₂_1 : (P F).M α
ra₁a₂_2 : r a₁_1 a₂_1
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁_1
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂_1
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
a : r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂)
⊢ Eq.{u + 1} (α := Quot r') ((fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) a₁)
    ((fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) a₂)

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
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁_1 a₂_1 : (P F).M α
ra₁a₂_2 : r a₁_1 a₂_1
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁_1
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂_1
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
⊢ r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂)

Tactic:
⟨a₁, a₂, ra₁a₂, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁_1 a₂_1 : (P F).M α
ra₁a₂_2 : r a₁_1 a₂_1
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁_1
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂_1
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
⊢ r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂)

Tactic:
exact ⟨a₁, a₂, ra₁a₂, rfl, rfl⟩
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
u : Quot r → Quot r' :=
  Quot.lift (r := r) (fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) ⋯
h :
  ∀ (x : (P F).M α),
    (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) x = (u ∘ Quot.mk r) x
⊢ (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) = u ∘ Quot.mk r

Tactic:
ext x
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
u : Quot r → Quot r' :=
  Quot.lift (r := r) (fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) ⋯
x : (P F).M α
⊢ (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) x = (u ∘ Quot.mk r) 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
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
u : Quot r → Quot r' :=
  Quot.lift (r := r) (fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) ⋯
⊢ (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) = u ∘ Quot.mk r

Tactic:
have hu : (Quot.mk r' ∘ fun x : q.P.M α => g <$$> x) = u ∘ Quot.mk r := by
          ext x
          rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
u : Quot r → Quot r' :=
  Quot.lift (r := r) (fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) ⋯
hu : (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) = u ∘ Quot.mk r
h :
  abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := β ::: (P F).M β) (γ := β ::: Quot r')
          (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r'))
          (appendFun (α := α) (α' := β) g fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x))
        (M.dest (P F) (α := α) a₁)) =
    abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := β ::: (P F).M β) (γ := β ::: Quot r')
          (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r'))
          (appendFun (α := α) (α' := β) g fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x))
        (M.dest (P F) (α := α) a₂))
⊢ abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := β ::: (P F).M β) (β := β ::: Quot r')
        (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r')) (M.dest (P F) (α := β) b₁)) =
    abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := β ::: (P F).M β) (β := β ::: Quot r')
        (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r')) (M.dest (P F) (α := β) b₂))

Tactic:
rw [b₁eq, b₂eq, M.dest_map, M.dest_map, ← q.P.comp_map, ← q.P.comp_map]

Premises used: MvPFunctor.comp_map, MvPFunctor.M.dest_map, MvQPF.P
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂_1 : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁
b₂eq : b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
u : Quot r → Quot r' :=
  Quot.lift (r := r) (fun (x : (P F).M α) ↦ Quot.mk r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g x)) ⋯
hu : (Quot.mk r' ∘ fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x) = u ∘ Quot.mk r
h :
  abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := α ::: Quot r) (γ := β ::: Quot r') (appendFun (α := α) (α' := β) g u)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
        (M.dest (P F) (α := α) a₁)) =
    abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := α ::: Quot r) (γ := β ::: Quot r') (appendFun (α := α) (α' := β) g u)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
        (M.dest (P F) (α := α) a₂))
⊢ abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := β ::: (P F).M β) (γ := β ::: Quot r')
          (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r'))
          (appendFun (α := α) (α' := β) g fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x))
        (M.dest (P F) (α := α) a₁)) =
    abs (F := F) (α := β ::: Quot r')
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).M α) (β := β ::: Quot r')
        (TypeVec.comp (α := α ::: (P F).M α) (β := β ::: (P F).M β) (γ := β ::: Quot r')
          (appendFun (α := β) (α' := β) (TypeVec.id (α := β)) (Quot.mk r'))
          (appendFun (α := α) (α' := β) g fun (x : (P F).M α) ↦ MvFunctor.map (F := (P F).M) (α := α) (β := β) g x))
        (M.dest (P F) (α := α) a₂))

Tactic:
rw [← appendFun_comp, id_comp, hu, ← comp_id g, appendFun_comp]

Premises used: TypeVec.appendFun_comp, TypeVec.comp_id, TypeVec.id_comp
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂ : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
⊢ r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)

Tactic:
⟨aa₁, aa₂, ra₁a₂, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
ra₁a₂ : r aa₁ aa₂
r' : (b₁ b₂ : (P F).M β) → Prop :=
  fun (b₁ b₂ : (P F).M β) ↦
    ∃ (a₁ : (P F).M α) (a₂ : (P F).M α),
      r a₁ a₂ ∧
        b₁ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₁ ∧
          b₂ = MvFunctor.map (F := (P F).M) (α := α) (β := β) g a₂
⊢ r' (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₁) (MvFunctor.map (F := (P F).M) (α := α) (β := β) g aa₂)

Tactic:
exact ⟨aa₁, aa₂, ra₁a₂, rfl, rfl⟩
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
dsimp :
  Eq (α := F (α ::: Cofix F α))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y)))
⊢ Eq.{u + 1} (α := F (α ::: Cofix F α))
    ((fun (x : (P F).M α) ↦
        (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
            (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) :
          F (α ::: Cofix F α)))
      x)
    ((fun (x : (P F).M α) ↦
        (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
            (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) :
          F (α ::: Cofix F α)))
      y)

Tactic:
dsimp
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 y_1 : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x_1 y_1
x y : (P F).M α
h : r x y
⊢ Mcongr (F := F) (α := α) x y

Tactic:
⟨r, pr, h⟩

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
x_1 y_1 : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x_1 y_1
x y : (P F).M α
h : r x y
⊢ Mcongr (F := F) (α := α) x y

Tactic:
exact ⟨r, pr, h⟩
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
⊢ ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y

Tactic:
have : ∀ x y, r x y → Mcongr x y := by
        intro x y h
        exact ⟨r, pr, h⟩
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y
rw :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
⊢ Eq (α := F (α ::: Cofix F α))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y)))

Tactic:
rw [← Quot.factor_mk_eq _ _ this]

Premises used: Quot.factor_mk_eq
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y
lhs :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
    (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x))
| MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))

Tactic:
lhs
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y
rw :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
    (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
| MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
    (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x))

Tactic:
rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map,
          ← appendFun_comp_id]

Premises used: MvQPF.comp_map, MvQPF.abs_map, TypeVec.appendFun_comp_id
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr (F := F) (α := α) r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr (F := F) (α := α) x y
rw :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
    (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))
| MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)) =
    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (Mcongr (F := F) (α := α)) this ∘ Quot.mk r))
      (abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) y))

Tactic:
lhs
        rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map,
          ← appendFun_comp_id]

Premises used: MvQPF.comp_map, MvQPF.abs_map, TypeVec.appendFun_comp_id