internlm/Lean-Github huggingface dataset:
Theorem: List.Index.map_eq_iff_eq_unmap
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
⊢ map f i = j ↔ i = unmap f j
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
⊢ map f i = j → i = unmap f j

case mpr
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
⊢ i = unmap f j → map f i = j
Theorem: List.Index.map_eq_iff_eq_unmap
Proof state before:
case mp
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
⊢ map f i = j → i = unmap f j
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
h : map f i = j
⊢ i = unmap f j
Theorem: List.Index.map_eq_iff_eq_unmap
Proof state before:
case mp
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
h : map f i = j
⊢ i = unmap f j
Tactic:
rw [←h, unmap_map]
Proof state after:
no goals
Theorem: List.Index.map_eq_iff_eq_unmap
Proof state before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
⊢ i = unmap f j → map f i = j
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
h : i = unmap f j
⊢ map f i = j
Theorem: List.Index.map_eq_iff_eq_unmap
Proof state before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
h : i = unmap f j
⊢ map f i = j
Tactic:
rw [h, map_unmap]
Proof state after:
no goals
Theorem: List.Index.unmap_eq_iff_eq_map
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : (List.map f xs).Index
j : xs.Index
⊢ unmap f i = j ↔ i = map f j
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : (List.map f xs).Index
j : xs.Index
⊢ unmap f i = j → i = map f j

case mpr
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : (List.map f xs).Index
j : xs.Index
⊢ i = map f j → unmap f i = j
Theorem: List.Index.unmap_eq_iff_eq_map
Proof state before:
case mp
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : (List.map f xs).Index
j : xs.Index
⊢ unmap f i = j → i = map f j
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : (List.map f xs).Index
j : xs.Index
h : unmap f i = j
⊢ i = map f j
Theorem: List.Index.unmap_eq_iff_eq_map
Proof state before:
case mp
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : (List.map f xs).Index
j : xs.Index
h : unmap f i = j
⊢ i = map f j
Tactic:
rw [←h, map_unmap]
Proof state after:
no goals
Theorem: List.Index.unmap_eq_iff_eq_map
Proof state before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : (List.map f xs).Index
j : xs.Index
⊢ i = map f j → unmap f i = j
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : (List.map f xs).Index
j : xs.Index
h : i = map f j
⊢ unmap f i = j
Theorem: List.Index.unmap_eq_iff_eq_map
Proof state before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : (List.map f xs).Index
j : xs.Index
h : i = map f j
⊢ unmap f i = j
Tactic:
rw [h, unmap_map]
Proof state after:
no goals
Theorem: List.Index.val_map
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
⊢ (map f i).val = f i.val
Tactic:
induction i with
| head => rfl
| tail _ ih => exact ih
Proof state after:
no goals
Theorem: List.Index.val_map
Proof state before:
case head
α : Type u_1
β : Type u_2
f : α → β
xs : List α
x✝ : α
xs✝ : List α
⊢ (map f head).val = f head.val
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.val_map
Proof state before:
case tail
α : Type u_1
β : Type u_2
f : α → β
xs xs✝ : List α
x✝ : α
a✝ : xs✝.Index
ih : (map f a✝).val = f a✝.val
⊢ (map f a✝.tail).val = f a✝.tail.val
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.Index.val_unmap
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : (List.map f xs).Index
⊢ i.val = f (unmap f i).val
Tactic:
rw [←map_unmap f i, val_map, unmap_map]
Proof state after:
no goals
Theorem: Nat.bit0_div_two
Proof state before:
x : Nat
⊢ 2 * x / 2 = x
Tactic:
omega
Proof state after:
no goals
Theorem: Nat.bit1_div_two
Proof state before:
x : Nat
⊢ (2 * x + 1) / 2 = x
Tactic:
omega
Proof state after:
no goals
Theorem: Nat.bit0_mod_two
Proof state before:
x : Nat
⊢ 2 * x % 2 = 0
Tactic:
omega
Proof state after:
no goals
Theorem: Nat.bit1_mod_two
Proof state before:
x : Nat
⊢ (2 * x + 1) % 2 = 1
Tactic:
omega
Proof state after:
no goals
Theorem: Nat.zero_bitwise
Proof state before:
f : Bool → Bool → Bool
y : Nat
⊢ bitwise f 0 y = bif f false true then y else 0
Tactic:
rw [bitwise]
Proof state after:
f : Bool → Bool → Bool
y : Nat
⊢ (if 0 = 0 then if f false true = true then y else 0
    else
      if y = 0 then if f true false = true then 0 else 0
      else
        let n' := 0 / 2;
        let m' := y / 2;
        let b₁ := 0 % 2 = 1;
        let b₂ := y % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bif f false true then y else 0
Theorem: Nat.zero_bitwise
Proof state before:
f : Bool → Bool → Bool
y : Nat
⊢ (if 0 = 0 then if f false true = true then y else 0
    else
      if y = 0 then if f true false = true then 0 else 0
      else
        let n' := 0 / 2;
        let m' := y / 2;
        let b₁ := 0 % 2 = 1;
        let b₂ := y % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bif f false true then y else 0
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.bitwise_zero
Proof state before:
f : Bool → Bool → Bool
x : Nat
⊢ bitwise f x 0 = bif f true false then x else 0
Tactic:
rw [bitwise]
Proof state after:
f : Bool → Bool → Bool
x : Nat
⊢ (if x = 0 then if f false true = true then 0 else 0
    else
      if 0 = 0 then if f true false = true then x else 0
      else
        let n' := x / 2;
        let m' := 0 / 2;
        let b₁ := x % 2 = 1;
        let b₂ := 0 % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bif f true false then x else 0
Theorem: Nat.bitwise_zero
Proof state before:
f : Bool → Bool → Bool
x : Nat
⊢ (if x = 0 then if f false true = true then 0 else 0
    else
      if 0 = 0 then if f true false = true then x else 0
      else
        let n' := x / 2;
        let m' := 0 / 2;
        let b₁ := x % 2 = 1;
        let b₂ := 0 % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bif f true false then x else 0
Tactic:
split <;> simp [*]
Proof state after:
no goals
Theorem: Nat.pos_bitwise_pos
Proof state before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
⊢ bitwise f x y = 2 * bitwise f (x / 2) (y / 2) + bif f (decide (x % 2 = 1)) (decide (y % 2 = 1)) then 1 else 0
Tactic:
rw [bitwise]
Proof state after:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
⊢ (if x = 0 then if f false true = true then y else 0
    else
      if y = 0 then if f true false = true then x else 0
      else
        let n' := x / 2;
        let m' := y / 2;
        let b₁ := x % 2 = 1;
        let b₂ := y % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    2 * bitwise f (x / 2) (y / 2) + bif f (decide (x % 2 = 1)) (decide (y % 2 = 1)) then 1 else 0
Theorem: Nat.pos_bitwise_pos
Proof state before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
⊢ (if x = 0 then if f false true = true then y else 0
    else
      if y = 0 then if f true false = true then x else 0
      else
        let n' := x / 2;
        let m' := y / 2;
        let b₁ := x % 2 = 1;
        let b₂ := y % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    2 * bitwise f (x / 2) (y / 2) + bif f (decide (x % 2 = 1)) (decide (y % 2 = 1)) then 1 else 0
Tactic:
simp [hx, hy]
Proof state after:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
⊢ (if f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true then bitwise f (x / 2) (y / 2) + bitwise f (x / 2) (y / 2) + 1
    else bitwise f (x / 2) (y / 2) + bitwise f (x / 2) (y / 2)) =
    2 * bitwise f (x / 2) (y / 2) + bif f (decide (x % 2 = 1)) (decide (y % 2 = 1)) then 1 else 0
Theorem: Nat.pos_bitwise_pos
Proof state before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
⊢ (if f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true then bitwise f (x / 2) (y / 2) + bitwise f (x / 2) (y / 2) + 1
    else bitwise f (x / 2) (y / 2) + bitwise f (x / 2) (y / 2)) =
    2 * bitwise f (x / 2) (y / 2) + bif f (decide (x % 2 = 1)) (decide (y % 2 = 1)) then 1 else 0
Tactic:
split <;> simp [*, Nat.two_mul]
Proof state after:
no goals
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
x y : Nat
⊢ bitwise f x y = bitwise (flip f) y x
Tactic:
if x = 0 then
  simp [*, flip]
else if y = 0 then
  simp [*, flip]
else
  simp [*, pos_bitwise_pos, flip, bitwise_flip f (x / 2) (y / 2)]
Proof state after:
no goals
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
⊢ bitwise f x y = bitwise (flip f) y x
Tactic:
simp [*, flip]
Proof state after:
no goals
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
⊢ bitwise f x y = bitwise (flip f) y x
Tactic:
if y = 0 then
simp [*, flip]
else
simp [*, pos_bitwise_pos, flip, bitwise_flip f (x / 2) (y / 2)]
Proof state after:
no goals
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ bitwise f x y = bitwise (flip f) y x
Tactic:
simp [*, flip]
Proof state after:
no goals
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ bitwise f x y = bitwise (flip f) y x
Tactic:
simp [*, pos_bitwise_pos, flip, bitwise_flip f (x / 2) (y / 2)]
Proof state after:
no goals
Theorem: Nat.bit0_bitwise_bit0
Proof state before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
⊢ bitwise f (2 * x) (2 * y) = 2 * bitwise f x y + bif f false false then 1 else 0
Tactic:
have hx2 : 2 * x ≠ 0 := by intro h; simp [Nat.mul_eq_zero] at h; contradiction
Proof state after:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
hx2 : 2 * x ≠ 0
⊢ bitwise f (2 * x) (2 * y) = 2 * bitwise f x y + bif f false false then 1 else 0
Theorem: Nat.bit0_bitwise_bit0
Proof state before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
hx2 : 2 * x ≠ 0
⊢ bitwise f (2 * x) (2 * y) = 2 * bitwise f x y + bif f false false then 1 else 0
Tactic:
have hy2 : 2 * y ≠ 0 := by intro h; simp [Nat.mul_eq_zero] at h; contradiction
Proof state after:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
hx2 : 2 * x ≠ 0
hy2 : 2 * y ≠ 0
⊢ bitwise f (2 * x) (2 * y) = 2 * bitwise f x y + bif f false false then 1 else 0
Theorem: Nat.bit0_bitwise_bit0
Proof state before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
hx2 : 2 * x ≠ 0
hy2 : 2 * y ≠ 0
⊢ bitwise f (2 * x) (2 * y) = 2 * bitwise f x y + bif f false false then 1 else 0
Tactic:
simp [pos_bitwise_pos _ hx2 hy2]
Proof state after:
no goals
Theorem: Nat.bit0_bitwise_bit0
Proof state before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
⊢ 2 * x ≠ 0
Tactic:
intro h
Proof state after:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
h : 2 * x = 0
⊢ False
Theorem: Nat.bit0_bitwise_bit0
Proof state before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
h : 2 * x = 0
⊢ False
Tactic:
simp [Nat.mul_eq_zero] at h
Proof state after:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
h : x = 0
⊢ False
Theorem: Nat.bit0_bitwise_bit0
Proof state before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
h : x = 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.bit0_bitwise_bit0
Proof state before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
hx2 : 2 * x ≠ 0
⊢ 2 * y ≠ 0
Tactic:
intro h
Proof state after:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
hx2 : 2 * x ≠ 0
h : 2 * y = 0
⊢ False
Theorem: Nat.bit0_bitwise_bit0
Proof state before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
hx2 : 2 * x ≠ 0
h : 2 * y = 0
⊢ False
Tactic:
simp [Nat.mul_eq_zero] at h
Proof state after:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
hx2 : 2 * x ≠ 0
h : y = 0
⊢ False
Theorem: Nat.bit0_bitwise_bit0
Proof state before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
hx2 : 2 * x ≠ 0
h : y = 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.bit1_bitwise_bit0
Proof state before:
f : Bool → Bool → Bool
x y : Nat
⊢ bitwise f (2 * x + 1) (2 * y) = 2 * bitwise f x y + bif f true false then 1 else 0
Tactic:
if y = 0 then
  have : 2 * y = 0 := by simp [*]
  simp [*]; cases (f true false) <;> simp [*]
else
  have hy : 2 * y ≠ 0 := by intro h; simp [Nat.mul_eq_zero] at h; contradiction
  simp [pos_bitwise_pos _ _ hy]
Proof state after:
no goals
Theorem: Nat.bit1_bitwise_bit0
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : y = 0
⊢ bitwise f (2 * x + 1) (2 * y) = 2 * bitwise f x y + bif f true false then 1 else 0
Tactic:
have : 2 * y = 0 := by simp [*]
Proof state after:
f : Bool → Bool → Bool
x y : Nat
h✝ : y = 0
this : 2 * y = 0
⊢ bitwise f (2 * x + 1) (2 * y) = 2 * bitwise f x y + bif f true false then 1 else 0
Theorem: Nat.bit1_bitwise_bit0
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : y = 0
this : 2 * y = 0
⊢ bitwise f (2 * x + 1) (2 * y) = 2 * bitwise f x y + bif f true false then 1 else 0
Tactic:
simp [*]
Proof state after:
f : Bool → Bool → Bool
x y : Nat
h✝ : y = 0
this : 2 * y = 0
⊢ (bif f true false then 2 * x + 1 else 0) = (2 * bif f true false then x else 0) + bif f true false then 1 else 0
Theorem: Nat.bit1_bitwise_bit0
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : y = 0
this : 2 * y = 0
⊢ (bif f true false then 2 * x + 1 else 0) = (2 * bif f true false then x else 0) + bif f true false then 1 else 0
Tactic:
cases (f true false) <;> simp [*]
Proof state after:
no goals
Theorem: Nat.bit1_bitwise_bit0
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : y = 0
⊢ 2 * y = 0
Tactic:
simp [*]
Proof state after:
no goals
Theorem: Nat.bit1_bitwise_bit0
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬y = 0
⊢ bitwise f (2 * x + 1) (2 * y) = 2 * bitwise f x y + bif f true false then 1 else 0
Tactic:
have hy : 2 * y ≠ 0 := by intro h; simp [Nat.mul_eq_zero] at h; contradiction
Proof state after:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬y = 0
hy : 2 * y ≠ 0
⊢ bitwise f (2 * x + 1) (2 * y) = 2 * bitwise f x y + bif f true false then 1 else 0
Theorem: Nat.bit1_bitwise_bit0
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬y = 0
hy : 2 * y ≠ 0
⊢ bitwise f (2 * x + 1) (2 * y) = 2 * bitwise f x y + bif f true false then 1 else 0
Tactic:
simp [pos_bitwise_pos _ _ hy]
Proof state after:
no goals
Theorem: Nat.bit1_bitwise_bit0
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬y = 0
⊢ 2 * y ≠ 0
Tactic:
intro h
Proof state after:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬y = 0
h : 2 * y = 0
⊢ False
Theorem: Nat.bit1_bitwise_bit0
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬y = 0
h : 2 * y = 0
⊢ False
Tactic:
simp [Nat.mul_eq_zero] at h
Proof state after:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬y = 0
h : y = 0
⊢ False
Theorem: Nat.bit1_bitwise_bit0
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬y = 0
h : y = 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.bit0_bitwise_bit1
Proof state before:
f : Bool → Bool → Bool
x y : Nat
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0
Tactic:
if x = 0 then
  have : 2 * x = 0 := by simp [*]
  simp [*]; cases (f false true) <;> simp [*]
else
  have hx : 2 * x ≠ 0 := by intro h; simp [Nat.mul_eq_zero] at h; contradiction
  simp [pos_bitwise_pos _ hx]
Proof state after:
no goals
Theorem: Nat.bit0_bitwise_bit1
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0
Tactic:
have : 2 * x = 0 := by simp [*]
Proof state after:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
this : 2 * x = 0
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0
Theorem: Nat.bit0_bitwise_bit1
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
this : 2 * x = 0
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0
Tactic:
simp [*]
Proof state after:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
this : 2 * x = 0
⊢ (bif f false true then 2 * y + 1 else 0) = (2 * bif f false true then y else 0) + bif f false true then 1 else 0
Theorem: Nat.bit0_bitwise_bit1
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
this : 2 * x = 0
⊢ (bif f false true then 2 * y + 1 else 0) = (2 * bif f false true then y else 0) + bif f false true then 1 else 0
Tactic:
cases (f false true) <;> simp [*]
Proof state after:
no goals
Theorem: Nat.bit0_bitwise_bit1
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
⊢ 2 * x = 0
Tactic:
simp [*]
Proof state after:
no goals
Theorem: Nat.bit0_bitwise_bit1
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0
Tactic:
have hx : 2 * x ≠ 0 := by intro h; simp [Nat.mul_eq_zero] at h; contradiction
Proof state after:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
hx : 2 * x ≠ 0
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0
Theorem: Nat.bit0_bitwise_bit1
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
hx : 2 * x ≠ 0
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0
Tactic:
simp [pos_bitwise_pos _ hx]
Proof state after:
no goals
Theorem: Nat.bit0_bitwise_bit1
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
⊢ 2 * x ≠ 0
Tactic:
intro h
Proof state after:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
h : 2 * x = 0
⊢ False
Theorem: Nat.bit0_bitwise_bit1
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
h : 2 * x = 0
⊢ False
Tactic:
simp [Nat.mul_eq_zero] at h
Proof state after:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
h : x = 0
⊢ False
Theorem: Nat.bit0_bitwise_bit1
Proof state before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
h : x = 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.bit1_bitwise_bit1
Proof state before:
f : Bool → Bool → Bool
x y : Nat
⊢ bitwise f (2 * x + 1) (2 * y + 1) = 2 * bitwise f x y + bif f true true then 1 else 0
Tactic:
simp [pos_bitwise_pos]
Proof state after:
no goals
Theorem: Nat.bit0_and_bit0
Proof state before:
x y : Nat
⊢ 2 * x &&& 2 * y = 2 * (x &&& y)
Tactic:
if x = 0 then
  simp [*, and_def]
else if y = 0 then
  simp [*, and_def]
else
  simp [*, and_def, bit0_bitwise_bit0]
Proof state after:
no goals
Theorem: Nat.bit0_and_bit0
Proof state before:
x y : Nat
h✝ : x = 0
⊢ 2 * x &&& 2 * y = 2 * (x &&& y)
Tactic:
simp [*, and_def]
Proof state after:
no goals
Theorem: Nat.bit0_and_bit0
Proof state before:
x y : Nat
h✝ : ¬x = 0
⊢ 2 * x &&& 2 * y = 2 * (x &&& y)
Tactic:
if y = 0 then
simp [*, and_def]
else
simp [*, and_def, bit0_bitwise_bit0]
Proof state after:
no goals
Theorem: Nat.bit0_and_bit0
Proof state before:
x y : Nat
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ 2 * x &&& 2 * y = 2 * (x &&& y)
Tactic:
simp [*, and_def]
Proof state after:
no goals
Theorem: Nat.bit0_and_bit0
Proof state before:
x y : Nat
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ 2 * x &&& 2 * y = 2 * (x &&& y)
Tactic:
simp [*, and_def, bit0_bitwise_bit0]
Proof state after:
no goals
Theorem: Nat.bit0_and_bit1
Proof state before:
x y : Nat
⊢ 2 * x &&& 2 * y + 1 = 2 * (x &&& y)
Tactic:
simp [and_def, bit0_bitwise_bit1]
Proof state after:
no goals
Theorem: Nat.bit1_and_bit0
Proof state before:
x y : Nat
⊢ 2 * x + 1 &&& 2 * y = 2 * (x &&& y)
Tactic:
simp [and_def, bit1_bitwise_bit0]
Proof state after:
no goals
Theorem: Nat.bit1_and_bit1
Proof state before:
x y : Nat
⊢ 2 * x + 1 &&& 2 * y + 1 = 2 * (x &&& y) + 1
Tactic:
simp [and_def, bit1_bitwise_bit1]
Proof state after:
no goals
Theorem: Nat.and_self
Proof state before:
x : Nat
⊢ x &&& x = x
Tactic:
induction x using Nat.recBit <;> simp [*]
Proof state after:
no goals
Theorem: Nat.and_comm
Proof state before:
x y : Nat
⊢ x &&& y = y &&& x
Tactic:
induction x using Nat.recBit generalizing y <;> cases y using Nat.casesBitOn <;> simp [*]
Proof state after:
no goals
Theorem: Nat.and_assoc
Proof state before:
x y z : Nat
⊢ x &&& y &&& z = x &&& (y &&& z)
Tactic:
induction x using Nat.recBit generalizing y z <;>
  cases y using Nat.casesBitOn <;> cases z using Nat.casesBitOn <;> simp [*]
Proof state after:
no goals
Theorem: Nat.bit0_or_bit0
Proof state before:
x y : Nat
⊢ 2 * x ||| 2 * y = 2 * (x ||| y)
Tactic:
if x = 0 then
  simp [*, or_def]
else if y = 0 then
  simp [*, or_def]
else
  simp [*, or_def, bit0_bitwise_bit0]
Proof state after:
no goals
Theorem: Nat.bit0_or_bit0
Proof state before:
x y : Nat
h✝ : x = 0
⊢ 2 * x ||| 2 * y = 2 * (x ||| y)
Tactic:
simp [*, or_def]
Proof state after:
no goals
Theorem: Nat.bit0_or_bit0
Proof state before:
x y : Nat
h✝ : ¬x = 0
⊢ 2 * x ||| 2 * y = 2 * (x ||| y)
Tactic:
if y = 0 then
simp [*, or_def]
else
simp [*, or_def, bit0_bitwise_bit0]
Proof state after:
no goals
Theorem: Nat.bit0_or_bit0
Proof state before:
x y : Nat
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ 2 * x ||| 2 * y = 2 * (x ||| y)
Tactic:
simp [*, or_def]
Proof state after:
no goals
Theorem: Nat.bit0_or_bit0
Proof state before:
x y : Nat
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ 2 * x ||| 2 * y = 2 * (x ||| y)
Tactic:
simp [*, or_def, bit0_bitwise_bit0]
Proof state after:
no goals
Theorem: Nat.bit0_or_bit1
Proof state before:
x y : Nat
⊢ 2 * x ||| 2 * y + 1 = 2 * (x ||| y) + 1
Tactic:
simp [or_def, bit0_bitwise_bit1]
Proof state after:
no goals
Theorem: Nat.bit1_or_bit0
Proof state before:
x y : Nat
⊢ 2 * x + 1 ||| 2 * y = 2 * (x ||| y) + 1
Tactic:
simp [or_def, bit1_bitwise_bit0]
Proof state after:
no goals
Theorem: Nat.bit1_or_bit1
Proof state before:
x y : Nat
⊢ 2 * x + 1 ||| 2 * y + 1 = 2 * (x ||| y) + 1
Tactic:
simp [or_def, bit1_bitwise_bit1]
Proof state after:
no goals
Theorem: Nat.or_self
Proof state before:
x : Nat
⊢ x ||| x = x
Tactic:
induction x using Nat.recBit <;> simp [*]
Proof state after:
no goals
Theorem: Nat.or_comm
Proof state before:
x y : Nat
⊢ x ||| y = y ||| x
Tactic:
induction x using Nat.recBit generalizing y <;> cases y using Nat.casesBitOn <;> simp [*]
Proof state after:
no goals
Theorem: Nat.or_assoc
Proof state before:
x y z : Nat
⊢ x ||| y ||| z = x ||| (y ||| z)
Tactic:
induction x using Nat.recBit generalizing y z <;>
  cases y using Nat.casesBitOn <;> cases z using Nat.casesBitOn <;> simp [*]
Proof state after:
no goals
Theorem: Nat.and_or_distrib_left
Proof state before:
x y z : Nat
⊢ x &&& (y ||| z) = x &&& y ||| x &&& z
Tactic:
induction x using Nat.recBit generalizing y z <;>
  cases y using Nat.casesBitOn <;> cases z using Nat.casesBitOn <;> simp [*]
Proof state after:
no goals
Theorem: Nat.and_distrib_right
Proof state before:
x y z : Nat
⊢ (x ||| y) &&& z = x &&& z ||| y &&& z
Tactic:
induction z using Nat.recBit generalizing x y <;>
  cases y using Nat.casesBitOn <;> cases x using Nat.casesBitOn <;> simp [*]
Proof state after:
no goals
Theorem: Nat.or_and_distrib_left
Proof state before:
x y z : Nat
⊢ x ||| y &&& z = (x ||| y) &&& (x ||| z)
Tactic:
induction x using Nat.recBit generalizing y z <;>
  cases y using Nat.casesBitOn <;> cases z using Nat.casesBitOn <;> simp [*]
Proof state after:
no goals
Theorem: Nat.or_and_distrib_right
Proof state before:
x y z : Nat
⊢ x &&& y ||| z = (x ||| z) &&& (y ||| z)
Tactic:
induction z using Nat.recBit generalizing x y <;>
  cases y using Nat.casesBitOn <;> cases x using Nat.casesBitOn <;> simp [*]
Proof state after:
no goals
Theorem: Nat.bit0_xor_bit0
Proof state before:
x y : Nat
⊢ 2 * x ^^^ 2 * y = 2 * (x ^^^ y)
Tactic:
if x = 0 then
  simp [*, xor_def]
else if y = 0 then
  simp [*, xor_def]
else
  simp [*, xor_def, bit0_bitwise_bit0]
Proof state after:
no goals