case pos
α : Type u_2
β : α → Type u_1
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_2
β : α → Type u_1
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
α : Type u_2
β : α → Type u_1
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
⊢ b ∈ Part.fix (↑f) a ↔ ∃ i, b ∈ approx (↑f) i a
by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
case pos
α : Type u_2
β : α → Type u_1
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a ↔ ∃ i, b ∈ approx (↑f) i a
case pos
α : Type u_2
β : α → Type u_1
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
simp only [Part.fix_def f h₀]
case pos.mp
α : Type u_2
β : α → Type u_1
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
hh : b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
⊢ ∃ i, b ∈ approx (↑f) i a

case pos.mpr
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
case pos
α : Type u_2
β : α → Type u_1
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a ↔ ∃ i, b ∈ approx (↑f) i a
constructor <;> intro hh
case pos.mpr
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
case pos.mpr
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
have h₁ := Nat.find_spec h₀
case pos.mpr
α : Type u_2
β : α → Type u_1
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₁ : ∃ y, y ∈ approx (↑f) (Nat.find h₀) a
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
case pos.mpr
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
rw [dom_iff_mem] at h₁
case pos.mpr.intro
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
case pos.mpr
α : Type u_2
β : α → Type u_1
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₁ : ∃ y, y ∈ approx (↑f) (Nat.find h₀) a
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
cases' h₁ with y h₁
case pos.mpr.intro
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
case pos.mpr.intro
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
replace h₁ := approx_mono' f _ _ h₁
case pos.mpr.intro
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
this : y = b
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a

case this
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
⊢ y = b
case pos.mpr.intro
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
suffices : y = b
case this.intro
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
i : ℕ
hh : b ∈ approx (↑f) i a
⊢ y = b
case this
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
⊢ y = b
cases' hh with i hh
case this.intro
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a → y = b
case this.intro
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
i : ℕ
hh : b ∈ approx (↑f) i a
⊢ y = b
revert h₁
case this.intro
α : Type u_2
β : α → Type u_1
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
case this.intro
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a → y = b
generalize succ (Nat.find h₀) = j
case this.intro
α : Type u_2
β : α → Type u_1
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
case this.intro
α : Type u_2
β : α → Type u_1
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
intro h₁
case this.intro.inr
α : Type u_2
β : α → Type u_1
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
this :
  ∀ {α : Type u_2} {β : α → Type u_1} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
⊢ y = b

α✝ : Type u_2
β✝ : α✝ → Type u_1
f✝ : ((a : α✝) → Part (β✝ a)) →o (a : α✝) → Part (β✝ a)
α : Type u_2
β : α → Type u_1
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
case : i ≤ j
⊢ y = b
case this.intro
α : Type u_2
β : α → Type u_1
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
wlog case : i ≤ j
α✝ : Type u_2
β✝ : α✝ → Type u_1
f✝ : ((a : α✝) → Part (β✝ a)) →o (a : α✝) → Part (β✝ a)
α : Type u_2
β : α → Type u_1
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
α✝ : Type u_2
β✝ : α✝ → Type u_1
f✝ : ((a : α✝) → Part (β✝ a)) →o (a : α✝) → Part (β✝ a)
α : Type u_2
β : α → Type u_1
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
case : i ≤ j
⊢ y = b
replace hh := approx_mono f case _ _ hh
no goals
α✝ : Type u_2
β✝ : α✝ → Type u_1
f✝ : ((a : α✝) → Part (β✝ a)) →o (a : α✝) → Part (β✝ a)
α : Type u_2
β : α → Type u_1
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
apply Part.mem_unique h₁ hh
no goals
case pos.mp
α : Type u_2
β : α → Type u_1
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (↑f) i a).Dom
hh : b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
⊢ ∃ i, b ∈ approx (↑f) i a
exact ⟨_, hh⟩
case pos.mpr.intro
α : Type u_2
β : α → Type u_1
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
h₁ : y ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
hh : ∃ i, y ∈ approx (↑f) i a
⊢ y ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
case pos.mpr.intro
α : Type u_2
β : α → Type u_1
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.succ (Nat.find h₀)) a
this : y = b
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
subst this
no goals
case pos.mpr.intro
α : Type u_2
β : α → Type u_1
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
h₀ : ∃ i, (approx (↑f) i a).Dom
y : β a
h₁ : y ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
hh : ∃ i, y ∈ approx (↑f) i a
⊢ y ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
exact h₁
no goals
case this.intro.inr
α : Type u_2
β : α → Type u_1
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
this :
  ∀ {α : Type u_2} {β : α → Type u_1} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (↑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (↑f) i a → ∀ (j : ℕ), y ∈ approx (↑f) j a → i ≤ j → y = b
case : ¬i ≤ j
⊢ y = b
cases' le_total i j with H H <;> [skip; symm] <;> apply_assumption <;> assumption
case neg
α : Type u_2
β : α → Type u_1
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (↑f) i a).Dom
⊢ ∀ (x : ℕ), ¬b ∈ approx (↑f) x a
case neg
α : Type u_2
β : α → Type u_1
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
simp only [fix_def' (⇑f) h₀, not_exists, false_iff_iff, not_mem_none]
case neg
α : Type u_2
β : α → Type u_1
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
case neg
α : Type u_2
β : α → Type u_1
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (↑f) i a).Dom
⊢ ∀ (x : ℕ), ¬b ∈ approx (↑f) x a
simp only [dom_iff_mem, not_exists] at h₀
case neg
α : Type u_2
β : α → Type u_1
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
case neg
α : Type u_2
β : α → Type u_1
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
intro
no goals
case neg
α : Type u_2
β : α → Type u_1
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
apply h₀