α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
⊢ Acc r x
α : Type u_1
r : α → α → Prop
⊢ WellFounded r ↔ ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
refine ⟨fun h => h.has_min, fun h => ⟨fun x => ?_⟩⟩
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
⊢ False
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
⊢ Acc r x
by_contra hx
case intro.intro
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
⊢ False
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
⊢ False
obtain ⟨m, hm, hm'⟩ := h {x | ¬Acc r x} ⟨x, hx⟩
case intro.intro
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
y : α
hy : r y m
⊢ Acc r y
case intro.intro
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
⊢ False
refine' hm ⟨_, fun y hy => _⟩
case intro.intro
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
y : α
hy : r y m
hy' : ¬Acc r y
⊢ False
case intro.intro
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
y : α
hy : r y m
⊢ Acc r y
by_contra hy'
no goals
case intro.intro
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
y : α
hy : r y m
hy' : ¬Acc r y
⊢ False
exact hm' y hy' hy