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

State before:
f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
⊢ a = b
Tactic:
wlog h3 : a ≤ b
State after:
case inr
f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
this :
  ∀ {f g : ℕ → ℕ},
    good f g →
      good g f → ∀ {a b : ℕ}, (∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k) → (∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k) → a ≤ b → a = b
h3 : ¬a ≤ b
⊢ a = b

f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
⊢ a = b

State before:
f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
⊢ a = b
Tactic:
refine h3.antisymm ((h2 _).mp ?_)
State after:
f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
⊢ ∃ x, g x = a

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

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

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

State before:
case intro.intro
f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
k d : ℕ
h4 : f (g d) = f a
h5 : f d = a + k
⊢ ∃ x, g x = a
Tactic:
exact ⟨d, lem4 h h0 ((h1 _).mpr <| h3.trans <| (h2 _).mp ⟨d, rfl⟩)
  ((h1 a).mpr a.le_refl) h4⟩
State after:
no goals

State before:
case inr
f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
this :
  ∀ {f g : ℕ → ℕ},
    good f g →
      good g f → ∀ {a b : ℕ}, (∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k) → (∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k) → a ≤ b → a = b
h3 : ¬a ≤ b
⊢ a = b
Tactic:
exact (this h0 h h2 h1 (le_of_not_le h3)).symm
State after:
no goals