Theorem: Nat.eq_zero_of_getBit (Algdata/Data/Nat/Bits.lean)

State before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
⊢ n = 0
Tactic:
cases n.eq_zero_or_pos
State after:
case inl
n : Nat
h : ∀ (i : Nat), getBit n i = false
h✝ : n = 0
⊢ n = 0

case inr
n : Nat
h : ∀ (i : Nat), getBit n i = false
h✝ : n > 0
⊢ n = 0

State before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hzero : n = 0
⊢ n = 0
Tactic:
case inl hzero => exact hzero
State after:
no goals

State before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
⊢ n = 0
Tactic:
case inr hpos =>
  have : n/2 < n := Nat.div_lt_self hpos (Nat.lt_succ_self 1)
  have : n/2 = 0 := eq_zero_of_getBit (n:=n/2) (λ i => h i.succ)
  have : n%2 = 0 := eq_mod2_of_decide (n:=0) (h 0)
  exact eq_of_div_mod_two_eq (n:=0) ‹n/2=0› ‹n%2=0›
State after:
no goals

State before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hzero : n = 0
⊢ n = 0
Tactic:
exact hzero
State after:
no goals

State before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
⊢ n = 0
Tactic:
have : n/2 < n := Nat.div_lt_self hpos (Nat.lt_succ_self 1)
State after:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this : n / 2 < n
⊢ n = 0

State before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this : n / 2 < n
⊢ n = 0
Tactic:
have : n/2 = 0 := eq_zero_of_getBit (n:=n/2) (λ i => h i.succ)
State after:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this✝ : n / 2 < n
this : n / 2 = 0
⊢ n = 0

State before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this✝ : n / 2 < n
this : n / 2 = 0
⊢ n = 0
Tactic:
have : n%2 = 0 := eq_mod2_of_decide (n:=0) (h 0)
State after:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this✝¹ : n / 2 < n
this✝ : n / 2 = 0
this : n % 2 = 0
⊢ n = 0

State before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this✝¹ : n / 2 < n
this✝ : n / 2 = 0
this : n % 2 = 0
⊢ n = 0
Tactic:
exact eq_of_div_mod_two_eq (n:=0) ‹n/2=0› ‹n%2=0›
State after:
no goals