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)
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)
    y

Tactic:
replace h₁ := approx_mono' f _ _ h₁
-- 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)
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
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
⊢ 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:
subst this
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
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
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:
h₁
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
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
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:
exact h₁
-- 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)
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
pos : 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

Tactic:
suffices y = b by
      subst this
      exact h₁
-- 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)
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
pos :
  ∀ (i : ℕ)
    (hh :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
        b),
    y = b
⊢ y = b

Tactic:
obtain ⟨i, hh⟩ := hh
-- 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
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
i : ℕ
hh : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
pos :
  ∀
    (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),
    y = b
⊢ y = b

Tactic:
revert h₁
-- 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
pos :
  ∀ (j : ℕ)
    (h₁ :
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a)
        y),
    y = b
⊢ ∀
    (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),
    y = b

Tactic:
generalize succ (Nat.find h₀) = j

Premises used: Nat.find, Nat.succ
-- 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
pos :
  ∀
    (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), y = b
wlog :
  ∀ {α : 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
⊢ y = b

Tactic:
wlog case : i ≤ j
-- 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
pos : ∀ (H : i ≤ j), y = b
pos₁ : ∀ (H : j ≤ i), y = b
⊢ y = b

Tactic:
rcases le_total i j with H | H

Premises used: le_total
-- 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
pos : b = y
⊢ y = b

Tactic:
symm
-- 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
pos : ∀ (H : i ≤ j), y = b
pos₁ : ∀ (H : j ≤ i), b = y
⊢ y = b

Tactic:
rcases le_total i j with H | H <;> [skip; symm]

Premises used: le_total
-- 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 : i ≤ j
pos : ∃ (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)) i a) b
pos₂ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y
pos₃ : i ≤ j
pos₄ : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
pos₅ pos₆ : ℕ
⊢ y = b

Tactic:
apply_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
pos : ∃ (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)) j a) y
pos₂ : Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
pos₃ : j ≤ i
pos₄ : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
pos₅ pos₆ : ℕ
⊢ b = y

Tactic:
apply_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 : i ≤ j
⊢ ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)

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 : i ≤ j
⊢ 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 : i ≤ j
⊢ Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y

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 : i ≤ j
⊢ i ≤ j

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
⊢ ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)

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
⊢ Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j a) y

Tactic:
assumption