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

Goal state before:
pp: case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f false false = true
⊢ (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) m n+1] else ↑(Nat.bitwise f m n))

pp: case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f false false = true
⊢ (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) m n+1] else ↑(Nat.bitwise f m n))

Tactic:
<;>

Goal state after:
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f false false = true
⊢ (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) m n+1] else ↑(Nat.bitwise f m n))

case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f false false = true
⊢ (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) m n+1] else ↑(Nat.bitwise f m n))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f false true = true
⊢ (bif f false true then -[Nat.bitwise (fun x y ↦ !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise (fun x y ↦ !f x !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) m n))

pp: case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f false true = true
⊢ (bif f false true then -[Nat.bitwise (fun x y ↦ !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise (fun x y ↦ !f x !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) m n))

Tactic:
<;>

Goal state after:
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f false true = true
⊢ (bif f false true then -[Nat.bitwise (fun x y ↦ !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise (fun x y ↦ !f x !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) m n))

case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f false true = true
⊢ (bif f false true then -[Nat.bitwise (fun x y ↦ !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise (fun x y ↦ !f x !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) m n))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f true false = true
⊢ (bif f true false then -[Nat.bitwise (fun x y ↦ !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise (fun x y ↦ !f (!x) y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) y) m n))

pp: case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f true false = true
⊢ (bif f true false then -[Nat.bitwise (fun x y ↦ !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise (fun x y ↦ !f (!x) y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) y) m n))

Tactic:
<;>

Goal state after:
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f true false = true
⊢ (bif f true false then -[Nat.bitwise (fun x y ↦ !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise (fun x y ↦ !f (!x) y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) y) m n))

case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f true false = true
⊢ (bif f true false then -[Nat.bitwise (fun x y ↦ !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise (fun x y ↦ !f (!x) y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) y) m n))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f true true = true
⊢ (bif f true true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) m n))

pp: case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f true true = true
⊢ (bif f true true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) m n))

Tactic:
<;>

Goal state after:
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f true true = true
⊢ (bif f true true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) m n))

case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f true true = true
⊢ (bif f true true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) m n))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
f : Bool → Bool → Bool
n : ℤ
k a✝ : ℕ
⊢ (bitwise f (ofNat a✝) n).testBit k = f ((ofNat a✝).testBit k) (n.testBit k)

pp: case negSucc
f : Bool → Bool → Bool
n : ℤ
k a✝ : ℕ
⊢ (bitwise f -[a✝+1] n).testBit k = f (-[a✝+1].testBit k) (n.testBit k)

Tactic:
<;>

Goal state after:
case ofNat
f : Bool → Bool → Bool
n : ℤ
k a✝ : ℕ
⊢ (bitwise f (ofNat a✝) n).testBit k = f ((ofNat a✝).testBit k) (n.testBit k)

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

Goal state before:
pp: case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f (ofNat a✝¹) (ofNat a✝)).testBit k = f ((ofNat a✝¹).testBit k) ((ofNat a✝).testBit k)

pp: case ofNat.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f (ofNat a✝¹) -[a✝+1]).testBit k = f ((ofNat a✝¹).testBit k) (-[a✝+1].testBit k)

pp: case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f -[a✝¹+1] (ofNat a✝)).testBit k = f (-[a✝¹+1].testBit k) ((ofNat a✝).testBit k)

pp: case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f -[a✝¹+1] -[a✝+1]).testBit k = f (-[a✝¹+1].testBit k) (-[a✝+1].testBit k)

Tactic:
<;>

Goal state after:
case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f (ofNat a✝¹) (ofNat a✝)).testBit k = f ((ofNat a✝¹).testBit k) ((ofNat a✝).testBit k)

case ofNat.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f (ofNat a✝¹) -[a✝+1]).testBit k = f ((ofNat a✝¹).testBit k) (-[a✝+1].testBit k)

case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f -[a✝¹+1] (ofNat a✝)).testBit k = f (-[a✝¹+1].testBit k) ((ofNat a✝).testBit k)

case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f -[a✝¹+1] -[a✝+1]).testBit k = f (-[a✝¹+1].testBit k) (-[a✝+1].testBit k)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f false false = true
⊢ (match bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise f a✝¹ a✝), k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) (a✝.testBit k)

pp: case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f false false = true
⊢ (match bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise f a✝¹ a✝), k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) (a✝.testBit k)

Tactic:
<;>

Goal state after:
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f false false = true
⊢ (match bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise f a✝¹ a✝), k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) (a✝.testBit k)

case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f false false = true
⊢ (match bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise f a✝¹ a✝), k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) (a✝.testBit k)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f false true = true
⊢ (match
      bif f false !false then -[Nat.bitwise (fun x y ↦ !f x !y) a✝¹ a✝+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) !a✝.testBit k

pp: case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f false true = true
⊢ (match
      bif f false !false then -[Nat.bitwise (fun x y ↦ !f x !y) a✝¹ a✝+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) !a✝.testBit k

Tactic:
<;>

Goal state after:
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f false true = true
⊢ (match
      bif f false !false then -[Nat.bitwise (fun x y ↦ !f x !y) a✝¹ a✝+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) !a✝.testBit k

case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f false true = true
⊢ (match
      bif f false !false then -[Nat.bitwise (fun x y ↦ !f x !y) a✝¹ a✝+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) !a✝.testBit k
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f true false = true
⊢ (match
      bif f (!false) false then -[Nat.bitwise (fun x y ↦ !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) (a✝.testBit k)

pp: case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f true false = true
⊢ (match
      bif f (!false) false then -[Nat.bitwise (fun x y ↦ !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) (a✝.testBit k)

Tactic:
<;>

Goal state after:
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f true false = true
⊢ (match
      bif f (!false) false then -[Nat.bitwise (fun x y ↦ !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) (a✝.testBit k)

case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f true false = true
⊢ (match
      bif f (!false) false then -[Nat.bitwise (fun x y ↦ !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) (a✝.testBit k)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f true true = true
⊢ (match
      bif f (!false) !false then -[Nat.bitwise (fun x y ↦ !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) !a✝.testBit k

pp: case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f true true = true
⊢ (match
      bif f (!false) !false then -[Nat.bitwise (fun x y ↦ !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) !a✝.testBit k

Tactic:
<;>

Goal state after:
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f true true = true
⊢ (match
      bif f (!false) !false then -[Nat.bitwise (fun x y ↦ !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) !a✝.testBit k

case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f true true = true
⊢ (match
      bif f (!false) !false then -[Nat.bitwise (fun x y ↦ !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) !a✝.testBit k
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case zero
m : ℕ
⊢ ↑m >>> ↑0 = ↑(m >>> 0)

pp: case succ
m n✝ : ℕ
⊢ ↑m >>> ↑(n✝ + 1) = ↑(m >>> (n✝ + 1))

Tactic:
<;>

Goal state after:
case zero
m : ℕ
⊢ ↑m >>> ↑0 = ↑(m >>> 0)

case succ
m n✝ : ℕ
⊢ ↑m >>> ↑(n✝ + 1) = ↑(m >>> (n✝ + 1))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case zero
m : ℕ
⊢ -[m+1] >>> ↑0 = -[m >>> 0+1]

pp: case succ
m n✝ : ℕ
⊢ -[m+1] >>> ↑(n✝ + 1) = -[m >>> (n✝ + 1)+1]

Tactic:
<;>

Goal state after:
case zero
m : ℕ
⊢ -[m+1] >>> ↑0 = -[m >>> 0+1]

case succ
m n✝ : ℕ
⊢ -[m+1] >>> ↑(n✝ + 1) = -[m >>> (n✝ + 1)+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
n a✝ : ℕ
⊢ (match ofNat a✝, ↑n with
    | ofNat m, ofNat n => ↑(Nat.shiftLeft' false m n)
    | ofNat m, -[n+1] => ↑(m.shiftRight n.succ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    (ofNat a✝).mul ↑(Nat.pow 2 n)

pp: case negSucc
n a✝ : ℕ
⊢ (match -[a✝+1], ↑n with
    | ofNat m, ofNat n => ↑(Nat.shiftLeft' false m n)
    | ofNat m, -[n+1] => ↑(m.shiftRight n.succ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    -[a✝+1].mul ↑(Nat.pow 2 n)

Tactic:
<;>

Goal state after:
case ofNat
n a✝ : ℕ
⊢ (match ofNat a✝, ↑n with
    | ofNat m, ofNat n => ↑(Nat.shiftLeft' false m n)
    | ofNat m, -[n+1] => ↑(m.shiftRight n.succ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    (ofNat a✝).mul ↑(Nat.pow 2 n)

case negSucc
n a✝ : ℕ
⊢ (match -[a✝+1], ↑n with
    | ofNat m, ofNat n => ↑(Nat.shiftLeft' false m n)
    | ofNat m, -[n+1] => ↑(m.shiftRight n.succ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    -[a✝+1].mul ↑(Nat.pow 2 n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
n a✝ : ℕ
⊢ ofNat a✝ >>> ↑n = ofNat a✝ >>> n

pp: case negSucc
n a✝ : ℕ
⊢ -[a✝+1] >>> ↑n = -[a✝+1] >>> n

Tactic:
<;>

Goal state after:
case ofNat
n a✝ : ℕ
⊢ ofNat a✝ >>> ↑n = ofNat a✝ >>> n

case negSucc
n a✝ : ℕ
⊢ -[a✝+1] >>> ↑n = -[a✝+1] >>> n
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
hp : p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

pp: case neg
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
hp : ¬p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
hp : p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

case neg
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
hp : ¬p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = xs ↔ ∀ (x : α), x ∈ xs → p x = true
hp : p x = true
⊢ takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

pp: case neg
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = xs ↔ ∀ (x : α), x ∈ xs → p x = true
hp : ¬p x = true
⊢ takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = xs ↔ ∀ (x : α), x ∈ xs → p x = true
hp : p x = true
⊢ takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

case neg
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = xs ↔ ∀ (x : α), x ∈ xs → p x = true
hp : ¬p x = true
⊢ takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
Module: Mathlib.Data.List.Fold

Goal state before:
pp: case nil
α : Type u_1
l : List α
⊢ foldl (flip cons) [] [] = [].reverse

pp: case cons
α : Type u_1
l : List α
head✝ : α
tail✝ : List α
tail_ih✝ : foldl (flip cons) [] tail✝ = tail✝.reverse
⊢ foldl (flip cons) [] (head✝ :: tail✝) = (head✝ :: tail✝).reverse

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
l : List α
⊢ foldl (flip cons) [] [] = [].reverse

case cons
α : Type u_1
l : List α
head✝ : α
tail✝ : List α
tail_ih✝ : foldl (flip cons) [] tail✝ = tail✝.reverse
⊢ foldl (flip cons) [] (head✝ :: tail✝) = (head✝ :: tail✝).reverse
Module: Mathlib.Data.List.Fold

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
v : β → α → β
hv : RightCommutative v
a : α
b : β
⊢ foldl v (v b a) [] = v (foldl v b []) a

pp: case cons
α : Type u_1
β : Type u_2
v : β → α → β
hv : RightCommutative v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {a : α} {b : β}, foldl v (v b a) tail✝ = v (foldl v b tail✝) a
a : α
b : β
⊢ foldl v (v b a) (head✝ :: tail✝) = v (foldl v b (head✝ :: tail✝)) a

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
v : β → α → β
hv : RightCommutative v
a : α
b : β
⊢ foldl v (v b a) [] = v (foldl v b []) a

case cons
α : Type u_1
β : Type u_2
v : β → α → β
hv : RightCommutative v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {a : α} {b : β}, foldl v (v b a) tail✝ = v (foldl v b tail✝) a
a : α
b : β
⊢ foldl v (v b a) (head✝ :: tail✝) = v (foldl v b (head✝ :: tail✝)) a
Module: Mathlib.Data.List.Fold

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
f : α → β → β
hf : LeftCommutative f
a : α
b : β
⊢ f a (foldr f b []) = foldr f (f a b) []

pp: case cons
α : Type u_1
β : Type u_2
f : α → β → β
hf : LeftCommutative f
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {a : α} {b : β}, f a (foldr f b tail✝) = foldr f (f a b) tail✝
a : α
b : β
⊢ f a (foldr f b (head✝ :: tail✝)) = foldr f (f a b) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
f : α → β → β
hf : LeftCommutative f
a : α
b : β
⊢ f a (foldr f b []) = foldr f (f a b) []

case cons
α : Type u_1
β : Type u_2
f : α → β → β
hf : LeftCommutative f
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {a : α} {b : β}, f a (foldr f b tail✝) = foldr f (f a b) tail✝
a : α
b : β
⊢ f a (foldr f b (head✝ :: tail✝)) = foldr f (f a b) (head✝ :: tail✝)
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get ⟨0, hl⟩) = true
hp : p x = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get ⟨0, hl⟩) = true

pp: case neg
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get ⟨0, hl⟩) = true
hp : ¬p x = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get ⟨0, hl⟩) = true

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get ⟨0, hl⟩) = true
hp : p x = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get ⟨0, hl⟩) = true

case neg
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = [] ↔ ∀ (hl : 0 < xs.length), ¬p (xs.get ⟨0, hl⟩) = true
hp : ¬p x = true
⊢ takeWhile p (x :: xs) = [] ↔ ∀ (hl : 0 < (x :: xs).length), ¬p ((x :: xs).get ⟨0, hl⟩) = true
Module: Mathlib.Data.List.Fold

Goal state before:
pp: case nil
α : Type u_1
l : List α
f : α → α → α
ha : Std.Associative f
b a : α
⊢ f (foldl f a []) b = f a (foldr f b [])

pp: case cons
α : Type u_1
l : List α
f : α → α → α
ha : Std.Associative f
b head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {a : α}, f (foldl f a tail✝) b = f a (foldr f b tail✝)
a : α
⊢ f (foldl f a (head✝ :: tail✝)) b = f a (foldr f b (head✝ :: tail✝))

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
l : List α
f : α → α → α
ha : Std.Associative f
b a : α
⊢ f (foldl f a []) b = f a (foldr f b [])

case cons
α : Type u_1
l : List α
f : α → α → α
ha : Std.Associative f
b head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {a : α}, f (foldl f a tail✝) b = f a (foldr f b tail✝)
a : α
⊢ f (foldl f a (head✝ :: tail✝)) b = f a (foldr f b (head✝ :: tail✝))
Module: Mathlib.Data.List.Fold

Goal state before:
pp: case nil
α : Type u_1
l : List α
a : α
f : α → α → α
inst✝ : Std.Associative f
ha : ∀ (x : α), f a x = f x a
⊢ foldl f a [] = foldr f a []

pp: case cons
α : Type u_1
l : List α
a : α
f : α → α → α
inst✝ : Std.Associative f
ha : ∀ (x : α), f a x = f x a
head✝ : α
tail✝ : List α
tail_ih✝ : foldl f a tail✝ = foldr f a tail✝
⊢ foldl f a (head✝ :: tail✝) = foldr f a (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
l : List α
a : α
f : α → α → α
inst✝ : Std.Associative f
ha : ∀ (x : α), f a x = f x a
⊢ foldl f a [] = foldr f a []

case cons
α : Type u_1
l : List α
a : α
f : α → α → α
inst✝ : Std.Associative f
ha : ∀ (x : α), f a x = f x a
head✝ : α
tail✝ : List α
tail_ih✝ : foldl f a tail✝ = foldr f a tail✝
⊢ foldl f a (head✝ :: tail✝) = foldr f a (head✝ :: tail✝)
Module: Mathlib.Data.List.Fold

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
f : α → β → β
inst✝ : LeftCommutative f
b : β
⊢ foldl (flip f) b [] = foldr f b []

pp: case cons
α : Type u_1
β : Type u_2
f : α → β → β
inst✝ : LeftCommutative f
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {b : β}, foldl (flip f) b tail✝ = foldr f b tail✝
b : β
⊢ foldl (flip f) b (head✝ :: tail✝) = foldr f b (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
f : α → β → β
inst✝ : LeftCommutative f
b : β
⊢ foldl (flip f) b [] = foldr f b []

case cons
α : Type u_1
β : Type u_2
f : α → β → β
inst✝ : LeftCommutative f
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {b : β}, foldl (flip f) b tail✝ = foldr f b tail✝
b : β
⊢ foldl (flip f) b (head✝ :: tail✝) = foldr f b (head✝ :: tail✝)
Module: Mathlib.Data.List.Fold

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
v : β → α → β
inst✝ : RightCommutative v
b : β
⊢ foldr (flip v) b [] = foldl v b []

pp: case cons
α : Type u_1
β : Type u_2
v : β → α → β
inst✝ : RightCommutative v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {b : β}, foldr (flip v) b tail✝ = foldl v b tail✝
b : β
⊢ foldr (flip v) b (head✝ :: tail✝) = foldl v b (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
v : β → α → β
inst✝ : RightCommutative v
b : β
⊢ foldr (flip v) b [] = foldl v b []

case cons
α : Type u_1
β : Type u_2
v : β → α → β
inst✝ : RightCommutative v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {b : β}, foldr (flip v) b tail✝ = foldl v b tail✝
b : β
⊢ foldr (flip v) b (head✝ :: tail✝) = foldl v b (head✝ :: tail✝)