internlm/Lean-Github huggingface dataset:
Theorem: Int.mk_add_mk
Proof state before:
case zero_zero
m₁ n₁ : Nat
⊢ (m₁ ⊖ n₁) + (0 ⊖ 0) = m₁ + 0 ⊖ n₁ + 0
Tactic:
rw [zero_mk_zero, Int.add_zero, Nat.add_zero, Nat.add_zero]
Proof state after:
no goals
Theorem: Int.mk_add_mk
Proof state before:
case zero_succ
m₁ n₁ n₂ : Nat
a✝ : (m₁ ⊖ n₁) + (0 ⊖ n₂) = m₁ + 0 ⊖ n₁ + n₂
⊢ (m₁ ⊖ n₁) + (0 ⊖ n₂ + 1) = m₁ + 0 ⊖ n₁ + (n₂ + 1)
Tactic:
rw [zero_mk_succ, Nat.add_succ, mk_add_negSucc]
Proof state after:
case zero_succ
m₁ n₁ n₂ : Nat
a✝ : (m₁ ⊖ n₁) + (0 ⊖ n₂) = m₁ + 0 ⊖ n₁ + n₂
⊢ m₁ ⊖ n₁ + n₂ + 1 = m₁ + 0 ⊖ (n₁ + n₂).succ
Theorem: Int.mk_add_mk
Proof state before:
case zero_succ
m₁ n₁ n₂ : Nat
a✝ : (m₁ ⊖ n₁) + (0 ⊖ n₂) = m₁ + 0 ⊖ n₁ + n₂
⊢ m₁ ⊖ n₁ + n₂ + 1 = m₁ + 0 ⊖ (n₁ + n₂).succ
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_add_mk
Proof state before:
case succ_zero
m₁ n₁ m₂ : Nat
a✝ : (m₁ ⊖ n₁) + (m₂ ⊖ 0) = m₁ + m₂ ⊖ n₁ + 0
⊢ (m₁ ⊖ n₁) + (m₂ + 1 ⊖ 0) = m₁ + (m₂ + 1) ⊖ n₁ + 0
Tactic:
rw [mk_zero, mk_add_ofNat]
Proof state after:
case succ_zero
m₁ n₁ m₂ : Nat
a✝ : (m₁ ⊖ n₁) + (m₂ ⊖ 0) = m₁ + m₂ ⊖ n₁ + 0
⊢ m₁ + (m₂ + 1) ⊖ n₁ = m₁ + (m₂ + 1) ⊖ n₁ + 0
Theorem: Int.mk_add_mk
Proof state before:
case succ_zero
m₁ n₁ m₂ : Nat
a✝ : (m₁ ⊖ n₁) + (m₂ ⊖ 0) = m₁ + m₂ ⊖ n₁ + 0
⊢ m₁ + (m₂ + 1) ⊖ n₁ = m₁ + (m₂ + 1) ⊖ n₁ + 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_add_mk
Proof state before:
case succ_succ
m₁ n₁ m₂ n₂ : Nat
ih : (m₁ ⊖ n₁) + (m₂ ⊖ n₂) = m₁ + m₂ ⊖ n₁ + n₂
⊢ (m₁ ⊖ n₁) + (m₂ + 1 ⊖ n₂ + 1) = m₁ + (m₂ + 1) ⊖ n₁ + (n₂ + 1)
Tactic:
rw [succ_mk_succ, Nat.add_succ m₁ m₂, Nat.add_succ n₁ n₂, succ_mk_succ]
Proof state after:
case succ_succ
m₁ n₁ m₂ n₂ : Nat
ih : (m₁ ⊖ n₁) + (m₂ ⊖ n₂) = m₁ + m₂ ⊖ n₁ + n₂
⊢ (m₁ ⊖ n₁) + (m₂ ⊖ n₂) = m₁ + m₂ ⊖ n₁ + n₂
Theorem: Int.mk_add_mk
Proof state before:
case succ_succ
m₁ n₁ m₂ n₂ : Nat
ih : (m₁ ⊖ n₁) + (m₂ ⊖ n₂) = m₁ + m₂ ⊖ n₁ + n₂
⊢ (m₁ ⊖ n₁) + (m₂ ⊖ n₂) = m₁ + m₂ ⊖ n₁ + n₂
Tactic:
exact ih
Proof state after:
no goals
Theorem: Int.neg_mk
Proof state before:
m n : Nat
⊢ -(m ⊖ n) = n ⊖ m
Tactic:
induction m, n with
| zero_zero => rw [zero_mk_zero]; rfl
| zero_succ n => rw [zero_mk_succ, succ_mk_zero]; rfl
| succ_zero m => rw [succ_mk_zero, zero_mk_succ]; rfl
| succ_succ m n ih => rw [succ_mk_succ, succ_mk_succ]; exact ih
Proof state after:
no goals
Theorem: Int.neg_mk
Proof state before:
case zero_zero

⊢ -(0 ⊖ 0) = 0 ⊖ 0
Tactic:
rw [zero_mk_zero]
Proof state after:
case zero_zero

⊢ -0 = 0
Theorem: Int.neg_mk
Proof state before:
case zero_zero

⊢ -0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.neg_mk
Proof state before:
case zero_succ
n : Nat
a✝ : -(0 ⊖ n) = n ⊖ 0
⊢ -(0 ⊖ n + 1) = n + 1 ⊖ 0
Tactic:
rw [zero_mk_succ, succ_mk_zero]
Proof state after:
case zero_succ
n : Nat
a✝ : -(0 ⊖ n) = n ⊖ 0
⊢ - -[n+1] = ofNat (n + 1)
Theorem: Int.neg_mk
Proof state before:
case zero_succ
n : Nat
a✝ : -(0 ⊖ n) = n ⊖ 0
⊢ - -[n+1] = ofNat (n + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.neg_mk
Proof state before:
case succ_zero
m : Nat
a✝ : -(m ⊖ 0) = 0 ⊖ m
⊢ -(m + 1 ⊖ 0) = 0 ⊖ m + 1
Tactic:
rw [succ_mk_zero, zero_mk_succ]
Proof state after:
case succ_zero
m : Nat
a✝ : -(m ⊖ 0) = 0 ⊖ m
⊢ -ofNat (m + 1) = -[m+1]
Theorem: Int.neg_mk
Proof state before:
case succ_zero
m : Nat
a✝ : -(m ⊖ 0) = 0 ⊖ m
⊢ -ofNat (m + 1) = -[m+1]
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.neg_mk
Proof state before:
case succ_succ
m n : Nat
ih : -(m ⊖ n) = n ⊖ m
⊢ -(m + 1 ⊖ n + 1) = n + 1 ⊖ m + 1
Tactic:
rw [succ_mk_succ, succ_mk_succ]
Proof state after:
case succ_succ
m n : Nat
ih : -(m ⊖ n) = n ⊖ m
⊢ -(m ⊖ n) = n ⊖ m
Theorem: Int.neg_mk
Proof state before:
case succ_succ
m n : Nat
ih : -(m ⊖ n) = n ⊖ m
⊢ -(m ⊖ n) = n ⊖ m
Tactic:
exact ih
Proof state after:
no goals
Theorem: Int.mk_sub_mk
Proof state before:
m₁ n₁ m₂ n₂ : Nat
⊢ (m₁ ⊖ n₁) + -(m₂ ⊖ n₂) = m₁ + n₂ ⊖ n₁ + m₂
Tactic:
rw [neg_mk, mk_add_mk]
Proof state after:
no goals
Theorem: Int.nonNeg_mk
Proof state before:
case zero_zero

⊢ (0 ⊖ 0).NonNeg ↔ 0 ≤ 0
Tactic:
rw [zero_mk_zero]
Proof state after:
case zero_zero

⊢ NonNeg 0 ↔ 0 ≤ 0
Theorem: Int.nonNeg_mk
Proof state before:
case zero_zero

⊢ NonNeg 0 ↔ 0 ≤ 0
Tactic:
constructor
Proof state after:
case zero_zero.mp

⊢ NonNeg 0 → 0 ≤ 0

case zero_zero.mpr

⊢ 0 ≤ 0 → NonNeg 0
Theorem: Int.nonNeg_mk
Proof state before:
case zero_zero.mp

⊢ NonNeg 0 → 0 ≤ 0
Tactic:
intro
Proof state after:
case zero_zero.mp
a✝ : NonNeg 0
⊢ 0 ≤ 0
Theorem: Int.nonNeg_mk
Proof state before:
case zero_zero.mp
a✝ : NonNeg 0
⊢ 0 ≤ 0
Tactic:
exact Nat.le_refl ..
Proof state after:
no goals
Theorem: Int.nonNeg_mk
Proof state before:
case zero_zero.mpr

⊢ 0 ≤ 0 → NonNeg 0
Tactic:
intro
Proof state after:
case zero_zero.mpr
a✝ : 0 ≤ 0
⊢ NonNeg 0
Theorem: Int.nonNeg_mk
Proof state before:
case zero_zero.mpr
a✝ : 0 ≤ 0
⊢ NonNeg 0
Tactic:
apply NonNeg.mk
Proof state after:
no goals
Theorem: Int.nonNeg_mk
Proof state before:
case zero_succ
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ (0 ⊖ n + 1).NonNeg ↔ n + 1 ≤ 0
Tactic:
rw [zero_mk_succ]
Proof state after:
case zero_succ
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ -[n+1].NonNeg ↔ n + 1 ≤ 0
Theorem: Int.nonNeg_mk
Proof state before:
case zero_succ
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ -[n+1].NonNeg ↔ n + 1 ≤ 0
Tactic:
constructor
Proof state after:
case zero_succ.mp
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ -[n+1].NonNeg → n + 1 ≤ 0

case zero_succ.mpr
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ n + 1 ≤ 0 → -[n+1].NonNeg
Theorem: Int.nonNeg_mk
Proof state before:
case zero_succ.mp
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ -[n+1].NonNeg → n + 1 ≤ 0
Tactic:
intro
Proof state after:
case zero_succ.mp
n : Nat
a✝¹ : (0 ⊖ n).NonNeg ↔ n ≤ 0
a✝ : -[n+1].NonNeg
⊢ n + 1 ≤ 0
Theorem: Int.nonNeg_mk
Proof state before:
case zero_succ.mp
n : Nat
a✝¹ : (0 ⊖ n).NonNeg ↔ n ≤ 0
a✝ : -[n+1].NonNeg
⊢ n + 1 ≤ 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Int.nonNeg_mk
Proof state before:
case zero_succ.mpr
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ n + 1 ≤ 0 → -[n+1].NonNeg
Tactic:
intro
Proof state after:
case zero_succ.mpr
n : Nat
a✝¹ : (0 ⊖ n).NonNeg ↔ n ≤ 0
a✝ : n + 1 ≤ 0
⊢ -[n+1].NonNeg
Theorem: Int.nonNeg_mk
Proof state before:
case zero_succ.mpr
n : Nat
a✝¹ : (0 ⊖ n).NonNeg ↔ n ≤ 0
a✝ : n + 1 ≤ 0
⊢ -[n+1].NonNeg
Tactic:
contradiction
Proof state after:
no goals
Theorem: Int.nonNeg_mk
Proof state before:
case succ_zero
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ (m + 1 ⊖ 0).NonNeg ↔ 0 ≤ m + 1
Tactic:
rw [succ_mk_zero]
Proof state after:
case succ_zero
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ (ofNat (m + 1)).NonNeg ↔ 0 ≤ m + 1
Theorem: Int.nonNeg_mk
Proof state before:
case succ_zero
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ (ofNat (m + 1)).NonNeg ↔ 0 ≤ m + 1
Tactic:
constructor
Proof state after:
case succ_zero.mp
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ (ofNat (m + 1)).NonNeg → 0 ≤ m + 1

case succ_zero.mpr
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ 0 ≤ m + 1 → (ofNat (m + 1)).NonNeg
Theorem: Int.nonNeg_mk
Proof state before:
case succ_zero.mp
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ (ofNat (m + 1)).NonNeg → 0 ≤ m + 1
Tactic:
intro
Proof state after:
case succ_zero.mp
m : Nat
a✝¹ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
a✝ : (ofNat (m + 1)).NonNeg
⊢ 0 ≤ m + 1
Theorem: Int.nonNeg_mk
Proof state before:
case succ_zero.mp
m : Nat
a✝¹ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
a✝ : (ofNat (m + 1)).NonNeg
⊢ 0 ≤ m + 1
Tactic:
apply Nat.zero_le
Proof state after:
no goals
Theorem: Int.nonNeg_mk
Proof state before:
case succ_zero.mpr
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ 0 ≤ m + 1 → (ofNat (m + 1)).NonNeg
Tactic:
intro
Proof state after:
case succ_zero.mpr
m : Nat
a✝¹ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
a✝ : 0 ≤ m + 1
⊢ (ofNat (m + 1)).NonNeg
Theorem: Int.nonNeg_mk
Proof state before:
case succ_zero.mpr
m : Nat
a✝¹ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
a✝ : 0 ≤ m + 1
⊢ (ofNat (m + 1)).NonNeg
Tactic:
apply NonNeg.mk
Proof state after:
no goals
Theorem: Int.nonNeg_mk
Proof state before:
case succ_succ
m n : Nat
ih : (m ⊖ n).NonNeg ↔ n ≤ m
⊢ (m + 1 ⊖ n + 1).NonNeg ↔ n + 1 ≤ m + 1
Tactic:
rw [succ_mk_succ]
Proof state after:
case succ_succ
m n : Nat
ih : (m ⊖ n).NonNeg ↔ n ≤ m
⊢ (m ⊖ n).NonNeg ↔ n + 1 ≤ m + 1
Theorem: Int.nonNeg_mk
Proof state before:
case succ_succ
m n : Nat
ih : (m ⊖ n).NonNeg ↔ n ≤ m
⊢ (m ⊖ n).NonNeg ↔ n + 1 ≤ m + 1
Tactic:
rw [Nat.succ_le_succ_iff]
Proof state after:
case succ_succ
m n : Nat
ih : (m ⊖ n).NonNeg ↔ n ≤ m
⊢ (m ⊖ n).NonNeg ↔ n ≤ m
Theorem: Int.nonNeg_mk
Proof state before:
case succ_succ
m n : Nat
ih : (m ⊖ n).NonNeg ↔ n ≤ m
⊢ (m ⊖ n).NonNeg ↔ n ≤ m
Tactic:
exact ih
Proof state after:
no goals
Theorem: Int.mk_le_mk
Proof state before:
m₁ n₁ m₂ n₂ : Nat
⊢ m₁ ⊖ n₁ ≤ m₂ ⊖ n₂ ↔ n₂ + m₁ ≤ m₂ + n₁
Tactic:
simp only [LE.le, Int.le]
Proof state after:
m₁ n₁ m₂ n₂ : Nat
⊢ ((m₂ ⊖ n₂) - (m₁ ⊖ n₁)).NonNeg ↔ (n₂ + m₁).le (m₂ + n₁)
Theorem: Int.mk_le_mk
Proof state before:
m₁ n₁ m₂ n₂ : Nat
⊢ ((m₂ ⊖ n₂) - (m₁ ⊖ n₁)).NonNeg ↔ (n₂ + m₁).le (m₂ + n₁)
Tactic:
rw [mk_sub_mk, nonNeg_mk]
Proof state after:
m₁ n₁ m₂ n₂ : Nat
⊢ n₂ + m₁ ≤ m₂ + n₁ ↔ (n₂ + m₁).le (m₂ + n₁)
Theorem: Int.mk_le_mk
Proof state before:
m₁ n₁ m₂ n₂ : Nat
⊢ n₂ + m₁ ≤ m₂ + n₁ ↔ (n₂ + m₁).le (m₂ + n₁)
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_lt_mk
Proof state before:
m₁ n₁ m₂ n₂ : Nat
⊢ m₁ ⊖ n₁ < m₂ ⊖ n₂ ↔ n₂ + m₁ < m₂ + n₁
Tactic:
simp only [LT.lt, Int.lt, Nat.lt]
Proof state after:
m₁ n₁ m₂ n₂ : Nat
⊢ (m₁ ⊖ n₁) + 1 ≤ m₂ ⊖ n₂ ↔ (n₂ + m₁).succ.le (m₂ + n₁)
Theorem: Int.mk_lt_mk
Proof state before:
m₁ n₁ m₂ n₂ : Nat
⊢ (m₁ ⊖ n₁) + 1 ≤ m₂ ⊖ n₂ ↔ (n₂ + m₁).succ.le (m₂ + n₁)
Tactic:
rw [←one_mk_zero, mk_add_mk, mk_le_mk, Nat.add_succ, Nat.add_zero]
Proof state after:
m₁ n₁ m₂ n₂ : Nat
⊢ (n₂ + m₁).succ ≤ m₂ + n₁ ↔ (n₂ + m₁).succ.le (m₂ + n₁)
Theorem: Int.mk_lt_mk
Proof state before:
m₁ n₁ m₂ n₂ : Nat
⊢ (n₂ + m₁).succ ≤ m₂ + n₁ ↔ (n₂ + m₁).succ.le (m₂ + n₁)
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.add_neg_self_left
Proof state before:
i : Int
⊢ -i + i = 0
Tactic:
cases i using Int.casesMkOn with
| mk mi ni => rw [neg_mk, mk_add_mk, Nat.add_comm mi ni, mk_self]
Proof state after:
no goals
Theorem: Int.add_neg_self_left
Proof state before:
case mk
mi ni : Nat
⊢ -(mi ⊖ ni) + (mi ⊖ ni) = 0
Tactic:
rw [neg_mk, mk_add_mk, Nat.add_comm mi ni, mk_self]
Proof state after:
no goals
Theorem: Int.add_neg_self_right
Proof state before:
i : Int
⊢ i + -i = 0
Tactic:
cases i using Int.casesMkOn with
| mk mi ni => rw [neg_mk, mk_add_mk, Nat.add_comm mi ni, mk_self]
Proof state after:
no goals
Theorem: Int.add_neg_self_right
Proof state before:
case mk
mi ni : Nat
⊢ (mi ⊖ ni) + -(mi ⊖ ni) = 0
Tactic:
rw [neg_mk, mk_add_mk, Nat.add_comm mi ni, mk_self]
Proof state after:
no goals
Theorem: Int.sub_add_assoc
Proof state before:
i j k : Int
⊢ i - j + k = i + -j + k
Tactic:
rw [Int.sub_eq]
Proof state after:
no goals
Theorem: Int.sub_add_assoc
Proof state before:
i j k : Int
⊢ i + -j + k = i + (-j + k)
Tactic:
rw [Int.add_assoc]
Proof state after:
no goals
Theorem: Int.sub_add_assoc
Proof state before:
i j k : Int
⊢ i + (-j + k) = i + (-j + - -k)
Tactic:
rw [Int.neg_neg]
Proof state after:
no goals
Theorem: Int.sub_add_assoc
Proof state before:
i j k : Int
⊢ i + (-j + - -k) = i + -(j + -k)
Tactic:
rw [Int.neg_add]
Proof state after:
no goals
Theorem: Int.sub_add_assoc
Proof state before:
i j k : Int
⊢ i + -(j + -k) = i - (j - k)
Tactic:
rw [Int.sub_eq, Int.sub_eq]
Proof state after:
no goals
Theorem: Int.mk_mul_ofNat
Proof state before:
m n k : Nat
⊢ (m ⊖ n) * ofNat k = m * k ⊖ n * k
Tactic:
induction m, n with
| zero_zero => rw [Nat.zero_mul, zero_mk_zero, Int.zero_mul]
| zero_succ n => rw [Nat.zero_mul, zero_mk, zero_mk]; rfl
| succ_zero m => rw [Nat.zero_mul, mk_zero, mk_zero]; rfl
| succ_succ m n ih => rw [Nat.succ_mul, Nat.succ_mul, succ_mk_succ, add_mk_add_right]; exact ih
Proof state after:
no goals
Theorem: Int.mk_mul_ofNat
Proof state before:
case zero_zero
k : Nat
⊢ (0 ⊖ 0) * ofNat k = 0 * k ⊖ 0 * k
Tactic:
rw [Nat.zero_mul, zero_mk_zero, Int.zero_mul]
Proof state after:
no goals
Theorem: Int.mk_mul_ofNat
Proof state before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) * ofNat k = 0 * k ⊖ n * k
⊢ (0 ⊖ n + 1) * ofNat k = 0 * k ⊖ (n + 1) * k
Tactic:
rw [Nat.zero_mul, zero_mk, zero_mk]
Proof state after:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) * ofNat k = 0 * k ⊖ n * k
⊢ negOfNat (n + 1) * ofNat k = negOfNat ((n + 1) * k)
Theorem: Int.mk_mul_ofNat
Proof state before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) * ofNat k = 0 * k ⊖ n * k
⊢ negOfNat (n + 1) * ofNat k = negOfNat ((n + 1) * k)
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_mul_ofNat
Proof state before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) * ofNat k = m * k ⊖ 0 * k
⊢ (m + 1 ⊖ 0) * ofNat k = (m + 1) * k ⊖ 0 * k
Tactic:
rw [Nat.zero_mul, mk_zero, mk_zero]
Proof state after:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) * ofNat k = m * k ⊖ 0 * k
⊢ ofNat (m + 1) * ofNat k = ofNat ((m + 1) * k)
Theorem: Int.mk_mul_ofNat
Proof state before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) * ofNat k = m * k ⊖ 0 * k
⊢ ofNat (m + 1) * ofNat k = ofNat ((m + 1) * k)
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_mul_ofNat
Proof state before:
case succ_succ
k m n : Nat
ih : (m ⊖ n) * ofNat k = m * k ⊖ n * k
⊢ (m + 1 ⊖ n + 1) * ofNat k = (m + 1) * k ⊖ (n + 1) * k
Tactic:
rw [Nat.succ_mul, Nat.succ_mul, succ_mk_succ, add_mk_add_right]
Proof state after:
case succ_succ
k m n : Nat
ih : (m ⊖ n) * ofNat k = m * k ⊖ n * k
⊢ (m ⊖ n) * ofNat k = m * k ⊖ n * k
Theorem: Int.mk_mul_ofNat
Proof state before:
case succ_succ
k m n : Nat
ih : (m ⊖ n) * ofNat k = m * k ⊖ n * k
⊢ (m ⊖ n) * ofNat k = m * k ⊖ n * k
Tactic:
exact ih
Proof state after:
no goals
Theorem: Int.mk_mul_negSucc
Proof state before:
m n k : Nat
⊢ (m ⊖ n) * -[k+1] = n * (k + 1) ⊖ m * (k + 1)
Tactic:
induction m, n with
| zero_zero => rw [Nat.zero_mul, zero_mk_zero, Int.zero_mul]
| zero_succ n => rw [Nat.zero_mul, zero_mk, mk_zero]; rfl
| succ_zero m => rw [Nat.zero_mul, mk_zero, zero_mk]; rfl
| succ_succ m n ih => rw [Nat.succ_mul, Nat.succ_mul, succ_mk_succ, add_mk_add_right]; exact ih
Proof state after:
no goals
Theorem: Int.mk_mul_negSucc
Proof state before:
case zero_zero
k : Nat
⊢ (0 ⊖ 0) * -[k+1] = 0 * (k + 1) ⊖ 0 * (k + 1)
Tactic:
rw [Nat.zero_mul, zero_mk_zero, Int.zero_mul]
Proof state after:
no goals
Theorem: Int.mk_mul_negSucc
Proof state before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) * -[k+1] = n * (k + 1) ⊖ 0 * (k + 1)
⊢ (0 ⊖ n + 1) * -[k+1] = (n + 1) * (k + 1) ⊖ 0 * (k + 1)
Tactic:
rw [Nat.zero_mul, zero_mk, mk_zero]
Proof state after:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) * -[k+1] = n * (k + 1) ⊖ 0 * (k + 1)
⊢ negOfNat (n + 1) * -[k+1] = ofNat ((n + 1) * (k + 1))
Theorem: Int.mk_mul_negSucc
Proof state before:
case zero_succ
k n : Nat
a✝ : (0 ⊖ n) * -[k+1] = n * (k + 1) ⊖ 0 * (k + 1)
⊢ negOfNat (n + 1) * -[k+1] = ofNat ((n + 1) * (k + 1))
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_mul_negSucc
Proof state before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) * -[k+1] = 0 * (k + 1) ⊖ m * (k + 1)
⊢ (m + 1 ⊖ 0) * -[k+1] = 0 * (k + 1) ⊖ (m + 1) * (k + 1)
Tactic:
rw [Nat.zero_mul, mk_zero, zero_mk]
Proof state after:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) * -[k+1] = 0 * (k + 1) ⊖ m * (k + 1)
⊢ ofNat (m + 1) * -[k+1] = negOfNat ((m + 1) * (k + 1))
Theorem: Int.mk_mul_negSucc
Proof state before:
case succ_zero
k m : Nat
a✝ : (m ⊖ 0) * -[k+1] = 0 * (k + 1) ⊖ m * (k + 1)
⊢ ofNat (m + 1) * -[k+1] = negOfNat ((m + 1) * (k + 1))
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.mk_mul_negSucc
Proof state before:
case succ_succ
k m n : Nat
ih : (m ⊖ n) * -[k+1] = n * (k + 1) ⊖ m * (k + 1)
⊢ (m + 1 ⊖ n + 1) * -[k+1] = (n + 1) * (k + 1) ⊖ (m + 1) * (k + 1)
Tactic:
rw [Nat.succ_mul, Nat.succ_mul, succ_mk_succ, add_mk_add_right]
Proof state after:
case succ_succ
k m n : Nat
ih : (m ⊖ n) * -[k+1] = n * (k + 1) ⊖ m * (k + 1)
⊢ (m ⊖ n) * -[k+1] = n * (k + 1) ⊖ m * (k + 1)
Theorem: Int.mk_mul_negSucc
Proof state before:
case succ_succ
k m n : Nat
ih : (m ⊖ n) * -[k+1] = n * (k + 1) ⊖ m * (k + 1)
⊢ (m ⊖ n) * -[k+1] = n * (k + 1) ⊖ m * (k + 1)
Tactic:
exact ih
Proof state after:
no goals
Theorem: Int.mk_mul_mk
Proof state before:
m₁ n₁ m₂ n₂ : Nat
⊢ (m₁ ⊖ n₁) * (m₂ ⊖ n₂) = m₁ * m₂ + n₁ * n₂ ⊖ m₁ * n₂ + n₁ * m₂
Tactic:
induction m₂, n₂ with
| zero_zero => simp only [Nat.zero_mul, Nat.mul_zero, Nat.add_zero, Nat.zero_add, zero_mk_zero, Int.mul_zero]
| zero_succ n₂ => simp only [Nat.zero_mul, Nat.mul_zero, Nat.add_zero, Nat.zero_add, zero_mk_succ, mk_mul_negSucc]
| succ_zero m₂ => simp only [Nat.zero_mul, Nat.mul_zero, Nat.add_zero, Nat.zero_add, succ_mk_zero, mk_mul_ofNat, Nat.mul_comm]
| succ_succ m₂ n₂ ih => simp only [Nat.mul_succ, Nat.succ_mul]; rw [succ_mk_succ, Nat.add_add_add_comm _ m₁ _ n₁, Nat.add_add_add_comm _ m₁ _ n₁, add_mk_add_right]; exact ih
Proof state after:
no goals
Theorem: Int.mk_mul_mk
Proof state before:
case zero_zero
m₁ n₁ : Nat
⊢ (m₁ ⊖ n₁) * (0 ⊖ 0) = m₁ * 0 + n₁ * 0 ⊖ m₁ * 0 + n₁ * 0
Tactic:
simp only [Nat.zero_mul, Nat.mul_zero, Nat.add_zero, Nat.zero_add, zero_mk_zero, Int.mul_zero]
Proof state after:
no goals
Theorem: Int.mk_mul_mk
Proof state before:
case zero_succ
m₁ n₁ n₂ : Nat
a✝ : (m₁ ⊖ n₁) * (0 ⊖ n₂) = m₁ * 0 + n₁ * n₂ ⊖ m₁ * n₂ + n₁ * 0
⊢ (m₁ ⊖ n₁) * (0 ⊖ n₂ + 1) = m₁ * 0 + n₁ * (n₂ + 1) ⊖ m₁ * (n₂ + 1) + n₁ * 0
Tactic:
simp only [Nat.zero_mul, Nat.mul_zero, Nat.add_zero, Nat.zero_add, zero_mk_succ, mk_mul_negSucc]
Proof state after:
no goals
Theorem: Int.mk_mul_mk
Proof state before:
case succ_zero
m₁ n₁ m₂ : Nat
a✝ : (m₁ ⊖ n₁) * (m₂ ⊖ 0) = m₁ * m₂ + n₁ * 0 ⊖ m₁ * 0 + n₁ * m₂
⊢ (m₁ ⊖ n₁) * (m₂ + 1 ⊖ 0) = m₁ * (m₂ + 1) + n₁ * 0 ⊖ m₁ * 0 + n₁ * (m₂ + 1)
Tactic:
simp only [Nat.zero_mul, Nat.mul_zero, Nat.add_zero, Nat.zero_add, succ_mk_zero, mk_mul_ofNat, Nat.mul_comm]
Proof state after:
no goals
Theorem: Int.mk_mul_mk
Proof state before:
case succ_succ
m₁ n₁ m₂ n₂ : Nat
ih : (m₁ ⊖ n₁) * (m₂ ⊖ n₂) = m₁ * m₂ + n₁ * n₂ ⊖ m₁ * n₂ + n₁ * m₂
⊢ (m₁ ⊖ n₁) * (m₂ + 1 ⊖ n₂ + 1) = m₁ * (m₂ + 1) + n₁ * (n₂ + 1) ⊖ m₁ * (n₂ + 1) + n₁ * (m₂ + 1)
Tactic:
simp only [Nat.mul_succ, Nat.succ_mul]
Proof state after:
case succ_succ
m₁ n₁ m₂ n₂ : Nat
ih : (m₁ ⊖ n₁) * (m₂ ⊖ n₂) = m₁ * m₂ + n₁ * n₂ ⊖ m₁ * n₂ + n₁ * m₂
⊢ (m₁ ⊖ n₁) * (m₂ + 1 ⊖ n₂ + 1) = m₁ * m₂ + m₁ + (n₁ * n₂ + n₁) ⊖ m₁ * n₂ + m₁ + (n₁ * m₂ + n₁)
Theorem: Int.mk_mul_mk
Proof state before:
case succ_succ
m₁ n₁ m₂ n₂ : Nat
ih : (m₁ ⊖ n₁) * (m₂ ⊖ n₂) = m₁ * m₂ + n₁ * n₂ ⊖ m₁ * n₂ + n₁ * m₂
⊢ (m₁ ⊖ n₁) * (m₂ + 1 ⊖ n₂ + 1) = m₁ * m₂ + m₁ + (n₁ * n₂ + n₁) ⊖ m₁ * n₂ + m₁ + (n₁ * m₂ + n₁)
Tactic:
rw [succ_mk_succ, Nat.add_add_add_comm _ m₁ _ n₁, Nat.add_add_add_comm _ m₁ _ n₁, add_mk_add_right]
Proof state after:
case succ_succ
m₁ n₁ m₂ n₂ : Nat
ih : (m₁ ⊖ n₁) * (m₂ ⊖ n₂) = m₁ * m₂ + n₁ * n₂ ⊖ m₁ * n₂ + n₁ * m₂
⊢ (m₁ ⊖ n₁) * (m₂ ⊖ n₂) = m₁ * m₂ + n₁ * n₂ ⊖ m₁ * n₂ + n₁ * m₂
Theorem: Int.mk_mul_mk
Proof state before:
case succ_succ
m₁ n₁ m₂ n₂ : Nat
ih : (m₁ ⊖ n₁) * (m₂ ⊖ n₂) = m₁ * m₂ + n₁ * n₂ ⊖ m₁ * n₂ + n₁ * m₂
⊢ (m₁ ⊖ n₁) * (m₂ ⊖ n₂) = m₁ * m₂ + n₁ * n₂ ⊖ m₁ * n₂ + n₁ * m₂
Tactic:
exact ih
Proof state after:
no goals
Theorem: congr_ndrec
Proof state before:
α : Sort u_1
γ : Sort u_2
x x' : α
β : α → Sort u_3
f : (x : α) → β x → γ
h : x = x'
y : β x
⊢ f x' (h ▸ y) = f x y
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
γ : Sort u_2
x : α
β : α → Sort u_3
f : (x : α) → β x → γ
y : β x
⊢ f x (⋯ ▸ y) = f x y
Theorem: congr_ndrec
Proof state before:
case refl
α : Sort u_1
γ : Sort u_2
x : α
β : α → Sort u_3
f : (x : α) → β x → γ
y : β x
⊢ f x (⋯ ▸ y) = f x y
Tactic:
rfl
Proof state after:
no goals
Theorem: dcast_id
Proof state before:
α : Sort u_1
a : α
motive : α → Sort u_2
h : a = a
t : motive a
⊢ dcast h t = t
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
a : α
motive : α → Sort u_2
t : motive a
⊢ dcast ⋯ t = t
Theorem: dcast_id
Proof state before:
case refl
α : Sort u_1
a : α
motive : α → Sort u_2
t : motive a
⊢ dcast ⋯ t = t
Tactic:
rfl
Proof state after:
no goals
Theorem: dcast_comp
Proof state before:
α : Sort u_1
a b c : α
motive : α → Sort u_2
hab : a = b
hbc : b = c
t : motive a
⊢ dcast hbc (dcast hab t) = dcast ⋯ t
Tactic:
cases hab
Proof state after:
case refl
α : Sort u_1
a c : α
motive : α → Sort u_2
t : motive a
hbc : a = c
⊢ dcast hbc (dcast ⋯ t) = dcast ⋯ t
Theorem: dcast_comp
Proof state before:
case refl
α : Sort u_1
a c : α
motive : α → Sort u_2
t : motive a
hbc : a = c
⊢ dcast hbc (dcast ⋯ t) = dcast ⋯ t
Tactic:
rfl
Proof state after:
no goals
Theorem: deq_dcast_left
Proof state before:
α : Sort u_1
a b c : α
motive : α → Sort u_2
h : a = b
t : motive a
u : motive c
⊢ DEq (dcast h t) u ↔ DEq t u
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
a c : α
motive : α → Sort u_2
t : motive a
u : motive c
⊢ DEq (dcast ⋯ t) u ↔ DEq t u
Theorem: deq_dcast_left
Proof state before:
case refl
α : Sort u_1
a c : α
motive : α → Sort u_2
t : motive a
u : motive c
⊢ DEq (dcast ⋯ t) u ↔ DEq t u
Tactic:
rfl
Proof state after:
no goals
Theorem: deq_dcast_right
Proof state before:
α : Sort u_1
b c a : α
motive : α → Sort u_2
h : b = c
t : motive a
u : motive b
⊢ DEq t (dcast h u) ↔ DEq t u
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
b a : α
motive : α → Sort u_2
t : motive a
u : motive b
⊢ DEq t (dcast ⋯ u) ↔ DEq t u
Theorem: deq_dcast_right
Proof state before:
case refl
α : Sort u_1
b a : α
motive : α → Sort u_2
t : motive a
u : motive b
⊢ DEq t (dcast ⋯ u) ↔ DEq t u
Tactic:
rfl
Proof state after:
no goals
Theorem: heq_dcast_left
Proof state before:
α : Sort u_1
a b c : α
motive : α → Sort u_2
h : a = b
t : motive a
u : motive c
⊢ HEq (dcast h t) u ↔ HEq t u
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
a c : α
motive : α → Sort u_2
t : motive a
u : motive c
⊢ HEq (dcast ⋯ t) u ↔ HEq t u
Theorem: heq_dcast_left
Proof state before:
case refl
α : Sort u_1
a c : α
motive : α → Sort u_2
t : motive a
u : motive c
⊢ HEq (dcast ⋯ t) u ↔ HEq t u
Tactic:
rfl
Proof state after:
no goals
Theorem: heq_dcast_right
Proof state before:
α : Sort u_1
b c a : α
motive : α → Sort u_2
h : b = c
t : motive a
u : motive b
⊢ HEq t (dcast h u) ↔ HEq t u
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
b a : α
motive : α → Sort u_2
t : motive a
u : motive b
⊢ HEq t (dcast ⋯ u) ↔ HEq t u
Theorem: heq_dcast_right
Proof state before:
case refl
α : Sort u_1
b a : α
motive : α → Sort u_2
t : motive a
u : motive b
⊢ HEq t (dcast ⋯ u) ↔ HEq t u
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.unappend_append
Proof state before:
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
⊢ (append i).unappend = i
Tactic:
induction xs generalizing ys with
| nil =>
  match i with
  | .inl i => contradiction
  | .inr j => rfl
| cons x xs ih =>
  match i with
  | .inl .head => rfl
  | .inl (.tail i) => simp only [append, unappend, ih]
  | .inr j => simp only [append, unappend, ih]
Proof state after:
no goals
Theorem: List.Index.unappend_append
Proof state before:
case nil
α✝ : Type u_1
ys : List α✝
i : [].Index ⊕ ys.Index
⊢ (append i).unappend = i
Tactic:
match i with
| .inl i => contradiction
| .inr j => rfl
Proof state after:
no goals
Theorem: List.Index.unappend_append
Proof state before:
α✝ : Type u_1
ys : List α✝
i✝ : [].Index ⊕ ys.Index
i : [].Index
⊢ (append (Sum.inl i)).unappend = Sum.inl i
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.unappend_append
Proof state before:
α✝ : Type u_1
ys : List α✝
i : [].Index ⊕ ys.Index
j : ys.Index
⊢ (append (Sum.inr j)).unappend = Sum.inr j
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.unappend_append
Proof state before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (i : xs.Index ⊕ ys.Index), (append i).unappend = i
ys : List α✝
i : (x :: xs).Index ⊕ ys.Index
⊢ (append i).unappend = i
Tactic:
match i with
| .inl .head => rfl
| .inl (.tail i) => simp only [append, unappend, ih]
| .inr j => simp only [append, unappend, ih]
Proof state after:
no goals
Theorem: List.Index.unappend_append
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (i : xs.Index ⊕ ys.Index), (append i).unappend = i
ys : List α✝
i : (x :: xs).Index ⊕ ys.Index
⊢ (append (Sum.inl head)).unappend = Sum.inl head
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.unappend_append
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (i : xs.Index ⊕ ys.Index), (append i).unappend = i
ys : List α✝
i✝ : (x :: xs).Index ⊕ ys.Index
i : xs.Index
⊢ (append (Sum.inl i.tail)).unappend = Sum.inl i.tail
Tactic:
simp only [append, unappend, ih]
Proof state after:
no goals