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

State before:
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
f g : ℕ → ℕ
h : good f g
h0 : good g f
⊢ f = g
Tactic:
obtain ⟨a, h1, h2⟩ := lem6 h h0
State after:
case intro.intro
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
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 = g

State before:
case intro.intro
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
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 = g
Tactic:
suffices h3 : ∀ n, a ≤ n → f n = n.succ ∧ g n = n.succ by
  ext x; rw [← Nat.succ_inj', ← h, (h3 _ <| (h2 _).mp ⟨x, rfl⟩).1]
State after:
case intro.intro
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
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
⊢ ∀ (n : ℕ), a ≤ n → f n = n.succ ∧ g n = n.succ

State before:
case intro.intro
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
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
⊢ ∀ (n : ℕ), a ≤ n → f n = n.succ ∧ g n = n.succ
Tactic:
refine Nat.le_induction ⟨lem7 h h0 h1 h2, lem7 h0 h h2 h1⟩
  (λ n _ h3 ↦ ⟨?_, ?_⟩)
State after:
case intro.intro.refine_1
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
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
n : ℕ
x✝ : a ≤ n
h3 : f n = n.succ ∧ g n = n.succ
⊢ f (n + 1) = (n + 1).succ

case intro.intro.refine_2
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
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
n : ℕ
x✝ : a ≤ n
h3 : f n = n.succ ∧ g n = n.succ
⊢ g (n + 1) = (n + 1).succ

State before:
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
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 : ∀ (n : ℕ), a ≤ n → f n = n.succ ∧ g n = n.succ
⊢ f = g
Tactic:
ext x
State after:
case h
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
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 : ∀ (n : ℕ), a ≤ n → f n = n.succ ∧ g n = n.succ
x : ℕ
⊢ f x = g x

State before:
case h
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
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 : ∀ (n : ℕ), a ≤ n → f n = n.succ ∧ g n = n.succ
x : ℕ
⊢ f x = g x
Tactic:
rw [← Nat.succ_inj', ← h, (h3 _ <| (h2 _).mp ⟨x, rfl⟩).1]
State after:
no goals

State before:
case intro.intro.refine_1
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
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
n : ℕ
x✝ : a ≤ n
h3 : f n = n.succ ∧ g n = n.succ
⊢ f (n + 1) = (n + 1).succ
Tactic:
rw [← Nat.succ_eq_add_one, ← h3.2, h, h3.1, h3.2]
State after:
no goals

State before:
case intro.intro.refine_2
f✝ g✝ : ℕ → ℕ
h✝ : good f✝ g✝
h0✝ : good g✝ f✝
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
n : ℕ
x✝ : a ≤ n
h3 : f n = n.succ ∧ g n = n.succ
⊢ g (n + 1) = (n + 1).succ
Tactic:
rw [← Nat.succ_eq_add_one, ← h3.1, h0, h3.1, h3.2]
State after:
no goals