Theorem: IMOSL.IMO2006A1.floor_f_natAbs_le (IMOSLLean4/IMO2006/A1/A1.lean)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ ⌊f r⌋.natAbs ≤ ⌊r⌋.natAbs
Tactic:
rw [← Nat.cast_le (α := ℤ), Int.cast_natAbs, Int.cast_natAbs,
  Int.cast_abs, Int.cast_id, Int.cast_abs, Int.cast_id]
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ |⌊f r⌋| ≤ |⌊r⌋|

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ |⌊f r⌋| ≤ |⌊r⌋|
Tactic:
rcases le_total 0 ⌊r⌋ with h | h
State after:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : 0 ≤ ⌊r⌋
⊢ |⌊f r⌋| ≤ |⌊r⌋|

case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ⌊r⌋ ≤ 0
⊢ |⌊f r⌋| ≤ |⌊r⌋|

State before:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : 0 ≤ ⌊r⌋
⊢ |⌊f r⌋| ≤ |⌊r⌋|
Tactic:
rw [abs_eq_self.mpr h, abs_eq_self.mpr (floor_f_nonneg h), ← Int.cast_le (R := R)]
State after:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : 0 ≤ ⌊r⌋
⊢ ↑⌊f r⌋ ≤ ↑⌊r⌋

State before:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : 0 ≤ ⌊r⌋
⊢ ↑⌊f r⌋ ≤ ↑⌊r⌋
Tactic:
exact (Int.floor_le _).trans <| mul_le_of_le_one_right
  (Int.cast_nonneg.mpr h) (Int.fract_lt_one r).le
State after:
no goals

State before:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ⌊r⌋ ≤ 0
⊢ |⌊f r⌋| ≤ |⌊r⌋|
Tactic:
rw [abs_eq_neg_self.mpr h, abs_eq_neg_self.mpr (floor_f_nonpos h),
  neg_le_neg_iff, Int.le_floor]
State after:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ⌊r⌋ ≤ 0
⊢ ↑⌊r⌋ ≤ f r

State before:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ⌊r⌋ ≤ 0
⊢ ↑⌊r⌋ ≤ f r
Tactic:
exact le_mul_of_le_one_right (Int.cast_nonpos.mpr h) (Int.fract_lt_one r).le
State after:
no goals