case mp
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y (WellFounded.succ (_ : WellFounded r) x) → r y x ∨ y = x

case mpr
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y x ∨ y = x → r y (WellFounded.succ (_ : WellFounded r) x)
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y (WellFounded.succ (_ : WellFounded r) x) ↔ r y x ∨ y = x
constructor
case mpr.inl
α : Type u_1
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
r : α → α → Prop
wo : IsWellOrder α r
y : α
h : ∃ y_1, r y y_1
⊢ r y (WellFounded.succ (_ : WellFounded r) y)
case mpr
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y x ∨ y = x → r y (WellFounded.succ (_ : WellFounded r) x)
rintro (hy | rfl)
case mpr.inr
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
y : α
h : ∃ y_1, r y y_1
⊢ r y (WellFounded.succ (_ : WellFounded r) y)
case mpr.inl
α : Type u_1
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
r : α → α → Prop
wo : IsWellOrder α r
y : α
h : ∃ y_1, r y y_1
⊢ r y (WellFounded.succ (_ : WellFounded r) y)
exact _root_.trans hy (wo.wf.lt_succ h)
no goals
case mpr.inr
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
y : α
h : ∃ y_1, r y y_1
⊢ r y (WellFounded.succ (_ : WellFounded r) y)
exact wo.wf.lt_succ h
case mp
α : Type u_1
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
case mp
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y (WellFounded.succ (_ : WellFounded r) x) → r y x ∨ y = x
intro h'
case mp
α : Type u_1
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
case mp
α : Type u_1
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
have : ¬r x y := by
  intro hy
  rw [WellFounded.succ, dif_pos] at h'
  exact wo.wf.not_lt_min _ h hy h'
case mp.inl
α : Type u_1
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
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
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
case mp
α : Type u_1
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
rcases trichotomous_of r x y with (hy | hy | hy)
case mp.inl.h
α : Type u_1
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
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
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
case mp.inl
α : Type u_1
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
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
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
exfalso
case mp.inr.inl
α : Type u_1
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
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
case mp.inl.h
α : Type u_1
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
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
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
exact this hy
case mp.inr.inl.h
α : Type u_1
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
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
case mp.inr.inl
α : Type u_1
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
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
right
case mp.inr.inr
α : Type u_1
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
case mp.inr.inl.h
α : Type u_1
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
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
exact hy.symm
case mp.inr.inr.h
α : Type u_1
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
case mp.inr.inr
α : Type u_1
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
left
no goals
case mp.inr.inr.h
α : Type u_1
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
exact hy
α : Type u_1
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
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (WellFounded.succ (_ : WellFounded r) x)
⊢ ¬r x y
intro hy
α : Type u_1
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
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
α : Type u_1
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
rw [WellFounded.succ, dif_pos] at h'
no goals
α : Type u_1
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
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
exact wo.wf.not_lt_min _ h hy h'