awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
u : F { p : α × α // r p.1 p.2 }
xeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$> u = x
yeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$> u = y
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → { p : α × α // r p.1 p.2 }
h : repr u = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f
⊢ y =
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α × α).2)
have h₁ : Eq (α := F α)
  (abs
    ((P F).map (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2)
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f)))
  (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α × α).2))
Tactic: rw [← yeq, ← abs_repr u, h, ← abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
a : PFunctor.A.{u, u_1} (P F)
f₀ f₁ : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀)
yeq : y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁)
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ Liftr r x y
have h₁ : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) sorry) =
    x ∧
  (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) sorry) =
    y
Tactic: use abs ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
a : PFunctor.A.{u, u_1} (P F)
f₀ f₁ : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀)
yeq : y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁)
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
        abs
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
            fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
      x ∧
    (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
        abs
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
            fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
      y
have h₁ : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
    abs
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
        fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) sorry) =
  x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
a : PFunctor.A.{u, u_1} (P F)
f₀ f₁ : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀)
yeq : y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁)
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
h₁ :
  (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
    x
⊢ (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
        abs
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
            fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
      x ∧
    (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
        abs
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
            fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
      y
have h₂ : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
    abs
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
        fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) sorry) =
  y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
a : PFunctor.A.{u, u_1} (P F)
f₀ f₁ : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀)
yeq : y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁)
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
    x
have h₁ : Eq (α := F α)
  (abs
    ((P F).map (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1)
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
        fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) sorry)))
  (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀))
Tactic: rw [xeq, ← abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
a : PFunctor.A.{u, u_1} (P F)
f₀ f₁ : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀)
yeq : y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁)
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
    y
have h₁ : Eq (α := F α)
  (abs
    ((P F).map (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2)
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
        fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) sorry)))
  (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁))
Tactic: rw [yeq, ← abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
g : F α → α
x : PFunctor.W.{u, u_1} (P F)
⊢ recF g x = g (abs ((P F).map (recF g) x.dest))
have mk : ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → WType.{u, u_1} (α := PFunctor.A.{u, u_1} (P F)) (P F).B),
  recF g (WType.mk (β := (P F).B) a f) = g (abs ((P F).map (recF g) (PFunctor.W.dest (WType.mk (β := (P F).B) a f))))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
h : Wequiv x y
⊢ recF u x = recF u y
have 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), recF u (f x) = recF u (f' x)),
      recF u (WType.mk (β := (P F).B) a f) = recF u (WType.mk (β := (P F).B) a f')
Tactic: induction h with
  | ind a f f' _ ih => simp only [recF_eq', PFunctor.map_eq, Function.comp_def, ih]
  | abs a f a' f' h => simp only [recF_eq', abs_map, h]
  | trans x y z _ _ ih₁ ih₂ => exact Eq.trans ih₁ ih₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF F
α : Type u
u : 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), recF u (f x) = recF u (f' x)),
        recF u (WType.mk (β := (P F).B) a f) = recF u (WType.mk (β := (P F).B) a f')
⊢ recF u x = recF u y
have 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) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))
      (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a' f'))),
  recF u (WType.mk (β := (P F).B) a f) = recF u (WType.mk (β := (P F).B) a' f')
Tactic: induction h with
  | ind a f f' _ ih => simp only [recF_eq', PFunctor.map_eq, Function.comp_def, ih]
  | abs a f a' f' h => simp only [recF_eq', abs_map, h]
  | trans x y z _ _ ih₁ ih₂ => exact Eq.trans ih₁ ih₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF F
α : Type u
u : 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), recF u (f x) = recF u (f' x)),
        recF u (WType.mk (β := (P F).B) a f) = recF u (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'))),
    recF u (WType.mk (β := (P F).B) a f) = recF u (WType.mk (β := (P F).B) a' f')
⊢ recF u x = recF u y
have trans : ∀ (x y z : (P F).W),
  Wequiv x y → Wequiv y z → ∀ (ih₁ : recF u x = recF u y) (ih₂ : recF u y = recF u z), recF u x = recF u z
Tactic: induction h with
  | ind a f f' _ ih => simp only [recF_eq', PFunctor.map_eq, Function.comp_def, ih]
  | abs a f a' f' h => simp only [recF_eq', abs_map, h]
  | trans x y z _ _ ih₁ ih₂ => exact Eq.trans ih₁ ih₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF F
x y : (P F).W
h : QPF.abs x.dest = QPF.abs y.dest
⊢ Wequiv x y
have mk : ∀ (a : (P F).A) (f : (P F).B a → WType (α := (P F).A) (P F).B)
  (h : QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a f)) = QPF.abs y.dest), Wequiv (WType.mk (β := (P F).B) a f) y
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF F
y : (P F).W
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
h : QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a f)) = QPF.abs y.dest
⊢ Wequiv (WType.mk (β := (P F).B) a f) y
have mk : ∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → WType (α := (P F).A) (P F).B)
  (h :
    QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a f)) =
      QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a_1 f_1))),
  Wequiv (WType.mk (β := (P F).B) a f) (WType.mk (β := (P F).B) a_1 f_1)
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
a_1 : (P F).A
f_1 : (P F).B a_1 → WType (α := (P F).A) (P F).B
h :
  QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a f)) = QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a_1 f_1))
⊢ Wequiv (WType.mk (β := (P F).B) a f) (WType.mk (β := (P F).B) a_1 f_1)
have mk : 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_1 f_1))
Tactic: apply Wequiv.abs
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF F
x : (P F).W
⊢ Wequiv x x
have obtain : ∀ (a : (P F).A) (f : (P F).B a → WType (α := (P F).A) (P F).B),
  Wequiv (WType.mk (β := (P F).B) a f) (WType.mk (β := (P F).B) a f)
Tactic: obtain ⟨a, f⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF F
x y : (P F).W
h : Wequiv x y
⊢ Wequiv y x
have 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)
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₁
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ Wequiv y x
have 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)
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₁
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ Wequiv y x
have trans : ∀ (x y z : (P F).W), Wequiv x y → Wequiv y z → ∀ (ih₁ : Wequiv y x) (ih₂ : Wequiv z y), Wequiv z 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₁
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF F
x : (P F).W
⊢ Wequiv (Wrepr x) x
have 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)
Tactic: induction x with | _ a f ih
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ Wequiv (Wrepr (WType.mk (β := (P F).B) a f)) (WType.mk (β := (P F).B) a f)
have 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)))
Tactic: apply Wequiv.trans
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)))
⊢ Wequiv (Wrepr (WType.mk (β := (P F).B) a f)) (WType.mk (β := (P F).B) a f)
have 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)
Tactic: apply Wequiv.trans
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ Wequiv (Wrepr (WType.mk (β := (P F).B) a f)) (WType.mk (β := (P F).B) a f)
have mk₂ : (P F).W
Tactic: apply Wequiv.trans
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ 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)))
have 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
Tactic: apply Wequiv.abs'
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (hypothesis)
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)
⊢ 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
have 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))))
Tactic: have : Wrepr ⟨a, f⟩ = PFunctor.W.mk (repr (abs (q.P.map Wrepr ⟨a, f⟩))) := rfl
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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 (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
have 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
Tactic: rw [this, PFunctor.W.dest_mk, abs_repr]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ 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)
have mk : ∀ (x : (P F).B a), Wequiv ((Wrepr ∘ f) x) (f x)
Tactic: apply Wequiv.ind
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
have 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)
Tactic: ext ⟨x⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ (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)
have h : Wequiv (fixToW (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) x)) x
Tactic: apply recF_eq_of_Wequiv
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (hypothesis)
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
⊢ rec g (mk x) = g (rec g <$> x)
have this : 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
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
| rec g (mk x) = g (rec g <$> x)
have lhs : rec g (mk x)
Tactic: lhs
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
| rec g (mk x) = g (rec g <$> x)
have rw : recF g (PFunctor.W.mk ((P F).map fixToW (repr x)))
Tactic: lhs
    rw [Fix.rec, Fix.mk]
    dsimp
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ recF g (PFunctor.W.mk ((P F).map fixToW (repr x))) = g (rec g <$> x)
have 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)
Tactic: rcases h : repr x with ⟨a, f⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [PFunctor.map_eq, recF_eq, ← PFunctor.map_eq, PFunctor.W.dest_mk, PFunctor.map_map, abs_map,
    ← h, abs_repr, this]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [PFunctor.map_eq, recF_eq, ← PFunctor.map_eq, PFunctor.W.dest_mk, PFunctor.map_map, abs_map,
    ← h, abs_repr, this]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [PFunctor.map_eq, recF_eq, ← PFunctor.map_eq, PFunctor.W.dest_mk, PFunctor.map_map, abs_map,
    ← h, abs_repr, this]