[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n' : ℕ
⊢ (∃ a b x, p { val := a, property := b }) ↔ ∃ h, p { val := n', property := h }
[PROOFSTEP]
simp_rw [mk_coe, @exists_comm (_ < _) (_ = _), exists_prop, exists_eq_left']
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
[PROOFSTEP]
have : ∃ (n' : ℕ) (n : ℕ+) (_ : n' = n), p n := Exists.elim h fun n hn => ⟨n, n, rfl, hn⟩
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
[PROOFSTEP]
have n := Nat.findX this
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
[PROOFSTEP]
refine' ⟨⟨n, _⟩, _, fun m hm pm => _⟩
[GOAL]
case refine'_1
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
⊢ 0 < ↑n
[PROOFSTEP]
obtain ⟨n', hn', -⟩ := n.prop.1
[GOAL]
case refine'_1.intro.intro
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
n' : ℕ+
hn' : ↑n = ↑n'
⊢ 0 < ↑n
[PROOFSTEP]
rw [hn']
[GOAL]
case refine'_1.intro.intro
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
n' : ℕ+
hn' : ↑n = ↑n'
⊢ 0 < ↑n'
[PROOFSTEP]
exact n'.prop
[GOAL]
case refine'_2
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
⊢ p { val := ↑n, property := (_ : 0 < ↑n) }
[PROOFSTEP]
obtain ⟨n', hn', pn'⟩ := n.prop.1
[GOAL]
case refine'_2.intro.intro
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
n' : ℕ+
hn' : ↑n = ↑n'
pn' : p n'
⊢ p { val := ↑n, property := (_ : 0 < ↑n) }
[PROOFSTEP]
simpa [hn', Subtype.coe_eta] using pn'
[GOAL]
case refine'_3
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
m : ℕ+
hm : m < { val := ↑n, property := (_ : 0 < ↑n) }
pm : p m
⊢ False
[PROOFSTEP]
exact n.prop.2 m hm ⟨m, rfl, pm⟩
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n m : ℕ+
⊢ PNat.find h = m ↔ p m ∧ ∀ (n : ℕ+), n < m → ¬p n
[PROOFSTEP]
constructor
[GOAL]
case mp
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n m : ℕ+
⊢ PNat.find h = m → p m ∧ ∀ (n : ℕ+), n < m → ¬p n
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n : ℕ+
⊢ p (PNat.find h) ∧ ∀ (n : ℕ+), n < PNat.find h → ¬p n
[PROOFSTEP]
exact ⟨PNat.find_spec h, fun _ => PNat.find_min h⟩
[GOAL]
case mpr
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n m : ℕ+
⊢ (p m ∧ ∀ (n : ℕ+), n < m → ¬p n) → PNat.find h = m
[PROOFSTEP]
rintro ⟨hm, hlt⟩
[GOAL]
case mpr.intro
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n m : ℕ+
hm : p m
hlt : ∀ (n : ℕ+), n < m → ¬p n
⊢ PNat.find h = m
[PROOFSTEP]
exact le_antisymm (PNat.find_min' h hm) (not_lt.1 <| imp_not_comm.1 (hlt _) <| PNat.find_spec h)
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n✝ m n : ℕ+
⊢ PNat.find h ≤ n ↔ ∃ m, m ≤ n ∧ p m
[PROOFSTEP]
simp only [exists_prop, ← lt_add_one_iff, find_lt_iff]
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n✝ m n : ℕ+
⊢ n ≤ PNat.find h ↔ ∀ (m : ℕ+), m < n → ¬p m
[PROOFSTEP]
simp only [← not_lt, find_lt_iff, not_exists, not_and]
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n✝ m n : ℕ+
⊢ n < PNat.find h ↔ ∀ (m : ℕ+), m ≤ n → ¬p m
[PROOFSTEP]
simp only [← add_one_le_iff, le_find_iff, add_le_add_iff_right]
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n m : ℕ+
⊢ PNat.find h = 1 ↔ p 1
[PROOFSTEP]
simp [find_eq_iff]
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n m : ℕ+
⊢ ¬1 < PNat.find h ↔ ¬¬p 1
[PROOFSTEP]
simp
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h✝ : ∃ n, p n
n m : ℕ+
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
⊢ PNat.find h = PNat.find h₂ + 1
[PROOFSTEP]
refine' (find_eq_iff _).2 ⟨PNat.find_spec h₂, fun n => PNat.recOn n _ _⟩
[GOAL]
case refine'_1
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h✝ : ∃ n, p n
n✝ m : ℕ+
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
n : ℕ+
⊢ 1 < PNat.find h₂ + 1 → ¬p 1
[PROOFSTEP]
simp [h1]
[GOAL]
case refine'_2
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h✝ : ∃ n, p n
n✝ m : ℕ+
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
n : ℕ+
⊢ ∀ (n : ℕ+), (n < PNat.find h₂ + 1 → ¬p n) → n + 1 < PNat.find h₂ + 1 → ¬p (n + 1)
[PROOFSTEP]
intro m _ hm
[GOAL]
case refine'_2
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h✝ : ∃ n, p n
n✝ m✝ : ℕ+
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
n m : ℕ+
a✝ : m < PNat.find h₂ + 1 → ¬p m
hm : m + 1 < PNat.find h₂ + 1
⊢ ¬p (m + 1)
[PROOFSTEP]
simp only [add_lt_add_iff_right, lt_find_iff] at hm 
[GOAL]
case refine'_2
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h✝ : ∃ n, p n
n✝ m✝ : ℕ+
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
n m : ℕ+
a✝ : m < PNat.find h₂ + 1 → ¬p m
hm : ∀ (m_1 : ℕ+), m_1 ≤ m → ¬p (m_1 + 1)
⊢ ¬p (m + 1)
[PROOFSTEP]
exact hm _ le_rfl
