Theorem: not_acc_iff (Logic/Vorspiel/Order.lean)

State before:
α : Sort u
r : α → α → Prop
x : α
⊢ ¬Acc r x → ∃ y, r y x ∧ ¬Acc r y
Tactic:
contrapose
State after:
α : Sort u
r : α → α → Prop
x : α
⊢ (¬∃ y, r y x ∧ ¬Acc r y) → ¬¬Acc r x

State before:
α : Sort u
r : α → α → Prop
x : α
⊢ (¬∃ y, r y x ∧ ¬Acc r y) → ¬¬Acc r x
Tactic:
simp
State after:
α : Sort u
r : α → α → Prop
x : α
⊢ (∀ (x_1 : α), r x_1 x → Acc r x_1) → Acc r x

State before:
α : Sort u
r : α → α → Prop
x : α
⊢ (∀ (x_1 : α), r x_1 x → Acc r x_1) → Acc r x
Tactic:
exact Acc.intro x
State after:
no goals

State before:
α : Sort u
r : α → α → Prop
x : α
⊢ (∃ y, r y x ∧ ¬Acc r y) → ¬Acc r x
Tactic:
contrapose
State after:
α : Sort u
r : α → α → Prop
x : α
⊢ ¬¬Acc r x → ¬∃ y, r y x ∧ ¬Acc r y

State before:
α : Sort u
r : α → α → Prop
x : α
⊢ ¬¬Acc r x → ¬∃ y, r y x ∧ ¬Acc r y
Tactic:
simp
State after:
α : Sort u
r : α → α → Prop
x : α
⊢ Acc r x → ∀ (x_1 : α), r x_1 x → Acc r x_1

State before:
α : Sort u
r : α → α → Prop
x : α
⊢ Acc r x → ∀ (x_1 : α), r x_1 x → Acc r x_1
Tactic:
rintro ⟨h⟩
State after:
case intro
α : Sort u
r : α → α → Prop
x : α
h✝ : ∀ (y : α), r y x → Acc r y
⊢ ∀ (x_1 : α), r x_1 x → Acc r x_1

State before:
case intro
α : Sort u
r : α → α → Prop
x : α
h✝ : ∀ (y : α), r y x → Acc r y
⊢ ∀ (x_1 : α), r x_1 x → Acc r x_1
Tactic:
assumption
State after:
no goals