[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ i)
[PROOFSTEP]
induction i with
| zero => dsimp [approx]; apply @bot_le _ _ _ (f ⊥)
| succ _ i_ih => intro; apply f.monotone; apply i_ih
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ i)
[PROOFSTEP]
induction i with
| zero => dsimp [approx]; apply @bot_le _ _ _ (f ⊥)
| succ _ i_ih => intro; apply f.monotone; apply i_ih
[GOAL]
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ approx (↑f) Nat.zero ≤ approx (↑f) (Nat.succ Nat.zero)
[PROOFSTEP]

| zero => dsimp [approx]; apply @bot_le _ _ _ (f ⊥)
[GOAL]
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ approx (↑f) Nat.zero ≤ approx (↑f) (Nat.succ Nat.zero)
[PROOFSTEP]
dsimp [approx]
[GOAL]
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ⊥ ≤ ↑f ⊥
[PROOFSTEP]
apply @bot_le _ _ _ (f ⊥)
[GOAL]
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
⊢ approx (↑f) (Nat.succ n✝) ≤ approx (↑f) (Nat.succ (Nat.succ n✝))
[PROOFSTEP]

| succ _ i_ih => intro; apply f.monotone; apply i_ih
[GOAL]
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
⊢ approx (↑f) (Nat.succ n✝) ≤ approx (↑f) (Nat.succ (Nat.succ n✝))
[PROOFSTEP]
intro
[GOAL]
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
i✝ : α
⊢ approx (↑f) (Nat.succ n✝) i✝ ≤ approx (↑f) (Nat.succ (Nat.succ n✝)) i✝
[PROOFSTEP]
apply f.monotone
[GOAL]
case succ.a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
i✝ : α
⊢ approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
[PROOFSTEP]
apply i_ih
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij : i ≤ j
⊢ approx (↑f) i ≤ approx (↑f) j
[PROOFSTEP]
induction' j with j ih
[GOAL]
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij✝ : i ≤ j
hij : i ≤ Nat.zero
⊢ approx (↑f) i ≤ approx (↑f) Nat.zero
[PROOFSTEP]
cases hij
[GOAL]
case zero.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
hij : Nat.zero ≤ j
⊢ approx (↑f) Nat.zero ≤ approx (↑f) Nat.zero
[PROOFSTEP]
exact le_rfl
[GOAL]
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j✝ : ℕ
hij✝ : i ≤ j✝
j : ℕ
ih : i ≤ j → approx (↑f) i ≤ approx (↑f) j
hij : i ≤ Nat.succ j
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ j)
[PROOFSTEP]
cases hij
[GOAL]
case succ.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j✝ j : ℕ
hij : Nat.succ j ≤ j✝
ih : Nat.succ j ≤ j → approx (↑f) (Nat.succ j) ≤ approx (↑f) j
⊢ approx (↑f) (Nat.succ j) ≤ approx (↑f) (Nat.succ j)
[PROOFSTEP]
exact le_rfl
[GOAL]
case succ.step
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j✝ : ℕ
hij : i ≤ j✝
j : ℕ
ih : i ≤ j → approx (↑f) i ≤ approx (↑f) j
a✝ : Nat.le i j
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ j)
[PROOFSTEP]
exact le_trans (ih ‹_›) (approx_mono' f)
[GOAL]
α : 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
[PROOFSTEP]
by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
[GOAL]
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
[PROOFSTEP]
simp only [Part.fix_def f h₀]
[GOAL]
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.succ (Nat.find h₀)) a ↔ ∃ i, b ∈ approx (↑f) i a
[PROOFSTEP]
constructor
[GOAL]
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
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a → ∃ i, b ∈ approx (↑f) i a
[PROOFSTEP]
intro hh
[GOAL]
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
⊢ (∃ i, b ∈ approx (↑f) i a) → b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
intro hh
[GOAL]
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.succ (Nat.find h₀)) a
⊢ ∃ i, b ∈ approx (↑f) i a
[PROOFSTEP]
exact ⟨_, hh⟩
[GOAL]
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.succ (Nat.find h₀)) a
[PROOFSTEP]
have h₁ := Nat.find_spec h₀
[GOAL]
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.succ (Nat.find h₀)) a
[PROOFSTEP]
rw [dom_iff_mem] at h₁ 
[GOAL]
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₁ : ∃ y, y ∈ approx (↑f) (Nat.find h₀) a
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
cases' h₁ with y h₁
[GOAL]
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.succ (Nat.find h₀)) a
[PROOFSTEP]
replace h₁ := approx_mono' f _ _ h₁
[GOAL]
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.succ (Nat.find h₀)) a
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
suffices : y = b
[GOAL]
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.succ (Nat.find h₀)) a
this : y = b
⊢ b ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
subst this
[GOAL]
case pos.mpr.intro
α : 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.succ (Nat.find h₀)) a
hh : ∃ i, y ∈ approx (↑f) i a
⊢ y ∈ approx (↑f) (Nat.succ (Nat.find h₀)) a
[PROOFSTEP]
exact h₁
[GOAL]
case this
α : 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.succ (Nat.find h₀)) a
⊢ y = b
[PROOFSTEP]
cases' hh with i hh
[GOAL]
case this.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.succ (Nat.find h₀)) a
i : ℕ
hh : b ∈ approx (↑f) i a
⊢ y = b
[PROOFSTEP]
revert h₁
[GOAL]
case this.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.succ (Nat.find h₀)) a → y = b
[PROOFSTEP]
generalize succ (Nat.find h₀) = j
[GOAL]
case this.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
[PROOFSTEP]
intro h₁
[GOAL]
case this.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
[PROOFSTEP]
wlog case : i ≤ j
[GOAL]
case this.intro.inr
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
[PROOFSTEP]
cases' le_total i j with H H <;> [skip; symm]
[GOAL]
case this.intro.inr
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
[PROOFSTEP]
cases' le_total i j with H H
[GOAL]
case this.intro.inr.inl
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
H : i ≤ j
⊢ y = b
[PROOFSTEP]
skip
[GOAL]
case this.intro.inr.inr
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
H : j ≤ i
⊢ y = b
[PROOFSTEP]
symm
[GOAL]
case this.intro.inr.inl
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
H : i ≤ j
⊢ y = b
[PROOFSTEP]
apply_assumption
[GOAL]
case this.intro.inr.inr
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
H : j ≤ i
⊢ b = y
[PROOFSTEP]
apply_assumption
[GOAL]
case this.intro.inr.inl.h₀
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
H : i ≤ j
⊢ ∃ i, (approx (↑?this.intro.inr.inl.f) i a).Dom
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inl.hh
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
H : i ≤ j
⊢ b ∈ approx ↑f ?this.intro.inr.inl.i a
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inl.h₁
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
H : i ≤ j
⊢ y ∈ approx ↑f ?this.intro.inr.inl.j a
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inl.case
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
H : i ≤ j
⊢ i ≤ j
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inr.h₀
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
H : j ≤ i
⊢ ∃ i, (approx (↑?this.intro.inr.inr.f) i a).Dom
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inr.hh
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
H : j ≤ i
⊢ y ∈ approx ↑f ?this.intro.inr.inr.i a
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inr.h₁
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
H : j ≤ i
⊢ b ∈ approx ↑f ?this.intro.inr.inr.j a
[PROOFSTEP]
assumption
[GOAL]
case this.intro.inr.inr.case
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (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
H : j ≤ i
⊢ j ≤ i
[PROOFSTEP]
assumption
[GOAL]
α✝ : 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 : ℕ
hh : b ∈ approx (↑f) i a
j : ℕ
h₁ : y ∈ approx (↑f) j a
case : i ≤ j
⊢ y = b
[PROOFSTEP]
replace hh := approx_mono f case _ _ hh
[GOAL]
α✝ : 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
[PROOFSTEP]
apply Part.mem_unique h₁ hh
[GOAL]
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
[PROOFSTEP]
simp only [fix_def' (⇑f) h₀, not_exists, false_iff_iff, not_mem_none]
[GOAL]
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
[PROOFSTEP]
simp only [dom_iff_mem, not_exists] at h₀ 
[GOAL]
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
[PROOFSTEP]
intro
[GOAL]
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
[PROOFSTEP]
apply h₀
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (↑f) i a
⊢ b ∈ Part.fix (↑f) a
[PROOFSTEP]
rw [mem_iff f]
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (↑f) i a
⊢ ∃ i, b ∈ approx (↑f) i a
[PROOFSTEP]
exact ⟨_, hh⟩
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
⊢ ∃ i, Part.fix (↑f) x ≤ approx (↑f) i x
[PROOFSTEP]
by_cases hh : ∃ i b, b ∈ approx f i x
[GOAL]
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
[PROOFSTEP]
rcases hh with ⟨i, b, hb⟩
[GOAL]
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
[PROOFSTEP]
exists i
[GOAL]
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
[PROOFSTEP]
intro b' h'
[GOAL]
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
[PROOFSTEP]
have hb' := approx_le_fix f i _ _ hb
[GOAL]
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
[PROOFSTEP]
obtain rfl := Part.mem_unique h' hb'
[GOAL]
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
[PROOFSTEP]
exact hb
[GOAL]
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
[PROOFSTEP]
simp only [not_exists] at hh 
[GOAL]
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
[PROOFSTEP]
exists 0
[GOAL]
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
[PROOFSTEP]
intro b' h'
[GOAL]
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
[PROOFSTEP]
simp only [mem_iff f] at h' 
[GOAL]
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
[PROOFSTEP]
cases' h' with i h'
[GOAL]
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
[PROOFSTEP]
cases hh _ _ h'
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : (a : α) → Part (β a)
⊢ x ∈ approxChain f → x ≤ ↑f x
[PROOFSTEP]
simp only [(· ∈ ·), forall_exists_index]
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : (a : α) → Part (β a)
⊢ ∀ (x_1 : ℕ), x = ↑(approxChain f) x_1 → x ≤ ↑f x
[PROOFSTEP]
rintro i rfl
[GOAL]
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ ↑(approxChain f) i ≤ ↑f (↑(approxChain f) i)
[PROOFSTEP]
apply approx_mono'
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ Part.fix ↑f = ωSup (approxChain f)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ Part.fix ↑f ≤ ωSup (approxChain f)
[PROOFSTEP]
intro x
[GOAL]
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
⊢ Part.fix (↑f) x ≤ ωSup (approxChain f) x
[PROOFSTEP]
cases' exists_fix_le_approx f x with i hx
[GOAL]
case a.intro
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ ωSup (approxChain f) x
[PROOFSTEP]
trans approx f i.succ x
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ approx (↑f) (Nat.succ i) x
[PROOFSTEP]
trans
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ ?m.11190
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ ?m.11190 ≤ approx (↑f) (Nat.succ i) x
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part (β x)
[PROOFSTEP]
apply hx
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ approx (↑f) i x ≤ approx (↑f) (Nat.succ i) x
[PROOFSTEP]
apply approx_mono' f
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ approx (↑f) (Nat.succ i) x ≤ ωSup (approxChain f) x
[PROOFSTEP]
apply le_ωSup_of_le i.succ
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ approx (↑f) (Nat.succ i) x ≤ ↑(Chain.map (approxChain f) (Pi.evalOrderHom x)) (Nat.succ i)
[PROOFSTEP]
dsimp [approx]
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ ↑f (approx (↑f) i) x ≤ ↑(approxChain f) (Nat.succ i) x
[PROOFSTEP]
rfl
[GOAL]
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ↑f
[PROOFSTEP]
apply ωSup_le _ _ _
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ ∀ (i : ℕ), ↑(approxChain f) i ≤ Part.fix ↑f
[PROOFSTEP]
simp only [Fix.approxChain, OrderHom.coe_mk]
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ ∀ (i : ℕ),
    ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } i ≤ Part.fix ↑f
[PROOFSTEP]
intro y x
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
y : ℕ
x : α✝
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } y x ≤ Part.fix (↑f) x
[PROOFSTEP]
apply approx_le_fix f
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ Part.fix ↑f ≤ X
[PROOFSTEP]
rw [fix_eq_ωSup f]
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ωSup (approxChain f) ≤ X
[PROOFSTEP]
apply ωSup_le _ _ _
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ∀ (i : ℕ), ↑(approxChain f) i ≤ X
[PROOFSTEP]
simp only [Fix.approxChain, OrderHom.coe_mk]
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ∀ (i : ℕ), ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } i ≤ X
[PROOFSTEP]
intro i
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
i : ℕ
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } i ≤ X
[PROOFSTEP]
induction i with
| zero => dsimp [Fix.approx]; apply bot_le
| succ _ i_ih => trans f X; apply f.monotone i_ih; apply hX
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
i : ℕ
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } i ≤ X
[PROOFSTEP]
induction i with
| zero => dsimp [Fix.approx]; apply bot_le
| succ _ i_ih => trans f X; apply f.monotone i_ih; apply hX
[GOAL]
case zero
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } Nat.zero ≤ X
[PROOFSTEP]

| zero => dsimp [Fix.approx]; apply bot_le
[GOAL]
case zero
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } Nat.zero ≤ X
[PROOFSTEP]
dsimp [Fix.approx]
[GOAL]
case zero
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } 0 ≤ X
[PROOFSTEP]
apply bot_le
[GOAL]
case succ
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } n✝ ≤ X
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } (Nat.succ n✝) ≤ X
[PROOFSTEP]

| succ _ i_ih => trans f X; apply f.monotone i_ih; apply hX
[GOAL]
case succ
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } n✝ ≤ X
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } (Nat.succ n✝) ≤ X
[PROOFSTEP]
trans f X
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } n✝ ≤ X
⊢ ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } (Nat.succ n✝) ≤ ↑f X
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } n✝ ≤ X
⊢ ↑f X ≤ X
[PROOFSTEP]
apply f.monotone i_ih
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : ↑{ toFun := approx ↑f, monotone' := (_ : ∀ ⦃i j : ℕ⦄, i ≤ j → approx (↑f) i ≤ approx (↑f) j) } n✝ ≤ X
⊢ ↑f X ≤ X
[PROOFSTEP]
apply hX
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ Part.fix ↑f = ↑f (Part.fix ↑f)
[PROOFSTEP]
rw [fix_eq_ωSup f, hc]
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ ωSup (approxChain f) = ωSup (Chain.map (approxChain f) f)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ ωSup (approxChain f) ≤ ωSup (Chain.map (approxChain f) f)
[PROOFSTEP]
apply ωSup_le_ωSup_of_le _
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ approxChain f ≤ Chain.map (approxChain f) f
[PROOFSTEP]
intro i
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
⊢ ∃ j, ↑(approxChain f) i ≤ ↑(Chain.map (approxChain f) f) j
[PROOFSTEP]
exists i
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
⊢ ↑(approxChain f) i ≤ ↑(Chain.map (approxChain f) f) i
[PROOFSTEP]
intro x
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
x : α✝
⊢ ↑(approxChain f) i x ≤ ↑(Chain.map (approxChain f) f) i x
[PROOFSTEP]
apply le_f_of_mem_approx _ ⟨i, rfl⟩
[GOAL]
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ ωSup (Chain.map (approxChain f) f) ≤ ωSup (approxChain f)
[PROOFSTEP]
apply ωSup_le_ωSup_of_le _
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
⊢ Chain.map (approxChain f) f ≤ approxChain f
[PROOFSTEP]
intro i
[GOAL]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type u_3
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
hc : Continuous f
i : ℕ
⊢ ∃ j, ↑(Chain.map (approxChain f) f) i ≤ ↑(approxChain f) j
[PROOFSTEP]
exists i.succ
[GOAL]
α : Type u_1
β : α → Type u_2
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ↑(toUnitMono f) (ωSup x✝) = ωSup (Chain.map x✝ (toUnitMono f))
[PROOFSTEP]
ext ⟨⟩ : 1
[GOAL]
case h.unit
α : Type u_1
β : α → Type u_2
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ↑(toUnitMono f) (ωSup x✝) PUnit.unit = ωSup (Chain.map x✝ (toUnitMono f)) PUnit.unit
[PROOFSTEP]
dsimp [OmegaCompletePartialOrder.ωSup]
[GOAL]
case h.unit
α : Type u_1
β : α → Type u_2
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ↑f (Part.ωSup (Chain.map x✝ (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup (Chain.map (Chain.map x✝ (toUnitMono f)) (Pi.evalOrderHom PUnit.unit))
[PROOFSTEP]
erw [hc, Chain.map_comp]
[GOAL]
case h.unit
α : Type u_1
β : α → Type u_2
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ωSup (Chain.map x✝ (OrderHom.comp f (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup (Chain.map x✝ (OrderHom.comp f (Pi.evalOrderHom PUnit.unit)))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : α → Type u_2
f : Part α →o Part α
hc : Continuous f
⊢ Part.fix ↑(toUnitMono f) () = ↑f (Fix.fix ↑f)
[PROOFSTEP]
rw [Part.fix_eq (to_unit_cont f hc)]
[GOAL]
α : Type u_1
β : α → Type u_2
f : Part α →o Part α
hc : Continuous f
⊢ ↑(toUnitMono f) (Part.fix ↑(toUnitMono f)) () = ↑f (Fix.fix ↑f)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
⊢ ↑(monotoneCurry α β γ) (ωSup c) = ωSup (Chain.map c (monotoneCurry α β γ))
[PROOFSTEP]
ext x y
[GOAL]
case h.h
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ ↑(monotoneCurry α β γ) (ωSup c) x y = ωSup (Chain.map c (monotoneCurry α β γ)) x y
[PROOFSTEP]
dsimp [curry, ωSup]
[GOAL]
case h.h
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ ωSup (Chain.map c (evalOrderHom { fst := x, snd := y })) =
    ωSup (Chain.map (Chain.map (Chain.map c (monotoneCurry α β γ)) (evalOrderHom x)) (evalOrderHom y))
[PROOFSTEP]
rw [map_comp, map_comp]
[GOAL]
case h.h
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ ωSup (Chain.map c (evalOrderHom { fst := x, snd := y })) =
    ωSup (Chain.map c (OrderHom.comp (OrderHom.comp (evalOrderHom y) (evalOrderHom x)) (monotoneCurry α β γ)))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
⊢ ↑(monotoneUncurry α β γ) (ωSup c) = ωSup (Chain.map c (monotoneUncurry α β γ))
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ↑(monotoneUncurry α β γ) (ωSup c) { fst := x, snd := y } =
    ωSup (Chain.map c (monotoneUncurry α β γ)) { fst := x, snd := y }
[PROOFSTEP]
dsimp [uncurry, ωSup]
[GOAL]
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (Chain.map (Chain.map c (evalOrderHom x)) (evalOrderHom y)) =
    ωSup (Chain.map (Chain.map c (monotoneUncurry α β γ)) (evalOrderHom { fst := x, snd := y }))
[PROOFSTEP]
rw [map_comp, map_comp]
[GOAL]
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (Chain.map c (OrderHom.comp (evalOrderHom y) (evalOrderHom x))) =
    ωSup (Chain.map c (OrderHom.comp (evalOrderHom { fst := x, snd := y }) (monotoneUncurry α β γ)))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y
hc : Continuous _f
⊢ fix ↑_f = ↑_f (fix ↑_f)
[PROOFSTEP]
dsimp [fix]
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y
hc : Continuous _f
⊢ curry (fix (uncurry ∘ ↑_f ∘ curry)) = ↑_f (curry (fix (uncurry ∘ ↑_f ∘ curry)))
[PROOFSTEP]
conv =>
  lhs
  erw [LawfulFix.fix_eq (uncurry_curry_continuous hc)]
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y
hc : Continuous _f
| curry (fix (uncurry ∘ ↑_f ∘ curry)) = ↑_f (curry (fix (uncurry ∘ ↑_f ∘ curry)))
[PROOFSTEP]
  lhs
  erw [LawfulFix.fix_eq (uncurry_curry_continuous hc)]
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y
hc : Continuous _f
| curry (fix (uncurry ∘ ↑_f ∘ curry)) = ↑_f (curry (fix (uncurry ∘ ↑_f ∘ curry)))
[PROOFSTEP]
  lhs
  erw [LawfulFix.fix_eq (uncurry_curry_continuous hc)]
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y
hc : Continuous _f
| curry (fix (uncurry ∘ ↑_f ∘ curry)) = ↑_f (curry (fix (uncurry ∘ ↑_f ∘ curry)))
[PROOFSTEP]
lhs
[GOAL]
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y
hc : Continuous _f
| curry (fix (uncurry ∘ ↑_f ∘ curry))
[PROOFSTEP]
erw [LawfulFix.fix_eq (uncurry_curry_continuous hc)]
