Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: 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
⊢ ∀ {a b : (V ⊕ W) ⊕ U},
    (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) a) ((Equiv.sumAssoc V W U) b) ↔ (G ⊕g H ⊕g I).Adj a b

Tactic:
rintro ((u | u) | u) ((v | v) | v)

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)