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

State before:
A : Set ℕ
t : ℕ
⊢ ∀ ⦃n1 n2 : ℕ⦄, enum A t n1 → enum A t n2 → n1 = n2
Tactic:
fix n1 : Nat
State after:
A : Set ℕ
t n1 : ℕ
⊢ ∀ ⦃n2 : ℕ⦄, enum A t n1 → enum A t n2 → n1 = n2

State before:
A : Set ℕ
t n1 : ℕ
⊢ ∀ ⦃n2 : ℕ⦄, enum A t n1 → enum A t n2 → n1 = n2
Tactic:
fix n2 : Nat
State after:
A : Set ℕ
t n1 n2 : ℕ
⊢ enum A t n1 → enum A t n2 → n1 = n2

State before:
A : Set ℕ
t n1 n2 : ℕ
⊢ enum A t n1 → enum A t n2 → n1 = n2
Tactic:
assume h1 : enum A t n1
State after:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
⊢ enum A t n2 → n1 = n2

State before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
⊢ enum A t n2 → n1 = n2
Tactic:
assume h2 : enum A t n2
State after:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
⊢ n1 = n2

State before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
⊢ n1 = n2
Tactic:
have h3 : n1 ≤ n2 := enum_le h1 h2
State after:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : n1 ≤ n2
⊢ n1 = n2

State before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : n1 ≤ n2
⊢ n1 = n2
Tactic:
have h4 : n2 ≤ n1 := enum_le h2 h1
State after:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : n1 ≤ n2
h4 : n2 ≤ n1
⊢ n1 = n2

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