Theorem: IMOSL.Extra.NatSeq_antitone_imp_const (IMOSLLean4/Extra/NatSequence/AntitoneConst.lean)

State before:
a : ℕ → ℕ
ha : Antitone a
⊢ ∃ C N, ∀ (n : ℕ), a (n + N) = C
Tactic:
by_contra h
State after:
a : ℕ → ℕ
ha : Antitone a
h : ¬∃ C N, ∀ (n : ℕ), a (n + N) = C
⊢ False

State before:
a : ℕ → ℕ
ha : Antitone a
h : ¬∃ C N, ∀ (n : ℕ), a (n + N) = C
⊢ False
Tactic:
simp only [not_exists, not_forall] at h
State after:
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
⊢ False

State before:
a : ℕ → ℕ
ha : Antitone a
h : ∀ (C : ℕ), ∃ N, ∀ (n : ℕ), a (n + N) + C ≤ a 0
⊢ False
Tactic:
rcases h (a 0).succ with ⟨N, h⟩
State after:
case intro
a : ℕ → ℕ
ha : Antitone a
h✝ : ∀ (C : ℕ), ∃ N, ∀ (n : ℕ), a (n + N) + C ≤ a 0
N : ℕ
h : ∀ (n : ℕ), a (n + N) + (a 0).succ ≤ a 0
⊢ False

State before:
case intro
a : ℕ → ℕ
ha : Antitone a
h✝ : ∀ (C : ℕ), ∃ N, ∀ (n : ℕ), a (n + N) + C ≤ a 0
N : ℕ
h : ∀ (n : ℕ), a (n + N) + (a 0).succ ≤ a 0
⊢ False
Tactic:
exact (h 0).not_lt (Nat.lt_add_left _ (a 0).lt_succ_self)
State after:
no goals

State before:
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C : ℕ
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + C ≤ a 0
Tactic:
induction' C with C hC
State after:
case zero
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + 0 ≤ a 0

case succ
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C : ℕ
hC : ∃ N, ∀ (n : ℕ), a (n + N) + C ≤ a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0

State before:
case zero
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + 0 ≤ a 0
Tactic:
exact ⟨0, λ n ↦ ha n.zero_le⟩
State after:
no goals

State before:
case succ
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C : ℕ
hC : ∃ N, ∀ (n : ℕ), a (n + N) + C ≤ a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Tactic:
rcases hC with ⟨N, hC⟩
State after:
case succ.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0

State before:
case succ.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Tactic:
rcases (hC 0).lt_or_eq with h0 | h0
State after:
case succ.intro.inl
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C < a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0

case succ.intro.inr
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0

State before:
case succ.intro.inl
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C < a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Tactic:
refine ⟨N, λ n ↦ h0.trans_le' (Nat.add_le_add_right (ha ?_) C)⟩
State after:
case succ.intro.inl
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C < a 0
n : ℕ
⊢ 0 + N ≤ n + N

State before:
case succ.intro.inl
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C < a 0
n : ℕ
⊢ 0 + N ≤ n + N
Tactic:
exact Nat.add_le_add_right n.zero_le N
State after:
no goals

State before:
case succ.intro.inr
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Tactic:
rcases h (a 0 - C) N with ⟨K, h1⟩
State after:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a 0 - C
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0

State before:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a 0 - C
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Tactic:
rw [← h0, Nat.add_sub_cancel, Nat.zero_add] at h1
State after:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0

State before:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Tactic:
refine ⟨K + N, λ n ↦ Nat.add_one_le_iff.mpr ?_⟩
State after:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
n : ℕ
⊢ (a (n + (K + N))).add C < a 0

State before:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
n : ℕ
⊢ (a (n + (K + N))).add C < a 0
Tactic:
rw [← h0, Nat.zero_add]
State after:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
n : ℕ
⊢ (a (n + (K + N))).add C < a N + C

State before:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
n : ℕ
⊢ (a (n + (K + N))).add C < a N + C
Tactic:
refine Nat.add_lt_add_right ((ha <| (K + N).le_add_left n).trans_lt ?_) C
State after:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
n : ℕ
⊢ a (K + N) < a N

State before:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
n : ℕ
⊢ a (K + N) < a N
Tactic:
exact (ha (N.le_add_left K)).lt_of_ne h1
State after:
no goals