awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
id_bitraverse :
  ∀ {α β : Type u} (x : bicompr F t α β),
    Eq (α := Id (bicompr F t α β)) (bitraverse (t := bicompr F t) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F_1 G : Type u → Type u} [inst_4 : Applicative F_1] [inst_5 : Applicative G] [LawfulApplicative F_1]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F_1 γ) (f' : β' → F_1 γ') (g : α → G β) (g' : α' → G β')
    (x : bicompr F t α α'),
    bitraverse (t := bicompr F t) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
      Functor.Comp.mk (bitraverse (t := bicompr F t) f f' <$> bitraverse (t := bicompr F t) g g' x)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : bicompr F t α α'),
    Eq (α := Id (bicompr F t β β')) (bitraverse (t := bicompr F t) (pure ∘ f) (pure ∘ f') x)
      (pure (bimap (F := bicompr F t) f f' x))
⊢ LawfulBitraversable.{u} (bicompr F t)
have binaturality : ∀ {F_1 G : Type u → Type u} [inst_4 : Applicative F_1] [inst_5 : Applicative G] [LawfulApplicative F_1]
  [LawfulApplicative G] (η : ApplicativeTransformation F_1 G) {α α' β β' : Type u} (f : α → F_1 β) (f' : α' → F_1 β')
  (x : bicompr F t α α'),
  Eq (α := G (bicompr F t β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := bicompr F t) f f' x))
    (bitraverse (t := bicompr F t) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
α α' β β' : Type u
f : α → β
f' : α' → β'
x : bicompr F t α α'
⊢ Eq (α := Id (bicompr F t β β')) (bitraverse (t := bicompr F t) (pure ∘ f) (pure ∘ f') x)
    (pure (bimap (F := bicompr F t) f f' x))
have bitraverse_eq_bimap_id : Eq (α := Id (bicompr F t β β')) (traverse (bitraverse (t := t) (pure ∘ f) (pure ∘ f')) x)
  (pure (bimap (F := bicompr F t) f f' x))
Tactic: simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
F_1 G : Type u → Type u
inst_4 : Applicative F_1
inst_5 : Applicative G
inst_6 : LawfulApplicative F_1
inst_7 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : bicompr F t α α'
⊢ Eq (α := G (bicompr F t β β')) ((fun {α : Type u} ↦ η.app α) (bitraverse (t := bicompr F t) f f' x))
    (bitraverse (t := bicompr F t) ((fun {α : Type u} ↦ η.app α) ∘ f) ((fun {α : Type u} ↦ η.app α) ∘ f') x)
have binaturality : η.app (bicompr F t β β') (traverse (bitraverse (t := t) f f') x) =
  traverse (bitraverse (t := t) (η.app β ∘ f) (η.app β' ∘ f')) x
Tactic: simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
α α' β β' : Type u
f : α → β
f' : α' → β'
x : bicompr F t α α'
⊢ Eq (α := Id (bicompr F t β β')) (traverse (bitraverse (t := t) (pure ∘ f) (pure ∘ f')) x)
    (pure (bimap (F := bicompr F t) f f' x))
have bitraverse_eq_bimap_id : Eq (α := Id (bicompr F t β β')) (pure (bimap (F := t) f f' <$> x)) (pure (bimap (F := bicompr F t) f f' x))
Tactic: simp only [bitraverse_eq_bimap_id', traverse_eq_map_id', Function.comp_apply]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Traversable F
inst_2 : LawfulTraversable F
inst_3 : LawfulBitraversable t
F_1 G : Type u → Type u
inst_4 : Applicative F_1
inst_5 : Applicative G
inst_6 : LawfulApplicative F_1
inst_7 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u
f : α → F_1 β
f' : α' → F_1 β'
x : bicompr F t α α'
⊢ η.app (bicompr F t β β') (traverse (bitraverse (t := t) f f') x) =
    traverse (bitraverse (t := t) (η.app β ∘ f) (η.app β' ∘ f')) x
have binaturality : η.app (F (t β β')) (traverse (bitraverse (t := t) f f') x) =
  traverse (bitraverse (t := t) (η.app β ∘ f) (η.app β' ∘ f')) x
Tactic: dsimp only [bicompr]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Lemmas (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α₀ α₁ α₂ β : Type u
f : α₀ → F α₁
f' : α₁ → G α₂
x : t α₀ β
⊢ Comp.mk (tfst (t := t) f' <$> tfst (t := t) f x) = tfst (t := t) (Comp.mk ∘ map f' ∘ f) x
have rw : bitraverse (t := t) (Comp.mk ∘ map f' ∘ f) (Comp.mk ∘ map pure ∘ pure) x = tfst (t := t) (Comp.mk ∘ map f' ∘ f) x
Tactic: rw [← comp_bitraverse]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Lemmas (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ Comp.mk (tfst (t := t) f <$> tsnd (t := t) f' x) =
    bitraverse (t := t) (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x
have rw : bitraverse (t := t) (Comp.mk ∘ map f ∘ pure) (Comp.mk ∘ map pure ∘ f') x =
  bitraverse (t := t) (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x
Tactic: rw [← comp_bitraverse]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Lemmas (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ Comp.mk (tsnd (t := t) f' <$> tfst (t := t) f x) =
    bitraverse (t := t) (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x
have rw : bitraverse (t := t) (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ map f' ∘ pure) x =
  bitraverse (t := t) (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x
Tactic: rw [← comp_bitraverse]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Lemmas (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ Comp.mk (tsnd (t := t) g' <$> tsnd (t := t) g x) = tsnd (t := t) (Comp.mk ∘ map g' ∘ g) x
have rw : bitraverse (t := t) (Comp.mk ∘ map pure ∘ pure) (Comp.mk ∘ map g' ∘ g) x = tsnd (t := t) (Comp.mk ∘ map g' ∘ g) x
Tactic: rw [← comp_bitraverse]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Lemmas (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F G : Type u → Type u
inst_1 : Applicative F
inst_2 : Applicative G
inst_3 : LawfulBitraversable t
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α β₀ β₁ β₂ : Type u
g : β₀ → F β₁
g' : β₁ → G β₂
x : t α β₀
⊢ bitraverse (t := t) (Comp.mk ∘ map pure ∘ pure) (Comp.mk ∘ map g' ∘ g) x = tsnd (t := t) (Comp.mk ∘ map g' ∘ g) x
have simp : Eq (α := Comp F G (t α β₂))
  (bitraverse (t := t) (fun (x : α) ↦ Comp.mk (pure (pure x))) (fun (x : β₀) ↦ Comp.mk (g' <$> g x)) x)
  (tsnd (t := t) (fun (x : β₀) ↦ Comp.mk (g' <$> g x)) x)
Tactic: simp only [Function.comp_def, map_pure]
-- Lean 4 proof step from Mathlib.Control.EquivFunctor.Instances (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Perm α → Perm α) (fun (p : Perm α) ↦ ((Equiv.refl α).symm.trans p).trans (Equiv.refl α)) id
have h : ∀ (x : Perm α) (x_1 : α),
  Eq (α := α) ((((Equiv.refl α).symm.trans x).trans (Equiv.refl α) : (a : α) → α) x_1 : α)
    ((id x : (a : α) → α) x_1 : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.EquivFunctor.Instances (goal)
Goal:
α β γ : Type u_1
x : α ≃ β
x_1 : β ≃ γ
⊢ Eq.{u_1 + 1} (α := Perm α → Perm γ) (fun (p : Perm α) ↦ ((x.trans x_1).symm.trans p).trans (x.trans x_1))
    ((fun (p : Perm β) ↦ (x_1.symm.trans p).trans x_1) ∘ fun (p : Perm α) ↦ (x.symm.trans p).trans x)
have h : ∀ (x_2 : Perm α) (x_3 : γ),
  Eq (α := γ) ((((x.trans x_1).symm.trans x_2).trans (x.trans x_1) : (a : γ) → γ) x_3 : γ)
    ((((fun (p : Perm β) ↦ (x_1.symm.trans p).trans x_1) ∘ fun (p : Perm α) ↦ (x.symm.trans p).trans x) x_2 :
          (a : γ) → γ)
        x_3 :
      γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.EquivFunctor.Instances (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset α → Finset α) (fun (s : Finset α) ↦ Finset.map (Equiv.refl α).toEmbedding s) id
have h : ∀ (x : Finset α) (a : α), a ∈ Finset.map (Equiv.refl α).toEmbedding x ↔ a ∈ id x
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.EquivFunctor.Instances (goal)
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
⊢ Eq.{u_1 + 1} (α := Finset α → Finset γ) (fun (s : Finset α) ↦ Finset.map (k.trans h).toEmbedding s)
    ((fun (s : Finset β) ↦ Finset.map h.toEmbedding s) ∘ fun (s : Finset α) ↦ Finset.map k.toEmbedding s)
have h₁ : ∀ (x : Finset α) (a : γ),
  a ∈ Finset.map (k.trans h).toEmbedding x ↔
    Membership.mem (γ := Finset γ)
      (((fun (s : Finset β) ↦ Finset.map h.toEmbedding s) ∘ fun (s : Finset α) ↦ Finset.map k.toEmbedding s) x) a
Tactic: ext _ a
-- Lean 4 proof step from Mathlib.Control.EquivFunctor.Instances (goal)
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a : γ
⊢ a ∈ Finset.map (k.trans h).toEmbedding x ↔
    Membership.mem (γ := Finset γ)
      (((fun (s : Finset β) ↦ Finset.map h.toEmbedding s) ∘ fun (s : Finset α) ↦ Finset.map k.toEmbedding s) x) a
have h₁ : (∃ a_1 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a) ↔
  Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
Tactic: simp
-- Lean 4 proof step from Mathlib.Control.EquivFunctor.Instances (goal)
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a : γ
⊢ (∃ a_1 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a) ↔
    Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
have h₁ : (∃ a_1 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a) →
  Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.EquivFunctor.Instances (goal)
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a : γ
h₁ :
  (∃ a_1 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a) →
    Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
⊢ (∃ a_1 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a) ↔
    Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
have h₂ : Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α) →
  ∃ a_2 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_2 : β) = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.EquivFunctor.Instances (goal)
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a : γ
h' : ∃ a_1 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a
⊢ Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
have h₁ : ∀ (a_1 : α) (ha₁ : a_1 ∈ x) (ha₂ : (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a),
  Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
Tactic: let ⟨a, ha₁, ha₂⟩ := h'
-- Lean 4 proof step from Mathlib.Control.EquivFunctor.Instances (goal)
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a_1 : γ
h' : ∃ a ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a : β) = a_1
a : α
ha₁ : a ∈ x
ha₂ : (h : (a : β) → γ) ((k : (a : α) → β) a : β) = a_1
⊢ Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a_1 : β) : α)
have h₁ : Membership.mem (α := α) x
  ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) ((h : (a : β) → γ) ((k : (a : α) → β) a : β) : γ) : β) : α)
Tactic: rw [← ha₂]
-- Lean 4 proof step from Mathlib.Control.EquivFunctor.Instances (goal)
Goal:
α β γ : Type u_1
k : α ≃ β
h : β ≃ γ
x : Finset α
a : γ
h' : Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α)
⊢ ∃ a_1 ∈ x, (h : (a : β) → γ) ((k : (a : α) → β) a_1 : β) = a
have h₁ : Membership.mem (α := α) x ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α) ∧
  (h : (a : β) → γ) ((k : (a : α) → β) ((k.symm : (a : β) → α) ((h.symm : (a : γ) → β) a : β) : α) : β) = a
Tactic: exists (Equiv.symm k) ((Equiv.symm h) a)
-- Lean 4 proof step from Mathlib.Control.EquivFunctor.Instances (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Fintype α → Fintype α)
    (fun (x : Fintype α) ↦ Fintype.ofBijective (⇑(Equiv.refl α) : (a : α) → α) ⋯) id
have h : ∀ (x : Fintype α), Fintype.ofBijective (⇑(Equiv.refl α) : (a : α) → α) sorry = id x
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.EquivFunctor (goal)
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ map e.symm (map e x) = x
have h : x = map (e.trans e.symm) x
Tactic: convert! (congr_fun (EquivFunctor.map_trans' e e.symm) x).symm
-- Lean 4 proof step from Mathlib.Control.EquivFunctor (goal)
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α β : Type u₀
e : α ≃ β
y : f β
⊢ map e (map e.symm y) = y
have h : y = map (e.symm.trans e) y
Tactic: convert! (congr_fun (EquivFunctor.map_trans' e.symm e) y).symm
-- Lean 4 proof step from Mathlib.Control.EquivFunctor (goal)
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α : Type u₀
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
have H : ∀ (x : f α),
  Eq (α := f α) ((mapEquiv f (Equiv.refl α) : (a : f α) → f α) x : f α) ((Equiv.refl (f α) : (a : f α) → f α) x : f α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.EquivFunctor (goal)
Goal:
f : Type u₀ → Type u₁
inst : Functor f
inst_1 : LawfulFunctor f
α : Type u₀
⊢ Eq.{u₁ + 1} (α := f α → f α) (Functor.map (⇑(Equiv.refl α) : (a : α) → α)) id
have h : ∀ (x : f α), (⇑(Equiv.refl α) : (a : α) → α) <$> x = id x
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.EquivFunctor (goal)
Goal:
f : Type u₀ → Type u₁
inst : Functor f
inst_1 : LawfulFunctor f
α β γ : Type u₀
k : α ≃ β
h : β ≃ γ
⊢ Eq.{u₁ + 1} (α := f α → f γ) (Functor.map (⇑(k.trans h) : (a : α) → γ))
    (comp (β := f β) (Functor.map (⇑h : (a : β) → γ)) (Functor.map (⇑k : (a : α) → β)))
have h₁ : ∀ (x : f α),
  Eq (α := f γ) ((⇑(k.trans h) : (a : α) → γ) <$> x)
    (comp (β := f β) (Functor.map (⇑h : (a : β) → γ)) (Functor.map (⇑k : (a : α) → β)) x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Control.Fix (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
⊢ Part.fix (β := β) f x =
    Fix.approx (β := β) f (Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h').succ x
have this : p (Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h')
Tactic: have : p (Nat.find h') := Nat.find_spec h'
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
this : p (Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h')
⊢ Part.fix (β := β) f x =
    Fix.approx (β := β) f (Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h').succ x
have generalize : ∀ (k : ℕ) (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k),
  Part.fix (β := β) f x = Fix.approx (β := β) f k.succ x
Tactic: generalize hk : Nat.find h' = k
-- Lean 4 proof step from Mathlib.Control.Fix (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
this : p (Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h')
k : ℕ
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k
⊢ Part.fix (β := β) f x = Fix.approx (β := β) f k.succ x
have hk₁ : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑(Upto.zero (p := p)) : ℕ)
Tactic: replace hk : Nat.find h' = k + (@Upto.zero p).val := hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Control.Fix (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
this : p (Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h')
k : ℕ
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑(Upto.zero (p := p)) : ℕ)
⊢ Part.fix (β := β) f x = Fix.approx (β := β) f k.succ x
have this₁ : p (k + (↑(Upto.zero (p := p)) : ℕ))
Tactic: rw [hk] at this
Cleared hypotheses: this, hk
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
k : ℕ
this : p (k + (↑(Upto.zero (p := p)) : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑(Upto.zero (p := p)) : ℕ)
⊢ Part.fix (β := β) f x = Fix.approx (β := β) f k.succ x
have revert : ∀ (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑(Upto.zero (p := p)) : ℕ)),
  Part.fix (β := β) f x = Fix.approx (β := β) f k.succ x
Tactic: revert hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
k : ℕ
this : p (k + (↑(Upto.zero (p := p)) : ℕ))
⊢ ∀ (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑(Upto.zero (p := p)) : ℕ)),
    (assert (∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom) fun (h : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom) ↦
        ⋯.fix (C := fun (y : Upto fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom) ↦ (a : α) → Part (β a)) (r :=
          Upto.GT fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)
          (fixAux (β := β) f (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom))
          (Upto.zero (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)) x) =
      Fix.approx (β := β) f (k + 1) x
have rw : ∀ (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑(Upto.zero (p := p)) : ℕ)),
  sorry.fix (C := fun (y : Upto fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom) ↦ (a : α) → Part (β a)) (r :=
      Upto.GT fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)
      (fixAux (β := β) f (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom))
      (Upto.zero (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)) x =
    Fix.approx (β := β) f (k + 1) x
Tactic: rw [assert_pos h']
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
k : ℕ
this : p (k + (↑(Upto.zero (p := p)) : ℕ))
⊢ ∀ (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑(Upto.zero (p := p)) : ℕ)),
    ⋯.fix (C := fun (y : Upto fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom) ↦ (a : α) → Part (β a)) (r :=
        Upto.GT fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)
        (fixAux (β := β) f (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom))
        (Upto.zero (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)) x =
      Fix.approx (β := β) f (k + 1) x
have revert : ∀ (this : p (k + (↑(Upto.zero (p := p)) : ℕ)))
  (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑(Upto.zero (p := p)) : ℕ)),
  sorry.fix (C := fun (y : Upto fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom) ↦ (a : α) → Part (β a)) (r :=
      Upto.GT fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)
      (fixAux (β := β) f (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom))
      (Upto.zero (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)) x =
    Fix.approx (β := β) f (k + 1) x
Tactic: revert this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
k : ℕ
⊢ ∀ (this : p (k + (↑(Upto.zero (p := p)) : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑(Upto.zero (p := p)) : ℕ)),
    ⋯.fix (C := fun (y : Upto fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom) ↦ (a : α) → Part (β a)) (r :=
        Upto.GT fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)
        (fixAux (β := β) f (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom))
        (Upto.zero (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)) x =
      Fix.approx (β := β) f (k + 1) x
have generalize : ∀ (z : Upto p) (this : p (k + (↑z : ℕ)))
  (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑z : ℕ)),
  sorry.fix (C := fun (y : Upto fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom) ↦ (a : α) → Part (β a)) (r :=
      Upto.GT fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)
      (fixAux (β := β) f (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)) z x =
    Fix.approx (β := β) f (k + 1) x
Tactic: generalize Upto.zero = z
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
k : ℕ
z : Upto p
_this : p (k + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑z : ℕ)
⊢ ⋯.fix (C := fun (y : Upto fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom) ↦ (a : α) → Part (β a)) (r :=
      Upto.GT fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)
      (fixAux (β := β) f (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)) z x =
    Fix.approx (β := β) f (k + 1) x
have suffices : ∀ (x' : α) (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
  hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y) (fixAux (β := β) f (p := p))
      z x' =
    Fix.approx (β := β) f k.succ x'
Tactic: suffices ∀ x' hwf,
    WellFounded.fix hwf (fixAux f) z x' = Fix.approx f (succ k) x'
    from this _ _
-- Lean 4 proof step from Mathlib.Control.Fix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
z : Upto p
_this : p (0 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = 0 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
⊢ hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y) (fixAux (β := β) f (p := p))
      z x' =
    Fix.approx (β := β) f (Nat.succ 0) x'
have zero : f
    (fun (x : α) ↦
      assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
        hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
          (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x)
    x' =
  f (Fix.approx (β := β) f 0) x'
Tactic: rw [Fix.approx, WellFounded.fix_eq, fixAux]