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

State before:
m n : Nat
⊢ (∀ (i : Nat), getBit m i = getBit n i) → m = n
Tactic:
intro h
State after:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
⊢ m = n

State before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
⊢ m = n
Tactic:
have : m % 2 = n % 2 := eq_mod2_of_decide $ h 0
State after:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
⊢ m = n

State before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
⊢ m = n
Tactic:
have : m / 2 = n / 2 := by
  cases m.eq_zero_or_pos
  case inl hm => 
    cases hm; apply Eq.symm
    apply eq_zero_of_getBit
    exact λ i => zero_getBit i.succ ▸ (h i.succ).symm
  case inr hm =>
    have : m/2 < m := Nat.div_lt_self hm (Nat.lt_succ_self 1)
    exact bitext (m:=m/2) (n:=n/2) (λ i => h i.succ)
State after:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this✝ : m % 2 = n % 2
this : m / 2 = n / 2
⊢ m = n

State before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this✝ : m % 2 = n % 2
this : m / 2 = n / 2
⊢ m = n
Tactic:
exact eq_of_div_mod_two_eq ‹_› ‹_›
State after:
no goals

State before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
⊢ m / 2 = n / 2
Tactic:
cases m.eq_zero_or_pos
State after:
case inl
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
h✝ : m = 0
⊢ m / 2 = n / 2

case inr
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
h✝ : m > 0
⊢ m / 2 = n / 2

State before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
hm : m = 0
⊢ m / 2 = n / 2
Tactic:
case inl hm => 
  cases hm; apply Eq.symm
  apply eq_zero_of_getBit
  exact λ i => zero_getBit i.succ ▸ (h i.succ).symm
State after:
no goals

State before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
hm : m > 0
⊢ m / 2 = n / 2
Tactic:
case inr hm =>
  have : m/2 < m := Nat.div_lt_self hm (Nat.lt_succ_self 1)
  exact bitext (m:=m/2) (n:=n/2) (λ i => h i.succ)
State after:
no goals

State before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
hm : m = 0
⊢ m / 2 = n / 2
Tactic:
cases hm
State after:
case refl
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ 0 / 2 = n / 2

State before:
case refl
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ 0 / 2 = n / 2
Tactic:
apply Eq.symm
State after:
case refl.h
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ n / 2 = 0 / 2

State before:
case refl.h
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ n / 2 = 0 / 2
Tactic:
apply eq_zero_of_getBit
State after:
case refl.h.h
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ ∀ (i : Nat), getBit (n / 2) i = false

State before:
case refl.h.h
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ ∀ (i : Nat), getBit (n / 2) i = false
Tactic:
exact λ i => zero_getBit i.succ ▸ (h i.succ).symm
State after:
no goals

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

State before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this✝ : m % 2 = n % 2
hm : m > 0
this : m / 2 < m
⊢ m / 2 = n / 2
Tactic:
exact bitext (m:=m/2) (n:=n/2) (λ i => h i.succ)
State after:
no goals