α : Type u_2
β : Type u_1
γ : Type ?u.57688
G : SimpleGraph α
H : SimpleGraph β
b : β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ x z y : α
h : Adj G x y
w : Walk G y z
⊢ cons (_ : Adj G (x, b).fst (↑(Embedding.toHom (boxProdLeft G H b)) y).fst) (ofBoxProdLeft (Walk.boxProdLeft H b w)) =
    cons' x y z h w

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

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

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

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

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

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