Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case 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
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ val✝ : V
huv : (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝))

pp: case 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
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ : V
val✝ : W
huv : (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝))

pp: case inr.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
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ : W
val✝ : V
huv : (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝))

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
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ val✝ : W
huv : (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝))

Tactic:
<;>

Goal state after:
case 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
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ val✝ : V
huv : (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝))

case 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
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ : V
val✝ : W
huv : (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝))

case inr.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
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ : W
val✝ : V
huv : (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝))

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
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ val✝ : W
huv : (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝))