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

case mpr
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (i : xs.Index) × (f i.val).Index
j : (xs.bind f).Index
⊢ i = unbind f j → bind f i = j
Theorem: List.Index.bind_eq_iff_eq_unbind
Proof state before:
case mp
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (i : xs.Index) × (f i.val).Index
j : (xs.bind f).Index
⊢ bind f i = j → i = unbind f j
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (i : xs.Index) × (f i.val).Index
j : (xs.bind f).Index
h : bind f i = j
⊢ i = unbind f j
Theorem: List.Index.bind_eq_iff_eq_unbind
Proof state before:
case mp
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (i : xs.Index) × (f i.val).Index
j : (xs.bind f).Index
h : bind f i = j
⊢ i = unbind f j
Tactic:
rw [←h, unbind_bind]
Proof state after:
no goals
Theorem: List.Index.bind_eq_iff_eq_unbind
Proof state before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (i : xs.Index) × (f i.val).Index
j : (xs.bind f).Index
⊢ i = unbind f j → bind f i = j
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (i : xs.Index) × (f i.val).Index
j : (xs.bind f).Index
h : i = unbind f j
⊢ bind f i = j
Theorem: List.Index.bind_eq_iff_eq_unbind
Proof state before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (i : xs.Index) × (f i.val).Index
j : (xs.bind f).Index
h : i = unbind f j
⊢ bind f i = j
Tactic:
rw [h, bind_unbind]
Proof state after:
no goals
Theorem: List.Index.unbind_eq_iff_eq_bind
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (xs.bind f).Index
j : (i : xs.Index) × (f i.val).Index
⊢ unbind f i = j ↔ i = bind f j
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (xs.bind f).Index
j : (i : xs.Index) × (f i.val).Index
⊢ unbind f i = j → i = bind f j

case mpr
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (xs.bind f).Index
j : (i : xs.Index) × (f i.val).Index
⊢ i = bind f j → unbind f i = j
Theorem: List.Index.unbind_eq_iff_eq_bind
Proof state before:
case mp
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (xs.bind f).Index
j : (i : xs.Index) × (f i.val).Index
⊢ unbind f i = j → i = bind f j
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (xs.bind f).Index
j : (i : xs.Index) × (f i.val).Index
h : unbind f i = j
⊢ i = bind f j
Theorem: List.Index.unbind_eq_iff_eq_bind
Proof state before:
case mp
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (xs.bind f).Index
j : (i : xs.Index) × (f i.val).Index
h : unbind f i = j
⊢ i = bind f j
Tactic:
rw [←h, bind_unbind]
Proof state after:
no goals
Theorem: List.Index.unbind_eq_iff_eq_bind
Proof state before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (xs.bind f).Index
j : (i : xs.Index) × (f i.val).Index
⊢ i = bind f j → unbind f i = j
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (xs.bind f).Index
j : (i : xs.Index) × (f i.val).Index
h : i = bind f j
⊢ unbind f i = j
Theorem: List.Index.unbind_eq_iff_eq_bind
Proof state before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (xs.bind f).Index
j : (i : xs.Index) × (f i.val).Index
h : i = bind f j
⊢ unbind f i = j
Tactic:
rw [h, unbind_bind]
Proof state after:
no goals
Theorem: List.Index.val_bind
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (i : xs.Index) × (f i.val).Index
⊢ (bind f i).val = i.snd.val
Tactic:
induction xs with
| nil => cases i; contradiction
| cons x xs ih =>
  match i with
  | ⟨head, j⟩ => rw [bind, val_append_inl]
  | ⟨tail i, j⟩ => rw [bind, val_append_inr, ih]
Proof state after:
no goals
Theorem: List.Index.val_bind
Proof state before:
case nil
α : Type u_1
β : Type u_2
f : α → List β
i : (i : [].Index) × (f i.val).Index
⊢ (bind f i).val = i.snd.val
Tactic:
cases i
Proof state after:
case nil.mk
α : Type u_1
β : Type u_2
f : α → List β
fst✝ : [].Index
snd✝ : (f fst✝.val).Index
⊢ (bind f ⟨fst✝, snd✝⟩).val = ⟨fst✝, snd✝⟩.snd.val
Theorem: List.Index.val_bind
Proof state before:
case nil.mk
α : Type u_1
β : Type u_2
f : α → List β
fst✝ : [].Index
snd✝ : (f fst✝.val).Index
⊢ (bind f ⟨fst✝, snd✝⟩).val = ⟨fst✝, snd✝⟩.snd.val
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.val_bind
Proof state before:
case cons
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (bind f i).val = i.snd.val
i : (i : (x :: xs).Index) × (f i.val).Index
⊢ (bind f i).val = i.snd.val
Tactic:
match i with
| ⟨head, j⟩ => rw [bind, val_append_inl]
| ⟨tail i, j⟩ => rw [bind, val_append_inr, ih]
Proof state after:
no goals
Theorem: List.Index.val_bind
Proof state before:
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (bind f i).val = i.snd.val
i : (i : (x :: xs).Index) × (f i.val).Index
j : (f head.val).Index
⊢ (bind f ⟨head, j⟩).val = ⟨head, j⟩.snd.val
Tactic:
rw [bind, val_append_inl]
Proof state after:
no goals
Theorem: List.Index.val_bind
Proof state before:
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (bind f i).val = i.snd.val
i✝ : (i : (x :: xs).Index) × (f i.val).Index
i : xs.Index
j : (f i.tail.val).Index
⊢ (bind f ⟨i.tail, j⟩).val = ⟨i.tail, j⟩.snd.val
Tactic:
rw [bind, val_append_inr, ih]
Proof state after:
no goals
Theorem: List.Index.val_unbind
Proof state before:
α : Type u_1
β : Type u_2
f : α → List β
xs : List α
i : (xs.bind f).Index
⊢ (unbind f i).snd.val = i.val
Tactic:
rw [←bind_unbind f i, val_bind, unbind_bind]
Proof state after:
no goals
Theorem: List.Index.unarr_arr
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h : xs.Index → ys.Index
⊢ (arr h).unarr = h
Tactic:
rw [arr, unarr, unpi_pi]
Proof state after:
no goals
Theorem: List.Index.arr_unarr
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.arr ys).Index
⊢ arr k.unarr = k
Tactic:
rw [arr, unarr, pi_unpi]
Proof state after:
no goals
Theorem: List.Index.arr_eq_iff_eq_unarr
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h : xs.Index → ys.Index
k : (xs.arr ys).Index
⊢ arr h = k ↔ h = k.unarr
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h : xs.Index → ys.Index
k : (xs.arr ys).Index
⊢ arr h = k → h = k.unarr

case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h : xs.Index → ys.Index
k : (xs.arr ys).Index
⊢ h = k.unarr → arr h = k
Theorem: List.Index.arr_eq_iff_eq_unarr
Proof state before:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h : xs.Index → ys.Index
k : (xs.arr ys).Index
⊢ arr h = k → h = k.unarr
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h✝ : xs.Index → ys.Index
k : (xs.arr ys).Index
h : arr h✝ = k
⊢ h✝ = k.unarr
Theorem: List.Index.arr_eq_iff_eq_unarr
Proof state before:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h✝ : xs.Index → ys.Index
k : (xs.arr ys).Index
h : arr h✝ = k
⊢ h✝ = k.unarr
Tactic:
rw [←h, unarr_arr]
Proof state after:
no goals
Theorem: List.Index.arr_eq_iff_eq_unarr
Proof state before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h : xs.Index → ys.Index
k : (xs.arr ys).Index
⊢ h = k.unarr → arr h = k
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h✝ : xs.Index → ys.Index
k : (xs.arr ys).Index
h : h✝ = k.unarr
⊢ arr h✝ = k
Theorem: List.Index.arr_eq_iff_eq_unarr
Proof state before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h✝ : xs.Index → ys.Index
k : (xs.arr ys).Index
h : h✝ = k.unarr
⊢ arr h✝ = k
Tactic:
rw [h, arr_unarr]
Proof state after:
no goals
Theorem: List.Index.unarr_eq_iff_eq_arr
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.arr ys).Index
h : xs.Index → ys.Index
⊢ k.unarr = h ↔ k = arr h
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.arr ys).Index
h : xs.Index → ys.Index
⊢ k.unarr = h → k = arr h

case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.arr ys).Index
h : xs.Index → ys.Index
⊢ k = arr h → k.unarr = h
Theorem: List.Index.unarr_eq_iff_eq_arr
Proof state before:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.arr ys).Index
h : xs.Index → ys.Index
⊢ k.unarr = h → k = arr h
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.arr ys).Index
h✝ : xs.Index → ys.Index
h : k.unarr = h✝
⊢ k = arr h✝
Theorem: List.Index.unarr_eq_iff_eq_arr
Proof state before:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.arr ys).Index
h✝ : xs.Index → ys.Index
h : k.unarr = h✝
⊢ k = arr h✝
Tactic:
rw [←h, arr_unarr]
Proof state after:
no goals
Theorem: List.Index.unarr_eq_iff_eq_arr
Proof state before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.arr ys).Index
h : xs.Index → ys.Index
⊢ k = arr h → k.unarr = h
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.arr ys).Index
h✝ : xs.Index → ys.Index
h : k = arr h✝
⊢ k.unarr = h✝
Theorem: List.Index.unarr_eq_iff_eq_arr
Proof state before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.arr ys).Index
h✝ : xs.Index → ys.Index
h : k = arr h✝
⊢ k.unarr = h✝
Tactic:
rw [h, unarr_arr]
Proof state after:
no goals
Theorem: List.Index.unprod_prod
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
⊢ (prod i).unprod = i
Tactic:
simp only [prod, unprod]
Proof state after:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
⊢ ((unbind (fun x => List.map (Prod.mk x) ys)
          (bind (fun x => List.map (Prod.mk x) ys) ⟨i.fst, map (Prod.mk i.fst.val) i.snd⟩)).fst,
      unmap
        (Prod.mk
          (unbind (fun x => List.map (Prod.mk x) ys)
                (bind (fun x => List.map (Prod.mk x) ys) ⟨i.fst, map (Prod.mk i.fst.val) i.snd⟩)).fst.val)
        (unbind (fun x => List.map (Prod.mk x) ys)
            (bind (fun x => List.map (Prod.mk x) ys) ⟨i.fst, map (Prod.mk i.fst.val) i.snd⟩)).snd) =
    i
Theorem: List.Index.unprod_prod
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
⊢ ((unbind (fun x => List.map (Prod.mk x) ys)
          (bind (fun x => List.map (Prod.mk x) ys) ⟨i.fst, map (Prod.mk i.fst.val) i.snd⟩)).fst,
      unmap
        (Prod.mk
          (unbind (fun x => List.map (Prod.mk x) ys)
                (bind (fun x => List.map (Prod.mk x) ys) ⟨i.fst, map (Prod.mk i.fst.val) i.snd⟩)).fst.val)
        (unbind (fun x => List.map (Prod.mk x) ys)
            (bind (fun x => List.map (Prod.mk x) ys) ⟨i.fst, map (Prod.mk i.fst.val) i.snd⟩)).snd) =
    i
Tactic:
rw [unbind_bind, unmap_map]
Proof state after:
no goals
Theorem: List.Index.prod_unprod
Proof state before:
α : Type u_2
β : Type u_1
xs : List α
ys : List β
k : (xs.prod ys).Index
⊢ prod k.unprod = k
Tactic:
simp only [prod, unprod]
Proof state after:
α : Type u_2
β : Type u_1
xs : List α
ys : List β
k : (xs.prod ys).Index
⊢ bind (fun x => List.map (Prod.mk x) ys)
      ⟨(unbind (fun x => List.map (Prod.mk x) ys) k).fst,
        map (Prod.mk (unbind (fun x => List.map (Prod.mk x) ys) k).fst.val)
          (unmap (Prod.mk (unbind (fun x => List.map (Prod.mk x) ys) k).fst.val)
            (unbind (fun x => List.map (Prod.mk x) ys) k).snd)⟩ =
    k
Theorem: List.Index.prod_unprod
Proof state before:
α : Type u_2
β : Type u_1
xs : List α
ys : List β
k : (xs.prod ys).Index
⊢ bind (fun x => List.map (Prod.mk x) ys)
      ⟨(unbind (fun x => List.map (Prod.mk x) ys) k).fst,
        map (Prod.mk (unbind (fun x => List.map (Prod.mk x) ys) k).fst.val)
          (unmap (Prod.mk (unbind (fun x => List.map (Prod.mk x) ys) k).fst.val)
            (unbind (fun x => List.map (Prod.mk x) ys) k).snd)⟩ =
    k
Tactic:
rw [map_unmap, bind_unbind]
Proof state after:
no goals
Theorem: List.Index.prod_eq_iff_eq_unprod
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
k : (xs.prod ys).Index
⊢ prod i = k ↔ i = k.unprod
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
k : (xs.prod ys).Index
⊢ prod i = k → i = k.unprod

case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
k : (xs.prod ys).Index
⊢ i = k.unprod → prod i = k
Theorem: List.Index.prod_eq_iff_eq_unprod
Proof state before:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
k : (xs.prod ys).Index
⊢ prod i = k → i = k.unprod
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
k : (xs.prod ys).Index
h : prod i = k
⊢ i = k.unprod
Theorem: List.Index.prod_eq_iff_eq_unprod
Proof state before:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
k : (xs.prod ys).Index
h : prod i = k
⊢ i = k.unprod
Tactic:
rw [←h, unprod_prod]
Proof state after:
no goals
Theorem: List.Index.prod_eq_iff_eq_unprod
Proof state before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
k : (xs.prod ys).Index
⊢ i = k.unprod → prod i = k
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
k : (xs.prod ys).Index
h : i = k.unprod
⊢ prod i = k
Theorem: List.Index.prod_eq_iff_eq_unprod
Proof state before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
k : (xs.prod ys).Index
h : i = k.unprod
⊢ prod i = k
Tactic:
rw [h, prod_unprod]
Proof state after:
no goals
Theorem: List.Index.unprod_eq_iff_eq_prod
Proof state before:
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
⊢ i.unprod = j ↔ i = prod j
Tactic:
constructor
Proof state after:
case mp
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
⊢ i.unprod = j → i = prod j

case mpr
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
⊢ i = prod j → i.unprod = j
Theorem: List.Index.unprod_eq_iff_eq_prod
Proof state before:
case mp
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
⊢ i.unprod = j → i = prod j
Tactic:
intro h
Proof state after:
case mp
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
h : i.unprod = j
⊢ i = prod j
Theorem: List.Index.unprod_eq_iff_eq_prod
Proof state before:
case mp
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
h : i.unprod = j
⊢ i = prod j
Tactic:
rw [←h, prod_unprod]
Proof state after:
no goals
Theorem: List.Index.unprod_eq_iff_eq_prod
Proof state before:
case mpr
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
⊢ i = prod j → i.unprod = j
Tactic:
intro h
Proof state after:
case mpr
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
h : i = prod j
⊢ i.unprod = j
Theorem: List.Index.unprod_eq_iff_eq_prod
Proof state before:
case mpr
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
h : i = prod j
⊢ i.unprod = j
Tactic:
rw [h, unprod_prod]
Proof state after:
no goals
Theorem: List.Index.val_prod
Proof state before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
⊢ (prod i).val = (i.fst.val, i.snd.val)
Tactic:
rw [prod, val_bind, val_map]
Proof state after:
no goals
Theorem: List.Index.val_unprod
Proof state before:
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
⊢ (i.unprod.fst.val, i.unprod.snd.val) = i.val
Tactic:
rw [←prod_unprod i, val_prod, unprod_prod]
Proof state after:
no goals
Theorem: Int.add_add_add_comm
Proof state before:
i₁ i₂ j₁ j₂ : Int
⊢ i₁ + i₂ + (j₁ + j₂) = i₁ + (i₂ + (j₁ + j₂))
Tactic:
rw [Int.add_assoc]
Proof state after:
no goals
Theorem: Int.add_add_add_comm
Proof state before:
i₁ i₂ j₁ j₂ : Int
⊢ i₁ + (i₂ + (j₁ + j₂)) = i₁ + (j₁ + (i₂ + j₂))
Tactic:
rw [Int.add_left_comm i₂ j₁ j₂]
Proof state after:
no goals
Theorem: Int.add_add_add_comm
Proof state before:
i₁ i₂ j₁ j₂ : Int
⊢ i₁ + (j₁ + (i₂ + j₂)) = i₁ + j₁ + (i₂ + j₂)
Tactic:
rw [Int.add_assoc]
Proof state after:
no goals
Theorem: Int.mul_mul_mul_comm
Proof state before:
i₁ i₂ j₁ j₂ : Int
⊢ i₁ * i₂ * (j₁ * j₂) = i₁ * (i₂ * (j₁ * j₂))
Tactic:
rw [Int.mul_assoc]
Proof state after:
no goals
Theorem: Int.mul_mul_mul_comm
Proof state before:
i₁ i₂ j₁ j₂ : Int
⊢ i₁ * (i₂ * (j₁ * j₂)) = i₁ * (j₁ * (i₂ * j₂))
Tactic:
rw [Int.mul_left_comm i₂ j₁ j₂]
Proof state after:
no goals
Theorem: Int.mul_mul_mul_comm
Proof state before:
i₁ i₂ j₁ j₂ : Int
⊢ i₁ * (j₁ * (i₂ * j₂)) = i₁ * j₁ * (i₂ * j₂)
Tactic:
rw [Int.mul_assoc]
Proof state after:
no goals
Theorem: Int.mk_self
Proof state before:
m : Nat
⊢ m ⊖ m = 0
Tactic:
induction m with
| zero => rfl
| succ m ih => rw [succ_mk_succ]; exact ih
Proof state after:
no goals
Theorem: Int.mk_self
Proof state before:
case zero

⊢ 0 ⊖ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_self
Proof state before:
case succ
m : Nat
ih : m ⊖ m = 0
⊢ m + 1 ⊖ m + 1 = 0
Tactic:
rw [succ_mk_succ]
Proof state after:
case succ
m : Nat
ih : m ⊖ m = 0
⊢ m ⊖ m = 0
Theorem: Int.mk_self
Proof state before:
case succ
m : Nat
ih : m ⊖ m = 0
⊢ m ⊖ m = 0
Tactic:
exact ih
Proof state after:
no goals
Theorem: Int.add_mk_add_left
Proof state before:
k m n : Nat
⊢ k + m ⊖ k + n = m ⊖ n
Tactic:
induction k with
| zero => rw [Nat.zero_add, Nat.zero_add]
| succ k ih => rw [Nat.succ_add, Nat.succ_add, succ_mk_succ]; exact ih
Proof state after:
no goals
Theorem: Int.add_mk_add_left
Proof state before:
case zero
m n : Nat
⊢ 0 + m ⊖ 0 + n = m ⊖ n
Tactic:
rw [Nat.zero_add, Nat.zero_add]
Proof state after:
no goals
Theorem: Int.add_mk_add_left
Proof state before:
case succ
m n k : Nat
ih : k + m ⊖ k + n = m ⊖ n
⊢ k + 1 + m ⊖ k + 1 + n = m ⊖ n
Tactic:
rw [Nat.succ_add, Nat.succ_add, succ_mk_succ]
Proof state after:
case succ
m n k : Nat
ih : k + m ⊖ k + n = m ⊖ n
⊢ k + m ⊖ k + n = m ⊖ n
Theorem: Int.add_mk_add_left
Proof state before:
case succ
m n k : Nat
ih : k + m ⊖ k + n = m ⊖ n
⊢ k + m ⊖ k + n = m ⊖ n
Tactic:
exact ih
Proof state after:
no goals
Theorem: Int.add_mk_add_right
Proof state before:
k m n : Nat
⊢ m + k ⊖ n + k = m ⊖ n
Tactic:
induction k with
| zero => rw [Nat.add_zero, Nat.add_zero]
| succ k ih => rw [Nat.add_succ m k, Nat.add_succ n k, succ_mk_succ]; exact ih
Proof state after:
no goals
Theorem: Int.add_mk_add_right
Proof state before:
case zero
m n : Nat
⊢ m + 0 ⊖ n + 0 = m ⊖ n
Tactic:
rw [Nat.add_zero, Nat.add_zero]
Proof state after:
no goals
Theorem: Int.add_mk_add_right
Proof state before:
case succ
m n k : Nat
ih : m + k ⊖ n + k = m ⊖ n
⊢ m + (k + 1) ⊖ n + (k + 1) = m ⊖ n
Tactic:
rw [Nat.add_succ m k, Nat.add_succ n k, succ_mk_succ]
Proof state after:
case succ
m n k : Nat
ih : m + k ⊖ n + k = m ⊖ n
⊢ m + k ⊖ n + k = m ⊖ n
Theorem: Int.add_mk_add_right
Proof state before:
case succ
m n k : Nat
ih : m + k ⊖ n + k = m ⊖ n
⊢ m + k ⊖ n + k = m ⊖ n
Tactic:
exact ih
Proof state after:
no goals
Theorem: Int.mk_add_ofNat
Proof state before:
m n k : Nat
⊢ (m ⊖ n) + ofNat k = m + k ⊖ n
Tactic:
induction m, n with
| zero_zero => rw [zero_mk_zero, Int.zero_add, Nat.zero_add, mk_zero]
| zero_succ n => rw [zero_mk_succ, Nat.zero_add]; rfl
| succ_zero m => rw [succ_mk_zero, mk_zero]; rfl
| succ_succ m n ih => rw [succ_mk_succ, Nat.succ_add, succ_mk_succ, ih]
Proof state after:
no goals
Theorem: Int.mk_add_ofNat
Proof state before:
case zero_zero
k : Nat
⊢ (0 ⊖ 0) + ofNat k = 0 + k ⊖ 0
Tactic:
rw [zero_mk_zero, Int.zero_add, Nat.zero_add, mk_zero]
Proof state after:
no goals
Theorem: Int.mk_add_ofNat
Proof state before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) + ofNat k = 0 + k ⊖ n
⊢ (0 ⊖ n + 1) + ofNat k = 0 + k ⊖ n + 1
Tactic:
rw [zero_mk_succ, Nat.zero_add]
Proof state after:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) + ofNat k = 0 + k ⊖ n
⊢ -[n+1] + ofNat k = k ⊖ n + 1
Theorem: Int.mk_add_ofNat
Proof state before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) + ofNat k = 0 + k ⊖ n
⊢ -[n+1] + ofNat k = k ⊖ n + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_add_ofNat
Proof state before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) + ofNat k = m + k ⊖ 0
⊢ (m + 1 ⊖ 0) + ofNat k = m + 1 + k ⊖ 0
Tactic:
rw [succ_mk_zero, mk_zero]
Proof state after:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) + ofNat k = m + k ⊖ 0
⊢ ofNat (m + 1) + ofNat k = ofNat (m + 1 + k)
Theorem: Int.mk_add_ofNat
Proof state before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) + ofNat k = m + k ⊖ 0
⊢ ofNat (m + 1) + ofNat k = ofNat (m + 1 + k)
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_add_ofNat
Proof state before:
case succ_succ
k m n : Nat
ih : (m ⊖ n) + ofNat k = m + k ⊖ n
⊢ (m + 1 ⊖ n + 1) + ofNat k = m + 1 + k ⊖ n + 1
Tactic:
rw [succ_mk_succ, Nat.succ_add, succ_mk_succ, ih]
Proof state after:
no goals
Theorem: Int.mk_add_negSucc
Proof state before:
m n k : Nat
⊢ (m ⊖ n) + -[k+1] = m ⊖ n + k + 1
Tactic:
induction m, n with
| zero_zero => rw [zero_mk_zero, Int.zero_add, Nat.zero_add]; rfl
| zero_succ n => rw [zero_mk_succ, zero_mk_succ, Nat.succ_add]; rfl
| succ_zero m => rw [succ_mk_zero, Nat.zero_add]; rfl
| succ_succ m n ih => rw [succ_mk_succ, Nat.succ_add, succ_mk_succ]; exact ih
Proof state after:
no goals
Theorem: Int.mk_add_negSucc
Proof state before:
case zero_zero
k : Nat
⊢ (0 ⊖ 0) + -[k+1] = 0 ⊖ 0 + k + 1
Tactic:
rw [zero_mk_zero, Int.zero_add, Nat.zero_add]
Proof state after:
case zero_zero
k : Nat
⊢ -[k+1] = 0 ⊖ k + 1
Theorem: Int.mk_add_negSucc
Proof state before:
case zero_zero
k : Nat
⊢ -[k+1] = 0 ⊖ k + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_add_negSucc
Proof state before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) + -[k+1] = 0 ⊖ n + k + 1
⊢ (0 ⊖ n + 1) + -[k+1] = 0 ⊖ n + 1 + k + 1
Tactic:
rw [zero_mk_succ, zero_mk_succ, Nat.succ_add]
Proof state after:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) + -[k+1] = 0 ⊖ n + k + 1
⊢ -[n+1] + -[k+1] = -[(n + k).succ+1]
Theorem: Int.mk_add_negSucc
Proof state before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) + -[k+1] = 0 ⊖ n + k + 1
⊢ -[n+1] + -[k+1] = -[(n + k).succ+1]
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_add_negSucc
Proof state before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) + -[k+1] = m ⊖ 0 + k + 1
⊢ (m + 1 ⊖ 0) + -[k+1] = m + 1 ⊖ 0 + k + 1
Tactic:
rw [succ_mk_zero, Nat.zero_add]
Proof state after:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) + -[k+1] = m ⊖ 0 + k + 1
⊢ ofNat (m + 1) + -[k+1] = m + 1 ⊖ k + 1
Theorem: Int.mk_add_negSucc
Proof state before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) + -[k+1] = m ⊖ 0 + k + 1
⊢ ofNat (m + 1) + -[k+1] = m + 1 ⊖ k + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_add_negSucc
Proof state before:
case succ_succ
k m n : Nat
ih : (m ⊖ n) + -[k+1] = m ⊖ n + k + 1
⊢ (m + 1 ⊖ n + 1) + -[k+1] = m + 1 ⊖ n + 1 + k + 1
Tactic:
rw [succ_mk_succ, Nat.succ_add, succ_mk_succ]
Proof state after:
case succ_succ
k m n : Nat
ih : (m ⊖ n) + -[k+1] = m ⊖ n + k + 1
⊢ (m ⊖ n) + -[k+1] = m ⊖ n + k + 1
Theorem: Int.mk_add_negSucc
Proof state before:
case succ_succ
k m n : Nat
ih : (m ⊖ n) + -[k+1] = m ⊖ n + k + 1
⊢ (m ⊖ n) + -[k+1] = m ⊖ n + k + 1
Tactic:
exact ih
Proof state after:
no goals
Theorem: Int.mk_add_mk
Proof state before:
m₁ n₁ m₂ n₂ : Nat
⊢ (m₁ ⊖ n₁) + (m₂ ⊖ n₂) = m₁ + m₂ ⊖ n₁ + n₂
Tactic:
induction m₂, n₂ with
| zero_zero => rw [zero_mk_zero, Int.add_zero, Nat.add_zero, Nat.add_zero]
| zero_succ n₂ => rw [zero_mk_succ, Nat.add_succ, mk_add_negSucc]; rfl
| succ_zero m₂ => rw [mk_zero, mk_add_ofNat]; rfl
| succ_succ m₂ n₂ ih => rw [succ_mk_succ, Nat.add_succ m₁ m₂, Nat.add_succ n₁ n₂, succ_mk_succ]; exact ih
Proof state after:
no goals