-- Mathlib/Order/InitialSeg.lean
theorem eq_or_principal [IsWellOrder β s] (f : r ≼i s) :
    Surjective f ∨ ∃ b, ∀ x, x ∈ Set.range f ↔ s x b

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
⊢ ∃ a, f a = x

Tactic:
obtain ⟨y, ⟨hy, hs⟩ | ⟨hy, hs⟩⟩ := h x

Result:
case intro.inl.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
⊢ ∃ a, f a = x

case intro.inr.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∉ Set.range ⇑f
hs : s y x
⊢ ∃ a, f a = x

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
⊢ ∃ a, f a = b

Tactic:
apply IsWellFounded.induction s b

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
⊢ ∀ (x : β), (∀ (y : β), s y x → ∃ a, f a = y) → ∃ a, f a = x

Proof state:
case intro.inl.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
⊢ ∃ a, f a = x

Tactic:
obtain (rfl | h) := (trichotomous y x).resolve_left hs

Result:
case intro.inl.intro.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
y : β
hy : y ∈ Set.range ⇑f
IH : ∀ (y_1 : β), s y_1 y → ∃ a, f a = y_1
hs : ¬s y y
⊢ ∃ a, f a = y

case intro.inl.intro.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h✝ : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
h : s x y
⊢ ∃ a, f a = x

Proof state:
case intro.inr.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
z : α
hy : f z ∉ Set.range ⇑f
hs : s (f z) x
⊢ ∃ a, f a = x

Tactic:
cases hy (Set.mem_range_self z)

Result:
no goals

Proof state:
case intro.inl.intro.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
y : β
hy : y ∈ Set.range ⇑f
IH : ∀ (y_1 : β), s y_1 y → ∃ a, f a = y_1
hs : ¬s y y
⊢ ∃ a, f a = y

Tactic:
exact hy

Result:
no goals

Proof state:
case intro.inl.intro.inr.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h✝ : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
z : α
hs : ¬s (f z) x
h : s x (f z)
⊢ ∃ a, f a = x

Tactic:
exact f.mem_range_of_rel h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
⊢ Surjective ⇑f ∨ ∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b

Tactic:
apply or_iff_not_imp_right.2

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
⊢ (¬∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b) → Surjective ⇑f

Proof state:
case intro.inr.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∉ Set.range ⇑f
hs : s y x
⊢ ∃ a, f a = x

Tactic:
obtain ⟨z, rfl⟩ := IH y hs

Result:
case intro.inr.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
z : α
hy : f z ∉ Set.range ⇑f
hs : s (f z) x
⊢ ∃ a, f a = x

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
⊢ ∀ (x : β), (∀ (y : β), s y x → ∃ a, f a = y) → ∃ a, f a = x

Tactic:
intro x IH

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
⊢ ∃ a, f a = x

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
⊢ (¬∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b) → Surjective ⇑f

Tactic:
intro h b

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b
b : β
⊢ ∃ a, f a = b

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b
b : β
⊢ ∃ a, f a = b

Tactic:
push_neg at h

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
⊢ ∃ a, f a = b

Proof state:
case intro.inl.intro.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h✝ : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
h : s x y
⊢ ∃ a, f a = x

Tactic:
obtain ⟨z, rfl⟩ := hy

Result:
case intro.inl.intro.inr.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h✝ : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
z : α
hs : ¬s (f z) x
h : s x (f z)
⊢ ∃ a, f a = x