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

State before:
⊢ ∀ ⦃m n : ℕ⦄, I m ∼ I n → m = n
Tactic:
by_induc
State after:
case Base_Case

⊢ ∀ ⦃n : ℕ⦄, I 0 ∼ I n → 0 = n

case Induction_Step

⊢ ∀ (m : ℕ), (∀ ⦃n : ℕ⦄, I m ∼ I n → m = n) → ∀ ⦃n : ℕ⦄, I (m + 1) ∼ I n → m + 1 = n

State before:
case Base_Case

⊢ ∀ ⦃n : ℕ⦄, I 0 ∼ I n → 0 = n
Tactic:
fix n : Nat
State after:
case Base_Case
n : ℕ
⊢ I 0 ∼ I n → 0 = n

State before:
case Base_Case
n : ℕ
⊢ I 0 ∼ I n → 0 = n
Tactic:
assume h1 : I 0 ∼ I n
State after:
case Base_Case
n : ℕ
h1 : I 0 ∼ I n
⊢ 0 = n

State before:
case Base_Case
n : ℕ
h1 : I 0 ∼ I n
⊢ 0 = n
Tactic:
show 0 = n from (eq_zero_of_I_zero_equinum h1).symm
State after:
no goals

State before:
case Induction_Step

⊢ ∀ (m : ℕ), (∀ ⦃n : ℕ⦄, I m ∼ I n → m = n) → ∀ ⦃n : ℕ⦄, I (m + 1) ∼ I n → m + 1 = n
Tactic:
fix m : Nat
State after:
case Induction_Step
m : ℕ
⊢ (∀ ⦃n : ℕ⦄, I m ∼ I n → m = n) → ∀ ⦃n : ℕ⦄, I (m + 1) ∼ I n → m + 1 = n

State before:
case Induction_Step
m : ℕ
⊢ (∀ ⦃n : ℕ⦄, I m ∼ I n → m = n) → ∀ ⦃n : ℕ⦄, I (m + 1) ∼ I n → m + 1 = n
Tactic:
assume ih : ∀ ⦃n : Nat⦄, I m ∼ I n → m = n
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
⊢ ∀ ⦃n : ℕ⦄, I (m + 1) ∼ I n → m + 1 = n

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
⊢ ∀ ⦃n : ℕ⦄, I (m + 1) ∼ I n → m + 1 = n
Tactic:
fix n : Nat
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
⊢ I (m + 1) ∼ I n → m + 1 = n

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
⊢ I (m + 1) ∼ I n → m + 1 = n
Tactic:
assume h1 : I (m + 1) ∼ I n
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
⊢ m + 1 = n

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
⊢ m + 1 = n
Tactic:
have h2 : n ≠ 0 := by
  by_contra h2
  have h3 : I n ∼ I (m + 1) := Theorem_8_1_3_2 h1
  rewrite [h2] at h3
  have h4 : m + 1 = 0 := eq_zero_of_I_zero_equinum h3
  linarith
  done
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n ≠ 0
⊢ m + 1 = n

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n ≠ 0
⊢ m + 1 = n
Tactic:
obtain (k : Nat) (h3 : n = k + 1) from exists_eq_add_one_of_ne_zero h2
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n ≠ 0
k : ℕ
h3 : n = k + 1
⊢ m + 1 = n

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n ≠ 0
k : ℕ
h3 : n = k + 1
⊢ m + 1 = n
Tactic:
rewrite [h3] at h1
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
⊢ m + 1 = n

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
⊢ m + 1 = n
Tactic:
rewrite [h3]
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
⊢ m + 1 = k + 1

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
⊢ m + 1 = k + 1
Tactic:
have h4 : m ∈ I (m + 1) := I_max m
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
⊢ m + 1 = k + 1

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
⊢ m + 1 = k + 1
Tactic:
have h5 : k ∈ I (k + 1) := I_max k
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
⊢ m + 1 = k + 1

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
⊢ m + 1 = k + 1
Tactic:
have h6 : I (m + 1) \ {m} ∼ I (k + 1) \ {k} :=
  remove_one_equinum h1 h4 h5
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I (m + 1) \ {m} ∼ I (k + 1) \ {k}
⊢ m + 1 = k + 1

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I (m + 1) \ {m} ∼ I (k + 1) \ {k}
⊢ m + 1 = k + 1
Tactic:
rewrite [I_diff, I_diff] at h6
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I m ∼ I k
⊢ m + 1 = k + 1

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I m ∼ I k
⊢ m + 1 = k + 1
Tactic:
have h7 : m = k := ih h6
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I m ∼ I k
h7 : m = k
⊢ m + 1 = k + 1

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I m ∼ I k
h7 : m = k
⊢ m + 1 = k + 1
Tactic:
rewrite [h7]
State after:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I m ∼ I k
h7 : m = k
⊢ k + 1 = k + 1

State before:
case Induction_Step
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h2 : n ≠ 0
k : ℕ
h1 : I (m + 1) ∼ I (k + 1)
h3 : n = k + 1
h4 : m ∈ I (m + 1)
h5 : k ∈ I (k + 1)
h6 : I m ∼ I k
h7 : m = k
⊢ k + 1 = k + 1
Tactic:
rfl
State after:
no goals

State before:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
⊢ n ≠ 0
Tactic:
by_contra h2
State after:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
⊢ False

State before:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
⊢ False
Tactic:
have h3 : I n ∼ I (m + 1) := Theorem_8_1_3_2 h1
State after:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
h3 : I n ∼ I (m + 1)
⊢ False

State before:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
h3 : I n ∼ I (m + 1)
⊢ False
Tactic:
rewrite [h2] at h3
State after:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
h3 : I 0 ∼ I (m + 1)
⊢ False

State before:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
h3 : I 0 ∼ I (m + 1)
⊢ False
Tactic:
have h4 : m + 1 = 0 := eq_zero_of_I_zero_equinum h3
State after:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
h3 : I 0 ∼ I (m + 1)
h4 : m + 1 = 0
⊢ False

State before:
m : ℕ
ih : ∀ ⦃n : ℕ⦄, I m ∼ I n → m = n
n : ℕ
h1 : I (m + 1) ∼ I n
h2 : n = 0
h3 : I 0 ∼ I (m + 1)
h4 : m + 1 = 0
⊢ False
Tactic:
linarith
State after:
no goals