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

State before:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
⊢ a1 + b1 ≤ a2 + b2
Tactic:
by_contra h2
State after:
a1 b1 a2 b2 : ℕ
h1 : fnnn (a1, b1) = fnnn (a2, b2)
h2 : ¬a1 + b1 ≤ a2 + b2
⊢ False

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

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

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

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
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 + 1 ≤ a1 + b1
⊢ fnnn (a2, b2) = tri (a2 + b2) + a2
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 + 1 ≤ a1 + b1
⊢ tri (a2 + b2) + a2 < tri (a2 + b2) + (a2 + b2) + 1
Tactic:
linarith
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 + 1 ≤ a1 + b1
⊢ tri (a1 + b1) ≤ tri (a1 + b1) + a1
Tactic:
linarith
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 + 1 ≤ a1 + b1
⊢ tri (a1 + b1) + a1 = fnnn (a1, b1)
Tactic:
rfl
State after:
no goals