Theorem: SimpleGraph.adj_sup_iff (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
V : Type u_6
s : Finset ι
f : ι → SimpleGraph V
x y : V
⊢ Adj (sup s f) x y ↔ ∃ i ∈ s, Adj (f i) x y
Tactic:
induction' s using Finset.cons_induction_on with a s has ih
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
V : Type u_6
f : ι → SimpleGraph V
x y : V
⊢ Adj (sup ∅ f) x y ↔ ∃ i ∈ ∅, Adj (f i) x y

case h₂
V✝ : Type u_1
V' : Type u_2
G : SimpleGraph V✝
K : Type u_3
K' : Type u_4
ι : Type u_5
V : Type u_6
f : ι → SimpleGraph V
x y : V
a : ι
s : Finset ι
has : a ∉ s
ih : Adj (sup s f) x y ↔ ∃ i ∈ s, Adj (f i) x y
⊢ Adj (sup (cons a s has) f) x y ↔ ∃ i ∈ cons a s has, Adj (f i) 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
V : Type u_6
f : ι → SimpleGraph V
x y : V
⊢ Adj (sup ∅ f) x y ↔ ∃ i ∈ ∅, Adj (f i) x y
Tactic:
simp
State after:
no goals

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
V : Type u_6
f : ι → SimpleGraph V
x y : V
a : ι
s : Finset ι
has : a ∉ s
ih : Adj (sup s f) x y ↔ ∃ i ∈ s, Adj (f i) x y
⊢ Adj (sup (cons a s has) f) x y ↔ ∃ i ∈ cons a s has, Adj (f i) x y
Tactic:
simp [or_and_right, exists_or, ih]
State after:
no goals