[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ : SimpleGraph α
H✝ : SimpleGraph β
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (fun x y => Adj G x.fst y.fst ∧ x.snd = y.snd ∨ Adj H x.snd y.snd ∧ x.fst = y.fst) x y →
    (fun x y => Adj G x.fst y.fst ∧ x.snd = y.snd ∨ Adj H x.snd y.snd ∧ x.fst = y.fst) y x
[PROOFSTEP]
simp [and_comm, or_comm, eq_comm, adj_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ : SimpleGraph α
H✝ : SimpleGraph β
G : SimpleGraph α
H : SimpleGraph β
x : α × β
⊢ ¬(fun x y => Adj G x.fst y.fst ∧ x.snd = y.snd ∨ Adj H x.snd y.snd ∧ x.fst = y.fst) x x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
a₁ : α
b : β
a₂ : α
⊢ Adj (G □ H) (a₁, b) (a₂, b) ↔ Adj G a₁ a₂
[PROOFSTEP]
simp only [boxProd_adj, and_true, SimpleGraph.irrefl, false_and, or_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
a : α
b₁ b₂ : β
⊢ Adj (G □ H) (a, b₁) (a, b₂) ↔ Adj H b₁ b₂
[PROOFSTEP]
simp only [boxProd_adj, SimpleGraph.irrefl, false_and, and_true, false_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
⊢ neighborSet (G □ H) x = neighborSet G x.fst ×ˢ {x.snd} ∪ {x.fst} ×ˢ neighborSet H x.snd
[PROOFSTEP]
ext ⟨a', b'⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
a' : α
b' : β
⊢ (a', b') ∈ neighborSet (G □ H) x ↔ (a', b') ∈ neighborSet G x.fst ×ˢ {x.snd} ∪ {x.fst} ×ˢ neighborSet H x.snd
[PROOFSTEP]
simp only [mem_neighborSet, Set.mem_union, boxProd_adj, Set.mem_prod, Set.mem_singleton_iff]
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
a' : α
b' : β
⊢ Adj G x.fst a' ∧ x.snd = b' ∨ Adj H x.snd b' ∧ x.fst = a' ↔ Adj G x.fst a' ∧ b' = x.snd ∨ a' = x.fst ∧ Adj H x.snd b'
[PROOFSTEP]
simp only [eq_comm, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
x y : (α × β) × γ
⊢ Adj (G □ (H □ I)) (↑(Equiv.prodAssoc α β γ) x) (↑(Equiv.prodAssoc α β γ) y) ↔ Adj (G □ H □ I) x y
[PROOFSTEP]
simp only [boxProd_adj, Equiv.prodAssoc_apply, or_and_right, or_assoc, Prod.ext_iff, and_assoc,
  @and_comm (x.fst.fst = _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [Walk.boxProdLeft, map_cons, ofBoxProdLeft, Or.by_cases, dif_pos, ← Walk.boxProdLeft]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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_1
β : Type u_2
γ : Type u_3
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_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
simp [ofBoxProdLeft_boxProdLeft]
[GOAL]
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
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_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
exact ⟨h, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [Walk.boxProdRight, map_cons, ofBoxProdRight, Or.by_cases, dif_pos, ← Walk.boxProdRight]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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_2
γ : Type u_3
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_2
γ : Type u_3
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
[PROOFSTEP]
simp [ofBoxProdLeft_boxProdRight]
[GOAL]
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
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_2
γ : Type u_3
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
[PROOFSTEP]
exact ⟨h, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Preconnected G
hH : Preconnected H
⊢ Preconnected (G □ H)
[PROOFSTEP]
rintro x y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Preconnected G
hH : Preconnected H
x y : α × β
⊢ Reachable (G □ H) x y
[PROOFSTEP]
obtain ⟨w₁⟩ := hG x.1 y.1
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Preconnected G
hH : Preconnected H
x y : α × β
w₁ : Walk G x.fst y.fst
⊢ Reachable (G □ H) x y
[PROOFSTEP]
obtain ⟨w₂⟩ := hH x.2 y.2
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Preconnected G
hH : Preconnected H
x y : α × β
w₁ : Walk G x.fst y.fst
w₂ : Walk H x.snd y.snd
⊢ Reachable (G □ H) x y
[PROOFSTEP]
rw [← @Prod.mk.eta _ _ x, ← @Prod.mk.eta _ _ y]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Preconnected G
hH : Preconnected H
x y : α × β
w₁ : Walk G x.fst y.fst
w₂ : Walk H x.snd y.snd
⊢ Reachable (G □ H) (x.fst, x.snd) (y.fst, y.snd)
[PROOFSTEP]
exact ⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : Preconnected (G □ H)
⊢ Preconnected G
[PROOFSTEP]
classical
rintro a₁ a₂
obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)
exact ⟨w.ofBoxProdLeft⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : Preconnected (G □ H)
⊢ Preconnected G
[PROOFSTEP]
rintro a₁ a₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : Preconnected (G □ H)
a₁ a₂ : α
⊢ Reachable G a₁ a₂
[PROOFSTEP]
obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : Preconnected (G □ H)
a₁ a₂ : α
w : Walk (G □ H) (a₁, Classical.arbitrary β) (a₂, Classical.arbitrary β)
⊢ Reachable G a₁ a₂
[PROOFSTEP]
exact ⟨w.ofBoxProdLeft⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : Preconnected (G □ H)
⊢ Preconnected H
[PROOFSTEP]
classical
rintro b₁ b₂
obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
exact ⟨w.ofBoxProdRight⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : Preconnected (G □ H)
⊢ Preconnected H
[PROOFSTEP]
rintro b₁ b₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : Preconnected (G □ H)
b₁ b₂ : β
⊢ Reachable H b₁ b₂
[PROOFSTEP]
obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : Preconnected (G □ H)
b₁ b₂ : β
w : Walk (G □ H) (Classical.arbitrary α, b₁) (Classical.arbitrary α, b₂)
⊢ Reachable H b₁ b₂
[PROOFSTEP]
exact ⟨w.ofBoxProdRight⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Connected G
hH : Connected H
⊢ Connected (G □ H)
[PROOFSTEP]
haveI := hG.nonempty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Connected G
hH : Connected H
this : Nonempty α
⊢ Connected (G □ H)
[PROOFSTEP]
haveI := hH.nonempty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
hG : Connected G
hH : Connected H
this✝ : Nonempty α
this : Nonempty β
⊢ Connected (G □ H)
[PROOFSTEP]
exact ⟨hG.preconnected.boxProd hH.preconnected⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
⊢ Connected G
[PROOFSTEP]
haveI := (nonempty_prod.1 h.nonempty).1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
this : Nonempty α
⊢ Connected G
[PROOFSTEP]
haveI := (nonempty_prod.1 h.nonempty).2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
this✝ : Nonempty α
this : Nonempty β
⊢ Connected G
[PROOFSTEP]
exact ⟨h.preconnected.ofBoxProdLeft⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
⊢ Connected H
[PROOFSTEP]
haveI := (nonempty_prod.1 h.nonempty).1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
this : Nonempty α
⊢ Connected H
[PROOFSTEP]
haveI := (nonempty_prod.1 h.nonempty).2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
h : Connected (G □ H)
this✝ : Nonempty α
this : Nonempty β
⊢ Connected H
[PROOFSTEP]
exact ⟨h.preconnected.ofBoxProdRight⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(neighborSet G x.fst)
inst✝ : Fintype ↑(neighborSet H x.snd)
y : α × β
⊢ y ∈
      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)) ↔
    ↑(Equiv.refl (α × β)) y ∈ neighborSet (G □ H) x
[PROOFSTEP]
simp_rw [Finset.mem_disjUnion, Finset.mem_product, Finset.mem_singleton, mem_neighborFinset, mem_neighborSet,
  Equiv.refl_apply, boxProd_adj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(neighborSet G x.fst)
inst✝ : Fintype ↑(neighborSet H x.snd)
y : α × β
⊢ Adj G x.fst y.fst ∧ y.snd = x.snd ∨ y.fst = x.fst ∧ Adj H x.snd y.snd ↔
    Adj G x.fst y.fst ∧ x.snd = y.snd ∨ Adj H x.snd y.snd ∧ x.fst = y.fst
[PROOFSTEP]
simp only [eq_comm, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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))
[PROOFSTEP]
letI : Fintype ((G □ H).neighborSet x) := SimpleGraph.boxProdFintypeNeighborSet _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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))
[PROOFSTEP]
convert_to (G □ H).neighborFinset x = _ using 2
[GOAL]
case convert_2
α : Type u_1
β : Type u_2
γ : Type u_3
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))
[PROOFSTEP]
exact Eq.trans (Finset.map_map _ _ _) Finset.attach_map_val
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(neighborSet G x.fst)
inst✝¹ : Fintype ↑(neighborSet H x.snd)
inst✝ : Fintype ↑(neighborSet (G □ H) x)
⊢ degree (G □ H) x = degree G x.fst + degree H x.snd
[PROOFSTEP]
rw [degree, degree, degree, boxProd_neighborFinset, Finset.card_disjUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(neighborSet G x.fst)
inst✝¹ : Fintype ↑(neighborSet H x.snd)
inst✝ : Fintype ↑(neighborSet (G □ H) x)
⊢ Finset.card (neighborFinset G x.fst ×ˢ {x.snd}) + Finset.card ({x.fst} ×ˢ neighborFinset H x.snd) =
    Finset.card (neighborFinset G x.fst) + Finset.card (neighborFinset H x.snd)
[PROOFSTEP]
simp_rw [Finset.card_product, Finset.card_singleton, mul_one, one_mul]
