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

State before:
A : Set ℕ
⊢ ∀ ⦃n s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
Tactic:
by_induc
State after:
case Base_Case
A : Set ℕ
⊢ ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A 0 s1 → num_elts_below A 0 s2 → s1 = s2

case Induction_Step
A : Set ℕ
⊢ ∀ (n : ℕ),
    (∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2) →
      ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2

State before:
case Base_Case
A : Set ℕ
⊢ ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A 0 s1 → num_elts_below A 0 s2 → s1 = s2
Tactic:
fix s1 : Nat
State after:
case Base_Case
A : Set ℕ
s1 : ℕ
⊢ ∀ ⦃s2 : ℕ⦄, num_elts_below A 0 s1 → num_elts_below A 0 s2 → s1 = s2

State before:
case Base_Case
A : Set ℕ
s1 : ℕ
⊢ ∀ ⦃s2 : ℕ⦄, num_elts_below A 0 s1 → num_elts_below A 0 s2 → s1 = s2
Tactic:
fix s2 : Nat
State after:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
⊢ num_elts_below A 0 s1 → num_elts_below A 0 s2 → s1 = s2

State before:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
⊢ num_elts_below A 0 s1 → num_elts_below A 0 s2 → s1 = s2
Tactic:
assume h1 : num_elts_below A 0 s1
State after:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : num_elts_below A 0 s1
⊢ num_elts_below A 0 s2 → s1 = s2

State before:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : num_elts_below A 0 s1
⊢ num_elts_below A 0 s2 → s1 = s2
Tactic:
assume h2 : num_elts_below A 0 s2
State after:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : num_elts_below A 0 s1
h2 : num_elts_below A 0 s2
⊢ s1 = s2

State before:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : num_elts_below A 0 s1
h2 : num_elts_below A 0 s2
⊢ s1 = s2
Tactic:
define at h1
State after:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : s1 = 0
h2 : num_elts_below A 0 s2
⊢ s1 = s2

State before:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : s1 = 0
h2 : num_elts_below A 0 s2
⊢ s1 = s2
Tactic:
define at h2
State after:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : s1 = 0
h2 : s2 = 0
⊢ s1 = s2

State before:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : s1 = 0
h2 : s2 = 0
⊢ s1 = s2
Tactic:
rewrite [h1, h2]
State after:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : s1 = 0
h2 : s2 = 0
⊢ 0 = 0

State before:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : s1 = 0
h2 : s2 = 0
⊢ 0 = 0
Tactic:
rfl
State after:
no goals

State before:
case Induction_Step
A : Set ℕ
⊢ ∀ (n : ℕ),
    (∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2) →
      ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Tactic:
fix n : Nat
State after:
case Induction_Step
A : Set ℕ
n : ℕ
⊢ (∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2) →
    ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2

State before:
case Induction_Step
A : Set ℕ
n : ℕ
⊢ (∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2) →
    ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Tactic:
assume ih : ∀ ⦃s1 s2 : Nat⦄,
  num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
State after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
⊢ ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2

State before:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
⊢ ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Tactic:
fix s1 : Nat
State after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 : ℕ
⊢ ∀ ⦃s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2

State before:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 : ℕ
⊢ ∀ ⦃s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Tactic:
fix s2 : Nat
State after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
⊢ num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2

State before:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
⊢ num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Tactic:
assume h1 : num_elts_below A (n + 1) s1
State after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
⊢ num_elts_below A (n + 1) s2 → s1 = s2

State before:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
⊢ num_elts_below A (n + 1) s2 → s1 = s2
Tactic:
assume h2 : num_elts_below A (n + 1) s2
State after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
h2 : num_elts_below A (n + 1) s2
⊢ s1 = s2

State before:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
h2 : num_elts_below A (n + 1) s2
⊢ s1 = s2
Tactic:
by_cases h3 : n ∈ A
State after:
case pos
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
h2 : num_elts_below A (n + 1) s2
h3 : n ∈ A
⊢ s1 = s2

case neg
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
h2 : num_elts_below A (n + 1) s2
h3 : n ∉ A
⊢ s1 = s2

State before:
case pos
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
h2 : num_elts_below A (n + 1) s2
h3 : n ∈ A
⊢ s1 = s2
Tactic:
rewrite [neb_step_elt h3] at h1
State after:
case pos
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : 1 ≤ s1 ∧ num_elts_below A n (s1 - 1)
h2 : num_elts_below A (n + 1) s2
h3 : n ∈ A
⊢ s1 = s2

State before:
case pos
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : 1 ≤ s1 ∧ num_elts_below A n (s1 - 1)
h2 : num_elts_below A (n + 1) s2
h3 : n ∈ A
⊢ s1 = s2
Tactic:
rewrite [neb_step_elt h3] at h2
State after:
case pos
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : 1 ≤ s1 ∧ num_elts_below A n (s1 - 1)
h2 : 1 ≤ s2 ∧ num_elts_below A n (s2 - 1)
h3 : n ∈ A
⊢ s1 = s2

State before:
case pos
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : 1 ≤ s1 ∧ num_elts_below A n (s1 - 1)
h2 : 1 ≤ s2 ∧ num_elts_below A n (s2 - 1)
h3 : n ∈ A
⊢ s1 = s2
Tactic:
have h4 : s1 - 1 = s2 - 1 := ih h1.right h2.right
State after:
case pos
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : 1 ≤ s1 ∧ num_elts_below A n (s1 - 1)
h2 : 1 ≤ s2 ∧ num_elts_below A n (s2 - 1)
h3 : n ∈ A
h4 : s1 - 1 = s2 - 1
⊢ s1 = s2

State before:
case pos
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : 1 ≤ s1 ∧ num_elts_below A n (s1 - 1)
h2 : 1 ≤ s2 ∧ num_elts_below A n (s2 - 1)
h3 : n ∈ A
h4 : s1 - 1 = s2 - 1
⊢ s1 = s2
Tactic:
show s1 = s2 from
  calc s1
    _ = s1 - 1 + 1 := (Nat.sub_add_cancel h1.left).symm
    _ = s2 - 1 + 1 := by rw [h4]
    _ = s2 := Nat.sub_add_cancel h2.left
State after:
no goals

State before:
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : 1 ≤ s1 ∧ num_elts_below A n (s1 - 1)
h2 : 1 ≤ s2 ∧ num_elts_below A n (s2 - 1)
h3 : n ∈ A
h4 : s1 - 1 = s2 - 1
⊢ s1 - 1 + 1 = s2 - 1 + 1
Tactic:
rw [h4]
State after:
no goals

State before:
case neg
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
h2 : num_elts_below A (n + 1) s2
h3 : n ∉ A
⊢ s1 = s2
Tactic:
rewrite [neb_step_not_elt h3] at h1
State after:
case neg
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A n s1
h2 : num_elts_below A (n + 1) s2
h3 : n ∉ A
⊢ s1 = s2

State before:
case neg
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A n s1
h2 : num_elts_below A (n + 1) s2
h3 : n ∉ A
⊢ s1 = s2
Tactic:
rewrite [neb_step_not_elt h3] at h2
State after:
case neg
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A n s1
h2 : num_elts_below A n s2
h3 : n ∉ A
⊢ s1 = s2

State before:
case neg
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A n s1
h2 : num_elts_below A n s2
h3 : n ∉ A
⊢ s1 = s2
Tactic:
show s1 = s2 from ih h1 h2
State after:
no goals