-- Mathlib/Order/WellFoundedSet.lean
theorem wellFoundedOn_iff :
    s.WellFoundedOn r ↔ WellFounded fun a b : α => r a b ∧ a ∈ s ∧ b ∈ s

Proof state:
case neg.intro
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
hst : ¬(s ∩ t).Nonempty
m : α
mt : m ∈ t
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
exact ⟨m, mt, fun x _ ⟨_, _, ms⟩ => hst ⟨m, ⟨ms, mt⟩⟩⟩

Result:
no goals

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.WellFoundedOn r ↔ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
have f : RelEmbedding (fun (a : s) (b : s) => r a b) fun a b : α => r a b ∧ a ∈ s ∧ b ∈ s :=
  ⟨⟨(↑), Subtype.coe_injective⟩, by simp⟩

Result:
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
⊢ s.WellFoundedOn r ↔ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s

Proof state:
case pos
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : (Subtype.val ⁻¹' t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
rcases h.has_min (Subtype.val ⁻¹' t) hst with ⟨⟨m, ms⟩, mt, hm⟩

Result:
case pos.intro.mk.intro
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : (Subtype.val ⁻¹' t).Nonempty
m : α
ms : m ∈ s
mt : ⟨m, ms⟩ ∈ Subtype.val ⁻¹' t
hm : ∀ x ∈ Subtype.val ⁻¹' t, ¬r ↑x ↑⟨m, ms⟩
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
⊢ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
rw [WellFounded.wellFounded_iff_has_min]

Result:
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
⊢ ∀ (s_1 : Set α), s_1.Nonempty → ∃ m ∈ s_1, ∀ x ∈ s_1, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Proof state:
case pos
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : (s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
rw [← Subtype.preimage_coe_nonempty] at hst

Result:
case pos
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : (Subtype.val ⁻¹' t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
⊢ ∀ (s_1 : Set α), s_1.Nonempty → ∃ m ∈ s_1, ∀ x ∈ s_1, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
intro t ht

Result:
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Proof state:
case neg
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : ¬(s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
rcases ht with ⟨m, mt⟩

Result:
case neg.intro
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
hst : ¬(s ∩ t).Nonempty
m : α
mt : m ∈ t
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
by_cases hst : (s ∩ t).Nonempty

Result:
case pos
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : (s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

case neg
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : ¬(s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Proof state:
case pos.intro.mk.intro
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : (Subtype.val ⁻¹' t).Nonempty
m : α
ms : m ∈ s
mt : ⟨m, ms⟩ ∈ Subtype.val ⁻¹' t
hm : ∀ x ∈ Subtype.val ⁻¹' t, ¬r ↑x ↑⟨m, ms⟩
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
exact ⟨m, mt, fun x xt ⟨xm, xs, _⟩ => hm ⟨x, xs⟩ xt xm⟩

Result:
no goals

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
⊢ s.WellFoundedOn r ↔ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
refine ⟨fun h => ?_, f.wellFounded⟩

Result:
α : Type u_2
r : α → α → Prop
s : Set α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
⊢ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
⊢ ∀ {a b : ↑s},
    r ({ toFun := Subtype.val, inj' := ⋯ } a) ({ toFun := Subtype.val, inj' := ⋯ } b) ∧
        { toFun := Subtype.val, inj' := ⋯ } a ∈ s ∧ { toFun := Subtype.val, inj' := ⋯ } b ∈ s ↔
      r ↑a ↑b

Tactic:
simp

Result:
no goals