[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
⊢ WellFounded r ↔ ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
[PROOFSTEP]
refine ⟨fun h => h.has_min, fun h => ⟨fun x => ?_⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
⊢ Acc r x
[PROOFSTEP]
by_contra hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
h : ∀ (s : Set α), Set.Nonempty s → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
⊢ False
[PROOFSTEP]
obtain ⟨m, hm, hm'⟩ := h {x | ¬Acc r x} ⟨x, hx⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' 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
[PROOFSTEP]
refine' hm ⟨_, fun y hy => _⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' 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
[PROOFSTEP]
by_contra hy'
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' 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
[PROOFSTEP]
exact hm' y hy' hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wf : WellFounded r
x : α
h : ∃ y, r x y
⊢ r x (WellFounded.succ wf x)
[PROOFSTEP]
rw [WellFounded.succ, dif_pos h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wf : WellFounded r
x : α
h : ∃ y, r x y
⊢ r x (min wf {y | r x y} h)
[PROOFSTEP]
apply min_mem
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y (WellFounded.succ (_ : WellFounded r) x) ↔ r y x ∨ y = x
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y (WellFounded.succ (_ : WellFounded r) x) → r y x ∨ y = x
[PROOFSTEP]
intro h'
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
⊢ r y x ∨ y = x
[PROOFSTEP]
have : ¬r x y := by
  intro hy
  rw [WellFounded.succ, dif_pos] at h' 
  exact wo.wf.not_lt_min _ h hy h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
⊢ ¬r x y
[PROOFSTEP]
intro hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
hy : r x y
⊢ False
[PROOFSTEP]
rw [WellFounded.succ, dif_pos] at h' 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h'✝ : r y (if h : ∃ y, r x y then min (_ : WellFounded r) {y | r x y} h else x)
h' : r y (min (_ : WellFounded r) {y | r x y} ?hc)
hy : r x y
⊢ False
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (if h : ∃ y, r x y then min (_ : WellFounded r) {y | r x y} h else x)
hy : r x y
⊢ ∃ y, r x y
[PROOFSTEP]
exact wo.wf.not_lt_min _ h hy h'
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
⊢ r y x ∨ y = x
[PROOFSTEP]
rcases trichotomous_of r x y with (hy | hy | hy)
[GOAL]
case mp.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r x y
⊢ r y x ∨ y = x
case mp.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : x = y
⊢ r y x ∨ y = x
case mp.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r y x
⊢ r y x ∨ y = x
[PROOFSTEP]
exfalso
[GOAL]
case mp.inl.h
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r x y
⊢ False
case mp.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : x = y
⊢ r y x ∨ y = x
case mp.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r y x
⊢ r y x ∨ y = x
[PROOFSTEP]
exact this hy
[GOAL]
case mp.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : x = y
⊢ r y x ∨ y = x
case mp.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r y x
⊢ r y x ∨ y = x
[PROOFSTEP]
right
[GOAL]
case mp.inr.inl.h
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : x = y
⊢ y = x
case mp.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r y x
⊢ r y x ∨ y = x
[PROOFSTEP]
exact hy.symm
[GOAL]
case mp.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r y x
⊢ r y x ∨ y = x
[PROOFSTEP]
left
[GOAL]
case mp.inr.inr.h
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
this : ¬r x y
hy : r y x
⊢ r y x
[PROOFSTEP]
exact hy
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y x ∨ y = x → r y (WellFounded.succ (_ : WellFounded r) x)
[PROOFSTEP]
rintro (hy | rfl)
[GOAL]
case mpr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
hy : r y x
⊢ r y (WellFounded.succ (_ : WellFounded r) x)
case mpr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
y : α
h : ∃ y_1, r y y_1
⊢ r y (WellFounded.succ (_ : WellFounded r) y)
[PROOFSTEP]
exact _root_.trans hy (wo.wf.lt_succ h)
[GOAL]
case mpr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r' r : α → α → Prop
wo : IsWellOrder α r
y : α
h : ∃ y_1, r y y_1
⊢ r y (WellFounded.succ (_ : WellFounded r) y)
[PROOFSTEP]
exact wo.wf.lt_succ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
⊢ f b ≤ g b
[PROOFSTEP]
obtain ⟨c, hc⟩ : g b ∈ Set.range f := by
  rw [hfg]
  exact Set.mem_range_self b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
⊢ g b ∈ range f
[PROOFSTEP]
rw [hfg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
⊢ g b ∈ range g
[PROOFSTEP]
exact Set.mem_range_self b
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
⊢ f b ≤ g b
[PROOFSTEP]
cases' lt_or_le c b with hcb hbc
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
hcb : c < b
⊢ f b ≤ g b
[PROOFSTEP]
rw [H c hcb] at hc 
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : g c = g b
hcb : c < b
⊢ f b ≤ g b
[PROOFSTEP]
rw [hg.injective hc] at hcb 
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : g c = g b
hcb : b < b
⊢ f b ≤ g b
[PROOFSTEP]
exact hcb.false.elim
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
hbc : b ≤ c
⊢ f b ≤ g b
[PROOFSTEP]
rw [← hc]
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
b : β
H : ∀ (a : β), a < b → f a = g a
c : β
hc : f c = g b
hbc : b ≤ c
⊢ f b ≤ f c
[PROOFSTEP]
exact hf.monotone hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
⊢ f = g
[PROOFSTEP]
funext a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
a : β
⊢ f a = g a
[PROOFSTEP]
apply h.induction a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f g : β → γ
hf : StrictMono f
hg : StrictMono g
hfg : range f = range g
a : β
⊢ ∀ (x : β), (∀ (y : β), y < x → f y = g y) → f x = g x
[PROOFSTEP]
exact fun b H =>
  le_antisymm (eq_strictMono_iff_eq_range_aux hf hg hfg H)
    (eq_strictMono_iff_eq_range_aux hg hf hfg.symm fun a hab => (H a hab).symm)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f : β → β
hf : StrictMono f
⊢ ∀ (n : β), n ≤ f n
[PROOFSTEP]
by_contra' h₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f : β → β
hf : StrictMono f
h₁ : ∃ n, f n < n
⊢ False
[PROOFSTEP]
have h₂ := h.min_mem _ h₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r r' : α → α → Prop
inst✝¹ : LinearOrder β
h : WellFounded fun x x_1 => x < x_1
inst✝ : PartialOrder γ
f : β → β
hf : StrictMono f
h₁ : ∃ n, f n < n
h₂ : min h (fun x => Preorder.toLT.1 (f x) x) h₁ ∈ fun x => Preorder.toLT.1 (f x) x
⊢ False
[PROOFSTEP]
exact h.not_lt_min _ h₁ (hf h₂) h₂
