internlm/Lean-Github huggingface dataset:
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mpr
U : Type
A : Set U
⊢ empty A → numElts A 0
Tactic:
assume h1 : empty A
Proof state after:
case mpr
U : Type
A : Set U
h1 : empty A
⊢ numElts A 0
Theorem: HTPI.zero_elts_iff_empty
Proof state before:
case mpr
U : Type
A : Set U
h1 : empty A
⊢ numElts A 0
Tactic:
show ∃ (R : Rel Nat U), matching R (I 0) A from
  Exists.intro (emptyRel Nat U) (empty_match I_0_empty h1)
Proof state after:
no goals
Theorem: HTPI.nonempty_of_pos_numElts
Proof state before:
U : Type
A : Set U
n : ℕ
h1 : numElts A n
h2 : n > 0
⊢ ∃ x, x ∈ A
Tactic:
define at h1
Proof state after:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
⊢ ∃ x, x ∈ A
Theorem: HTPI.nonempty_of_pos_numElts
Proof state before:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
⊢ ∃ x, x ∈ A
Tactic:
obtain (R : Rel Nat U) (h3 : matching R (I n) A) from h1
Proof state after:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : matching R (I n) A
⊢ ∃ x, x ∈ A
Theorem: HTPI.nonempty_of_pos_numElts
Proof state before:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : matching R (I n) A
⊢ ∃ x, x ∈ A
Tactic:
define at h3
Proof state after:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
⊢ ∃ x, x ∈ A
Theorem: HTPI.nonempty_of_pos_numElts
Proof state before:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
⊢ ∃ x, x ∈ A
Tactic:
have h4 : 0 ∈ I n := h2
Proof state after:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
h4 : 0 ∈ I n
⊢ ∃ x, x ∈ A
Theorem: HTPI.nonempty_of_pos_numElts
Proof state before:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
h4 : 0 ∈ I n
⊢ ∃ x, x ∈ A
Tactic:
obtain (x : U) (h5 : R 0 x) from fcnl_exists h3.right.left h4
Proof state after:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
h4 : 0 ∈ I n
x : U
h5 : R 0 x
⊢ ∃ x, x ∈ A
Theorem: HTPI.nonempty_of_pos_numElts
Proof state before:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
h4 : 0 ∈ I n
x : U
h5 : R 0 x
⊢ ∃ x, x ∈ A
Tactic:
have h6 : 0 ∈ I n ∧ x ∈ A := h3.left h5
Proof state after:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
h4 : 0 ∈ I n
x : U
h5 : R 0 x
h6 : 0 ∈ I n ∧ x ∈ A
⊢ ∃ x, x ∈ A
Theorem: HTPI.nonempty_of_pos_numElts
Proof state before:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
h4 : 0 ∈ I n
x : U
h5 : R 0 x
h6 : 0 ∈ I n ∧ x ∈ A
⊢ ∃ x, x ∈ A
Tactic:
show ∃ (x : U), x ∈ A from Exists.intro x h6.right
Proof state after:
no goals
Theorem: HTPI.relext
Proof state before:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
⊢ R = S
Tactic:
have h2 : extension R = extension S := by
  apply Set.ext
  fix (u, v) : U × V rewrite [ext_def, ext_def]  show R u v ↔ S u v from h u v
  done
Proof state after:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
h2 : extension R = extension S
⊢ R = S
Theorem: HTPI.relext
Proof state before:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
h2 : extension R = extension S
⊢ R = S
Tactic:
show R = S from
  calc R
    _ = RelFromExt (extension R) := by rfl
    _ = RelFromExt (extension S) := by rw [h2]
    _ = S := by rfl
Proof state after:
no goals
Theorem: HTPI.relext
Proof state before:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
⊢ extension R = extension S
Tactic:
apply Set.ext
Proof state after:
case h
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
⊢ ∀ (x : U × V), x ∈ extension R ↔ x ∈ extension S
Theorem: HTPI.relext
Proof state before:
case h
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
⊢ ∀ (x : U × V), x ∈ extension R ↔ x ∈ extension S
Tactic:
fix (u, v) : U × V
Proof state after:
case h
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
u : U
v : V
⊢ (u, v) ∈ extension R ↔ (u, v) ∈ extension S
Theorem: HTPI.relext
Proof state before:
case h
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
u : U
v : V
⊢ (u, v) ∈ extension R ↔ (u, v) ∈ extension S
Tactic:
rewrite [ext_def, ext_def]
Proof state after:
case h
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
u : U
v : V
⊢ R u v ↔ S u v
Theorem: HTPI.relext
Proof state before:
case h
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
u : U
v : V
⊢ R u v ↔ S u v
Tactic:
show R u v ↔ S u v from h u v
Proof state after:
no goals
Theorem: HTPI.relext
Proof state before:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
h2 : extension R = extension S
⊢ R = RelFromExt (extension R)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.relext
Proof state before:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
h2 : extension R = extension S
⊢ RelFromExt (extension R) = RelFromExt (extension S)
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: HTPI.relext
Proof state before:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
h2 : extension R = extension S
⊢ RelFromExt (extension S) = S
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.remove_one_def
Proof state before:
U V : Type
R : Rel U V
u x : U
v y : V
⊢ remove_one R u v x y ↔ x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.remove_one_rel_within
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : matching R A B
h2 : remove_one R u v x y
⊢ x ∈ A \ {u} ∧ y ∈ B \ {v}
Tactic:
define at h1
Proof state after:
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : remove_one R u v x y
⊢ x ∈ A \ {u} ∧ y ∈ B \ {v}
Theorem: HTPI.remove_one_rel_within
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : remove_one R u v x y
⊢ x ∈ A \ {u} ∧ y ∈ B \ {v}
Tactic:
define at h2
Proof state after:
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
⊢ x ∈ A \ {u} ∧ y ∈ B \ {v}
Theorem: HTPI.remove_one_rel_within
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : x ∈ A ∧ y ∈ B
⊢ x ∈ A \ {u} ∧ y ∈ B \ {v}
Tactic:
show x ∈ A \ {u} ∧ y ∈ B \ {v} from
  And.intro (And.intro h3.left h2.left) (And.intro h3.right h2.right.left)
Proof state after:
no goals
Theorem: HTPI.remove_one_rel_within
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
⊢ x ∈ A ∧ y ∈ B
Tactic:
by_cases on h2.right.right with h3
Proof state after:
case Case_1
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x y
⊢ x ∈ A ∧ y ∈ B

case Case_2
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x v ∧ R u y
⊢ x ∈ A ∧ y ∈ B
Theorem: HTPI.remove_one_rel_within
Proof state before:
case Case_1
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x y
⊢ x ∈ A ∧ y ∈ B
Tactic:
show x ∈ A ∧ y ∈ B from h1.left h3
Proof state after:
no goals
Theorem: HTPI.remove_one_rel_within
Proof state before:
case Case_2
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x v ∧ R u y
⊢ x ∈ A ∧ y ∈ B
Tactic:
have h4 : x ∈ A ∧ v ∈ B := h1.left h3.left
Proof state after:
case Case_2
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x v ∧ R u y
h4 : x ∈ A ∧ v ∈ B
⊢ x ∈ A ∧ y ∈ B
Theorem: HTPI.remove_one_rel_within
Proof state before:
case Case_2
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x v ∧ R u y
h4 : x ∈ A ∧ v ∈ B
⊢ x ∈ A ∧ y ∈ B
Tactic:
have h5 : u ∈ A ∧ y ∈ B := h1.left h3.right
Proof state after:
case Case_2
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x v ∧ R u y
h4 : x ∈ A ∧ v ∈ B
h5 : u ∈ A ∧ y ∈ B
⊢ x ∈ A ∧ y ∈ B
Theorem: HTPI.remove_one_rel_within
Proof state before:
case Case_2
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x v ∧ R u y
h4 : x ∈ A ∧ v ∈ B
h5 : u ∈ A ∧ y ∈ B
⊢ x ∈ A ∧ y ∈ B
Tactic:
show x ∈ A ∧ y ∈ B from And.intro h4.left h5.right
Proof state after:
no goals
Theorem: HTPI.remove_one_inv
Proof state before:
U V : Type
R : Rel U V
u : U
v : V
⊢ invRel (remove_one R u v) = remove_one (invRel R) v u
Tactic:
apply relext
Proof state after:
case h
U V : Type
R : Rel U V
u : U
v : V
⊢ ∀ (u_1 : V) (v_1 : U), invRel (remove_one R u v) u_1 v_1 ↔ remove_one (invRel R) v u u_1 v_1
Theorem: HTPI.remove_one_inv
Proof state before:
case h
U V : Type
R : Rel U V
u : U
v : V
⊢ ∀ (u_1 : V) (v_1 : U), invRel (remove_one R u v) u_1 v_1 ↔ remove_one (invRel R) v u u_1 v_1
Tactic:
fix y : V
Proof state after:
case h
U V : Type
R : Rel U V
u : U
v y : V
⊢ ∀ (v_1 : U), invRel (remove_one R u v) y v_1 ↔ remove_one (invRel R) v u y v_1
Theorem: HTPI.remove_one_inv
Proof state before:
case h
U V : Type
R : Rel U V
u : U
v y : V
⊢ ∀ (v_1 : U), invRel (remove_one R u v) y v_1 ↔ remove_one (invRel R) v u y v_1
Tactic:
fix x : U
Proof state after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ invRel (remove_one R u v) y x ↔ remove_one (invRel R) v u y x
Theorem: HTPI.remove_one_inv
Proof state before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ invRel (remove_one R u v) y x ↔ remove_one (invRel R) v u y x
Tactic:
rewrite [invRel_def, remove_one_def, remove_one_def]
Proof state after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y) ↔ y ≠ v ∧ x ≠ u ∧ (invRel R y x ∨ invRel R y u ∧ invRel R v x)
Theorem: HTPI.remove_one_inv
Proof state before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y) ↔ y ≠ v ∧ x ≠ u ∧ (invRel R y x ∨ invRel R y u ∧ invRel R v x)
Tactic:
rewrite [invRel_def, invRel_def, invRel_def]
Proof state after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y) ↔ y ≠ v ∧ x ≠ u ∧ (R x y ∨ R u y ∧ R x v)
Theorem: HTPI.remove_one_inv
Proof state before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y) ↔ y ≠ v ∧ x ≠ u ∧ (R x y ∨ R u y ∧ R x v)
Tactic:
rewrite [←and_assoc, ←and_assoc]
Proof state after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
Theorem: HTPI.remove_one_inv
Proof state before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
Tactic:
have h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u := and_comm
Proof state after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u
⊢ (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
Theorem: HTPI.remove_one_inv
Proof state before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u
⊢ (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
Tactic:
have h2 : R x v ∧ R u y ↔ R u y ∧ R x v := and_comm
Proof state after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u
h2 : R x v ∧ R u y ↔ R u y ∧ R x v
⊢ (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
Theorem: HTPI.remove_one_inv
Proof state before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u
h2 : R x v ∧ R u y ↔ R u y ∧ R x v
⊢ (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
Tactic:
rewrite [h1, h2]
Proof state after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u
h2 : R x v ∧ R u y ↔ R u y ∧ R x v
⊢ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
Theorem: HTPI.remove_one_inv
Proof state before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u
h2 : R x v ∧ R u y ↔ R u y ∧ R x v
⊢ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.remove_one_fcnl
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : matching R A B
h2 : u ∈ A
v : V
⊢ fcnl_on (remove_one R u v) (A \ {u})
Tactic:
define
Proof state after:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : matching R A B
h2 : u ∈ A
v : V
⊢ ∀ ⦃x : U⦄, x ∈ A \ {u} → ∃! y, remove_one R u v x y
Theorem: HTPI.remove_one_fcnl
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : matching R A B
h2 : u ∈ A
v : V
⊢ ∀ ⦃x : U⦄, x ∈ A \ {u} → ∃! y, remove_one R u v x y
Tactic:
fix x : U
Proof state after:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : matching R A B
h2 : u ∈ A
v : V
x : U
⊢ x ∈ A \ {u} → ∃! y, remove_one R u v x y
Theorem: HTPI.remove_one_fcnl
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : matching R A B
h2 : u ∈ A
v : V
x : U
⊢ x ∈ A \ {u} → ∃! y, remove_one R u v x y
Tactic:
assume h3 : x ∈ A \ {u}
Proof state after:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : matching R A B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
⊢ ∃! y, remove_one R u v x y
Theorem: HTPI.remove_one_fcnl
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : matching R A B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
⊢ ∃! y, remove_one R u v x y
Tactic:
obtain (w : U) (h4 : w ∈ A ∧ ∀ (y : V),
  remove_one R u v x y ↔ R w y) from remove_one_iff h1 h2 v h3
Proof state after:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : matching R A B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∃! y, remove_one R u v x y
Theorem: HTPI.remove_one_fcnl
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : matching R A B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∃! y, remove_one R u v x y
Tactic:
define at h1
Proof state after:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∃! y, remove_one R u v x y
Theorem: HTPI.remove_one_fcnl
Proof state before:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∃! y, remove_one R u v x y
Tactic:
exists_unique
Proof state after:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∃ y, remove_one R u v x y

case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∀ (y_1 y_2 : V), remove_one R u v x y_1 → remove_one R u v x y_2 → y_1 = y_2
Theorem: HTPI.remove_one_fcnl
Proof state before:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∃ y, remove_one R u v x y
Tactic:
obtain (y : V) (h5 : R w y) from fcnl_exists h1.right.left h4.left
Proof state after:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y : V
h5 : R w y
⊢ ∃ y, remove_one R u v x y
Theorem: HTPI.remove_one_fcnl
Proof state before:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y : V
h5 : R w y
⊢ ∃ y, remove_one R u v x y
Tactic:
apply Exists.intro y
Proof state after:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y : V
h5 : R w y
⊢ remove_one R u v x y
Theorem: HTPI.remove_one_fcnl
Proof state before:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y : V
h5 : R w y
⊢ remove_one R u v x y
Tactic:
rewrite [h4.right]
Proof state after:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y : V
h5 : R w y
⊢ R w y
Theorem: HTPI.remove_one_fcnl
Proof state before:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y : V
h5 : R w y
⊢ R w y
Tactic:
show R w y from h5
Proof state after:
no goals
Theorem: HTPI.remove_one_fcnl
Proof state before:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∀ (y_1 y_2 : V), remove_one R u v x y_1 → remove_one R u v x y_2 → y_1 = y_2
Tactic:
fix y1 : V
Proof state after:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 : V
⊢ ∀ (y_2 : V), remove_one R u v x y1 → remove_one R u v x y_2 → y1 = y_2
Theorem: HTPI.remove_one_fcnl
Proof state before:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 : V
⊢ ∀ (y_2 : V), remove_one R u v x y1 → remove_one R u v x y_2 → y1 = y_2
Tactic:
fix y2 : V
Proof state after:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
⊢ remove_one R u v x y1 → remove_one R u v x y2 → y1 = y2
Theorem: HTPI.remove_one_fcnl
Proof state before:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
⊢ remove_one R u v x y1 → remove_one R u v x y2 → y1 = y2
Tactic:
rewrite [h4.right, h4.right]
Proof state after:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
⊢ R w y1 → R w y2 → y1 = y2
Theorem: HTPI.remove_one_fcnl
Proof state before:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
⊢ R w y1 → R w y2 → y1 = y2
Tactic:
assume h5 : R w y1
Proof state after:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
h5 : R w y1
⊢ R w y2 → y1 = y2
Theorem: HTPI.remove_one_fcnl
Proof state before:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
h5 : R w y1
⊢ R w y2 → y1 = y2
Tactic:
assume h6 : R w y2
Proof state after:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
h5 : R w y1
h6 : R w y2
⊢ y1 = y2
Theorem: HTPI.remove_one_fcnl
Proof state before:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
h5 : R w y1
h6 : R w y2
⊢ y1 = y2
Tactic:
show y1 = y2 from fcnl_unique h1.right.left h4.left h5 h6
Proof state after:
no goals
Theorem: HTPI.remove_one_match
Proof state before:
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
⊢ matching (remove_one R u v) (A \ {u}) (B \ {v})
Tactic:
define
Proof state after:
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
⊢ rel_within (remove_one R u v) (A \ {u}) (B \ {v}) ∧
    fcnl_on (remove_one R u v) (A \ {u}) ∧ fcnl_on (invRel (remove_one R u v)) (B \ {v})
Theorem: HTPI.remove_one_match
Proof state before:
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
⊢ rel_within (remove_one R u v) (A \ {u}) (B \ {v}) ∧
    fcnl_on (remove_one R u v) (A \ {u}) ∧ fcnl_on (invRel (remove_one R u v)) (B \ {v})
Tactic:
apply And.intro
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
⊢ rel_within (remove_one R u v) (A \ {u}) (B \ {v})

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})
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
⊢ rel_within (remove_one R u v) (A \ {u}) (B \ {v})
Tactic:
define
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}