Theorem: HTPI.Theorem_5_4_5 (HTPILib/Chap5.lean)

State before:
A : Type
f : A → A
B : Set A
⊢ ∃ C, closure f B C
Tactic:
set F : Set (Set A) := {D : Set A | B ⊆ D ∧ closed f D}
State after:
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
⊢ ∃ C, closure f B C

State before:
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
⊢ ∃ C, closure f B C
Tactic:
set C : Set A := ⋂₀ F
State after:
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
⊢ ∃ C, closure f B C

State before:
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
⊢ ∃ C, closure f B C
Tactic:
apply Exists.intro C
State after:
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
⊢ closure f B C

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

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

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

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

State before:
case left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
⊢ B ⊆ C ∧ closed f C
Tactic:
apply And.intro
State after:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
⊢ B ⊆ C

case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
⊢ closed f C

State before:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
⊢ B ⊆ C
Tactic:
fix a : A
State after:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
⊢ a ∈ B → a ∈ C

State before:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
⊢ a ∈ B → a ∈ C
Tactic:
assume h1 : a ∈ B
State after:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ B
⊢ a ∈ C

State before:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ B
⊢ a ∈ C
Tactic:
define
State after:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ B
⊢ ∀ t ∈ F, a ∈ t

State before:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ B
⊢ ∀ t ∈ F, a ∈ t
Tactic:
fix D : Set A
State after:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ B
D : Set A
⊢ D ∈ F → a ∈ D

State before:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ B
D : Set A
⊢ D ∈ F → a ∈ D
Tactic:
assume h2 : D ∈ F
State after:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ B
D : Set A
h2 : D ∈ F
⊢ a ∈ D

State before:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ B
D : Set A
h2 : D ∈ F
⊢ a ∈ D
Tactic:
define at h2
State after:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ B
D : Set A
h2 : B ⊆ D ∧ closed f D
⊢ a ∈ D

State before:
case left.left
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ B
D : Set A
h2 : B ⊆ D ∧ closed f D
⊢ a ∈ D
Tactic:
show a ∈ D from h2.left h1
State after:
no goals

State before:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
⊢ closed f C
Tactic:
define
State after:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
⊢ ∀ x ∈ C, f x ∈ C

State before:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
⊢ ∀ x ∈ C, f x ∈ C
Tactic:
fix a : A
State after:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
⊢ a ∈ C → f a ∈ C

State before:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
⊢ a ∈ C → f a ∈ C
Tactic:
assume h1 : a ∈ C
State after:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ C
⊢ f a ∈ C

State before:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ C
⊢ f a ∈ C
Tactic:
define
State after:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ C
⊢ ∀ t ∈ F, f a ∈ t

State before:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ C
⊢ ∀ t ∈ F, f a ∈ t
Tactic:
fix D : Set A
State after:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ C
D : Set A
⊢ D ∈ F → f a ∈ D

State before:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ C
D : Set A
⊢ D ∈ F → f a ∈ D
Tactic:
assume h2 : D ∈ F
State after:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ C
D : Set A
h2 : D ∈ F
⊢ f a ∈ D

State before:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : a ∈ C
D : Set A
h2 : D ∈ F
⊢ f a ∈ D
Tactic:
define at h1
State after:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : ∀ t ∈ F, a ∈ t
D : Set A
h2 : D ∈ F
⊢ f a ∈ D

State before:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : ∀ t ∈ F, a ∈ t
D : Set A
h2 : D ∈ F
⊢ f a ∈ D
Tactic:
have h3 : a ∈ D := h1 D h2
State after:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : ∀ t ∈ F, a ∈ t
D : Set A
h2 : D ∈ F
h3 : a ∈ D
⊢ f a ∈ D

State before:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : ∀ t ∈ F, a ∈ t
D : Set A
h2 : D ∈ F
h3 : a ∈ D
⊢ f a ∈ D
Tactic:
define at h2
State after:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : ∀ t ∈ F, a ∈ t
D : Set A
h2 : B ⊆ D ∧ closed f D
h3 : a ∈ D
⊢ f a ∈ D

State before:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : ∀ t ∈ F, a ∈ t
D : Set A
h2 : B ⊆ D ∧ closed f D
h3 : a ∈ D
⊢ f a ∈ D
Tactic:
have h4 : closed f D := h2.right
State after:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : ∀ t ∈ F, a ∈ t
D : Set A
h2 : B ⊆ D ∧ closed f D
h3 : a ∈ D
h4 : closed f D
⊢ f a ∈ D

State before:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : ∀ t ∈ F, a ∈ t
D : Set A
h2 : B ⊆ D ∧ closed f D
h3 : a ∈ D
h4 : closed f D
⊢ f a ∈ D
Tactic:
define at h4
State after:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : ∀ t ∈ F, a ∈ t
D : Set A
h2 : B ⊆ D ∧ closed f D
h3 : a ∈ D
h4 : ∀ x ∈ D, f x ∈ D
⊢ f a ∈ D

State before:
case left.right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
a : A
h1 : ∀ t ∈ F, a ∈ t
D : Set A
h2 : B ⊆ D ∧ closed f D
h3 : a ∈ D
h4 : ∀ x ∈ D, f x ∈ D
⊢ f a ∈ D
Tactic:
show f a ∈ D from h4 a h3
State after:
no goals

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

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

State before:
case right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
D : Set A
h1 : D ∈ F
⊢ sub A C D
Tactic:
define
State after:
case right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
D : Set A
h1 : D ∈ F
⊢ ∀ ⦃a : A⦄, a ∈ C → a ∈ D

State before:
case right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
D : Set A
h1 : D ∈ F
⊢ ∀ ⦃a : A⦄, a ∈ C → a ∈ D
Tactic:
fix a : A
State after:
case right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
D : Set A
h1 : D ∈ F
a : A
⊢ a ∈ C → a ∈ D

State before:
case right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
D : Set A
h1 : D ∈ F
a : A
⊢ a ∈ C → a ∈ D
Tactic:
assume h2 : a ∈ C
State after:
case right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
D : Set A
h1 : D ∈ F
a : A
h2 : a ∈ C
⊢ a ∈ D

State before:
case right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
D : Set A
h1 : D ∈ F
a : A
h2 : a ∈ C
⊢ a ∈ D
Tactic:
define at h2
State after:
case right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
D : Set A
h1 : D ∈ F
a : A
h2 : ∀ t ∈ F, a ∈ t
⊢ a ∈ D

State before:
case right
A : Type
f : A → A
B : Set A
F : Set (Set A) := {D | B ⊆ D ∧ closed f D}
C : Set A := ⋂₀ F
D : Set A
h1 : D ∈ F
a : A
h2 : ∀ t ∈ F, a ∈ t
⊢ a ∈ D
Tactic:
show a ∈ D from h2 D h1
State after:
no goals