Theorem: Nat.div_le_div (Algdata/Init/Nat.lean)

State before:
a b c : Nat
⊢ a ≤ b → a / c ≤ b / c
Tactic:
intro hab
State after:
a b c : Nat
hab : a ≤ b
⊢ a / c ≤ b / c

State before:
a b c : Nat
hab : a ≤ b
⊢ a / c ≤ b / c
Tactic:
cases Nat.lt_or_ge (b/c) (a/c)
State after:
case inl
a b c : Nat
hab : a ≤ b
h✝ : b / c < a / c
⊢ a / c ≤ b / c

case inr
a b c : Nat
hab : a ≤ b
h✝ : b / c ≥ a / c
⊢ a / c ≤ b / c

State before:
a b c : Nat
hab : a ≤ b
hge : b / c ≥ a / c
⊢ a / c ≤ b / c
Tactic:
case inr hge => exact hge
State after:
no goals

State before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
⊢ a / c ≤ b / c
Tactic:
case inl hlt =>
  have : c > 0 := (Nat.lt_or_ge 0 c).elim id $ by
    intro h; cases h; rw [Nat.div_zero, Nat.div_zero] at hlt; cases hlt
  have := (Nat.div_lt_iff_lt_mul ‹c>0›).mp hlt
  have := calc
    b < a/c*c := this
    _ ≤ a := Nat.div_mul_le_self a c
    _ ≤ b := hab
  exact absurd this (Nat.lt_irrefl b)
State after:
no goals

State before:
a b c : Nat
hab : a ≤ b
hge : b / c ≥ a / c
⊢ a / c ≤ b / c
Tactic:
exact hge
State after:
no goals

State before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
⊢ a / c ≤ b / c
Tactic:
have : c > 0 := (Nat.lt_or_ge 0 c).elim id $ by
  intro h; cases h; rw [Nat.div_zero, Nat.div_zero] at hlt; cases hlt
State after:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this : c > 0
⊢ a / c ≤ b / c

State before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this : c > 0
⊢ a / c ≤ b / c
Tactic:
have := (Nat.div_lt_iff_lt_mul ‹c>0›).mp hlt
State after:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this✝ : c > 0
this : b < a / c * c
⊢ a / c ≤ b / c

State before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this✝ : c > 0
this : b < a / c * c
⊢ a / c ≤ b / c
Tactic:
have := calc
  b < a/c*c := this
  _ ≤ a := Nat.div_mul_le_self a c
  _ ≤ b := hab
State after:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this✝¹ : c > 0
this✝ : b < a / c * c
this : b < b
⊢ a / c ≤ b / c

State before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this✝¹ : c > 0
this✝ : b < a / c * c
this : b < b
⊢ a / c ≤ b / c
Tactic:
exact absurd this (Nat.lt_irrefl b)
State after:
no goals

State before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
⊢ 0 ≥ c → c > 0
Tactic:
intro h
State after:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
h : 0 ≥ c
⊢ c > 0

State before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
h : 0 ≥ c
⊢ c > 0
Tactic:
cases h
State after:
case refl
a b : Nat
hab : a ≤ b
hlt : b / 0 < a / 0
⊢ 0 > 0

State before:
case refl
a b : Nat
hab : a ≤ b
hlt : b / 0 < a / 0
⊢ 0 > 0
Tactic:
rw [Nat.div_zero, Nat.div_zero] at hlt
State after:
case refl
a b : Nat
hab : a ≤ b
hlt : 0 < 0
⊢ 0 > 0

State before:
case refl
a b : Nat
hab : a ≤ b
hlt : 0 < 0
⊢ 0 > 0
Tactic:
cases hlt
State after:
no goals