-- Mathlib/Algebra/Order/Floor.lean
theorem floor_div_nat (a : α) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

Tactic:
obtain rfl | hn := n.eq_zero_or_pos

Result:
case inr.inl
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
⊢ ⌊a / ↑0⌋₊ = ⌊a⌋₊ / 0

case inr.inr
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

Proof state:
case inr.inr.refine_2.right
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ a / ↑n < ↑(⌊a⌋₊ / n) + 1

Tactic:
rw [div_lt_iff₀, add_mul, one_mul, ← cast_mul, ← cast_add, ← floor_lt ha]

Result:
case inr.inr.refine_2.right
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ⌊a⌋₊ < ⌊a⌋₊ / n * n + n

case inr.inr.refine_2.right
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ 0 < ↑n

Proof state:
case inr.inr.refine_2.left
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ↑(⌊a⌋₊ / n) ≤ a / ↑n

Tactic:
exact cast_div_le.trans (div_le_div_of_nonneg_right (floor_le ha) n.cast_nonneg)

Result:
no goals

Proof state:
case inr.inl
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
⊢ ⌊a / ↑0⌋₊ = ⌊a⌋₊ / 0

Tactic:
rw [cast_zero, div_zero, Nat.div_zero, floor_zero]

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ a / ↑n ≤ 0

Tactic:
apply div_nonpos_of_nonpos_of_nonneg ha n.cast_nonneg

Result:
no goals

Proof state:
case inr.inr
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

Tactic:
refine (floor_eq_iff ?_).2 ?_

Result:
case inr.inr.refine_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ 0 ≤ a / ↑n

case inr.inr.refine_2
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ↑(⌊a⌋₊ / n) ≤ a / ↑n ∧ a / ↑n < ↑(⌊a⌋₊ / n) + 1

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

Tactic:
rw [floor_of_nonpos, floor_of_nonpos ha]

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ 0 = 0 / n

case inl
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ a / ↑n ≤ 0

Proof state:
case inr.inr.refine_2.right
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ 0 < ↑n

Tactic:
exact cast_pos.2 hn

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ 0 = 0 / n

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr.refine_2.right
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ⌊a⌋₊ < ⌊a⌋₊ / n * n + n

Tactic:
exact lt_div_mul_add hn

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

Tactic:
rcases le_total a 0 with ha | ha

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

case inr
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

Proof state:
case inr.inr.refine_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ 0 ≤ a / ↑n

Tactic:
exact div_nonneg ha n.cast_nonneg

Result:
no goals

Proof state:
case inr.inr.refine_2
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ↑(⌊a⌋₊ / n) ≤ a / ↑n ∧ a / ↑n < ↑(⌊a⌋₊ / n) + 1

Tactic:
constructor

Result:
case inr.inr.refine_2.left
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ↑(⌊a⌋₊ / n) ≤ a / ↑n

case inr.inr.refine_2.right
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ a / ↑n < ↑(⌊a⌋₊ / n) + 1