Theorem: inter_even_up_to (meetings/ex1.lean)

State before:
⊢ ⋂ j ∈ Set.univ, even_up_to j = Set.singleton 0
Tactic:
simp
State after:
⊢ ⋂ j, even_up_to j = Set.singleton 0

State before:
⊢ ⋂ j, even_up_to j = Set.singleton 0
Tactic:
simp_rw [even_up_to, Set.ext_iff]
State after:
⊢ ∀ (x : ℕ), x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ Set.singleton 0

State before:
⊢ ∀ (x : ℕ), x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ Set.singleton 0
Tactic:
intro x
State after:
x : ℕ
⊢ x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ Set.singleton 0

State before:
x : ℕ
⊢ x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m} ↔ x ∈ Set.singleton 0
Tactic:
constructor
State after:
case mp
x : ℕ
⊢ x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m} → x ∈ Set.singleton 0

case mpr
x : ℕ
⊢ x ∈ Set.singleton 0 → x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m}

State before:
case mp
x : ℕ
⊢ x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m} → x ∈ Set.singleton 0
Tactic:
simp
State after:
case mp
x : ℕ
⊢ (∀ (i : ℕ), x ≤ 2 * i ∧ Even x) → x ∈ Set.singleton 0

State before:
case mp
x : ℕ
⊢ (∀ (i : ℕ), x ≤ 2 * i ∧ Even x) → x ∈ Set.singleton 0
Tactic:
intro imp
State after:
case mp
x : ℕ
imp : ∀ (i : ℕ), x ≤ 2 * i ∧ Even x
⊢ x ∈ Set.singleton 0

State before:
case mp
x : ℕ
imp : ∀ (i : ℕ), x ≤ 2 * i ∧ Even x
⊢ x ∈ Set.singleton 0
Tactic:
specialize imp 0
State after:
case mp
x : ℕ
imp : x ≤ 2 * 0 ∧ Even x
⊢ x ∈ Set.singleton 0

State before:
case mp
x : ℕ
imp : x ≤ 2 * 0 ∧ Even x
⊢ x ∈ Set.singleton 0
Tactic:
simp at imp
State after:
case mp
x : ℕ
imp : x = 0 ∧ Even x
⊢ x ∈ Set.singleton 0

State before:
case mp
x : ℕ
imp : x = 0 ∧ Even x
⊢ x ∈ Set.singleton 0
Tactic:
rcases imp with ⟨hle, _⟩
State after:
case mp.intro
x : ℕ
hle : x = 0
right✝ : Even x
⊢ x ∈ Set.singleton 0

State before:
case mp.intro
x : ℕ
hle : x = 0
right✝ : Even x
⊢ x ∈ Set.singleton 0
Tactic:
exact Set.mem_singleton_of_eq hle
State after:
no goals

State before:
case mpr
x : ℕ
⊢ x ∈ Set.singleton 0 → x ∈ ⋂ j, {m | m ≤ 2 * j ∧ Even m}
Tactic:
simp
State after:
case mpr
x : ℕ
⊢ x ∈ Set.singleton 0 → ∀ (i : ℕ), x ≤ 2 * i ∧ Even x

State before:
case mpr
x : ℕ
⊢ x ∈ Set.singleton 0 → ∀ (i : ℕ), x ≤ 2 * i ∧ Even x
Tactic:
intros mem i
State after:
case mpr
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
⊢ x ≤ 2 * i ∧ Even x

State before:
case mpr
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
⊢ x ≤ 2 * i ∧ Even x
Tactic:
have mem' := Set.eq_of_mem_singleton mem
State after:
case mpr
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ x ≤ 2 * i ∧ Even x

State before:
case mpr
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ x ≤ 2 * i ∧ Even x
Tactic:
constructor
State after:
case mpr.left
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ x ≤ 2 * i

case mpr.right
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ Even x

State before:
case mpr.left
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ x ≤ 2 * i
Tactic:
rw [mem']
State after:
case mpr.left
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ 0 ≤ 2 * i

State before:
case mpr.left
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ 0 ≤ 2 * i
Tactic:
linarith
State after:
no goals

State before:
case mpr.right
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ Even x
Tactic:
rw [mem']
State after:
case mpr.right
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ Even 0

State before:
case mpr.right
x : ℕ
mem : x ∈ Set.singleton 0
i : ℕ
mem' : x = 0
⊢ Even 0
Tactic:
simp
State after:
no goals