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

State before:
n : Nat
⊢ n % 2 = 0 → n ||| 1 = n + 1
Tactic:
intro hn
State after:
n : Nat
hn : n % 2 = 0
⊢ n ||| 1 = n + 1

State before:
n : Nat
hn : n % 2 = 0
⊢ n ||| 1 = n + 1
Tactic:
have hn2_neq_1: n % 2 ≠ 1 := λ h => absurd (Eq.trans hn.symm h) Nat.zero_ne_one
State after:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
⊢ n ||| 1 = n + 1

State before:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
⊢ n ||| 1 = n + 1
Tactic:
conv =>
  lhs;
  dsimp [HOr.hOr, OrOp.or, Nat.lor]; unfold bitwise
  rw [if_neg Nat.one_ne_zero, Bool.false_or, if_pos rfl]
  zeta
  rw [decide_eq_false hn2_neq_1, Bool.false_or, decide_eq_true, if_pos rfl]
  change if n = 0 then 1 else ((n/2) ||| 0) + ((n/2) ||| 0) + 1
  rw [Nat.lor_zero, ←Nat.mul_two]
  rw [Nat.div_mul_cancel ((Nat.dvd_iff_mod_eq_zero 2 n).mpr hn)]
State after:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
⊢ (if n = 0 then 1 else n + 1) = n + 1

State before:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
⊢ (if n = 0 then 1 else n + 1) = n + 1
Tactic:
by_cases n = 0
State after:
case pos
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h✝ : n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1

case neg
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h✝ : ¬n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1

State before:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h : n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1
Tactic:
case pos h => cases h; rw [if_pos rfl]
State after:
no goals

State before:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h : ¬n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1
Tactic:
case neg h => rw [if_neg h]
State after:
no goals

State before:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h : n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1
Tactic:
cases h
State after:
case refl
hn : 0 % 2 = 0
hn2_neq_1 : 0 % 2 ≠ 1
⊢ (if 0 = 0 then 1 else 0 + 1) = 0 + 1

State before:
case refl
hn : 0 % 2 = 0
hn2_neq_1 : 0 % 2 ≠ 1
⊢ (if 0 = 0 then 1 else 0 + 1) = 0 + 1
Tactic:
rw [if_pos rfl]
State after:
no goals

State before:
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
h : ¬n = 0
⊢ (if n = 0 then 1 else n + 1) = n + 1
Tactic:
rw [if_neg h]
State after:
no goals