internlm/Lean-Github huggingface dataset:
Theorem: QueueData.nonEmptyPull
Proof state before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
⊢ t = xs
Tactic:
rw [← p3, ← p4] at p1
Proof state after:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1✝ : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p1 : t ++ List.reverse [] = xs ∧ h = x ∧ { init := t, tail := [] } = { init := t, tail := [] }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1✝.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
⊢ t = xs
Theorem: QueueData.nonEmptyPull
Proof state before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1✝ : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p1 : t ++ List.reverse [] = xs ∧ h = x ∧ { init := t, tail := [] } = { init := t, tail := [] }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1✝.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
⊢ t = xs
Tactic:
simp at p1
Proof state after:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1✝ : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1✝.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
p1 : t = xs ∧ h = x
⊢ t = xs
Theorem: QueueData.nonEmptyPull
Proof state before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1✝ : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1✝.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
p1 : t = xs ∧ h = x
⊢ t = xs
Tactic:
simp [p1]
Proof state after:
no goals
Theorem: QueueData.nonEmptyPull
Proof state before:
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ h :: t ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match h :: t with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)
Tactic:
simp
Proof state after:
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ h = x ∧ t ++ List.reverse tail = xs ↔ ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt
Theorem: QueueData.nonEmptyPull
Proof state before:
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ h = x ∧ t ++ List.reverse tail = xs ↔ ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ h = x ∧ t ++ List.reverse tail = xs → ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt

case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt) →
    h = x ∧ t ++ List.reverse tail = xs
Theorem: QueueData.nonEmptyPull
Proof state before:
case mp
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ h = x ∧ t ++ List.reverse tail = xs → ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt

case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt) →
    h = x ∧ t ++ List.reverse tail = xs
Tactic:
. intro pp
  let qt: QueueData α := ⟨ t, q.tail ⟩
  exists qt
  simp
  rw [pp.left, pp.right]    
  simp
Proof state after:
case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt) →
    h = x ∧ t ++ List.reverse tail = xs
Theorem: QueueData.nonEmptyPull
Proof state before:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
⊢ h = x ∧ t ++ List.reverse tail = xs
Tactic:
rw [p2, ← p1]
Proof state after:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
⊢ x = x ∧ t ++ List.reverse tail = init ++ List.reverse tail
Theorem: QueueData.nonEmptyPull
Proof state before:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
⊢ x = x ∧ t ++ List.reverse tail = init ++ List.reverse tail
Tactic:
simp
Proof state after:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
⊢ t ++ List.reverse tail = qti ++ List.reverse qtt
Theorem: QueueData.nonEmptyPull
Proof state before:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
p4 : (fun x => init) { init := t, tail := tail } = (fun x => init) { init := qti, tail := qtt } :=
  congrArg (fun x => init) p3
p5 : (fun x => tail) { init := t, tail := tail } = (fun x => tail) { init := qti, tail := qtt } :=
  congrArg (fun x => tail) p3
⊢ t ++ List.reverse tail = qti ++ List.reverse qtt
Tactic:
simp at p4 p5
Proof state after:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
p4 : t = qti := congrArg (fun x => init) p3
p5 : tail = qtt := congrArg (fun x => tail) p3
⊢ t ++ List.reverse tail = qti ++ List.reverse qtt
Theorem: QueueData.nonEmptyPull
Proof state before:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
p4 : t = qti := congrArg (fun x => init) p3
p5 : tail = qtt := congrArg (fun x => tail) p3
⊢ t ++ List.reverse tail = qti ++ List.reverse qtt
Tactic:
rw [p4, p5]
Proof state after:
no goals
Theorem: Dir.leftRight
Proof state before:
d : Dir
⊢ rechtsaf (linksaf d) = d
Tactic:
cases d <;> simp [linksaf, rechtsaf]
Proof state after:
no goals
Theorem: Dir.rightLeft
Proof state before:
d : Dir
⊢ linksaf (rechtsaf d) = d
Tactic:
cases d <;> simp [linksaf, rechtsaf]
Proof state after:
no goals
Theorem: Dir.backBack
Proof state before:
d : Dir
⊢ back (back d) = d
Tactic:
cases d <;> simp [back]
Proof state after:
no goals
Theorem: Array.append_size
Proof state before:
α : Type u_1
n m : Nat
arr₁ arr₂ : Array α
h1 : size arr₁ = n
h2 : size arr₂ = m
⊢ size (arr₁ ++ arr₂) = n + m
Tactic:
unfold Array.size at *
Proof state after:
α : Type u_1
n m : Nat
arr₁ arr₂ : Array α
h1 : List.length arr₁.data = n
h2 : List.length arr₂.data = m
⊢ List.length (arr₁ ++ arr₂).data = n + m
Theorem: Array.append_size
Proof state before:
α : Type u_1
n m : Nat
arr₁ arr₂ : Array α
h1 : List.length arr₁.data = n
h2 : List.length arr₂.data = m
⊢ List.length (arr₁ ++ arr₂).data = n + m
Tactic:
simp [h1, h2]
Proof state after:
no goals
Theorem: Int.modToNat_le
Proof state before:
a : Int
n : Nat
⊢ modToNat a (succ n) < succ n
Tactic:
cases a with
| ofNat x => simp only [modToNat_ofNat, x.mod_lt (n.succ_pos)]
| negSucc x =>
  let y := x % n.succ
  have : n.succ - y - 1 ≤ n := by
    have : n.succ - y - 1 = n - y := n.add_sub_add_right 1 y
    rw [this]
    exact n.sub_le y
  exact Nat.lt_succ_of_le this
Proof state after:
no goals
Theorem: Int.modToNat_le
Proof state before:
case ofNat
n x : Nat
⊢ modToNat (ofNat x) (succ n) < succ n
Tactic:
simp only [modToNat_ofNat, x.mod_lt (n.succ_pos)]
Proof state after:
no goals
Theorem: Int.modToNat_le
Proof state before:
case negSucc
n x : Nat
⊢ modToNat -[x+1] (succ n) < succ n
Tactic:
let y := x % n.succ
Proof state after:
case negSucc
n x : Nat
y : Nat := x % succ n
⊢ modToNat -[x+1] (succ n) < succ n
Theorem: Int.modToNat_le
Proof state before:
case negSucc
n x : Nat
y : Nat := x % succ n
⊢ modToNat -[x+1] (succ n) < succ n
Tactic:
have : n.succ - y - 1 ≤ n := by
  have : n.succ - y - 1 = n - y := n.add_sub_add_right 1 y
  rw [this]
  exact n.sub_le y
Proof state after:
case negSucc
n x : Nat
y : Nat := x % succ n
this : succ n - y - 1 ≤ n
⊢ modToNat -[x+1] (succ n) < succ n
Theorem: Int.modToNat_le
Proof state before:
case negSucc
n x : Nat
y : Nat := x % succ n
this : succ n - y - 1 ≤ n
⊢ modToNat -[x+1] (succ n) < succ n
Tactic:
exact Nat.lt_succ_of_le this
Proof state after:
no goals
Theorem: Int.modToNat_le
Proof state before:
n x : Nat
y : Nat := x % succ n
⊢ succ n - y - 1 ≤ n
Tactic:
have : n.succ - y - 1 = n - y := n.add_sub_add_right 1 y
Proof state after:
n x : Nat
y : Nat := x % succ n
this : succ n - y - 1 = n - y
⊢ succ n - y - 1 ≤ n
Theorem: Int.modToNat_le
Proof state before:
n x : Nat
y : Nat := x % succ n
this : succ n - y - 1 = n - y
⊢ succ n - y - 1 ≤ n
Tactic:
rw [this]
Proof state after:
n x : Nat
y : Nat := x % succ n
this : succ n - y - 1 = n - y
⊢ n - y ≤ n
Theorem: Int.modToNat_le
Proof state before:
n x : Nat
y : Nat := x % succ n
this : succ n - y - 1 = n - y
⊢ n - y ≤ n
Tactic:
exact n.sub_le y
Proof state after:
no goals
Theorem: Nat.div2_lt
Proof state before:
n : Nat
h : n ≠ 0
⊢ n / 2 < n
Tactic:
match n with
| 1   => decide
| 2   => decide
| 3   => decide
| n+4 =>
  rw [div_eq, if_pos]
  refine succ_lt_succ (Nat.lt_trans ?_ (lt_succ_self _))
  exact @div2_lt (n + 2) (by simp_arith)
  simp_arith
Proof state after:
no goals
Theorem: Nat.div2_lt
Proof state before:
n : Nat
h : 1 ≠ 0
⊢ 1 / 2 < 1
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.div2_lt
Proof state before:
n : Nat
h : 2 ≠ 0
⊢ 2 / 2 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.div2_lt
Proof state before:
n : Nat
h : 3 ≠ 0
⊢ 3 / 2 < 3
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.div2_lt
Proof state before:
n✝ n : Nat
h : n + 4 ≠ 0
⊢ (n + 4) / 2 < n + 4
Tactic:
rw [div_eq, if_pos]
Proof state after:
n✝ n : Nat
h : n + 4 ≠ 0
⊢ (n + 4 - 2) / 2 + 1 < n + 4

case hc
n✝ n : Nat
h : n + 4 ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n + 4
Theorem: Nat.div2_lt
Proof state before:
n✝ n : Nat
h : n + 4 ≠ 0
⊢ (n + 4 - 2) / 2 + 1 < n + 4

case hc
n✝ n : Nat
h : n + 4 ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n + 4
Tactic:
refine succ_lt_succ (Nat.lt_trans ?_ (lt_succ_self _))
Proof state after:
n✝ n : Nat
h : n + 4 ≠ 0
⊢ (n + 4 - 2) / 2 < n + 2

case hc
n✝ n : Nat
h : n + 4 ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n + 4
Theorem: Nat.div2_lt
Proof state before:
n✝ n : Nat
h : n + 4 ≠ 0
⊢ (n + 4 - 2) / 2 < n + 2

case hc
n✝ n : Nat
h : n + 4 ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n + 4
Tactic:
exact @div2_lt (n + 2) (by simp_arith)
Proof state after:
case hc
n✝ n : Nat
h : n + 4 ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n + 4
Theorem: Nat.div2_lt
Proof state before:
case hc
n✝ n : Nat
h : n + 4 ≠ 0
⊢ 0 < 2 ∧ 2 ≤ n + 4
Tactic:
simp_arith
Proof state after:
no goals
Theorem: Nat.div2_lt
Proof state before:
n✝ n : Nat
h : n + 4 ≠ 0
⊢ n + 2 ≠ 0
Tactic:
simp_arith
Proof state after:
no goals
Theorem: ByteArray.sliceL.aux_size
Proof state before:
acc : Array UInt8
n : Nat
bs : List UInt8
⊢ Array.size (aux acc n bs) = Array.size acc + n
Tactic:
induction bs generalizing acc n
Proof state after:
case nil
acc : Array UInt8
n : Nat
⊢ Array.size (aux acc n []) = Array.size acc + n

case cons
head✝ : UInt8
tail✝ : List UInt8
tail_ih✝ : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n : Nat
⊢ Array.size (aux acc n (head✝ :: tail✝)) = Array.size acc + n
Theorem: ByteArray.sliceL.aux_size
Proof state before:
case cons
head✝ : UInt8
tail✝ : List UInt8
tail_ih✝ : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n : Nat
⊢ Array.size (aux acc n (head✝ :: tail✝)) = Array.size acc + n
Tactic:
rename_i ih
Proof state after:
case cons
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n : Nat
⊢ Array.size (aux acc n (head✝ :: tail✝)) = Array.size acc + n
Theorem: ByteArray.sliceL.aux_size
Proof state before:
case cons
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n : Nat
⊢ Array.size (aux acc n (head✝ :: tail✝)) = Array.size acc + n
Tactic:
cases n
Proof state after:
case cons.zero
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
⊢ Array.size (aux acc Nat.zero (head✝ :: tail✝)) = Array.size acc + Nat.zero

case cons.succ
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n✝ : Nat
⊢ Array.size (aux acc (Nat.succ n✝) (head✝ :: tail✝)) = Array.size acc + Nat.succ n✝
Theorem: ByteArray.sliceL.aux_size
Proof state before:
case cons.succ
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n✝ : Nat
⊢ Array.size (aux acc (Nat.succ n✝) (head✝ :: tail✝)) = Array.size acc + Nat.succ n✝
Tactic:
simp [sliceL.aux, ByteArray.size, ih]
Proof state after:
case cons.succ
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n✝ : Nat
⊢ Array.size acc + 1 + n✝ = Array.size acc + Nat.succ n✝
Theorem: ByteArray.sliceL.aux_size
Proof state before:
case cons.succ
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n✝ : Nat
⊢ Array.size acc + 1 + n✝ = Array.size acc + Nat.succ n✝
Tactic:
rw [Nat.succ_eq_add_one, Nat.add_assoc, Nat.add_comm 1 _]
Proof state after:
no goals
Theorem: ByteArray.sliceL.aux_size
Proof state before:
case nil
acc : Array UInt8
n : Nat
⊢ Array.size (aux acc n []) = Array.size acc + n
Tactic:
induction n <;> simp [sliceL.aux, ByteArray.size, Array.size]
Proof state after:
no goals
Theorem: ByteArray.sliceL.aux_size
Proof state before:
case cons.zero
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
⊢ Array.size (aux acc Nat.zero (head✝ :: tail✝)) = Array.size acc + Nat.zero
Tactic:
simp [sliceL.aux]
Proof state after:
no goals
Theorem: ByteArray.slice_size
Proof state before:
bytes : ByteArray
i n : Nat
⊢ size (slice bytes i n) = n
Tactic:
simp [slice, sliceL, sliceL.aux, sliceL.aux_size, ByteArray.size]
Proof state after:
no goals
Theorem: ByteArray.set_size
Proof state before:
arr : ByteArray
i : Fin (size arr)
u : UInt8
⊢ size (set arr i u) = size arr
Tactic:
simp [size, set]
Proof state after:
no goals
Theorem: ByteArray.set!_size
Proof state before:
arr : ByteArray
i : Nat
u : UInt8
⊢ size (set! arr i u) = size arr
Tactic:
simp [size, set!, Array.set!, Array.setD]
Proof state after:
arr : ByteArray
i : Nat
u : UInt8
⊢ Array.size (if h : i < Array.size arr.data then Array.set arr.data { val := i, isLt := h } u else arr.data) =
    Array.size arr.data
Theorem: ByteArray.set!_size
Proof state before:
arr : ByteArray
i : Nat
u : UInt8
⊢ Array.size (if h : i < Array.size arr.data then Array.set arr.data { val := i, isLt := h } u else arr.data) =
    Array.size arr.data
Tactic:
by_cases h : i < arr.data.size <;> simp [h]
Proof state after:
no goals
Theorem: Abstract.Matrix.lt_succ
Proof state before:
A : Type ?u.204
inst✝³ : Inhabited A
inst✝² : Add A
inst✝¹ : Mul A
inst✝ : OfNat A 0
n : Nat
⊢ n < n + 1
Tactic:
rw [add_one]
Proof state after:
A : Type ?u.204
inst✝³ : Inhabited A
inst✝² : Add A
inst✝¹ : Mul A
inst✝ : OfNat A 0
n : Nat
⊢ n < succ n
Theorem: Abstract.Matrix.lt_succ
Proof state before:
A : Type ?u.204
inst✝³ : Inhabited A
inst✝² : Add A
inst✝¹ : Mul A
inst✝ : OfNat A 0
n : Nat
⊢ n < succ n
Tactic:
apply lt_succ_of_le
Proof state after:
case a
A : Type ?u.204
inst✝³ : Inhabited A
inst✝² : Add A
inst✝¹ : Mul A
inst✝ : OfNat A 0
n : Nat
⊢ n ≤ n
Theorem: Abstract.Matrix.lt_succ
Proof state before:
case a
A : Type ?u.204
inst✝³ : Inhabited A
inst✝² : Add A
inst✝¹ : Mul A
inst✝ : OfNat A 0
n : Nat
⊢ n ≤ n
Tactic:
apply Nat.le_refl
Proof state after:
no goals
Theorem: UInt16.toByteArray_size_2
Proof state before:
n : UInt16
⊢ ByteArray.size (toByteArray n) = 2
Tactic:
simp [ByteArray.size, Array.size, List.length]
Proof state after:
no goals
Theorem: UInt32.toByteArray_size_4
Proof state before:
n : UInt32
⊢ ByteArray.size (toByteArray n) = 4
Tactic:
simp [ByteArray.size, Array.size, List.length]
Proof state after:
no goals
Theorem: UInt64.toByteArray_size_8
Proof state before:
n : UInt64
⊢ ByteArray.size (toByteArray n) = 8
Tactic:
simp [ByteArray.size, Array.size, List.length]
Proof state after:
no goals
Theorem: Cached.eq_of_subsingleton
Proof state before:
α : Sort u_1
inst✝ : Subsingleton α
a b : α
⊢ (a = b) = True
Tactic:
simp [Subsingleton.allEq a b]
Proof state after:
no goals
Theorem: cong
Proof state before:
x y : ℤ
f : ℤ → ℤ
⊢ x = y → f x = f y
Tactic:
simp_all
Proof state after:
no goals
Theorem: replace
Proof state before:
⊢ "a".replace "a" "b" = "b"
Tactic:
admit
Proof state after:
no goals
Theorem: assoc
Proof state before:
f : Bool → Bool → Bool
p q r : Bool
⊢ (f p (f q r) == f (f p q) r) = true
Tactic:
admit
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.sumBounds₁
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
⊢ a < b → c < d → a + c < b + d
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c < d
⊢ a + c < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₁
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c < d
⊢ a + c < b + d
Tactic:
have r₁: a + c < a + d := add_lt_add_left h₂ a
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c < d
r₁ : a + c < a + d
⊢ a + c < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₁
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c < d
r₁ : a + c < a + d
⊢ a + c < b + d
Tactic:
have r₂: a + d < b + d := add_lt_add_right h₁ d
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c < d
r₁ : a + c < a + d
r₂ : a + d < b + d
⊢ a + c < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₁
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c < d
r₁ : a + c < a + d
r₂ : a + d < b + d
⊢ a + c < b + d
Tactic:
exact lt_trans r₁ r₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.sumBounds₂
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
⊢ a < b → c ≤ d → a + c < b + d
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
⊢ a + c < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₂
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
⊢ a + c < b + d
Tactic:
have r₁: a + c ≤ a + d := add_le_add_left h₂ a
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
⊢ a + c < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₂
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
⊢ a + c < b + d
Tactic:
have r₂: a + d < b + d := add_lt_add_right h₁ d
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
r₂ : a + d < b + d
⊢ a + c < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₂
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
r₂ : a + d < b + d
⊢ a + c < b + d
Tactic:
exact lt_of_le_of_lt r₁ r₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.sumBounds₃
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
⊢ a < b → c = d → a + c < b + d
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c = d
⊢ a + c < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₃
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c = d
⊢ a + c < b + d
Tactic:
rewrite [h₂]
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c = d
⊢ a + d < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₃
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c = d
⊢ a + d < b + d
Tactic:
exact add_lt_add_right h₁ d
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.sumBounds₄
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
⊢ a ≤ b → c < d → a + c < b + d
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c < d
⊢ a + c < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₄
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c < d
⊢ a + c < b + d
Tactic:
have r₁ : a + c < a + d := add_lt_add_left h₂ a
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c < d
r₁ : a + c < a + d
⊢ a + c < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₄
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c < d
r₁ : a + c < a + d
⊢ a + c < b + d
Tactic:
have r₂ : a + d ≤ b + d := add_le_add_right h₁ d
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c < d
r₁ : a + c < a + d
r₂ : a + d ≤ b + d
⊢ a + c < b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₄
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c < d
r₁ : a + c < a + d
r₂ : a + d ≤ b + d
⊢ a + c < b + d
Tactic:
exact lt_of_lt_of_le r₁ r₂
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.sumBounds₅
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
⊢ a ≤ b → c ≤ d → a + c ≤ b + d
Tactic:
intros h₁ h₂
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
⊢ a + c ≤ b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₅
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
⊢ a + c ≤ b + d
Tactic:
have r₁ : a + c ≤ a + d := add_le_add_left h₂ a
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
⊢ a + c ≤ b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₅
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
⊢ a + c ≤ b + d
Tactic:
have r₂ : a + d ≤ b + d := add_le_add_right h₁ d
Proof state after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
r₂ : a + d ≤ b + d
⊢ a + c ≤ b + d
Theorem: Smt.Reconstruct.Arith.sumBounds₅
Proof state before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
r₂ : a + d ≤ b + d
⊢ a + c ≤ b + d
Tactic:
exact le_trans r₁ r₂
Proof state after:
no goals