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

State before:
p : ℕ → Prop
h : ∃! n, p (n + 1)
⊢ ∃! n, 0 < n ∧ p n
Tactic:
obtain ⟨n, hn1, hn2⟩ := h
State after:
case intro.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ ∃! n, 0 < n ∧ p n

State before:
case intro.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ ∃! n, 0 < n ∧ p n
Tactic:
use n + 1
State after:
case h
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ (fun n => 0 < n ∧ p n) (n + 1) ∧ ∀ (y : ℕ), (fun n => 0 < n ∧ p n) y → y = n + 1

State before:
case h
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ (fun n => 0 < n ∧ p n) (n + 1) ∧ ∀ (y : ℕ), (fun n => 0 < n ∧ p n) y → y = n + 1
Tactic:
refine ⟨⟨Nat.succ_pos n, hn1⟩, ?_⟩
State after:
case h
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ ∀ (y : ℕ), (fun n => 0 < n ∧ p n) y → y = n + 1

State before:
case h
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ ∀ (y : ℕ), (fun n => 0 < n ∧ p n) y → y = n + 1
Tactic:
rintro m ⟨hm1, hm2⟩
State after:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
⊢ m = n + 1

State before:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
⊢ m = n + 1
Tactic:
have hm3 := hn2 (m - 1)
State after:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : (fun n => p (n + 1)) (m - 1) → m - 1 = n
⊢ m = n + 1

State before:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : (fun n => p (n + 1)) (m - 1) → m - 1 = n
⊢ m = n + 1
Tactic:
dsimp only at hm3
State after:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : p (m - 1 + 1) → m - 1 = n
⊢ m = n + 1

State before:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : p (m - 1 + 1) → m - 1 = n
⊢ m = n + 1
Tactic:
rw [Nat.sub_add_cancel hm1] at hm3
State after:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : p m → m - 1 = n
⊢ m = n + 1

State before:
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : p m → m - 1 = n
⊢ m = n + 1
Tactic:
exact Nat.eq_add_of_sub_eq hm1 (hm3 hm2)
State after:
no goals