Theorem: HTPI.fnnn_onto (HTPILib/Chap8Part2.lean)

State before:
⊢ onto fnnn
Tactic:
define
State after:
⊢ ∀ (y : ℕ), ∃ x, fnnn x = y

State before:
⊢ ∀ (y : ℕ), ∃ x, fnnn x = y
Tactic:
by_induc
State after:
case Base_Case

⊢ ∃ x, fnnn x = 0

case Induction_Step

⊢ ∀ (y : ℕ), (∃ x, fnnn x = y) → ∃ x, fnnn x = y + 1

State before:
case Base_Case

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

⊢ fnnn (0, 0) = 0

State before:
case Base_Case

⊢ fnnn (0, 0) = 0
Tactic:
rfl
State after:
no goals

State before:
case Induction_Step

⊢ ∀ (y : ℕ), (∃ x, fnnn x = y) → ∃ x, fnnn x = y + 1
Tactic:
fix n : Nat
State after:
case Induction_Step
n : ℕ
⊢ (∃ x, fnnn x = n) → ∃ x, fnnn x = n + 1

State before:
case Induction_Step
n : ℕ
⊢ (∃ x, fnnn x = n) → ∃ x, fnnn x = n + 1
Tactic:
assume ih : ∃ (x : Nat × Nat), fnnn x = n
State after:
case Induction_Step
n : ℕ
ih : ∃ x, fnnn x = n
⊢ ∃ x, fnnn x = n + 1

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
State after:
case Induction_Step
n : ℕ
ih : ∃ x, fnnn x = n
a b : ℕ
h1 : fnnn (a, b) = n
⊢ ∃ x, fnnn x = n + 1

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
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

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)
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

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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
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

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)
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

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals