-- Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
theorem Fix.ind_aux (a : q.P.A) (f' : q.P.drop.B a ⟹ α) (f : q.P.last.B a → q.P.W α) :
    Fix.mk (abs ⟨a, q.P.appendContents f' fun x => ⟦f x⟧⟩) = ⟦q.P.wMk a f' f⟧

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr ((P F).wMk a f' f)⟧

Tactic:
apply Quot.sound

Result:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ (wSetoid α) ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩)))
    (wrepr ((P F).wMk a f' f))

Proof state:
case a.h.e_a.e_snd
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ splitFun (TypeVec.id ⊚ f') (fixToW ∘ fun x => ⟦f x⟧) = splitFun (TypeVec.id ⊚ f') (wrepr ∘ f)

Tactic:
rfl

Result:
no goals

Proof state:
case a.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs ⟨a, (TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x => ⟦f x⟧⟩ =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))

Tactic:
conv =>
  rhs
  rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]

Result:
case a.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs ⟨a, (TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x => ⟦f x⟧⟩ =
    abs ⟨a, (TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f⟩

Proof state:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
this : mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr ((P F).wMk a f' f)⟧
⊢ (wSetoid α) (wrepr ((P F).wMk a f' f)) ((P F).wMk a f' f)

Tactic:
apply wrepr_equiv

Result:
no goals

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
this : mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr ((P F).wMk a f' f)⟧
⊢ ⟦wrepr ((P F).wMk a f' f)⟧ = ⟦(P F).wMk a f' f⟧

Tactic:
apply Quot.sound

Result:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
this : mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr ((P F).wMk a f' f)⟧
⊢ (wSetoid α) (wrepr ((P F).wMk a f' f)) ((P F).wMk a f' f)

Proof state:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ (wSetoid α) ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩)))
    (wrepr ((P F).wMk a f' f))

Tactic:
apply wEquiv.abs'

Result:
case a.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs
      ((P F).wDest'
        ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩)))) =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))

Proof state:
case a.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs ⟨a, (TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x => ⟦f x⟧⟩ =
    abs ⟨a, (TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f⟩

Tactic:
congr 2

Result:
case a.h.e_a.e_snd
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ ((TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x => ⟦f x⟧) =
    (TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
this : mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr ((P F).wMk a f' f)⟧
⊢ mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦(P F).wMk a f' f⟧

Tactic:
rw [this]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
this : mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr ((P F).wMk a f' f)⟧
⊢ ⟦wrepr ((P F).wMk a f' f)⟧ = ⟦(P F).wMk a f' f⟧

Proof state:
case a.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs
      ((P F).wDest'
        ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩)))) =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))

Tactic:
rw [MvPFunctor.wDest'_wMk', abs_map, abs_repr, ← abs_map, MvPFunctor.map_eq]

Result:
case a.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs ⟨a, (TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x => ⟦f x⟧⟩ =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))

Proof state:
case a.h.e_a.e_snd
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ ((TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x => ⟦f x⟧) =
    (TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f

Tactic:
rw [MvPFunctor.appendContents, MvPFunctor.appendContents]

Result:
case a.h.e_a.e_snd
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ ((TypeVec.id ::: fixToW) ⊚ splitFun f' fun x => ⟦f x⟧) = (TypeVec.id ::: wrepr) ⊚ splitFun f' f

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦(P F).wMk a f' f⟧

Tactic:
have : Fix.mk (abs ⟨a, q.P.appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr (q.P.wMk a f' f)⟧ := by
  apply Quot.sound; apply wEquiv.abs'
  rw [MvPFunctor.wDest'_wMk', abs_map, abs_repr, ← abs_map, MvPFunctor.map_eq]
  conv =>
    rhs
    rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]
  congr 2; rw [MvPFunctor.appendContents, MvPFunctor.appendContents]
  rw [appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]
  rfl

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
this : mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr ((P F).wMk a f' f)⟧
⊢ mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦(P F).wMk a f' f⟧

Proof state:
case a.h.e_a.e_snd
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ ((TypeVec.id ::: fixToW) ⊚ splitFun f' fun x => ⟦f x⟧) = (TypeVec.id ::: wrepr) ⊚ splitFun f' f

Tactic:
rw [appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]

Result:
case a.h.e_a.e_snd
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ splitFun (TypeVec.id ⊚ f') (fixToW ∘ fun x => ⟦f x⟧) = splitFun (TypeVec.id ⊚ f') (wrepr ∘ f)