internlm/Lean-Github huggingface dataset:
Theorem: Nat.tri_add_inj
Proof state before:
case h.right.left.a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂ < n₁
Tactic:
exact Nat.gt_of_not_le hgt
Proof state after:
no goals
Theorem: Nat.tri_add_inj
Proof state before:
case h.right.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₁.tri ≤ n₁.tri + m₁
Tactic:
exact Nat.le_add_right ..
Proof state after:
no goals
Theorem: Nat.pair_succ_right
Proof state before:
x y : Nat
⊢ x.pair (y + 1) = (x + y).tri + (x + y) + 1 + x
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.pair_succ_right
Proof state before:
x y : Nat
⊢ (x + y).tri + (x + y) + 1 + x = (x + y).tri + (x + y) + x + 1
Tactic:
rw [Nat.add_right_comm _ x 1]
Proof state after:
no goals
Theorem: Nat.pair_succ_right
Proof state before:
x y : Nat
⊢ (x + y).tri + (x + y) + x + 1 = (x + y).tri + x + (x + y) + 1
Tactic:
rw [Nat.add_right_comm _ (x+y) x]
Proof state after:
no goals
Theorem: Nat.pair_zero_left
Proof state before:
y : Nat
⊢ pair 0 y = (0 + y).tri
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.pair_zero_left
Proof state before:
y : Nat
⊢ (0 + y).tri = y.tri
Tactic:
rw [Nat.zero_add]
Proof state after:
no goals
Theorem: Nat.pair_succ_left
Proof state before:
x y : Nat
⊢ (x + 1).pair y = (x + 1 + y).tri + (x + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.pair_succ_left
Proof state before:
x y : Nat
⊢ (x + 1 + y).tri + (x + 1) = (x + y + 1).tri + (x + 1)
Tactic:
rw [Nat.add_right_comm _ y 1]
Proof state after:
no goals
Theorem: Nat.pair_succ_left
Proof state before:
x y : Nat
⊢ (x + y + 1).tri + (x + 1) = (x + y).tri + (x + y) + 1 + (x + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.pair_succ_left
Proof state before:
x y : Nat
⊢ (x + y).tri + (x + y) + 1 + (x + 1) = (x + y).tri + x + y + 1 + (x + 1)
Tactic:
rw [Nat.add_assoc _ x y]
Proof state after:
no goals
Theorem: Nat.pair_succ_left
Proof state before:
x y : Nat
⊢ (x + y).tri + x + y + 1 + (x + 1) = x.pair y + y + 1 + (x + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.pair_succ_left
Proof state before:
x y : Nat
⊢ x.pair y + y + 1 + (x + 1) = x.pair y + y + (x + 1) + 1
Tactic:
rw [Nat.add_right_comm _ (x+1) 1]
Proof state after:
no goals
Theorem: Nat.pair_succ_left
Proof state before:
x y : Nat
⊢ x.pair y + y + (x + 1) + 1 = x.pair y + y + x + 1 + 1
Tactic:
rw [Nat.add_assoc _ x 1]
Proof state after:
no goals
Theorem: Nat.pair_succ_left
Proof state before:
x y : Nat
⊢ x.pair y + y + x + 1 + 1 = x.pair y + (y + x) + 1 + 1
Tactic:
rw [Nat.add_assoc _ y x]
Proof state after:
no goals
Theorem: Nat.pair_succ_left
Proof state before:
x y : Nat
⊢ x.pair y + (y + x) + 1 + 1 = x.pair y + (x + y) + 1 + 1
Tactic:
rw [Nat.add_comm x y]
Proof state after:
no goals
Theorem: Nat.split_eq
Proof state before:
case zero

⊢ (split 0).fst.tri + ↑(split 0).snd = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.split_eq
Proof state before:
case succ
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ (n + 1).split.fst.tri + ↑(n + 1).split.snd = n + 1
Tactic:
symmetry
Proof state after:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ n + 1 = (n + 1).split.fst.tri + ↑(n + 1).split.snd
Theorem: Nat.split_eq
Proof state before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ n + 1 = (n + 1).split.fst.tri + ↑(n + 1).split.snd
Tactic:
transitivity (tri (split n).fst + ((split n).snd + 1))
Proof state after:
case left
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ n + 1 = n.split.fst.tri + (↑n.split.snd + 1)

case right
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ n.split.fst.tri + (↑n.split.snd + 1) = (n + 1).split.fst.tri + ↑(n + 1).split.snd
Theorem: Nat.split_eq
Proof state before:
case left
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ n + 1 = n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
rw [←Nat.add_assoc (tri (split n).fst) (split n).snd 1, H]
Proof state after:
no goals
Theorem: Nat.split_eq
Proof state before:
case right
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ n.split.fst.tri + (↑n.split.snd + 1) = (n + 1).split.fst.tri + ↑(n + 1).split.snd
Tactic:
symmetry
Proof state after:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ (n + 1).split.fst.tri + ↑(n + 1).split.snd = n.split.fst.tri + (↑n.split.snd + 1)
Theorem: Nat.split_eq
Proof state before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ (n + 1).split.fst.tri + ↑(n + 1).split.snd = n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
simp only [split]
Proof state after:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ (if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Theorem: Nat.split_eq
Proof state before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ (if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
split
Proof state after:
case isTrue
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)

case isFalse
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Theorem: Nat.split_eq
Proof state before:
case isTrue
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)

case isFalse
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
next h =>
  dsimp only [Nat.add_eq] at h ⊢
  rw [dif_pos h]
Proof state after:
case isFalse
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Theorem: Nat.split_eq
Proof state before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h : ↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
dsimp only [Nat.add_eq] at h ⊢
Proof state after:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h : ↑n.split.2 < n.split.fst
⊢ n.split.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Theorem: Nat.split_eq
Proof state before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h : ↑n.split.2 < n.split.fst
⊢ n.split.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
rw [dif_pos h]
Proof state after:
no goals
Theorem: Nat.split_eq
Proof state before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h : ¬↑n.split.2 < n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
have h : ¬((split n).snd.val < (split n).fst) := h
Proof state after:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Theorem: Nat.split_eq
Proof state before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
heq : ↑n.split.snd = n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)
Tactic:
rw [dif_neg h, ←Nat.add_assoc, heq]
Proof state after:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
heq : ↑n.split.snd = n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri + ↑⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.snd = n.split.fst.tri + n.split.fst + 1
Theorem: Nat.split_eq
Proof state before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
heq : ↑n.split.snd = n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri + ↑⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.snd = n.split.fst.tri + n.split.fst + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.split_eq
Proof state before:
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
⊢ ↑n.split.snd = n.split.fst
Tactic:
apply Nat.le_antisymm
Proof state after:
case h₁
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
⊢ ↑n.split.snd ≤ n.split.fst

case h₂
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
⊢ n.split.fst ≤ ↑n.split.snd
Theorem: Nat.split_eq
Proof state before:
case h₁
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
⊢ ↑n.split.snd ≤ n.split.fst
Tactic:
exact Nat.le_of_lt_succ (split n).snd.isLt
Proof state after:
no goals
Theorem: Nat.split_eq
Proof state before:
case h₂
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
⊢ n.split.fst ≤ ↑n.split.snd
Tactic:
exact Nat.le_of_not_gt h
Proof state after:
no goals
Theorem: Nat.split_pair_fst
Proof state before:
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ ⟨t, ⟨s, hs⟩⟩.fst = x + y
Tactic:
apply Nat.tri_add_inj (Nat.le_of_lt_succ hs) (Nat.le_add_right x y)
Proof state after:
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + s = (x + y).tri + x
Theorem: Nat.split_pair_fst
Proof state before:
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + s = (x + y).tri + x
Tactic:
transitivity (tri (split (pair x y)).fst + (split (pair x y)).snd)
Proof state after:
case left
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + s = (x.pair y).split.fst.tri + ↑(x.pair y).split.snd

case right
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ (x.pair y).split.fst.tri + ↑(x.pair y).split.snd = (x + y).tri + x
Theorem: Nat.split_pair_fst
Proof state before:
case left
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + s = (x.pair y).split.fst.tri + ↑(x.pair y).split.snd
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Nat.split_pair_fst
Proof state before:
case right
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ (x.pair y).split.fst.tri + ↑(x.pair y).split.snd = (x + y).tri + x
Tactic:
rw [split_eq, pair]
Proof state after:
no goals
Theorem: Nat.split_pair_snd
Proof state before:
x y : Nat
⊢ ↑(x.pair y).split.snd = x
Tactic:
apply Nat.add_left_cancel (n:=tri (split (pair x y)).fst)
Proof state after:
x y : Nat
⊢ (x.pair y).split.fst.tri + ↑(x.pair y).split.snd = (x.pair y).split.fst.tri + x
Theorem: Nat.split_pair_snd
Proof state before:
x y : Nat
⊢ (x.pair y).split.fst.tri + ↑(x.pair y).split.snd = (x.pair y).split.fst.tri + x
Tactic:
rw [split_eq, split_pair_fst, pair]
Proof state after:
no goals
Theorem: Nat.snd_pair
Proof state before:
x y : Nat
⊢ (x.pair y).snd = y
Tactic:
unfold Nat.snd
Proof state after:
x y : Nat
⊢ (x.pair y).split.fst - ↑(x.pair y).split.snd = y
Theorem: Nat.snd_pair
Proof state before:
x y : Nat
⊢ (x.pair y).split.fst - ↑(x.pair y).split.snd = y
Tactic:
rw [Nat.split_pair_snd]
Proof state after:
x y : Nat
⊢ (x.pair y).split.fst - x = y
Theorem: Nat.snd_pair
Proof state before:
x y : Nat
⊢ (x.pair y).split.fst - x = y
Tactic:
rw [Nat.split_pair_fst]
Proof state after:
x y : Nat
⊢ x + y - x = y
Theorem: Nat.snd_pair
Proof state before:
x y : Nat
⊢ x + y - x = y
Tactic:
rw [Nat.add_sub_cancel_left]
Proof state after:
no goals
Theorem: Nat.pair_fst_snd
Proof state before:
n : Nat
⊢ n.fst.pair n.snd = n
Tactic:
unfold pair Nat.fst Nat.snd
Proof state after:
n : Nat
⊢ (↑n.split.snd + (n.split.fst - ↑n.split.snd)).tri + ↑n.split.snd = n
Theorem: Nat.pair_fst_snd
Proof state before:
n : Nat
⊢ (↑n.split.snd + (n.split.fst - ↑n.split.snd)).tri + ↑n.split.snd = n
Tactic:
match h : split n with
| ⟨t,⟨s,hs⟩⟩ =>
  rw [Nat.add_comm s, Nat.sub_add_cancel (Nat.le_of_lt_succ hs)]
  rw [←split_eq n, h]
Proof state after:
no goals
Theorem: Nat.pair_fst_snd
Proof state before:
n t s : Nat
hs : s < t + 1
h : n.split = ⟨t, ⟨s, hs⟩⟩
⊢ (↑⟨t, ⟨s, hs⟩⟩.snd + (⟨t, ⟨s, hs⟩⟩.fst - ↑⟨t, ⟨s, hs⟩⟩.snd)).tri + ↑⟨t, ⟨s, hs⟩⟩.snd = n
Tactic:
rw [Nat.add_comm s, Nat.sub_add_cancel (Nat.le_of_lt_succ hs)]
Proof state after:
n t s : Nat
hs : s < t + 1
h : n.split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + ↑⟨t, ⟨s, hs⟩⟩.snd = n
Theorem: Nat.pair_fst_snd
Proof state before:
n t s : Nat
hs : s < t + 1
h : n.split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + ↑⟨t, ⟨s, hs⟩⟩.snd = n
Tactic:
rw [←split_eq n, h]
Proof state after:
no goals
Theorem: Nat.isEven_eq_isEvenImpl
Proof state before:
⊢ isEven = Nat.isEvenImpl
Tactic:
funext n
Proof state after:
case h
n : Nat
⊢ n.isEven = Nat.isEvenImpl n
Theorem: Nat.isEven_eq_isEvenImpl
Proof state before:
case h
n : Nat
⊢ n.isEven = Nat.isEvenImpl n
Tactic:
induction n using Nat.recTwo with
| zero => rfl
| one => rfl
| step n ih =>
  unfold Nat.isEven
  rw [isEvenImpl, Nat.add_mod_right, ih]
Proof state after:
no goals
Theorem: Nat.isEven_eq_isEvenImpl
Proof state before:
case h.zero

⊢ isEven 0 = Nat.isEvenImpl 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.isEven_eq_isEvenImpl
Proof state before:
case h.one

⊢ isEven 1 = Nat.isEvenImpl 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.isEven_eq_isEvenImpl
Proof state before:
case h.step
n : Nat
ih : n.isEven = Nat.isEvenImpl n
⊢ (n + 2).isEven = Nat.isEvenImpl (n + 2)
Tactic:
unfold Nat.isEven
Proof state after:
case h.step
n : Nat
ih : n.isEven = Nat.isEvenImpl n
⊢ n.isEven = Nat.isEvenImpl (n + 2)
Theorem: Nat.isEven_eq_isEvenImpl
Proof state before:
case h.step
n : Nat
ih : n.isEven = Nat.isEvenImpl n
⊢ n.isEven = Nat.isEvenImpl (n + 2)
Tactic:
rw [isEvenImpl, Nat.add_mod_right, ih]
Proof state after:
no goals
Theorem: Nat.isEven_or_isOdd
Proof state before:
n : Nat
⊢ n.isEven = true ∨ n.isOdd = true
Tactic:
rw [←Bool.or_eq_true]
Proof state after:
n : Nat
⊢ (n.isEven || n.isOdd) = true
Theorem: Nat.isEven_or_isOdd
Proof state before:
n : Nat
⊢ (n.isEven || n.isOdd) = true
Tactic:
exact Bool.or_not_self ..
Proof state after:
no goals
Theorem: Nat.not_isOdd_eq_isEven
Proof state before:
n : Nat
⊢ (!n.isOdd) = n.isEven
Tactic:
rw [Bool.not_not]
Proof state after:
no goals
Theorem: Nat.half_eq_halfImpl
Proof state before:
⊢ half = halfImpl
Tactic:
funext n
Proof state after:
case h
n : Nat
⊢ n.half = n.halfImpl
Theorem: Nat.half_eq_halfImpl
Proof state before:
case h
n : Nat
⊢ n.half = n.halfImpl
Tactic:
induction n using Nat.recTwo with
| zero => rfl
| one => rfl
| step n ih =>
  unfold Nat.half
  rw [halfImpl, Nat.add_div_right, ih]
  nat_is_pos
Proof state after:
no goals
Theorem: Nat.half_eq_halfImpl
Proof state before:
case h.zero

⊢ half 0 = halfImpl 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.half_eq_halfImpl
Proof state before:
case h.one

⊢ half 1 = halfImpl 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.half_eq_halfImpl
Proof state before:
case h.step
n : Nat
ih : n.half = n.halfImpl
⊢ (n + 2).half = (n + 2).halfImpl
Tactic:
unfold Nat.half
Proof state after:
case h.step
n : Nat
ih : n.half = n.halfImpl
⊢ n.half + 1 = (n + 2).halfImpl
Theorem: Nat.half_eq_halfImpl
Proof state before:
case h.step
n : Nat
ih : n.half = n.halfImpl
⊢ n.half + 1 = (n + 2).halfImpl
Tactic:
rw [halfImpl, Nat.add_div_right, ih]
Proof state after:
case h.step.H
n : Nat
ih : n.half = n.halfImpl
⊢ 0 < 2
Theorem: Nat.half_eq_halfImpl
Proof state before:
case h.step.H
n : Nat
ih : n.half = n.halfImpl
⊢ 0 < 2
Tactic:
nat_is_pos
Proof state after:
no goals
Theorem: Nat.isEven_inl
Proof state before:
n : Nat
⊢ n.inl.isEven = true
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  unfold Nat.inl at ih ⊢
  rw [Nat.mul_succ]
  exact ih
Proof state after:
no goals
Theorem: Nat.isEven_inl
Proof state before:
case zero

⊢ (Nat.inl 0).isEven = true
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.isEven_inl
Proof state before:
case succ
n : Nat
ih : n.inl.isEven = true
⊢ (n + 1).inl.isEven = true
Tactic:
unfold Nat.inl at ih ⊢
Proof state after:
case succ
n : Nat
ih : (2 * n).isEven = true
⊢ (2 * (n + 1)).isEven = true
Theorem: Nat.isEven_inl
Proof state before:
case succ
n : Nat
ih : (2 * n).isEven = true
⊢ (2 * (n + 1)).isEven = true
Tactic:
rw [Nat.mul_succ]
Proof state after:
case succ
n : Nat
ih : (2 * n).isEven = true
⊢ (2 * n + 2).isEven = true
Theorem: Nat.isEven_inl
Proof state before:
case succ
n : Nat
ih : (2 * n).isEven = true
⊢ (2 * n + 2).isEven = true
Tactic:
exact ih
Proof state after:
no goals
Theorem: Nat.isOdd_inr
Proof state before:
n : Nat
⊢ n.inr.isOdd = true
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  unfold Nat.inr at ih ⊢
  rw [Nat.mul_succ]
  exact ih
Proof state after:
no goals
Theorem: Nat.isOdd_inr
Proof state before:
case zero

⊢ (Nat.inr 0).isOdd = true
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.isOdd_inr
Proof state before:
case succ
n : Nat
ih : n.inr.isOdd = true
⊢ (n + 1).inr.isOdd = true
Tactic:
unfold Nat.inr at ih ⊢
Proof state after:
case succ
n : Nat
ih : (2 * n + 1).isOdd = true
⊢ (2 * (n + 1) + 1).isOdd = true
Theorem: Nat.isOdd_inr
Proof state before:
case succ
n : Nat
ih : (2 * n + 1).isOdd = true
⊢ (2 * (n + 1) + 1).isOdd = true
Tactic:
rw [Nat.mul_succ]
Proof state after:
case succ
n : Nat
ih : (2 * n + 1).isOdd = true
⊢ (2 * n + 2 + 1).isOdd = true
Theorem: Nat.isOdd_inr
Proof state before:
case succ
n : Nat
ih : (2 * n + 1).isOdd = true
⊢ (2 * n + 2 + 1).isOdd = true
Tactic:
exact ih
Proof state after:
no goals
Theorem: Nat.half_inl_eq
Proof state before:
n : Nat
⊢ n.inl.half = n
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  unfold Nat.inl at ih ⊢
  rw [Nat.mul_succ, Nat.half, ih]
Proof state after:
no goals
Theorem: Nat.half_inl_eq
Proof state before:
case zero

⊢ (Nat.inl 0).half = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.half_inl_eq
Proof state before:
case succ
n : Nat
ih : n.inl.half = n
⊢ (n + 1).inl.half = n + 1
Tactic:
unfold Nat.inl at ih ⊢
Proof state after:
case succ
n : Nat
ih : (2 * n).half = n
⊢ (2 * (n + 1)).half = n + 1
Theorem: Nat.half_inl_eq
Proof state before:
case succ
n : Nat
ih : (2 * n).half = n
⊢ (2 * (n + 1)).half = n + 1
Tactic:
rw [Nat.mul_succ, Nat.half, ih]
Proof state after:
no goals
Theorem: Nat.half_inr_eq
Proof state before:
n : Nat
⊢ n.inr.half = n
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  unfold Nat.inr at ih ⊢
  rw [Nat.mul_succ, Nat.half, ih]
Proof state after:
no goals
Theorem: Nat.half_inr_eq
Proof state before:
case zero

⊢ (Nat.inr 0).half = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.half_inr_eq
Proof state before:
case succ
n : Nat
ih : n.inr.half = n
⊢ (n + 1).inr.half = n + 1
Tactic:
unfold Nat.inr at ih ⊢
Proof state after:
case succ
n : Nat
ih : (2 * n + 1).half = n
⊢ (2 * (n + 1) + 1).half = n + 1
Theorem: Nat.half_inr_eq
Proof state before:
case succ
n : Nat
ih : (2 * n + 1).half = n
⊢ (2 * (n + 1) + 1).half = n + 1
Tactic:
rw [Nat.mul_succ, Nat.half, ih]
Proof state after:
no goals
Theorem: Nat.inl_half_eq_of_isEven
Proof state before:
n : Nat
⊢ n.isEven = true → n.half.inl = n
Tactic:
induction n using Nat.recTwo with
| zero => intro; rfl
| one => intro; contradiction
| step n ih =>
  intro h
  unfold Nat.inl at ih ⊢
  unfold Nat.half
  rw [Nat.mul_succ, ih h]
Proof state after:
no goals
Theorem: Nat.inl_half_eq_of_isEven
Proof state before:
case zero

⊢ isEven 0 = true → (half 0).inl = 0
Tactic:
intro
Proof state after:
case zero
a✝ : isEven 0 = true
⊢ (half 0).inl = 0
Theorem: Nat.inl_half_eq_of_isEven
Proof state before:
case zero
a✝ : isEven 0 = true
⊢ (half 0).inl = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.inl_half_eq_of_isEven
Proof state before:
case one

⊢ isEven 1 = true → (half 1).inl = 1
Tactic:
intro
Proof state after:
case one
a✝ : isEven 1 = true
⊢ (half 1).inl = 1
Theorem: Nat.inl_half_eq_of_isEven
Proof state before:
case one
a✝ : isEven 1 = true
⊢ (half 1).inl = 1
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.inl_half_eq_of_isEven
Proof state before:
case step
n : Nat
ih : n.isEven = true → n.half.inl = n
⊢ (n + 2).isEven = true → (n + 2).half.inl = n + 2
Tactic:
intro h
Proof state after:
case step
n : Nat
ih : n.isEven = true → n.half.inl = n
h : (n + 2).isEven = true
⊢ (n + 2).half.inl = n + 2
Theorem: Nat.inl_half_eq_of_isEven
Proof state before:
case step
n : Nat
ih : n.isEven = true → n.half.inl = n
h : (n + 2).isEven = true
⊢ (n + 2).half.inl = n + 2
Tactic:
unfold Nat.inl at ih ⊢
Proof state after:
case step
n : Nat
ih : n.isEven = true → 2 * n.half = n
h : (n + 2).isEven = true
⊢ 2 * (n + 2).half = n + 2
Theorem: Nat.inl_half_eq_of_isEven
Proof state before:
case step
n : Nat
ih : n.isEven = true → 2 * n.half = n
h : (n + 2).isEven = true
⊢ 2 * (n + 2).half = n + 2
Tactic:
unfold Nat.half
Proof state after:
case step
n : Nat
ih : n.isEven = true → 2 * n.half = n
h : (n + 2).isEven = true
⊢ 2 * (n.half + 1) = n + 2
Theorem: Nat.inl_half_eq_of_isEven
Proof state before:
case step
n : Nat
ih : n.isEven = true → 2 * n.half = n
h : (n + 2).isEven = true
⊢ 2 * (n.half + 1) = n + 2
Tactic:
rw [Nat.mul_succ, ih h]
Proof state after:
no goals
Theorem: Nat.inr_half_eq_of_isOdd
Proof state before:
n : Nat
⊢ n.isOdd = true → n.half.inr = n
Tactic:
induction n using Nat.recTwo with
| zero => intro; contradiction
| one => intro; rfl
| step n ih =>
  intro h
  unfold Nat.inr at ih ⊢
  unfold Nat.half
  rw [Nat.mul_succ, Nat.add_succ, Nat.add_succ, ih h]
Proof state after:
no goals
Theorem: Nat.inr_half_eq_of_isOdd
Proof state before:
case zero

⊢ isOdd 0 = true → (half 0).inr = 0
Tactic:
intro
Proof state after:
case zero
a✝ : isOdd 0 = true
⊢ (half 0).inr = 0
Theorem: Nat.inr_half_eq_of_isOdd
Proof state before:
case zero
a✝ : isOdd 0 = true
⊢ (half 0).inr = 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.inr_half_eq_of_isOdd
Proof state before:
case one

⊢ isOdd 1 = true → (half 1).inr = 1
Tactic:
intro
Proof state after:
case one
a✝ : isOdd 1 = true
⊢ (half 1).inr = 1
Theorem: Nat.inr_half_eq_of_isOdd
Proof state before:
case one
a✝ : isOdd 1 = true
⊢ (half 1).inr = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.inr_half_eq_of_isOdd
Proof state before:
case step
n : Nat
ih : n.isOdd = true → n.half.inr = n
⊢ (n + 2).isOdd = true → (n + 2).half.inr = n + 2
Tactic:
intro h
Proof state after:
case step
n : Nat
ih : n.isOdd = true → n.half.inr = n
h : (n + 2).isOdd = true
⊢ (n + 2).half.inr = n + 2
Theorem: Nat.inr_half_eq_of_isOdd
Proof state before:
case step
n : Nat
ih : n.isOdd = true → n.half.inr = n
h : (n + 2).isOdd = true
⊢ (n + 2).half.inr = n + 2
Tactic:
unfold Nat.inr at ih ⊢
Proof state after:
case step
n : Nat
ih : n.isOdd = true → 2 * n.half + 1 = n
h : (n + 2).isOdd = true
⊢ 2 * (n + 2).half + 1 = n + 2