Theorem: normal_normalizing (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ normal R x → normalizes R x
Tactic:
simp [normal]
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ (∀ (x_1 : A), ¬R x x_1) → normalizes R x

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ (∀ (x_1 : A), ¬R x x_1) → normalizes R x
Tactic:
intros norm_x div_x
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
⊢ False

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
⊢ False
Tactic:
match div_x with
  | Exists.intro xs (And.intro zero_case incr_case) =>
  apply norm_x (xs 1)
  rw [←zero_case]
  apply incr_case
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
xs : ℕ → A
zero_case : xs 0 = x
incr_case : ∀ (n : ℕ), R (xs n) (xs (n + 1))
⊢ False
Tactic:
apply norm_x (xs 1)
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
xs : ℕ → A
zero_case : xs 0 = x
incr_case : ∀ (n : ℕ), R (xs n) (xs (n + 1))
⊢ R x (xs 1)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
xs : ℕ → A
zero_case : xs 0 = x
incr_case : ∀ (n : ℕ), R (xs n) (xs (n + 1))
⊢ R x (xs 1)
Tactic:
rw [←zero_case]
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
xs : ℕ → A
zero_case : xs 0 = x
incr_case : ∀ (n : ℕ), R (xs n) (xs (n + 1))
⊢ R (xs 0) (xs 1)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
xs : ℕ → A
zero_case : xs 0 = x
incr_case : ∀ (n : ℕ), R (xs n) (xs (n + 1))
⊢ R (xs 0) (xs 1)
Tactic:
apply incr_case
State after:
no goals