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

State before:
⊢ one_to_one fnnn
Tactic:
fix (a1, b1) : Nat × Nat
State after:
a1 b1 : ℕ
⊢ ∀ (x2 : ℕ × ℕ), fnnn (a1, b1) = fnnn x2 → (a1, b1) = x2

State before:
a1 b1 : ℕ
⊢ ∀ (x2 : ℕ × ℕ), fnnn (a1, b1) = fnnn x2 → (a1, b1) = x2
Tactic:
fix (a2, b2) : Nat × Nat
State after:
a1 b1 a2 b2 : ℕ
⊢ fnnn (a1, b1) = fnnn (a2, b2) → (a1, b1) = (a2, b2)

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)
State after:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
⊢ (a1, b1) = (a2, b2)

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
State after:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : a1 + b1 ≤ a2 + b2
⊢ (a1, b1) = (a2, b2)

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

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

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

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

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

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

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

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

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