awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this_1 : Nonempty α
this : Nonempty β
⊢ G.Connected

Tactic:
exact ⟨h.preconnected.ofBoxProdLeft⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this_1 : Nonempty α
this : Nonempty β
⊢ H.Connected

Tactic:
⟨h.preconnected.ofBoxProdRight⟩

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.Connected.mk, SimpleGraph.Preconnected.ofBoxProdRight
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this_1 : Nonempty α
this : Nonempty β
⊢ H.Connected

Tactic:
exact ⟨h.preconnected.ofBoxProdRight⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
⊢ (G □ H).Connected ↔ G.Connected ∧ H.Connected

Tactic:
⟨fun h => ⟨h.ofBoxProdLeft, h.ofBoxProdRight⟩, fun h => h.1.boxProd h.2⟩

Premises used: SimpleGraph.Connected.boxProd, SimpleGraph.Connected.ofBoxProdRight, And.right, And.left, And.intro, Iff.intro, SimpleGraph.Connected.ofBoxProdLeft
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst : Fintype (↑(G.neighborSet x.1) : Type u_1)
inst_1 : Fintype (↑(H.neighborSet x.2) : Type u_2)
y : α × β
simp_rw : G.Adj x.1 y.1 ∧ y.2 = x.2 ∨ y.1 = x.1 ∧ H.Adj x.2 y.2 ↔ G.Adj x.1 y.1 ∧ x.2 = y.2 ∨ H.Adj x.2 y.2 ∧ x.1 = y.1
⊢ y ∈
      (SProd.sprod (β := Finset β) (G.neighborFinset x.1) {x.2}).disjUnion
        (SProd.sprod (α := Finset α) {x.1} (H.neighborFinset x.2)) ⋯ ↔
    Membership.mem (α := α × β) ((G □ H).neighborSet x) ((Equiv.refl (α × β) : (a : α × β) → α × β) y : α × β)

Tactic:
simp_rw [Finset.mem_disjUnion, Finset.mem_product, Finset.mem_singleton, mem_neighborFinset,
        mem_neighborSet, Equiv.refl_apply, boxProd_adj]

Premises used: Finset.mem_singleton, Equiv.refl_apply, SimpleGraph.mem_neighborSet, SimpleGraph.mem_neighborFinset, Finset.mem_disjUnion, SimpleGraph.boxProd_adj, Finset.mem_product
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst : Fintype (↑(G.neighborSet x.1) : Type u_1)
inst_1 : Fintype (↑(H.neighborSet x.2) : Type u_2)
y : α × β
⊢ G.Adj x.1 y.1 ∧ y.2 = x.2 ∨ y.1 = x.1 ∧ H.Adj x.2 y.2 ↔ G.Adj x.1 y.1 ∧ x.2 = y.2 ∨ H.Adj x.2 y.2 ∧ x.1 = y.1

Tactic:
simp only [eq_comm, and_comm]

Premises used: and_comm, eq_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst : Fintype (↑(G.neighborSet x.1) : Type u_1)
inst_1 : Fintype (↑(H.neighborSet x.2) : Type u_2)
inst_2 : Fintype (↑((G □ H).neighborSet x) : Type (max u_1 u_2))
this : Fintype (↑((G □ H).neighborSet x) : Type (max u_1 u_2)) := boxProdFintypeNeighborSet x
convert_2 :
  (G □ H).neighborFinset x =
    (SProd.sprod (β := Finset β) (G.neighborFinset x.1) {x.2}).disjUnion
      (SProd.sprod (α := Finset α) {x.1} (H.neighborFinset x.2)) ⋯
⊢ (G □ H).neighborFinset x =
    (SProd.sprod (β := Finset β) (G.neighborFinset x.1) {x.2}).disjUnion
      (SProd.sprod (α := Finset α) {x.1} (H.neighborFinset x.2)) ⋯

Tactic:
convert_to (G □ H).neighborFinset x = _ using 2

Premises used: SimpleGraph.boxProd, SimpleGraph.neighborFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst : Fintype (↑(G.neighborSet x.1) : Type u_1)
inst_1 : Fintype (↑(H.neighborSet x.2) : Type u_2)
inst_2 : Fintype (↑((G □ H).neighborSet x) : Type (max u_1 u_2))
this : Fintype (↑((G □ H).neighborSet x) : Type (max u_1 u_2)) := boxProdFintypeNeighborSet x
⊢ (G □ H).neighborFinset x =
    (SProd.sprod (β := Finset β) (G.neighborFinset x.1) {x.2}).disjUnion
      (SProd.sprod (α := Finset α) {x.1} (H.neighborFinset x.2)) ⋯

Tactic:
Eq.trans (Finset.map_map _ _ _) Finset.attach_map_val

Premises used: Finset.attach_map_val, Finset.map_map, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst : Fintype (↑(G.neighborSet x.1) : Type u_1)
inst_1 : Fintype (↑(H.neighborSet x.2) : Type u_2)
inst_2 : Fintype (↑((G □ H).neighborSet x) : Type (max u_1 u_2))
this : Fintype (↑((G □ H).neighborSet x) : Type (max u_1 u_2)) := boxProdFintypeNeighborSet x
⊢ (G □ H).neighborFinset x =
    (SProd.sprod (β := Finset β) (G.neighborFinset x.1) {x.2}).disjUnion
      (SProd.sprod (α := Finset α) {x.1} (H.neighborFinset x.2)) ⋯

Tactic:
exact Eq.trans (Finset.map_map _ _ _) Finset.attach_map_val
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst : Fintype (↑(G.neighborSet x.1) : Type u_1)
inst_1 : Fintype (↑(H.neighborSet x.2) : Type u_2)
inst_2 : Fintype (↑((G □ H).neighborSet x) : Type (max u_1 u_2))
rw :
  (SProd.sprod (β := Finset β) (G.neighborFinset x.1) {x.2}).card +
      (SProd.sprod (α := Finset α) {x.1} (H.neighborFinset x.2)).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card
⊢ (G □ H).degree x = G.degree x.1 + H.degree x.2

Tactic:
rw [degree, degree, degree, neighborFinset_boxProd, Finset.card_disjUnion]

Premises used: SimpleGraph.neighborFinset_boxProd, Finset.card_disjUnion, SimpleGraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst : Fintype (↑(G.neighborSet x.1) : Type u_1)
inst_1 : Fintype (↑(H.neighborSet x.2) : Type u_2)
inst_2 : Fintype (↑((G □ H).neighborSet x) : Type (max u_1 u_2))
simp_rw :
  (G.neighborFinset x.1).card * Finset.card (α := β) {x.2} + Finset.card (α := α) {x.1} * (H.neighborFinset x.2).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card
simp_rw₁ :
  (G.neighborFinset x.1).card * 1 + 1 * (H.neighborFinset x.2).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card
simp_rw₂ :
  (G.neighborFinset x.1).card + 1 * (H.neighborFinset x.2).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card
⊢ (SProd.sprod (β := Finset β) (G.neighborFinset x.1) {x.2}).card +
      (SProd.sprod (α := Finset α) {x.1} (H.neighborFinset x.2)).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card

Tactic:
simp_rw [Finset.card_product, Finset.card_singleton, mul_one, one_mul]

Premises used: Finset.card_product, mul_one, one_mul, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
mp : (G □ H).Reachable x y → G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2
mpr : G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2 → (G □ H).Reachable x y
⊢ (G □ H).Reachable x y ↔ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
w : (G □ H).Walk x y
⊢ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2

Tactic:
⟨⟨w.ofBoxProdLeft⟩, ⟨w.ofBoxProdRight⟩⟩

Premises used: SimpleGraph.Walk.ofBoxProdLeft, Nonempty.intro, And.intro, SimpleGraph.Walk.ofBoxProdRight
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
w : (G □ H).Walk x y
⊢ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2

Tactic:
exact ⟨⟨w.ofBoxProdLeft⟩, ⟨w.ofBoxProdRight⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
w₁ : G.Walk x.1 y.1
w₂ : H.Walk x.2 y.2
⊢ (G □ H).Reachable x y

Tactic:
⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩

Premises used: SimpleGraph.Walk.boxProdRight, SimpleGraph.Walk.boxProdLeft, Nonempty.intro, SimpleGraph.Reachable, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
w₁ : G.Walk x.1 y.1
w₂ : H.Walk x.2 y.2
⊢ (G □ H).Reachable x y

Tactic:
exact ⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
mp : (G □ H).Reachable x y → G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2
mpr mpr₁ : G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2 → (G □ H).Reachable x y
⊢ (G □ H).Reachable x y ↔ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2

Tactic:
classical
  constructor
  · intro ⟨w⟩
    exact ⟨⟨w.ofBoxProdLeft⟩, ⟨w.ofBoxProdRight⟩⟩
  · intro ⟨⟨w₁⟩, ⟨w₂⟩⟩
    exact ⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
simp_rw : ¬(G □ H).edist x y ≠ ⊤ ↔ ¬G.edist x.1 y.1 ≠ ⊤ ∨ ¬H.edist x.2 y.2 ≠ ⊤
simp_rw₁ : ¬(G □ H).Reachable x y ↔ ¬G.Reachable x.1 y.1 ∨ ¬H.Reachable x.2 y.2
simp_rw₂ : ¬(G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2) ↔ ¬G.Reachable x.1 y.1 ∨ ¬H.Reachable x.2 y.2
⊢ (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤

Tactic:
simp_rw [← not_ne_iff, edist_ne_top_iff_reachable, reachable_boxProd, not_and_or]

Premises used: SimpleGraph.edist_ne_top_iff_reachable, not_ne_iff, SimpleGraph.reachable_boxProd, not_and_or
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤

Tactic:
have top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤ := by
    simp_rw [← not_ne_iff, edist_ne_top_iff_reachable, reachable_boxProd, not_and_or]
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
pos : ∀ (h : (G □ H).edist x y = ⊤), (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
neg : ∀ (h : ¬(G □ H).edist x y = ⊤), (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
by_cases h : (G □ H).edist x y = ⊤

Premises used: SimpleGraph.boxProd, SimpleGraph.edist
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : (G □ H).edist x y = ⊤
⊢ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤

Tactic:
rw [top_case] at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
⊢ ¬(G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤)

Tactic:
rw [top_case] at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤)
⊢ G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
⊢ G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤

Tactic:
have rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤ := by rw [top_case] at h; aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
neg :
  ∀ (wG : G.Walk x.1 y.1) (hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1),
    (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
have ⟨wG, hwG⟩ := exists_walk_of_edist_ne_top rGH.1
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
neg :
  ∀ (wH : H.Walk x.2 y.2) (hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2),
    (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
have ⟨wH, hwH⟩ := exists_walk_of_edist_ne_top rGH.2
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
unfold :
  ((Walk.map (G.boxProdLeft H x.2).toHom wG).append (Walk.map (G.boxProdRight H y.1).toHom wH)).length =
    wG.length + wH.length
⊢ w_app.length = wG.length + wH.length

Tactic:
unfold w_app Walk.boxProdLeft Walk.boxProdRight

Premises used: SimpleGraph.Walk.boxProdRight, SimpleGraph.Walk.boxProdLeft
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
⊢ ((Walk.map (G.boxProdLeft H x.2).toHom wG).append (Walk.map (G.boxProdRight H y.1).toHom wH)).length =
    wG.length + wH.length

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
⊢ w_app.length = wG.length + wH.length

Tactic:
have w_len : w_app.length = wG.length + wH.length := by
      unfold w_app Walk.boxProdLeft Walk.boxProdRight; simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
neg : (G □ H).edist x y ≤ G.edist x.1 y.1 + H.edist x.2 y.2
neg₁ : G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (G □ H).edist x y
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ (G □ H).edist x y ≤ (↑w_app.length : ℕ∞)

Tactic:
edist_le _

Premises used: SimpleGraph.edist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ (G □ H).edist x y ≤ (↑w_app.length : ℕ∞)

Tactic:
exact edist_le _

Premises used: SimpleGraph.edist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ (↑w_app.length : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑wG.length : ℕ∞) (↑wH.length : ℕ∞)

Tactic:
exact_mod_cast w_len
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ HAdd.hAdd (α := ℕ∞) (↑wG.length : ℕ∞) (↑wH.length : ℕ∞) = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
simp only [hwG, hwH]
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
calc : (G □ H).edist x y ≤ (↑w_app.length : ℕ∞)
calc₁ : (↑w_app.length : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑wG.length : ℕ∞) (↑wH.length : ℕ∞)
calc₂ : HAdd.hAdd (α := ℕ∞) (↑wG.length : ℕ∞) (↑wH.length : ℕ∞) = G.edist x.1 y.1 + H.edist x.2 y.2
⊢ (G □ H).edist x y ≤ G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
calc (G □ H).edist x y ≤ w_app.length := by exact edist_le _
          _ = wG.length + wH.length := by exact_mod_cast w_len
          _ = G.edist x.1 y.1 + H.edist x.2 y.2 := by simp only [hwG, hwH]

Premises used: SimpleGraph.boxProd, SimpleGraph.Walk.length, Prod.fst, SimpleGraph.edist, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
neg :
  ∀ (w : (G □ H).Walk x y) (hw : (↑w.length : ℕ∞) = (G □ H).edist x y),
    G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (G □ H).edist x y
⊢ G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (G □ H).edist x y

Tactic:
have ⟨w, hw⟩ := exists_walk_of_edist_ne_top h
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
w : (G □ H).Walk x y
hw : (↑w.length : ℕ∞) = (G □ H).edist x y
neg : G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (↑(w.ofBoxProdLeft.length + w.ofBoxProdRight.length) : ℕ∞)
⊢ G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (G □ H).edist x y

Tactic:
rw [← hw, Walk.length_boxProd]

Premises used: SimpleGraph.Walk.length_boxProd
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
w : (G □ H).Walk x y
hw : (↑w.length : ℕ∞) = (G □ H).edist x y
⊢ G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (↑(w.ofBoxProdLeft.length + w.ofBoxProdRight.length) : ℕ∞)

Tactic:
add_le_add (edist_le w.ofBoxProdLeft) (edist_le w.ofBoxProdRight)

Premises used: add_le_add, WithTop.map₂, SimpleGraph.Walk.ofBoxProdLeft, WithTop.some, SimpleGraph.edist_le, SimpleGraph.Walk.ofBoxProdRight, Option.map₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : (↑wG.length : ℕ∞) = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : (↑wH.length : ℕ∞) = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := Walk.append (Walk.boxProdLeft H x.2 wG) (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
w : (G □ H).Walk x y
hw : (↑w.length : ℕ∞) = (G □ H).edist x y
⊢ G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (↑(w.ofBoxProdLeft.length + w.ofBoxProdRight.length) : ℕ∞)

Tactic:
exact add_le_add (edist_le w.ofBoxProdLeft) (edist_le w.ofBoxProdRight)

Premises used: add_le_add, SimpleGraph.Walk.ofBoxProdLeft, SimpleGraph.edist_le, SimpleGraph.Walk.ofBoxProdRight