internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Theorem_5_3_1
Proof state before:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = b
h4 : (b, a2) ∈ inv (graph f)
⊢ a1 = a2
Tactic:
define at h4
Proof state after:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = b
h4 : f a2 = b
⊢ a1 = a2
Theorem: HTPI.Theorem_5_3_1
Proof state before:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = b
h4 : f a2 = b
⊢ a1 = a2
Tactic:
rewrite [←h4] at h3
Proof state after:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = f a2
h4 : f a2 = b
⊢ a1 = a2
Theorem: HTPI.Theorem_5_3_1
Proof state before:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = f a2
h4 : f a2 = b
⊢ a1 = a2
Tactic:
define at h1
Proof state after:
case Uniqueness
A B : Type
f : A → B
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = f a2
h4 : f a2 = b
⊢ a1 = a2
Theorem: HTPI.Theorem_5_3_1
Proof state before:
case Uniqueness
A B : Type
f : A → B
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = f a2
h4 : f a2 = b
⊢ a1 = a2
Tactic:
show a1 = a2 from h1 a1 a2 h3
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_2_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
⊢ g ∘ f = id
Tactic:
apply funext
Proof state after:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
⊢ ∀ (x : A), (g ∘ f) x = id x
Theorem: HTPI.Theorem_5_3_2_1
Proof state before:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
⊢ ∀ (x : A), (g ∘ f) x = id x
Tactic:
fix a : A
Proof state after:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ (g ∘ f) a = id a
Theorem: HTPI.Theorem_5_3_2_1
Proof state before:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ (g ∘ f) a = id a
Tactic:
have h2 : (f a, a) ∈ graph g := by
  rewrite [h1]         define               rfl
  done
Proof state after:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
h2 : (f a, a) ∈ graph g
⊢ (g ∘ f) a = id a
Theorem: HTPI.Theorem_5_3_2_1
Proof state before:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
h2 : (f a, a) ∈ graph g
⊢ (g ∘ f) a = id a
Tactic:
define at h2
Proof state after:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
h2 : g (f a) = a
⊢ (g ∘ f) a = id a
Theorem: HTPI.Theorem_5_3_2_1
Proof state before:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
h2 : g (f a) = a
⊢ (g ∘ f) a = id a
Tactic:
show (g ∘ f) a = id a from h2
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_2_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ (f a, a) ∈ graph g
Tactic:
rewrite [h1]
Proof state after:
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ (f a, a) ∈ inv (graph f)
Theorem: HTPI.Theorem_5_3_2_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ (f a, a) ∈ inv (graph f)
Tactic:
define
Proof state after:
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ f a = f a
Theorem: HTPI.Theorem_5_3_2_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ f a = f a
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_3_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
⊢ one_to_one f
Tactic:
define
Proof state after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
⊢ ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
Theorem: HTPI.Theorem_5_3_3_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
⊢ ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
Tactic:
fix a1 : A
Proof state after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 : A
⊢ ∀ (x2 : A), f a1 = f x2 → a1 = x2
Theorem: HTPI.Theorem_5_3_3_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 : A
⊢ ∀ (x2 : A), f a1 = f x2 → a1 = x2
Tactic:
fix a2 : A
Proof state after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
⊢ f a1 = f a2 → a1 = a2
Theorem: HTPI.Theorem_5_3_3_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
⊢ f a1 = f a2 → a1 = a2
Tactic:
assume h2 : f a1 = f a2
Proof state after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ a1 = a2
Theorem: HTPI.Theorem_5_3_3_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ a1 = a2
Tactic:
show a1 = a2 from
  calc a1
    _ = id a1 := by rfl
    _ = (g ∘ f) a1 := by rw [h1]
    _ = g (f a1) := by rfl
    _ = g (f a2) := by rw [h2]
    _ = (g ∘ f) a2 := by rfl
    _ = id a2 := by rw [h1]
    _ = a2 := by rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_3_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ a1 = id a1
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_3_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ id a1 = (g ∘ f) a1
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_3_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ (g ∘ f) a1 = g (f a1)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_3_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ g (f a1) = g (f a2)
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_3_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ g (f a2) = (g ∘ f) a2
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_3_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ (g ∘ f) a2 = id a2
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_3_1
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ id a2 = a2
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_5
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
⊢ graph g = inv (graph f)
Tactic:
have h3 : one_to_one f := Theorem_5_3_3_1 f g h1
Proof state after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
⊢ graph g = inv (graph f)
Theorem: HTPI.Theorem_5_3_5
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
⊢ graph g = inv (graph f)
Tactic:
have h4 : onto f := Theorem_5_3_3_2 f g h2
Proof state after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
⊢ graph g = inv (graph f)
Theorem: HTPI.Theorem_5_3_5
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
⊢ graph g = inv (graph f)
Tactic:
obtain (g' : B → A) (h5 : graph g' = inv (graph f))
  from Theorem_5_3_1 f h3 h4
Proof state after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
⊢ graph g = inv (graph f)
Theorem: HTPI.Theorem_5_3_5
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
⊢ graph g = inv (graph f)
Tactic:
have h6 : g' ∘ f = id := Theorem_5_3_2_1 f g' h5
Proof state after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ graph g = inv (graph f)
Theorem: HTPI.Theorem_5_3_5
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ graph g = inv (graph f)
Tactic:
have h7 : g = g' :=
  calc g
    _ = id ∘ g := by rfl
    _ = (g' ∘ f) ∘ g := by rw [h6]
    _ = g' ∘ (f ∘ g) := by rfl
    _ = g' ∘ id := by rw [h2]
    _ = g' := by rfl
Proof state after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
h7 : g = g'
⊢ graph g = inv (graph f)
Theorem: HTPI.Theorem_5_3_5
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
h7 : g = g'
⊢ graph g = inv (graph f)
Tactic:
rewrite [←h7] at h5
Proof state after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g = inv (graph f)
h6 : g' ∘ f = id
h7 : g = g'
⊢ graph g = inv (graph f)
Theorem: HTPI.Theorem_5_3_5
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g = inv (graph f)
h6 : g' ∘ f = id
h7 : g = g'
⊢ graph g = inv (graph f)
Tactic:
show graph g = inv (graph f) from h5
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_5
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ g = id ∘ g
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_5
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ id ∘ g = (g' ∘ f) ∘ g
Tactic:
rw [h6]
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_5
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ (g' ∘ f) ∘ g = g' ∘ f ∘ g
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_5
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ g' ∘ f ∘ g = g' ∘ id
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_5
Proof state before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ g' ∘ id = g'
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_5_4_5
Proof 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}
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof 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
Theorem: HTPI.Theorem_5_4_5
Proof 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
Proof state after:
no goals
Theorem: HTPI.image_def
Proof state before:
A B : Type
f : A → B
X : Set A
b : B
⊢ b ∈ image f X ↔ ∃ x ∈ X, f x = b
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.inverse_image_def
Proof state before:
A B : Type
f : A → B
Y : Set B
a : A
⊢ a ∈ inverse_image f Y ↔ f a ∈ Y
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_5_5_2_1
Proof state before:
A B : Type
f : A → B
W X : Set A
⊢ image f (W ∩ X) ⊆ image f W ∩ image f X
Tactic:
fix y : B
Proof state after:
A B : Type
f : A → B
W X : Set A
y : B
⊢ y ∈ image f (W ∩ X) → y ∈ image f W ∩ image f X
Theorem: HTPI.Theorem_5_5_2_1
Proof state before:
A B : Type
f : A → B
W X : Set A
y : B
⊢ y ∈ image f (W ∩ X) → y ∈ image f W ∩ image f X
Tactic:
assume h1 : y ∈ image f (W ∩ X)
Proof state after:
A B : Type
f : A → B
W X : Set A
y : B
h1 : y ∈ image f (W ∩ X)
⊢ y ∈ image f W ∩ image f X
Theorem: HTPI.Theorem_5_5_2_1
Proof state before:
A B : Type
f : A → B
W X : Set A
y : B
h1 : y ∈ image f (W ∩ X)
⊢ y ∈ image f W ∩ image f X
Tactic:
define at h1
Proof state after:
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
⊢ y ∈ image f W ∩ image f X
Theorem: HTPI.Theorem_5_5_2_1
Proof state before:
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
⊢ y ∈ image f W ∩ image f X
Tactic:
obtain (x : A) (h2 : x ∈ W ∩ X ∧ f x = y) from h1
Proof state after:
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : x ∈ W ∩ X ∧ f x = y
⊢ y ∈ image f W ∩ image f X