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

Goal state before:
pp: case zero.false
n : ℕ
⊢ (false.toNat != 0) = false

pp: case zero.true
n : ℕ
⊢ (true.toNat != 0) = true

Tactic:
<;>

Goal state after:
case zero.false
n : ℕ
⊢ (false.toNat != 0) = false

case zero.true
n : ℕ
⊢ (true.toNat != 0) = true
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case succ.nil
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ [].tail.getI i = [].getI (i + 1)

pp: case succ.cons
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
head✝ : Bool
tail✝ : List Bool
⊢ (head✝ :: tail✝).tail.getI i = (head✝ :: tail✝).getI (i + 1)

Tactic:
<;>

Goal state after:
case succ.nil
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ [].tail.getI i = [].getI (i + 1)

case succ.cons
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
head✝ : Bool
tail✝ : List Bool
⊢ (head✝ :: tail✝).tail.getI i = (head✝ :: tail✝).getI (i + 1)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case false
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ bit false 0 ≠ 0 → false = true

pp: case true
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ bit true 0 ≠ 0 → true = true

Tactic:
<;>

Goal state after:
case false
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ bit false 0 ≠ 0 → false = true

case true
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ bit true 0 ≠ 0 → true = true
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case e'_2
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
i : ℕ
⊢ n.testBit i = (bit b n).testBit (i + 1)

pp: case e'_3
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
i : ℕ
⊢ m.testBit i = (bit b' m).testBit (i + 1)

Tactic:
<;>

Goal state after:
case e'_2
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
i : ℕ
⊢ n.testBit i = (bit b n).testBit (i + 1)

case e'_3
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
i : ℕ
⊢ m.testBit i = (bit b' m).testBit (i + 1)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case e'_2
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
⊢ n.testBit j = (bit b n).testBit j.succ

pp: case e'_3
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
⊢ m.testBit j = (bit b' m).testBit j.succ

Tactic:
<;>

Goal state after:
case e'_2
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
⊢ n.testBit j = (bit b n).testBit j.succ

case e'_3
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
⊢ m.testBit j = (bit b' m).testBit j.succ
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n m i : ℕ
hn : n.testBit i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j
⊢ n < m

Tactic:
induction n using Nat.binaryRec generalizing i m with
  | zero =>
    rw [Nat.pos_iff_ne_zero]
    rintro rfl
    simp at hm
  | bit b n hn' =>
    induction m using Nat.binaryRec generalizing i with
    | zero => exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))
    | bit b' m hm' =>
      by_cases hi : i = 0
      · subst hi
        simp only [testBit_bit_zero] at hn hm
        have : n = m :=
          eq_of_testBit_eq fun i => by convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1
          <;> rw [testBit_bit_succ]
        rw [hn, hm, this, bit_false, bit_true]
        exact Nat.lt_succ_self _
      · obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
        simp only [testBit_bit_succ] at hn hm
        have := hn' _ hn hm fun j hj => by
          convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
        exact bit_lt_bit b b' this

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

Goal state before:
pp: case inl
n i : ℕ
⊢ (n &&& 2 ^ i).testBit i = ((n.testBit i).toNat * 2 ^ i).testBit i

pp: case inr
n i j : ℕ
hij : i ≠ j
⊢ (n &&& 2 ^ i).testBit j = ((n.testBit i).toNat * 2 ^ i).testBit j

Tactic:
<;>

Goal state after:
case inl
n i : ℕ
⊢ (n &&& 2 ^ i).testBit i = ((n.testBit i).toNat * 2 ^ i).testBit i

case inr
n i j : ℕ
hij : i ≠ j
⊢ (n &&& 2 ^ i).testBit j = ((n.testBit i).toNat * 2 ^ i).testBit j
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.pair.some.none
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
val✝ : ℕ
⊢ ((some val✝).bind fun a ↦ Option.none.bind fun y ↦ some (Nat.pair a y)) =
    (Option.map Nat.pair (some val✝)).bind fun a ↦ Option.map a Option.none

pp: case succ.pair.some.some
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
val✝¹ val✝ : ℕ
⊢ ((some val✝¹).bind fun a ↦ (some val✝).bind fun y ↦ some (Nat.pair a y)) =
    (Option.map Nat.pair (some val✝¹)).bind fun a ↦ Option.map a (some val✝)

Tactic:
<;>

Goal state after:
case succ.pair.some.none
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
val✝ : ℕ
⊢ ((some val✝).bind fun a ↦ Option.none.bind fun y ↦ some (Nat.pair a y)) =
    (Option.map Nat.pair (some val✝)).bind fun a ↦ Option.map a Option.none

case succ.pair.some.some
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.pair cg)) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.pair cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.pair cg)
lg : encode cg < encode (cf.pair cg)
val✝¹ val✝ : ℕ
⊢ ((some val✝¹).bind fun a ↦ (some val✝).bind fun y ↦ some (Nat.pair a y)) =
    (Option.map Nat.pair (some val✝¹)).bind fun a ↦ Option.map a (some val✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one
⊢ 1 + one = one.succ

pp: case bit1
a✝ : PosNum
⊢ 1 + a✝.bit1 = a✝.bit1.succ

pp: case bit0
a✝ : PosNum
⊢ 1 + a✝.bit0 = a✝.bit0.succ

Tactic:
<;>

Goal state after:
case one
⊢ 1 + one = one.succ

case bit1
a✝ : PosNum
⊢ 1 + a✝.bit1 = a✝.bit1.succ

case bit0
a✝ : PosNum
⊢ 1 + a✝.bit0 = a✝.bit0.succ
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one
⊢ one + 1 = one.succ

pp: case bit1
a✝ : PosNum
⊢ a✝.bit1 + 1 = a✝.bit1.succ

pp: case bit0
a✝ : PosNum
⊢ a✝.bit0 + 1 = a✝.bit0.succ

Tactic:
<;>

Goal state after:
case one
⊢ one + 1 = one.succ

case bit1
a✝ : PosNum
⊢ a✝.bit1 + 1 = a✝.bit1.succ

case bit0
a✝ : PosNum
⊢ a✝.bit0 + 1 = a✝.bit0.succ
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case false
⊢ sectionΓ'Bool (inclusionBoolΓ' false) = false

pp: case true
⊢ sectionΓ'Bool (inclusionBoolΓ' true) = true

Tactic:
<;>

Goal state after:
case false
⊢ sectionΓ'Bool (inclusionBoolΓ' false) = false

case true
⊢ sectionΓ'Bool (inclusionBoolΓ' true) = true
Module: Mathlib.Computability.Encoding

Goal state before:
pp: b : Bool
⊢ sectionΓ'Bool (inclusionBoolΓ' b) = b

Tactic:
by
  cases b <;> rfl

Goal state after:
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case zero
⊢ decodeNum (encodeNum Num.zero) = Num.zero

pp: case pos
n : PosNum
⊢ decodeNum (encodeNum (Num.pos n)) = Num.pos n

Tactic:
<;>

Goal state after:
case zero
⊢ decodeNum (encodeNum Num.zero) = Num.zero

case pos
n : PosNum
⊢ decodeNum (encodeNum (Num.pos n)) = Num.pos n
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: x n m : ℕ
h : x < 2 ^ n
⊢ x <<< m < 2 ^ (n + m)

Tactic:
simp only [Nat.pow_add, shiftLeft_eq, Nat.mul_lt_mul_right (Nat.two_pow_pos _), h]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one
⊢ ∀ (n : PosNum), (one.cmp n).swap = n.cmp one

pp: case bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ ∀ (n : PosNum), (m.bit1.cmp n).swap = n.cmp m.bit1

pp: case bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ ∀ (n : PosNum), (m.bit0.cmp n).swap = n.cmp m.bit0

Tactic:
<;>

Goal state after:
case one
⊢ ∀ (n : PosNum), (one.cmp n).swap = n.cmp one

case bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ ∀ (n : PosNum), (m.bit1.cmp n).swap = n.cmp m.bit1

case bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ ∀ (n : PosNum), (m.bit0.cmp n).swap = n.cmp m.bit0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one
n : PosNum
⊢ (one.cmp n).swap = n.cmp one

pp: case bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n).swap = n.cmp m.bit1

pp: case bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n).swap = n.cmp m.bit0

Tactic:
<;>

Goal state after:
case one
n : PosNum
⊢ (one.cmp n).swap = n.cmp one

case bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n).swap = n.cmp m.bit1

case bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n).swap = n.cmp m.bit0
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case cons.none
α : Type u_1
β : Type u_2
f : α → β
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
⊢ (map (Option.map f) (none :: tl)).reduceOption = map f (none :: tl).reduceOption

pp: case cons.some
α : Type u_1
β : Type u_2
f : α → β
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
val✝ : α
⊢ (map (Option.map f) (some val✝ :: tl)).reduceOption = map f (some val✝ :: tl).reduceOption

Tactic:
<;>

Goal state after:
case cons.none
α : Type u_1
β : Type u_2
f : α → β
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
⊢ (map (Option.map f) (none :: tl)).reduceOption = map f (none :: tl).reduceOption

case cons.some
α : Type u_1
β : Type u_2
f : α → β
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
val✝ : α
⊢ (map (Option.map f) (some val✝ :: tl)).reduceOption = map f (some val✝ :: tl).reduceOption
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one.one
⊢ (one.cmp one).swap = one.cmp one

pp: case one.bit1
n : PosNum
⊢ (one.cmp n.bit1).swap = n.bit1.cmp one

pp: case one.bit0
n : PosNum
⊢ (one.cmp n.bit0).swap = n.bit0.cmp one

pp: case bit1.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ (m.bit1.cmp one).swap = one.cmp m.bit1

pp: case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n.bit1).swap = n.bit1.cmp m.bit1

pp: case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n.bit0).swap = n.bit0.cmp m.bit1

pp: case bit0.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ (m.bit0.cmp one).swap = one.cmp m.bit0

pp: case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n.bit1).swap = n.bit1.cmp m.bit0

pp: case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n.bit0).swap = n.bit0.cmp m.bit0

Tactic:
<;>

Goal state after:
case one.one
⊢ (one.cmp one).swap = one.cmp one

case one.bit1
n : PosNum
⊢ (one.cmp n.bit1).swap = n.bit1.cmp one

case one.bit0
n : PosNum
⊢ (one.cmp n.bit0).swap = n.bit0.cmp one

case bit1.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ (m.bit1.cmp one).swap = one.cmp m.bit1

case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n.bit1).swap = n.bit1.cmp m.bit1

case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n.bit0).swap = n.bit0.cmp m.bit1

case bit0.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ (m.bit0.cmp one).swap = one.cmp m.bit0

case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n.bit1).swap = n.bit1.cmp m.bit0

case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n.bit0).swap = n.bit0.cmp m.bit0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case one.one
⊢ Ordering.eq.swap = Ordering.eq

pp: case one.bit1
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

pp: case one.bit0
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

pp: case bit1.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt

pp: case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m

pp: case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.lt Ordering.gt

pp: case bit0.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt

pp: case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.gt Ordering.gt

pp: case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m

Tactic:
<;>

Goal state after:
case one.one
⊢ Ordering.eq.swap = Ordering.eq

case one.bit1
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

case one.bit0
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

case bit1.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt

case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m

case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.lt Ordering.gt

case bit0.one
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt

case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.gt Ordering.gt

case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
obtain ⟨l₁, _, h, hl₁, hl₂⟩ := h

Goal state after:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
hl₂ : w✝.reduceOption = [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m

pp: case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.lt Ordering.gt

pp: case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.gt Ordering.gt

pp: case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m

Tactic:
<;>

Goal state after:
case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m

case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.lt Ordering.gt

case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.gt Ordering.gt

case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (m.cmp n).swap Ordering.lt Ordering.lt Ordering.gt

pp: case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (m.cmp n).swap Ordering.lt Ordering.gt Ordering.gt

Tactic:
<;>

Goal state after:
case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (m.cmp n).swap Ordering.lt Ordering.lt Ordering.gt

case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (m.cmp n).swap Ordering.lt Ordering.gt Ordering.gt
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mpr.inl
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x

pp: case mpr.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x

Tactic:
<;>

Goal state after:
case mpr.inl
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x

case mpr.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x