Theorem: int_wf_of_lower_bound (RealsQuasiMorphisms/Field.lean)

State before:
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
⊢ (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
Tactic:
ext x y
State after:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ Measure (fun x => Int.natAbs (↑x - a)) x y

State before:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ Measure (fun x => Int.natAbs (↑x - a)) x y
Tactic:
unfold Measure InvImage
State after:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ (fun a b => a < b) ((fun x => Int.natAbs (↑x - a)) x) ((fun x => Int.natAbs (↑x - a)) y)

State before:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ (fun a b => a < b) ((fun x => Int.natAbs (↑x - a)) x) ((fun x => Int.natAbs (↑x - a)) y)
Tactic:
dsimp
State after:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ Int.natAbs (↑x - a) < Int.natAbs (↑y - a)

State before:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ Int.natAbs (↑x - a) < Int.natAbs (↑y - a)
Tactic:
rewrite [←Int.ofNat_lt, this, this]
State after:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ ↑x - a < ↑y - a

State before:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ ↑x - a < ↑y - a
Tactic:
apply Iff.intro
State after:
case h.h.a.mp
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y → ↑x - a < ↑y - a

case h.h.a.mpr
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x - a < ↑y - a → ↑x < ↑y

State before:
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this✝ : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
this : (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
⊢ Set.IsWf s
Tactic:
unfold Set.IsWf Set.WellFoundedOn
State after:
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this✝ : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
this : (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
⊢ WellFounded fun a b => (fun x x_1 => x < x_1) ↑a ↑b

State before:
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this✝ : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
this : (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
⊢ WellFounded fun a b => (fun x x_1 => x < x_1) ↑a ↑b
Tactic:
rewrite [this]
State after:
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this✝ : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
this : (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
⊢ WellFounded (Measure fun x => Int.natAbs (↑x - a))

State before:
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this✝ : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
this : (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
⊢ WellFounded (Measure fun x => Int.natAbs (↑x - a))
Tactic:
apply IsWellFounded.wf
State after:
no goals