Theorem: Imo2014P1.lemma1 (Compfiles/Imo2014P1.lean)

State before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
⊢ ∃! i, s i < z ∧ z ≤ s (i + 1)
Tactic:
have hmono : StrictMono s := strictMono_nat_of_lt_succ hs
State after:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
⊢ ∃! i, s i < z ∧ z ≤ s (i + 1)

State before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
⊢ ∃! i, s i < z ∧ z ≤ s (i + 1)
Tactic:
let S := { i | z ≤ s (i + 1) }
State after:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
⊢ ∃! i, s i < z ∧ z ≤ s (i + 1)

State before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ ∃! i, s i < z ∧ z ≤ s (i + 1)
Tactic:
use Nat.find h3
State after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ (fun i => s i < z ∧ z ≤ s (i + 1)) (Nat.find h3) ∧ ∀ (y : ℕ), (fun i => s i < z ∧ z ≤ s (i + 1)) y → y = Nat.find h3

State before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ (fun i => s i < z ∧ z ≤ s (i + 1)) (Nat.find h3) ∧ ∀ (y : ℕ), (fun i => s i < z ∧ z ≤ s (i + 1)) y → y = Nat.find h3
Tactic:
dsimp [S]
State after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ (s (Nat.find h3) < z ∧ z ≤ s (Nat.find h3 + 1)) ∧ ∀ (y : ℕ), s y < z ∧ z ≤ s (y + 1) → y = Nat.find h3

State before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ (s (Nat.find h3) < z ∧ z ≤ s (Nat.find h3 + 1)) ∧ ∀ (y : ℕ), s y < z ∧ z ≤ s (y + 1) → y = Nat.find h3
Tactic:
refine ⟨⟨?_, ?_⟩, ?_⟩
State after:
case h.refine_1
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ s (Nat.find h3) < z

case h.refine_2
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ z ≤ s (Nat.find h3 + 1)

case h.refine_3
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ ∀ (y : ℕ), s y < z ∧ z ≤ s (y + 1) → y = Nat.find h3

State before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
⊢ ∃ j, j ∈ S
Tactic:
use Int.toNat (z - s 0)
State after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
⊢ (z - s 0).toNat ∈ S

State before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
⊢ (z - s 0).toNat ∈ S
Tactic:
rw [Set.mem_setOf_eq]
State after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
⊢ z ≤ s ((z - s 0).toNat + 1)

State before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
have h8 := h5 (Int.toNat (z - s 0))
State after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
⊢ z ≤ s ((z - s 0).toNat + 1)

State before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
have h6 : 0 ≤ z - s 0 := by omega
State after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)

State before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
have h7 : ((Int.toNat (z - s 0)) :ℤ) = z - s 0 := Int.toNat_of_nonneg h6
State after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)

State before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
rw [h7] at h8
State after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + (z - s 0) ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)

State before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + (z - s 0) ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
rw [add_sub_cancel] at h8
State after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : z ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)

State before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : z ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
have h12 : s (Int.toNat (z - s 0)) < s (Int.toNat (z - s 0) + 1) := hs _
State after:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : z ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
h12 : s (z - s 0).toNat < s ((z - s 0).toNat + 1)
⊢ z ≤ s ((z - s 0).toNat + 1)

State before:
case h
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : z ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
h12 : s (z - s 0).toNat < s ((z - s 0).toNat + 1)
⊢ z ≤ s ((z - s 0).toNat + 1)
Tactic:
omega
State after:
no goals

State before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
⊢ s 0 + ↑i ≤ s i
Tactic:
induction' i with i ih
State after:
case zero
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
⊢ s 0 + ↑0 ≤ s 0

case succ
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
⊢ s 0 + ↑(i + 1) ≤ s (i + 1)

State before:
case zero
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
⊢ s 0 + ↑0 ≤ s 0
Tactic:
simp
State after:
no goals

State before:
case succ
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
⊢ s 0 + ↑(i + 1) ≤ s (i + 1)
Tactic:
have h10 : (Nat.succ i : ℤ) = (i : ℤ) + 1 := by norm_cast
State after:
case succ
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
h10 : ↑i.succ = ↑i + 1
⊢ s 0 + ↑(i + 1) ≤ s (i + 1)

State before:
case succ
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
h10 : ↑i.succ = ↑i + 1
⊢ s 0 + ↑(i + 1) ≤ s (i + 1)
Tactic:
rw [h10, ←add_assoc]
State after:
case succ
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
h10 : ↑i.succ = ↑i + 1
⊢ s 0 + ↑i + 1 ≤ s (i + 1)

State before:
case succ
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
h10 : ↑i.succ = ↑i + 1
⊢ s 0 + ↑i + 1 ≤ s (i + 1)
Tactic:
exact add_le_of_add_le_right (hs i) ih
State after:
no goals

State before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
i : ℕ
ih : s 0 + ↑i ≤ s i
⊢ ↑i.succ = ↑i + 1
Tactic:
norm_cast
State after:
no goals

State before:
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
⊢ 0 ≤ z - s 0
Tactic:
omega
State after:
no goals

State before:
case h.refine_1
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ s (Nat.find h3) < z
Tactic:
have h4 := Nat.find_min h3 (m := (Nat.find h3 - 1))
State after:
case h.refine_1
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
⊢ s (Nat.find h3) < z

State before:
case h.refine_1
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
⊢ s (Nat.find h3) < z
Tactic:
cases' Nat.eq_zero_or_pos (Nat.find h3) with h5 h5
State after:
case h.refine_1.inl
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 = 0
⊢ s (Nat.find h3) < z

case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
⊢ s (Nat.find h3) < z

State before:
case h.refine_1.inl
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 = 0
⊢ s (Nat.find h3) < z
Tactic:
rwa [h5]
State after:
no goals

State before:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
⊢ s (Nat.find h3) < z
Tactic:
have h6 : Nat.find h3 - 1 < Nat.find h3 :=
  Nat.sub_one_lt_of_le h5 Nat.le.refl
State after:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
⊢ s (Nat.find h3) < z

State before:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
⊢ s (Nat.find h3) < z
Tactic:
have h7 := h4 h6
State after:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
h7 : Nat.find h3 - 1 ∉ S
⊢ s (Nat.find h3) < z

State before:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
h7 : Nat.find h3 - 1 ∉ S
⊢ s (Nat.find h3) < z
Tactic:
rw [Set.mem_setOf_eq] at h7
State after:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
h7 : ¬z ≤ s (Nat.find h3 - 1 + 1)
⊢ s (Nat.find h3) < z

State before:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
h7 : ¬z ≤ s (Nat.find h3 - 1 + 1)
⊢ s (Nat.find h3) < z
Tactic:
push_neg at h7
State after:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
h7 : s (Nat.find h3 - 1 + 1) < z
⊢ s (Nat.find h3) < z

State before:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
h7 : s (Nat.find h3 - 1 + 1) < z
⊢ s (Nat.find h3) < z
Tactic:
rwa [Nat.sub_add_cancel h5] at h7
State after:
no goals

State before:
case h.refine_2
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ z ≤ s (Nat.find h3 + 1)
Tactic:
exact Nat.find_spec h3
State after:
no goals

State before:
case h.refine_3
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ ∀ (y : ℕ), s y < z ∧ z ≤ s (y + 1) → y = Nat.find h3
Tactic:
rintro m ⟨hm1, hm2⟩
State after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ m = Nat.find h3

State before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ m = Nat.find h3
Tactic:
symm
State after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ Nat.find h3 = m

State before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ Nat.find h3 = m
Tactic:
rw [Nat.find_eq_iff]
State after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ z ≤ s (m + 1) ∧ ∀ n < m, ¬z ≤ s (n + 1)

State before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ z ≤ s (m + 1) ∧ ∀ n < m, ¬z ≤ s (n + 1)
Tactic:
refine ⟨hm2, ?_⟩
State after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ ∀ n < m, ¬z ≤ s (n + 1)

State before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ ∀ n < m, ¬z ≤ s (n + 1)
Tactic:
intro k hk
State after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
k : ℕ
hk : k < m
⊢ ¬z ≤ s (k + 1)

State before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
k : ℕ
hk : k < m
⊢ ¬z ≤ s (k + 1)
Tactic:
intro hkk
State after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
k : ℕ
hk : k < m
hkk : z ≤ s (k + 1)
⊢ False

State before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
k : ℕ
hk : k < m
hkk : z ≤ s (k + 1)
⊢ False
Tactic:
have h9 : s (k + 1) ≤ s m := (StrictMono.le_iff_le hmono).mpr hk
State after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
k : ℕ
hk : k < m
hkk : z ≤ s (k + 1)
h9 : s (k + 1) ≤ s m
⊢ False

State before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
k : ℕ
hk : k < m
hkk : z ≤ s (k + 1)
h9 : s (k + 1) ≤ s m
⊢ False
Tactic:
omega
State after:
no goals