-- Mathlib/Control/LawfulFix.lean
theorem mem_iff (a : α) (b : β a) : b ∈ Part.fix f a ↔ ∃ i, b ∈ approx f i a

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
h₁ : y ∈ approx (⇑f) (Nat.find h₀).succ a
hh : ∃ i, y ∈ approx (⇑f) i a
⊢ y ∈ approx (⇑f) (Nat.find h₀).succ a

Tactic:
exact h₁

Result:
no goals

Proof state:
case pos.mpr.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
y : β a
h₁ : y ∈ approx (⇑f) (Nat.find h₀) a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a

Tactic:
replace h₁ := approx_mono' f _ _ h₁

Result:
case pos.mpr.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
y : β a
h₁ : y ∈ approx (⇑f) (Nat.find h₀).succ a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a

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

Tactic:
simp only [fix_def' (⇑f) h₀, not_exists, false_iff, not_mem_none]

Result:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (⇑f) i a).Dom
⊢ ∀ (x : ℕ), b ∉ approx (⇑f) x a

Proof state:
case pos.mpr.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
⊢ y ∈ approx (⇑f) (Nat.find h₀).succ a → y = b

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

Result:
case pos.mpr.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
⊢ y ∈ approx (⇑f) j a → y = b

Proof state:
case pos.mpr.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
h₁ : y ∈ approx (⇑f) (Nat.find h₀).succ a
i : ℕ
hh : b ∈ approx (⇑f) i a
⊢ y = b

Tactic:
revert h₁

Result:
case pos.mpr.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
⊢ y ∈ approx (⇑f) (Nat.find h₀).succ a → y = b

Proof state:
case pos.mpr.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
y : β a
h₁ : y ∈ approx (⇑f) (Nat.find h₀).succ a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a

Tactic:
suffices y = b by
  subst this
  exact h₁

Result:
case pos.mpr.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
y : β a
h₁ : y ∈ approx (⇑f) (Nat.find h₀).succ a
⊢ y = b

Proof state:
α✝ : Type u_1
β✝ : α✝ → Type u_2
f✝ : ((a : α✝) → Part (β✝ a)) →o (a : α✝) → Part (β✝ a)
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i j : ℕ
h₁ : y ∈ approx (⇑f) j a
case : i ≤ j
hh : b ∈ approx (⇑f) j a
⊢ y = b

Tactic:
apply Part.mem_unique h₁ hh

Result:
no goals

Proof state:
case pos.mpr.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
y : β a
h₁ : y ∈ approx (⇑f) (Nat.find h₀).succ a
⊢ y = b

Tactic:
obtain ⟨i, hh⟩ := hh

Result:
case pos.mpr.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
h₁ : y ∈ approx (⇑f) (Nat.find h₀).succ a
i : ℕ
hh : b ∈ approx (⇑f) i a
⊢ y = b

Proof state:
case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a

Tactic:
have h₁ := Nat.find_spec h₀

Result:
case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
h₁ : (approx (⇑f) (Nat.find h₀) a).Dom
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a

Proof state:
case neg
α : 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) x a
x✝ : ℕ
⊢ b ∉ approx (⇑f) x✝ a

Tactic:
apply h₀

Result:
no goals

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

Tactic:
by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom

Result:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

Proof state:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (⇑f) i a).Dom
⊢ ∀ (x : ℕ), b ∉ approx (⇑f) x a

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

Result:
case neg
α : 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) x a
⊢ ∀ (x : ℕ), b ∉ approx (⇑f) x a

Proof state:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
simp only [Part.fix_def f h₀]

Result:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a ↔ ∃ i, b ∈ approx (⇑f) i a

Proof state:
case neg
α : 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) x a
⊢ ∀ (x : ℕ), b ∉ approx (⇑f) x a

Tactic:
intro

Result:
case neg
α : 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) x a
x✝ : ℕ
⊢ b ∉ approx (⇑f) x✝ a

Proof state:
case pos.mpr.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
⊢ y ∈ approx (⇑f) j a → y = b

Tactic:
intro h₁

Result:
case pos.mpr.intro.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
⊢ y = b

Proof state:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
constructor <;> intro hh

Result:
case pos.mp
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : b ∈ approx (⇑f) (Nat.find h₀).succ a
⊢ ∃ i, b ∈ approx (⇑f) i a

case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a