Theorem: normal_red (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
⊢ normal R x → refl_trans_clos R x y → x = y
Tactic:
intros norm red
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
norm : normal R x
red : refl_trans_clos R x y
⊢ x = y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
norm : normal R x
red : refl_trans_clos R x y
⊢ x = y
Tactic:
cases red
State after:
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm : normal R x
⊢ x = x

case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
norm : normal R x
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ y
⊢ x = y

State before:
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm : normal R x
⊢ x = x

case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
norm : normal R x
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ y
⊢ x = y
Tactic:
trivial
State after:
case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
norm : normal R x
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ y
⊢ x = y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
⊢ x = y✝
Tactic:
case step y _ _ =>
by_contra
apply norm; exists y
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
⊢ x = y✝
Tactic:
by_contra
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
x✝ : ¬x = y✝
⊢ False

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
x✝ : ¬x = y✝
⊢ False
Tactic:
apply norm
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
x✝ : ¬x = y✝
⊢ ∃ x', R x x'

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
x✝ : ¬x = y✝
⊢ ∃ x', R x x'
Tactic:
exists y
State after:
no goals