[GOAL]
p : ℕ → Prop
x : ℕ
h : p x
⊢ WellFounded (Upto.GT p)
[PROOFSTEP]
suffices Upto.GT p = InvImage (· < ·) fun y : Nat.Upto p => x - y.val
  by
  rw [this]
  exact (measure _).wf
[GOAL]
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun x x_1 => x < x_1) fun y => x - ↑y
⊢ WellFounded (Upto.GT p)
[PROOFSTEP]
rw [this]
[GOAL]
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun x x_1 => x < x_1) fun y => x - ↑y
⊢ WellFounded (InvImage (fun x x_1 => x < x_1) fun y => x - ↑y)
[PROOFSTEP]
exact (measure _).wf
[GOAL]
p : ℕ → Prop
x : ℕ
h : p x
⊢ Upto.GT p = InvImage (fun x x_1 => x < x_1) fun y => x - ↑y
[PROOFSTEP]
ext ⟨a, ha⟩ ⟨b, _⟩
[GOAL]
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✝ } ↔
    InvImage (fun x x_1 => x < x_1) (fun y => x - ↑y) { val := a, property := ha } { val := b, property := property✝ }
[PROOFSTEP]
dsimp [InvImage, Upto.GT]
[GOAL]
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
[PROOFSTEP]
rw [tsub_lt_tsub_iff_left_of_le (le_of_not_lt fun h' => ha _ h' h)]
[GOAL]
p : ℕ → Prop
x : Upto p
h : ¬p ↑x
j : ℕ
h' : j < Nat.succ ↑x
⊢ ¬p j
[PROOFSTEP]
rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl) <;> [exact x.2 _ h'; exact h]
[GOAL]
p : ℕ → Prop
x : Upto p
h : ¬p ↑x
j : ℕ
h' : j < Nat.succ ↑x
⊢ ¬p j
[PROOFSTEP]
rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl)
[GOAL]
case inl
p : ℕ → Prop
x : Upto p
h : ¬p ↑x
j : ℕ
h'✝ : j < Nat.succ ↑x
h' : j < ↑x
⊢ ¬p j
[PROOFSTEP]
exact x.2 _ h'
[GOAL]
case inr
p : ℕ → Prop
x : Upto p
h : ¬p ↑x
h' : ↑x < Nat.succ ↑x
⊢ ¬p ↑x
[PROOFSTEP]
exact h
