awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.Functor (goal)
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ { map := @m, mapConst := @mc : Functor F } = { map := @m', mapConst := @mc' }
have refl : ∀ (H2 : LawfulFunctor F) (H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x),
  { map := @m, mapConst := @mc : Functor F } = { map := @m, mapConst := @mc' }
Tactic: cases show @m = @m' by funext α β f x; apply H
Cleared hypotheses: m', H2, H
-- Lean 4 proof step from Mathlib.Control.Functor (goal)
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ { map := @m, mapConst := @mc : Functor F } = { map := @m, mapConst := @mc' }
have refl : @mc = @mc'
Tactic: congr
-- Lean 4 proof step from Mathlib.Control.Functor (goal)
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ @mc = @mc'
have refl : ∀ (α β : Type u_1), Eq (α := α → F β → F α) mc mc'
Tactic: funext α β
-- Lean 4 proof step from Mathlib.Control.Functor (hypothesis)
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
⊢ Eq (α := α → F β → F α) mc mc'
have E1 : ∀ {α β : Type u_1}, Eq (α := α → F β → F α) mapConst (map ∘ Function.const β)
Tactic: have E1 := @map_const _ ⟨@m, @mc⟩ H1
-- Lean 4 proof step from Mathlib.Control.Functor (hypothesis)
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
E1 : ∀ {α β : Type u_1}, Eq (α := α → F β → F α) mapConst (map ∘ Function.const β)
⊢ Eq (α := α → F β → F α) mc mc'
have E2 : ∀ {α β : Type u_1}, Eq (α := α → F β → F α) mapConst (map ∘ Function.const β)
Tactic: have E2 := @map_const _ ⟨@m, @mc'⟩ H2
-- Lean 4 proof step from Mathlib.Control.Functor (goal)
Goal:
γ : Type u_1
⊢ LawfulFunctor.{u_2, u_1} (Const γ)
have map_const : ∀ {α β : Type u_2}, Eq (α := α → Const γ β → Const γ α) mapConst (map ∘ Function.const β)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Functor (goal)
Goal:
γ : Type u_1
map_const : ∀ {α β : Type u_2}, Eq (α := α → Const γ β → Const γ α) mapConst (map ∘ Function.const β)
⊢ LawfulFunctor.{u_2, u_1} (Const γ)
have id_map : ∀ {α : Type u_2} (x : Const γ α), id <$> x = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Functor (goal)
Goal:
γ : Type u_1
map_const : ∀ {α β : Type u_2}, Eq (α := α → Const γ β → Const γ α) mapConst (map ∘ Function.const β)
id_map : ∀ {α : Type u_2} (x : Const γ α), id <$> x = x
⊢ LawfulFunctor.{u_2, u_1} (Const γ)
have comp_map : ∀ {α β γ_1 : Type u_2} (g : α → β) (h : β → γ_1) (x : Const γ α), (h ∘ g) <$> x = h <$> g <$> x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Functor (goal)
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Functor F
inst_1 : Functor G
inst_2 : LawfulFunctor F
inst_3 : LawfulFunctor G
α : Type v
x : F (G α)
⊢ Comp.map id (mk x) = mk x
have simp : mk (mk x) = mk x
Tactic: simp only [Comp.map, id_map, id_map']
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (Nat.succ 0))
have zero : LE.le (α := (a : α) → Part (β a)) (⊥ : (a : α) → Part (β a))
  ((f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) ⊥ : (a : α) → Part (β a))
Tactic: dsimp [approx]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ)
have zero : LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
  (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (Nat.succ 0))
Tactic: induction i with
  | zero => dsimp [approx]; apply @bot_le _ _ _ (f ⊥)
  | succ _ i_ih => intro; apply f.monotone; apply i_ih
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
zero :
  LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (Nat.succ 0))
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ)
have succ : ∀ (n : ℕ)
  (i_ih :
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n.succ)),
  LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (n + 1))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (n + 1).succ)
Tactic: induction i with
  | zero => dsimp [approx]; apply @bot_le _ _ _ (f ⊥)
  | succ _ i_ih => intro; apply f.monotone; apply i_ih
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
hij : i ≤ 0
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
have zero : LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
  (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
Tactic: cases hij
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih :
  ∀ (hij : i ≤ j),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)
hij : i ≤ j + 1
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
have succ : ∀
  (ih :
    ∀ (hij : j + 1 ≤ j),
      LE.le (α := (a : α) → Part (β a))
        (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
        (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)),
  LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
Tactic: cases hij
Cleared hypotheses: i, ih, hij
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih :
  ∀ (hij : i ≤ j),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)
hij : i ≤ j + 1
succ :
  ∀
    (ih :
      ∀ (hij : j + 1 ≤ j),
        LE.le (α := (a : α) → Part (β a))
          (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
          (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
have succ₁ : i.le j →
  LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
Tactic: cases hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij : i ≤ j
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)
have zero : ∀ (hij : i ≤ 0),
  LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
Tactic: induction j with
  | zero => cases hij; exact le_rfl
  | succ j ih =>
    cases hij; · exact le_rfl
    exact le_trans (ih ‹_›) (approx_mono' f)
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij : i ≤ j
zero :
  ∀ (hij : i ≤ 0),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)
have succ : ∀ (j : ℕ)
  (ih :
    ∀ (hij : i ≤ j),
      LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
        (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j))
  (hij : i ≤ j + 1),
  LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
Tactic: induction j with
  | zero => cases hij; exact le_rfl
  | succ j ih =>
    cases hij; · exact le_rfl
    exact le_trans (ih ‹_›) (approx_mono' f)
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
⊢ Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
have pos : ∀ (h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)),
  Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
Tactic: by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
pos :
  ∀
    (h₀ :
      ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)),
    Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
      ∃ (i : ℕ),
        Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
          b
⊢ Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
have neg : ∀
  (h₀ :
    ¬∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)),
  Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
Tactic: by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
⊢ Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
have pos : Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b ↔
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
Tactic: simp only [Part.fix_def f h₀]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
⊢ Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
            Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a))
            h₀).succ
        a)
      b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
have pos : Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b →
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
pos :
  Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
            Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a))
            h₀).succ
        a)
      b →
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
⊢ Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
            Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a))
            h₀).succ
        a)
      b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
have pos₁ : (∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b) →
  Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.LawfulFix (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
hh :
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
⊢ Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b
have h₁ : Dom.{u_2} (α := β a)
  (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
    (Nat.find (p := fun (n : ℕ) ↦
      Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀)
    a)
Tactic: have h₁ := Nat.find_spec h₀
-- Lean 4 proof step from Mathlib.Control.LawfulFix (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
hh :
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
h₁ :
  Dom.{u_2} (α := β a)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
        Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀)
      a)
⊢ Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b
have h₂ : ∃ (y : β a),
  Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
        Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀)
      a)
    y
Tactic: rw [dom_iff_mem] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
hh :
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
h₁ :
  ∃ (y : β a),
    Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀)
        a)
      y
⊢ Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b
have pos : ∀ (y : β a)
  (h₁ :
    Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀)
        a)
      y),
  Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b
Tactic: obtain ⟨y, h₁⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Control.LawfulFix (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
hh :
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
y : β a
h₁ :
  Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
        Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀)
      a)
    y
⊢ Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b
have h₂ : Membership.mem (γ := Part (β a))
  (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
    (Nat.find (p := fun (n : ℕ) ↦
        Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
    a)
  y
Tactic: replace h₁ := approx_mono' f _ _ h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
hh :
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
y : β a
h₁ :
  Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    y
this : y = b
⊢ Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b
have subst : ∀
  (hh :
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
        y),
  Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    y
Tactic: subst this
Cleared hypotheses: b, hh, this