-- Mathlib/Order/WellFounded.lean
theorem lt_succ_iff {r : α → α → Prop} [wo : IsWellOrder α r] {x : α} (h : ∃ y, r x y)
    (y : α) : r y (wo.wf.succ x) ↔ r y x ∨ y = x

Proof state:
case mp.inl
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
this : ¬r x y
hy : r x y
⊢ r y x ∨ y = x

Tactic:
exfalso

Result:
case mp.inl
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
this : ¬r x y
hy : r x y
⊢ False

Proof state:
case mp.inr.inl.h
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
this : ¬r x y
hy : x = y
⊢ y = x

Tactic:
exact hy.symm

Result:
no goals

Proof state:
case mp.inr.inl
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
this : ¬r x y
hy : x = y
⊢ r y x ∨ y = x

Tactic:
right

Result:
case mp.inr.inl.h
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
this : ¬r x y
hy : x = y
⊢ y = x

Proof state:
case mp
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
this : ¬r x y
⊢ r y x ∨ y = x

Tactic:
rcases trichotomous_of r x y with (hy | hy | hy)

Result:
case mp.inl
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ 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 (⋯.succ 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 (⋯.succ x)
this : ¬r x y
hy : r y x
⊢ r y x ∨ y = x

Proof state:
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
hy : r x y
⊢ False

Tactic:
rw [WellFounded.succ, dif_pos] at h'

Result:
α : 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 {y | r x y} h else x)
h' : r y (⋯.min {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 {y | r x y} h else x)
hy : r x y
⊢ ∃ y, r x y

Proof state:
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y (⋯.succ x) ↔ r y x ∨ y = x

Tactic:
constructor

Result:
case mp
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y (⋯.succ 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 (⋯.succ x)

Proof state:
case mp.inr.inr
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
this : ¬r x y
hy : r y x
⊢ r y x ∨ y = x

Tactic:
left

Result:
case mp.inr.inr.h
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
this : ¬r x y
hy : r y x
⊢ r y x

Proof state:
case mp.inl
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
this : ¬r x y
hy : r x y
⊢ False

Tactic:
exact this hy

Result:
no goals

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

Tactic:
intro h'

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

Proof state:
case mpr
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
⊢ r y x ∨ y = x → r y (⋯.succ x)

Tactic:
rintro (hy | rfl)

Result:
case mpr.inl
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
hy : r y x
⊢ r y (⋯.succ x)

case mpr.inr
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
y : α
h : ∃ y_1, r y y_1
⊢ r y (⋯.succ y)

Proof state:
case mp.inr.inr.h
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
this : ¬r x y
hy : r y x
⊢ r y x

Tactic:
exact hy

Result:
no goals

Proof state:
case mpr.inl
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
hy : r y x
⊢ r y (⋯.succ x)

Tactic:
exact _root_.trans hy (wo.wf.lt_succ h)

Result:
no goals

Proof state:
case mp
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
⊢ r y x ∨ y = x

Tactic:
have : ¬r x y := by
  intro hy
  rw [WellFounded.succ, dif_pos] at h'
  exact wo.wf.not_lt_min _ h hy h'

Result:
case mp
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
this : ¬r x y
⊢ r y x ∨ y = x

Proof state:
case mpr.inr
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
y : α
h : ∃ y_1, r y y_1
⊢ r y (⋯.succ y)

Tactic:
exact wo.wf.lt_succ h

Result:
no goals

Proof state:
α : 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 {y | r x y} h else x)
h' : r y (⋯.min {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 {y | r x y} h else x)
hy : r x y
⊢ ∃ y, r x y

Tactic:
exact wo.wf.not_lt_min _ h hy h'

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
⊢ ¬r x y

Tactic:
intro hy

Result:
α : Type u_1
r : α → α → Prop
wo : IsWellOrder α r
x : α
h : ∃ y, r x y
y : α
h' : r y (⋯.succ x)
hy : r x y
⊢ False