-- Mathlib/Algebra/Order/Floor.lean
theorem floor_sub_nat [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) (n : ℕ) :
    ⌊a - n⌋₊ = ⌊a⌋₊ - n

Proof state:
case inr.inr
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
rw [eq_tsub_iff_add_eq_of_le (le_floor h), ← floor_add_nat _, tsub_add_cancel_of_le h]

Result:
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ 0 ≤ a - ↑n

Proof state:
case inr.inl
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a⌋₊ ≤ n

Tactic:
exact Nat.cast_le.1 ((Nat.floor_le ha).trans h)

Result:
no goals

Proof state:
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ 0 ≤ a - ↑n

Tactic:
exact le_tsub_of_add_le_left ((add_zero _).trans_le h)

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : a ≤ 0
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
rw [floor_of_nonpos ha, floor_of_nonpos (tsub_nonpos_of_le (ha.trans n.cast_nonneg)), zero_tsub]

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
rcases le_total a n with h | h

Result:
case inr.inl
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

case inr.inr
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Proof state:
case inr.inl
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
rw [floor_of_nonpos (tsub_nonpos_of_le h), eq_comm, tsub_eq_zero_iff_le]

Result:
case inr.inl
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a⌋₊ ≤ n

Proof state:
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
obtain ha | ha := le_total a 0

Result:
case inl
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : a ≤ 0
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

case inr
α : Type u_2
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n