internlm/Lean-Github huggingface dataset:
Theorem: HTPI.remove_one_match
Proof state before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ ∀ ⦃x : U⦄ ⦃y : V⦄, remove_one R u v x y → x ∈ A \ {u} ∧ y ∈ B \ {v}
Tactic:
fix x : U
Proof state after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
x : U
⊢ ∀ ⦃y : V⦄, remove_one R u v x y → x ∈ A \ {u} ∧ y ∈ B \ {v}
Theorem: HTPI.remove_one_match
Proof state before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
x : U
⊢ ∀ ⦃y : V⦄, remove_one R u v x y → x ∈ A \ {u} ∧ y ∈ B \ {v}
Tactic:
fix y : V
Proof state after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
x : U
y : V
⊢ remove_one R u v x y → x ∈ A \ {u} ∧ y ∈ B \ {v}
Theorem: HTPI.remove_one_match
Proof state before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
x : U
y : V
⊢ remove_one R u v x y → x ∈ A \ {u} ∧ y ∈ B \ {v}
Tactic:
assume h4 : remove_one R u v x y
Proof state after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
x : U
y : V
h4 : remove_one R u v x y
⊢ x ∈ A \ {u} ∧ y ∈ B \ {v}
Theorem: HTPI.remove_one_match
Proof state before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
x : U
y : V
h4 : remove_one R u v x y
⊢ x ∈ A \ {u} ∧ y ∈ B \ {v}
Tactic:
show x ∈ A \ {u} ∧ y ∈ B \ {v} from remove_one_rel_within h1 h4
Proof state after:
no goals
Theorem: HTPI.remove_one_match
Proof state before:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ fcnl_on (remove_one R u v) (A \ {u}) ∧ fcnl_on (invRel (remove_one R u v)) (B \ {v})
Tactic:
apply And.intro (remove_one_fcnl h1 h2 v)
Proof state after:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ fcnl_on (invRel (remove_one R u v)) (B \ {v})
Theorem: HTPI.remove_one_match
Proof state before:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ fcnl_on (invRel (remove_one R u v)) (B \ {v})
Tactic:
rewrite [remove_one_inv]
Proof state after:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ fcnl_on (remove_one (invRel R) v u) (B \ {v})
Theorem: HTPI.remove_one_match
Proof state before:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ fcnl_on (remove_one (invRel R) v u) (B \ {v})
Tactic:
show fcnl_on (remove_one (invRel R) v u) (B \ {v}) from
  remove_one_fcnl (inv_match h1) h3 u
Proof state after:
no goals
Theorem: HTPI.remove_one_equinum
Proof state before:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
⊢ A \ {u} ∼ B \ {v}
Tactic:
define
Proof state after:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
⊢ ∃ R, matching R (A \ {u}) (B \ {v})
Theorem: HTPI.remove_one_equinum
Proof state before:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
⊢ ∃ R, matching R (A \ {u}) (B \ {v})
Tactic:
obtain (R : Rel U V) (h4 : matching R A B) from h1
Proof state after:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
R : Rel U V
h4 : matching R A B
⊢ ∃ R, matching R (A \ {u}) (B \ {v})
Theorem: HTPI.remove_one_equinum
Proof state before:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
R : Rel U V
h4 : matching R A B
⊢ ∃ R, matching R (A \ {u}) (B \ {v})
Tactic:
apply Exists.intro (remove_one R u v)
Proof state after:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
R : Rel U V
h4 : matching R A B
⊢ matching (remove_one R u v) (A \ {u}) (B \ {v})
Theorem: HTPI.remove_one_equinum
Proof state before:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
R : Rel U V
h4 : matching R A B
⊢ matching (remove_one R u v) (A \ {u}) (B \ {v})
Tactic:
show matching (remove_one R u v) (A \ {u}) (B \ {v}) from
  remove_one_match h4 h2 h3
Proof state after:
no goals
Theorem: HTPI.I_max
Proof state before:
n : ℕ
⊢ n ∈ I (n + 1)
Tactic:
define
Proof state after:
n : ℕ
⊢ n < n + 1
Theorem: HTPI.I_max
Proof state before:
n : ℕ
⊢ n < n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.I_diff
Proof state before:
n : ℕ
⊢ I (n + 1) \ {n} = I n
Tactic:
apply Set.ext
Proof state after:
case h
n : ℕ
⊢ ∀ (x : ℕ), x ∈ I (n + 1) \ {n} ↔ x ∈ I n
Theorem: HTPI.I_diff
Proof state before:
case h
n : ℕ
⊢ ∀ (x : ℕ), x ∈ I (n + 1) \ {n} ↔ x ∈ I n
Tactic:
fix x : Nat
Proof state after:
case h
n x : ℕ
⊢ x ∈ I (n + 1) \ {n} ↔ x ∈ I n
Theorem: HTPI.I_diff
Proof state before:
case h
n x : ℕ
⊢ x ∈ I (n + 1) \ {n} ↔ x ∈ I n
Tactic:
apply Iff.intro
Proof state after:
case h.mp
n x : ℕ
⊢ x ∈ I (n + 1) \ {n} → x ∈ I n

case h.mpr
n x : ℕ
⊢ x ∈ I n → x ∈ I (n + 1) \ {n}
Theorem: HTPI.I_diff
Proof state before:
case h.mp
n x : ℕ
⊢ x ∈ I (n + 1) \ {n} → x ∈ I n
Tactic:
assume h1 : x ∈ I (n + 1) \ {n}
Proof state after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) \ {n}
⊢ x ∈ I n
Theorem: HTPI.I_diff
Proof state before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) \ {n}
⊢ x ∈ I n
Tactic:
define
Proof state after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) \ {n}
⊢ x < n
Theorem: HTPI.I_diff
Proof state before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) \ {n}
⊢ x < n
Tactic:
define at h1
Proof state after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
⊢ x < n
Theorem: HTPI.I_diff
Proof state before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
⊢ x < n
Tactic:
have h2 : x ∈ I (n + 1) := h1.left
Proof state after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x ∈ I (n + 1)
⊢ x < n
Theorem: HTPI.I_diff
Proof state before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x ∈ I (n + 1)
⊢ x < n
Tactic:
have h3 : ¬x ∈ {n} := h1.right
Proof state after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x ∈ I (n + 1)
h3 : x ∉ {n}
⊢ x < n
Theorem: HTPI.I_diff
Proof state before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x ∈ I (n + 1)
h3 : x ∉ {n}
⊢ x < n
Tactic:
define at h2
Proof state after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x < n + 1
h3 : x ∉ {n}
⊢ x < n
Theorem: HTPI.I_diff
Proof state before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x < n + 1
h3 : x ∉ {n}
⊢ x < n
Tactic:
define at h3
Proof state after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x < n + 1
h3 : ¬x = n
⊢ x < n
Theorem: HTPI.I_diff
Proof state before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x < n + 1
h3 : ¬x = n
⊢ x < n
Tactic:
have h4 : x ≤ n := Nat.le_of_lt_succ h2
Proof state after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x < n + 1
h3 : ¬x = n
h4 : x ≤ n
⊢ x < n
Theorem: HTPI.I_diff
Proof state before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x < n + 1
h3 : ¬x = n
h4 : x ≤ n
⊢ x < n
Tactic:
show x < n from Nat.lt_of_le_of_ne h4 h3
Proof state after:
no goals
Theorem: HTPI.I_diff
Proof state before:
case h.mpr
n x : ℕ
⊢ x ∈ I n → x ∈ I (n + 1) \ {n}
Tactic:
assume h1 : x ∈ I n
Proof state after:
case h.mpr
n x : ℕ
h1 : x ∈ I n
⊢ x ∈ I (n + 1) \ {n}
Theorem: HTPI.I_diff
Proof state before:
case h.mpr
n x : ℕ
h1 : x ∈ I n
⊢ x ∈ I (n + 1) \ {n}
Tactic:
define at h1
Proof state after:
case h.mpr
n x : ℕ
h1 : x < n
⊢ x ∈ I (n + 1) \ {n}
Theorem: HTPI.I_diff
Proof state before:
case h.mpr
n x : ℕ
h1 : x < n
⊢ x ∈ I (n + 1) \ {n}
Tactic:
define
Proof state after:
case h.mpr
n x : ℕ
h1 : x < n
⊢ x ∈ I (n + 1) ∧ x ∉ {n}
Theorem: HTPI.I_diff
Proof state before:
case h.mpr
n x : ℕ
h1 : x < n
⊢ x ∈ I (n + 1) ∧ x ∉ {n}
Tactic:
apply And.intro
Proof state after:
case h.mpr.left
n x : ℕ
h1 : x < n
⊢ x ∈ I (n + 1)

case h.mpr.right
n x : ℕ
h1 : x < n
⊢ x ∉ {n}
Theorem: HTPI.I_diff
Proof state before:
case h.mpr.left
n x : ℕ
h1 : x < n
⊢ x ∈ I (n + 1)
Tactic:
define
Proof state after:
case h.mpr.left
n x : ℕ
h1 : x < n
⊢ x < n + 1
Theorem: HTPI.I_diff
Proof state before:
case h.mpr.left
n x : ℕ
h1 : x < n
⊢ x < n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.I_diff
Proof state before:
case h.mpr.right
n x : ℕ
h1 : x < n
⊢ x ∉ {n}
Tactic:
by_contra h2
Proof state after:
case h.mpr.right
n x : ℕ
h1 : x < n
h2 : x ∈ {n}
⊢ False
Theorem: HTPI.I_diff
Proof state before:
case h.mpr.right
n x : ℕ
h1 : x < n
h2 : x ∈ {n}
⊢ False
Tactic:
define at h2
Proof state after:
case h.mpr.right
n x : ℕ
h1 : x < n
h2 : x = n
⊢ False
Theorem: HTPI.I_diff
Proof state before:
case h.mpr.right
n x : ℕ
h1 : x < n
h2 : x = n
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.remove_one_numElts
Proof state before:
U : Type
A : Set U
n : ℕ
a : U
h1 : numElts A (n + 1)
h2 : a ∈ A
⊢ numElts (A \ {a}) n
Tactic:
have h3 : n ∈ I (n + 1) := I_max n
Proof state after:
U : Type
A : Set U
n : ℕ
a : U
h1 : numElts A (n + 1)
h2 : a ∈ A
h3 : n ∈ I (n + 1)
⊢ numElts (A \ {a}) n
Theorem: HTPI.remove_one_numElts
Proof state before:
U : Type
A : Set U
n : ℕ
a : U
h1 : numElts A (n + 1)
h2 : a ∈ A
h3 : n ∈ I (n + 1)
⊢ numElts (A \ {a}) n
Tactic:
rewrite [numElts_def] at h1
Proof state after:
U : Type
A : Set U
n : ℕ
a : U
h1 : I (n + 1) ∼ A
h2 : a ∈ A
h3 : n ∈ I (n + 1)
⊢ numElts (A \ {a}) n
Theorem: HTPI.remove_one_numElts
Proof state before:
U : Type
A : Set U
n : ℕ
a : U
h1 : I (n + 1) ∼ A
h2 : a ∈ A
h3 : n ∈ I (n + 1)
⊢ numElts (A \ {a}) n
Tactic:
have h4 : I (n + 1) \ {n} ∼ A \ {a} := remove_one_equinum h1 h3 h2
Proof state after:
U : Type
A : Set U
n : ℕ
a : U
h1 : I (n + 1) ∼ A
h2 : a ∈ A
h3 : n ∈ I (n + 1)
h4 : I (n + 1) \ {n} ∼ A \ {a}
⊢ numElts (A \ {a}) n
Theorem: HTPI.remove_one_numElts
Proof state before:
U : Type
A : Set U
n : ℕ
a : U
h1 : I (n + 1) ∼ A
h2 : a ∈ A
h3 : n ∈ I (n + 1)
h4 : I (n + 1) \ {n} ∼ A \ {a}
⊢ numElts (A \ {a}) n
Tactic:
rewrite [I_diff] at h4
Proof state after:
U : Type
A : Set U
n : ℕ
a : U
h1 : I (n + 1) ∼ A
h2 : a ∈ A
h3 : n ∈ I (n + 1)
h4 : I n ∼ A \ {a}
⊢ numElts (A \ {a}) n
Theorem: HTPI.remove_one_numElts
Proof state before:
U : Type
A : Set U
n : ℕ
a : U
h1 : I (n + 1) ∼ A
h2 : a ∈ A
h3 : n ∈ I (n + 1)
h4 : I n ∼ A \ {a}
⊢ numElts (A \ {a}) n
Tactic:
show numElts (A \ {a}) n from h4
Proof state after:
no goals
Theorem: HTPI.one_match_def
Proof state before:
U V : Type
a x : U
b y : V
⊢ one_match a b x y ↔ x = a ∧ y = b
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.I_1_singleton
Proof state before:
⊢ I 1 = {0}
Tactic:
apply Set.ext
Proof state after:
case h

⊢ ∀ (x : ℕ), x ∈ I 1 ↔ x ∈ {0}
Theorem: HTPI.I_1_singleton
Proof state before:
case h

⊢ ∀ (x : ℕ), x ∈ I 1 ↔ x ∈ {0}
Tactic:
fix x : Nat
Proof state after:
case h
x : ℕ
⊢ x ∈ I 1 ↔ x ∈ {0}
Theorem: HTPI.I_1_singleton
Proof state before:
case h
x : ℕ
⊢ x ∈ I 1 ↔ x ∈ {0}
Tactic:
apply Iff.intro
Proof state after:
case h.mp
x : ℕ
⊢ x ∈ I 1 → x ∈ {0}

case h.mpr
x : ℕ
⊢ x ∈ {0} → x ∈ I 1
Theorem: HTPI.I_1_singleton
Proof state before:
case h.mp
x : ℕ
⊢ x ∈ I 1 → x ∈ {0}
Tactic:
assume h1 : x ∈ I 1
Proof state after:
case h.mp
x : ℕ
h1 : x ∈ I 1
⊢ x ∈ {0}
Theorem: HTPI.I_1_singleton
Proof state before:
case h.mp
x : ℕ
h1 : x ∈ I 1
⊢ x ∈ {0}
Tactic:
rewrite [I_def] at h1
Proof state after:
case h.mp
x : ℕ
h1 : x < 1
⊢ x ∈ {0}
Theorem: HTPI.I_1_singleton
Proof state before:
case h.mp
x : ℕ
h1 : x < 1
⊢ x ∈ {0}
Tactic:
define
Proof state after:
case h.mp
x : ℕ
h1 : x < 1
⊢ x = 0
Theorem: HTPI.I_1_singleton
Proof state before:
case h.mp
x : ℕ
h1 : x < 1
⊢ x = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.I_1_singleton
Proof state before:
case h.mpr
x : ℕ
⊢ x ∈ {0} → x ∈ I 1
Tactic:
assume h1 : x ∈ {0}
Proof state after:
case h.mpr
x : ℕ
h1 : x ∈ {0}
⊢ x ∈ I 1
Theorem: HTPI.I_1_singleton
Proof state before:
case h.mpr
x : ℕ
h1 : x ∈ {0}
⊢ x ∈ I 1
Tactic:
define at h1
Proof state after:
case h.mpr
x : ℕ
h1 : x = 0
⊢ x ∈ I 1
Theorem: HTPI.I_1_singleton
Proof state before:
case h.mpr
x : ℕ
h1 : x = 0
⊢ x ∈ I 1
Tactic:
rewrite [h1, I_def]
Proof state after:
case h.mpr
x : ℕ
h1 : x = 0
⊢ 0 < 1
Theorem: HTPI.I_1_singleton
Proof state before:
case h.mpr
x : ℕ
h1 : x = 0
⊢ 0 < 1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.singleton_of_diff_empty
Proof state before:
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
⊢ A = {a}
Tactic:
apply Set.ext
Proof state after:
case h
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
⊢ ∀ (x : U), x ∈ A ↔ x ∈ {a}
Theorem: HTPI.singleton_of_diff_empty
Proof state before:
case h
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
⊢ ∀ (x : U), x ∈ A ↔ x ∈ {a}
Tactic:
fix x : U
Proof state after:
case h
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
⊢ x ∈ A ↔ x ∈ {a}
Theorem: HTPI.singleton_of_diff_empty
Proof state before:
case h
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
⊢ x ∈ A ↔ x ∈ {a}
Tactic:
apply Iff.intro
Proof state after:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
⊢ x ∈ A → x ∈ {a}

case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
⊢ x ∈ {a} → x ∈ A
Theorem: HTPI.singleton_of_diff_empty
Proof state before:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
⊢ x ∈ A → x ∈ {a}
Tactic:
assume h3 : x ∈ A
Proof state after:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
⊢ x ∈ {a}
Theorem: HTPI.singleton_of_diff_empty
Proof state before:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
⊢ x ∈ {a}
Tactic:
contradict h2 with h4
Proof state after:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
h4 : ¬x ∈ {a}
⊢ ∃ x, x ∈ A \ {a}
Theorem: HTPI.singleton_of_diff_empty
Proof state before:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
h4 : ¬x ∈ {a}
⊢ ∃ x, x ∈ A \ {a}
Tactic:
apply Exists.intro x
Proof state after:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
h4 : ¬x ∈ {a}
⊢ x ∈ A \ {a}
Theorem: HTPI.singleton_of_diff_empty
Proof state before:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
h4 : ¬x ∈ {a}
⊢ x ∈ A \ {a}
Tactic:
define
Proof state after:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
h4 : ¬x ∈ {a}
⊢ x ∈ A ∧ x ∉ {a}
Theorem: HTPI.singleton_of_diff_empty
Proof state before:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
h4 : ¬x ∈ {a}
⊢ x ∈ A ∧ x ∉ {a}
Tactic:
show x ∈ A ∧ ¬x ∈ {a} from And.intro h3 h4
Proof state after:
no goals
Theorem: HTPI.singleton_of_diff_empty
Proof state before:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
⊢ x ∈ {a} → x ∈ A
Tactic:
assume h3 : x ∈ {a}
Proof state after:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ {a}
⊢ x ∈ A
Theorem: HTPI.singleton_of_diff_empty
Proof state before:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ {a}
⊢ x ∈ A
Tactic:
define at h3
Proof state after:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x = a
⊢ x ∈ A
Theorem: HTPI.singleton_of_diff_empty
Proof state before:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x = a
⊢ x ∈ A
Tactic:
rewrite [h3]
Proof state after:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x = a
⊢ a ∈ A
Theorem: HTPI.singleton_of_diff_empty
Proof state before:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x = a
⊢ a ∈ A
Tactic:
show a ∈ A from h1
Proof state after:
no goals
Theorem: HTPI.singleton_one_elt
Proof state before:
U : Type
u : U
⊢ numElts {u} 1
Tactic:
define
Proof state after:
U : Type
u : U
⊢ ∃ R, matching R (I 1) {u}
Theorem: HTPI.singleton_one_elt
Proof state before:
U : Type
u : U
⊢ ∃ R, matching R (I 1) {u}
Tactic:
rewrite [I_1_singleton]
Proof state after:
U : Type
u : U
⊢ ∃ R, matching R {0} {u}
Theorem: HTPI.singleton_one_elt
Proof state before:
U : Type
u : U
⊢ ∃ R, matching R {0} {u}
Tactic:
show ∃ (R : Rel Nat U), matching R {0} {u} from
  Exists.intro (one_match 0 u) (one_match_match 0 u)
Proof state after:
no goals
Theorem: HTPI.one_elt_iff_singleton
Proof state before:
U : Type
A : Set U
⊢ numElts A 1 ↔ ∃ x, A = {x}
Tactic:
apply Iff.intro
Proof state after:
case mp
U : Type
A : Set U
⊢ numElts A 1 → ∃ x, A = {x}

case mpr
U : Type
A : Set U
⊢ (∃ x, A = {x}) → numElts A 1
Theorem: HTPI.one_elt_iff_singleton
Proof state before:
case mp
U : Type
A : Set U
⊢ numElts A 1 → ∃ x, A = {x}
Tactic:
assume h1 : numElts A 1
Proof state after:
case mp
U : Type
A : Set U
h1 : numElts A 1
⊢ ∃ x, A = {x}
Theorem: HTPI.one_elt_iff_singleton
Proof state before:
case mp
U : Type
A : Set U
h1 : numElts A 1
⊢ ∃ x, A = {x}
Tactic:
have h2 : 1 > 0 := by decide
Proof state after:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
⊢ ∃ x, A = {x}
Theorem: HTPI.one_elt_iff_singleton
Proof state before:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
⊢ ∃ x, A = {x}
Tactic:
obtain (x : U) (h3 : x ∈ A) from nonempty_of_pos_numElts h1 h2
Proof state after:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
x : U
h3 : x ∈ A
⊢ ∃ x, A = {x}
Theorem: HTPI.one_elt_iff_singleton
Proof state before:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
x : U
h3 : x ∈ A
⊢ ∃ x, A = {x}
Tactic:
have h4 : numElts (A \ {x}) 0 := remove_one_numElts h1 h3
Proof state after:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
x : U
h3 : x ∈ A
h4 : numElts (A \ {x}) 0
⊢ ∃ x, A = {x}
Theorem: HTPI.one_elt_iff_singleton
Proof state before:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
x : U
h3 : x ∈ A
h4 : numElts (A \ {x}) 0
⊢ ∃ x, A = {x}
Tactic:
rewrite [zero_elts_iff_empty] at h4
Proof state after:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
x : U
h3 : x ∈ A
h4 : empty (A \ {x})
⊢ ∃ x, A = {x}
Theorem: HTPI.one_elt_iff_singleton
Proof state before:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
x : U
h3 : x ∈ A
h4 : empty (A \ {x})
⊢ ∃ x, A = {x}
Tactic:
show ∃ (x : U), A = {x} from
  Exists.intro x (singleton_of_diff_empty h3 h4)
Proof state after:
no goals
Theorem: HTPI.one_elt_iff_singleton
Proof state before:
U : Type
A : Set U
h1 : numElts A 1
⊢ 1 > 0
Tactic:
decide
Proof state after:
no goals
Theorem: HTPI.one_elt_iff_singleton
Proof state before:
case mpr
U : Type
A : Set U
⊢ (∃ x, A = {x}) → numElts A 1
Tactic:
assume h1 : ∃ (x : U), A = {x}
Proof state after:
case mpr
U : Type
A : Set U
h1 : ∃ x, A = {x}
⊢ numElts A 1
Theorem: HTPI.one_elt_iff_singleton
Proof state before:
case mpr
U : Type
A : Set U
h1 : ∃ x, A = {x}
⊢ numElts A 1
Tactic:
obtain (x : U) (h2 : A = {x}) from h1
Proof state after:
case mpr
U : Type
A : Set U
h1 : ∃ x, A = {x}
x : U
h2 : A = {x}
⊢ numElts A 1
Theorem: HTPI.one_elt_iff_singleton
Proof state before:
case mpr
U : Type
A : Set U
h1 : ∃ x, A = {x}
x : U
h2 : A = {x}
⊢ numElts A 1
Tactic:
rewrite [h2]
Proof state after:
case mpr
U : Type
A : Set U
h1 : ∃ x, A = {x}
x : U
h2 : A = {x}
⊢ numElts {x} 1
Theorem: HTPI.one_elt_iff_singleton
Proof state before:
case mpr
U : Type
A : Set U
h1 : ∃ x, A = {x}
x : U
h2 : A = {x}
⊢ numElts {x} 1
Tactic:
show numElts {x} 1 from singleton_one_elt x
Proof state after:
no goals
Theorem: HTPI.Exercises.rep_image_family_base
Proof state before:
A : Type
F : Set (A → A)
B : Set A
⊢ rep_image_family F 0 B = B
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Exercises.rep_image_family_step
Proof state before:
A : Type
F : Set (A → A)
n : ℕ
B : Set A
⊢ rep_image_family F (n + 1) B = {x | ∃ f ∈ F, x ∈ image f (rep_image_family F n B)}
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Exercises.rep_image2_base
Proof state before:
A : Type
f : A → A → A
B : Set A
⊢ rep_image2 f 0 B = B
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Exercises.rep_image2_step
Proof state before:
A : Type
f : A → A → A
n : ℕ
B : Set A
⊢ rep_image2 f (n + 1) B = image2 f (rep_image2 f n B)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Exercises.rep_un_image2_base
Proof state before:
A : Type
f : A → A → A
B : Set A
⊢ rep_un_image2 f 0 B = B
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Exercises.rep_un_image2_step
Proof state before:
A : Type
f : A → A → A
n : ℕ
B : Set A
⊢ rep_un_image2 f (n + 1) B = un_image2 f (rep_un_image2 f n B)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_4_2_5_1
Proof state before:
A B : Type
R : Set (A × B)
⊢ inv (inv R) = R
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_4_2_5_2
Proof state before:
A B : Type
R : Set (A × B)
⊢ Dom (inv R) = Ran R
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_4_2_5_3
Proof state before:
A B : Type
R : Set (A × B)
⊢ Ran (inv R) = Dom R
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
⊢ comp T (comp S R) = comp (comp T S) R
Tactic:
apply Set.ext
Proof state after:
case h
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
⊢ ∀ (x : A × D), x ∈ comp T (comp S R) ↔ x ∈ comp (comp T S) R
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
⊢ ∀ (x : A × D), x ∈ comp T (comp S R) ↔ x ∈ comp (comp T S) R
Tactic:
fix (a, d) : A × D
Proof state after:
case h
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
⊢ (a, d) ∈ comp T (comp S R) ↔ (a, d) ∈ comp (comp T S) R
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
⊢ (a, d) ∈ comp T (comp S R) ↔ (a, d) ∈ comp (comp T S) R
Tactic:
apply Iff.intro
Proof state after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
⊢ (a, d) ∈ comp T (comp S R) → (a, d) ∈ comp (comp T S) R

case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
⊢ (a, d) ∈ comp (comp T S) R → (a, d) ∈ comp T (comp S R)
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
⊢ (a, d) ∈ comp T (comp S R) → (a, d) ∈ comp (comp T S) R
Tactic:
assume h1 : (a, d) ∈ comp T (comp S R)
Proof state after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp T (comp S R)
⊢ (a, d) ∈ comp (comp T S) R
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp T (comp S R)
⊢ (a, d) ∈ comp (comp T S) R
Tactic:
define
Proof state after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp T (comp S R)
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp T (comp S R)
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Tactic:
define at h1
Proof state after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Tactic:
obtain (c : C) (h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T) from h1
Proof state after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Theorem: HTPI.Theorem_4_2_5_4
Proof state before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Tactic:
have h3 : (a, c) ∈ comp S R := h2.left
Proof state after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : (a, c) ∈ comp S R
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S