Theorem: HTPI.Theorem_8_1_5_2_to_3 (HTPILib/Chap8Part2.lean)

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
⊢ ∃ R, fcnl_one_one_to_nat R A
Tactic:
obtain (S : Rel Nat U) (h2 : fcnl_onto_from_nat S A) from h1
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : fcnl_onto_from_nat S A
⊢ ∃ R, fcnl_one_one_to_nat R A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : fcnl_onto_from_nat S A
⊢ ∃ R, fcnl_one_one_to_nat R A
Tactic:
define at h2
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
⊢ ∃ R, fcnl_one_one_to_nat R A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
⊢ ∃ R, fcnl_one_one_to_nat R A
Tactic:
set R : Rel U Nat := least_rel_to S
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ ∃ R, fcnl_one_one_to_nat R A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ ∃ R, fcnl_one_one_to_nat R A
Tactic:
apply Exists.intro R
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ fcnl_one_one_to_nat R A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ fcnl_one_one_to_nat R A
Tactic:
define
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ fcnl_on R A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ fcnl_on R A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2
Tactic:
apply And.intro
State after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ fcnl_on R A

case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2

State before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ fcnl_on R A
Tactic:
define
State after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y

State before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
Tactic:
fix x : U
State after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
⊢ x ∈ A → ∃! y, R x y

State before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
⊢ x ∈ A → ∃! y, R x y
Tactic:
assume h4 : x ∈ A
State after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
⊢ ∃! y, R x y

State before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
⊢ ∃! y, R x y
Tactic:
exists_unique
State after:
case left.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
⊢ ∃ y, R x y

case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
⊢ ∀ (y_1 y_2 : ℕ), R x y_1 → R x y_2 → y_1 = y_2

State before:
case left.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
⊢ ∃ y, R x y
Tactic:
have h5 : ∃ (n : Nat), S n x := h2.right h4
State after:
case left.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
h5 : ∃ n, S n x
⊢ ∃ y, R x y

State before:
case left.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
h5 : ∃ n, S n x
⊢ ∃ y, R x y
Tactic:
show ∃ (n : Nat), R x n from exists_least_rel_to h5
State after:
no goals

State before:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
⊢ ∀ (y_1 y_2 : ℕ), R x y_1 → R x y_2 → y_1 = y_2
Tactic:
fix n1 : Nat
State after:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 : ℕ
⊢ ∀ (y_2 : ℕ), R x n1 → R x y_2 → n1 = y_2

State before:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 : ℕ
⊢ ∀ (y_2 : ℕ), R x n1 → R x y_2 → n1 = y_2
Tactic:
fix n2 : Nat
State after:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
⊢ R x n1 → R x n2 → n1 = n2

State before:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
⊢ R x n1 → R x n2 → n1 = n2
Tactic:
assume h5 : R x n1
State after:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
h5 : R x n1
⊢ R x n2 → n1 = n2

State before:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
h5 : R x n1
⊢ R x n2 → n1 = n2
Tactic:
assume h6 : R x n2
State after:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
h5 : R x n1
h6 : R x n2
⊢ n1 = n2

State before:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
h5 : R x n1
h6 : R x n2
⊢ n1 = n2
Tactic:
define at h5
State after:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : R x n2
⊢ n1 = n2

State before:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : R x n2
⊢ n1 = n2
Tactic:
define at h6
State after:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : S n2 x ∧ ∀ (m : ℕ), S m x → n2 ≤ m
⊢ n1 = n2

State before:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : S n2 x ∧ ∀ (m : ℕ), S m x → n2 ≤ m
⊢ n1 = n2
Tactic:
have h7 : n1 ≤ n2 := h5.right n2 h6.left
State after:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : S n2 x ∧ ∀ (m : ℕ), S m x → n2 ≤ m
h7 : n1 ≤ n2
⊢ n1 = n2

State before:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : S n2 x ∧ ∀ (m : ℕ), S m x → n2 ≤ m
h7 : n1 ≤ n2
⊢ n1 = n2
Tactic:
have h8 : n2 ≤ n1 := h6.right n1 h5.left
State after:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : S n2 x ∧ ∀ (m : ℕ), S m x → n2 ≤ m
h7 : n1 ≤ n2
h8 : n2 ≤ n1
⊢ n1 = n2

State before:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : S n2 x ∧ ∀ (m : ℕ), S m x → n2 ≤ m
h7 : n1 ≤ n2
h8 : n2 ≤ n1
⊢ n1 = n2
Tactic:
linarith
State after:
no goals

State before:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2
Tactic:
fix x1 : U
State after:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 : U
⊢ ∀ ⦃x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2

State before:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 : U
⊢ ∀ ⦃x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2
Tactic:
fix x2 : U
State after:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
⊢ ∀ ⦃n : ℕ⦄, x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2

State before:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
⊢ ∀ ⦃n : ℕ⦄, x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2
Tactic:
fix n : Nat
State after:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
⊢ x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2

State before:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
⊢ x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2
Tactic:
assume h4 : x1 ∈ A ∧ R x1 n
State after:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
h4 : x1 ∈ A ∧ R x1 n
⊢ x2 ∈ A ∧ R x2 n → x1 = x2

State before:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
h4 : x1 ∈ A ∧ R x1 n
⊢ x2 ∈ A ∧ R x2 n → x1 = x2
Tactic:
assume h5 : x2 ∈ A ∧ R x2 n
State after:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
⊢ x1 = x2

State before:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
⊢ x1 = x2
Tactic:
have h6 : R x1 n := h4.right
State after:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : R x1 n
⊢ x1 = x2

State before:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : R x1 n
⊢ x1 = x2
Tactic:
have h7 : R x2 n := h5.right
State after:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : R x1 n
h7 : R x2 n
⊢ x1 = x2

State before:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : R x1 n
h7 : R x2 n
⊢ x1 = x2
Tactic:
define at h6
State after:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : S n x1 ∧ ∀ (m : ℕ), S m x1 → n ≤ m
h7 : R x2 n
⊢ x1 = x2

State before:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : S n x1 ∧ ∀ (m : ℕ), S m x1 → n ≤ m
h7 : R x2 n
⊢ x1 = x2
Tactic:
define at h7
State after:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : S n x1 ∧ ∀ (m : ℕ), S m x1 → n ≤ m
h7 : S n x2 ∧ ∀ (m : ℕ), S m x2 → n ≤ m
⊢ x1 = x2

State before:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x1 x2 : U
n : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : S n x1 ∧ ∀ (m : ℕ), S m x1 → n ≤ m
h7 : S n x2 ∧ ∀ (m : ℕ), S m x2 → n ≤ m
⊢ x1 = x2
Tactic:
show x1 = x2 from h2.left h6.left h7.left
State after:
no goals