Theorem: HTPI.le_nonzero_prod_left (HTPILib/Chap7.lean)

State before:
a b : ℕ
h : a * b ≠ 0
⊢ a ≤ a * b
Tactic:
have h1 : b ≠ 0 := by
  contradict h with h1
  rewrite [h1]
  ring
  done
State after:
a b : ℕ
h : a * b ≠ 0
h1 : b ≠ 0
⊢ a ≤ a * b

State before:
a b : ℕ
h : a * b ≠ 0
h1 : b ≠ 0
⊢ a ≤ a * b
Tactic:
have h2 : 1 ≤ b := Nat.pos_of_ne_zero h1
State after:
a b : ℕ
h : a * b ≠ 0
h1 : b ≠ 0
h2 : 1 ≤ b
⊢ a ≤ a * b

State before:
a b : ℕ
h : a * b ≠ 0
h1 : b ≠ 0
h2 : 1 ≤ b
⊢ a ≤ a * b
Tactic:
show a ≤ a * b from
  calc a
      = a * 1 := (mul_one a).symm
    _ ≤ a * b := by rel [h2]
State after:
no goals

State before:
a b : ℕ
h : a * b ≠ 0
⊢ b ≠ 0
Tactic:
contradict h with h1
State after:
a b : ℕ
h : a * b ≠ 0
h1 : b = 0
⊢ a * b = 0

State before:
a b : ℕ
h : a * b ≠ 0
h1 : b = 0
⊢ a * b = 0
Tactic:
rewrite [h1]
State after:
a b : ℕ
h : a * b ≠ 0
h1 : b = 0
⊢ a * 0 = 0

State before:
a b : ℕ
h : a * b ≠ 0
h1 : b = 0
⊢ a * 0 = 0
Tactic:
ring
State after:
no goals

State before:
a b : ℕ
h : a * b ≠ 0
h1 : b ≠ 0
h2 : 1 ≤ b
⊢ a * 1 ≤ a * b
Tactic:
rel [h2]
State after:
no goals