Theorem: sterbenz (Fl.lean)

State before:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ 2 * b
⊢ trunc n (a - b) = a - b
Tactic:
rewrite [Nat.two_mul] at hab
State after:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ trunc n (a - b) = a - b

State before:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ trunc n (a - b) = a - b
Tactic:
apply trunc_eq_of_le_of_ulp_dvd b
State after:
case hle
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ a - b ≤ b

case hdvd
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a - b

State before:
case hle
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ a - b ≤ b

case hdvd
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a - b
Tactic:
. exact tsub_le_iff_right.mpr hab
State after:
case hdvd
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a - b

State before:
case hdvd
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a - b
Tactic:
. apply Nat.dvd_sub'
  . trans ulp n a
    . exact ulp_dvd_ulp n hba
    . exact ulp_dvd_of_trunc_eq hfa
  . exact ulp_dvd_of_trunc_eq hfb
State after:
no goals

State before:
case hle
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ a - b ≤ b
Tactic:
exact tsub_le_iff_right.mpr hab
State after:
no goals

State before:
case hdvd
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a - b
Tactic:
apply Nat.dvd_sub'
State after:
case hdvd.h₁
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a

case hdvd.h₂
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ b

State before:
case hdvd.h₁
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a

case hdvd.h₂
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ b
Tactic:
. trans ulp n a
  . exact ulp_dvd_ulp n hba
  . exact ulp_dvd_of_trunc_eq hfa
State after:
case hdvd.h₂
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ b

State before:
case hdvd.h₂
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ b
Tactic:
. exact ulp_dvd_of_trunc_eq hfb
State after:
no goals

State before:
case hdvd.h₁
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a
Tactic:
trans ulp n a
State after:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ ulp n a

n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n a ∣ a

State before:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ ulp n a

n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n a ∣ a
Tactic:
. exact ulp_dvd_ulp n hba
State after:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n a ∣ a

State before:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n a ∣ a
Tactic:
. exact ulp_dvd_of_trunc_eq hfa
State after:
no goals

State before:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ ulp n a
Tactic:
exact ulp_dvd_ulp n hba
State after:
no goals

State before:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n a ∣ a
Tactic:
exact ulp_dvd_of_trunc_eq hfa
State after:
no goals

State before:
case hdvd.h₂
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ b
Tactic:
exact ulp_dvd_of_trunc_eq hfb
State after:
no goals