Theorem: union_even_up_to (meetings/ex1.lean)

State before:
⊢ ⋃ j ∈ Set.univ, even_up_to j = {m | Even m}
Tactic:
simp
State after:
⊢ ⋃ j, even_up_to j = {m | Even m}

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

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

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

case mpr
x : ℕ
⊢ x ∈ {m | Even m} → x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m}

State before:
case mp
x : ℕ
⊢ x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m} → x ∈ {m | Even m}
Tactic:
simp
State after:
no goals

State before:
case mpr
x : ℕ
⊢ x ∈ {m | Even m} → x ∈ ⋃ j, {m | m ≤ 2 * j ∧ Even m}
Tactic:
simp
State after:
case mpr
x : ℕ
⊢ Even x → (∃ x_1, x ≤ 2 * x_1) ∧ Even x

State before:
case mpr
x : ℕ
⊢ Even x → (∃ x_1, x ≤ 2 * x_1) ∧ Even x
Tactic:
intro heven
State after:
case mpr
x : ℕ
heven : Even x
⊢ (∃ x_1, x ≤ 2 * x_1) ∧ Even x

State before:
case mpr
x : ℕ
heven : Even x
⊢ (∃ x_1, x ≤ 2 * x_1) ∧ Even x
Tactic:
constructor
State after:
case mpr.left
x : ℕ
heven : Even x
⊢ ∃ x_1, x ≤ 2 * x_1

case mpr.right
x : ℕ
heven : Even x
⊢ Even x

State before:
case mpr.left
x : ℕ
heven : Even x
⊢ ∃ x_1, x ≤ 2 * x_1
Tactic:
use x
State after:
case h
x : ℕ
heven : Even x
⊢ x ≤ 2 * x

State before:
case h
x : ℕ
heven : Even x
⊢ x ≤ 2 * x
Tactic:
linarith
State after:
no goals

State before:
case mpr.right
x : ℕ
heven : Even x
⊢ Even x
Tactic:
exact heven
State after:
no goals