awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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 (α := (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)
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)
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)
⊢ 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 (α := Fix F) (recF g ∘ 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]
-- 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)
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)
⊢ 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 (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)
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)
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)
⊢ 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 ((recF g ∘ fixToW) <$> abs (repr x)) = 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)
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)
⊢ 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 ((recF g ∘ fixToW) <$> x) = 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)
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)
⊢ 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 (rec g <$> x) = 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
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)⟧
have 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))
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ (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))
have 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
Tactic: apply Wequiv.abs'
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ 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
have 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
Tactic: rw [PFunctor.W.dest_mk, abs_map, abs_repr, ← abs_map, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (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 (Wrepr (WType.mk (β := (P F).B) a f)).dest
have 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))))
Tactic: simp only [Wrepr, recF_eq, PFunctor.W.dest_mk, abs_repr, Function.comp]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (hypothesis)
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⟧)) =
    ⟦WType.mk (β := (P F).B) a f⟧
have 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)⟧
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
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)⟧
⊢ 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⟧
have rw : Eq (α := Fix F) ⟦Wrepr (WType.mk (β := (P F).B) a f)⟧ ⟦WType.mk (β := (P F).B) a f⟧
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)⟧
⊢ Eq (α := Fix F) ⟦Wrepr (WType.mk (β := (P F).B) a f)⟧ ⟦WType.mk (β := (P F).B) a f⟧
have a₁ : (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 Quot.sound
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
x : (P F).W
⊢ g₁ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) x) = g₂ (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) 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),
      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))
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 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 : 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))
⊢ 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))
have mk : g₁ ⟦WType.mk (β := (P F).B) a f⟧ = g₂ ⟦WType.mk (β := (P F).B) a f⟧
Tactic: change g₁ ⟦⟨a, f⟩⟧ = g₂ ⟦⟨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₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (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))
⊢ g₁ ⟦WType.mk (β := (P F).B) a f⟧ = g₂ ⟦WType.mk (β := (P F).B) a f⟧
have mk : g₁ (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₂ (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: rw [← Fix.ind_aux 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₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (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))
⊢ g₁ (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₂ (mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)))
have 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⟧)
Tactic: apply h
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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 : 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))
⊢ 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⟧)
have 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⟧)))
Tactic: rw [← abs_map, ← abs_map, PFunctor.map_eq, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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 : 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))
⊢ 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⟧)))
have 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
Tactic: congr 2 with 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 α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
⊢ rec g = h
have h₁ : ∀ (x : Fix F), rec g x = h 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 α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ rec g x = h x
have h₁ : ∀ (x : F (Fix F)), rec g <$> x = h <$> x → rec g (mk x) = h (mk x)
Tactic: apply Fix.ind_rec
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ rec g (mk x) = h (mk x)
have h₁ : rec g (mk x) = g (h <$> x)
Tactic: rw [hyp, ← hyp', Fix.rec_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ rec g (mk x) = h (mk x)
have h₂ : rec g (mk x) = g (rec g <$> x)
Tactic: rw [hyp, ← hyp', Fix.rec_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ rec g (mk x) = h (mk x)
have h₃ : g (rec g <$> x) = g (rec g <$> x)
Tactic: rw [hyp, ← hyp', Fix.rec_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x : Fix F
⊢ mk x.dest = x
have change : (mk ∘ dest) x = id x
Tactic: change (Fix.mk ∘ Fix.dest) x = id x
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x : Fix F
⊢ (mk ∘ dest) x = id x
have h : ∀ (x : F (Fix F)), (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)
Tactic: apply Fix.ind_rec (mk ∘ dest) id
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x_1 : Fix F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)
have h : mk <$> rec (Functor.map mk) <$> x = x → mk (mk <$> rec (Functor.map mk) <$> x) = mk x
Tactic: rw [Function.comp_apply, id_eq, Fix.dest, Fix.rec_eq, id_map, comp_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
have h₁ : mk x = mk x
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ rec (Functor.map mk) (mk x) = x
have rw : (mk ∘ dest) <$> x = x
Tactic: rw [Fix.rec_eq, ← Fix.dest, ← comp_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x : F (Fix F)
| (mk ∘ dest) <$> x = x
have rhs : x
Tactic: rhs
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x : F (Fix F)
| x
have rw : id <$> x
Tactic: rw [← id_map x]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x : F (Fix F)
| (mk ∘ dest) <$> x = x
have rw : id <$> x
Tactic: rhs
    rw [← id_map x]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = x
have conv : (mk ∘ dest) <$> x = id <$> x
Tactic: conv =>
    rhs
    rw [← id_map x]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x
have e_a : ∀ (x : Fix F), (mk ∘ dest) x = id x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x_1 : Fix F
x : (P F).W
⊢ p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) 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), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))),
  p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (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 u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (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), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
⊢ p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (WType.mk (β := (P F).B) a f))
have mk : p ⟦WType.mk (β := (P F).B) a f⟧
Tactic: change p ⟦⟨a, f⟩⟧
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (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), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
⊢ p ⟦WType.mk (β := (P F).B) a f⟧
have mk : p (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: rw [← Fix.ind_aux a f]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (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), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
⊢ p (mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)))
have mk : Liftp p (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