[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
a : ℤ
b : ℕ
hb : b ≠ 0
⊢ toNat a < b ↔ a < ↑b
[PROOFSTEP]
rw [← toNat_lt_toNat, toNat_coe_nat]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
a : ℤ
b : ℕ
hb : b ≠ 0
⊢ 0 < ↑b
[PROOFSTEP]
exact coe_nat_pos.2 hb.bot_lt
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : NonAssocRing α
m : ℤ
⊢ ∀ (n : ℤ), ↑(0 * n) = ↑0 * ↑n
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : NonAssocRing α
m k : ℤ
x✝ : 0 ≤ k
ih : ∀ (n : ℤ), ↑(k * n) = ↑k * ↑n
n : ℤ
⊢ ↑((k + 1) * n) = ↑(k + 1) * ↑n
[PROOFSTEP]
simp [add_mul, ih]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : NonAssocRing α
m k : ℤ
x✝ : k ≤ 0
ih : ∀ (n : ℤ), ↑(k * n) = ↑k * ↑n
n : ℤ
⊢ ↑((k - 1) * n) = ↑(k - 1) * ↑n
[PROOFSTEP]
simp [sub_mul, ih]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑↑n) x
[PROOFSTEP]
simpa using n.cast_commute x
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑-[n+1]) x
[PROOFSTEP]
simpa only [cast_negSucc, Commute.neg_left_iff, Commute.neg_right_iff] using (n + 1).cast_commute (-x)
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : OrderedRing α
⊢ Monotone fun x => ↑x
[PROOFSTEP]
intro m n h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : OrderedRing α
m n : ℤ
h : m ≤ n
⊢ (fun x => ↑x) m ≤ (fun x => ↑x) n
[PROOFSTEP]
rw [← sub_nonneg] at h 
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : OrderedRing α
m n : ℤ
h✝ : m ≤ n
h : 0 ≤ n - m
⊢ (fun x => ↑x) m ≤ (fun x => ↑x) n
[PROOFSTEP]
lift n - m to ℕ using h with k hk
[GOAL]
case intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : OrderedRing α
m n : ℤ
h : m ≤ n
k : ℕ
hk : ↑k = n - m
⊢ ↑m ≤ ↑n
[PROOFSTEP]
rw [← sub_nonneg, ← cast_sub, ← hk, cast_ofNat]
[GOAL]
case intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : OrderedRing α
m n : ℤ
h : m ≤ n
k : ℕ
hk : ↑k = n - m
⊢ 0 ≤ ↑k
[PROOFSTEP]
exact k.cast_nonneg
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
⊢ 0 ≤ ↑↑n ↔ 0 ≤ ↑n
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]
[PROOFSTEP]
have : -(n : α) < 1 := lt_of_le_of_lt (by simp) zero_lt_one
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
⊢ -↑n ≤ 0
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
this : -↑n < 1
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]
[PROOFSTEP]
simpa [(negSucc_lt_zero n).not_le, ← sub_eq_add_neg, le_neg] using this.not_le
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
m n : ℤ
⊢ ↑m ≤ ↑n ↔ m ≤ n
[PROOFSTEP]
rw [← sub_nonneg, ← cast_sub, cast_nonneg, sub_nonneg]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℤ
⊢ ↑n ≤ 0 ↔ n ≤ 0
[PROOFSTEP]
rw [← cast_zero, cast_le]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℤ
⊢ 0 < ↑n ↔ 0 < n
[PROOFSTEP]
rw [← cast_zero, cast_lt]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℤ
⊢ ↑n < 0 ↔ n < 0
[PROOFSTEP]
rw [← cast_zero, cast_lt]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
⊢ ↑|a| = |↑a|
[PROOFSTEP]
simp [abs_eq_max_neg]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
h : 0 < a
⊢ 1 ≤ ↑a
[PROOFSTEP]
exact_mod_cast Int.add_one_le_of_lt h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
h : a < 0
⊢ ↑a ≤ -1
[PROOFSTEP]
rw [← Int.cast_one, ← Int.cast_neg, cast_le]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
h : a < 0
⊢ a ≤ -1
[PROOFSTEP]
exact Int.le_sub_one_of_lt h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
⊢ 0 ≤ ↑n * x + ↑n * ↑n
[PROOFSTEP]
have hnx : 0 < n → 0 ≤ x + n := fun hn =>
  by
  have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
  rwa [add_left_neg] at this 
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hn : 0 < n
⊢ 0 ≤ x + ↑n
[PROOFSTEP]
have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hn : 0 < n
this : -1 + 1 ≤ x + ↑n
⊢ 0 ≤ x + ↑n
[PROOFSTEP]
rwa [add_left_neg] at this 
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
⊢ 0 ≤ ↑n * x + ↑n * ↑n
[PROOFSTEP]
have hnx' : n < 0 → x + n ≤ 0 := fun hn =>
  by
  have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
  rwa [add_right_neg] at this 
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hn : n < 0
⊢ x + ↑n ≤ 0
[PROOFSTEP]
have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hn : n < 0
this : x + ↑n ≤ 1 + -1
⊢ x + ↑n ≤ 0
[PROOFSTEP]
rwa [add_right_neg] at this 
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n * x + ↑n * ↑n
[PROOFSTEP]
rw [← mul_add, mul_nonneg_iff]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
[PROOFSTEP]
rcases lt_trichotomy n 0 with (h | rfl | h)
[GOAL]
case inl
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : n < 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
[PROOFSTEP]
exact Or.inr ⟨by exact_mod_cast h.le, hnx' h⟩
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : n < 0
⊢ ↑n ≤ 0
[PROOFSTEP]
exact_mod_cast h.le
[GOAL]
case inr.inl
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < 0 → 0 ≤ x + ↑0
hnx' : 0 < 0 → x + ↑0 ≤ 0
⊢ 0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0
[PROOFSTEP]
simp [le_total 0 x]
[GOAL]
case inr.inr
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
[PROOFSTEP]
exact Or.inl ⟨by exact_mod_cast h.le, hnx h⟩
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n
[PROOFSTEP]
exact_mod_cast h.le
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
⊢ ↑(natAbs n) = ↑|n|
[PROOFSTEP]
cases n
[GOAL]
case ofNat
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b : ℤ
a✝ : ℕ
⊢ ↑(natAbs (ofNat a✝)) = ↑|ofNat a✝|
[PROOFSTEP]
simp
[GOAL]
case negSucc
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b : ℤ
a✝ : ℕ
⊢ ↑(natAbs -[a✝+1]) = ↑|-[a✝+1]|
[PROOFSTEP]
rw [abs_eq_natAbs, natAbs_negSucc, cast_succ, cast_ofNat, cast_succ]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
A : Type u_5
inst✝ : AddGroupWithOne A
f : ℤ →+ A
h1 : ↑f 1 = 1
⊢ ↑f 1 = ↑(castAddHom A) 1
[PROOFSTEP]
simp [h1]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
⊢ f = g
[PROOFSTEP]
ext (x | x)
[GOAL]
case h.ofNat
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f (ofNat x) = ↑g (ofNat x)
[PROOFSTEP]
exact (FunLike.congr_fun h_nat x : _)
[GOAL]
case h.negSucc
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f -[x+1] = ↑g -[x+1]
[PROOFSTEP]
rw [Int.negSucc_eq, ← neg_one_mul, f.map_mul, g.map_mul]
[GOAL]
case h.negSucc
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f (-1) * ↑f (↑x + 1) = ↑g (-1) * ↑g (↑x + 1)
[PROOFSTEP]
congr 1
[GOAL]
case h.negSucc.e_a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f (↑x + 1) = ↑g (↑x + 1)
[PROOFSTEP]
exact_mod_cast (FunLike.congr_fun h_nat (x + 1) : _)
