internlm/Lean-Github huggingface dataset:
Theorem: HTPI.func_from_graph_rtl
Proof state before:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ F
⊢ (x, y) ∈ graph f
Tactic:
define
Proof state after:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ F
⊢ f x = y
Theorem: HTPI.func_from_graph_rtl
Proof state before:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ F
⊢ f x = y
Tactic:
obtain (z : B) (h5 : (x, z) ∈ F)
  (h6 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x
Proof state after:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ F
z : B
h5 : (x, z) ∈ F
h6 : ∀ (y_1 y_2 : B), (x, y_1) ∈ F → (x, y_2) ∈ F → y_1 = y_2
⊢ f x = y
Theorem: HTPI.func_from_graph_rtl
Proof state before:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ F
z : B
h5 : (x, z) ∈ F
h6 : ∀ (y_1 y_2 : B), (x, y_1) ∈ F → (x, y_2) ∈ F → y_1 = y_2
⊢ f x = y
Tactic:
show f x = y from h6 (f x) y h3 h4
Proof state after:
no goals
Theorem: HTPI.Theorem_5_1_5
Proof state before:
A B C : Type
f : A → B
g : B → C
⊢ ∃ h, graph h = comp (graph g) (graph f)
Tactic:
set h : A → C := fun (x : A) => g (f x)
Proof state after:
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
⊢ ∃ h, graph h = comp (graph g) (graph f)
Theorem: HTPI.Theorem_5_1_5
Proof state before:
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
⊢ ∃ h, graph h = comp (graph g) (graph f)
Tactic:
apply Exists.intro h
Proof state after:
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
⊢ graph h = comp (graph g) (graph f)
Theorem: HTPI.Theorem_5_1_5
Proof state before:
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
⊢ graph h = comp (graph g) (graph f)
Tactic:
apply Set.ext
Proof state after:
case h
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
⊢ ∀ (x : A × C), x ∈ graph h ↔ x ∈ comp (graph g) (graph f)
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
⊢ ∀ (x : A × C), x ∈ graph h ↔ x ∈ comp (graph g) (graph f)
Tactic:
fix (a, c) : A × C
Proof state after:
case h
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
⊢ (a, c) ∈ graph h ↔ (a, c) ∈ comp (graph g) (graph f)
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
⊢ (a, c) ∈ graph h ↔ (a, c) ∈ comp (graph g) (graph f)
Tactic:
apply Iff.intro
Proof state after:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
⊢ (a, c) ∈ graph h → (a, c) ∈ comp (graph g) (graph f)

case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
⊢ (a, c) ∈ comp (graph g) (graph f) → (a, c) ∈ graph h
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
⊢ (a, c) ∈ graph h → (a, c) ∈ comp (graph g) (graph f)
Tactic:
assume h1 : (a, c) ∈ graph h
Proof state after:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : (a, c) ∈ graph h
⊢ (a, c) ∈ comp (graph g) (graph f)
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : (a, c) ∈ graph h
⊢ (a, c) ∈ comp (graph g) (graph f)
Tactic:
define at h1
Proof state after:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (a, c) ∈ comp (graph g) (graph f)
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (a, c) ∈ comp (graph g) (graph f)
Tactic:
define
Proof state after:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
Tactic:
apply Exists.intro (f a)
Proof state after:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (a, f a) ∈ graph f ∧ (f a, c) ∈ graph g
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (a, f a) ∈ graph f ∧ (f a, c) ∈ graph g
Tactic:
apply And.intro
Proof state after:
case h.mp.left
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (a, f a) ∈ graph f

case h.mp.right
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (f a, c) ∈ graph g
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mp.left
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (a, f a) ∈ graph f
Tactic:
define
Proof state after:
case h.mp.left
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ f a = f a
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mp.left
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ f a = f a
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mp.right
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (f a, c) ∈ graph g
Tactic:
define
Proof state after:
case h.mp.right
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ g (f a) = c
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mp.right
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ g (f a) = c
Tactic:
show g (f a) = c from h1
Proof state after:
no goals
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
⊢ (a, c) ∈ comp (graph g) (graph f) → (a, c) ∈ graph h
Tactic:
assume h1 : (a, c) ∈ comp (graph g) (graph f)
Proof state after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : (a, c) ∈ comp (graph g) (graph f)
⊢ (a, c) ∈ graph h
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : (a, c) ∈ comp (graph g) (graph f)
⊢ (a, c) ∈ graph h
Tactic:
define
Proof state after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : (a, c) ∈ comp (graph g) (graph f)
⊢ h a = c
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : (a, c) ∈ comp (graph g) (graph f)
⊢ h a = c
Tactic:
define at h1
Proof state after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
⊢ h a = c
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
⊢ h a = c
Tactic:
obtain (b : B) (h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g) from h1
Proof state after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
⊢ h a = c
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
⊢ h a = c
Tactic:
have h3 : (a, b) ∈ graph f := h2.left
Proof state after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : (a, b) ∈ graph f
⊢ h a = c
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : (a, b) ∈ graph f
⊢ h a = c
Tactic:
have h4 : (b, c) ∈ graph g := h2.right
Proof state after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : (a, b) ∈ graph f
h4 : (b, c) ∈ graph g
⊢ h a = c
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : (a, b) ∈ graph f
h4 : (b, c) ∈ graph g
⊢ h a = c
Tactic:
define at h3
Proof state after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : f a = b
h4 : (b, c) ∈ graph g
⊢ h a = c
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : f a = b
h4 : (b, c) ∈ graph g
⊢ h a = c
Tactic:
define at h4
Proof state after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : f a = b
h4 : g b = c
⊢ h a = c
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : f a = b
h4 : g b = c
⊢ h a = c
Tactic:
rewrite [←h3] at h4
Proof state after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : f a = b
h4 : g (f a) = c
⊢ h a = c
Theorem: HTPI.Theorem_5_1_5
Proof state before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : f a = b
h4 : g (f a) = c
⊢ h a = c
Tactic:
show h a = c from h4
Proof state after:
no goals
Theorem: HTPI.Theorem_5_2_5_1
Proof state before:
A B C : Type
f : A → B
g : B → C
⊢ one_to_one f → one_to_one g → one_to_one (g ∘ f)
Tactic:
assume h1 : one_to_one f
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : one_to_one f
⊢ one_to_one g → one_to_one (g ∘ f)
Theorem: HTPI.Theorem_5_2_5_1
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : one_to_one f
⊢ one_to_one g → one_to_one (g ∘ f)
Tactic:
assume h2 : one_to_one g
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : one_to_one f
h2 : one_to_one g
⊢ one_to_one (g ∘ f)
Theorem: HTPI.Theorem_5_2_5_1
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : one_to_one f
h2 : one_to_one g
⊢ one_to_one (g ∘ f)
Tactic:
define at h1
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : one_to_one g
⊢ one_to_one (g ∘ f)
Theorem: HTPI.Theorem_5_2_5_1
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : one_to_one g
⊢ one_to_one (g ∘ f)
Tactic:
define at h2
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
⊢ one_to_one (g ∘ f)
Theorem: HTPI.Theorem_5_2_5_1
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
⊢ one_to_one (g ∘ f)
Tactic:
define
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
⊢ ∀ (x1 x2 : A), (g ∘ f) x1 = (g ∘ f) x2 → x1 = x2
Theorem: HTPI.Theorem_5_2_5_1
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
⊢ ∀ (x1 x2 : A), (g ∘ f) x1 = (g ∘ f) x2 → x1 = x2
Tactic:
fix a1 : A
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 : A
⊢ ∀ (x2 : A), (g ∘ f) a1 = (g ∘ f) x2 → a1 = x2
Theorem: HTPI.Theorem_5_2_5_1
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 : A
⊢ ∀ (x2 : A), (g ∘ f) a1 = (g ∘ f) x2 → a1 = x2
Tactic:
fix a2 : A
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
⊢ (g ∘ f) a1 = (g ∘ f) a2 → a1 = a2
Theorem: HTPI.Theorem_5_2_5_1
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
⊢ (g ∘ f) a1 = (g ∘ f) a2 → a1 = a2
Tactic:
define : (g ∘ f) a1
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
⊢ g (f a1) = (g ∘ f) a2 → a1 = a2
Theorem: HTPI.Theorem_5_2_5_1
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
⊢ g (f a1) = (g ∘ f) a2 → a1 = a2
Tactic:
define : (g ∘ f) a2
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
⊢ g (f a1) = g (f a2) → a1 = a2
Theorem: HTPI.Theorem_5_2_5_1
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
⊢ g (f a1) = g (f a2) → a1 = a2
Tactic:
assume h3 : g (f a1) = g (f a2)
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
h3 : g (f a1) = g (f a2)
⊢ a1 = a2
Theorem: HTPI.Theorem_5_2_5_1
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
h3 : g (f a1) = g (f a2)
⊢ a1 = a2
Tactic:
have h4 : f a1 = f a2 := h2 (f a1) (f a2) h3
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
h3 : g (f a1) = g (f a2)
h4 : f a1 = f a2
⊢ a1 = a2
Theorem: HTPI.Theorem_5_2_5_1
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
h3 : g (f a1) = g (f a2)
h4 : f a1 = f a2
⊢ a1 = a2
Tactic:
show a1 = a2 from h1 a1 a2 h4
Proof state after:
no goals
Theorem: HTPI.comp_def
Proof state before:
A B C : Type
g : B → C
f : A → B
x : A
⊢ (g ∘ f) x = g (f x)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_5_2_5_2
Proof state before:
A B C : Type
f : A → B
g : B → C
⊢ onto f → onto g → onto (g ∘ f)
Tactic:
assume h1 : onto f
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : onto f
⊢ onto g → onto (g ∘ f)
Theorem: HTPI.Theorem_5_2_5_2
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : onto f
⊢ onto g → onto (g ∘ f)
Tactic:
assume h2 : onto g
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : onto f
h2 : onto g
⊢ onto (g ∘ f)
Theorem: HTPI.Theorem_5_2_5_2
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : onto f
h2 : onto g
⊢ onto (g ∘ f)
Tactic:
define at h1
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : onto g
⊢ onto (g ∘ f)
Theorem: HTPI.Theorem_5_2_5_2
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : onto g
⊢ onto (g ∘ f)
Tactic:
define at h2
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
⊢ onto (g ∘ f)
Theorem: HTPI.Theorem_5_2_5_2
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
⊢ onto (g ∘ f)
Tactic:
define
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
⊢ ∀ (y : C), ∃ x, (g ∘ f) x = y
Theorem: HTPI.Theorem_5_2_5_2
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
⊢ ∀ (y : C), ∃ x, (g ∘ f) x = y
Tactic:
fix c : C
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
⊢ ∃ x, (g ∘ f) x = c
Theorem: HTPI.Theorem_5_2_5_2
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
⊢ ∃ x, (g ∘ f) x = c
Tactic:
obtain (b : B) (h3 : g b = c) from h2 c
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
⊢ ∃ x, (g ∘ f) x = c
Theorem: HTPI.Theorem_5_2_5_2
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
⊢ ∃ x, (g ∘ f) x = c
Tactic:
obtain (a : A) (h4 : f a = b) from h1 b
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
a : A
h4 : f a = b
⊢ ∃ x, (g ∘ f) x = c
Theorem: HTPI.Theorem_5_2_5_2
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
a : A
h4 : f a = b
⊢ ∃ x, (g ∘ f) x = c
Tactic:
apply Exists.intro a
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
a : A
h4 : f a = b
⊢ (g ∘ f) a = c
Theorem: HTPI.Theorem_5_2_5_2
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
a : A
h4 : f a = b
⊢ (g ∘ f) a = c
Tactic:
rewrite [comp_def]
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
a : A
h4 : f a = b
⊢ g (f a) = c
Theorem: HTPI.Theorem_5_2_5_2
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
a : A
h4 : f a = b
⊢ g (f a) = c
Tactic:
rewrite [←h4] at h3
Proof state after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
a : A
h3 : g (f a) = c
h4 : f a = b
⊢ g (f a) = c
Theorem: HTPI.Theorem_5_2_5_2
Proof state before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
a : A
h3 : g (f a) = c
h4 : f a = b
⊢ g (f a) = c
Tactic:
show g (f a) = c from h3
Proof state after:
no goals
Theorem: HTPI.Theorem_5_3_1
Proof state before:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
⊢ ∃ g, graph g = inv (graph f)
Tactic:
rewrite [func_from_graph]
Proof state after:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
⊢ is_func_graph (inv (graph f))
Theorem: HTPI.Theorem_5_3_1
Proof state before:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
⊢ is_func_graph (inv (graph f))
Tactic:
define
Proof state after:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
⊢ ∀ (x : B), ∃! y, (x, y) ∈ inv (graph f)
Theorem: HTPI.Theorem_5_3_1
Proof state before:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
⊢ ∀ (x : B), ∃! y, (x, y) ∈ inv (graph f)
Tactic:
fix b : B
Proof state after:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
⊢ ∃! y, (b, y) ∈ inv (graph f)
Theorem: HTPI.Theorem_5_3_1
Proof state before:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
⊢ ∃! y, (b, y) ∈ inv (graph f)
Tactic:
exists_unique
Proof state after:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
⊢ ∃ y, (b, y) ∈ inv (graph f)

case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
⊢ ∀ (y_1 y_2 : A), (b, y_1) ∈ inv (graph f) → (b, y_2) ∈ inv (graph f) → y_1 = y_2
Theorem: HTPI.Theorem_5_3_1
Proof state before:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
⊢ ∃ y, (b, y) ∈ inv (graph f)
Tactic:
define at h2
Proof state after:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
⊢ ∃ y, (b, y) ∈ inv (graph f)
Theorem: HTPI.Theorem_5_3_1
Proof state before:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
⊢ ∃ y, (b, y) ∈ inv (graph f)
Tactic:
obtain (a : A) (h4 : f a = b) from h2 b
Proof state after:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
a : A
h4 : f a = b
⊢ ∃ y, (b, y) ∈ inv (graph f)
Theorem: HTPI.Theorem_5_3_1
Proof state before:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
a : A
h4 : f a = b
⊢ ∃ y, (b, y) ∈ inv (graph f)
Tactic:
apply Exists.intro a
Proof state after:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
a : A
h4 : f a = b
⊢ (b, a) ∈ inv (graph f)
Theorem: HTPI.Theorem_5_3_1
Proof state before:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
a : A
h4 : f a = b
⊢ (b, a) ∈ inv (graph f)
Tactic:
define
Proof state after:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
a : A
h4 : f a = b
⊢ f a = b
Theorem: HTPI.Theorem_5_3_1
Proof state before:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
a : A
h4 : f a = b
⊢ f a = b
Tactic:
show f a = b from h4
Proof state after:
no goals
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
⊢ ∀ (y_1 y_2 : A), (b, y_1) ∈ inv (graph f) → (b, y_2) ∈ inv (graph f) → y_1 = y_2
Tactic:
fix a1 : A
Proof state after:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 : A
⊢ ∀ (y_2 : A), (b, a1) ∈ inv (graph f) → (b, y_2) ∈ inv (graph f) → a1 = y_2
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 : A
⊢ ∀ (y_2 : A), (b, a1) ∈ inv (graph f) → (b, y_2) ∈ inv (graph f) → a1 = y_2
Tactic:
fix a2 : A
Proof state after:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
⊢ (b, a1) ∈ inv (graph f) → (b, a2) ∈ inv (graph f) → 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
⊢ (b, a1) ∈ inv (graph f) → (b, a2) ∈ inv (graph f) → a1 = a2
Tactic:
assume h3 : (b, a1) ∈ inv (graph f)
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 : (b, a1) ∈ inv (graph f)
⊢ (b, a2) ∈ inv (graph f) → 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 : (b, a1) ∈ inv (graph f)
⊢ (b, a2) ∈ inv (graph f) → a1 = a2
Tactic:
assume h4 : (b, a2) ∈ inv (graph f)
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 : (b, a1) ∈ inv (graph f)
h4 : (b, a2) ∈ inv (graph f)
⊢ 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 : (b, a1) ∈ inv (graph f)
h4 : (b, a2) ∈ inv (graph f)
⊢ a1 = a2
Tactic:
define 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 = b
h4 : (b, a2) ∈ inv (graph f)
⊢ a1 = a2