Theorem: ind_normalizing (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) → ∀ (x : A), P x) → normalizing R
Tactic:
intros ih x
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x : A
⊢ normalizes R x

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x : A
⊢ normalizes R x
Tactic:
apply ih
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x : A
⊢ ∀ (x : A), (∀ (y : A), R x y → normalizes R y) → normalizes R x

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x : A
⊢ ∀ (x : A), (∀ (y : A), R x y → normalizes R y) → normalizes R x
Tactic:
intros x red_norm div
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
div : diverge_from R x
⊢ False

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
div : diverge_from R x
⊢ False
Tactic:
cases div
State after:
case a.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
w✝ : ℕ → A
h✝ : w✝ 0 = x ∧ ∀ (n : ℕ), R (w✝ n) (w✝ (n + 1))
⊢ False

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ False
Tactic:
case a.intro f h =>
  apply red_norm
  . simp [← h.1]
    apply h.2 0
  . exists (λ n ↦ f (n+1))
    simp
    intros n; apply h.2
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ False
Tactic:
apply red_norm
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ R x ?y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ diverge_from R ?y

case y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ A

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ R x ?y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ diverge_from R ?y

case y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ A
Tactic:
. simp [← h.1]
  apply h.2 0
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ diverge_from R (f (0 + 1))

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ diverge_from R (f (0 + 1))
Tactic:
. exists (λ n ↦ f (n+1))
  simp
  intros n; apply h.2
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ R x ?y
Tactic:
simp [← h.1]
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ R (f 0) ?y

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ R (f 0) ?y
Tactic:
apply h.2 0
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ diverge_from R (f (0 + 1))
Tactic:
exists (λ n ↦ f (n+1))
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ (fun n => f (n + 1)) 0 = f (0 + 1) ∧ ∀ (n : ℕ), R ((fun n => f (n + 1)) n) ((fun n => f (n + 1)) (n + 1))

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ (fun n => f (n + 1)) 0 = f (0 + 1) ∧ ∀ (n : ℕ), R ((fun n => f (n + 1)) n) ((fun n => f (n + 1)) (n + 1))
Tactic:
simp
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ ∀ (n : ℕ), R (f (n + 1)) (f (n + 1 + 1))

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ ∀ (n : ℕ), R (f (n + 1)) (f (n + 1 + 1))
Tactic:
intros n
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
n : ℕ
⊢ R (f (n + 1)) (f (n + 1 + 1))

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
n : ℕ
⊢ R (f (n + 1)) (f (n + 1 + 1))
Tactic:
apply h.2
State after:
no goals