Theorem: HTPI.I_diff (HTPILib/Chap8Part1.lean)

State before:
n : ℕ
⊢ I (n + 1) \ {n} = I n
Tactic:
apply Set.ext
State after:
case h
n : ℕ
⊢ ∀ (x : ℕ), x ∈ I (n + 1) \ {n} ↔ x ∈ I n

State before:
case h
n : ℕ
⊢ ∀ (x : ℕ), x ∈ I (n + 1) \ {n} ↔ x ∈ I n
Tactic:
fix x : Nat
State after:
case h
n x : ℕ
⊢ x ∈ I (n + 1) \ {n} ↔ x ∈ I n

State before:
case h
n x : ℕ
⊢ x ∈ I (n + 1) \ {n} ↔ x ∈ I n
Tactic:
apply Iff.intro
State after:
case h.mp
n x : ℕ
⊢ x ∈ I (n + 1) \ {n} → x ∈ I n

case h.mpr
n x : ℕ
⊢ x ∈ I n → x ∈ I (n + 1) \ {n}

State before:
case h.mp
n x : ℕ
⊢ x ∈ I (n + 1) \ {n} → x ∈ I n
Tactic:
assume h1 : x ∈ I (n + 1) \ {n}
State after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) \ {n}
⊢ x ∈ I n

State before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) \ {n}
⊢ x ∈ I n
Tactic:
define
State after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) \ {n}
⊢ x < n

State before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) \ {n}
⊢ x < n
Tactic:
define at h1
State after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
⊢ x < n

State before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
⊢ x < n
Tactic:
have h2 : x ∈ I (n + 1) := h1.left
State after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x ∈ I (n + 1)
⊢ x < n

State before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x ∈ I (n + 1)
⊢ x < n
Tactic:
have h3 : ¬x ∈ {n} := h1.right
State after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x ∈ I (n + 1)
h3 : x ∉ {n}
⊢ x < n

State before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x ∈ I (n + 1)
h3 : x ∉ {n}
⊢ x < n
Tactic:
define at h2
State after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x < n + 1
h3 : x ∉ {n}
⊢ x < n

State before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x < n + 1
h3 : x ∉ {n}
⊢ x < n
Tactic:
define at h3
State after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x < n + 1
h3 : ¬x = n
⊢ x < n

State before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x < n + 1
h3 : ¬x = n
⊢ x < n
Tactic:
have h4 : x ≤ n := Nat.le_of_lt_succ h2
State after:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x < n + 1
h3 : ¬x = n
h4 : x ≤ n
⊢ x < n

State before:
case h.mp
n x : ℕ
h1 : x ∈ I (n + 1) ∧ x ∉ {n}
h2 : x < n + 1
h3 : ¬x = n
h4 : x ≤ n
⊢ x < n
Tactic:
show x < n from Nat.lt_of_le_of_ne h4 h3
State after:
no goals

State before:
case h.mpr
n x : ℕ
⊢ x ∈ I n → x ∈ I (n + 1) \ {n}
Tactic:
assume h1 : x ∈ I n
State after:
case h.mpr
n x : ℕ
h1 : x ∈ I n
⊢ x ∈ I (n + 1) \ {n}

State before:
case h.mpr
n x : ℕ
h1 : x ∈ I n
⊢ x ∈ I (n + 1) \ {n}
Tactic:
define at h1
State after:
case h.mpr
n x : ℕ
h1 : x < n
⊢ x ∈ I (n + 1) \ {n}

State before:
case h.mpr
n x : ℕ
h1 : x < n
⊢ x ∈ I (n + 1) \ {n}
Tactic:
define
State after:
case h.mpr
n x : ℕ
h1 : x < n
⊢ x ∈ I (n + 1) ∧ x ∉ {n}

State before:
case h.mpr
n x : ℕ
h1 : x < n
⊢ x ∈ I (n + 1) ∧ x ∉ {n}
Tactic:
apply And.intro
State after:
case h.mpr.left
n x : ℕ
h1 : x < n
⊢ x ∈ I (n + 1)

case h.mpr.right
n x : ℕ
h1 : x < n
⊢ x ∉ {n}

State before:
case h.mpr.left
n x : ℕ
h1 : x < n
⊢ x ∈ I (n + 1)
Tactic:
define
State after:
case h.mpr.left
n x : ℕ
h1 : x < n
⊢ x < n + 1

State before:
case h.mpr.left
n x : ℕ
h1 : x < n
⊢ x < n + 1
Tactic:
linarith
State after:
no goals

State before:
case h.mpr.right
n x : ℕ
h1 : x < n
⊢ x ∉ {n}
Tactic:
by_contra h2
State after:
case h.mpr.right
n x : ℕ
h1 : x < n
h2 : x ∈ {n}
⊢ False

State before:
case h.mpr.right
n x : ℕ
h1 : x < n
h2 : x ∈ {n}
⊢ False
Tactic:
define at h2
State after:
case h.mpr.right
n x : ℕ
h1 : x < n
h2 : x = n
⊢ False

State before:
case h.mpr.right
n x : ℕ
h1 : x < n
h2 : x = n
⊢ False
Tactic:
linarith
State after:
no goals