Theorem: normalizing_normal (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ normalizes R x → ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
apply normalizes_ind
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ ∀ (x : A),
    (∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1) → ∃ y, refl_trans_clos R x y ∧ normal R y

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ ∀ (x : A),
    (∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1) → ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
intros x h
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
by_cases (∃ y, x ~> y)
State after:
case pos
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y

case neg
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y

State before:
case pos
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y

case neg
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
. cases' h with y h'
  cases' h _ h' with z h''
  cases h''
  exists z
  constructor <;> aesop
State after:
case neg
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y

State before:
case neg
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
. exists x; constructor
  . constructor
  . apply h
State after:
no goals

State before:
case pos
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
cases' h with y h'
State after:
case pos.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
y : A
h' : R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y

State before:
case pos.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
y : A
h' : R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
cases' h _ h' with z h''
State after:
case pos.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
y : A
h' : R x y
z : A
h'' : refl_trans_clos R y z ∧ normal R z
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y

State before:
case pos.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
y : A
h' : R x y
z : A
h'' : refl_trans_clos R y z ∧ normal R z
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
cases h''
State after:
case pos.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
y : A
h' : R x y
z : A
left✝ : refl_trans_clos R y z
right✝ : normal R z
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y

State before:
case pos.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
y : A
h' : R x y
z : A
left✝ : refl_trans_clos R y z
right✝ : normal R z
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
exists z
State after:
case pos.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
y : A
h' : R x y
z : A
left✝ : refl_trans_clos R y z
right✝ : normal R z
⊢ refl_trans_clos R x z ∧ normal R z

State before:
case pos.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
y : A
h' : R x y
z : A
left✝ : refl_trans_clos R y z
right✝ : normal R z
⊢ refl_trans_clos R x z ∧ normal R z
Tactic:
constructor <;> aesop
State after:
no goals

State before:
case neg
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
exists x
State after:
case neg
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ refl_trans_clos R x x ∧ normal R x

State before:
case neg
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ refl_trans_clos R x x ∧ normal R x
Tactic:
constructor
State after:
case neg.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ refl_trans_clos R x x

case neg.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ normal R x

State before:
case neg.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ refl_trans_clos R x x

case neg.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ normal R x
Tactic:
. constructor
State after:
case neg.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ normal R x

State before:
case neg.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ normal R x
Tactic:
. apply h
State after:
no goals

State before:
case neg.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ refl_trans_clos R x x
Tactic:
constructor
State after:
no goals

State before:
case neg.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ normal R x
Tactic:
apply h
State after:
no goals