-- Mathlib/Order/WellFoundedSet.lean
theorem wellFoundedOn_iff_no_descending_seq :
    s.WellFoundedOn r ↔ ∀ f : ((· > ·) : ℕ → ℕ → Prop) ↪r r, ¬∀ n, f n ∈ s

Proof state:
case mpr.intro.mk
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b
hfs : ∀ (n : ℕ), f n ∈ s
⊢ Nonempty ((fun x1 x2 => x1 > x2) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s)

Tactic:
refine ⟨⟨f, ?_⟩⟩

Result:
case mpr.intro.mk
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b
hfs : ∀ (n : ℕ), f n ∈ s
⊢ ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b

Proof state:
case mp.intro.mk
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
⊢ ∃ x, ∀ (n : ℕ), x n ∈ s

Tactic:
have H : ∀ n, f n ∈ s := fun n => (hf.2 n.lt_succ_self).2.2

Result:
case mp.intro.mk
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
H : ∀ (n : ℕ), f n ∈ s
⊢ ∃ x, ∀ (n : ℕ), x n ∈ s

Proof state:
case mpr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ (∃ x, ∀ (n : ℕ), x n ∈ s) → Nonempty ((fun x1 x2 => x1 > x2) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s)

Tactic:
rintro ⟨⟨f, hf⟩, hfs : ∀ n, f n ∈ s⟩

Result:
case mpr.intro.mk
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b
hfs : ∀ (n : ℕ), f n ∈ s
⊢ Nonempty ((fun x1 x2 => x1 > x2) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s)

Proof state:
case mp.intro.mk
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
H : ∀ (n : ℕ), f n ∈ s
⊢ ∃ x, ∀ (n : ℕ), x n ∈ s

Tactic:
refine ⟨⟨f, ?_⟩, H⟩

Result:
case mp.intro.mk
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
H : ∀ (n : ℕ), f n ∈ s
⊢ ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b

Proof state:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ s.WellFoundedOn r ↔ ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s

Tactic:
simp only [wellFoundedOn_iff, RelEmbedding.wellFounded_iff_no_descending_seq, ← not_exists, ←
  not_nonempty_iff, not_iff_not]

Result:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ Nonempty ((fun x1 x2 => x1 > x2) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s) ↔ ∃ x, ∀ (n : ℕ), x n ∈ s

Proof state:
case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ Nonempty ((fun x1 x2 => x1 > x2) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s) → ∃ x, ∀ (n : ℕ), x n ∈ s

Tactic:
rintro ⟨⟨f, hf⟩⟩

Result:
case mp.intro.mk
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
⊢ ∃ x, ∀ (n : ℕ), x n ∈ s

Proof state:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ Nonempty ((fun x1 x2 => x1 > x2) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s) ↔ ∃ x, ∀ (n : ℕ), x n ∈ s

Tactic:
constructor

Result:
case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ Nonempty ((fun x1 x2 => x1 > x2) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s) → ∃ x, ∀ (n : ℕ), x n ∈ s

case mpr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ (∃ x, ∀ (n : ℕ), x n ∈ s) → Nonempty ((fun x1 x2 => x1 > x2) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s)

Proof state:
case mp.intro.mk
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
H : ∀ (n : ℕ), f n ∈ s
⊢ ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b

Tactic:
simpa only [H, and_true] using @hf

Result:
no goals

Proof state:
case mpr.intro.mk
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b
hfs : ∀ (n : ℕ), f n ∈ s
⊢ ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b

Tactic:
simpa only [hfs, and_true] using @hf

Result:
no goals