awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t_1 : Set α
a b : α
P : α → Prop
inst : LE α
t : RelUpperSet P
carrier : Set α
isRelUpperSet' : IsRelUpperSet carrier P
h : (RelUpperSet.mk (P := P) carrier isRelUpperSet').carrier (P := P) = t.carrier (P := P)
⊢ RelUpperSet.mk (P := P) carrier isRelUpperSet' = t
have mk : ∀ (carrier_1 : Set α) (isRelUpperSet'_1 : IsRelUpperSet carrier_1 P)
  (h :
    (RelUpperSet.mk (P := P) carrier isRelUpperSet').carrier (P := P) =
      (RelUpperSet.mk (P := P) carrier_1 isRelUpperSet'_1).carrier (P := P)),
  RelUpperSet.mk (P := P) carrier isRelUpperSet' = RelUpperSet.mk (P := P) carrier_1 isRelUpperSet'_1
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s_1 t_1 : Set α
a b : α
P : α → Prop
inst : LE α
s t : RelLowerSet P
h : s.carrier (P := P) = t.carrier (P := P)
⊢ s = t
have mk : ∀ (carrier : Set α) (isRelLowerSet' : IsRelLowerSet carrier P)
  (h : (RelLowerSet.mk (P := P) carrier isRelLowerSet').carrier (P := P) = t.carrier (P := P)),
  RelLowerSet.mk (P := P) carrier isRelLowerSet' = t
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t_1 : Set α
a b : α
P : α → Prop
inst : LE α
t : RelLowerSet P
carrier : Set α
isRelLowerSet' : IsRelLowerSet carrier P
h : (RelLowerSet.mk (P := P) carrier isRelLowerSet').carrier (P := P) = t.carrier (P := P)
⊢ RelLowerSet.mk (P := P) carrier isRelLowerSet' = t
have mk : ∀ (carrier_1 : Set α) (isRelLowerSet'_1 : IsRelLowerSet carrier_1 P)
  (h :
    (RelLowerSet.mk (P := P) carrier isRelLowerSet').carrier (P := P) =
      (RelLowerSet.mk (P := P) carrier_1 isRelLowerSet'_1).carrier (P := P)),
  RelLowerSet.mk (P := P) carrier isRelLowerSet' = RelLowerSet.mk (P := P) carrier_1 isRelLowerSet'_1
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
a : α
inst : Preorder α
c x : α
b : x ∈ Icc a c
⊢ (fun (x : α) ↦ x ≤ c) x ∧ ∀ ⦃b : α⦄, x ≤ b → (fun (x : α) ↦ x ≤ c) b → b ∈ Icc a c
have simp_all : ∀ (b : a ≤ x ∧ x ≤ c) ⦃b : α⦄, x ≤ b → b ≤ c → a ≤ b
Tactic: simp_all only [mem_Icc, and_true, true_and]
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.UpperLower.Relative (goal)
Goal:
α : Type u_1
a : α
inst : Preorder α
c x : α
b : x ∈ Icc c a
⊢ (fun (x : α) ↦ c ≤ x) x ∧ ∀ ⦃b : α⦄, b ≤ x → (fun (x : α) ↦ c ≤ x) b → b ∈ Icc c a
have simp_all : ∀ (b : c ≤ x ∧ x ≤ a) ⦃b : α⦄, b ≤ x → c ≤ b → b ≤ a
Tactic: simp_all only [mem_Icc, true_and]
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.WellFounded (hypothesis)
Goal:
α : Sort u_1
a : α
r : α → α → Prop
h : ¬Acc r a
⊢ ∃ (b : α), ¬Acc r b ∧ r b a
have h₁ : ¬∀ (b : α), r b a → Acc r b
Tactic: rw [acc_def] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.WellFounded (hypothesis)
Goal:
α : Sort u_1
a : α
r : α → α → Prop
h : ¬∀ (b : α), r b a → Acc r b
⊢ ∃ (b : α), ¬Acc r b ∧ r b a
have h₁ : ∃ (b : α), r b a ∧ ¬Acc r b
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
Goal:
α : Sort u_1
r : α → α → Prop
x : α
⊢ Acc r x ↔ IsEmpty.{max 1 u_1} { f : ℕ → α // f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n) }
have contrapose! : ¬Acc r x ↔ Nonempty.{max 1 u_1} { f : ℕ → α // f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n) }
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
Goal:
α : Sort u_1
r : α → α → Prop
x : α
⊢ ¬Acc r x ↔ Nonempty.{max 1 u_1} { f : ℕ → α // f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n) }
have rw : ¬Acc r x ↔ ∃ (a : ℕ → α), a 0 = x ∧ ∀ (n : ℕ), r (a (n + 1)) (a n)
Tactic: rw [nonempty_subtype]
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
Goal:
α : Type u_1
r : α → α → Prop
⊢ WellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
have refine : ∀ (h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m) (x : α), Acc r x
Tactic: refine ⟨fun h => h.has_min, fun h => ⟨fun x => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
Goal:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
⊢ Acc r x
have by_contra : ∀ (hx : ¬Acc r x), False
Tactic: by_contra hx
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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
⊢ False
have 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
Tactic: obtain ⟨m, hm, hm'⟩ := h {x | ¬Acc r x} ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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
have refine : ∀ (y : α) (hy : r y m), Acc r y
Tactic: refine hm ⟨_, fun y hy => ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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
⊢ Acc r y
have by_contra : ∀ (hy' : ¬Acc r y), False
Tactic: by_contra hy'
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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)
have refine_1 : ∀ (h : IsWellOrder α r) (s : Set α) (hs : 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 := ?_ }⟩
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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)
⊢ IsWellOrder α r ↔ ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
have refine_2 : ∀ (h : ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)), WellFounded r
Tactic: refine ⟨fun h s hs ↦ ?_, fun h ↦ { wf := ?_, trichotomous a b := ?_ }⟩
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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
⊢ IsWellOrder α r ↔ ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
have 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
Tactic: refine ⟨fun h s hs ↦ ?_, fun h ↦ { wf := ?_, trichotomous a b := ?_ }⟩
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
Goal:
α : Type u_1
β : Type u_2
r : β → β → Prop
inst : Std.Trichotomous r
wf : WellFounded r
f : α → β
s : Set α
hne : s.Nonempty
⊢ wf.min (r := r) (f '' s) ⋯ = f (min (r := Function.onFun r f) ⋯ s hne)
have apply : ∀ (x : β), x ∈ f '' s → ¬r x (f (min (r := Function.onFun r f) sorry s hne))
Tactic: apply min_eq_of_forall_not_lt wf <| Set.mem_image_of_mem f <| min_mem wf.onFun s hne
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
Goal:
α : Type u_1
r : α → α → Prop
h : IsWellFounded α r
f : ℕ → α
⊢ ∃ (n : ℕ), ¬r (f (n + 1)) (f n)
have by_contra! : ∀ (hf : ∀ (n : ℕ), r (f (n + 1)) (f n)), False
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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
⊢ f = g
have h : ∀ (a : β), f a = g a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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 : β
⊢ f a = g a
have h : ∀ (x : β), (∀ (y : β), y < x → f y = g y) → f x = g x
Tactic: apply WellFoundedLT.induction a
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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
⊢ f a = g a
have h : ∀ (b : β) (hb : g b = f a), f a = g a
Tactic: obtain ⟨b, hb⟩ := hfg ▸ mem_range_self a
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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
⊢ f a = g a
have h : ∀ (h : b < a), f a = g a
Tactic: obtain h | rfl | h := lt_trichotomy b a
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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
⊢ f a = g a
have h₁ : ∀ (IH : ∀ (y : β), y < b → f y = g y) (hb : g b = f b), f b = g b
Tactic: obtain h | rfl | h := lt_trichotomy b a
Cleared hypotheses: a, IH, hb
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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
⊢ f a = g a
have h₂ : ∀ (h : a < b), f a = g a
Tactic: obtain h | rfl | h := lt_trichotomy b a
-- Lean 4 proof step from Mathlib.Order.WellFounded (hypothesis)
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 a = g a
have hb₁ : f b = f a
Tactic: rw [← IH b h] at hb
Cleared hypotheses: hb, h
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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
⊢ f b = g b
have h : f b = f b
Tactic: rw [hb]
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
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
⊢ f a = g a
have h₁ : ∀ (c : β) (hc : f c = g a), f a = g a
Tactic: obtain ⟨c, hc⟩ := hfg.symm ▸ mem_range_self a
-- Lean 4 proof step from Mathlib.Order.WellFounded (hypothesis)
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
⊢ f a = g a
have this : g a < g b
Tactic: have := hg h
-- Lean 4 proof step from Mathlib.Order.WellFounded (hypothesis)
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
⊢ f a = g a
have this₁ : c < a
Tactic: rw [hb, ← hc, hf.lt_iff_lt] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.WellFounded (hypothesis)
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
⊢ f a = g a
have hc₁ : g c = g a
Tactic: rw [IH c this] at hc
Cleared hypotheses: hc, this
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
Goal:
β : Type u_2
inst : LinearOrder β
inst_1 : WellFoundedLT β
f : β → β
hf : StrictMono f
⊢ id ≤ f
have rw : ∀ (i : β), id i ≤ f i
Tactic: rw [Pi.le_def]
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
Goal:
β : Type u_2
inst : LinearOrder β
inst_1 : WellFoundedLT β
f : β → β
hf : StrictMono f
⊢ ∀ (i : β), id i ≤ f i
have by_contra! : ∀ (H : ∃ (i : β), f i < id i), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
Goal:
β : Type u_2
inst : LinearOrder β
inst_1 : WellFoundedLT β
f : β → β
hf : StrictMono f
H : ∃ (i : β), f i < id i
⊢ False
have obtain : ∀ (m : β) (hm : Membership.mem (γ := Set β) {i : β | f i < i} m)
  (hm' : ∀ (x : β), Membership.mem (γ := Set β) {i : β | f i < i} x → ¬x < m), False
Tactic: obtain ⟨m, hm, hm'⟩ := wellFounded_lt.has_min {i | f i < i} H
-- Lean 4 proof step from Mathlib.Order.WellFounded (goal)
Goal:
β : Type u_2
inst : LinearOrder β
f : β → β
inst_1 : WellFoundedLT β
inst_2 : NoMaxOrder β
hf : StrictMono f
a : β
ha : a ∈ upperBounds (Set.range f)
⊢ False
have obtain : ∀ (b : β) (hb : a < b), False
Tactic: obtain ⟨b, hb⟩ := exists_gt a
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.WellFoundedOn r ↔ WellFounded fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s
have 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
Tactic: have f : RelEmbedding (Subrel r (· ∈ s)) fun a b : α => r a b ∧ a ∈ s ∧ b ∈ s :=
    ⟨⟨(↑), Subtype.coe_injective⟩, by simp⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
have refine : ∀ (h : s.WellFoundedOn r), WellFounded fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s
Tactic: refine ⟨fun h => ?_, f.wellFounded⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ WellFounded fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s
have rw : ∀ (s_1 : Set α), s_1.Nonempty → ∃ m ∈ s_1, ∀ x ∈ s_1, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
Tactic: rw [WellFounded.wellFounded_iff_has_min]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
have pos : ∀ (hst : (s ∩ t).Nonempty), ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
Tactic: by_cases hst : (s ∩ t).Nonempty
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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)
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
have neg : ∀ (hst : ¬(s ∩ t).Nonempty), ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
Tactic: by_cases hst : (s ∩ t).Nonempty
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
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
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
have hst₁ : Set.Nonempty (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
Tactic: rw [← Subtype.preimage_coe_nonempty] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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 ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
have 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)
Tactic: rcases h.has_min (Subtype.val ⁻¹' t) hst with ⟨⟨m, ms⟩, mt, hm⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
have neg : ∀ (m : α) (mt : m ∈ t), ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
Tactic: rcases ht with ⟨m, mt⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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)
have refine : ∀ (h : WellFounded (r on f)) (a : { x : α // x ∈ range f }), Acc (Subrel r fun (x : α) ↦ x ∈ range f) a
Tactic: refine ⟨fun h => (InvImage.wf f' h).mono fun c c' => id, fun h => ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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) ⋯)
have refine_1 : ∀ {a : β} {b : (↑(range f) : Type u_2)}, Subrel r (fun (x : α) ↦ x ∈ range f) b (f' a) → ∃ (c : β), f' c = b
Tactic: refine Acc.of_downward_closed f' ?_ _ ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ Acc (α := { x : α // x ∈ range f }) (Subrel r fun (x : α) ↦ x ∈ range f)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f c) ⋯)
have refine_2 : Acc (InvImage (Subrel r fun (x : α) ↦ x ∈ range f) f') c
Tactic: refine Acc.of_downward_closed f' ?_ _ ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
⊢ (f '' s).WellFoundedOn r ↔ s.WellFoundedOn (r on f)
have rw : WellFoundedOn (range fun (x : (↑s : Type u_3)) ↦ f (↑x : β)) r ↔ s.WellFoundedOn (r on f)
Tactic: rw [image_eq_range]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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 : α)
⊢ P x
have change : Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
Tactic: change Q ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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)
have refine : ∀ (x : { x : α // x ∈ s }), (∀ (y : { x : α // x ∈ s }), Subrel r (fun (x : α) ↦ x ∈ s) y x → Q y) → Q x
Tactic: refine WellFounded.induction hs ⟨x, hx⟩ ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r r' : α → α → Prop
s t : Set α
h : t.WellFoundedOn r'
hle : r ≤ r'
hst : s ⊆ t
⊢ s.WellFoundedOn r
have 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
Tactic: rw [wellFoundedOn_iff] at *
Cleared hypotheses: h, hle, hst
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_6
r : α → α → Prop
a : α
⊢ ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
have refine : ∀ (h : Acc r a) (b : { x : α // Membership.mem (γ := Set α) {b : α | ReflTransGen r b a} x }), Acc r (↑b : α)
Tactic: refine fun h => ⟨fun b => InvImage.accessible Subtype.val ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_6
r : α → α → Prop
a : α
h : Acc r a
b : { x : α // Membership.mem (γ := Set α) {b : α | ReflTransGen r b a} x }
⊢ Acc r (↑b : α)
have rw : ∀ (h : Acc (TransGen r) a) (b : { x : α // Membership.mem (γ := Set α) {b : α | ReflTransGen r b a} x }),
  Acc (TransGen r) (↑b : α)
Tactic: rw [← acc_transGen_iff] at h ⊢
Cleared hypotheses: h, b
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : { x : α // Membership.mem (γ := Set α) {b : α | ReflTransGen r b a} x }
⊢ Acc (TransGen r) (↑b : α)
have inl : ∀ (h' : a = (↑b : α)), Acc (TransGen r) (↑b : α)
Tactic: obtain h' | h' := reflTransGen_iff_eq_or_transGen.1 b.2
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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 : α)
⊢ Acc (TransGen r) (↑b : α)
have inr : ∀ (h' : TransGen r (↑b : α) a), Acc (TransGen r) (↑b : α)
Tactic: obtain h' | h' := reflTransGen_iff_eq_or_transGen.1 b.2