Theorem: Nat.mul_div (ListPowersProblem.lean)

State before:
a b : ℕ
hb : 0 < b
⊢ a * b / b = a
Tactic:
have hb' : b ≠ 0 := by 
  rintro ⟨⟩; contradiction
State after:
a b : ℕ
hb : 0 < b
hb' : b ≠ 0
⊢ a * b / b = a

State before:
a b : ℕ
hb : 0 < b
hb' : b ≠ 0
⊢ a * b / b = a
Tactic:
induction a generalizing b
<;> simp [Nat.succ_mul, Nat.add_div hb, hb', *]
State after:
no goals

State before:
a b : ℕ
hb : 0 < b
⊢ b ≠ 0
Tactic:
rintro ⟨⟩
State after:
case refl
a : ℕ
hb : 0 < 0
⊢ False

State before:
case refl
a : ℕ
hb : 0 < 0
⊢ False
Tactic:
contradiction
State after:
no goals