α : Type u_1
β : Type ?u.70148
γ : Type ?u.70151
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ cons (_ : Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd)
      (ofBoxProdRight (Walk.boxProdRight G a w)) =
    cons' x y z h w

case hc
α : Type u_1
β : Type ?u.70148
γ : Type ?u.70151
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd ∧
    (a, x).fst = (↑(Embedding.toHom (boxProdRight G G a)) y).fst

case hc
α : Type u_1
β : Type ?u.70148
γ : Type ?u.70151
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd ∧
    (a, x).fst = (↑(Embedding.toHom (boxProdRight G G a)) y).fst
α : Type u_1
β : Type ?u.70148
γ : Type ?u.70151
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ ofBoxProdRight (Walk.boxProdRight G a (cons' x y z h w)) = cons' x y z h w
rw [Walk.boxProdRight, map_cons, ofBoxProdRight, Or.by_cases, dif_pos, ←
  Walk.boxProdRight]
case hc
α : Type u_1
β : Type ?u.70148
γ : Type ?u.70151
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd ∧
    (a, x).fst = (↑(Embedding.toHom (boxProdRight G G a)) y).fst

case hc
α : Type u_1
β : Type ?u.70148
γ : Type ?u.70151
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd ∧
    (a, x).fst = (↑(Embedding.toHom (boxProdRight G G a)) y).fst
α : Type u_1
β : Type ?u.70148
γ : Type ?u.70151
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ cons (_ : Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd)
      (ofBoxProdRight (Walk.boxProdRight G a w)) =
    cons' x y z h w

case hc
α : Type u_1
β : Type ?u.70148
γ : Type ?u.70151
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd ∧
    (a, x).fst = (↑(Embedding.toHom (boxProdRight G G a)) y).fst

case hc
α : Type u_1
β : Type ?u.70148
γ : Type ?u.70151
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd ∧
    (a, x).fst = (↑(Embedding.toHom (boxProdRight G G a)) y).fst
simp [ofBoxProdLeft_boxProdRight]
no goals
case hc
α : Type u_1
β : Type ?u.70148
γ : Type ?u.70151
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd ∧
    (a, x).fst = (↑(Embedding.toHom (boxProdRight G G a)) y).fst

case hc
α : Type u_1
β : Type ?u.70148
γ : Type ?u.70151
G : SimpleGraph α
H : SimpleGraph β
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
b₁ b₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ Adj G (a, x).snd (↑(Embedding.toHom (boxProdRight G G a)) y).snd ∧
    (a, x).fst = (↑(Embedding.toHom (boxProdRight G G a)) y).fst
exact⟨h, rfl⟩