Theorem: idx_set_not_inter (meetings/ex2.lean)

State before:
⊢ ∃ α β J I A, J ⊆ I ∧ ¬⋂ j ∈ J, A j ⊆ ⋂ i ∈ I, A i
Tactic:
use ℕ
State after:
case h

⊢ ∃ β J I A, J ⊆ I ∧ ¬⋂ j ∈ J, A j ⊆ ⋂ i ∈ I, A i

State before:
case h

⊢ ∃ β J I A, J ⊆ I ∧ ¬⋂ j ∈ J, A j ⊆ ⋂ i ∈ I, A i
Tactic:
use ℕ
State after:
case h

⊢ ∃ J I A, J ⊆ I ∧ ¬⋂ j ∈ J, A j ⊆ ⋂ i ∈ I, A i

State before:
case h

⊢ ∃ J I A, J ⊆ I ∧ ¬⋂ j ∈ J, A j ⊆ ⋂ i ∈ I, A i
Tactic:
use {1}
State after:
case h

⊢ ∃ I A, {1} ⊆ I ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ I, A i

State before:
case h

⊢ ∃ I A, {1} ⊆ I ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ I, A i
Tactic:
use {1, 2}
State after:
case h

⊢ ∃ A, {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i

State before:
case h

⊢ ∃ A, {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i
Tactic:
let A := λ n : ℕ => ({0, n} : Set ℕ)
State after:
case h
A : ℕ → Set ℕ := fun n => {0, n}
⊢ ∃ A, {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i

State before:
case h
A : ℕ → Set ℕ := fun n => {0, n}
⊢ ∃ A, {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i
Tactic:
use A
State after:
case h
A : ℕ → Set ℕ := fun n => {0, n}
⊢ {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i

State before:
case h
A : ℕ → Set ℕ := fun n => {0, n}
⊢ {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i
Tactic:
simp only [Set.mem_singleton_iff, OfNat.one_ne_ofNat, Set.singleton_subset_iff,
  Set.mem_insert_iff, or_false, Set.iInter_iInter_eq_left, Set.iInter_iInter_eq_or_left,
  Set.subset_inter_iff, not_false_eq_true, Set.insert_subset_insert_iff, Set.subset_singleton_iff,
  imp_self, forall_const, forall_eq, and_false, and_self]
State after:
no goals