Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl.inl.inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u v : V
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl u))) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inl u)) (Sum.inl (Sum.inl v))

pp: case inl.inl.inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u : V
v : W
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl u))) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inl u)) (Sum.inl (Sum.inr v))

pp: case inl.inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u : V
v : U
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl u))) ((Equiv.sumAssoc V W U) (Sum.inr v)) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inl u)) (Sum.inr v)

pp: case inl.inr.inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' u : W
v : V
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr u))) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inr u)) (Sum.inl (Sum.inl v))

pp: case inl.inr.inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' u v : W
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr u))) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inr u)) (Sum.inl (Sum.inr v))

pp: case inl.inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' u : W
v : U
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr u))) ((Equiv.sumAssoc V W U) (Sum.inr v)) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inr u)) (Sum.inr v)

pp: case inr.inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u : U
v : V
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inr u)) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inr u) (Sum.inl (Sum.inl v))

pp: case inr.inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u : U
v : W
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inr u)) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inr u) (Sum.inl (Sum.inr v))

pp: case inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u v : U
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inr u)) ((Equiv.sumAssoc V W U) (Sum.inr v)) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inr u) (Sum.inr v)

Tactic:
<;>

Goal state after:
case inl.inl.inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u v : V
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl u))) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inl u)) (Sum.inl (Sum.inl v))

case inl.inl.inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u : V
v : W
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl u))) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inl u)) (Sum.inl (Sum.inr v))

case inl.inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u : V
v : U
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl u))) ((Equiv.sumAssoc V W U) (Sum.inr v)) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inl u)) (Sum.inr v)

case inl.inr.inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' u : W
v : V
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr u))) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inr u)) (Sum.inl (Sum.inl v))

case inl.inr.inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' u v : W
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr u))) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inr u)) (Sum.inl (Sum.inr v))

case inl.inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' u : W
v : U
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr u))) ((Equiv.sumAssoc V W U) (Sum.inr v)) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inr u)) (Sum.inr v)

case inr.inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u : U
v : V
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inr u)) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inr u) (Sum.inl (Sum.inl v))

case inr.inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u : U
v : W
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inr u)) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inr u) (Sum.inl (Sum.inr v))

case inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u v : U
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inr u)) ((Equiv.sumAssoc V W U) (Sum.inr v)) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inr u) (Sum.inr v)