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

State before:
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
⊢ f a = a.succ
Tactic:
refine (Nat.succ_le_of_lt (lem3 h0 h1)).eq_or_gt.resolve_right λ h3 ↦ ?_
State after:
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3 : a.succ < f a
⊢ False

State before:
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3 : a.succ < f a
⊢ False
Tactic:
obtain ⟨t, h3⟩ := Nat.exists_eq_add_of_lt h3
State after:
case intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t : ℕ
h3 : f a = a.succ + t + 1
⊢ False

State before:
case intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t : ℕ
h3 : f a = a.succ + t + 1
⊢ False
Tactic:
obtain ⟨x, h4⟩ := (h1 (a + t)).mpr (a.le_add_right t)
State after:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t : ℕ
h3 : f a = a.succ + t + 1
x : ℕ
h4 : f x = a + t
⊢ False

State before:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t : ℕ
h3 : f a = a.succ + t + 1
x : ℕ
h4 : f x = a + t
⊢ False
Tactic:
obtain ⟨y, h5⟩ := (h1 (g x)).mpr <| (h2 _).mp ⟨x, rfl⟩
State after:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t : ℕ
h3 : f a = a.succ + t + 1
x : ℕ
h4 : f x = a + t
y : ℕ
h5 : f y = g x
⊢ False

State before:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t : ℕ
h3 : f a = a.succ + t + 1
x : ℕ
h4 : f x = a + t
y : ℕ
h5 : f y = g x
⊢ False
Tactic:
rw [Nat.succ_add, ← h4, ← h, ← Nat.succ_eq_add_one, ← h, ← h5] at h3
State after:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t x : ℕ
h4 : f x = a + t
y : ℕ
h3 : f a = f (g (f y))
h5 : f y = g x
⊢ False

State before:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t x : ℕ
h4 : f x = a + t
y : ℕ
h3 : f a = f (g (f y))
h5 : f y = g x
⊢ False
Tactic:
refine (lem4 h h0 ((h1 a).mpr a.le_refl)
  ((h1 _).mpr <| (h2 _).mp ⟨f y, rfl⟩) h3).not_lt ?_
State after:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t x : ℕ
h4 : f x = a + t
y : ℕ
h3 : f a = f (g (f y))
h5 : f y = g x
⊢ a < g (f y)

State before:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t x : ℕ
h4 : f x = a + t
y : ℕ
h3 : f a = f (g (f y))
h5 : f y = g x
⊢ a < g (f y)
Tactic:
rw [h0, Nat.lt_succ_iff, ← h2]
State after:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t x : ℕ
h4 : f x = a + t
y : ℕ
h3 : f a = f (g (f y))
h5 : f y = g x
⊢ ∃ x, g x = g y

State before:
case intro.intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
a : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ a ≤ k
h3✝ : a.succ < f a
t x : ℕ
h4 : f x = a + t
y : ℕ
h3 : f a = f (g (f y))
h5 : f y = g x
⊢ ∃ x, g x = g y
Tactic:
exact ⟨y, rfl⟩
State after:
no goals