awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
x y : (P F).W
a : (P F).A
f f' : (P F).B a → (P F).W
h : ∀ (x : (P F).B a), Wequiv (f x) (f' x)
ih : ∀ (x : (P F).B a), Wequiv (f' x) (f x)
⊢ Wequiv (WType.mk (β := (P F).B) a f') (WType.mk (β := (P F).B) a f)

Tactic:
Wequiv.ind _ _ _ ih

Premises used: QPF.Wequiv.ind
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
x y : (P F).W
a : (P F).A
f f' : (P F).B a → (P F).W
h : ∀ (x : (P F).B a), Wequiv (f x) (f' x)
ih : ∀ (x : (P F).B a), Wequiv (f' x) (f x)
⊢ Wequiv (WType.mk (β := (P F).B) a f') (WType.mk (β := (P F).B) a f)

Tactic:
exact Wequiv.ind _ _ _ ih

Premises used: QPF.Wequiv.ind
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
x y : (P F).W
a : (P F).A
f : (P F).B a → (P F).W
a' : (P F).A
f' : (P F).B a' → (P F).W
h :
  Eq (α := F (P F).W) (QPF.abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))
    (QPF.abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a' f'))
⊢ Wequiv (WType.mk (β := (P F).B) a' f') (WType.mk (β := (P F).B) a f)

Tactic:
Wequiv.abs _ _ _ _ h.symm

Premises used: QPF.Wequiv.abs, Eq.symm
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
x y : (P F).W
a : (P F).A
f : (P F).B a → (P F).W
a' : (P F).A
f' : (P F).B a' → (P F).W
h :
  Eq (α := F (P F).W) (QPF.abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))
    (QPF.abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a' f'))
⊢ Wequiv (WType.mk (β := (P F).B) a' f') (WType.mk (β := (P F).B) a f)

Tactic:
exact Wequiv.abs _ _ _ _ h.symm

Premises used: QPF.Wequiv.abs, Eq.symm
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
x_1 y_1 x y z : (P F).W
h : Wequiv x y
h_1 : Wequiv y z
ih₁ : Wequiv y x
ih₂ : Wequiv z y
⊢ Wequiv z x

Tactic:
QPF.Wequiv.trans _ _ _ ih₂ ih₁

Premises used: QPF.Wequiv.trans
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
x_1 y_1 x y z : (P F).W
h : Wequiv x y
h_1 : Wequiv y z
ih₁ : Wequiv y x
ih₂ : Wequiv z y
⊢ Wequiv z x

Tactic:
exact QPF.Wequiv.trans _ _ _ ih₂ ih₁

Premises used: QPF.Wequiv.trans
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
x y : (P F).W
h : Wequiv x y
ind :
  ∀ (a : (P F).A) (f f' : (P F).B a → (P F).W),
    (∀ (x : (P F).B a), Wequiv (f x) (f' x)) →
      ∀ (ih : ∀ (x : (P F).B a), Wequiv (f' x) (f x)),
        Wequiv (WType.mk (β := (P F).B) a f') (WType.mk (β := (P F).B) a f)
abs :
  ∀ (a : (P F).A) (f : (P F).B a → (P F).W) (a' : (P F).A) (f' : (P F).B a' → (P F).W)
    (h :
      Eq (α := F (P F).W) (QPF.abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))
        (QPF.abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a' f'))),
    Wequiv (WType.mk (β := (P F).B) a' f') (WType.mk (β := (P F).B) a f)
trans : ∀ (x y z : (P F).W), Wequiv x y → Wequiv y z → ∀ (ih₁ : Wequiv y x) (ih₂ : Wequiv z y), Wequiv z x
⊢ Wequiv y x

Tactic:
induction h with
  | ind a f f' _ ih => exact Wequiv.ind _ _ _ ih
  | abs a f a' f' h => exact Wequiv.abs _ _ _ _ h.symm
  | trans x y z _ _ ih₁ ih₂ => exact QPF.Wequiv.trans _ _ _ ih₂ ih₁

Premises used: QPF.Wequiv.trans, QPF.Wequiv.abs, QPF.Wequiv.ind
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
x : (P F).W
mk :
  ∀ (a : (P F).A) (f : (P F).B a → WType (α := (P F).A) (P F).B) (ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)),
    Wequiv (Wrepr (WType.mk (β := (P F).B) a f)) (WType.mk (β := (P F).B) a f)
⊢ Wequiv (Wrepr x) x

Tactic:
induction x with | _ a f ih
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
mk :
  Wequiv (Wrepr (WType.mk (β := (P F).B) a f))
    (PFunctor.W.mk ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f)))
mk₁ :
  Wequiv (PFunctor.W.mk ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f)))
    (WType.mk (β := (P F).B) a f)
mk₂ : (P F).W
⊢ Wequiv (Wrepr (WType.mk (β := (P F).B) a f)) (WType.mk (β := (P F).B) a f)

Tactic:
apply Wequiv.trans

Premises used: QPF.Wequiv.trans
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
mk :
  abs (Wrepr (WType.mk (β := (P F).B) a f)).dest =
    abs (PFunctor.W.mk ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))).dest
⊢ Wequiv (Wrepr (WType.mk (β := (P F).B) a f))
    (PFunctor.W.mk ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f)))

Tactic:
apply Wequiv.abs'

Premises used: QPF.Wequiv.abs'
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ Wrepr (WType.mk (β := (P F).B) a f) =
    PFunctor.W.mk (repr (abs ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))))

Tactic:
have : Wrepr ⟨a, f⟩ = PFunctor.W.mk (repr (abs (q.P.map Wrepr ⟨a, f⟩))) := rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this :
  Wrepr (WType.mk (β := (P F).B) a f) =
    PFunctor.W.mk (repr (abs ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))))
mk :
  abs ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f)) =
    abs (PFunctor.W.mk ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))).dest
⊢ abs (Wrepr (WType.mk (β := (P F).B) a f)).dest =
    abs (PFunctor.W.mk ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))).dest

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

Premises used: PFunctor.W.dest_mk, QPF.abs_repr
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this :
  Wrepr (WType.mk (β := (P F).B) a f) =
    PFunctor.W.mk (repr (abs ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))))
⊢ abs ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f)) =
    abs (PFunctor.W.mk ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))).dest

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
mk : ∀ (x : (P F).B a), Wequiv ((Wrepr ∘ f) x) (f x)
⊢ Wequiv (PFunctor.W.mk ((P F).map Wrepr (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f)))
    (WType.mk (β := (P F).B) a f)

Tactic:
apply Wequiv.ind

Premises used: QPF.Wequiv.ind
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (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:
ih

Premises used: QPF.Wrepr
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (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
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
h :
  ∀ (x : Fix F) (x : (P F).W),
    (recF g ∘ fixToW) (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) x) =
      rec g (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) x)
⊢ Eq (α := Fix F → α) (recF g ∘ fixToW) (rec g)

Tactic:
ext ⟨x⟩
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x_1 : F (Fix F)
x_2 : Fix F
x : (P F).W
h : Wequiv (fixToW (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) x)) x
⊢ (recF g ∘ fixToW) (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) x) =
    rec g (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) x)

Tactic:
apply recF_eq_of_Wequiv

Premises used: QPF.recF_eq_of_Wequiv
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x_1 : F (Fix F)
x_2 : Fix F
x : (P F).W
⊢ Wequiv (Quotient.lift Wrepr ⋯ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) x)) x

Tactic:
apply Wrepr_equiv

Premises used: QPF.Wrepr_equiv
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
⊢ Eq (α := Fix F → α) (recF g ∘ fixToW) (rec g)

Tactic:
have : recF g ∘ fixToW = Fix.rec g := by
    ext ⟨x⟩
    apply recF_eq_of_Wequiv
    rw [fixToW]
    apply Wrepr_equiv
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : Eq (α := Fix F → α) (recF g ∘ fixToW) (rec g)
lhs : rec g (mk x)
| rec g (mk x) = g (rec g <$> x)

Tactic:
lhs
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : Eq (α := Fix F → α) (recF g ∘ fixToW) (rec g)
rw : recF g (PFunctor.W.mk ((P F).map fixToW (repr x)))
| rec g (mk x) = g (rec g <$> x)

Tactic:
lhs
    rw [Fix.rec, Fix.mk]
    dsimp

Premises used: QPF.Fix.mk, QPF.Fix.rec
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : Eq (α := Fix F → α) (recF g ∘ fixToW) (rec g)
rcases :
  ∀ (a : (P F).A) (f : (P F).B a → Fix F) (h : repr x = Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a f),
    recF g (PFunctor.W.mk ((P F).map fixToW (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a f))) =
      g (rec g <$> x)
⊢ recF g (PFunctor.W.mk ((P F).map fixToW (repr x))) = g (rec g <$> x)

Tactic:
rcases h : repr x with ⟨a, f⟩

Premises used: QPF.repr
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : Eq (α := Fix F → α) (recF g ∘ fixToW) (rec g)
a : (P F).A
f : (P F).B a → Fix F
h : repr x = Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a f
rw : recF g (PFunctor.W.mk (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a (fixToW ∘ f))) = g (rec g <$> x)
rw₁ :
  g
      (abs
        ((P F).map (recF g)
          (PFunctor.W.mk (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a (fixToW ∘ f))).dest)) =
    g (rec g <$> x)
rw₂ :
  g
      (abs
        ((P F).map (recF g)
          (PFunctor.W.mk ((P F).map fixToW (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a f))).dest)) =
    g (rec g <$> x)
rw₃ :
  g
      (abs
        ((P F).map (α := (P F).W) (recF g)
          ((P F).map fixToW (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a f)))) =
    g (rec g <$> x)
rw₄ :
  g (abs ((P F).map (α := Fix F) (recF g ∘ fixToW) (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a f))) =
    g (rec g <$> x)
rw₅ :
  g (Functor.map (α := Fix F) (recF g ∘ fixToW) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a f))) =
    g (rec g <$> x)
rw₆ : g ((recF g ∘ fixToW) <$> abs (repr x)) = g (rec g <$> x)
rw₇ : g ((recF g ∘ fixToW) <$> x) = g (rec g <$> x)
rw₈ rw₉ : g (rec g <$> x) = g (rec g <$> x)
⊢ recF g (PFunctor.W.mk ((P F).map fixToW (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a f))) =
    g (rec g <$> x)

Tactic:
rw [PFunctor.map_eq, recF_eq, ← PFunctor.map_eq, PFunctor.W.dest_mk, PFunctor.map_map, abs_map,
    ← h, abs_repr, this]

Premises used: PFunctor.W.dest_mk, QPF.abs_repr, PFunctor.map_map, QPF.abs_map, QPF.recF_eq, PFunctor.map_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
a₁ :
  (Wsetoid : (P F).W → (P F).W → Prop)
    (PFunctor.W.mk
      ((P F).map fixToW
        (repr (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)))))
    (Wrepr (WType.mk (β := (P F).B) a f))
⊢ mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)) =
    ⟦Wrepr (WType.mk (β := (P F).B) a f)⟧

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
a₁ :
  abs
      (PFunctor.W.dest
        (PFunctor.W.mk
          ((P F).map fixToW
            (repr (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)))))) =
    abs (Wrepr (WType.mk (β := (P F).B) a f)).dest
⊢ (Wsetoid : (P F).W → (P F).W → Prop)
    (PFunctor.W.mk
      ((P F).map fixToW
        (repr (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)))))
    (Wrepr (WType.mk (β := (P F).B) a f))

Tactic:
apply Wequiv.abs'

Premises used: QPF.Wequiv.abs'
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
a₁ :
  abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a (fixToW ∘ fun (x : (P F).B a) ↦ ⟦f x⟧)) =
    abs (Wrepr (WType.mk (β := (P F).B) a f)).dest
⊢ abs
      (PFunctor.W.dest
        (PFunctor.W.mk
          ((P F).map fixToW
            (repr (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)))))) =
    abs (Wrepr (WType.mk (β := (P F).B) a f)).dest

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

Premises used: PFunctor.W.dest_mk, QPF.abs_repr, QPF.abs_map, PFunctor.map_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
a₁ :
  Eq (α := F (P F).W)
    (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a (fixToW ∘ fun (x : (P F).B a) ↦ ⟦f x⟧)))
    (abs ((P F).map (recF (PFunctor.W.mk ∘ repr)) (PFunctor.W.dest (WType.mk (β := (P F).B) a f))))
⊢ abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a (fixToW ∘ fun (x : (P F).B a) ↦ ⟦f x⟧)) =
    abs (Wrepr (WType.mk (β := (P F).B) a f)).dest

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

Premises used: PFunctor.W.dest_mk, QPF.abs_repr, QPF.Wrepr, Function.comp, QPF.recF_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ Eq (α := F (P F).W)
    (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a (fixToW ∘ fun (x : (P F).B a) ↦ ⟦f x⟧)))
    (abs ((P F).map (recF (PFunctor.W.mk ∘ repr)) (PFunctor.W.dest (WType.mk (β := (P F).B) a f))))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)) =
    ⟦Wrepr (WType.mk (β := (P F).B) 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
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
this :
  mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)) =
    ⟦Wrepr (WType.mk (β := (P F).B) a f)⟧
rw : Eq (α := Fix F) ⟦Wrepr (WType.mk (β := (P F).B) a f)⟧ ⟦WType.mk (β := (P F).B) a f⟧
⊢ mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)) =
    ⟦WType.mk (β := (P F).B) a f⟧

Tactic:
rw [this]
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
this :
  mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)) =
    ⟦Wrepr (WType.mk (β := (P F).B) a f)⟧
a₁ : (Wsetoid : (P F).W → (P F).W → Prop) (Wrepr (WType.mk (β := (P F).B) a f)) (WType.mk (β := (P F).B) a f)
⊢ Eq (α := Fix F) ⟦Wrepr (WType.mk (β := (P F).B) a f)⟧ ⟦WType.mk (β := (P F).B) a f⟧

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
this :
  mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)) =
    ⟦Wrepr (WType.mk (β := (P F).B) a f)⟧
⊢ (Wsetoid : (P F).W → (P F).W → Prop) (Wrepr (WType.mk (β := (P F).B) a f)) (WType.mk (β := (P F).B) a f)

Tactic:
apply Wrepr_equiv

Premises used: QPF.Wrepr_equiv
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (Fix.mk x) = g₂ (Fix.mk x)
x_1 : Fix F
x : (P F).W
mk :
  ∀ (a : (P F).A) (f : (P F).B a → WType (α := (P F).A) (P F).B)
    (ih :
      ∀ (a : (P F).B a),
        g₁ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a)) =
          g₂ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))),
    g₁ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (WType.mk (β := (P F).B) a f)) =
      g₂ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (WType.mk (β := (P F).B) a f))
⊢ g₁ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) x) = g₂ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) x)

Tactic:
induction x with | _ a f ih
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (Fix.mk x) = g₂ (Fix.mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih :
  ∀ (a : (P F).B a),
    g₁ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a)) = g₂ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
mk : g₁ ⟦WType.mk (β := (P F).B) a f⟧ = g₂ ⟦WType.mk (β := (P F).B) a f⟧
⊢ g₁ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (WType.mk (β := (P F).B) a f)) =
    g₂ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (WType.mk (β := (P F).B) a f))

Tactic:
change g₁ ⟦⟨a, f⟩⟧ = g₂ ⟦⟨a, f⟩⟧

Premises used: Quotient.mk, WType.mk
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (Fix.mk x) = g₂ (Fix.mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih :
  ∀ (a : (P F).B a),
    g₁ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a)) = g₂ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
mk :
  g₁ (Fix.mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧))) =
    g₂ (Fix.mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)))
⊢ g₁ ⟦WType.mk (β := (P F).B) a f⟧ = g₂ ⟦WType.mk (β := (P F).B) a f⟧

Tactic:
rw [← Fix.ind_aux a f]

Premises used: QPF.Fix.ind_aux
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (Fix.mk x) = g₂ (Fix.mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih :
  ∀ (a : (P F).B a),
    g₁ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a)) = g₂ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
mk :
  g₁ <$> abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧) =
    g₂ <$> abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)
⊢ g₁ (Fix.mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧))) =
    g₂ (Fix.mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)))

Tactic:
apply h
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (Fix.mk x) = g₂ (Fix.mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih :
  ∀ (a : (P F).B a),
    g₁ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a)) = g₂ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
mk :
  Eq (α := F α) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → α) a (g₁ ∘ fun (x : (P F).B a) ↦ ⟦f x⟧)))
    (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → α) a (g₂ ∘ fun (x : (P F).B a) ↦ ⟦f x⟧)))
⊢ g₁ <$> abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧) =
    g₂ <$> abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)

Tactic:
rw [← abs_map, ← abs_map, PFunctor.map_eq, PFunctor.map_eq]

Premises used: QPF.abs_map, PFunctor.map_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (Fix.mk x) = g₂ (Fix.mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih :
  ∀ (a : (P F).B a),
    g₁ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a)) = g₂ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
mk : ∀ (x : (P F).B a), (g₁ ∘ fun (x : (P F).B a) ↦ ⟦f x⟧) x = (g₂ ∘ fun (x : (P F).B a) ↦ ⟦f x⟧) x
⊢ Eq (α := F α) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → α) a (g₁ ∘ fun (x : (P F).B a) ↦ ⟦f x⟧)))
    (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → α) a (g₂ ∘ fun (x : (P F).B a) ↦ ⟦f x⟧)))

Tactic:
congr 2 with x
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x_1 : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih :
  ∀ (a : (P F).B a),
    g₁ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a)) = g₂ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
x : (P F).B a
⊢ (g₁ ∘ fun (x : (P F).B a) ↦ ⟦f x⟧) x = (g₂ ∘ fun (x : (P F).B a) ↦ ⟦f x⟧) x

Tactic:
apply ih
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
h₁ : ∀ (x : Fix F), rec g x = h x
⊢ rec g = h

Tactic:
ext x
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
h₁ : ∀ (x : F (Fix F)), rec g <$> x = h <$> x → rec g (mk x) = h (mk x)
⊢ rec g x = h x

Tactic:
apply Fix.ind_rec

Premises used: QPF.Fix.ind_rec
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x_1 : Fix F
x : F (Fix F)
hyp' : rec g <$> x = h <$> x
h₁ : rec g (mk x) = g (h <$> x)
h₂ : rec g (mk x) = g (rec g <$> x)
h₃ h₄ : g (rec g <$> x) = g (rec g <$> x)
⊢ rec g (mk x) = h (mk x)

Tactic:
rw [hyp, ← hyp', Fix.rec_eq]

Premises used: QPF.Fix.rec_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x : Fix F
change : (mk ∘ dest) x = id x
⊢ mk x.dest = x

Tactic:
change (Fix.mk ∘ Fix.dest) x = id x

Premises used: Function.comp, id, QPF.Fix.dest, QPF.Fix.mk
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x : Fix F
h : ∀ (x : F (Fix F)), (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)
⊢ (mk ∘ dest) x = id x

Tactic:
apply Fix.ind_rec (mk ∘ dest) id

Premises used: Function.comp, QPF.Fix.ind_rec, id, QPF.Fix.dest, QPF.Fix.mk
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x_1 : Fix F
x : F (Fix F)
h : mk <$> rec (Functor.map mk) <$> x = x → mk (mk <$> rec (Functor.map mk) <$> x) = mk x
⊢ (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)

Tactic:
rw [Function.comp_apply, id_eq, Fix.dest, Fix.rec_eq, id_map, comp_map]

Premises used: QPF.Fix.rec_eq, QPF.Fix.dest, QPF.comp_map, QPF.id_map, Function.comp_apply, id_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x_1 : Fix F
x : F (Fix F)
h : mk <$> rec (Functor.map mk) <$> x = x
h₁ h₂ : mk x = mk x
⊢ mk (mk <$> rec (Functor.map mk) <$> x) = mk x

Tactic:
rw [h]