Theorem: normalizing_ind (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → normalizing R → ∀ (x : A), P x
Tactic:
intros P IH norm x
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ P x

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ P x
Tactic:
apply normalizes_ind
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ ∀ (x : A), (∀ (y : A), ?R x y → P y) → P x

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ normalizes ?R x

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ A → A → Prop

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ ∀ (x : A), (∀ (y : A), ?R x y → P y) → P x

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ normalizes ?R x

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ A → A → Prop
Tactic:
. apply IH
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ normalizes (fun x y => R x y) x

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ normalizes (fun x y => R x y) x
Tactic:
. apply norm
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ ∀ (x : A), (∀ (y : A), ?R x y → P y) → P x
Tactic:
apply IH
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ normalizes (fun x y => R x y) x
Tactic:
apply norm
State after:
no goals