awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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) (α := α))
⊢ x = y
have a : r' x y
Tactic: apply Cofix.bisim_aux r'
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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 α
⊢ r' x x
have h' : x = x
Tactic: left
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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
⊢ 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) (α := α))
have 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) (α := α))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (hypothesis)
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
⊢ 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) (α := α))
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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
this : ∀ (x y : Cofix F α), r x y → 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) (α := α))
have h₁ : MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r')
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r r' this ∘ Quot.mk r))
    (x.dest (F := F) (α := α)) =
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r')
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r r' this ∘ Quot.mk r)) (y.dest (F := F) (α := α))
Tactic: rw [← Quot.factor_mk_eq _ _ this]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this ∘ Quot.mk r))
      (x.dest (F := F) (α := α)) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this ∘ Quot.mk r))
      (y.dest (F := F) (α := α))
have h₁ : MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
    (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: Quot r) (γ := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
    (x.dest (F := F) (α := α)) =
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
    (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: Quot r) (γ := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
    (y.dest (F := F) (α := α))
Tactic: rw [appendFun_comp_id]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: Quot r) (γ := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
      (x.dest (F := F) (α := α)) =
    MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (TypeVec.comp (α := α ::: Cofix F α) (β := α ::: Quot r) (γ := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)))
      (y.dest (F := F) (α := α))
have h₁ : MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α))) =
  MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α)))
Tactic: rw [@comp_map _ _ q _ _ _ (appendFun id (Quot.mk r)),
        @comp_map _ _ q _ _ _ (appendFun id (Quot.mk r))]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (x.dest (F := F) (α := α))) =
    MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α)))
have h₁ : MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α))) =
  MvFunctor.map (F := F) (α := α ::: Quot r) (β := α ::: Quot fun (x y : Cofix F α) ↦ x = y ∨ r x y)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor r (fun (x y : Cofix F α) ↦ x = y ∨ r x y) this))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: Quot r)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) (y.dest (F := F) (α := α)))
Tactic: rw [h _ _ r'xy]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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
⊢ 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) (α := α))
have h₁ : ∀ (h : 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) (α := α))
Tactic: cases r'xy with
    | inl h =>
      rw [h]
    | inr r'xy =>
      have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
      rw [← Quot.factor_mk_eq _ _ this]
      dsimp [r']
      rw [appendFun_comp_id]
      rw [@comp_map _ _ q _ _ _ (appendFun id (Quot.mk r)),
        @comp_map _ _ q _ _ _ (appendFun id (Quot.mk r))]
      rw [h _ _ r'xy]
Cleared hypotheses: r'xy
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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
h₁ :
  ∀ (h : 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) (α := α))
⊢ 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) (α := α))
have h₂ : ∀ (r'xy : 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) (α := α))
Tactic: cases r'xy with
    | inl h =>
      rw [h]
    | inr r'xy =>
      have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
      rw [← Quot.factor_mk_eq _ _ this]
      dsimp [r']
      rw [appendFun_comp_id]
      rw [@comp_map _ _ q _ _ _ (appendFun id (Quot.mk r)),
        @comp_map _ _ q _ _ _ (appendFun id (Quot.mk r))]
      rw [h _ _ r'xy]
Cleared hypotheses: r'xy
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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 → LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
⊢ ∀ (x y : Cofix F α), r x y → x = y
have 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) (α := α))
Tactic: apply Cofix.bisim_rel
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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 → LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
x y : Cofix F α
rxy : 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) (α := α))
have h₁ : ∀ (a : (P F).A) (f₀ f₁ : (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
  (dxeq :
    x.dest (F := F) (α := α) =
      MvQPF.abs (F := F) (α := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) a f₀))
  (dyeq :
    y.dest (F := F) (α := α) =
      MvQPF.abs (F := F) (α := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) a f₁))
  (h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)),
  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: rcases (liftR_iff (fun a b => RelLast α r b) (dest x) (dest y)).mp (h x y rxy)
    with ⟨a, f₀, f₁, dxeq, dyeq, h'⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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 → LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a
dxeq :
  x.dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) a f₀)
dyeq :
  y.dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) a f₁)
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
⊢ 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) (α := α))
have h₁ : Eq (α := F (α ::: Quot r))
  (MvQPF.abs (F := F) (α := α ::: Quot r)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
      (TypeVec.comp (α := (P F).B a) (β := α ::: Cofix F α) (γ := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) f₀)))
  (MvQPF.abs (F := F) (α := α ::: Quot r)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
      (TypeVec.comp (α := (P F).B a) (β := α ::: Cofix F α) (γ := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) f₁)))
Tactic: rw [dxeq, dyeq, ← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
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 → LiftR (F := F) (α := α ::: Cofix F α) (α.RelLast r) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a
dxeq :
  x.dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) a f₀)
dyeq :
  y.dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) a f₁)
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
⊢ Eq (α := F (α ::: Quot r))
    (MvQPF.abs (F := F) (α := α ::: Quot r)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
        (TypeVec.comp (α := (P F).B a) (β := α ::: Cofix F α) (γ := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) f₀)))
    (MvQPF.abs (F := F) (α := α ::: Quot r)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
        (TypeVec.comp (α := (P F).B a) (β := α ::: Cofix F α) (γ := α ::: Quot r)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r)) f₁)))
have h₁ : Eq (α := F (α ::: Quot r))
  (MvQPF.abs (F := F) (α := α ::: Quot r)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
      (TypeVec.comp (α := (P F).B a) (β := α ::: Cofix F α) (γ := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r))
        (splitFun (α := (P F).B a) (α' := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
          (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀)
          (lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₀)))))
  (MvQPF.abs (F := F) (α := α ::: Quot r)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Quot r) a
      (TypeVec.comp (α := (P F).B a) (β := α ::: Cofix F α) (γ := α ::: Quot r)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk r))
        (splitFun (α := (P F).B a) (α' := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a)
          (dropFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁)
          (lastFun (α := (P F).B a) (β := fun (a : Fin2 (n + 1)) ↦ (α ::: Cofix F α) a) f₁)))))
Tactic: rw [← split_dropFun_lastFun f₀, ← split_dropFun_lastFun f₁]