awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LT β
inst_1 : WellFoundedLT β
s : Set α
a : α
ha : a ∈ s
⊢ ¬f a < f (argminOn f s ⋯)

Tactic:
WellFounded.not_lt_min (InvImage.wf f wellFounded_lt) s ha

Premises used: InvImage, wellFounded_lt, WellFounded.not_lt_min, InvImage.wf, Function.argminOn
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder β
inst_1 : WellFoundedLT β
a : α
inst_2 : Nonempty α
⊢ f (argmin f) ≤ f a

Tactic:
not_lt.mp <| not_lt_argmin f a

Premises used: not_lt, Iff.mp, Function.not_lt_argmin
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder β
inst_1 : WellFoundedLT β
inst_2 : Nonempty α
⊢ MinimalFor (fun (x : α) ↦ True) f (argmin f)

Tactic:
⟨trivial, fun a _ _ ↦ argmin_le f a⟩

Premises used: trivial, And.intro, Function.argmin_le, MinimalFor
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder β
inst_1 : WellFoundedLT β
s : Set α
a : α
ha : a ∈ s
⊢ f (argminOn f s ⋯) ≤ f a

Tactic:
not_lt.mp <| not_lt_argminOn f s ha

Premises used: not_lt, Iff.mp, Function.not_lt_argminOn
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder β
inst_1 : WellFoundedLT β
s : Set α
hs : s.Nonempty
⊢ MinimalFor (fun (x : α) ↦ x ∈ s) f (argminOn f s hs)

Tactic:
⟨argminOn_mem f s hs, fun _ h _ ↦ argminOn_le f s h⟩

Premises used: Function.argminOn_mem, Function.argminOn_le, And.intro, MinimalFor
-- Module: Mathlib.Order.WellFounded
Goal:
α : Sort u_4
β : Sort u_5
r : α → α → Prop
a bot : α
ha : Acc r a
C : β → Prop
f : α → β
ih : ∀ (b : α), f b ≠ f bot → C (f b) → ∃ (c : α), r c b ∧ C (f c)
⊢ C (f a) → C (f bot)

Tactic:
(@Acc.recOn _ _ (fun x _ => C (f x) → C (f bot)) _ ha) fun x _ ih' hC =>
    (eq_or_ne (f x) (f bot)).elim (fun h => h ▸ hC) (fun h =>
      let ⟨y, hy₁, hy₂⟩ := ih x h hC
      ih' y hy₁ hy₂)

Premises used: Eq.rec, _private.0.Acc.induction_bot'.match_1, Acc.recOn, eq_or_ne, Or.elim
-- Module: Mathlib.Order.WellFounded
Goal:
α : Sort u_4
r : α → α → Prop
a bot : α
ha : Acc r a
C : α → Prop
ih : ∀ (b : α), b ≠ bot → C b → ∃ (c : α), r c b ∧ C c
⊢ C a → C bot

Tactic:
ha.induction_bot' ih

Premises used: Acc.induction_bot'
-- Module: Mathlib.Order.WellFounded
Goal:
α : Sort u_4
β : Sort u_5
r : α → α → Prop
hwf : WellFounded r
a bot : α
C : β → Prop
f : α → β
ih : ∀ (b : α), f b ≠ f bot → C (f b) → ∃ (c : α), r c b ∧ C (f c)
⊢ C (f a) → C (f bot)

Tactic:
(hwf.apply a).induction_bot' ih

Premises used: WellFounded.apply, Acc.induction_bot'
-- Module: Mathlib.Order.WellFounded
Goal:
α : Sort u_4
r : α → α → Prop
hwf : WellFounded r
a bot : α
C : α → Prop
ih : ∀ (b : α), b ≠ bot → C b → ∃ (c : α), r c b ∧ C c
⊢ C a → C bot

Tactic:
hwf.induction_bot' ih

Premises used: WellFounded.induction_bot'
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
⊢ WellFoundedOn ∅ r

Tactic:
wellFounded_of_isEmpty _

Premises used: wellFounded_of_isEmpty, Set.WellFoundedOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
⊢ ∀ {a b : { x : α // x ∈ s }},
    r (({ toFun := Subtype.val (p := fun (x : α) ↦ x ∈ s), inj' := ⋯ } : (a : { x : α // x ∈ s }) → α) a)
          (({ toFun := Subtype.val (p := fun (x : α) ↦ x ∈ s), inj' := ⋯ } : (a : { x : α // x ∈ s }) → α) b) ∧
        Membership.mem (α := α) s
            (({ toFun := Subtype.val (p := fun (x : α) ↦ x ∈ s), inj' := ⋯ } : (a : { x : α // x ∈ s }) → α) a : α) ∧
          Membership.mem (α := α) s
            (({ toFun := Subtype.val (p := fun (x : α) ↦ x ∈ s), inj' := ⋯ } : (a : { x : α // x ∈ s }) → α) b : α) ↔
      Subrel r (fun (x : α) ↦ x ∈ s) a b

Tactic:
simp
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
have :
  ∀ (f : RelEmbedding (α := { x : α // x ∈ s }) (Subrel r fun (x : α) ↦ x ∈ s) fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s),
    s.WellFoundedOn r ↔ WellFounded 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:
have f : RelEmbedding (Subrel r (· ∈ s)) fun a b : α => r a b ∧ a ∈ s ∧ b ∈ s :=
    ⟨⟨(↑), Subtype.coe_injective⟩, by simp⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
f : RelEmbedding (α := { x : α // x ∈ s }) (Subrel r fun (x : α) ↦ x ∈ s) 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:
⟨fun h => ?_, f.wellFounded⟩

Premises used: RelEmbedding.wellFounded, Iff.intro
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
f : RelEmbedding (α := { x : α // x ∈ s }) (Subrel r fun (x : α) ↦ x ∈ s) fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s
refine : ∀ (h : s.WellFoundedOn r), WellFounded 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⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
f : RelEmbedding (α := { x : α // x ∈ s }) (Subrel r fun (x : α) ↦ x ∈ s) fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
rw : ∀ (s_1 : Set α), s_1.Nonempty → ∃ m ∈ s_1, ∀ x ∈ s_1, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
⊢ WellFounded fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
rw [WellFounded.wellFounded_iff_has_min]

Premises used: WellFounded.wellFounded_iff_has_min
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
f : RelEmbedding (α := { x : α // x ∈ s }) (Subrel r fun (x : α) ↦ x ∈ s) fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
pos : ∀ (hst : (s ∩ t).Nonempty), ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
neg : ∀ (hst : ¬(s ∩ t).Nonempty), ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

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

Premises used: Inter.inter, Set.Nonempty
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
f : RelEmbedding (α := { x : α // x ∈ s }) (Subrel r fun (x : α) ↦ x ∈ s) fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : (s ∩ t).Nonempty
⊢ Set.Nonempty (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)

Tactic:
rw [← Subtype.preimage_coe_nonempty] at hst

Premises used: Subtype.preimage_coe_nonempty
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
f : RelEmbedding (α := { x : α // x ∈ s }) (Subrel r fun (x : α) ↦ x ∈ s) fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : Set.Nonempty (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
pos :
  ∀ (m : α) (ms : m ∈ s)
    (mt :
      Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) m ms))
    (hm :
      ∀ (x : { x : α // x ∈ s }),
        Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) x →
          ¬Subrel r (fun (x : α) ↦ x ∈ s) x (Subtype.mk (p := fun (x : α) ↦ x ∈ s) m ms)),
    ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
⊢ ∃ 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⟩

Premises used: mt, Set.preimage, WellFounded.has_min, Subtype.val
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
f : RelEmbedding (α := { x : α // x ∈ s }) (Subrel r fun (x : α) ↦ x ∈ s) fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : Set.Nonempty (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
m : α
ms : m ∈ s
mt :
  Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s) m ms)
hm :
  ∀ (x : { x : α // x ∈ s }),
    Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) x →
      ¬Subrel r (fun (x : α) ↦ x ∈ s) x (Subtype.mk (p := fun (x : α) ↦ x ∈ s) m ms)
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

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

Premises used: False, _private.0.Set.wellFoundedOn_iff.match_1, Subtype.mk, And.intro, Exists.intro
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
f : RelEmbedding (α := { x : α // x ∈ s }) (Subrel r fun (x : α) ↦ x ∈ s) fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : Set.Nonempty (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
m : α
ms : m ∈ s
mt :
  Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s) m ms)
hm :
  ∀ (x : { x : α // x ∈ s }),
    Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) x →
      ¬Subrel r (fun (x : α) ↦ x ∈ s) x (Subtype.mk (p := fun (x : α) ↦ x ∈ s) 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⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
f : RelEmbedding (α := { x : α // x ∈ s }) (Subrel r fun (x : α) ↦ x ∈ s) fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : ¬(s ∩ t).Nonempty
neg : ∀ (m : α) (mt : m ∈ t), ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
rcases ht with ⟨m, mt⟩

Premises used: mt
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
f : RelEmbedding (α := { x : α // x ∈ s }) (Subrel r fun (x : α) ↦ x ∈ s) 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:
⟨m, mt, fun x _ ⟨_, _, ms⟩ => hst ⟨m, ⟨ms, mt⟩⟩⟩

Premises used: False, _private.0.Set.wellFoundedOn_iff.match_1, And.intro, Exists.intro
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
f : RelEmbedding (α := { x : α // x ∈ s }) (Subrel r fun (x : α) ↦ x ∈ s) 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⟩⟩⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
⊢ WellFoundedOn univ r ↔ WellFounded r

Tactic:
simp [wellFoundedOn_iff]

Premises used: Set.wellFoundedOn_iff
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
⊢ WellFounded r → s.WellFoundedOn r

Tactic:
InvImage.wf _

Premises used: Subrel, InvImage.wf, Order.Preimage, Set.WellFoundedOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → (↑(range f) : Type u_2) := fun (c : β) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) ⋯
⊢ (range f).WellFoundedOn r ↔ WellFounded (r on f)

Tactic:
⟨fun h => (InvImage.wf f' h).mono fun c c' => id, fun h => ⟨?_⟩⟩

Premises used: id, WellFounded.intro, Iff.intro, WellFounded.mono, InvImage.wf
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → (↑(range f) : Type u_2) := fun (c : β) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) ⋯
refine : ∀ (h : WellFounded (r on f)) (a : { x : α // x ∈ range f }), Acc (Subrel r fun (x : α) ↦ x ∈ range f) a
⊢ (range f).WellFoundedOn r ↔ WellFounded (r on f)

Tactic:
refine ⟨fun h => (InvImage.wf f' h).mono fun c c' => id, fun h => ⟨?_⟩⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → (↑(range f) : Type u_2) := fun (c : β) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) ⋯
h : WellFounded (r on f)
c : β
⊢ Acc (α := { x : α // x ∈ range f }) (Subrel r fun (x : α) ↦ x ∈ range f)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) ⋯)

Tactic:
Acc.of_downward_closed f' ?_ _ ?_

Premises used: Acc.of_downward_closed
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → (↑(range f) : Type u_2) := fun (c : β) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) ⋯
h : WellFounded (r on f)
c : β
refine_1 : ∀ {a : β} {b : (↑(range f) : Type u_2)}, Subrel r (fun (x : α) ↦ x ∈ range f) b (f' a) → ∃ (c : β), f' c = b
refine_2 : Acc (InvImage (Subrel r fun (x : α) ↦ x ∈ range f) f') c
⊢ Acc (α := { x : α // x ∈ range f }) (Subrel r fun (x : α) ↦ x ∈ range f)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) ⋯)

Tactic:
refine Acc.of_downward_closed f' ?_ _ ?_

Premises used: Acc.of_downward_closed
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → (↑(range f) : Type u_2) := fun (c : β) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) ⋯
h : WellFounded (r on f)
c a c' : β
⊢ ∃ (c : β), f' c = Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c') ⋯

Tactic:
⟨c', rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → (↑(range f) : Type u_2) := fun (c : β) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) ⋯
h : WellFounded (r on f)
c a c' : β
⊢ ∃ (c : β), f' c = Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c') ⋯

Tactic:
exact ⟨c', rfl⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → (↑(range f) : Type u_2) := fun (c : β) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) ⋯
h : WellFounded (r on f)
c : β
⊢ Acc (InvImage (Subrel r fun (x : α) ↦ x ∈ range f) f') c

Tactic:
h.apply _

Premises used: WellFounded.apply, InvImage, Subrel, Order.Preimage
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → (↑(range f) : Type u_2) := fun (c : β) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) ⋯
h : WellFounded (r on f)
c : β
⊢ Acc (InvImage (Subrel r fun (x : α) ↦ x ∈ range f) f') c

Tactic:
exact h.apply _

Premises used: WellFounded.apply
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
rw : WellFoundedOn (range fun (x : (↑s : Type u_3)) ↦ f (↑x : β)) r ↔ s.WellFoundedOn (r on f)
⊢ (f '' s).WellFoundedOn r ↔ s.WellFoundedOn (r on f)

Tactic:
rw [image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
⊢ WellFoundedOn (range fun (x : (↑s : Type u_3)) ↦ f (↑x : β)) r ↔ s.WellFoundedOn (r on f)

Tactic:
wellFoundedOn_range

Premises used: Subrel, Set.wellFoundedOn_range, Order.Preimage, Set.WellFoundedOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
⊢ WellFoundedOn (range fun (x : (↑s : Type u_3)) ↦ f (↑x : β)) r ↔ s.WellFoundedOn (r on f)

Tactic:
exact wellFoundedOn_range

Premises used: Set.wellFoundedOn_range
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
let : P x
⊢ P x

Tactic:
let Q : s → Prop := fun y => P y
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
Q : (↑s : Type u_2) → Prop := fun (y : (↑s : Type u_2)) ↦ P (↑y : α)
change : Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
⊢ P x

Tactic:
change Q ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
Q : (↑s : Type u_2) → Prop := fun (y : (↑s : Type u_2)) ↦ P (↑y : α)
⊢ Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)

Tactic:
WellFounded.induction hs ⟨x, hx⟩ ?_

Premises used: Subtype.mk, WellFounded.induction
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
Q : (↑s : Type u_2) → Prop := fun (y : (↑s : Type u_2)) ↦ P (↑y : α)
refine : ∀ (x : { x : α // x ∈ s }), (∀ (y : { x : α // x ∈ s }), Subrel r (fun (x : α) ↦ x ∈ s) y x → Q y) → Q x
⊢ Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)

Tactic:
refine WellFounded.induction hs ⟨x, hx⟩ ?_

Premises used: Subtype.mk, WellFounded.induction
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
Q : (↑s : Type u_2) → Prop := fun (y : (↑s : Type u_2)) ↦ P (↑y : α)
⊢ ∀ (x : { x : α // x ∈ s }), (∀ (y : { x : α // x ∈ s }), Subrel r (fun (x : α) ↦ x ∈ s) y x → Q y) → Q x

Tactic:
simpa only [Subtype.forall]

Premises used: Subtype.forall
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r r' : α → α → Prop
s t : Set α
h : t.WellFoundedOn r'
hle : r ≤ r'
hst : s ⊆ t
rw :
  ∀ (h : WellFounded fun (a b : α) ↦ r' a b ∧ a ∈ t ∧ b ∈ t) (hle : r ≤ r') (hst : s ⊆ t),
    WellFounded fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s
⊢ s.WellFoundedOn r

Tactic:
rw [wellFoundedOn_iff] at *

Premises used: Set.wellFoundedOn_iff
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r r' : α → α → Prop
s t : Set α
h : WellFounded fun (a b : α) ↦ r' a b ∧ a ∈ t ∧ b ∈ t
hle : r ≤ r'
hst : s ⊆ t
⊢ WellFounded fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
Subrelation.wf (fun xy => ⟨hle _ _ xy.1, hst xy.2.1, hst xy.2.2⟩) h

Premises used: Subrelation.wf
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r r' : α → α → Prop
s t : Set α
h : WellFounded fun (a b : α) ↦ r' a b ∧ a ∈ t ∧ b ∈ t
hle : r ≤ r'
hst : s ⊆ t
⊢ WellFounded fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
exact Subrelation.wf (fun xy => ⟨hle _ _ xy.1, hst xy.2.1, hst xy.2.2⟩) h

Premises used: Subrelation.wf
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r r' : α → α → Prop
s : Set α
h : ∀ a ∈ s, ∀ b ∈ s, r' a b → r a b
⊢ s.WellFoundedOn r → s.WellFoundedOn r'

Tactic:
Subrelation.wf @fun a b => h _ a.2 _ b.2

Premises used: Subrelation.wf, Subtype.val, Subtype.property, Set.WellFoundedOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
h : t.WellFoundedOn r
hst : s ⊆ t
⊢ s.WellFoundedOn r

Tactic:
h.mono le_rfl hst

Premises used: le_rfl, Set.WellFoundedOn.mono
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
⊢ Acc r a

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
⊢ WellFoundedOn {b : α | ReflTransGen r b a} r

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
⊢ ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
⊢ ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r

Tactic:
fun h => ⟨fun b => InvImage.accessible Subtype.val ?_⟩

Premises used: InvImage.accessible, WellFounded.intro, Subtype.val, Set.WellFoundedOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
refine : ∀ (h : Acc r a) (b : { x : α // Membership.mem (γ := Set α) {b : α | ReflTransGen r b a} x }), Acc r (↑b : α)
⊢ ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r

Tactic:
refine fun h => ⟨fun b => InvImage.accessible Subtype.val ?_⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
h : Acc r a
b : { x : α // Membership.mem (γ := Set α) {b : α | ReflTransGen r b a} x }
rw :
  ∀ (h : Acc (TransGen r) a) (b : { x : α // Membership.mem (γ := Set α) {b : α | ReflTransGen r b a} x }),
    Acc (TransGen r) (↑b : α)
⊢ Acc r (↑b : α)

Tactic:
rw [← acc_transGen_iff] at h ⊢

Premises used: acc_transGen_iff
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : { x : α // Membership.mem (γ := Set α) {b : α | ReflTransGen r b a} x }
inl : ∀ (h' : a = (↑b : α)), Acc (TransGen r) (↑b : α)
inr : ∀ (h' : TransGen r (↑b : α) a), Acc (TransGen r) (↑b : α)
⊢ Acc (TransGen r) (↑b : α)

Tactic:
obtain h' | h' := reflTransGen_iff_eq_or_transGen.1 b.2

Premises used: Relation.reflTransGen_iff_eq_or_transGen, Iff.mp, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : { x : α // Membership.mem (γ := Set α) {b : α | ReflTransGen r b a} x }
h' : a = (↑b : α)
inl inl₁ inl₂ inl₃ : ∀ (h : Acc (TransGen r) (↑b : α)) (h' : a = (↑b : α)), Acc (TransGen r) (↑b : α)
⊢ Acc (TransGen r) (↑b : α)

Tactic:
rwa [h'] at h
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : { x : α // Membership.mem (γ := Set α) {b : α | ReflTransGen r b a} x }
h' : TransGen r (↑b : α) a
⊢ Acc (TransGen r) (↑b : α)

Tactic:
h.inv h'

Premises used: Acc.inv
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : { x : α // Membership.mem (γ := Set α) {b : α | ReflTransGen r b a} x }
h' : TransGen r (↑b : α) a
⊢ Acc (TransGen r) (↑b : α)

Tactic:
exact h.inv h'

Premises used: Acc.inv
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
⊢ ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r

Tactic:
tfae_have 1 → 2 := by
    refine fun h => ⟨fun b => InvImage.accessible Subtype.val ?_⟩
    rw [← acc_transGen_iff] at h ⊢
    obtain h' | h' := reflTransGen_iff_eq_or_transGen.1 b.2
    · rwa [h'] at h
    · exact h.inv h'
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
⊢ WellFoundedOn {b : α | ReflTransGen r b a} r

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
⊢ WellFoundedOn {b : α | TransGen r b a} r

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
⊢ ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
⊢ ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r

Tactic:
tfae_have 2 → 3 := fun h => h.subset fun _ => TransGen.to_reflTransGen
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
tfae_2_to_3 : ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r
⊢ WellFoundedOn {b : α | TransGen r b a} r

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
tfae_2_to_3 : ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r
⊢ Acc r a

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false