Theorem: HTPI.Theorem_6_5_1 (HTPILib/Chap6.lean)

State before:
A : Type
f : A → A
B : Set A
⊢ closure f B (cumul_image f B)
Tactic:
define
State after:
A : Type
f : A → A
B : Set A
⊢ cumul_image f B ∈ {D | B ⊆ D ∧ closed f D} ∧ ∀ x ∈ {D | B ⊆ D ∧ closed f D}, sub A (cumul_image f B) x

State before:
A : Type
f : A → A
B : Set A
⊢ cumul_image f B ∈ {D | B ⊆ D ∧ closed f D} ∧ ∀ x ∈ {D | B ⊆ D ∧ closed f D}, sub A (cumul_image f B) x
Tactic:
apply And.intro
State after:
case left
A : Type
f : A → A
B : Set A
⊢ cumul_image f B ∈ {D | B ⊆ D ∧ closed f D}

case right
A : Type
f : A → A
B : Set A
⊢ ∀ x ∈ {D | B ⊆ D ∧ closed f D}, sub A (cumul_image f B) x

State before:
case left
A : Type
f : A → A
B : Set A
⊢ cumul_image f B ∈ {D | B ⊆ D ∧ closed f D}
Tactic:
define
State after:
case left
A : Type
f : A → A
B : Set A
⊢ B ⊆ cumul_image f B ∧ closed f (cumul_image f B)

State before:
case left
A : Type
f : A → A
B : Set A
⊢ B ⊆ cumul_image f B ∧ closed f (cumul_image f B)
Tactic:
apply And.intro
State after:
case left.left
A : Type
f : A → A
B : Set A
⊢ B ⊆ cumul_image f B

case left.right
A : Type
f : A → A
B : Set A
⊢ closed f (cumul_image f B)

State before:
case left.left
A : Type
f : A → A
B : Set A
⊢ B ⊆ cumul_image f B
Tactic:
fix x : A
State after:
case left.left
A : Type
f : A → A
B : Set A
x : A
⊢ x ∈ B → x ∈ cumul_image f B

State before:
case left.left
A : Type
f : A → A
B : Set A
x : A
⊢ x ∈ B → x ∈ cumul_image f B
Tactic:
assume h1 : x ∈ B
State after:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ x ∈ cumul_image f B

State before:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ x ∈ cumul_image f B
Tactic:
define
State after:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ ∃ n, x ∈ rep_image f n B

State before:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ ∃ n, x ∈ rep_image f n B
Tactic:
apply Exists.intro 0
State after:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ x ∈ rep_image f 0 B

State before:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ x ∈ rep_image f 0 B
Tactic:
rewrite [rep_image_base]
State after:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ x ∈ B

State before:
case left.left
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ B
⊢ x ∈ B
Tactic:
show x ∈ B from h1
State after:
no goals

State before:
case left.right
A : Type
f : A → A
B : Set A
⊢ closed f (cumul_image f B)
Tactic:
define
State after:
case left.right
A : Type
f : A → A
B : Set A
⊢ ∀ x ∈ cumul_image f B, f x ∈ cumul_image f B

State before:
case left.right
A : Type
f : A → A
B : Set A
⊢ ∀ x ∈ cumul_image f B, f x ∈ cumul_image f B
Tactic:
fix x : A
State after:
case left.right
A : Type
f : A → A
B : Set A
x : A
⊢ x ∈ cumul_image f B → f x ∈ cumul_image f B

State before:
case left.right
A : Type
f : A → A
B : Set A
x : A
⊢ x ∈ cumul_image f B → f x ∈ cumul_image f B
Tactic:
assume h1 : x ∈ cumul_image f B
State after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ cumul_image f B
⊢ f x ∈ cumul_image f B

State before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : x ∈ cumul_image f B
⊢ f x ∈ cumul_image f B
Tactic:
define at h1
State after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
⊢ f x ∈ cumul_image f B

State before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
⊢ f x ∈ cumul_image f B
Tactic:
obtain (m : Nat) (h2 : x ∈ rep_image f m B) from h1
State after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x ∈ cumul_image f B

State before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x ∈ cumul_image f B
Tactic:
define
State after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ ∃ n, f x ∈ rep_image f n B

State before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ ∃ n, f x ∈ rep_image f n B
Tactic:
apply Exists.intro (m + 1)
State after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x ∈ rep_image f (m + 1) B

State before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x ∈ rep_image f (m + 1) B
Tactic:
rewrite [rep_image_step]
State after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x ∈ image f (rep_image f m B)

State before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x ∈ image f (rep_image f m B)
Tactic:
define
State after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ ∃ x_1 ∈ rep_image f m B, f x_1 = f x

State before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ ∃ x_1 ∈ rep_image f m B, f x_1 = f x
Tactic:
apply Exists.intro x
State after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ x ∈ rep_image f m B ∧ f x = f x

State before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ x ∈ rep_image f m B ∧ f x = f x
Tactic:
apply And.intro h2
State after:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x = f x

State before:
case left.right
A : Type
f : A → A
B : Set A
x : A
h1 : ∃ n, x ∈ rep_image f n B
m : ℕ
h2 : x ∈ rep_image f m B
⊢ f x = f x
Tactic:
rfl
State after:
no goals

State before:
case right
A : Type
f : A → A
B : Set A
⊢ ∀ x ∈ {D | B ⊆ D ∧ closed f D}, sub A (cumul_image f B) x
Tactic:
fix D : Set A
State after:
case right
A : Type
f : A → A
B D : Set A
⊢ D ∈ {D | B ⊆ D ∧ closed f D} → sub A (cumul_image f B) D

State before:
case right
A : Type
f : A → A
B D : Set A
⊢ D ∈ {D | B ⊆ D ∧ closed f D} → sub A (cumul_image f B) D
Tactic:
assume h1 : D ∈ {D : Set A | B ⊆ D ∧ closed f D}
State after:
case right
A : Type
f : A → A
B D : Set A
h1 : D ∈ {D | B ⊆ D ∧ closed f D}
⊢ sub A (cumul_image f B) D

State before:
case right
A : Type
f : A → A
B D : Set A
h1 : D ∈ {D | B ⊆ D ∧ closed f D}
⊢ sub A (cumul_image f B) D
Tactic:
define at h1
State after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
⊢ sub A (cumul_image f B) D

State before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
⊢ sub A (cumul_image f B) D
Tactic:
define
State after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
⊢ ∀ ⦃a : A⦄, a ∈ cumul_image f B → a ∈ D

State before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
⊢ ∀ ⦃a : A⦄, a ∈ cumul_image f B → a ∈ D
Tactic:
fix x : A
State after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
⊢ x ∈ cumul_image f B → x ∈ D

State before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
⊢ x ∈ cumul_image f B → x ∈ D
Tactic:
assume h2 : x ∈ cumul_image f B
State after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : x ∈ cumul_image f B
⊢ x ∈ D

State before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : x ∈ cumul_image f B
⊢ x ∈ D
Tactic:
define at h2
State after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : ∃ n, x ∈ rep_image f n B
⊢ x ∈ D

State before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : ∃ n, x ∈ rep_image f n B
⊢ x ∈ D
Tactic:
obtain (m : Nat) (h3 : x ∈ rep_image f m B) from h2
State after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : ∃ n, x ∈ rep_image f n B
m : ℕ
h3 : x ∈ rep_image f m B
⊢ x ∈ D

State before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : ∃ n, x ∈ rep_image f n B
m : ℕ
h3 : x ∈ rep_image f m B
⊢ x ∈ D
Tactic:
have h4 : rep_image f m B ⊆ D :=
  rep_image_sub_closed h1.left h1.right m
State after:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : ∃ n, x ∈ rep_image f n B
m : ℕ
h3 : x ∈ rep_image f m B
h4 : rep_image f m B ⊆ D
⊢ x ∈ D

State before:
case right
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D ∧ closed f D
x : A
h2 : ∃ n, x ∈ rep_image f n B
m : ℕ
h3 : x ∈ rep_image f m B
h4 : rep_image f m B ⊆ D
⊢ x ∈ D
Tactic:
show x ∈ D from h4 h3
State after:
no goals