-- Mathlib/Control/LawfulFix.lean
theorem exists_fix_le_approx (x : α) : ∃ i, Part.fix f x ≤ approx f i x

Proof state:
case neg.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), x_2 ∉ approx (⇑f) x_1 x
b' : β x
i : ℕ
h' : b' ∈ approx (⇑f) i x
⊢ b' ∈ approx (⇑f) 0 x

Tactic:
cases hh _ _ h'

Result:
no goals

Proof state:
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

Tactic:
exists i

Result:
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) i x

Proof state:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), x_2 ∉ approx (⇑f) x_1 x
b' : β x
h' : ∃ i, b' ∈ approx (⇑f) i x
⊢ b' ∈ approx (⇑f) 0 x

Tactic:
obtain ⟨i, h'⟩ := h'

Result:
case neg.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), x_2 ∉ approx (⇑f) x_1 x
b' : β x
i : ℕ
h' : b' ∈ approx (⇑f) i x
⊢ b' ∈ approx (⇑f) 0 x

Proof state:
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
b' : β x
h' : b' ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) i x

Tactic:
have hb' := approx_le_fix f i _ _ hb

Result:
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
b' : β x
h' : b' ∈ Part.fix (⇑f) x
hb' : b ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) i x

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

Tactic:
by_cases hh : ∃ i b, b ∈ approx f i x

Result:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∃ i b, b ∈ approx (⇑f) i x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ¬∃ i b, b ∈ approx (⇑f) i x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

Proof state:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∃ i b, b ∈ approx (⇑f) i x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

Tactic:
rcases hh with ⟨i, b, hb⟩

Result:
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

Proof state:
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b' : β x
h' : b' ∈ Part.fix (⇑f) x
hb : b' ∈ approx (⇑f) i x
hb' : b' ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) i x

Tactic:
exact hb

Result:
no goals

Proof state:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ¬∃ i b, b ∈ approx (⇑f) i x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

Tactic:
simp only [not_exists] at hh

Result:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), x_2 ∉ approx (⇑f) x_1 x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

Proof state:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), x_2 ∉ approx (⇑f) x_1 x
b' : β x
h' : b' ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) 0 x

Tactic:
simp only [mem_iff f] at h'

Result:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), x_2 ∉ approx (⇑f) x_1 x
b' : β x
h' : ∃ i, b' ∈ approx (⇑f) i x
⊢ b' ∈ approx (⇑f) 0 x

Proof state:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), x_2 ∉ approx (⇑f) x_1 x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) 0 x

Tactic:
intro b' h'

Result:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), x_2 ∉ approx (⇑f) x_1 x
b' : β x
h' : b' ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) 0 x

Proof state:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), x_2 ∉ approx (⇑f) x_1 x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

Tactic:
exists 0

Result:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (x_1 : ℕ) (x_2 : β x), x_2 ∉ approx (⇑f) x_1 x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) 0 x

Proof state:
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) i x

Tactic:
intro b' h'

Result:
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
b' : β x
h' : b' ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) i x

Proof state:
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b : β x
hb : b ∈ approx (⇑f) i x
b' : β x
h' : b' ∈ Part.fix (⇑f) x
hb' : b ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) i x

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

Result:
case pos.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
b' : β x
h' : b' ∈ Part.fix (⇑f) x
hb : b' ∈ approx (⇑f) i x
hb' : b' ∈ Part.fix (⇑f) x
⊢ b' ∈ approx (⇑f) i x