Theorem: HTPI.well_ord_princ (HTPILib/Chap6.lean)

State before:
S : Set ℕ
⊢ (∃ n, n ∈ S) → ∃ n ∈ S, ∀ m ∈ S, n ≤ m
Tactic:
contrapos
State after:
S : Set ℕ
⊢ (¬∃ n ∈ S, ∀ m ∈ S, n ≤ m) → ¬∃ n, n ∈ S

State before:
S : Set ℕ
⊢ (¬∃ n ∈ S, ∀ m ∈ S, n ≤ m) → ¬∃ n, n ∈ S
Tactic:
assume h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
⊢ ¬∃ n, n ∈ S

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
⊢ ¬∃ n, n ∈ S
Tactic:
quant_neg
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
⊢ ∀ (n : ℕ), n ∉ S

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
⊢ ∀ (n : ℕ), n ∉ S
Tactic:
by_strong_induc
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
⊢ ∀ (n : ℕ), (∀ n_1 < n, n_1 ∉ S) → n ∉ S

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
⊢ ∀ (n : ℕ), (∀ n_1 < n, n_1 ∉ S) → n ∉ S
Tactic:
fix n : Nat
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
⊢ (∀ n_1 < n, n_1 ∉ S) → n ∉ S

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
⊢ (∀ n_1 < n, n_1 ∉ S) → n ∉ S
Tactic:
assume ih : ∀ n_1 < n, n_1 ∉ S
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
⊢ n ∉ S

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
⊢ n ∉ S
Tactic:
contradict h1 with h2
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
⊢ ∃ n ∈ S, ∀ m ∈ S, n ≤ m

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
⊢ ∃ n ∈ S, ∀ m ∈ S, n ≤ m
Tactic:
apply Exists.intro n
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
⊢ n ∈ S ∧ ∀ m ∈ S, n ≤ m

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
⊢ n ∈ S ∧ ∀ m ∈ S, n ≤ m
Tactic:
apply And.intro h2
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
⊢ ∀ m ∈ S, n ≤ m

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
⊢ ∀ m ∈ S, n ≤ m
Tactic:
fix m : Nat
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
⊢ m ∈ S → n ≤ m

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
⊢ m ∈ S → n ≤ m
Tactic:
assume h3 : m ∈ S
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
⊢ n ≤ m

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
⊢ n ≤ m
Tactic:
have h4 : m < n → m ∉ S := ih m
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
h4 : m < n → m ∉ S
⊢ n ≤ m

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
h4 : m < n → m ∉ S
⊢ n ≤ m
Tactic:
contrapos at h4
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
h4 : m ∈ S → ¬m < n
⊢ n ≤ m

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
h4 : m ∈ S → ¬m < n
⊢ n ≤ m
Tactic:
have h5 : ¬m < n := h4 h3
State after:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
h4 : m ∈ S → ¬m < n
h5 : ¬m < n
⊢ n ≤ m

State before:
S : Set ℕ
h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
n : ℕ
ih : ∀ n_1 < n, n_1 ∉ S
h2 : n ∈ S
m : ℕ
h3 : m ∈ S
h4 : m ∈ S → ¬m < n
h5 : ¬m < n
⊢ n ≤ m
Tactic:
linarith
State after:
no goals