awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.LawfulFix
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)
y : β a
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
j : ℕ
h₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
this :
  ∀ {α : 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))
    (y : β a) (i : ℕ)
    (hh :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b)
    (j : ℕ)
    (h₁ :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y)
    (case : i ≤ j), y = b
case : ¬i ≤ j
H : j ≤ i
⊢ Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b

Tactic:
assumption
-- Module: Mathlib.Control.LawfulFix
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)
y : β a
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
j : ℕ
h₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
this :
  ∀ {α : 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))
    (y : β a) (i : ℕ)
    (hh :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b)
    (j : ℕ)
    (h₁ :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y)
    (case : i ≤ j), y = b
case : ¬i ≤ j
H : j ≤ i
⊢ j ≤ i

Tactic:
assumption
-- Module: Mathlib.Control.LawfulFix
Goal:
α_1 : Type u_1
β_1 : α_1 → Type u_2
f_1 : ((a : α_1) → Part (β_1 a)) →o (a : α_1) → Part (β_1 a)
α : 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)
y : β a
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
j : ℕ
h₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
case : i ≤ j
⊢ Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) b

Tactic:
replace hh := approx_mono f case _ _ hh
-- Module: Mathlib.Control.LawfulFix
Goal:
α_1 : Type u_1
β_1 : α_1 → Type u_2
f_1 : ((a : α_1) → Part (β_1 a)) →o (a : α_1) → Part (β_1 a)
α : 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)
y : β a
i j : ℕ
h₁ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
case : i ≤ j
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) b
⊢ y = b

Tactic:
apply Part.mem_unique h₁ hh

Premises used: Part.mem_unique
-- Module: Mathlib.Control.LawfulFix
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)
neg : ∀ (x : ℕ), b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x 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:
simp only [fix_def' (⇑f) h₀, not_exists, false_iff, notMem_none]

Premises used: not_exists, false_iff, Part.fix_def', Part.notMem_none, DFunLike.coe
-- Module: Mathlib.Control.LawfulFix
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)
⊢ ∀ (x : ℕ) (x_1 : β a), x_1 ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x a

Tactic:
simp only [dom_iff_mem, not_exists] at h₀

Premises used: not_exists, Part.dom_iff_mem
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∀ (x : ℕ) (x_1 : β a), x_1 ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x a
x : ℕ
⊢ b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x a

Tactic:
apply h₀
-- Module: Mathlib.Control.LawfulFix
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
neg 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
⊢ 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:
classical
  by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
  · simp only [Part.fix_def f h₀]
    constructor <;> intro hh
    · exact ⟨_, hh⟩
    have h₁ := Nat.find_spec h₀
    rw [dom_iff_mem] at h₁
    obtain ⟨y, h₁⟩ := h₁
    replace h₁ := approx_mono' f _ _ h₁
    suffices y = b by
      subst this
      exact h₁
    obtain ⟨i, hh⟩ := hh
    revert h₁; generalize succ (Nat.find h₀) = j; intro h₁
    wlog case : i ≤ j
    · rcases le_total i j with H | H <;> [skip; symm] <;> apply_assumption <;> assumption
    replace hh := approx_mono f case _ _ hh
    apply Part.mem_unique h₁ hh
  · simp only [fix_def' (⇑f) h₀, not_exists, false_iff, notMem_none]
    simp only [dom_iff_mem, not_exists] at h₀
    intro; apply h₀

Premises used: not_exists, Part.dom_iff_mem, false_iff, Part.notMem_none
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
rw :
  ∃ (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

Tactic:
rw [mem_iff f]

Premises used: Part.Fix.mem_iff
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
⊢ ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b

Tactic:
⟨_, hh⟩

Premises used: Exists.intro
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
⊢ ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b

Tactic:
exact ⟨_, hh⟩
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
pos :
  ∀
    (hh :
      ∃ (i : ℕ) (b : β x),
        Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
          b),
    ∃ (i : ℕ),
      LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
        (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
neg :
  ∀ (hh : ∀ (i : ℕ) (b : β x), b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x),
    ∃ (i : ℕ),
      LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
        (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
⊢ ∃ (i : ℕ),
    LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)

Tactic:
by_cases! hh : ∃ i b, b ∈ approx f i x
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh :
  ∃ (i : ℕ) (b : β x),
    Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b
pos :
  ∀ (i : ℕ) (b : β x)
    (hb :
      Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
        b),
    ∃ (i : ℕ),
      LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
        (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
⊢ ∃ (i : ℕ),
    LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)

Tactic:
rcases hh with ⟨i, b, hb⟩
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b
pos :
  LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
⊢ ∃ (i : ℕ),
    LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)

Tactic:
exists i
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b
b' : β x
h' : Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b'
⊢ Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b

Tactic:
have hb' := approx_le_fix f i _ _ hb
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b
b' : β x
h' : Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b'
hb' : Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b
⊢ Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'

Tactic:
obtain rfl := Part.mem_unique h' hb'

Premises used: rfl, Part.mem_unique
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b
b' : β x
h' : Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b'
hb' : Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b
hb₁ : Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'
⊢ Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b'

Tactic:
obtain rfl := Part.mem_unique h' hb'

Premises used: rfl, Part.mem_unique
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b' : β x
h' : Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b'
hb : Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'
hb' : Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b'
⊢ Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'

Tactic:
hb
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b' : β x
h' : Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b'
hb : Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'
hb' : Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b'
⊢ Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'

Tactic:
exact hb
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x
neg :
  LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0 x)
⊢ ∃ (i : ℕ),
    LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)

Tactic:
exists 0
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x
b' : β x
h' : Membership.mem (γ := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x) b'
⊢ ∃ (i : ℕ),
    Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'

Tactic:
simp only [mem_iff f] at h'

Premises used: Part.Fix.mem_iff
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x
b' : β x
h' :
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'
neg :
  ∀ (i : ℕ)
    (h' :
      Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
        b'),
    Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0 x) b'
⊢ Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0 x) b'

Tactic:
obtain ⟨i, h'⟩ := h'
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x
b' : β x
i : ℕ
h' : Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x) b'
⊢ Membership.mem (γ := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0 x) b'

Tactic:
cases hh _ _ h'
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : (a : α) → Part (β a)
simp :
  ∀ (x_1 : ℕ) (h : x = (approxChain (β := β) f : (a : ℕ) → (a : α) → Part (β a)) x_1),
    x ≤ (f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x
⊢ x ∈ approxChain (β := β) f → x ≤ (f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x

Tactic:
simp only [Membership.mem, forall_exists_index]

Premises used: Membership.mem, forall_exists_index
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ LE.le (α := (a : α) → Part (β a)) ((approxChain (β := β) f : (a : ℕ) → (a : α) → Part (β a)) i : (a : α) → Part (β a))
    ((f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        ((approxChain (β := β) f : (a : ℕ) → (a : α) → Part (β a)) i : (a : α) → Part (β a)) :
      (a : α) → Part (β a))

Tactic:
apply approx_mono'

Premises used: Part.Fix.approx_mono'
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i ∈ approxChain (β := β) f

Tactic:
Stream'.mem_of_get_eq rfl

Premises used: Stream'.mem_of_get_eq, Stream'.get, rfl, Stream'.Any
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) ≤ ωSup (approxChain (β := β) f)
a₁ : ωSup (approxChain (β := β) f) ≤ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
⊢ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) = ωSup (approxChain (β := β) f)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
a :
  ∀ (i : ℕ)
    (hx :
      LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
        (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)),
    Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x ≤ ωSup (approxChain (β := β) f) x
⊢ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x ≤ ωSup (approxChain (β := β) f) x

Tactic:
obtain ⟨i, hx⟩ := exists_fix_le_approx f x

Premises used: Part.Fix.exists_fix_le_approx
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx :
  LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
trans :
  LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x)
trans₁ :
  approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x ≤ ωSup (approxChain (β := β) f) x
⊢ Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x ≤ ωSup (approxChain (β := β) f) x

Tactic:
trans approx f i.succ x

Premises used: Part.Fix.approx, Nat.succ, DFunLike.coe
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx trans :
  LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
trans₁ :
  LE.le.{u_2} (α := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x)
trans₂ : Part (β x)
⊢ LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x)

Tactic:
trans
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx :
  LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
⊢ LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)

Tactic:
apply hx
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx :
  LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
⊢ LE.le.{u_2} (α := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x)

Tactic:
apply approx_mono' f

Premises used: Part.Fix.approx_mono'
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx :
  LE.le.{u_2} (α := Part (β x)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) x)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i x)
apply :
  LE.le.{u_2} (α := Part (β x)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x)
    (((approxChain (β := β) f).map (Pi.evalOrderHom (π := fun (a : α) ↦ Part (β a)) x) : (a : ℕ) → Part (β x)) i.succ)
⊢ approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ x ≤ ωSup (approxChain (β := β) f) x

Tactic:
apply le_ωSup_of_le i.succ

Premises used: Nat.succ, OmegaCompletePartialOrder.le_ωSup_of_le