Theorem: IMOSL.IMO2010A6.lem1 (IMOSLLean4/IMO2010/A6/A6.lean)

State before:
f g : ℕ → ℕ
h : good f g
⊢ ∃ a, ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
Tactic:
have h0 : ∃ n, ∃ x, f x = n := ⟨f 0, 0, rfl⟩
State after:
f g : ℕ → ℕ
h : good f g
h0 : ∃ n x, f x = n
⊢ ∃ a, ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k

State before:
f g : ℕ → ℕ
h : good f g
h0 : ∃ n x, f x = n
⊢ ∃ a, ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
Tactic:
refine ⟨Nat.find h0, λ k ↦
  ⟨Nat.find_min' h0, Nat.le_induction (Nat.find_spec h0) ?_ k⟩⟩
State after:
f g : ℕ → ℕ
h : good f g
h0 : ∃ n x, f x = n
k : ℕ
⊢ ∀ (n : ℕ), Nat.find h0 ≤ n → (∃ x, f x = n) → ∃ x, f x = n + 1

State before:
f g : ℕ → ℕ
h : good f g
h0 : ∃ n x, f x = n
k : ℕ
⊢ ∀ (n : ℕ), Nat.find h0 ≤ n → (∃ x, f x = n) → ∃ x, f x = n + 1
Tactic:
rintro n h1 ⟨x, rfl⟩
State after:
case intro
f g : ℕ → ℕ
h : good f g
h0 : ∃ n x, f x = n
k x : ℕ
h1 : Nat.find h0 ≤ f x
⊢ ∃ x_1, f x_1 = f x + 1

State before:
case intro
f g : ℕ → ℕ
h : good f g
h0 : ∃ n x, f x = n
k x : ℕ
h1 : Nat.find h0 ≤ f x
⊢ ∃ x_1, f x_1 = f x + 1
Tactic:
exact ⟨g x, h x⟩
State after:
no goals