internlm/Lean-Github huggingface dataset:
Theorem: List.Index.unjoin_eq_iff_eq_join
Proof state before:
case mpr
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
⊢ k = join i → k.unjoin = i
Tactic:
intro h
Proof state after:
case mpr
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
h : k = join i
⊢ k.unjoin = i
Theorem: List.Index.unjoin_eq_iff_eq_join
Proof state before:
case mpr
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
h : k = join i
⊢ k.unjoin = i
Tactic:
rw [h, unjoin_join]
Proof state after:
no goals
Theorem: List.Index.val_join
Proof state before:
α✝ : Type u_1
xss : List (List α✝)
i : (i : xss.Index) × i.val.Index
⊢ (join i).val = i.snd.val
Tactic:
induction xss with
| nil => cases i; contradiction
| cons xs xss ih =>
  match i with
  | ⟨head, j⟩ => rw [join, val_append_inl]
  | ⟨tail i, j⟩ => rw [join, val_append_inr, ih]
Proof state after:
no goals
Theorem: List.Index.val_join
Proof state before:
case nil
α✝ : Type u_1
i : (i : [].Index) × i.val.Index
⊢ (join i).val = i.snd.val
Tactic:
cases i
Proof state after:
case nil.mk
α✝ : Type u_1
fst✝ : [].Index
snd✝ : fst✝.val.Index
⊢ (join ⟨fst✝, snd✝⟩).val = ⟨fst✝, snd✝⟩.snd.val
Theorem: List.Index.val_join
Proof state before:
case nil.mk
α✝ : Type u_1
fst✝ : [].Index
snd✝ : fst✝.val.Index
⊢ (join ⟨fst✝, snd✝⟩).val = ⟨fst✝, snd✝⟩.snd.val
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.val_join
Proof state before:
case cons
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).val = i.snd.val
i : (i : (xs :: xss).Index) × i.val.Index
⊢ (join i).val = i.snd.val
Tactic:
match i with
| ⟨head, j⟩ => rw [join, val_append_inl]
| ⟨tail i, j⟩ => rw [join, val_append_inr, ih]
Proof state after:
no goals
Theorem: List.Index.val_join
Proof state before:
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).val = i.snd.val
i : (i : (xs :: xss).Index) × i.val.Index
j : head.val.Index
⊢ (join ⟨head, j⟩).val = ⟨head, j⟩.snd.val
Tactic:
rw [join, val_append_inl]
Proof state after:
no goals
Theorem: List.Index.val_join
Proof state before:
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).val = i.snd.val
i✝ : (i : (xs :: xss).Index) × i.val.Index
i : xss.Index
j : i.tail.val.Index
⊢ (join ⟨i.tail, j⟩).val = ⟨i.tail, j⟩.snd.val
Tactic:
rw [join, val_append_inr, ih]
Proof state after:
no goals
Theorem: List.Index.val_unjoin
Proof state before:
α : Type u_1
xss : List (List α)
k : xss.join.Index
⊢ k.unjoin.snd.val = k.val
Tactic:
rw [←join_unjoin k, val_join, unjoin_join]
Proof state after:
no goals
Theorem: Int.succ_mk_zero
Proof state before:
m : Nat
⊢ m + 1 ⊖ 0 = ofNat (m + 1)
Tactic:
rw [Int.mk, Int.subNatNat, Nat.zero_sub, Nat.sub_zero]
Proof state after:
no goals
Theorem: Int.succ_mk_succ
Proof state before:
m n : Nat
⊢ m + 1 ⊖ n + 1 = m ⊖ n
Tactic:
rw [Int.mk, Int.subNatNat, Int.subNatNat, Nat.succ_sub_succ, Nat.succ_sub_succ]
Proof state after:
no goals
Theorem: Int.mk_zero
Proof state before:
m : Nat
⊢ m ⊖ 0 = ofNat m
Tactic:
rw [Int.mk, Int.subNatNat, Nat.zero_sub, Nat.sub_zero]
Proof state after:
no goals
Theorem: List.Index.val_iota
Proof state before:
α✝ : Type u_1
xs : List α✝
i : xs.Index
⊢ i.iota.val = i
Tactic:
induction i with
| head => rfl
| tail i ih => rw [iota, val_tail, val_map, ih]
Proof state after:
no goals
Theorem: List.Index.val_iota
Proof state before:
case head
α✝ : Type u_1
xs : List α✝
x✝ : α✝
xs✝ : List α✝
⊢ head.iota.val = head
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.val_iota
Proof state before:
case tail
α✝ : Type u_1
xs xs✝ : List α✝
x✝ : α✝
i : xs✝.Index
ih : i.iota.val = i
⊢ i.tail.iota.val = i.tail
Tactic:
rw [iota, val_tail, val_map, ih]
Proof state after:
no goals
Theorem: List.Index.iota_val
Proof state before:
α : Type u_1
xs : List α
i : xs.indexIota.Index
⊢ i.val.iota = i
Tactic:
induction xs with
| nil => contradiction
| cons x xs ih =>
  match i with
  | head => rfl
  | tail i => rw [←map_unmap Index.tail i, val_tail, val_unmap Index.tail, iota, ih, map_unmap]
Proof state after:
no goals
Theorem: List.Index.iota_val
Proof state before:
case nil
α : Type u_1
i : [].indexIota.Index
⊢ i.val.iota = i
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.iota_val
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (i : xs.indexIota.Index), i.val.iota = i
i : (x :: xs).indexIota.Index
⊢ i.val.iota = i
Tactic:
match i with
| head => rfl
| tail i => rw [←map_unmap Index.tail i, val_tail, val_unmap Index.tail, iota, ih, map_unmap]
Proof state after:
no goals
Theorem: List.Index.iota_val
Proof state before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : xs.indexIota.Index), i.val.iota = i
i : (x :: xs).indexIota.Index
⊢ head.val.iota = head
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.iota_val
Proof state before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : xs.indexIota.Index), i.val.iota = i
i✝ : (x :: xs).indexIota.Index
i : (List.map tail xs.indexIota).Index
⊢ i.tail.val.iota = i.tail
Tactic:
rw [←map_unmap Index.tail i, val_tail, val_unmap Index.tail, iota, ih, map_unmap]
Proof state after:
no goals
Theorem: Pos.succ_ne_one
Proof state before:
x : Pos
⊢ x + 1 ≠ 1
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ x.toNat + 1 ≠ 1
Theorem: Pos.succ_ne_one
Proof state before:
x : Pos
⊢ x.toNat + 1 ≠ 1
Tactic:
intro h
Proof state after:
x : Pos
h : x.toNat + 1 = 1
⊢ False
Theorem: Pos.succ_ne_one
Proof state before:
x : Pos
h : x.toNat + 1 = 1
⊢ False
Tactic:
absurd (Nat.succ.inj h)
Proof state after:
x : Pos
h : x.toNat + 1 = 1
⊢ ¬x.toNat = 0
Theorem: Pos.succ_ne_one
Proof state before:
x : Pos
h : x.toNat + 1 = 1
⊢ ¬x.toNat = 0
Tactic:
exact Nat.ne_zero _
Proof state after:
no goals
Theorem: Pos.one_add_eq_add_one
Proof state before:
x : Pos
⊢ 1 + x = x + 1
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ 1 + x.toNat = x.toNat + 1
Theorem: Pos.one_add_eq_add_one
Proof state before:
x : Pos
⊢ 1 + x.toNat = x.toNat + 1
Tactic:
exact Nat.one_add _
Proof state after:
no goals
Theorem: Pos.add_succ
Proof state before:
x y : Pos
⊢ x + (y + 1) = x + y + 1
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ x.toNat + (y.toNat + 1) = x.toNat + y.toNat + 1
Theorem: Pos.add_succ
Proof state before:
x y : Pos
⊢ x.toNat + (y.toNat + 1) = x.toNat + y.toNat + 1
Tactic:
exact Nat.add_succ ..
Proof state after:
no goals
Theorem: Pos.succ_add
Proof state before:
x y : Pos
⊢ x + 1 + y = x + y + 1
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ x.toNat + 1 + y.toNat = x.toNat + y.toNat + 1
Theorem: Pos.succ_add
Proof state before:
x y : Pos
⊢ x.toNat + 1 + y.toNat = x.toNat + y.toNat + 1
Tactic:
exact Nat.succ_add ..
Proof state after:
no goals
Theorem: Pos.add_assoc
Proof state before:
x y z : Pos
⊢ x + y + z = x + (y + z)
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ x.toNat + y.toNat + z.toNat = x.toNat + (y.toNat + z.toNat)
Theorem: Pos.add_assoc
Proof state before:
x y z : Pos
⊢ x.toNat + y.toNat + z.toNat = x.toNat + (y.toNat + z.toNat)
Tactic:
exact Nat.add_assoc ..
Proof state after:
no goals
Theorem: Pos.add_comm
Proof state before:
x y : Pos
⊢ x + y = y + x
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ x.toNat + y.toNat = y.toNat + x.toNat
Theorem: Pos.add_comm
Proof state before:
x y : Pos
⊢ x.toNat + y.toNat = y.toNat + x.toNat
Tactic:
exact Nat.add_comm ..
Proof state after:
no goals
Theorem: Pos.add_left_comm
Proof state before:
x y z : Pos
⊢ x + (y + z) = y + (x + z)
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ x.toNat + (y.toNat + z.toNat) = y.toNat + (x.toNat + z.toNat)
Theorem: Pos.add_left_comm
Proof state before:
x y z : Pos
⊢ x.toNat + (y.toNat + z.toNat) = y.toNat + (x.toNat + z.toNat)
Tactic:
exact Nat.add_left_comm ..
Proof state after:
no goals
Theorem: Pos.add_right_comm
Proof state before:
x y z : Pos
⊢ x + y + z = x + z + y
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ x.toNat + y.toNat + z.toNat = x.toNat + z.toNat + y.toNat
Theorem: Pos.add_right_comm
Proof state before:
x y z : Pos
⊢ x.toNat + y.toNat + z.toNat = x.toNat + z.toNat + y.toNat
Tactic:
exact Nat.add_right_comm ..
Proof state after:
no goals
Theorem: Pos.add_left_cancel
Proof state before:
x y z : Pos
⊢ x + y = x + z → y = z
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ x.toNat + y.toNat = x.toNat + z.toNat → y.toNat = z.toNat
Theorem: Pos.add_left_cancel
Proof state before:
x y z : Pos
⊢ x.toNat + y.toNat = x.toNat + z.toNat → y.toNat = z.toNat
Tactic:
exact Nat.add_left_cancel
Proof state after:
no goals
Theorem: Pos.add_right_cancel
Proof state before:
x y z : Pos
⊢ x + y = z + y → x = z
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ x.toNat + y.toNat = z.toNat + y.toNat → x.toNat = z.toNat
Theorem: Pos.add_right_cancel
Proof state before:
x y z : Pos
⊢ x.toNat + y.toNat = z.toNat + y.toNat → x.toNat = z.toNat
Tactic:
exact Nat.add_right_cancel
Proof state after:
no goals
Theorem: Pos.ne_add_self_left
Proof state before:
x y : Pos
⊢ x ≠ y + x
Tactic:
induction x with
| one =>
  apply Ne.symm
  exact Pos.succ_ne_one y
| succ x H =>
  intro h
  rw [Pos.add_succ] at h
  apply H
  exact Pos.add_right_cancel h
Proof state after:
no goals
Theorem: Pos.ne_add_self_left
Proof state before:
case one
y : Pos
⊢ 1 ≠ y + 1
Tactic:
apply Ne.symm
Proof state after:
case one.h
y : Pos
⊢ y + 1 ≠ 1
Theorem: Pos.ne_add_self_left
Proof state before:
case one.h
y : Pos
⊢ y + 1 ≠ 1
Tactic:
exact Pos.succ_ne_one y
Proof state after:
no goals
Theorem: Pos.ne_add_self_left
Proof state before:
case succ
y x : Pos
H : x ≠ y + x
⊢ x + 1 ≠ y + (x + 1)
Tactic:
intro h
Proof state after:
case succ
y x : Pos
H : x ≠ y + x
h : x + 1 = y + (x + 1)
⊢ False
Theorem: Pos.ne_add_self_left
Proof state before:
case succ
y x : Pos
H : x ≠ y + x
h : x + 1 = y + (x + 1)
⊢ False
Tactic:
rw [Pos.add_succ] at h
Proof state after:
case succ
y x : Pos
H : x ≠ y + x
h : x + 1 = y + x + 1
⊢ False
Theorem: Pos.ne_add_self_left
Proof state before:
case succ
y x : Pos
H : x ≠ y + x
h : x + 1 = y + x + 1
⊢ False
Tactic:
apply H
Proof state after:
case succ
y x : Pos
H : x ≠ y + x
h : x + 1 = y + x + 1
⊢ x = y + x
Theorem: Pos.ne_add_self_left
Proof state before:
case succ
y x : Pos
H : x ≠ y + x
h : x + 1 = y + x + 1
⊢ x = y + x
Tactic:
exact Pos.add_right_cancel h
Proof state after:
no goals
Theorem: Pos.ne_add_self_right
Proof state before:
x y : Pos
⊢ x ≠ x + y
Tactic:
induction x with
| one =>
  apply Ne.symm
  rw [Pos.one_add_eq_add_one]
  exact Pos.succ_ne_one y
| succ x H =>
  intro h
  rw [Pos.succ_add] at h
  apply H
  exact Pos.add_right_cancel h
Proof state after:
no goals
Theorem: Pos.ne_add_self_right
Proof state before:
case one
y : Pos
⊢ 1 ≠ 1 + y
Tactic:
apply Ne.symm
Proof state after:
case one.h
y : Pos
⊢ 1 + y ≠ 1
Theorem: Pos.ne_add_self_right
Proof state before:
case one.h
y : Pos
⊢ 1 + y ≠ 1
Tactic:
rw [Pos.one_add_eq_add_one]
Proof state after:
case one.h
y : Pos
⊢ y + 1 ≠ 1
Theorem: Pos.ne_add_self_right
Proof state before:
case one.h
y : Pos
⊢ y + 1 ≠ 1
Tactic:
exact Pos.succ_ne_one y
Proof state after:
no goals
Theorem: Pos.ne_add_self_right
Proof state before:
case succ
y x : Pos
H : x ≠ x + y
⊢ x + 1 ≠ x + 1 + y
Tactic:
intro h
Proof state after:
case succ
y x : Pos
H : x ≠ x + y
h : x + 1 = x + 1 + y
⊢ False
Theorem: Pos.ne_add_self_right
Proof state before:
case succ
y x : Pos
H : x ≠ x + y
h : x + 1 = x + 1 + y
⊢ False
Tactic:
rw [Pos.succ_add] at h
Proof state after:
case succ
y x : Pos
H : x ≠ x + y
h : x + 1 = x + y + 1
⊢ False
Theorem: Pos.ne_add_self_right
Proof state before:
case succ
y x : Pos
H : x ≠ x + y
h : x + 1 = x + y + 1
⊢ False
Tactic:
apply H
Proof state after:
case succ
y x : Pos
H : x ≠ x + y
h : x + 1 = x + y + 1
⊢ x = x + y
Theorem: Pos.ne_add_self_right
Proof state before:
case succ
y x : Pos
H : x ≠ x + y
h : x + 1 = x + y + 1
⊢ x = x + y
Tactic:
exact Pos.add_right_cancel h
Proof state after:
no goals
Theorem: Pos.one_mul
Proof state before:
x : Pos
⊢ 1 * x = x
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ 1 * x.toNat = x.toNat
Theorem: Pos.one_mul
Proof state before:
x : Pos
⊢ 1 * x.toNat = x.toNat
Tactic:
exact Nat.one_mul _
Proof state after:
no goals
Theorem: Pos.mul_one
Proof state before:
x : Pos
⊢ x * 1 = x
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ x.toNat * 1 = x.toNat
Theorem: Pos.mul_one
Proof state before:
x : Pos
⊢ x.toNat * 1 = x.toNat
Tactic:
exact Nat.mul_one _
Proof state after:
no goals
Theorem: Pos.succ_mul
Proof state before:
x y : Pos
⊢ (x + 1) * y = x * y + y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ (x.toNat + 1) * y.toNat = x.toNat * y.toNat + y.toNat
Theorem: Pos.succ_mul
Proof state before:
x y : Pos
⊢ (x.toNat + 1) * y.toNat = x.toNat * y.toNat + y.toNat
Tactic:
exact Nat.succ_mul ..
Proof state after:
no goals
Theorem: Pos.mul_succ
Proof state before:
x y : Pos
⊢ x * (y + 1) = x * y + x
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ x.toNat * (y.toNat + 1) = x.toNat * y.toNat + x.toNat
Theorem: Pos.mul_succ
Proof state before:
x y : Pos
⊢ x.toNat * (y.toNat + 1) = x.toNat * y.toNat + x.toNat
Tactic:
exact Nat.mul_succ ..
Proof state after:
no goals
Theorem: Pos.mul_assoc
Proof state before:
x y z : Pos
⊢ x * y * z = x * (y * z)
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ x.toNat * y.toNat * z.toNat = x.toNat * (y.toNat * z.toNat)
Theorem: Pos.mul_assoc
Proof state before:
x y z : Pos
⊢ x.toNat * y.toNat * z.toNat = x.toNat * (y.toNat * z.toNat)
Tactic:
exact Nat.mul_assoc ..
Proof state after:
no goals
Theorem: Pos.mul_comm
Proof state before:
x y : Pos
⊢ x * y = y * x
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ x.toNat * y.toNat = y.toNat * x.toNat
Theorem: Pos.mul_comm
Proof state before:
x y : Pos
⊢ x.toNat * y.toNat = y.toNat * x.toNat
Tactic:
exact Nat.mul_comm ..
Proof state after:
no goals
Theorem: Pos.mul_left_comm
Proof state before:
x y z : Pos
⊢ x * (y * z) = y * (x * z)
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ x.toNat * (y.toNat * z.toNat) = y.toNat * (x.toNat * z.toNat)
Theorem: Pos.mul_left_comm
Proof state before:
x y z : Pos
⊢ x.toNat * (y.toNat * z.toNat) = y.toNat * (x.toNat * z.toNat)
Tactic:
exact Nat.mul_left_comm ..
Proof state after:
no goals
Theorem: Pos.mul_right_comm
Proof state before:
x y z : Pos
⊢ x * y * z = x * z * y
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ x.toNat * y.toNat * z.toNat = x.toNat * z.toNat * y.toNat
Theorem: Pos.mul_right_comm
Proof state before:
x y z : Pos
⊢ x.toNat * y.toNat * z.toNat = x.toNat * z.toNat * y.toNat
Tactic:
exact Nat.mul_right_comm ..
Proof state after:
no goals
Theorem: Pos.left_distrib
Proof state before:
x y z : Pos
⊢ x * (y + z) = x * y + x * z
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ x.toNat * (y.toNat + z.toNat) = x.toNat * y.toNat + x.toNat * z.toNat
Theorem: Pos.left_distrib
Proof state before:
x y z : Pos
⊢ x.toNat * (y.toNat + z.toNat) = x.toNat * y.toNat + x.toNat * z.toNat
Tactic:
exact Nat.left_distrib ..
Proof state after:
no goals
Theorem: Pos.right_distrib
Proof state before:
x y z : Pos
⊢ (x + y) * z = x * z + y * z
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ (x.toNat + y.toNat) * z.toNat = x.toNat * z.toNat + y.toNat * z.toNat
Theorem: Pos.right_distrib
Proof state before:
x y z : Pos
⊢ (x.toNat + y.toNat) * z.toNat = x.toNat * z.toNat + y.toNat * z.toNat
Tactic:
exact Nat.right_distrib ..
Proof state after:
no goals
Theorem: Pos.mul_left_cancel
Proof state before:
x y z : Pos
⊢ x * y = x * z → y = z
Tactic:
intro h
Proof state after:
x y z : Pos
h : x * y = x * z
⊢ y = z
Theorem: Pos.mul_left_cancel
Proof state before:
x y z : Pos
h : x * y = x * z
⊢ y = z
Tactic:
induction y, z with
| one_one => rfl
| one_succ z _ =>
  rw [Pos.mul_one, Pos.mul_succ] at h
  absurd h
  apply Pos.ne_add_self_left
| succ_one y _ =>
  rw [Pos.mul_one, Pos.mul_succ] at h
  absurd h.symm
  apply Pos.ne_add_self_left
| succ_succ y z H =>
  rw [Pos.mul_succ, Pos.mul_succ] at h
  rw [H (Pos.add_right_cancel h)]
Proof state after:
no goals
Theorem: Pos.mul_left_cancel
Proof state before:
case one_one
x : Pos
h : x * 1 = x * 1
⊢ 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Pos.mul_left_cancel
Proof state before:
case one_succ
x z : Pos
a✝ : x * 1 = x * z → 1 = z
h : x * 1 = x * (z + 1)
⊢ 1 = z + 1
Tactic:
rw [Pos.mul_one, Pos.mul_succ] at h
Proof state after:
case one_succ
x z : Pos
a✝ : x * 1 = x * z → 1 = z
h : x = x * z + x
⊢ 1 = z + 1
Theorem: Pos.mul_left_cancel
Proof state before:
case one_succ
x z : Pos
a✝ : x * 1 = x * z → 1 = z
h : x = x * z + x
⊢ 1 = z + 1
Tactic:
absurd h
Proof state after:
case one_succ
x z : Pos
a✝ : x * 1 = x * z → 1 = z
h : x = x * z + x
⊢ ¬x = x * z + x
Theorem: Pos.mul_left_cancel
Proof state before:
case one_succ
x z : Pos
a✝ : x * 1 = x * z → 1 = z
h : x = x * z + x
⊢ ¬x = x * z + x
Tactic:
apply Pos.ne_add_self_left
Proof state after:
no goals
Theorem: Pos.mul_left_cancel
Proof state before:
case succ_one
x y : Pos
a✝ : x * y = x * 1 → y = 1
h : x * (y + 1) = x * 1
⊢ y + 1 = 1
Tactic:
rw [Pos.mul_one, Pos.mul_succ] at h
Proof state after:
case succ_one
x y : Pos
a✝ : x * y = x * 1 → y = 1
h : x * y + x = x
⊢ y + 1 = 1
Theorem: Pos.mul_left_cancel
Proof state before:
case succ_one
x y : Pos
a✝ : x * y = x * 1 → y = 1
h : x * y + x = x
⊢ y + 1 = 1
Tactic:
absurd h.symm
Proof state after:
case succ_one
x y : Pos
a✝ : x * y = x * 1 → y = 1
h : x * y + x = x
⊢ ¬x = x * y + x
Theorem: Pos.mul_left_cancel
Proof state before:
case succ_one
x y : Pos
a✝ : x * y = x * 1 → y = 1
h : x * y + x = x
⊢ ¬x = x * y + x
Tactic:
apply Pos.ne_add_self_left
Proof state after:
no goals
Theorem: Pos.mul_left_cancel
Proof state before:
case succ_succ
x y z : Pos
H : x * y = x * z → y = z
h : x * (y + 1) = x * (z + 1)
⊢ y + 1 = z + 1
Tactic:
rw [Pos.mul_succ, Pos.mul_succ] at h
Proof state after:
case succ_succ
x y z : Pos
H : x * y = x * z → y = z
h : x * y + x = x * z + x
⊢ y + 1 = z + 1
Theorem: Pos.mul_left_cancel
Proof state before:
case succ_succ
x y z : Pos
H : x * y = x * z → y = z
h : x * y + x = x * z + x
⊢ y + 1 = z + 1
Tactic:
rw [H (Pos.add_right_cancel h)]
Proof state after:
no goals
Theorem: Pos.mul_right_cancel
Proof state before:
x y z : Pos
⊢ x * y = z * y → x = z
Tactic:
intro h
Proof state after:
x y z : Pos
h : x * y = z * y
⊢ x = z
Theorem: Pos.mul_right_cancel
Proof state before:
x y z : Pos
h : x * y = z * y
⊢ x = z
Tactic:
induction x, z with
| one_one => rfl
| one_succ x _ =>
  rw [Pos.one_mul, Pos.succ_mul] at h
  absurd h
  apply Pos.ne_add_self_left
| succ_one z _ =>
  rw [Pos.one_mul, Pos.succ_mul] at h
  absurd h.symm
  apply Pos.ne_add_self_left
| succ_succ x z H =>
  rw [Pos.succ_mul, Pos.succ_mul] at h
  rw [H (Pos.add_right_cancel h)]
Proof state after:
no goals
Theorem: Pos.mul_right_cancel
Proof state before:
case one_one
y : Pos
h : 1 * y = 1 * y
⊢ 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Pos.mul_right_cancel
Proof state before:
case one_succ
y x : Pos
a✝ : 1 * y = x * y → 1 = x
h : 1 * y = (x + 1) * y
⊢ 1 = x + 1
Tactic:
rw [Pos.one_mul, Pos.succ_mul] at h
Proof state after:
case one_succ
y x : Pos
a✝ : 1 * y = x * y → 1 = x
h : y = x * y + y
⊢ 1 = x + 1
Theorem: Pos.mul_right_cancel
Proof state before:
case one_succ
y x : Pos
a✝ : 1 * y = x * y → 1 = x
h : y = x * y + y
⊢ 1 = x + 1
Tactic:
absurd h
Proof state after:
case one_succ
y x : Pos
a✝ : 1 * y = x * y → 1 = x
h : y = x * y + y
⊢ ¬y = x * y + y
Theorem: Pos.mul_right_cancel
Proof state before:
case one_succ
y x : Pos
a✝ : 1 * y = x * y → 1 = x
h : y = x * y + y
⊢ ¬y = x * y + y
Tactic:
apply Pos.ne_add_self_left
Proof state after:
no goals
Theorem: Pos.mul_right_cancel
Proof state before:
case succ_one
y z : Pos
a✝ : z * y = 1 * y → z = 1
h : (z + 1) * y = 1 * y
⊢ z + 1 = 1
Tactic:
rw [Pos.one_mul, Pos.succ_mul] at h
Proof state after:
case succ_one
y z : Pos
a✝ : z * y = 1 * y → z = 1
h : z * y + y = y
⊢ z + 1 = 1
Theorem: Pos.mul_right_cancel
Proof state before:
case succ_one
y z : Pos
a✝ : z * y = 1 * y → z = 1
h : z * y + y = y
⊢ z + 1 = 1
Tactic:
absurd h.symm
Proof state after:
case succ_one
y z : Pos
a✝ : z * y = 1 * y → z = 1
h : z * y + y = y
⊢ ¬y = z * y + y
Theorem: Pos.mul_right_cancel
Proof state before:
case succ_one
y z : Pos
a✝ : z * y = 1 * y → z = 1
h : z * y + y = y
⊢ ¬y = z * y + y
Tactic:
apply Pos.ne_add_self_left
Proof state after:
no goals
Theorem: Pos.mul_right_cancel
Proof state before:
case succ_succ
y x z : Pos
H : x * y = z * y → x = z
h : (x + 1) * y = (z + 1) * y
⊢ x + 1 = z + 1
Tactic:
rw [Pos.succ_mul, Pos.succ_mul] at h
Proof state after:
case succ_succ
y x z : Pos
H : x * y = z * y → x = z
h : x * y + y = z * y + y
⊢ x + 1 = z + 1
Theorem: Pos.mul_right_cancel
Proof state before:
case succ_succ
y x z : Pos
H : x * y = z * y → x = z
h : x * y + y = z * y + y
⊢ x + 1 = z + 1
Tactic:
rw [H (Pos.add_right_cancel h)]
Proof state after:
no goals
Theorem: Pos.pow_zero
Proof state before:
x : Pos
⊢ x ^ 0 = 1
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ x.toNat ^ 0 = 1
Theorem: Pos.pow_zero
Proof state before:
x : Pos
⊢ x.toNat ^ 0 = 1
Tactic:
exact Nat.pow_zero _
Proof state after:
no goals
Theorem: Pos.pow_one
Proof state before:
x : Pos
⊢ x ^ 1 = x
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ x.toNat ^ 1 = x.toNat
Theorem: Pos.pow_one
Proof state before:
x : Pos
⊢ x.toNat ^ 1 = x.toNat
Tactic:
exact Nat.pow_one ..
Proof state after:
no goals
Theorem: Pos.one_pow
Proof state before:
x : Nat
⊢ 1 ^ x = 1
Tactic:
exact Nat.one_pow ..
Proof state after:
no goals
Theorem: Pos.pow_succ
Proof state before:
x : Pos
y : Nat
⊢ x ^ (y + 1) = x ^ y * x
Tactic:
by_toNat
Proof state after:
x : Pos
y : Nat
⊢ x.toNat ^ (y + 1) = x.toNat ^ y * x.toNat
Theorem: Pos.pow_succ
Proof state before:
x : Pos
y : Nat
⊢ x.toNat ^ (y + 1) = x.toNat ^ y * x.toNat
Tactic:
exact Nat.pow_succ ..
Proof state after:
no goals
Theorem: Pos.pow_add
Proof state before:
x : Pos
y z : Nat
⊢ x ^ (y + z) = x ^ y * x ^ z
Tactic:
by_toNat
Proof state after:
x : Pos
y z : Nat
⊢ x.toNat ^ (y + z) = x.toNat ^ y * x.toNat ^ z
Theorem: Pos.pow_add
Proof state before:
x : Pos
y z : Nat
⊢ x.toNat ^ (y + z) = x.toNat ^ y * x.toNat ^ z
Tactic:
exact Nat.pow_add ..
Proof state after:
no goals
Theorem: Pos.mul_pow
Proof state before:
x y : Pos
z : Nat
⊢ (x * y) ^ z = x ^ z * y ^ z
Tactic:
by_toNat
Proof state after:
x y : Pos
z : Nat
⊢ (x.toNat * y.toNat) ^ z = x.toNat ^ z * y.toNat ^ z
Theorem: Pos.mul_pow
Proof state before:
x y : Pos
z : Nat
⊢ (x.toNat * y.toNat) ^ z = x.toNat ^ z * y.toNat ^ z
Tactic:
exact Nat.mul_pow ..
Proof state after:
no goals
Theorem: Pos.pow_mul
Proof state before:
x : Pos
y z : Nat
⊢ x ^ (y * z) = (x ^ y) ^ z
Tactic:
by_toNat
Proof state after:
x : Pos
y z : Nat
⊢ x.toNat ^ (y * z) = (x.toNat ^ y) ^ z
Theorem: Pos.pow_mul
Proof state before:
x : Pos
y z : Nat
⊢ x.toNat ^ (y * z) = (x.toNat ^ y) ^ z
Tactic:
exact Nat.pow_mul ..
Proof state after:
no goals
Theorem: Pos.pow_mul'
Proof state before:
x : Pos
y z : Nat
⊢ x ^ (y * z) = (x ^ z) ^ y
Tactic:
by_toNat
Proof state after:
x : Pos
y z : Nat
⊢ x.toNat ^ (y * z) = (x.toNat ^ z) ^ y
Theorem: Pos.pow_mul'
Proof state before:
x : Pos
y z : Nat
⊢ x.toNat ^ (y * z) = (x.toNat ^ z) ^ y
Tactic:
exact Nat.pow_mul' ..
Proof state after:
no goals
Theorem: Pos.pow_assoc
Proof state before:
x : Pos
y z : Nat
⊢ (x ^ y) ^ z = x ^ (y * z)
Tactic:
rw [Pos.pow_mul]
Proof state after:
no goals
Theorem: Pos.le_refl
Proof state before:
x : Pos
⊢ x ≤ x
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ x.toNat ≥ x.toNat
Theorem: Pos.le_refl
Proof state before:
x : Pos
⊢ x.toNat ≥ x.toNat
Tactic:
exact Nat.le_refl ..
Proof state after:
no goals
Theorem: Pos.le_trans
Proof state before:
x y z : Pos
⊢ x ≤ y → y ≤ z → x ≤ z
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ y.toNat ≥ x.toNat → z.toNat ≥ y.toNat → z.toNat ≥ x.toNat
Theorem: Pos.le_trans
Proof state before:
x y z : Pos
⊢ y.toNat ≥ x.toNat → z.toNat ≥ y.toNat → z.toNat ≥ x.toNat
Tactic:
exact Nat.le_trans
Proof state after:
no goals
Theorem: Pos.le_antisymm
Proof state before:
x y : Pos
⊢ x ≤ y → y ≤ x → x = y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat → x.toNat ≥ y.toNat → x.toNat = y.toNat
Theorem: Pos.le_antisymm
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat → x.toNat ≥ y.toNat → x.toNat = y.toNat
Tactic:
exact Nat.le_antisymm
Proof state after:
no goals