α : Type u_1
β : Type u_2
γ : Type ?u.86875
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(neighborSet G x.fst)
inst✝¹ : Fintype ↑(neighborSet H x.snd)
inst✝ : Fintype ↑(neighborSet (G □ H) x)
this : Fintype ↑(neighborSet (G □ H) x) := boxProdFintypeNeighborSet x
⊢ neighborFinset (G □ H) x =
    Finset.disjUnion (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd)
      (_ : Disjoint (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd))
α : Type u_1
β : Type u_2
γ : Type ?u.86875
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(neighborSet G x.fst)
inst✝¹ : Fintype ↑(neighborSet H x.snd)
inst✝ : Fintype ↑(neighborSet (G □ H) x)
⊢ neighborFinset (G □ H) x =
    Finset.disjUnion (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd)
      (_ : Disjoint (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd))
letI : Fintype ((G □ H).neighborSet x) := SimpleGraph.boxProdFintypeNeighborSet _
α : Type u_1
β : Type u_2
γ : Type ?u.86875
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(neighborSet G x.fst)
inst✝¹ : Fintype ↑(neighborSet H x.snd)
inst✝ : Fintype ↑(neighborSet (G □ H) x)
this : Fintype ↑(neighborSet (G □ H) x) := boxProdFintypeNeighborSet x
⊢ neighborFinset (G □ H) x =
    Finset.disjUnion (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd)
      (_ : Disjoint (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd))
α : Type u_1
β : Type u_2
γ : Type ?u.86875
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(neighborSet G x.fst)
inst✝¹ : Fintype ↑(neighborSet H x.snd)
inst✝ : Fintype ↑(neighborSet (G □ H) x)
this : Fintype ↑(neighborSet (G □ H) x) := boxProdFintypeNeighborSet x
⊢ neighborFinset (G □ H) x =
    Finset.disjUnion (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd)
      (_ : Disjoint (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd))
convert_to (G □ H).neighborFinset x = _ using 2
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.86875
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(neighborSet G x.fst)
inst✝¹ : Fintype ↑(neighborSet H x.snd)
inst✝ : Fintype ↑(neighborSet (G □ H) x)
this : Fintype ↑(neighborSet (G □ H) x) := boxProdFintypeNeighborSet x
⊢ neighborFinset (G □ H) x =
    Finset.disjUnion (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd)
      (_ : Disjoint (neighborFinset G x.fst ×ˢ {x.snd}) ({x.fst} ×ˢ neighborFinset H x.snd))
exact Eq.trans (Finset.map_map _ _ _) Finset.attach_map_val