-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem Fix.ind_aux (a : q.P.A) (f : q.P.B a → q.P.W) :
    Fix.mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦⟨a, f⟩⟧

Proof state:
case a
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
this : mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr (WType.mk a f)⟧
⊢ Wsetoid (Wrepr (WType.mk a f)) (WType.mk a f)

Tactic:
apply Wrepr_equiv

Result:
no goals

Proof state:
case a.h
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs (PFunctor.W.mk ((P F).map fixToW (repr (abs ⟨a, fun x => ⟦f x⟧⟩)))).dest = abs (Wrepr (WType.mk a f)).dest

Tactic:
rw [PFunctor.W.dest_mk, abs_map, abs_repr, ← abs_map, PFunctor.map_eq]

Result:
case a.h
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs ⟨a, fixToW ∘ fun x => ⟦f x⟧⟩ = abs (Wrepr (WType.mk a f)).dest

Proof state:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr (WType.mk a f)⟧

Tactic:
apply Quot.sound

Result:
case a
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ Wsetoid (PFunctor.W.mk ((P F).map fixToW (repr (abs ⟨a, fun x => ⟦f x⟧⟩)))) (Wrepr (WType.mk a f))

Proof state:
case a.h
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs ⟨a, fixToW ∘ fun x => ⟦f x⟧⟩ = abs ((P F).map (recF (PFunctor.W.mk ∘ repr)) (PFunctor.W.dest (WType.mk a f)))

Tactic:
rfl

Result:
no goals

Proof state:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦WType.mk a f⟧

Tactic:
have : Fix.mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr ⟨a, f⟩⟧ := by
  apply Quot.sound; apply Wequiv.abs'
  rw [PFunctor.W.dest_mk, abs_map, abs_repr, ← abs_map, PFunctor.map_eq]
  simp only [Wrepr, recF_eq, PFunctor.W.dest_mk, abs_repr, Function.comp]
  rfl

Result:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
this : mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr (WType.mk a f)⟧
⊢ mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦WType.mk a f⟧

Proof state:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
this : mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr (WType.mk a f)⟧
⊢ mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦WType.mk a f⟧

Tactic:
rw [this]

Result:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
this : mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr (WType.mk a f)⟧
⊢ ⟦Wrepr (WType.mk a f)⟧ = ⟦WType.mk a f⟧

Proof state:
case a
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ Wsetoid (PFunctor.W.mk ((P F).map fixToW (repr (abs ⟨a, fun x => ⟦f x⟧⟩)))) (Wrepr (WType.mk a f))

Tactic:
apply Wequiv.abs'

Result:
case a.h
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs (PFunctor.W.mk ((P F).map fixToW (repr (abs ⟨a, fun x => ⟦f x⟧⟩)))).dest = abs (Wrepr (WType.mk a f)).dest

Proof state:
case a.h
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs ⟨a, fixToW ∘ fun x => ⟦f x⟧⟩ = abs (Wrepr (WType.mk a f)).dest

Tactic:
simp only [Wrepr, recF_eq, PFunctor.W.dest_mk, abs_repr, Function.comp]

Result:
case a.h
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs ⟨a, fixToW ∘ fun x => ⟦f x⟧⟩ = abs ((P F).map (recF (PFunctor.W.mk ∘ repr)) (PFunctor.W.dest (WType.mk a f)))

Proof state:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
this : mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr (WType.mk a f)⟧
⊢ ⟦Wrepr (WType.mk a f)⟧ = ⟦WType.mk a f⟧

Tactic:
apply Quot.sound

Result:
case a
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
this : mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr (WType.mk a f)⟧
⊢ Wsetoid (Wrepr (WType.mk a f)) (WType.mk a f)