Theorem: normalizes_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) → ∀ (x : A), normalizes R x → P x
Tactic:
intros P IH x norm
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
x : A
norm : normalizes R x
⊢ 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
x : A
norm : normalizes R x
⊢ P x
Tactic:
apply Classical.byContradiction
State after:
case h
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
x : A
norm : normalizes R x
⊢ ¬P x → False

State before:
case h
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
x : A
norm : normalizes R x
⊢ ¬P x → False
Tactic:
intro h
State after:
case h
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
x : A
norm : normalizes R x
h : ¬P x
⊢ False

State before:
case h
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
x : A
norm : normalizes R x
h : ¬P x
⊢ False
Tactic:
apply norm
State after:
case h
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
x : A
norm : normalizes R x
h : ¬P x
⊢ diverge_from R x

State before:
case h
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
x : A
norm : normalizes R x
h : ¬P x
⊢ diverge_from R x
Tactic:
have h' : ∃ f : ℕ → A, f 0 = x ∧ ∀ n, ¬ P (f n) ∧ f n ~> f (n+1) :=
by
  apply (dependent_choice''  (λ a ↦ ¬ P a))
  . exact h
  . intros a npa
    apply Classical.byContradiction
    simp; intros p
    apply npa
    apply IH; intros y ry
    apply Classical.byContradiction; intros npy
    apply (p y npy ry)
State after:
case h
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
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
⊢ diverge_from R x

State before:
case h
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
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
⊢ diverge_from R x
Tactic:
rw [diverge_from]
State after:
case h
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
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
⊢ ∃ xs, xs 0 = x ∧ ∀ (n : ℕ), R (xs n) (xs (n + 1))

State before:
case h
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
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
⊢ ∃ xs, xs 0 = x ∧ ∀ (n : ℕ), R (xs n) (xs (n + 1))
Tactic:
match h' with
  | Exists.intro xs ⟨P0, P1⟩ =>
    exists xs; aesop
State after:
no goals

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
x : A
norm : normalizes R x
h : ¬P x
⊢ ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
Tactic:
apply (dependent_choice''  (λ a ↦ ¬ P a))
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
x : A
norm : normalizes R x
h : ¬P x
⊢ ¬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
x : A
norm : normalizes R x
h : ¬P x
⊢ ∀ (a : A), ¬P a → ∃ b, ¬P b ∧ R a b

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
x : A
norm : normalizes R x
h : ¬P x
⊢ ¬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
x : A
norm : normalizes R x
h : ¬P x
⊢ ∀ (a : A), ¬P a → ∃ b, ¬P b ∧ R a b
Tactic:
. exact h
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
x : A
norm : normalizes R x
h : ¬P x
⊢ ∀ (a : A), ¬P a → ∃ b, ¬P b ∧ R a b

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
x : A
norm : normalizes R x
h : ¬P x
⊢ ∀ (a : A), ¬P a → ∃ b, ¬P b ∧ R a b
Tactic:
. intros a npa
  apply Classical.byContradiction
  simp; intros p
  apply npa
  apply IH; intros y ry
  apply Classical.byContradiction; intros npy
  apply (p y npy ry)
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
x : A
norm : normalizes R x
h : ¬P x
⊢ ¬P x
Tactic:
exact h
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
x : A
norm : normalizes R x
h : ¬P x
⊢ ∀ (a : A), ¬P a → ∃ b, ¬P b ∧ R a b
Tactic:
intros a npa
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
⊢ ∃ b, ¬P b ∧ R a b

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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
⊢ ∃ b, ¬P b ∧ R a b
Tactic:
apply Classical.byContradiction
State after:
case a.h
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
⊢ (¬∃ b, ¬P b ∧ R a b) → False

State before:
case a.h
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
⊢ (¬∃ b, ¬P b ∧ R a b) → False
Tactic:
simp
State after:
case a.h
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
⊢ (∀ (x : A), ¬P x → ¬R a x) → False

State before:
case a.h
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
⊢ (∀ (x : A), ¬P x → ¬R a x) → False
Tactic:
intros p
State after:
case a.h
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ False

State before:
case a.h
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ False
Tactic:
apply npa
State after:
case a.h
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ P a

State before:
case a.h
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ P a
Tactic:
apply IH
State after:
case a.h.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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ ∀ (y : A), R a y → P y

State before:
case a.h.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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ ∀ (y : A), R a y → P y
Tactic:
intros y ry
State after:
case a.h.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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
y : A
ry : R a y
⊢ P y

State before:
case a.h.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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
y : A
ry : R a y
⊢ P y
Tactic:
apply Classical.byContradiction
State after:
case a.h.a.h
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
y : A
ry : R a y
⊢ ¬P y → False

State before:
case a.h.a.h
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
y : A
ry : R a y
⊢ ¬P y → False
Tactic:
intros npy
State after:
case a.h.a.h
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
y : A
ry : R a y
npy : ¬P y
⊢ False

State before:
case a.h.a.h
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
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
y : A
ry : R a y
npy : ¬P y
⊢ False
Tactic:
apply (p y npy ry)
State after:
no goals

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
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
xs : ℕ → A
P0 : xs 0 = x
P1 : ∀ (n : ℕ), ¬P (xs n) ∧ R (xs n) (xs (n + 1))
⊢ ∃ xs, xs 0 = x ∧ ∀ (n : ℕ), R (xs n) (xs (n + 1))
Tactic:
exists xs
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
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
xs : ℕ → A
P0 : xs 0 = x
P1 : ∀ (n : ℕ), ¬P (xs n) ∧ R (xs n) (xs (n + 1))
⊢ xs 0 = x ∧ ∀ (n : ℕ), R (xs n) (xs (n + 1))

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
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
xs : ℕ → A
P0 : xs 0 = x
P1 : ∀ (n : ℕ), ¬P (xs n) ∧ R (xs n) (xs (n + 1))
⊢ xs 0 = x ∧ ∀ (n : ℕ), R (xs n) (xs (n + 1))
Tactic:
aesop
State after:
no goals