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
f : G →g G'
g : H →g H'
val✝¹ val✝ : V
⊢ (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inl val✝¹)) (Sum.map (⇑f) (⇑g) (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
f : G →g G'
g : H →g H'
val✝¹ : V
val✝ : W
⊢ (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inl val✝¹)) (Sum.map (⇑f) (⇑g) (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
f : G →g G'
g : H →g H'
val✝¹ : W
val✝ : V
⊢ (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inr val✝¹)) (Sum.map (⇑f) (⇑g) (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
f : G →g G'
g : H →g H'
val✝¹ val✝ : W
⊢ (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inr val✝¹)) (Sum.map (⇑f) (⇑g) (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
f : G →g G'
g : H →g H'
val✝¹ val✝ : V
⊢ (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inl val✝¹)) (Sum.map (⇑f) (⇑g) (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
f : G →g G'
g : H →g H'
val✝¹ : V
val✝ : W
⊢ (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inl val✝¹)) (Sum.map (⇑f) (⇑g) (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
f : G →g G'
g : H →g H'
val✝¹ : W
val✝ : V
⊢ (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inr val✝¹)) (Sum.map (⇑f) (⇑g) (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
f : G →g G'
g : H →g H'
val✝¹ val✝ : W
⊢ (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inr val✝¹)) (Sum.map (⇑f) (⇑g) (Sum.inr val✝))