Theorem: SimpleGraph.neighborSet_iInf (ExponentialRamsey/Prereq/Mathlib/Combinatorics/SimpleGraph/Basic.lean)

State before:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x : V
⊢ neighborSet (⨅ i, s i) x = ⋂ i, neighborSet (s i) x
Tactic:
ext y
State after:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
⊢ y ∈ neighborSet (⨅ i, s i) x ↔ y ∈ ⋂ i, neighborSet (s i) x

State before:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
⊢ y ∈ neighborSet (⨅ i, s i) x ↔ y ∈ ⋂ i, neighborSet (s i) x
Tactic:
simp only [mem_neighborSet, iInf_adj, Ne.def, Set.iInf_eq_iInter, Set.mem_iInter,
  and_iff_left_iff_imp]
State after:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
⊢ (∀ (i : ι), Adj (s i) x y) → ¬x = y

State before:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
⊢ (∀ (i : ι), Adj (s i) x y) → ¬x = y
Tactic:
intro h
State after:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
h : ∀ (i : ι), Adj (s i) x y
⊢ ¬x = y

State before:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
h : ∀ (i : ι), Adj (s i) x y
⊢ ¬x = y
Tactic:
inhabit ι
State after:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
h : ∀ (i : ι), Adj (s i) x y
inhabited_h : Inhabited ι
⊢ ¬x = y

State before:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
h : ∀ (i : ι), Adj (s i) x y
inhabited_h : Inhabited ι
⊢ ¬x = y
Tactic:
exact (h default).ne
State after:
no goals