internlm/Lean-Github huggingface dataset:
Theorem: HTPI.sum_step
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
h3 : f (n + 1) = f (k + (n + 1 - k))
⊢ (sum_seq (n + 1 - k + 1) k fun i => f i) = (Sum i from k to n, f i) + f (k + (n + 1 - k))
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.sum_step
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
⊢ n + 1 + 1 - k = n + 1 - k + 1
Tactic:
rewrite [←h1, add_assoc, add_assoc, Nat.add_sub_cancel_left,
  add_assoc, Nat.add_sub_cancel_left, add_assoc]
Proof state after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
⊢ j + (1 + 1) = j + (1 + 1)
Theorem: HTPI.sum_step
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
⊢ j + (1 + 1) = j + (1 + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.sum_step
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
⊢ f (n + 1) = f (k + (n + 1 - k))
Tactic:
rewrite [←h1, add_assoc, Nat.add_sub_cancel_left]
Proof state after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
⊢ f (k + (j + 1)) = f (k + (j + 1))
Theorem: HTPI.sum_step
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
⊢ f (k + (j + 1)) = f (k + (j + 1))
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.sum_empty
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : n < k
⊢ Sum i from k to n, f i = 0
Tactic:
define : Sum i from k to n, f i
Proof state after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : n < k
⊢ (sum_seq (n + 1 - k) k fun i => f i) = 0
Theorem: HTPI.sum_empty
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : n < k
⊢ (sum_seq (n + 1 - k) k fun i => f i) = 0
Tactic:
have h2 : n + 1 - k = 0 := Nat.sub_eq_zero_of_le h
Proof state after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : n < k
h2 : n + 1 - k = 0
⊢ (sum_seq (n + 1 - k) k fun i => f i) = 0
Theorem: HTPI.sum_empty
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : n < k
h2 : n + 1 - k = 0
⊢ (sum_seq (n + 1 - k) k fun i => f i) = 0
Tactic:
rewrite [h2]
Proof state after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : n < k
h2 : n + 1 - k = 0
⊢ (sum_seq 0 k fun i => f i) = 0
Theorem: HTPI.sum_empty
Proof state before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : n < k
h2 : n + 1 - k = 0
⊢ (sum_seq 0 k fun i => f i) = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fnz_even
Proof state before:
k : ℕ
⊢ fnz (2 * k) = ↑k
Tactic:
have h1 : 2 ∣ 2 * k := by
  apply Exists.intro k
  rfl
  done
Proof state after:
k : ℕ
h1 : 2 ∣ 2 * k
⊢ fnz (2 * k) = ↑k
Theorem: HTPI.fnz_even
Proof state before:
k : ℕ
h1 : 2 ∣ 2 * k
⊢ fnz (2 * k) = ↑k
Tactic:
have h2 : fnz (2 * k) = if 2 ∣ 2 * k then ↑(2 * k / 2)
  else -↑((2 * k + 1) / 2) := by rfl
Proof state after:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = if 2 ∣ 2 * k then ↑(2 * k / 2) else -↑((2 * k + 1) / 2)
⊢ fnz (2 * k) = ↑k
Theorem: HTPI.fnz_even
Proof state before:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = if 2 ∣ 2 * k then ↑(2 * k / 2) else -↑((2 * k + 1) / 2)
⊢ fnz (2 * k) = ↑k
Tactic:
rewrite [if_pos h1] at h2
Proof state after:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑(2 * k / 2)
⊢ fnz (2 * k) = ↑k
Theorem: HTPI.fnz_even
Proof state before:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑(2 * k / 2)
⊢ fnz (2 * k) = ↑k
Tactic:
have h3 : 0 < 2 := by linarith
Proof state after:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑(2 * k / 2)
h3 : 0 < 2
⊢ fnz (2 * k) = ↑k
Theorem: HTPI.fnz_even
Proof state before:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑(2 * k / 2)
h3 : 0 < 2
⊢ fnz (2 * k) = ↑k
Tactic:
rewrite [Nat.mul_div_cancel_left k h3] at h2
Proof state after:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑k
h3 : 0 < 2
⊢ fnz (2 * k) = ↑k
Theorem: HTPI.fnz_even
Proof state before:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑k
h3 : 0 < 2
⊢ fnz (2 * k) = ↑k
Tactic:
show fnz (2 * k) = ↑k from h2
Proof state after:
no goals
Theorem: HTPI.fnz_even
Proof state before:
k : ℕ
⊢ 2 ∣ 2 * k
Tactic:
apply Exists.intro k
Proof state after:
k : ℕ
⊢ 2 * k = 2 * k
Theorem: HTPI.fnz_even
Proof state before:
k : ℕ
⊢ 2 * k = 2 * k
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fnz_even
Proof state before:
k : ℕ
h1 : 2 ∣ 2 * k
⊢ fnz (2 * k) = if 2 ∣ 2 * k then ↑(2 * k / 2) else -↑((2 * k + 1) / 2)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fnz_even
Proof state before:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑(2 * k / 2)
⊢ 0 < 2
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.fzn_nat
Proof state before:
k : ℕ
⊢ fzn ↑k = 2 * k
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fzn_neg_succ_nat
Proof state before:
k : ℕ
⊢ fzn (-↑(k + 1)) = 2 * k + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fzn_fnz
Proof state before:
⊢ fzn ∘ fnz = id
Tactic:
apply funext
Proof state after:
case h

⊢ ∀ (x : ℕ), (fzn ∘ fnz) x = id x
Theorem: HTPI.fzn_fnz
Proof state before:
case h

⊢ ∀ (x : ℕ), (fzn ∘ fnz) x = id x
Tactic:
fix n : Nat
Proof state after:
case h
n : ℕ
⊢ (fzn ∘ fnz) n = id n
Theorem: HTPI.fzn_fnz
Proof state before:
case h
n : ℕ
⊢ (fzn ∘ fnz) n = id n
Tactic:
rewrite [comp_def]
Proof state after:
case h
n : ℕ
⊢ fzn (fnz n) = id n
Theorem: HTPI.fzn_fnz
Proof state before:
case h
n : ℕ
⊢ fzn (fnz n) = id n
Tactic:
have h1 : nat_even n ∨ nat_odd n := Exercise_6_1_16a1 n
Proof state after:
case h
n : ℕ
h1 : nat_even n ∨ nat_odd n
⊢ fzn (fnz n) = id n
Theorem: HTPI.fzn_fnz
Proof state before:
case h
n : ℕ
h1 : nat_even n ∨ nat_odd n
⊢ fzn (fnz n) = id n
Tactic:
by_cases on h1
Proof state after:
case h.Case_1
n : ℕ
h1 : nat_even n
⊢ fzn (fnz n) = id n

case h.Case_2
n : ℕ
h1 : nat_odd n
⊢ fzn (fnz n) = id n
Theorem: HTPI.fzn_fnz
Proof state before:
case h.Case_1
n : ℕ
h1 : nat_even n
⊢ fzn (fnz n) = id n
Tactic:
obtain (k : Nat) (h2 : n = 2 * k) from h1
Proof state after:
case h.Case_1
n : ℕ
h1 : nat_even n
k : ℕ
h2 : n = 2 * k
⊢ fzn (fnz n) = id n
Theorem: HTPI.fzn_fnz
Proof state before:
case h.Case_1
n : ℕ
h1 : nat_even n
k : ℕ
h2 : n = 2 * k
⊢ fzn (fnz n) = id n
Tactic:
rewrite [h2, fnz_even, fzn_nat]
Proof state after:
case h.Case_1
n : ℕ
h1 : nat_even n
k : ℕ
h2 : n = 2 * k
⊢ 2 * k = id (2 * k)
Theorem: HTPI.fzn_fnz
Proof state before:
case h.Case_1
n : ℕ
h1 : nat_even n
k : ℕ
h2 : n = 2 * k
⊢ 2 * k = id (2 * k)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fzn_fnz
Proof state before:
case h.Case_2
n : ℕ
h1 : nat_odd n
⊢ fzn (fnz n) = id n
Tactic:
obtain (k : Nat) (h2 : n = 2 * k + 1) from h1
Proof state after:
case h.Case_2
n : ℕ
h1 : nat_odd n
k : ℕ
h2 : n = 2 * k + 1
⊢ fzn (fnz n) = id n
Theorem: HTPI.fzn_fnz
Proof state before:
case h.Case_2
n : ℕ
h1 : nat_odd n
k : ℕ
h2 : n = 2 * k + 1
⊢ fzn (fnz n) = id n
Tactic:
rewrite [h2, fnz_odd, fzn_neg_succ_nat]
Proof state after:
case h.Case_2
n : ℕ
h1 : nat_odd n
k : ℕ
h2 : n = 2 * k + 1
⊢ 2 * k + 1 = id (2 * k + 1)
Theorem: HTPI.fzn_fnz
Proof state before:
case h.Case_2
n : ℕ
h1 : nat_odd n
k : ℕ
h2 : n = 2 * k + 1
⊢ 2 * k + 1 = id (2 * k + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fnnn_def
Proof state before:
a b : ℕ
⊢ fnnn (a, b) = tri (a + b) + a
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.le_of_fnnn_eq
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
⊢ a1 + b1 ≤ a2 + b2
Tactic:
by_contra h2
Proof state after:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : ¬a1 + b1 ≤ a2 + b2
⊢ False
Theorem: HTPI.le_of_fnnn_eq
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : ¬a1 + b1 ≤ a2 + b2
⊢ False
Tactic:
have h3 : a2 + b2 + 1 ≤ a1 + b1 := by linarith
Proof state after:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : ¬a1 + b1 ≤ a2 + b2
h3 : a2 + b2 + 1 ≤ a1 + b1
⊢ False
Theorem: HTPI.le_of_fnnn_eq
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : ¬a1 + b1 ≤ a2 + b2
h3 : a2 + b2 + 1 ≤ a1 + b1
⊢ False
Tactic:
have h4 : fnnn (a2, b2) < fnnn (a1, b1) :=
  calc fnnn (a2, b2)
    _ = tri (a2 + b2) + a2 := by rfl
    _ < tri (a2 + b2) + (a2 + b2) + 1 := by linarith
    _ = tri (a2 + b2 + 1) := (tri_step _).symm
    _ ≤ tri (a1 + b1) := tri_incr h3
    _ ≤ tri (a1 + b1) + a1 := by linarith
    _ = fnnn (a1, b1) := by rfl
Proof state after:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : ¬a1 + b1 ≤ a2 + b2
h3 : a2 + b2 + 1 ≤ a1 + b1
h4 : fnnn (a2, b2) < fnnn (a1, b1)
⊢ False
Theorem: HTPI.le_of_fnnn_eq
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : ¬a1 + b1 ≤ a2 + b2
h3 : a2 + b2 + 1 ≤ a1 + b1
h4 : fnnn (a2, b2) < fnnn (a1, b1)
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.le_of_fnnn_eq
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : ¬a1 + b1 ≤ a2 + b2
⊢ a2 + b2 + 1 ≤ a1 + b1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.le_of_fnnn_eq
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : ¬a1 + b1 ≤ a2 + b2
h3 : a2 + b2 + 1 ≤ a1 + b1
⊢ fnnn (a2, b2) = tri (a2 + b2) + a2
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.le_of_fnnn_eq
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : ¬a1 + b1 ≤ a2 + b2
h3 : a2 + b2 + 1 ≤ a1 + b1
⊢ tri (a2 + b2) + a2 < tri (a2 + b2) + (a2 + b2) + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.le_of_fnnn_eq
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : ¬a1 + b1 ≤ a2 + b2
h3 : a2 + b2 + 1 ≤ a1 + b1
⊢ tri (a1 + b1) ≤ tri (a1 + b1) + a1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.le_of_fnnn_eq
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : ¬a1 + b1 ≤ a2 + b2
h3 : a2 + b2 + 1 ≤ a1 + b1
⊢ tri (a1 + b1) + a1 = fnnn (a1, b1)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fnnn_one_one
Proof state before:
⊢ one_to_one fnnn
Tactic:
fix (a1, b1) : Nat × Nat
Proof state after:
a1 b1 : ℕ
⊢ ∀ (x2 : ℕ × ℕ), fnnn (a1, b1) = fnnn x2 → (a1, b1) = x2
Theorem: HTPI.fnnn_one_one
Proof state before:
a1 b1 : ℕ
⊢ ∀ (x2 : ℕ × ℕ), fnnn (a1, b1) = fnnn x2 → (a1, b1) = x2
Tactic:
fix (a2, b2) : Nat × Nat
Proof state after:
a1 b1 a2 b2 : ℕ
⊢ fnnn (a1, b1) = fnnn (a2, b2) → (a1, b1) = (a2, b2)
Theorem: HTPI.fnnn_one_one
Proof state before:
a1 b1 a2 b2 : ℕ
⊢ fnnn (a1, b1) = fnnn (a2, b2) → (a1, b1) = (a2, b2)
Tactic:
assume h1 : fnnn (a1, b1) = fnnn (a2, b2)
Proof state after:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
⊢ (a1, b1) = (a2, b2)
Theorem: HTPI.fnnn_one_one
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
⊢ (a1, b1) = (a2, b2)
Tactic:
have h2 : a1 + b1 ≤ a2 + b2 := le_of_fnnn_eq h1
Proof state after:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : a1 + b1 ≤ a2 + b2
⊢ (a1, b1) = (a2, b2)
Theorem: HTPI.fnnn_one_one
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : a1 + b1 ≤ a2 + b2
⊢ (a1, b1) = (a2, b2)
Tactic:
have h3 : a2 + b2 ≤ a1 + b1 := le_of_fnnn_eq h1.symm
Proof state after:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
⊢ (a1, b1) = (a2, b2)
Theorem: HTPI.fnnn_one_one
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
⊢ (a1, b1) = (a2, b2)
Tactic:
have h4 : a1 + b1 = a2 + b2 := by linarith
Proof state after:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
h4 : a1 + b1 = a2 + b2
⊢ (a1, b1) = (a2, b2)
Theorem: HTPI.fnnn_one_one
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
h4 : a1 + b1 = a2 + b2
⊢ (a1, b1) = (a2, b2)
Tactic:
rewrite [fnnn_def, fnnn_def, h4] at h1
Proof state after:
a1 b1 a2 b2 : ℕ
h1 : tri (a2 + b2) + a1 = tri (a2 + b2) + a2
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
h4 : a1 + b1 = a2 + b2
⊢ (a1, b1) = (a2, b2)
Theorem: HTPI.fnnn_one_one
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : tri (a2 + b2) + a1 = tri (a2 + b2) + a2
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
h4 : a1 + b1 = a2 + b2
⊢ (a1, b1) = (a2, b2)
Tactic:
have h6 : a1 = a2 := Nat.add_left_cancel h1
Proof state after:
a1 b1 a2 b2 : ℕ
h1 : tri (a2 + b2) + a1 = tri (a2 + b2) + a2
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
h4 : a1 + b1 = a2 + b2
h6 : a1 = a2
⊢ (a1, b1) = (a2, b2)
Theorem: HTPI.fnnn_one_one
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : tri (a2 + b2) + a1 = tri (a2 + b2) + a2
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
h4 : a1 + b1 = a2 + b2
h6 : a1 = a2
⊢ (a1, b1) = (a2, b2)
Tactic:
rewrite [h6] at h4
Proof state after:
a1 b1 a2 b2 : ℕ
h1 : tri (a2 + b2) + a1 = tri (a2 + b2) + a2
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
h4 : a2 + b1 = a2 + b2
h6 : a1 = a2
⊢ (a1, b1) = (a2, b2)
Theorem: HTPI.fnnn_one_one
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : tri (a2 + b2) + a1 = tri (a2 + b2) + a2
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
h4 : a2 + b1 = a2 + b2
h6 : a1 = a2
⊢ (a1, b1) = (a2, b2)
Tactic:
have h7 : b1 = b2 := Nat.add_left_cancel h4
Proof state after:
a1 b1 a2 b2 : ℕ
h1 : tri (a2 + b2) + a1 = tri (a2 + b2) + a2
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
h4 : a2 + b1 = a2 + b2
h6 : a1 = a2
h7 : b1 = b2
⊢ (a1, b1) = (a2, b2)
Theorem: HTPI.fnnn_one_one
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : tri (a2 + b2) + a1 = tri (a2 + b2) + a2
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
h4 : a2 + b1 = a2 + b2
h6 : a1 = a2
h7 : b1 = b2
⊢ (a1, b1) = (a2, b2)
Tactic:
rewrite [h6, h7]
Proof state after:
a1 b1 a2 b2 : ℕ
h1 : tri (a2 + b2) + a1 = tri (a2 + b2) + a2
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
h4 : a2 + b1 = a2 + b2
h6 : a1 = a2
h7 : b1 = b2
⊢ (a2, b2) = (a2, b2)
Theorem: HTPI.fnnn_one_one
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : tri (a2 + b2) + a1 = tri (a2 + b2) + a2
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
h4 : a2 + b1 = a2 + b2
h6 : a1 = a2
h7 : b1 = b2
⊢ (a2, b2) = (a2, b2)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fnnn_one_one
Proof state before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : a1 + b1 ≤ a2 + b2
h3 : a2 + b2 ≤ a1 + b1
⊢ a1 + b1 = a2 + b2
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
⊢ onto fnnn
Tactic:
define
Proof state after:
⊢ ∀ (y : ℕ), ∃ x, fnnn x = y
Theorem: HTPI.fnnn_onto
Proof state before:
⊢ ∀ (y : ℕ), ∃ x, fnnn x = y
Tactic:
by_induc
Proof state after:
case Base_Case

⊢ ∃ x, fnnn x = 0

case Induction_Step

⊢ ∀ (y : ℕ), (∃ x, fnnn x = y) → ∃ x, fnnn x = y + 1
Theorem: HTPI.fnnn_onto
Proof state before:
case Base_Case

⊢ ∃ x, fnnn x = 0
Tactic:
apply Exists.intro (0, 0)
Proof state after:
case Base_Case

⊢ fnnn (0, 0) = 0
Theorem: HTPI.fnnn_onto
Proof state before:
case Base_Case

⊢ fnnn (0, 0) = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
case Induction_Step

⊢ ∀ (y : ℕ), (∃ x, fnnn x = y) → ∃ x, fnnn x = y + 1
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
n : ℕ
⊢ (∃ x, fnnn x = n) → ∃ x, fnnn x = n + 1
Theorem: HTPI.fnnn_onto
Proof state before:
case Induction_Step
n : ℕ
⊢ (∃ x, fnnn x = n) → ∃ x, fnnn x = n + 1
Tactic:
assume ih : ∃ (x : Nat × Nat), fnnn x = n
Proof state after:
case Induction_Step
n : ℕ
ih : ∃ x, fnnn x = n
⊢ ∃ x, fnnn x = n + 1
Theorem: HTPI.fnnn_onto
Proof state before:
case Induction_Step
n : ℕ
ih : ∃ x, fnnn x = n
⊢ ∃ x, fnnn x = n + 1
Tactic:
obtain ((a, b) : Nat × Nat) (h1 : fnnn (a, b) = n) from ih
Proof state after:
case Induction_Step
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
⊢ ∃ x, fnnn x = n + 1
Theorem: HTPI.fnnn_onto
Proof state before:
case Induction_Step
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
⊢ ∃ x, fnnn x = n + 1
Tactic:
by_cases h2 : b = 0
Proof state after:
case pos
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : b = 0
⊢ ∃ x, fnnn x = n + 1

case neg
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : ¬b = 0
⊢ ∃ x, fnnn x = n + 1
Theorem: HTPI.fnnn_onto
Proof state before:
case pos
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : b = 0
⊢ ∃ x, fnnn x = n + 1
Tactic:
apply Exists.intro (0, a + 1)
Proof state after:
case pos
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : b = 0
⊢ fnnn (0, a + 1) = n + 1
Theorem: HTPI.fnnn_onto
Proof state before:
case pos
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : b = 0
⊢ fnnn (0, a + 1) = n + 1
Tactic:
show fnnn (0, a + 1) = n + 1 from
  calc fnnn (0, a + 1)
    _ = tri (0 + (a + 1)) + 0 := by rfl
    _ = tri (a + 1) := by ring
    _ = tri a + a + 1 := tri_step a
    _ = tri (a + 0) + a + 1 := by ring
    _ = fnnn (a, b) + 1 := by rw [h2, fnnn_def]
    _ = n + 1 := by rw [h1]
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : b = 0
⊢ fnnn (0, a + 1) = tri (0 + (a + 1)) + 0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : b = 0
⊢ tri (0 + (a + 1)) + 0 = tri (a + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : b = 0
⊢ tri a + a + 1 = tri (a + 0) + a + 1
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : b = 0
⊢ tri (a + 0) + a + 1 = fnnn (a, b) + 1
Tactic:
rw [h2, fnnn_def]
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : b = 0
⊢ fnnn (a, b) + 1 = n + 1
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
case neg
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : ¬b = 0
⊢ ∃ x, fnnn x = n + 1
Tactic:
obtain (k : Nat) (h3 : b = k + 1) from
  exists_eq_add_one_of_ne_zero h2
Proof state after:
case neg
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : ¬b = 0
k : ℕ
h3 : b = k + 1
⊢ ∃ x, fnnn x = n + 1
Theorem: HTPI.fnnn_onto
Proof state before:
case neg
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : ¬b = 0
k : ℕ
h3 : b = k + 1
⊢ ∃ x, fnnn x = n + 1
Tactic:
apply Exists.intro (a + 1, k)
Proof state after:
case neg
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : ¬b = 0
k : ℕ
h3 : b = k + 1
⊢ fnnn (a + 1, k) = n + 1
Theorem: HTPI.fnnn_onto
Proof state before:
case neg
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : ¬b = 0
k : ℕ
h3 : b = k + 1
⊢ fnnn (a + 1, k) = n + 1
Tactic:
show fnnn (a + 1, k) = n + 1 from
  calc fnnn (a + 1, k)
    _ = tri (a + 1 + k) + (a + 1) := by rfl
    _ = tri (a + (k + 1)) + a + 1 := by ring
    _ = tri (a + b) + a + 1 := by rw [h3]
    _ = fnnn (a, b) + 1 := by rfl
    _ = n + 1 := by rw [h1]
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : ¬b = 0
k : ℕ
h3 : b = k + 1
⊢ fnnn (a + 1, k) = tri (a + 1 + k) + (a + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : ¬b = 0
k : ℕ
h3 : b = k + 1
⊢ tri (a + 1 + k) + (a + 1) = tri (a + (k + 1)) + a + 1
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : ¬b = 0
k : ℕ
h3 : b = k + 1
⊢ tri (a + (k + 1)) + a + 1 = tri (a + b) + a + 1
Tactic:
rw [h3]
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : ¬b = 0
k : ℕ
h3 : b = k + 1
⊢ tri (a + b) + a + 1 = fnnn (a, b) + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fnnn_onto
Proof state before:
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
h2 : ¬b = 0
k : ℕ
h3 : b = k + 1
⊢ fnnn (a, b) + 1 = n + 1
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: HTPI.one_one_on_of_one_one
Proof state before:
U V : Type
f : U → V
h : one_to_one f
A : Set U
⊢ one_one_on f A
Tactic:
define
Proof state after:
U V : Type
f : U → V
h : one_to_one f
A : Set U
⊢ ∀ ⦃x1 x2 : U⦄, x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2
Theorem: HTPI.one_one_on_of_one_one
Proof state before:
U V : Type
f : U → V
h : one_to_one f
A : Set U
⊢ ∀ ⦃x1 x2 : U⦄, x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2
Tactic:
fix x1 : U
Proof state after:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 : U
⊢ ∀ ⦃x2 : U⦄, x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2
Theorem: HTPI.one_one_on_of_one_one
Proof state before:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 : U
⊢ ∀ ⦃x2 : U⦄, x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2
Tactic:
fix x2 : U
Proof state after:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 x2 : U
⊢ x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2
Theorem: HTPI.one_one_on_of_one_one
Proof state before:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 x2 : U
⊢ x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2
Tactic:
assume h1 : x1 ∈ A
Proof state after:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 x2 : U
h1 : x1 ∈ A
⊢ x2 ∈ A → f x1 = f x2 → x1 = x2
Theorem: HTPI.one_one_on_of_one_one
Proof state before:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 x2 : U
h1 : x1 ∈ A
⊢ x2 ∈ A → f x1 = f x2 → x1 = x2
Tactic:
assume h2 : x2 ∈ A
Proof state after:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 x2 : U
h1 : x1 ∈ A
h2 : x2 ∈ A
⊢ f x1 = f x2 → x1 = x2
Theorem: HTPI.one_one_on_of_one_one
Proof state before:
U V : Type
f : U → V
h : one_to_one f
A : Set U
x1 x2 : U
h1 : x1 ∈ A
h2 : x2 ∈ A
⊢ f x1 = f x2 → x1 = x2
Tactic:
show f x1 = f x2 → x1 = x2 from h x1 x2
Proof state after:
no goals
Theorem: HTPI.elt_Univ
Proof state before:
U : Type
u : U
⊢ u ∈ Univ U
Tactic:
trivial
Proof state after:
no goals
Theorem: HTPI.equinum_Univ
Proof state before:
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
h3 : image f (Univ U) = Univ V
⊢ Univ U ∼ Univ V
Tactic:
show Univ U ∼ Univ V from
  equinum_image (one_one_on_of_one_one h1 (Univ U)) h3
Proof state after:
no goals
Theorem: HTPI.equinum_Univ
Proof state before:
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
⊢ image f (Univ U) = Univ V
Tactic:
apply Set.ext
Proof state after:
case h
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
⊢ ∀ (x : V), x ∈ image f (Univ U) ↔ x ∈ Univ V
Theorem: HTPI.equinum_Univ
Proof state before:
case h
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
⊢ ∀ (x : V), x ∈ image f (Univ U) ↔ x ∈ Univ V
Tactic:
fix v : V
Proof state after:
case h
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
⊢ v ∈ image f (Univ U) ↔ v ∈ Univ V
Theorem: HTPI.equinum_Univ
Proof state before:
case h
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
⊢ v ∈ image f (Univ U) ↔ v ∈ Univ V
Tactic:
apply Iff.intro
Proof state after:
case h.mp
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
⊢ v ∈ image f (Univ U) → v ∈ Univ V

case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
⊢ v ∈ Univ V → v ∈ image f (Univ U)
Theorem: HTPI.equinum_Univ
Proof state before:
case h.mp
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
⊢ v ∈ image f (Univ U) → v ∈ Univ V
Tactic:
assume h3 : v ∈ image f (Univ U)
Proof state after:
case h.mp
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ image f (Univ U)
⊢ v ∈ Univ V
Theorem: HTPI.equinum_Univ
Proof state before:
case h.mp
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ image f (Univ U)
⊢ v ∈ Univ V
Tactic:
show v ∈ Univ V from elt_Univ v
Proof state after:
no goals
Theorem: HTPI.equinum_Univ
Proof state before:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
⊢ v ∈ Univ V → v ∈ image f (Univ U)
Tactic:
assume h3 : v ∈ Univ V
Proof state after:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
⊢ v ∈ image f (Univ U)
Theorem: HTPI.equinum_Univ
Proof state before:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
⊢ v ∈ image f (Univ U)
Tactic:
obtain (u : U) (h4 : f u = v) from h2 v
Proof state after:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
u : U
h4 : f u = v
⊢ v ∈ image f (Univ U)