-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.abs_repr {α} (x : Cofix F α) : Quot.mk _ (Cofix.repr x) = x

Proof state:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) (repr (Quot.mk Mcongr a✝))))
    (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr a✝))

Tactic:
simp only [Cofix.repr, M.dest_corec, abs_map, MvQPF.abs_repr, Function.comp]

Result:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id ::: M.corec (P F) (MvQPF.repr ∘ dest)) <$$> dest (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
⊢ ∀ (x y : Cofix F α), R x y → LiftR' (α.RelLast' R) x.dest y.dest

Tactic:
rintro x y h

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
x y : Cofix F α
h : R x y
⊢ LiftR' (α.RelLast' R) x.dest y.dest

Proof state:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        (Quot.mk Mcongr ∘
            M.corec (P F)
              (MvQPF.repr ∘ Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) ∘
          Quot.mk Mcongr) <$$>
      MvQPF.abs (M.dest (P F) a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))

Tactic:
apply liftR_map_last

Result:
case mk.hh
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
a✝ : (P F).M α
⊢ ∀ (x : (P F).M α),
    R
      (((Quot.mk Mcongr ∘
            M.corec (P F)
              (MvQPF.repr ∘ Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) ∘
          Quot.mk Mcongr)
        x)
      (Quot.mk Mcongr x)

Proof state:
case mk.hh
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
a✝ x✝ : (P F).M α
⊢ R
    (((Quot.mk Mcongr ∘
          M.corec (P F)
            (MvQPF.repr ∘ Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) ∘
        Quot.mk Mcongr)
      x✝)
    (Quot.mk Mcongr x✝)

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
y : Cofix F α
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) y.repr))
    (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ y)

Tactic:
induction y using Quot.ind

Result:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) (repr (Quot.mk Mcongr a✝))))
    (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr a✝))

Proof state:
case mk.hh
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
a✝ : (P F).M α
⊢ ∀ (x : (P F).M α),
    R
      (((Quot.mk Mcongr ∘
            M.corec (P F)
              (MvQPF.repr ∘ Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) ∘
          Quot.mk Mcongr)
        x)
      (Quot.mk Mcongr x)

Tactic:
intros

Result:
case mk.hh
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
a✝ x✝ : (P F).M α
⊢ R
    (((Quot.mk Mcongr ∘
          M.corec (P F)
            (MvQPF.repr ∘ Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) ∘
        Quot.mk Mcongr)
      x✝)
    (Quot.mk Mcongr x✝)

Proof state:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id ::: M.corec (P F) (MvQPF.repr ∘ dest)) <$$> dest (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))

Tactic:
conv => congr; rfl; rw [Cofix.dest]

Result:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id :::
          M.corec (P F)
            (MvQPF.repr ∘ Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) <$$>
        Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))

Proof state:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id ::: Quot.mk Mcongr) <$$>
      (TypeVec.id :::
          M.corec (P F)
            (MvQPF.repr ∘ Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) <$$>
        Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))

Tactic:
rw [MvFunctor.map_map, MvFunctor.map_map, ← appendFun_comp_id, ← appendFun_comp_id]

Result:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
a✝ : (P F).M α
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        (Quot.mk Mcongr ∘
            M.corec (P F)
              (MvQPF.repr ∘ Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) ∘
          Quot.mk Mcongr) <$$>
      MvQPF.abs (M.dest (P F) a✝))
    ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
⊢ Quot.mk Mcongr x.repr = x

Tactic:
let R := fun x y : Cofix F α => abs (repr y) = x

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
⊢ Quot.mk Mcongr x.repr = x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
y : Cofix F α
⊢ LiftR' (α.RelLast' R) (abs y.repr).dest y.dest

Tactic:
dsimp [Cofix.dest, Cofix.abs]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
y : Cofix F α
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) y.repr))
    (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ y)