-- Mathlib/Data/Num/Lemmas.lean
theorem castNum_shiftRight (m : Num) (n : Nat) : ↑(m >>> n) = (m : ℕ) >>> (n : ℕ)

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
m✝ : ℕ
⊢ (m✝ + m✝) / 2 = m✝

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑m = (↑m + ↑m) >>> 1

Tactic:
simp [-add_assoc, Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, hdiv2]

Result:
no goals

Proof state:
case zero
n : ℕ
⊢ ↑0 = ↑zero >>> n

Tactic:
symm

Result:
case zero
n : ℕ
⊢ ↑zero >>> n = ↑0

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m + 1) >>> 1 >>> n

Tactic:
apply congr_arg fun x => Nat.shiftRight x n

Result:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑m = (↑m + ↑m + 1) >>> 1

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(pos m) >>> n = ↑(pos m.bit0) >>> (n + 1)

Tactic:
change Nat.shiftRight m n = Nat.shiftRight (m + m) (n + 1)

Result:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m).shiftRight (n + 1)

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
m✝ : ℕ
⊢ (m✝ + m✝).div2 = m✝

Tactic:
rw [Nat.div2_val]

Result:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
m✝ : ℕ
⊢ (m✝ + m✝) / 2 = m✝

Proof state:
case zero
n : ℕ
⊢ ↑zero >>> n = ↑0

Tactic:
apply Nat.zero_shiftRight

Result:
no goals

Proof state:
case pos.succ.bit1
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit1) >>> (n + 1)

Tactic:
trans

Result:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ?m.194077

n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ?m.194077 = ↑(pos m.bit1) >>> (n + 1)

n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ℕ

Proof state:
case pos
n : ℕ
m : PosNum
⊢ ↑(m >>> n) = ↑(pos m) >>> n

Tactic:
induction' n with n IH generalizing m

Result:
case pos.zero
m : PosNum
⊢ ↑(m >>> 0) = ↑(pos m) >>> 0

case pos.succ
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
⊢ ↑(m >>> (n + 1)) = ↑(pos m) >>> (n + 1)

Proof state:
case pos.succ.one.h₀
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(pos one) < 2 ^ (n + 1)

Tactic:
simp

Result:
no goals

Proof state:
case pos.succ
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
⊢ ↑(m >>> (n + 1)) = ↑(pos m) >>> (n + 1)

Tactic:
have hdiv2 : ∀ m, Nat.div2 (m + m) = m := by intro; rw [Nat.div2_val]; omega

Result:
case pos.succ
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(m >>> (n + 1)) = ↑(pos m) >>> (n + 1)

Proof state:
case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(one.shiftr (n + 1)) = ↑(pos one) >>> (n + 1)

Tactic:
rw [Nat.shiftRight_eq_div_pow]

Result:
case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(one.shiftr (n + 1)) = ↑(pos one) / 2 ^ (n + 1)

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
⊢ ∀ (m : ℕ), (m + m).div2 = m

Tactic:
intro

Result:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
m✝ : ℕ
⊢ (m✝ + m✝).div2 = m✝

Proof state:
m : Num
n : ℕ
⊢ ↑(m >>> n) = ↑m >>> n

Tactic:
obtain - | m := m <;> dsimp only [← shiftr_eq_shiftRight, shiftr]

Result:
case zero
n : ℕ
⊢ ↑0 = ↑zero >>> n

case pos
n : ℕ
m : PosNum
⊢ ↑(m >>> n) = ↑(pos m) >>> n

Proof state:
case pos.zero
m : PosNum
⊢ ↑(m >>> 0) = ↑(pos m) >>> 0

Tactic:
cases m <;> rfl

Result:
no goals

Proof state:
case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(one.shiftr (n + 1)) = ↑(pos one) / 2 ^ (n + 1)

Tactic:
symm

Result:
case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(pos one) / 2 ^ (n + 1) = ↑(one.shiftr (n + 1))

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m) >>> 1 >>> n

Tactic:
apply congr_arg fun x => Nat.shiftRight x n

Result:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑m = (↑m + ↑m) >>> 1

Proof state:
case pos.succ
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(m >>> (n + 1)) = ↑(pos m) >>> (n + 1)

Tactic:
obtain - | m | m := m <;> dsimp only [PosNum.shiftr, ← PosNum.shiftr_eq_shiftRight]

Result:
case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(one.shiftr (n + 1)) = ↑(pos one) >>> (n + 1)

case pos.succ.bit1
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit1) >>> (n + 1)

case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit0) >>> (n + 1)

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m + 1).shiftRight (n + 1)

Tactic:
rw [add_comm n 1, @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]

Result:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m + 1) >>> 1 >>> n

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(pos m) >>> n = ↑(pos m.bit1) >>> (n + 1)

Tactic:
change Nat.shiftRight m n = Nat.shiftRight (m + m + 1) (n + 1)

Result:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m + 1).shiftRight (n + 1)

Proof state:
case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(pos one) / 2 ^ (n + 1) = ↑(one.shiftr (n + 1))

Tactic:
apply Nat.div_eq_of_lt

Result:
case pos.succ.one.h₀
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑(pos one) < 2 ^ (n + 1)

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ?m.195607

Tactic:
apply IH

Result:
no goals

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m).shiftRight (n + 1)

Tactic:
rw [add_comm n 1,  @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]

Result:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑m).shiftRight n = (↑m + ↑m) >>> 1 >>> n

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑m = (↑m + ↑m + 1) >>> 1

Tactic:
simp [-add_assoc, Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, hdiv2]

Result:
no goals

Proof state:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ?m.194077

Tactic:
apply IH

Result:
no goals