Theorem: Pos.asBin.toNat_ne_zero (GMLInit/Data/Pos.lean)

State before:
n : Pos.asBin
⊢ n.toNat ≠ 0
Tactic:
induction n with
| one => exact Nat.one_ne_zero
| bit0 n ih =>
  rw [←Nat.mul_zero 2, asBin.toNat_bit0]
  intro h
  absurd ih
  exact Nat.eq_of_mul_eq_mul_left (Nat.is_pos 2) h
| bit1 n _ => exact Nat.succ_ne_zero (2 * n.toNat)
State after:
no goals

State before:
case one

⊢ one.toNat ≠ 0
Tactic:
exact Nat.one_ne_zero
State after:
no goals

State before:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
⊢ n.bit0.toNat ≠ 0
Tactic:
rw [←Nat.mul_zero 2, asBin.toNat_bit0]
State after:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
⊢ 2 * n.toNat ≠ 2 * 0

State before:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
⊢ 2 * n.toNat ≠ 2 * 0
Tactic:
intro h
State after:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
h : 2 * n.toNat = 2 * 0
⊢ False

State before:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
h : 2 * n.toNat = 2 * 0
⊢ False
Tactic:
absurd ih
State after:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
h : 2 * n.toNat = 2 * 0
⊢ n.toNat = 0

State before:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
h : 2 * n.toNat = 2 * 0
⊢ n.toNat = 0
Tactic:
exact Nat.eq_of_mul_eq_mul_left (Nat.is_pos 2) h
State after:
no goals

State before:
case bit1
n : Pos.asBin
a_ih✝ : n.toNat ≠ 0
⊢ n.bit1.toNat ≠ 0
Tactic:
exact Nat.succ_ne_zero (2 * n.toNat)
State after:
no goals