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

State before:
U : Type
S : Rel ℕ U
x : U
h1 : ∃ n, S n x
⊢ ∃ n, least_rel_to S x n
Tactic:
set W : Set Nat := {n : Nat | S n x}
State after:
U : Type
S : Rel ℕ U
x : U
h1 : ∃ n, S n x
W : Set ℕ := {n | S n x}
⊢ ∃ n, least_rel_to S x n

State before:
U : Type
S : Rel ℕ U
x : U
h1 : ∃ n, S n x
W : Set ℕ := {n | S n x}
⊢ ∃ n, least_rel_to S x n
Tactic:
have h2 : ∃ (n : Nat), n ∈ W := h1
State after:
U : Type
S : Rel ℕ U
x : U
h1 : ∃ n, S n x
W : Set ℕ := {n | S n x}
h2 : ∃ n, n ∈ W
⊢ ∃ n, least_rel_to S x n

State before:
U : Type
S : Rel ℕ U
x : U
h1 : ∃ n, S n x
W : Set ℕ := {n | S n x}
h2 : ∃ n, n ∈ W
⊢ ∃ n, least_rel_to S x n
Tactic:
show ∃ (n : Nat), least_rel_to S x n from well_ord_princ W h2
State after:
no goals