awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFounded
Goal:
α : Sort u_1
r : α → α → Prop
x : α
contrapose! : ¬Acc r x ↔ Nonempty.{max 1 u_1} { f : ℕ → α // f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n) }
⊢ Acc r x ↔ IsEmpty.{max 1 u_1} { f : ℕ → α // f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n) }

Tactic:
contrapose!
-- Module: Mathlib.Order.WellFounded
Goal:
α : Sort u_1
r : α → α → Prop
x : α
rw : ¬Acc r x ↔ ∃ (a : ℕ → α), a 0 = x ∧ ∀ (n : ℕ), r (a (n + 1)) (a n)
⊢ ¬Acc r x ↔ Nonempty.{max 1 u_1} { f : ℕ → α // f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n) }

Tactic:
rw [nonempty_subtype]

Premises used: nonempty_subtype
-- Module: Mathlib.Order.WellFounded
Goal:
α : Sort u_1
r : α → α → Prop
x : α
⊢ ¬Acc r x ↔ ∃ (a : ℕ → α), a 0 = x ∧ ∀ (n : ℕ), r (a (n + 1)) (a n)

Tactic:
not_acc_iff_exists_descending_chain

Premises used: not_acc_iff_exists_descending_chain
-- Module: Mathlib.Order.WellFounded
Goal:
α : Sort u_1
r : α → α → Prop
x : α
⊢ ¬Acc r x ↔ ∃ (a : ℕ → α), a 0 = x ∧ ∀ (n : ℕ), r (a (n + 1)) (a n)

Tactic:
exact not_acc_iff_exists_descending_chain

Premises used: not_acc_iff_exists_descending_chain
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
⊢ Std.Asymm r

Tactic:
⟨h.asymmetric⟩

Premises used: WellFounded.asymmetric, Std.Asymm.mk
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
⊢ Std.Irrefl r

Tactic:
@Std.Asymm.irrefl α r h.asymm

Premises used: Std.Asymm.irrefl
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst : WellFoundedRelation α
⊢ Std.Asymm.{u_1 + 1} (α := α) WellFoundedRelation.rel

Tactic:
WellFoundedRelation.wf.asymm

Premises used: WellFoundedRelation.wf, WellFounded.asymm
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r r' : α → α → Prop
hr : WellFounded r
h : ∀ (a b : α), r' a b → r a b
⊢ WellFounded r'

Tactic:
Subrelation.wf (h _ _) hr

Premises used: Subrelation.wf
-- Module: Mathlib.Order.WellFounded
Goal:
α : Sort u_4
β : Sort u_5
r : β → β → Prop
f : α → β
⊢ WellFounded r → WellFounded (r on f)

Tactic:
InvImage.wf _

Premises used: InvImage, InvImage.wf
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
H : WellFounded r
s : Set α
h : s.Nonempty
⊢ H.min (r := r) s h ∈ s

Tactic:
let ⟨h, _⟩ := Classical.choose_spec (H.has_min s h)
  h

Premises used: Membership.mem, Classical.choose_spec, _private.0.WellFounded.min_mem.match_1, WellFounded.min, WellFounded.has_min
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
H : WellFounded r
p : α → Prop
h : ∃ (a : α), p a
⊢ p (H.min (r := r) {a : α | p a} h)

Tactic:
H.min_mem {a | p a} h

Premises used: WellFounded.min_mem, Set.Mem, setOf
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
H : WellFounded r
s : Set α
x : α
hx : x ∈ s
⊢ ¬r x (H.min (r := r) s ⋯)

Tactic:
let ⟨_, h'⟩ := Classical.choose_spec (H.has_min s ⟨x, hx⟩)
  h' _ hx

Premises used: _private.0.WellFounded.not_lt_min.match_1, Classical.choose_spec, WellFounded.min, Exists.intro, WellFounded.has_min, Not
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Trichotomous r
wf : WellFounded r
s : Set α
m : α
hms : m ∈ s
hrm : ∀ (x : α), x ∈ s → ¬r x m
⊢ wf.min (r := r) s ⋯ = m

Tactic:
Std.Trichotomous.trichotomous _ m (hrm _ <| wf.min_mem s _) (wf.not_lt_min s hms)

Premises used: WellFounded.min_mem, WellFounded.not_lt_min, Std.Trichotomous.trichotomous
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
wf : WellFounded r
s : Set α
hs : s.Nonempty
x : α
hx : r x (wf.min (r := r) s hs)
⊢ ¬x ∈ s

Tactic:
(wf.not_lt_min s · hx)

Premises used: WellFounded.not_lt_min, Not
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
wf : WellFounded r
s : Set α
hs : sᶜ.Nonempty
x : α
hx : r x (wf.min (r := r) sᶜ hs)
⊢ x ∈ s

Tactic:
Set.notMem_compl_iff.mp <| notMem_of_lt_min hx

Premises used: WellFounded.notMem_of_lt_min, Set.notMem_compl_iff, Iff.mp
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
⊢ WellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m

Tactic:
⟨fun h => h.has_min, fun h => ⟨fun x => ?_⟩⟩

Premises used: WellFounded.intro, Iff.intro, WellFounded.has_min
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
refine : ∀ (h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m) (x : α), Acc r x
⊢ WellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m

Tactic:
refine ⟨fun h => h.has_min, fun h => ⟨fun x => ?_⟩⟩
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
by_contra : ∀ (hx : ¬Acc r x), False
⊢ Acc r x

Tactic:
by_contra hx
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
obtain :
  ∀ (m : α) (hm : Membership.mem (γ := Set α) {x : α | ¬Acc r x} m)
    (hm' : ∀ (x : α), Membership.mem (γ := Set α) {x : α | ¬Acc r x} x → ¬r x m), False
⊢ False

Tactic:
obtain ⟨m, hm, hm'⟩ := h {x | ¬Acc r x} ⟨x, hx⟩

Premises used: setOf, Acc, Exists.intro, Not
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : Membership.mem (γ := Set α) {x : α | ¬Acc r x} m
hm' : ∀ (x : α), Membership.mem (γ := Set α) {x : α | ¬Acc r x} x → ¬r x m
⊢ False

Tactic:
hm ⟨_, fun y hy => ?_⟩

Premises used: Acc.intro
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : Membership.mem (γ := Set α) {x : α | ¬Acc r x} m
hm' : ∀ (x : α), Membership.mem (γ := Set α) {x : α | ¬Acc r x} x → ¬r x m
refine : ∀ (y : α) (hy : r y m), Acc r y
⊢ False

Tactic:
refine hm ⟨_, fun y hy => ?_⟩

Premises used: Acc.intro
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : Membership.mem (γ := Set α) {x : α | ¬Acc r x} m
hm' : ∀ (x : α), Membership.mem (γ := Set α) {x : α | ¬Acc r x} x → ¬r x m
y : α
hy : r y m
by_contra : ∀ (hy' : ¬Acc r y), False
⊢ Acc r y

Tactic:
by_contra hy'
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : Membership.mem (γ := Set α) {x : α | ¬Acc r x} m
hm' : ∀ (x : α), Membership.mem (γ := Set α) {x : α | ¬Acc r x} x → ¬r x m
y : α
hy : r y m
hy' : ¬Acc r y
⊢ False

Tactic:
hm' y hy' hy
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : Membership.mem (γ := Set α) {x : α | ¬Acc r x} m
hm' : ∀ (x : α), Membership.mem (γ := Set α) {x : α | ¬Acc r x} x → ¬r x m
y : α
hy : r y m
hy' : ¬Acc r y
⊢ False

Tactic:
exact hm' y hy' hy
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
inst : Preorder α
⊢ WellFoundedLT α ↔ ∀ (s : Set α), s.Nonempty → ∃ (m : α), Minimal (fun (x : α) ↦ x ∈ s) m

Tactic:
simp only [isWellFounded_iff, wellFounded_iff_has_min, not_lt_iff_le_imp_ge, Minimal]

Premises used: isWellFounded_iff, WellFounded.wellFounded_iff_has_min, Minimal, not_lt_iff_le_imp_ge
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
⊢ IsWellOrder α r ↔ ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)

Tactic:
⟨fun h s hs ↦ ?_, fun h ↦ { wf := ?_, trichotomous a b := ?_ }⟩

Premises used: IsWellOrder.mk, Iff.intro
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
refine_1 :
  ∀ (h : IsWellOrder α r) (s : Set α) (hs : s.Nonempty), ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
refine_2 :
  ∀ (h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)), WellFounded r
refine_3 :
  ∀ (h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)) (a b : α),
    ¬r a b → ¬r b a → a = b
⊢ IsWellOrder α r ↔ ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)

Tactic:
refine ⟨fun h s hs ↦ ?_, fun h ↦ { wf := ?_, trichotomous a b := ?_ }⟩
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
s : Set α
hs : s.Nonempty
⊢ ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)

Tactic:
grind [h.wf.has_min, trichotomous_of r]

Premises used: IsWellFounded.wf, WellFounded.has_min, trichotomous_of
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
⊢ WellFounded r

Tactic:
grind [wellFounded_iff_has_min]

Premises used: WellFounded.wellFounded_iff_has_min
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
a b : α
⊢ Set.Nonempty (α := α) {a, b}

Tactic:
simp
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
a b : α
⊢ ¬r a b → ¬r b a → a = b

Tactic:
grind [h {a, b} <| by simp]

Premises used: Insert.insert, Singleton.singleton
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
β : Type u_2
r : β → β → Prop
inst : Std.Trichotomous r
wf : WellFounded r
f : α → β
s : Set α
hne : s.Nonempty
apply : ∀ (x : β), x ∈ f '' s → ¬r x (f (min (r := Function.onFun r f) ⋯ s hne))
⊢ wf.min (r := r) (f '' s) ⋯ = f (min (r := Function.onFun r f) ⋯ s hne)

Tactic:
apply min_eq_of_forall_not_lt wf <| Set.mem_image_of_mem f <| min_mem wf.onFun s hne

Premises used: WellFounded.min_mem, WellFounded.min_eq_of_forall_not_lt, Set.mem_image_of_mem, WellFounded.onFun
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
β : Type u_2
r : β → β → Prop
inst : Std.Trichotomous r
wf : WellFounded r
f : α → β
s : Set α
hne : s.Nonempty
a : α
has : a ∈ s
⊢ ¬r (f a) (f (min (r := Function.onFun r f) ⋯ s hne))

Tactic:
wf.onFun.not_lt_min s has

Premises used: WellFounded.not_lt_min, WellFounded.onFun
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
β : Type u_2
r : β → β → Prop
inst : Std.Trichotomous r
wf : WellFounded r
f : α → β
s : Set α
hne : s.Nonempty
a : α
has : a ∈ s
⊢ ¬r (f a) (f (min (r := Function.onFun r f) ⋯ s hne))

Tactic:
exact wf.onFun.not_lt_min s has

Premises used: WellFounded.not_lt_min, WellFounded.onFun
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : IsWellFounded α r
f : ℕ → α
by_contra! : ∀ (hf : ∀ (n : ℕ), r (f (n + 1)) (f n)), False
⊢ ∃ (n : ℕ), ¬r (f (n + 1)) (f n)

Tactic:
by_contra! hf
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : IsWellFounded α r
f : ℕ → α
hf : ∀ (n : ℕ), r (f (n + 1)) (f n)
⊢ False

Tactic:
(wellFounded_iff_isEmpty_descending_chain.1 h.wf).elim ⟨f, hf⟩

Premises used: wellFounded_iff_isEmpty_descending_chain, IsEmpty.elim, IsWellFounded.wf, Subtype.mk, Iff.mp
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
h : IsWellFounded α r
f : ℕ → α
hf : ∀ (n : ℕ), r (f (n + 1)) (f n)
⊢ False

Tactic:
exact (wellFounded_iff_isEmpty_descending_chain.1 h.wf).elim ⟨f, hf⟩
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
r : α → α → Prop
wf : WellFounded r
s : Set α
h : Bounded r s
x : α
hx : x ∈ s
⊢ r x (wf.sup (r := r) s h)

Tactic:
min_mem wf { x | ∀ a ∈ s, r a x } h x hx

Premises used: WellFounded.min_mem, setOf, WellFounded.sup
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
h : WellFounded fun (x1 x2 : β) ↦ x1 < x2
x : β
s : Set β
hx : x ∈ s
⊢ h.min (r := fun (x1 x2 : β) ↦ x1 < x2) s ⋯ ≤ x

Tactic:
not_lt.1 <| h.not_lt_min _ hx

Premises used: not_lt, Iff.mp, WellFounded.not_lt_min
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
h : ∀ (a : β), f a = g a
⊢ f = g

Tactic:
ext a
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a : β
h : ∀ (x : β), (∀ (y : β), y < x → f y = g y) → f x = g x
⊢ f a = g a

Tactic:
apply WellFoundedLT.induction a

Premises used: WellFoundedLT.induction
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a_1 a : β
IH : ∀ (y : β), y < a → f y = g y
h : ∀ (b : β) (hb : g b = f a), f a = g a
⊢ f a = g a

Tactic:
obtain ⟨b, hb⟩ := hfg ▸ mem_range_self a
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a_1 a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : ∀ (h : b < a), f a = g a
h₁ : ∀ (IH : ∀ (y : β), y < b → f y = g y) (hb : g b = f b), f b = g b
h₂ : ∀ (h : a < b), f a = g a
⊢ f a = g a

Tactic:
obtain h | rfl | h := lt_trichotomy b a

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a_1 a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : b < a
⊢ f b = f a

Tactic:
rw [← IH b h] at hb
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a_1 a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : b < a
hb₁ : f b = f a
⊢ b < a

Tactic:
rw [← IH b h] at hb
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a_1 a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : f b = f a
h : b < a
⊢ f a = g a

Tactic:
cases (hf.injective hb).not_lt h

Premises used: StrictMono.injective, Eq.not_lt
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a b : β
IH : ∀ (y : β), y < b → f y = g y
hb : g b = f b
h h₁ : f b = f b
⊢ f b = g b

Tactic:
rw [hb]
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a_1 a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
h₁ : ∀ (c : β) (hc : f c = g a), f a = g a
⊢ f a = g a

Tactic:
obtain ⟨c, hc⟩ := hfg.symm ▸ mem_range_self a
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a_1 a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
⊢ g a < g b

Tactic:
have := hg h
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a_1 a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : g a < g b
⊢ c < a

Tactic:
rw [hb, ← hc, hf.lt_iff_lt] at this

Premises used: StrictMono.lt_iff_lt
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a_1 a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : c < a
⊢ g c = g a

Tactic:
rw [IH c this] at hc
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a_1 a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : c < a
hc₁ : g c = g a
⊢ c < a

Tactic:
rw [IH c this] at hc
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f : β → γ
hf : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} f
g : β → γ
hg : Membership.mem (γ := Set (β → γ)) {f : β → γ | StrictMono f} g
hfg : range f = range g
a_1 a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : g c = g a
this : c < a
⊢ f a = g a

Tactic:
cases (hg.injective hc).not_lt this

Premises used: StrictMono.injective, Eq.not_lt
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedGT β
⊢ InjOn (α := β → γ) range {f : β → γ | StrictAnti f}

Tactic:
fun _ hf _ hg ↦ Set.range_injOn_strictMono (β := βᵒᵈ) hf.dual hg.dual

Premises used: StrictAnti.dual, Set.range_injOn_strictMono, OrderDual, Set.InjOn
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedLT β
f g : β → γ
hf : StrictMono f
hg : StrictMono g
⊢ Set.range f = Set.range g ↔ f = g

Tactic:
Set.range_injOn_strictMono.eq_iff hf hg

Premises used: Set.InjOn.eq_iff, Set.range_injOn_strictMono
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : Preorder γ
inst_2 : WellFoundedGT β
f g : β → γ
hf : StrictAnti f
hg : StrictAnti g
⊢ Set.range f = Set.range g ↔ f = g

Tactic:
Set.range_injOn_strictAnti.eq_iff hf hg

Premises used: Set.InjOn.eq_iff, Set.range_injOn_strictAnti
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
inst_1 : WellFoundedLT β
f : β → β
hf : StrictMono f
rw : ∀ (i : β), id i ≤ f i
⊢ id ≤ f

Tactic:
rw [Pi.le_def]

Premises used: Pi.le_def
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
inst_1 : WellFoundedLT β
f : β → β
hf : StrictMono f
by_contra! : ∀ (H : ∃ (i : β), f i < id i), False
⊢ ∀ (i : β), id i ≤ f i

Tactic:
by_contra! H
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
inst_1 : WellFoundedLT β
f : β → β
hf : StrictMono f
H : ∃ (i : β), f i < id i
obtain :
  ∀ (m : β) (hm : Membership.mem (γ := Set β) {i : β | f i < i} m)
    (hm' : ∀ (x : β), Membership.mem (γ := Set β) {i : β | f i < i} x → ¬x < m), False
⊢ False

Tactic:
obtain ⟨m, hm, hm'⟩ := wellFounded_lt.has_min {i | f i < i} H

Premises used: setOf, wellFounded_lt, LT.lt, WellFounded.has_min
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
inst_1 : WellFoundedLT β
f : β → β
hf : StrictMono f
H : ∃ (i : β), f i < id i
m : β
hm : Membership.mem (γ := Set β) {i : β | f i < i} m
hm' : ∀ (x : β), Membership.mem (γ := Set β) {i : β | f i < i} x → ¬x < m
⊢ False

Tactic:
hm' _ (hf hm) hm
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
inst_1 : WellFoundedLT β
f : β → β
hf : StrictMono f
H : ∃ (i : β), f i < id i
m : β
hm : Membership.mem (γ := Set β) {i : β | f i < i} m
hm' : ∀ (x : β), Membership.mem (γ := Set β) {i : β | f i < i} x → ¬x < m
⊢ False

Tactic:
exact hm' _ (hf hm) hm
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
inst_1 : WellFoundedLT β
f : β → β
hf : StrictMono f
x : β
⊢ x ≤ f x

Tactic:
hf.id_le x

Premises used: StrictMono.id_le
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
inst_1 : WellFoundedGT β
f : β → β
hf : StrictMono f
⊢ f ≤ id

Tactic:
StrictMono.id_le (β := βᵒᵈ) hf.dual

Premises used: StrictMono.dual, StrictMono.id_le, OrderDual
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
inst_1 : WellFoundedGT β
f : β → β
hf : StrictMono f
x : β
⊢ f x ≤ x

Tactic:
StrictMono.le_apply (β := βᵒᵈ) hf.dual

Premises used: StrictMono.le_apply, StrictMono.dual
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
f : β → β
inst_1 : WellFoundedLT β
inst_2 : NoMaxOrder β
hf : StrictMono f
a : β
ha : a ∈ upperBounds (Set.range f)
obtain : ∀ (b : β) (hb : a < b), False
⊢ False

Tactic:
obtain ⟨b, hb⟩ := exists_gt a

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
f : β → β
inst_1 : WellFoundedLT β
inst_2 : NoMaxOrder β
hf : StrictMono f
a : β
ha : a ∈ upperBounds (Set.range f)
b : β
hb : a < b
⊢ False

Tactic:
((hf.le_apply.trans_lt (hf hb)).trans_le <| ha (Set.mem_range_self _)).false

Premises used: StrictMono.le_apply, Set.mem_range_self, LT.lt.trans_le, LT.lt.false, LE.le.trans_lt
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
f : β → β
inst_1 : WellFoundedLT β
inst_2 : NoMaxOrder β
hf : StrictMono f
a : β
ha : a ∈ upperBounds (Set.range f)
b : β
hb : a < b
⊢ False

Tactic:
exact ((hf.le_apply.trans_lt (hf hb)).trans_le <| ha (Set.mem_range_self _)).false

Premises used: StrictMono.le_apply, Set.mem_range_self, LT.lt.trans_le, LT.lt.false, LE.le.trans_lt
-- Module: Mathlib.Order.WellFounded
Goal:
β : Type u_2
inst : LinearOrder β
f : β → β
inst_1 : WellFoundedGT β
inst_2 : NoMinOrder β
hf : StrictMono f
⊢ ¬BddBelow (Set.range f)

Tactic:
hf.dual.not_bddAbove_range_of_wellFoundedLT

Premises used: lowerBounds, Set.Mem, setOf, StrictMono.not_bddAbove_range_of_wellFoundedLT, StrictMono.dual, BddBelow, OrderDual
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LT β
inst_1 : WellFoundedLT β
inst_2 : Nonempty α
a : α
⊢ ¬f a < f (argmin f)

Tactic:
WellFounded.not_lt_min (InvImage.wf f wellFounded_lt) _ (Set.mem_univ a)

Premises used: Function.argmin, InvImage, wellFounded_lt, Set.mem_univ, WellFounded.not_lt_min, InvImage.wf
-- Module: Mathlib.Order.WellFounded
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LT β
inst_1 : WellFoundedLT β
s : Set α
hs : s.Nonempty
⊢ argminOn f s hs ∈ s

Tactic:
WellFounded.min_mem _ _ _

Premises used: WellFounded.min_mem, Set.Mem, Function.argminOn