-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem Wrepr_equiv (x : q.P.W) : Wequiv (Wrepr x) x

Proof state:
case mk.a.a
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ ∀ (x : (P F).B a), Wequiv ((Wrepr ∘ f) x) (f x)

Tactic:
exact ih

Result:
no goals

Proof state:
case mk.a.h
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ abs (Wrepr (WType.mk a f)).dest = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest

Tactic:
have : Wrepr ⟨a, f⟩ = PFunctor.W.mk (repr (abs (q.P.map Wrepr ⟨a, f⟩))) := rfl

Result:
case mk.a.h
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))
⊢ abs (Wrepr (WType.mk a f)).dest = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest

Proof state:
case mk.a.h
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))
⊢ abs ((P F).map Wrepr ⟨a, f⟩) = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest

Tactic:
rfl

Result:
no goals

Proof state:
F : Type u → Type u
q : QPF F
x : (P F).W
⊢ Wequiv (Wrepr x) x

Tactic:
induction' x with a f ih

Result:
case mk
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) (WType.mk a f)

Proof state:
case mk.a
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩))

Tactic:
apply Wequiv.abs'

Result:
case mk.a.h
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ abs (Wrepr (WType.mk a f)).dest = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest

Proof state:
case mk.a
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) ?mk.v

Tactic:
change Wequiv (Wrepr ⟨a, f⟩) (PFunctor.W.mk (q.P.map Wrepr ⟨a, f⟩))

Result:
case mk.a
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩))

Proof state:
case mk.a
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)) (WType.mk a f)

Tactic:
apply Wequiv.ind

Result:
case mk.a.a
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ ∀ (x : (P F).B a), Wequiv ((Wrepr ∘ f) x) (f x)

Proof state:
case mk.a.h
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))
⊢ abs (Wrepr (WType.mk a f)).dest = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest

Tactic:
rw [this, PFunctor.W.dest_mk, abs_repr]

Result:
case mk.a.h
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))
⊢ abs ((P F).map Wrepr ⟨a, f⟩) = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest

Proof state:
case mk
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) (WType.mk a f)

Tactic:
apply Wequiv.trans

Result:
case mk.a
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) ?mk.v

case mk.a
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv ?mk.v (WType.mk a f)

case mk.v
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ (P F).W