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 ((f.sumCongr g.toEquiv) (Sum.inl val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inl val✝)) ↔
    (G ⊕g H).Adj (Sum.inl val✝¹) (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 ((f.sumCongr g.toEquiv) (Sum.inl val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inr val✝)) ↔
    (G ⊕g H).Adj (Sum.inl val✝¹) (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 ((f.sumCongr g.toEquiv) (Sum.inr val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inl val✝)) ↔
    (G ⊕g H).Adj (Sum.inr val✝¹) (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 ((f.sumCongr g.toEquiv) (Sum.inr val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inr val✝)) ↔
    (G ⊕g H).Adj (Sum.inr val✝¹) (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 ((f.sumCongr g.toEquiv) (Sum.inl val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inl val✝)) ↔
    (G ⊕g H).Adj (Sum.inl val✝¹) (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 ((f.sumCongr g.toEquiv) (Sum.inl val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inr val✝)) ↔
    (G ⊕g H).Adj (Sum.inl val✝¹) (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 ((f.sumCongr g.toEquiv) (Sum.inr val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inl val✝)) ↔
    (G ⊕g H).Adj (Sum.inr val✝¹) (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 ((f.sumCongr g.toEquiv) (Sum.inr val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inr val✝)) ↔
    (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝)