ι : Type ?u.146971
α : Type u_1
β : Type ?u.146977
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) ↔ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
ι : Type ?u.146971
α : Type u_1
β : Type ?u.146977
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ PartiallyWellOrderedOn s r ↔ ¬∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
rw [iff_forall_not_isBadSeq, ← not_exists, not_congr]
case mp
ι : Type ?u.146971
α : Type u_1
β : Type ?u.146977
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) → ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

case mpr
ι : Type ?u.146971
α : Type u_1
β : Type ?u.146977
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f) → ∃ x, IsBadSeq r s x
ι : Type ?u.146971
α : Type u_1
β : Type ?u.146977
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) ↔ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
constructor
no goals
case mp
ι : Type ?u.146971
α : Type u_1
β : Type ?u.146977
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) → ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
apply exists_min_bad_of_exists_bad
case mpr.intro.intro
ι : Type ?u.146971
α : Type u_1
β : Type ?u.146977
r : α → α → Prop
rk : α → ℕ
s : Set α
f : ℕ → α
hf1 : IsBadSeq r s f
⊢ ∃ x, IsBadSeq r s x
case mpr
ι : Type ?u.146971
α : Type u_1
β : Type ?u.146977
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f) → ∃ x, IsBadSeq r s x
rintro ⟨f, hf1, -⟩
no goals
case mpr.intro.intro
ι : Type ?u.146971
α : Type u_1
β : Type ?u.146977
r : α → α → Prop
rk : α → ℕ
s : Set α
f : ℕ → α
hf1 : IsBadSeq r s f
⊢ ∃ x, IsBadSeq r s x
exact ⟨f, hf1⟩