-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_div_eq_div_mul (m n k : Nat) : m / n / k = m / (n * k)

Proof state:
m n k : Nat
⊢ m / n / k = m / (n * k)

Tactic:
cases eq_zero_or_pos k with
| inl k0 => rw [k0, Nat.mul_zero, Nat.div_zero, Nat.div_zero] | inr kpos => ?_

Result:
case inr
m n k : Nat
kpos : k > 0
⊢ m / n / k = m / (n * k)

Proof state:
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k * (n * k) ≤ m

case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Tactic:
rw [Nat.mul_comm n k, ← Nat.mul_assoc]

Result:
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k * k * n ≤ m

case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Proof state:
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k ≤ m / n / k

case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Tactic:
(apply Nat.le_refl)

Result:
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Proof state:
case inr.inr
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k = m / (n * k)

Tactic:
apply Nat.le_antisymm

Result:
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k ≤ m / (n * k)

case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Proof state:
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) * k ≤ m / n

Tactic:
apply (le_div_iff_mul_le npos).2

Result:
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) * k * n ≤ m

Proof state:
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k * k ≤ m / n

case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Tactic:
apply (le_div_iff_mul_le kpos).1

Result:
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k ≤ m / n / k

case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Proof state:
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Tactic:
apply (le_div_iff_mul_le kpos).2

Result:
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) * k ≤ m / n

Proof state:
case inr
m n k : Nat
kpos : k > 0
⊢ m / n / k = m / (n * k)

Tactic:
cases eq_zero_or_pos n with
| inl n0 => rw [n0, Nat.zero_mul, Nat.div_zero, Nat.zero_div] | inr npos => ?_

Result:
case inr.inr
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k = m / (n * k)

Proof state:
case inl
m n k : Nat
k0 : k = 0
⊢ m / n / k = m / (n * k)

Tactic:
rw [k0, Nat.mul_zero, Nat.div_zero, Nat.div_zero]

Result:
no goals

Proof state:
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k ≤ m / (n * k)

case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Tactic:
apply (le_div_iff_mul_le (Nat.mul_pos npos kpos)).2

Result:
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k * (n * k) ≤ m

case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Proof state:
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) * k * n ≤ m

Tactic:
rw [Nat.mul_assoc, Nat.mul_comm n k]

Result:
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (k * n) * (k * n) ≤ m

Proof state:
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k ≤ m / n / k

case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Tactic:
apply Nat.le_refl

Result:
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Proof state:
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (k * n) ≤ m / (k * n)

Tactic:
apply Nat.le_refl

Result:
no goals

Proof state:
case inr.inl
m n k : Nat
kpos : k > 0
n0 : n = 0
⊢ m / n / k = m / (n * k)

Tactic:
rw [n0, Nat.zero_mul, Nat.div_zero, Nat.zero_div]

Result:
no goals

Proof state:
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k * k * n ≤ m

case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Tactic:
apply (le_div_iff_mul_le npos).1

Result:
case inr.inr.h₁
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / n / k * k ≤ m / n

case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (n * k) ≤ m / n / k

Proof state:
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (k * n) * (k * n) ≤ m

Tactic:
apply (le_div_iff_mul_le (Nat.mul_pos kpos npos)).1

Result:
case inr.inr.h₂
m n k : Nat
kpos : k > 0
npos : n > 0
⊢ m / (k * n) ≤ m / (k * n)