p : ℕ → Prop
x : ℕ
h : p x
⊢ Upto.GT p = Measure fun y => x - ↑y
p : ℕ → Prop
x : ℕ
h : p x
⊢ WellFounded (Upto.GT p)
suffices Upto.GT p = Measure fun y : Nat.Upto p => x - y.val by
  rw [this]
  exact (measure _).wf
case h.mk.h.mk.a
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property✝ : ∀ (j : ℕ), j < b → ¬p j
⊢ Upto.GT p { val := a, property := ha } { val := b, property := property✝ } ↔
    Measure (fun y => x - ↑y) { val := a, property := ha } { val := b, property := property✝ }
p : ℕ → Prop
x : ℕ
h : p x
⊢ Upto.GT p = Measure fun y => x - ↑y
ext (⟨a, ha⟩⟨b, _⟩)
case h.mk.h.mk.a
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property✝ : ∀ (j : ℕ), j < b → ¬p j
⊢ a > b ↔ x - a < x - b
case h.mk.h.mk.a
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property✝ : ∀ (j : ℕ), j < b → ¬p j
⊢ Upto.GT p { val := a, property := ha } { val := b, property := property✝ } ↔
    Measure (fun y => x - ↑y) { val := a, property := ha } { val := b, property := property✝ }
dsimp [Measure, InvImage, Upto.GT]
no goals
case h.mk.h.mk.a
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property✝ : ∀ (j : ℕ), j < b → ¬p j
⊢ a > b ↔ x - a < x - b
rw [tsub_lt_tsub_iff_left_of_le (le_of_not_lt fun h' => ha _ h' h)]
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = Measure fun y => x - ↑y
⊢ WellFounded (Measure fun y => x - ↑y)
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = Measure fun y => x - ↑y
⊢ WellFounded (Upto.GT p)
rw [this]
no goals
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = Measure fun y => x - ↑y
⊢ WellFounded (Measure fun y => x - ↑y)
exact (measure _).wf