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

State before:
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ ∀ (n : ℕ), rep_image f n B ⊆ D
Tactic:
by_induc
State after:
case Base_Case
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ rep_image f 0 B ⊆ D

case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ ∀ (n : ℕ), rep_image f n B ⊆ D → rep_image f (n + 1) B ⊆ D

State before:
case Base_Case
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ rep_image f 0 B ⊆ D
Tactic:
rewrite [rep_image_base]
State after:
case Base_Case
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ B ⊆ D

State before:
case Base_Case
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ B ⊆ D
Tactic:
show B ⊆ D from h1
State after:
no goals

State before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
⊢ ∀ (n : ℕ), rep_image f n B ⊆ D → rep_image f (n + 1) B ⊆ D
Tactic:
fix n : Nat
State after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
⊢ rep_image f n B ⊆ D → rep_image f (n + 1) B ⊆ D

State before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
⊢ rep_image f n B ⊆ D → rep_image f (n + 1) B ⊆ D
Tactic:
assume ih : rep_image f n B ⊆ D
State after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
⊢ rep_image f (n + 1) B ⊆ D

State before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
⊢ rep_image f (n + 1) B ⊆ D
Tactic:
fix x : A
State after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
⊢ x ∈ rep_image f (n + 1) B → x ∈ D

State before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
⊢ x ∈ rep_image f (n + 1) B → x ∈ D
Tactic:
assume h3 : x ∈ rep_image f (n + 1) B
State after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : x ∈ rep_image f (n + 1) B
⊢ x ∈ D

State before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : x ∈ rep_image f (n + 1) B
⊢ x ∈ D
Tactic:
rewrite [rep_image_step] at h3
State after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : x ∈ image f (rep_image f n B)
⊢ x ∈ D

State before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : x ∈ image f (rep_image f n B)
⊢ x ∈ D
Tactic:
define at h3
State after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
⊢ x ∈ D

State before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
⊢ x ∈ D
Tactic:
obtain (b : A) (h4 : b ∈ rep_image f n B ∧ f b = x) from h3
State after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
⊢ x ∈ D

State before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
⊢ x ∈ D
Tactic:
rewrite [←h4.right]
State after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
⊢ f b ∈ D

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

State before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : closed f D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
h5 : b ∈ D
⊢ f b ∈ D
Tactic:
define at h2
State after:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : ∀ x ∈ D, f x ∈ D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
h5 : b ∈ D
⊢ f b ∈ D

State before:
case Induction_Step
A : Type
f : A → A
B D : Set A
h1 : B ⊆ D
h2 : ∀ x ∈ D, f x ∈ D
n : ℕ
ih : rep_image f n B ⊆ D
x : A
h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
b : A
h4 : b ∈ rep_image f n B ∧ f b = x
h5 : b ∈ D
⊢ f b ∈ D
Tactic:
show f b ∈ D from h2 b h5
State after:
no goals