Theorem: trunc_eq_trunc_of_le_of_lt (Fl/Trunc.lean)

State before:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ trunc n x = trunc n y
Tactic:
have ulp_eq : ulp n x = ulp n y := by
  rewrite [← ulp_trunc npos]
  apply le_antisymm
  . apply ulp_le_ulp
    exact h
  . rewrite [ulp_trunc npos]
    unfold ulp expt
    apply Nat.pow_le_pow_of_le_right two_pos
    apply tsub_le_tsub_right
    rewrite [Nat.size_le]
    apply Nat.lt_of_lt_of_le k
    exact next_trunc_le npos x
State after:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ trunc n x = trunc n y

State before:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ trunc n x = trunc n y
Tactic:
unfold trunc
State after:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x = y / ulp n y * ulp n y

State before:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x = y / ulp n y * ulp n y
Tactic:
rewrite [← ulp_eq]
State after:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x = y / ulp n x * ulp n x

State before:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x = y / ulp n x * ulp n x
Tactic:
apply Eq.symm
State after:
case h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x * ulp n x = x / ulp n x * ulp n x

State before:
case h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x * ulp n x = x / ulp n x * ulp n x
Tactic:
apply congr_arg (fun w => w * ulp n x)
State after:
case h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x = x / ulp n x

State before:
case h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x = x / ulp n x
Tactic:
apply Nat.eq_of_le_of_lt_succ
State after:
case h.h₁
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x ≤ y / ulp n x

case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x < x / ulp n x + 1

State before:
case h.h₁
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x ≤ y / ulp n x

case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x < x / ulp n x + 1
Tactic:
. rewrite [← Nat.mul_div_cancel (x / ulp n x) (ulp_pos n x)]
  exact Nat.div_le_div_right h
State after:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x < x / ulp n x + 1

State before:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x < x / ulp n x + 1
Tactic:
. rewrite [Nat.div_lt_iff_lt_mul (ulp_pos n x)]
  rewrite [Nat.mul_comm, Nat.mul_succ, Nat.mul_comm]
  rewrite [← trunc, ← ulp_trunc npos, ← next]
  exact k
State after:
no goals

State before:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n x = ulp n y
Tactic:
rewrite [← ulp_trunc npos]
State after:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n (trunc n x) = ulp n y

State before:
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n (trunc n x) = ulp n y
Tactic:
apply le_antisymm
State after:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n (trunc n x) ≤ ulp n y

case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n (trunc n x)

State before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n (trunc n x) ≤ ulp n y

case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n (trunc n x)
Tactic:
. apply ulp_le_ulp
  exact h
State after:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n (trunc n x)

State before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n (trunc n x)
Tactic:
. rewrite [ulp_trunc npos]
  unfold ulp expt
  apply Nat.pow_le_pow_of_le_right two_pos
  apply tsub_le_tsub_right
  rewrite [Nat.size_le]
  apply Nat.lt_of_lt_of_le k
  exact next_trunc_le npos x
State after:
no goals

State before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n (trunc n x) ≤ ulp n y
Tactic:
apply ulp_le_ulp
State after:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ trunc n x ≤ y

State before:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ trunc n x ≤ y
Tactic:
exact h
State after:
no goals

State before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n (trunc n x)
Tactic:
rewrite [ulp_trunc npos]
State after:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n x

State before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n x
Tactic:
unfold ulp expt
State after:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ 2 ^ (Nat.size y - n) ≤ 2 ^ (Nat.size x - n)

State before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ 2 ^ (Nat.size y - n) ≤ 2 ^ (Nat.size x - n)
Tactic:
apply Nat.pow_le_pow_of_le_right two_pos
State after:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ Nat.size y - n ≤ Nat.size x - n

State before:
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ Nat.size y - n ≤ Nat.size x - n
Tactic:
apply tsub_le_tsub_right
State after:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ Nat.size y ≤ Nat.size x

State before:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ Nat.size y ≤ Nat.size x
Tactic:
rewrite [Nat.size_le]
State after:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ y < 2 ^ Nat.size x

State before:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ y < 2 ^ Nat.size x
Tactic:
apply Nat.lt_of_lt_of_le k
State after:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ next n (trunc n x) ≤ 2 ^ Nat.size x

State before:
case a.h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ next n (trunc n x) ≤ 2 ^ Nat.size x
Tactic:
exact next_trunc_le npos x
State after:
no goals

State before:
case h.h₁
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x ≤ y / ulp n x
Tactic:
rewrite [← Nat.mul_div_cancel (x / ulp n x) (ulp_pos n x)]
State after:
case h.h₁
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x / ulp n x ≤ y / ulp n x

State before:
case h.h₁
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x / ulp n x ≤ y / ulp n x
Tactic:
exact Nat.div_le_div_right h
State after:
no goals

State before:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x < x / ulp n x + 1
Tactic:
rewrite [Nat.div_lt_iff_lt_mul (ulp_pos n x)]
State after:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y < (x / ulp n x + 1) * ulp n x

State before:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y < (x / ulp n x + 1) * ulp n x
Tactic:
rewrite [Nat.mul_comm, Nat.mul_succ, Nat.mul_comm]
State after:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y < x / ulp n x * ulp n x + ulp n x

State before:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y < x / ulp n x * ulp n x + ulp n x
Tactic:
rewrite [← trunc, ← ulp_trunc npos, ← next]
State after:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y < next n (trunc n x)

State before:
case h.h₂
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y < next n (trunc n x)
Tactic:
exact k
State after:
no goals