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

State before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
⊢ n1 ≤ n2
Tactic:
by_contra h3
State after:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : ¬n1 ≤ n2
⊢ False

State before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : ¬n1 ≤ n2
⊢ False
Tactic:
have h4 : n2 + 1 ≤ n1 := by linarith
State after:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : ¬n1 ≤ n2
h4 : n2 + 1 ≤ n1
⊢ False

State before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : ¬n1 ≤ n2
h4 : n2 + 1 ≤ n1
⊢ False
Tactic:
define at h1
State after:
A : Set ℕ
t n1 n2 : ℕ
h1 : n1 ∈ A ∧ num_elts_below A n1 t
h2 : enum A t n2
h3 : ¬n1 ≤ n2
h4 : n2 + 1 ≤ n1
⊢ False

State before:
A : Set ℕ
t n1 n2 : ℕ
h1 : n1 ∈ A ∧ num_elts_below A n1 t
h2 : enum A t n2
h3 : ¬n1 ≤ n2
h4 : n2 + 1 ≤ n1
⊢ False
Tactic:
have h5 : t < t := neb_increase h2 h4 h1.right
State after:
A : Set ℕ
t n1 n2 : ℕ
h1 : n1 ∈ A ∧ num_elts_below A n1 t
h2 : enum A t n2
h3 : ¬n1 ≤ n2
h4 : n2 + 1 ≤ n1
h5 : t < t
⊢ False

State before:
A : Set ℕ
t n1 n2 : ℕ
h1 : n1 ∈ A ∧ num_elts_below A n1 t
h2 : enum A t n2
h3 : ¬n1 ≤ n2
h4 : n2 + 1 ≤ n1
h5 : t < t
⊢ False
Tactic:
linarith
State after:
no goals

State before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : ¬n1 ≤ n2
⊢ n2 + 1 ≤ n1
Tactic:
linarith
State after:
no goals