mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case hp
m n i j : ℕ
⊢ i.bodd = (j.bodd ^^ i.bodd ^^ j.bodd)

pp: case hn
m n i j : ℕ
⊢ (!i.bodd) = (j.bodd ^^ (j.bodd ^^ i.bodd ^^ Nat.bodd 1))

Tactic:
<;>

Goal state after:
case hp
m n i j : ℕ
⊢ i.bodd = (j.bodd ^^ i.bodd ^^ j.bodd)

case hn
m n i j : ℕ
⊢ (!i.bodd) = (j.bodd ^^ (j.bodd ^^ i.bodd ^^ Nat.bodd 1))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case hp.false
m n i j : ℕ
⊢ false = (j.bodd ^^ false ^^ j.bodd)

pp: case hp.true
m n i j : ℕ
⊢ true = (j.bodd ^^ true ^^ j.bodd)

pp: case hn.false
m n i j : ℕ
⊢ (!false) = (j.bodd ^^ (j.bodd ^^ false ^^ Nat.bodd 1))

pp: case hn.true
m n i j : ℕ
⊢ (!true) = (j.bodd ^^ (j.bodd ^^ true ^^ Nat.bodd 1))

Tactic:
<;>

Goal state after:
case hp.false
m n i j : ℕ
⊢ false = (j.bodd ^^ false ^^ j.bodd)

case hp.true
m n i j : ℕ
⊢ true = (j.bodd ^^ true ^^ j.bodd)

case hn.false
m n i j : ℕ
⊢ (!false) = (j.bodd ^^ (j.bodd ^^ false ^^ Nat.bodd 1))

case hn.true
m n i j : ℕ
⊢ (!true) = (j.bodd ^^ (j.bodd ^^ true ^^ Nat.bodd 1))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case zero
⊢ (negOfNat 0).bodd = Nat.bodd 0

pp: case succ
n✝ : ℕ
⊢ (negOfNat (n✝ + 1)).bodd = (n✝ + 1).bodd

Tactic:
<;>

Goal state after:
case zero
⊢ (negOfNat 0).bodd = Nat.bodd 0

case succ
n✝ : ℕ
⊢ (negOfNat (n✝ + 1)).bodd = (n✝ + 1).bodd
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
a✝ : ℕ
⊢ (-ofNat a✝).bodd = (ofNat a✝).bodd

pp: case negSucc
a✝ : ℕ
⊢ (- -[a✝+1]).bodd = -[a✝+1].bodd

Tactic:
<;>

Goal state after:
case ofNat
a✝ : ℕ
⊢ (-ofNat a✝).bodd = (ofNat a✝).bodd

case negSucc
a✝ : ℕ
⊢ (- -[a✝+1]).bodd = -[a✝+1].bodd
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
a✝ : ℕ
⊢ a✝.bodd = (ofNat a✝).bodd

pp: case negSucc
a✝ : ℕ
⊢ (↑(a✝ + 1)).bodd = -[a✝+1].bodd

Tactic:
<;>

Goal state after:
case ofNat
a✝ : ℕ
⊢ a✝.bodd = (ofNat a✝).bodd

case negSucc
a✝ : ℕ
⊢ (↑(a✝ + 1)).bodd = -[a✝+1].bodd
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
n : ℤ
m : ℕ
⊢ (ofNat m + n).bodd = ((ofNat m).bodd ^^ n.bodd)

pp: case negSucc
n : ℤ
m : ℕ
⊢ (-[m+1] + n).bodd = (-[m+1].bodd ^^ n.bodd)

Tactic:
<;>

Goal state after:
case ofNat
n : ℤ
m : ℕ
⊢ (ofNat m + n).bodd = ((ofNat m).bodd ^^ n.bodd)

case negSucc
n : ℤ
m : ℕ
⊢ (-[m+1] + n).bodd = (-[m+1].bodd ^^ n.bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ (ofNat m + ofNat n).bodd = ((ofNat m).bodd ^^ (ofNat n).bodd)

pp: case ofNat.negSucc
m n : ℕ
⊢ (ofNat m + -[n+1]).bodd = ((ofNat m).bodd ^^ -[n+1].bodd)

pp: case negSucc.ofNat
m n : ℕ
⊢ (-[m+1] + ofNat n).bodd = (-[m+1].bodd ^^ (ofNat n).bodd)

pp: case negSucc.negSucc
m n : ℕ
⊢ (-[m+1] + -[n+1]).bodd = (-[m+1].bodd ^^ -[n+1].bodd)

Tactic:
<;>

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ (ofNat m + ofNat n).bodd = ((ofNat m).bodd ^^ (ofNat n).bodd)

case ofNat.negSucc
m n : ℕ
⊢ (ofNat m + -[n+1]).bodd = ((ofNat m).bodd ^^ -[n+1].bodd)

case negSucc.ofNat
m n : ℕ
⊢ (-[m+1] + ofNat n).bodd = (-[m+1].bodd ^^ (ofNat n).bodd)

case negSucc.negSucc
m n : ℕ
⊢ (-[m+1] + -[n+1]).bodd = (-[m+1].bodd ^^ -[n+1].bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ (↑(m + n)).bodd = ((↑m).bodd ^^ (↑n).bodd)

pp: case ofNat.negSucc
m n : ℕ
⊢ (m.bodd ^^ n.succ.bodd) = ((↑m).bodd ^^ -[n+1].bodd)

pp: case negSucc.ofNat
m n : ℕ
⊢ (n.bodd ^^ m.succ.bodd) = (-[m+1].bodd ^^ (↑n).bodd)

pp: case negSucc.negSucc
m n : ℕ
⊢ -[(m + n).succ+1].bodd = (-[m+1].bodd ^^ -[n+1].bodd)

Tactic:
<;>

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ (↑(m + n)).bodd = ((↑m).bodd ^^ (↑n).bodd)

case ofNat.negSucc
m n : ℕ
⊢ (m.bodd ^^ n.succ.bodd) = ((↑m).bodd ^^ -[n+1].bodd)

case negSucc.ofNat
m n : ℕ
⊢ (n.bodd ^^ m.succ.bodd) = (-[m+1].bodd ^^ (↑n).bodd)

case negSucc.negSucc
m n : ℕ
⊢ -[(m + n).succ+1].bodd = (-[m+1].bodd ^^ -[n+1].bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
n : ℤ
m : ℕ
⊢ (ofNat m * n).bodd = ((ofNat m).bodd && n.bodd)

pp: case negSucc
n : ℤ
m : ℕ
⊢ (-[m+1] * n).bodd = (-[m+1].bodd && n.bodd)

Tactic:
<;>

Goal state after:
case ofNat
n : ℤ
m : ℕ
⊢ (ofNat m * n).bodd = ((ofNat m).bodd && n.bodd)

case negSucc
n : ℤ
m : ℕ
⊢ (-[m+1] * n).bodd = (-[m+1].bodd && n.bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ (ofNat m * ofNat n).bodd = ((ofNat m).bodd && (ofNat n).bodd)

pp: case ofNat.negSucc
m n : ℕ
⊢ (ofNat m * -[n+1]).bodd = ((ofNat m).bodd && -[n+1].bodd)

pp: case negSucc.ofNat
m n : ℕ
⊢ (-[m+1] * ofNat n).bodd = (-[m+1].bodd && (ofNat n).bodd)

pp: case negSucc.negSucc
m n : ℕ
⊢ (-[m+1] * -[n+1]).bodd = (-[m+1].bodd && -[n+1].bodd)

Tactic:
<;>

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ (ofNat m * ofNat n).bodd = ((ofNat m).bodd && (ofNat n).bodd)

case ofNat.negSucc
m n : ℕ
⊢ (ofNat m * -[n+1]).bodd = ((ofNat m).bodd && -[n+1].bodd)

case negSucc.ofNat
m n : ℕ
⊢ (-[m+1] * ofNat n).bodd = (-[m+1].bodd && (ofNat n).bodd)

case negSucc.negSucc
m n : ℕ
⊢ (-[m+1] * -[n+1]).bodd = (-[m+1].bodd && -[n+1].bodd)
Module: Mathlib.Data.Holor

Goal state before:
pp: case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0

Tactic:
· intro (hid' : Subtype.mk i _ ∉ Finset.attach (Finset.range d))
    exfalso
    exact absurd (Finset.mem_attach _ _) hid'

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ (↑(m * n)).bodd = ((↑m).bodd && (↑n).bodd)

pp: case ofNat.negSucc
m n : ℕ
⊢ (-↑(m * n.succ)).bodd = ((↑m).bodd && -[n+1].bodd)

pp: case negSucc.ofNat
m n : ℕ
⊢ (-↑(m.succ * n)).bodd = (-[m+1].bodd && (↑n).bodd)

pp: case negSucc.negSucc
m n : ℕ
⊢ (↑(m.succ * n.succ)).bodd = (-[m+1].bodd && -[n+1].bodd)

Tactic:
<;>

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ (↑(m * n)).bodd = ((↑m).bodd && (↑n).bodd)

case ofNat.negSucc
m n : ℕ
⊢ (-↑(m * n.succ)).bodd = ((↑m).bodd && -[n+1].bodd)

case negSucc.ofNat
m n : ℕ
⊢ (-↑(m.succ * n)).bodd = (-[m+1].bodd && (↑n).bodd)

case negSucc.negSucc
m n : ℕ
⊢ (↑(m.succ * n.succ)).bodd = (-[m+1].bodd && -[n+1].bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false
n : ℕ
⊢ (bif false then 1 else 0) = ↑(bif false then 1 else 0)

pp: case true
n : ℕ
⊢ (bif true then 1 else 0) = ↑(bif true then 1 else 0)

Tactic:
<;>

Goal state after:
case false
n : ℕ
⊢ (bif false then 1 else 0) = ↑(bif false then 1 else 0)

case true
n : ℕ
⊢ (bif true then 1 else 0) = ↑(bif true then 1 else 0)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false
n : ℕ
⊢ (bif !false then 1 else 0) + 2 * -[n+1].div2 = -[false.toNat + 2 * n.div2+1]

pp: case true
n : ℕ
⊢ (bif !true then 1 else 0) + 2 * -[n+1].div2 = -[true.toNat + 2 * n.div2+1]

Tactic:
<;>

Goal state after:
case false
n : ℕ
⊢ (bif !false then 1 else 0) + 2 * -[n+1].div2 = -[false.toNat + 2 * n.div2+1]

case true
n : ℕ
⊢ (bif !true then 1 else 0) + 2 * -[n+1].div2 = -[true.toNat + 2 * n.div2+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false
n : ℕ
⊢ (2 * ↑n + bif false then 1 else 0) = ↑(2 * n + false.toNat)

pp: case true
n : ℕ
⊢ (2 * ↑n + bif true then 1 else 0) = ↑(2 * n + true.toNat)

Tactic:
<;>

Goal state after:
case false
n : ℕ
⊢ (2 * ↑n + bif false then 1 else 0) = ↑(2 * n + false.toNat)

case true
n : ℕ
⊢ (2 * ↑n + bif true then 1 else 0) = ↑(2 * n + true.toNat)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false
n : ℕ
⊢ (2 * -[n+1] + bif false then 1 else 0) = -[2 * n + (!false).toNat+1]

pp: case true
n : ℕ
⊢ (2 * -[n+1] + bif true then 1 else 0) = -[2 * n + (!true).toNat+1]

Tactic:
<;>

Goal state after:
case false
n : ℕ
⊢ (2 * -[n+1] + bif false then 1 else 0) = -[2 * n + (!false).toNat+1]

case true
n : ℕ
⊢ (2 * -[n+1] + bif true then 1 else 0) = -[2 * n + (!true).toNat+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false
n : ℤ
⊢ (2 * n + bif false then 1 else 0).bodd = false

pp: case true
n : ℤ
⊢ (2 * n + bif true then 1 else 0).bodd = true

Tactic:
<;>

Goal state after:
case false
n : ℤ
⊢ (2 * n + bif false then 1 else 0).bodd = false

case true
n : ℤ
⊢ (2 * n + bif true then 1 else 0).bodd = true
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false.false
n : ℤ
⊢ (2 * n + bif false then 1 else 0).bodd = false

pp: case false.true
n : ℤ
⊢ (2 * n + bif false then 1 else 0).bodd = false

pp: case true.false
n : ℤ
⊢ (2 * n + bif true then 1 else 0).bodd = true

pp: case true.true
n : ℤ
⊢ (2 * n + bif true then 1 else 0).bodd = true

Tactic:
<;>

Goal state after:
case false.false
n : ℤ
⊢ (2 * n + bif false then 1 else 0).bodd = false

case false.true
n : ℤ
⊢ (2 * n + bif false then 1 else 0).bodd = false

case true.false
n : ℤ
⊢ (2 * n + bif true then 1 else 0).bodd = true

case true.true
n : ℤ
⊢ (2 * n + bif true then 1 else 0).bodd = true
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false
m n : ℕ
⊢ (!(Nat.bit (!false) n).testBit m.succ) = !n.testBit m

pp: case true
m n : ℕ
⊢ (!(Nat.bit (!true) n).testBit m.succ) = !n.testBit m

Tactic:
<;>

Goal state after:
case false
m n : ℕ
⊢ (!(Nat.bit (!false) n).testBit m.succ) = !n.testBit m

case true
m n : ℕ
⊢ (!(Nat.bit (!true) n).testBit m.succ) = !n.testBit m
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
n : ℤ
m : ℕ
⊢ bitwise or (ofNat m) n = (ofNat m).lor n

pp: case negSucc
n : ℤ
m : ℕ
⊢ bitwise or -[m+1] n = -[m+1].lor n

Tactic:
<;>

Goal state after:
case ofNat
n : ℤ
m : ℕ
⊢ bitwise or (ofNat m) n = (ofNat m).lor n

case negSucc
n : ℤ
m : ℕ
⊢ bitwise or -[m+1] n = -[m+1].lor n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = (ofNat m).lor (ofNat n)

pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]

pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)

pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]

Tactic:
<;>

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = (ofNat m).lor (ofNat n)

case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]

pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)

pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]

Tactic:
<;>

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc.e_f
m n : ℕ
⊢ (fun y x ↦ !(x || !y)) = fun a b ↦ a && !b

Tactic:
funext x y

Goal state after:
case ofNat.negSucc.e_f
m n : ℕ
x y : Bool
⊢ (!(y || !x)) = (x && !y)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc.e_f.false
m n : ℕ
y : Bool
⊢ (!(y || !false)) = (false && !y)

pp: case ofNat.negSucc.e_f.true
m n : ℕ
y : Bool
⊢ (!(y || !true)) = (true && !y)

Tactic:
<;>

Goal state after:
case ofNat.negSucc.e_f.false
m n : ℕ
y : Bool
⊢ (!(y || !false)) = (false && !y)

case ofNat.negSucc.e_f.true
m n : ℕ
y : Bool
⊢ (!(y || !true)) = (true && !y)
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: case true
n : ℤ
⊢ ofNat 0 = 0

pp: case true
n : ℤ
⊢ 1 < 2

Tactic:
<;>

Goal state after:
case true
n : ℤ
⊢ ofNat 0 = 0

case true
n : ℤ
⊢ 1 < 2
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc.e_f.false.false
m n : ℕ
⊢ (!(false || !false)) = (false && !false)

pp: case ofNat.negSucc.e_f.false.true
m n : ℕ
⊢ (!(true || !false)) = (false && !true)

pp: case ofNat.negSucc.e_f.true.false
m n : ℕ
⊢ (!(false || !true)) = (true && !false)

pp: case ofNat.negSucc.e_f.true.true
m n : ℕ
⊢ (!(true || !true)) = (true && !true)

Tactic:
<;>

Goal state after:
case ofNat.negSucc.e_f.false.false
m n : ℕ
⊢ (!(false || !false)) = (false && !false)

case ofNat.negSucc.e_f.false.true
m n : ℕ
⊢ (!(true || !false)) = (false && !true)

case ofNat.negSucc.e_f.true.false
m n : ℕ
⊢ (!(false || !true)) = (true && !false)

case ofNat.negSucc.e_f.true.true
m n : ℕ
⊢ (!(true || !true)) = (true && !true)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
n : ℤ
m : ℕ
⊢ bitwise and (ofNat m) n = (ofNat m).land n

pp: case negSucc
n : ℤ
m : ℕ
⊢ bitwise and -[m+1] n = -[m+1].land n

Tactic:
<;>

Goal state after:
case ofNat
n : ℤ
m : ℕ
⊢ bitwise and (ofNat m) n = (ofNat m).land n

case negSucc
n : ℤ
m : ℕ
⊢ bitwise and -[m+1] n = -[m+1].land n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise and (ofNat m) (ofNat n) = (ofNat m).land (ofNat n)

pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = (ofNat m).land -[n+1]

pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)

pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]

Tactic:
<;>

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ bitwise and (ofNat m) (ofNat n) = (ofNat m).land (ofNat n)

case ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = (ofNat m).land -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)

pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]

Tactic:
<;>

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat.e_f
m n : ℕ
⊢ (fun y x ↦ !x && y) = fun a b ↦ a && !b

Tactic:
funext x y

Goal state after:
case negSucc.ofNat.e_f
m n : ℕ
x y : Bool
⊢ (!y && x) = (x && !y)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat.e_f.false
m n : ℕ
y : Bool
⊢ (!y && false) = (false && !y)

pp: case negSucc.ofNat.e_f.true
m n : ℕ
y : Bool
⊢ (!y && true) = (true && !y)

Tactic:
<;>

Goal state after:
case negSucc.ofNat.e_f.false
m n : ℕ
y : Bool
⊢ (!y && false) = (false && !y)

case negSucc.ofNat.e_f.true
m n : ℕ
y : Bool
⊢ (!y && true) = (true && !y)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat.e_f.false.false
m n : ℕ
⊢ (!false && false) = (false && !false)

pp: case negSucc.ofNat.e_f.false.true
m n : ℕ
⊢ (!true && false) = (false && !true)

pp: case negSucc.ofNat.e_f.true.false
m n : ℕ
⊢ (!false && true) = (true && !false)

pp: case negSucc.ofNat.e_f.true.true
m n : ℕ
⊢ (!true && true) = (true && !true)

Tactic:
<;>

Goal state after:
case negSucc.ofNat.e_f.false.false
m n : ℕ
⊢ (!false && false) = (false && !false)

case negSucc.ofNat.e_f.false.true
m n : ℕ
⊢ (!true && false) = (false && !true)

case negSucc.ofNat.e_f.true.false
m n : ℕ
⊢ (!false && true) = (true && !false)

case negSucc.ofNat.e_f.true.true
m n : ℕ
⊢ (!true && true) = (true && !true)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
n : ℤ
m : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) n = (ofNat m).ldiff n

pp: case negSucc
n : ℤ
m : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] n = -[m+1].ldiff n

Tactic:
<;>

Goal state after:
case ofNat
n : ℤ
m : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) n = (ofNat m).ldiff n

case negSucc
n : ℤ
m : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] n = -[m+1].ldiff n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) (ofNat n) = (ofNat m).ldiff (ofNat n)

pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]

pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)

pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]

Tactic:
<;>

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) (ofNat n) = (ofNat m).ldiff (ofNat n)

case ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]

pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)

pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]

Tactic:
<;>

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc.e_f
m n : ℕ
⊢ (fun y x ↦ !x && !!y) = fun a b ↦ a && !b

Tactic:
funext x y

Goal state after:
case negSucc.negSucc.e_f
m n : ℕ
x y : Bool
⊢ (!y && !!x) = (x && !y)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc.e_f.false
m n : ℕ
y : Bool
⊢ (!y && !!false) = (false && !y)

pp: case negSucc.negSucc.e_f.true
m n : ℕ
y : Bool
⊢ (!y && !!true) = (true && !y)

Tactic:
<;>

Goal state after:
case negSucc.negSucc.e_f.false
m n : ℕ
y : Bool
⊢ (!y && !!false) = (false && !y)

case negSucc.negSucc.e_f.true
m n : ℕ
y : Bool
⊢ (!y && !!true) = (true && !y)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc.e_f.false.false
m n : ℕ
⊢ (!false && !!false) = (false && !false)

pp: case negSucc.negSucc.e_f.false.true
m n : ℕ
⊢ (!true && !!false) = (false && !true)

pp: case negSucc.negSucc.e_f.true.false
m n : ℕ
⊢ (!false && !!true) = (true && !false)

pp: case negSucc.negSucc.e_f.true.true
m n : ℕ
⊢ (!true && !!true) = (true && !true)

Tactic:
<;>

Goal state after:
case negSucc.negSucc.e_f.false.false
m n : ℕ
⊢ (!false && !!false) = (false && !false)

case negSucc.negSucc.e_f.false.true
m n : ℕ
⊢ (!true && !!false) = (false && !true)

case negSucc.negSucc.e_f.true.false
m n : ℕ
⊢ (!false && !!true) = (true && !false)

case negSucc.negSucc.e_f.true.true
m n : ℕ
⊢ (!true && !!true) = (true && !true)
Module: Mathlib.Data.Int.NatPrime

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ (k * k).natAbs

Tactic:
← natCast_dvd,

Goal state after:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ ↑p ∣ k * k
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
n : ℤ
m : ℕ
⊢ bitwise xor (ofNat m) n = (ofNat m).xor n

pp: case negSucc
n : ℤ
m : ℕ
⊢ bitwise xor -[m+1] n = -[m+1].xor n

Tactic:
<;>

Goal state after:
case ofNat
n : ℤ
m : ℕ
⊢ bitwise xor (ofNat m) n = (ofNat m).xor n

case negSucc
n : ℤ
m : ℕ
⊢ bitwise xor -[m+1] n = -[m+1].xor n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = (ofNat m).xor (ofNat n)

pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]

pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)

pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]

Tactic:
<;>

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = (ofNat m).xor (ofNat n)

case ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]

pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)

pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]

Tactic:
<;>

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(x ^^ !y)) m n = Nat.bitwise xor m n

pp: case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x ^^ y)) m n = Nat.bitwise xor m n

pp: case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x ^^ !y) m n) = ↑(Nat.bitwise xor m n)

Tactic:
<;>

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(x ^^ !y)) m n = Nat.bitwise xor m n

case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x ^^ y)) m n = Nat.bitwise xor m n

case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x ^^ !y) m n) = ↑(Nat.bitwise xor m n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b n) = bit (f a b) (bitwise f (ofNat m) n)

pp: case negSucc
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b n) = bit (f a b) (bitwise f -[m+1] n)

Tactic:
<;>

Goal state after:
case ofNat
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b n) = bit (f a b) (bitwise f (ofNat m) n)

case negSucc
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b n) = bit (f a b) (bitwise f -[m+1] n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b (ofNat n)) = bit (f a b) (bitwise f (ofNat m) (ofNat n))

pp: case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b -[n+1]) = bit (f a b) (bitwise f (ofNat m) -[n+1])

pp: case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b (ofNat n)) = bit (f a b) (bitwise f -[m+1] (ofNat n))

pp: case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b -[n+1]) = bit (f a b) (bitwise f -[m+1] -[n+1])

Tactic:
<;>

Goal state after:
case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b (ofNat n)) = bit (f a b) (bitwise f (ofNat m) (ofNat n))

case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b -[n+1]) = bit (f a b) (bitwise f (ofNat m) -[n+1])

case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b (ofNat n)) = bit (f a b) (bitwise f -[m+1] (ofNat n))

case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b -[n+1]) = bit (f a b) (bitwise f -[m+1] -[n+1])