[GOAL]
α : Type u_1
inst✝ : DivisionSemiring α
m n : ℕ
n_dvd : n ∣ m
n_nonzero : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
rcases n_dvd with ⟨k, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : DivisionSemiring α
n : ℕ
n_nonzero : ↑n ≠ 0
k : ℕ
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
[PROOFSTEP]
have : n ≠ 0 := by
  rintro rfl
  simp at n_nonzero 
[GOAL]
α : Type u_1
inst✝ : DivisionSemiring α
n : ℕ
n_nonzero : ↑n ≠ 0
k : ℕ
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝ : DivisionSemiring α
k : ℕ
n_nonzero : ↑0 ≠ 0
⊢ False
[PROOFSTEP]
simp at n_nonzero 
[GOAL]
case intro
α : Type u_1
inst✝ : DivisionSemiring α
n : ℕ
n_nonzero : ↑n ≠ 0
k : ℕ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
[PROOFSTEP]
rw [Nat.mul_div_cancel_left _ this.bot_lt, mul_comm n k, cast_mul, mul_div_cancel _ n_nonzero]
[GOAL]
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
[PROOFSTEP]
rcases eq_or_ne d 0 with (rfl | hd)
[GOAL]
case inl
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n : ℕ
hn : 0 ∣ n
hm : 0 ∣ m
⊢ ↑(m / 0) / ↑(n / 0) = ↑m / ↑n
[PROOFSTEP]
simp [zero_dvd_iff.mp hm]
[GOAL]
case inr
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
[PROOFSTEP]
replace hd : (d : α) ≠ 0
[GOAL]
case hd
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
case inr
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
[PROOFSTEP]
rw [cast_div hm, cast_div hn, div_div_div_cancel_right _ hd]
[GOAL]
case inr
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
exact hd
[GOAL]
case inr
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
exact hd
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n : ℕ
⊢ ↑(m / n) ≤ ↑m / ↑n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
inst✝ : LinearOrderedSemifield α
m : ℕ
⊢ ↑(m / zero) ≤ ↑m / ↑zero
[PROOFSTEP]
rw [cast_zero, div_zero, Nat.div_zero, cast_zero]
[GOAL]
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ ↑(m / succ n✝) ≤ ↑m / ↑(succ n✝)
[PROOFSTEP]
rw [le_div_iff, ← Nat.cast_mul, @Nat.cast_le]
[GOAL]
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ m / succ n✝ * succ n✝ ≤ m
case succ α : Type u_1 inst✝ : LinearOrderedSemifield α m n✝ : ℕ ⊢ 0 < ↑(succ n✝)
[PROOFSTEP]
exact (Nat.div_mul_le_self m _)
[GOAL]
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ 0 < ↑(succ n✝)
[PROOFSTEP]
exact Nat.cast_pos.2 (Nat.succ_pos _)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
n : ℕ
⊢ 0 < 1 / (↑n + 1)
[PROOFSTEP]
rw [one_div]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
n : ℕ
⊢ 0 < (↑n + 1)⁻¹
[PROOFSTEP]
exact inv_pos_of_nat
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n ≤ m
⊢ 1 / (↑m + 1) ≤ 1 / (↑n + 1)
[PROOFSTEP]
refine' one_div_le_one_div_of_le _ _
[GOAL]
case refine'_1
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n ≤ m
⊢ 0 < ↑n + 1
case refine'_2 α : Type u_1 inst✝ : LinearOrderedSemifield α n m : ℕ h : n ≤ m ⊢ ↑n + 1 ≤ ↑m + 1
[PROOFSTEP]
exact Nat.cast_add_one_pos _
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n ≤ m
⊢ ↑n + 1 ≤ ↑m + 1
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n < m
⊢ 1 / (↑m + 1) < 1 / (↑n + 1)
[PROOFSTEP]
refine' one_div_lt_one_div_of_lt _ _
[GOAL]
case refine'_1
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n < m
⊢ 0 < ↑n + 1
case refine'_2 α : Type u_1 inst✝ : LinearOrderedSemifield α n m : ℕ h : n < m ⊢ ↑n + 1 < ↑m + 1
[PROOFSTEP]
exact Nat.cast_add_one_pos _
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n < m
⊢ ↑n + 1 < ↑m + 1
[PROOFSTEP]
simpa
