Theorem: Nat.add_mul_div_left (Runtime/Utilities/Std.lean)

State before:
x z y : Nat
H : 0 < y
⊢ (x + y * z) / y = x / y + z
Tactic:
induction z with
| zero => rw [Nat.mul_zero, Nat.add_zero, Nat.add_zero]
| succ z ih => rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]; rfl
State after:
no goals

State before:
case zero
x y : Nat
H : 0 < y
⊢ (x + y * zero) / y = x / y + zero
Tactic:
rw [Nat.mul_zero, Nat.add_zero, Nat.add_zero]
State after:
no goals

State before:
case succ
x y : Nat
H : 0 < y
z : Nat
ih : (x + y * z) / y = x / y + z
⊢ (x + y * succ z) / y = x / y + succ z
Tactic:
rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]
State after:
case succ
x y : Nat
H : 0 < y
z : Nat
ih : (x + y * z) / y = x / y + z
⊢ succ (x / y + z) = x / y + succ z

State before:
case succ
x y : Nat
H : 0 < y
z : Nat
ih : (x + y * z) / y = x / y + z
⊢ succ (x / y + z) = x / y + succ z
Tactic:
rfl
State after:
no goals