awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ (map e.symm ∘ map e) x = map (e.trans e.symm) x

Tactic:
(congr_fun (EquivFunctor.map_trans' e e.symm) x).symm

Premises used: EquivFunctor.map_trans', congr_fun, Equiv.symm, Eq.symm
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
h : x = map (e.trans e.symm) x
⊢ map e.symm (map e x) = x

Tactic:
convert! (congr_fun (EquivFunctor.map_trans' e e.symm) x).symm

Premises used: EquivFunctor.map_trans', congr_fun, Equiv.symm, Eq.symm
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ x = map (e.trans e.symm) x

Tactic:
simp
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α β : Type u₀
e : α ≃ β
y : f β
⊢ (map e ∘ map e.symm) y = map (e.symm.trans e) y

Tactic:
(congr_fun (EquivFunctor.map_trans' e.symm e) y).symm

Premises used: EquivFunctor.map_trans', congr_fun, Equiv.symm, Eq.symm
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α β : Type u₀
e : α ≃ β
y : f β
h : y = map (e.symm.trans e) y
⊢ map e (map e.symm y) = y

Tactic:
convert! (congr_fun (EquivFunctor.map_trans' e.symm e) y).symm

Premises used: EquivFunctor.map_trans', congr_fun, Equiv.symm, Eq.symm
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α β : Type u₀
e : α ≃ β
y : f β
⊢ y = map (e.symm.trans e) y

Tactic:
simp
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ (mapEquiv f e : (a : f α) → f β) x = map e x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α β : Type u₀
e : α ≃ β
y : f β
⊢ ((mapEquiv f e).symm : (a : f β) → f α) y = map e.symm y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α : Type u₀
H :
  ∀ (x : f α),
    Eq (α := f α) ((mapEquiv f (Equiv.refl α) : (a : f α) → f α) x : f α) ((Equiv.refl (f α) : (a : f α) → f α) x : f α)
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)

Tactic:
ext
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α : Type u₀
x : f α
⊢ Eq (α := f α) ((mapEquiv f (Equiv.refl α) : (a : f α) → f α) x : f α) ((Equiv.refl (f α) : (a : f α) → f α) x : f α)

Tactic:
simp [mapEquiv]

Premises used: EquivFunctor.mapEquiv
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α β : Type u₀
e : α ≃ β
⊢ (mapEquiv f e).symm = mapEquiv f e.symm

Tactic:
Equiv.ext <| mapEquiv_symm_apply f e

Premises used: Equiv.ext, EquivFunctor.mapEquiv_symm_apply
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : EquivFunctor f
α β γ : Type u₀
ab : α ≃ β
bc : β ≃ γ
x : f α
⊢ Eq (α := f γ) (((mapEquiv f ab).trans (mapEquiv f bc) : (a : f α) → f γ) x : f γ)
    ((mapEquiv f (ab.trans bc) : (a : f α) → f γ) x : f γ)

Tactic:
simp [mapEquiv, map_trans']

Premises used: EquivFunctor.mapEquiv, EquivFunctor.map_trans'
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : Functor f
inst_1 : LawfulFunctor f
α : Type u₀
h : ∀ (x : f α), (⇑(Equiv.refl α) : (a : α) → α) <$> x = id x
⊢ Eq.{u₁ + 1} (α := f α → f α) (Functor.map (⇑(Equiv.refl α) : (a : α) → α)) id

Tactic:
ext
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : Functor f
inst_1 : LawfulFunctor f
α : Type u₀
x : f α
⊢ (⇑(Equiv.refl α) : (a : α) → α) <$> x = id x

Tactic:
apply LawfulFunctor.id_map

Premises used: LawfulFunctor.id_map
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : Functor f
inst_1 : LawfulFunctor f
α β γ : Type u₀
k : α ≃ β
h : β ≃ γ
h₁ :
  ∀ (x : f α),
    Eq (α := f γ) ((⇑(k.trans h) : (a : α) → γ) <$> x)
      (comp (β := f β) (Functor.map (⇑h : (a : β) → γ)) (Functor.map (⇑k : (a : α) → β)) x)
⊢ Eq.{u₁ + 1} (α := f α → f γ) (Functor.map (⇑(k.trans h) : (a : α) → γ))
    (comp (β := f β) (Functor.map (⇑h : (a : β) → γ)) (Functor.map (⇑k : (a : α) → β)))

Tactic:
ext x
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : Functor f
inst_1 : LawfulFunctor f
α β γ : Type u₀
k : α ≃ β
h : β ≃ γ
x : f α
⊢ Eq (α := f γ) ((⇑(k.trans h) : (a : α) → γ) <$> x)
    (comp (β := f β) (Functor.map (⇑h : (a : β) → γ)) (Functor.map (⇑k : (a : α) → β)) x)

Tactic:
apply LawfulFunctor.comp_map k h x

Premises used: DFunLike.coe, LawfulFunctor.comp_map
-- Module: Mathlib.Control.EquivFunctor
Goal:
f : Type u₀ → Type u₁
inst : Applicative f
inst_1 : LawfulApplicative f
α β : Type u₀
h : ∀ (γ : Type u₀), Injective.{u₀ + 1, u₁ + 1} (α := γ) (β := f γ) pure
e₁ e₂ : α ≃ β
H : mapEquiv f e₁ = mapEquiv f e₂
x : α
⊢ Eq.{u₁ + 1} (α := f β) (pure ((e₁ : (a : α) → β) x) : f β) (pure ((e₂ : (a : α) → β) x) : f β)

Tactic:
simpa [EquivFunctor.map] using Equiv.congr_fun H (pure x)

Premises used: Pure.pure, Equiv.congr_fun, EquivFunctor.map
-- Module: Mathlib.Control.Fix
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
⊢ p (Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h')

Tactic:
have : p (Nat.find h') := Nat.find_spec h'
-- Module: Mathlib.Control.Fix
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')
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
⊢ Part.fix (β := β) f x =
    Fix.approx (β := β) f (Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h').succ x

Tactic:
generalize hk : Nat.find h' = k

Premises used: Nat.find
-- Module: Mathlib.Control.Fix
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
⊢ 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
-- Module: Mathlib.Control.Fix
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)) : ℕ)
⊢ p (k + (↑(Upto.zero (p := p)) : ℕ))

Tactic:
rw [hk] at this
-- Module: Mathlib.Control.Fix
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)) : ℕ)
this₁ : p (k + (↑(Upto.zero (p := p)) : ℕ))
⊢ Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑(Upto.zero (p := p)) : ℕ)

Tactic:
rw [hk] at this
-- Module: Mathlib.Control.Fix
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)) : ℕ)
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
⊢ Part.fix (β := β) f x = Fix.approx (β := β) f k.succ x

Tactic:
revert hk
-- Module: Mathlib.Control.Fix
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)) : ℕ))
rw :
  ∀ (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
⊢ ∀ (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

Tactic:
rw [assert_pos h']

Premises used: Part.assert_pos
-- Module: Mathlib.Control.Fix
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)) : ℕ))
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)) : ℕ)),
    ⋯.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
⊢ ∀ (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

Tactic:
revert this
-- Module: Mathlib.Control.Fix
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 : ℕ
generalize :
  ∀ (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
⊢ ∀ (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

Tactic:
generalize Upto.zero = z

Premises used: Nat.Upto.zero
-- Module: Mathlib.Control.Fix
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 : ℕ)
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'
⊢ ⋯.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:
suffices ∀ x' hwf,
    WellFounded.fix hwf (fixAux f) z x' = Fix.approx f (succ k) x'
    from this _ _
-- Module: Mathlib.Control.Fix
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' : α
zero :
  ∀ (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'
⊢ ∀ (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'

Tactic:
_
-- Module: Mathlib.Control.Fix
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
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'
⊢ 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'

Tactic:
rw [Fix.approx, WellFounded.fix_eq, fixAux]

Premises used: WellFounded.fix_eq, Part.Fix.approx, Part.fixAux
-- Module: Mathlib.Control.Fix
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
zero :
  (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) =
    Fix.approx (β := β) f 0
⊢ 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:
congr
-- Module: Mathlib.Control.Fix
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
zero :
  ∀ (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) =
      Fix.approx (β := β) f 0 x
⊢ (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) =
    Fix.approx (β := β) f 0

Tactic:
ext x : 1
-- Module: Mathlib.Control.Fix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x_1 : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x_1).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x_1).Dom
z : Upto p
_this : p (0 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x_1).Dom) h' = 0 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x : α
zero : none = Fix.approx (β := β) f 0 x
zero₁ : ¬¬p (↑z : ℕ)
⊢ (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) =
    Fix.approx (β := β) f 0 x

Tactic:
rw [assert_neg]

Premises used: Part.assert_neg
-- Module: Mathlib.Control.Fix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x_1 : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x_1).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x_1).Dom
z : Upto p
_this : p (0 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x_1).Dom) h' = 0 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x : α
⊢ none = Fix.approx (β := β) f 0 x

Tactic:
rfl
-- Module: Mathlib.Control.Fix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x_1 : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x_1).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x_1).Dom
z : Upto p
_this : p (0 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x_1).Dom) h' = 0 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x : α
zero :
  ∀ (_this : p (↑z : ℕ)) (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x_1).Dom) h' = 0 + (↑z : ℕ))
    (x' : α), (WellFounded fun (y x : Upto p) ↦ x < y) → ∀ (x : α), ¬¬p (↑z : ℕ)
⊢ ¬¬p (↑z : ℕ)

Tactic:
rw [Nat.zero_add] at _this

Premises used: Nat.zero_add
-- Module: Mathlib.Control.Fix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x_1 : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x_1).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x_1).Dom
z : Upto p
_this : p (↑z : ℕ)
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x_1).Dom) h' = 0 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x : α
⊢ ¬¬p (↑z : ℕ)

Tactic:
simpa only [not_not, Coe]

Premises used: Classical.not_not, Coe
-- Module: Mathlib.Control.Fix
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
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑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 n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
succ :
  ∀ (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 (n + 1).succ 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 (n + 1).succ x'

Tactic:
_
-- Module: Mathlib.Control.Fix
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
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑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 n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
succ :
  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 (n + 1)) x'
⊢ 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 (n + 1).succ x'

Tactic:
rw [Fix.approx, WellFounded.fix_eq, fixAux]

Premises used: WellFounded.fix_eq, Part.Fix.approx, Part.fixAux
-- Module: Mathlib.Control.Fix
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
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑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 n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
succ :
  (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) =
    Fix.approx (β := β) f (n + 1)
⊢ 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 (n + 1)) x'

Tactic:
congr