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

State before:
⊢ I 1 = {0}
Tactic:
apply Set.ext
State after:
case h

⊢ ∀ (x : ℕ), x ∈ I 1 ↔ x ∈ {0}

State before:
case h

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

State before:
case h
x : ℕ
⊢ x ∈ I 1 ↔ x ∈ {0}
Tactic:
apply Iff.intro
State after:
case h.mp
x : ℕ
⊢ x ∈ I 1 → x ∈ {0}

case h.mpr
x : ℕ
⊢ x ∈ {0} → x ∈ I 1

State before:
case h.mp
x : ℕ
⊢ x ∈ I 1 → x ∈ {0}
Tactic:
assume h1 : x ∈ I 1
State after:
case h.mp
x : ℕ
h1 : x ∈ I 1
⊢ x ∈ {0}

State before:
case h.mp
x : ℕ
h1 : x ∈ I 1
⊢ x ∈ {0}
Tactic:
rewrite [I_def] at h1
State after:
case h.mp
x : ℕ
h1 : x < 1
⊢ x ∈ {0}

State before:
case h.mp
x : ℕ
h1 : x < 1
⊢ x ∈ {0}
Tactic:
define
State after:
case h.mp
x : ℕ
h1 : x < 1
⊢ x = 0

State before:
case h.mp
x : ℕ
h1 : x < 1
⊢ x = 0
Tactic:
linarith
State after:
no goals

State before:
case h.mpr
x : ℕ
⊢ x ∈ {0} → x ∈ I 1
Tactic:
assume h1 : x ∈ {0}
State after:
case h.mpr
x : ℕ
h1 : x ∈ {0}
⊢ x ∈ I 1

State before:
case h.mpr
x : ℕ
h1 : x ∈ {0}
⊢ x ∈ I 1
Tactic:
define at h1
State after:
case h.mpr
x : ℕ
h1 : x = 0
⊢ x ∈ I 1

State before:
case h.mpr
x : ℕ
h1 : x = 0
⊢ x ∈ I 1
Tactic:
rewrite [h1, I_def]
State after:
case h.mpr
x : ℕ
h1 : x = 0
⊢ 0 < 1

State before:
case h.mpr
x : ℕ
h1 : x = 0
⊢ 0 < 1
Tactic:
linarith
State after:
no goals