Theorem: trunc_le_trunc (Fl/Trunc.lean)

State before:
n x y : ℕ
npos : 0 < n
h : x ≤ y
⊢ trunc n x ≤ trunc n y
Tactic:
cases Nat.lt_or_ge (Nat.size x) (Nat.size y) with
| inl size_lt_size =>
  rewrite [← size_trunc_eq_size npos x] at size_lt_size
  rewrite [← size_trunc_eq_size npos y] at size_lt_size
  exact le_of_lt (lt_of_size_lt_size size_lt_size)
| inr size_ge_size =>
  have ulp_eq_ulp : ulp n x = ulp n y := by
    apply congr_arg (fun w => 2 ^ (w - n))
    exact Nat.le_antisymm (Nat.size_le_size h) size_ge_size
  unfold trunc
  rewrite [ulp_eq_ulp]
  exact Nat.mul_le_mul_right _ (Nat.div_le_div_right h)
State after:
no goals

State before:
case inl
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_lt_size : Nat.size x < Nat.size y
⊢ trunc n x ≤ trunc n y
Tactic:
rewrite [← size_trunc_eq_size npos x] at size_lt_size
State after:
case inl
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_lt_size : Nat.size (trunc n x) < Nat.size y
⊢ trunc n x ≤ trunc n y

State before:
case inl
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_lt_size : Nat.size (trunc n x) < Nat.size y
⊢ trunc n x ≤ trunc n y
Tactic:
rewrite [← size_trunc_eq_size npos y] at size_lt_size
State after:
case inl
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_lt_size : Nat.size (trunc n x) < Nat.size (trunc n y)
⊢ trunc n x ≤ trunc n y

State before:
case inl
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_lt_size : Nat.size (trunc n x) < Nat.size (trunc n y)
⊢ trunc n x ≤ trunc n y
Tactic:
exact le_of_lt (lt_of_size_lt_size size_lt_size)
State after:
no goals

State before:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
⊢ trunc n x ≤ trunc n y
Tactic:
have ulp_eq_ulp : ulp n x = ulp n y := by
  apply congr_arg (fun w => 2 ^ (w - n))
  exact Nat.le_antisymm (Nat.size_le_size h) size_ge_size
State after:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ trunc n x ≤ trunc n y

State before:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ trunc n x ≤ trunc n y
Tactic:
unfold trunc
State after:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x ≤ y / ulp n y * ulp n y

State before:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x ≤ y / ulp n y * ulp n y
Tactic:
rewrite [ulp_eq_ulp]
State after:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ x / ulp n y * ulp n y ≤ y / ulp n y * ulp n y

State before:
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ x / ulp n y * ulp n y ≤ y / ulp n y * ulp n y
Tactic:
exact Nat.mul_le_mul_right _ (Nat.div_le_div_right h)
State after:
no goals

State before:
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
⊢ ulp n x = ulp n y
Tactic:
apply congr_arg (fun w => 2 ^ (w - n))
State after:
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
⊢ Nat.size x = Nat.size y

State before:
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
⊢ Nat.size x = Nat.size y
Tactic:
exact Nat.le_antisymm (Nat.size_le_size h) size_ge_size
State after:
no goals