Theorem: trunc_trunc_sub_ulp_eq (Fl/Trunc.lean)

State before:
n x : ℕ
npos : 0 < n
⊢ trunc n (trunc n x - ulp n x) = trunc n x - ulp n x
Tactic:
apply trunc_eq_of_le_of_ulp_dvd
State after:
case hle
n x : ℕ
npos : 0 < n
⊢ trunc n x - ulp n x ≤ ?x

case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n ?x ∣ trunc n x - ulp n x

case x
n x : ℕ
npos : 0 < n
⊢ ℕ

State before:
case hle
n x : ℕ
npos : 0 < n
⊢ trunc n x - ulp n x ≤ ?x

case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n ?x ∣ trunc n x - ulp n x

case x
n x : ℕ
npos : 0 < n
⊢ ℕ
Tactic:
. exact tsub_le_self
State after:
case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n (trunc n x) ∣ trunc n x - ulp n x

State before:
case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n (trunc n x) ∣ trunc n x - ulp n x
Tactic:
. rewrite [ulp_trunc npos]
  apply Nat.dvd_sub'
  . exact ulp_dvd_trunc n _
  . exact Nat.dvd_refl _
State after:
no goals

State before:
case hle
n x : ℕ
npos : 0 < n
⊢ trunc n x - ulp n x ≤ ?x
Tactic:
exact tsub_le_self
State after:
no goals

State before:
case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n (trunc n x) ∣ trunc n x - ulp n x
Tactic:
rewrite [ulp_trunc npos]
State after:
case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ trunc n x - ulp n x

State before:
case hdvd
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ trunc n x - ulp n x
Tactic:
apply Nat.dvd_sub'
State after:
case hdvd.h₁
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ trunc n x

case hdvd.h₂
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ ulp n x

State before:
case hdvd.h₁
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ trunc n x

case hdvd.h₂
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ ulp n x
Tactic:
. exact ulp_dvd_trunc n _
State after:
case hdvd.h₂
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ ulp n x

State before:
case hdvd.h₂
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ ulp n x
Tactic:
. exact Nat.dvd_refl _
State after:
no goals

State before:
case hdvd.h₁
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ trunc n x
Tactic:
exact ulp_dvd_trunc n _
State after:
no goals

State before:
case hdvd.h₂
n x : ℕ
npos : 0 < n
⊢ ulp n x ∣ ulp n x
Tactic:
exact Nat.dvd_refl _
State after:
no goals