awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : DecidableEq β
inst_1 : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ G.Adj (x, b).1 (((G.boxProdLeft H b).toHom : (a : α) → α × β) y).1 ∧
    (x, b).2 = (((G.boxProdLeft H b).toHom : (a : α) → α × β) y).2

Tactic:
exact ⟨h, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
rw : cons ⋯ (Walk.boxProdRight G a w).ofBoxProdRight = cons' x y z h w
hc :
  G.Adj (a, x).2 (((G.boxProdRight G a).toHom : (a : α) → α × α) y).2 ∧
    (a, x).1 = (((G.boxProdRight G a).toHom : (a : α) → α × α) y).1
⊢ (Walk.boxProdRight G a (cons' x y z h w)).ofBoxProdRight = cons' x y z h w

Tactic:
rw [Walk.boxProdRight, map_cons, ofBoxProdRight, Or.by_cases, dif_pos, ←
      Walk.boxProdRight]

Premises used: SimpleGraph.Walk.boxProdRight, dif_pos, Or.by_cases, SimpleGraph.Walk.map_cons, SimpleGraph.Walk.ofBoxProdRight
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ cons ⋯ (Walk.boxProdRight G a w).ofBoxProdRight = cons' x y z h w

Tactic:
simp [ofBoxProdRight_boxProdRight]
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ G.Adj (a, x).2 (((G.boxProdRight G a).toHom : (a : α) → α × α) y).2 ∧
    (a, x).1 = (((G.boxProdRight G a).toHom : (a : α) → α × α) y).1

Tactic:
⟨h, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ G.Adj (a, x).2 (((G.boxProdRight G a).toHom : (a : α) → α × α) y).2 ∧
    (a, x).1 = (((G.boxProdRight G a).toHom : (a : α) → α × α) y).1

Tactic:
exact ⟨h, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂ : α
b₁ b₂ : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂, b₂)
⊢ length (V := α × β) (G := G □ H) (u := (a₁, b₁)) nil =
    length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (ofBoxProdLeft (H := H) nil) +
      length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (ofBoxProdRight (G := G) nil)

Tactic:
simp [ofBoxProdLeft, ofBoxProdRight]

Premises used: SimpleGraph.Walk.ofBoxProdLeft, SimpleGraph.Walk.ofBoxProdRight
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
rw :
  w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
        (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons ⋯ w'.ofBoxProdLeft)
          fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
          Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft ⋯) +
      length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
        (⋯.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons ⋯ w'.ofBoxProdRight)
          fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
          Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight ⋯)
⊢ (cons x w').length =
    length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
        (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons ⋯ w'.ofBoxProdLeft)
          fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
          Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft ⋯) +
      length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
        (⋯.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons ⋯ w'.ofBoxProdRight)
          fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
          Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight ⋯)

Tactic:
rw [length_cons, length_boxProd w']

Premises used: SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
⊢ G.Adj a₁ c.1 ∧ b₁ = c.2 ∨ H.Adj b₁ c.2 ∧ a₁ = c.1

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
⊢ G.Adj a₁ c.1 ∧ b₁ = c.2 ∨ H.Adj b₁ c.2 ∧ a₁ = c.1

Tactic:
have disj : (G.Adj a₁ c.1 ∧ b₁ = c.2) ∨ (H.Adj b₁ c.2 ∧ a₁ = c.1) := by simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
disj : G.Adj a₁ c.1 ∧ b₁ = c.2 ∨ H.Adj b₁ c.2 ∧ a₁ = c.1
inl :
  ∀ (h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2),
    w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
      length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
          (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons ⋯ w'.ofBoxProdLeft)
            fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
            Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft ⋯) +
        length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
          (⋯.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons ⋯ w'.ofBoxProdRight)
            fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
            Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight ⋯)
inr :
  ∀ (h₂ : H.Adj b₁ c.2 ∧ a₁ = c.1),
    w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
      length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
          (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons ⋯ w'.ofBoxProdLeft)
            fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
            Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft ⋯) +
        length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
          (⋯.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons ⋯ w'.ofBoxProdRight)
            fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
            Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight ⋯)
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
        (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons ⋯ w'.ofBoxProdLeft)
          fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
          Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft ⋯) +
      length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
        (⋯.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons ⋯ w'.ofBoxProdRight)
          fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
          Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight ⋯)

Tactic:
rcases disj with h₁ | h₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
inl :
  w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    w'.ofBoxProdLeft.length + 1 +
      length.{u_2} (V := β) (G := H) (u := b₁) (v := b₂)
        (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight
        else Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x b₂) w'.ofBoxProdRight ⋯)
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
        (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons ⋯ w'.ofBoxProdLeft)
          fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
          Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft ⋯) +
      length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
        (⋯.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons ⋯ w'.ofBoxProdRight)
          fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
          Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight ⋯)

Tactic:
simp only [h₁, and_self, ↓reduceDIte, length_cons, Or.by_cases]

Premises used: and_self, reduceDIte, Or.by_cases, SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
inl :
  1 + (w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length) =
    1 +
      (w'.ofBoxProdLeft.length +
        length.{u_2} (V := β) (G := H) (u := b₁) (v := b₂)
          (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight
          else Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x b₂) w'.ofBoxProdRight ⋯))
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    w'.ofBoxProdLeft.length + 1 +
      length.{u_2} (V := β) (G := H) (u := b₁) (v := b₂)
        (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight
        else Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x b₂) w'.ofBoxProdRight ⋯)

Tactic:
rw [add_comm, add_comm w'.ofBoxProdLeft.length 1, add_assoc]

Premises used: SimpleGraph.Walk.length, add_assoc, SimpleGraph.Walk.ofBoxProdLeft, add_comm, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
inl : c.2 = b₁
inl₁ :
  HEq w'.ofBoxProdRight (β := H.Walk b₁ b₂)
    (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight
    else Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x b₂) w'.ofBoxProdRight ⋯)
⊢ 1 + (w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length) =
    1 +
      (w'.ofBoxProdLeft.length +
        length.{u_2} (V := β) (G := H) (u := b₁) (v := b₂)
          (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight
          else Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x b₂) w'.ofBoxProdRight ⋯))

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
⊢ c.2 = b₁

Tactic:
simp [h₁.2.symm]

Premises used: And.right, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
⊢ HEq w'.ofBoxProdRight (β := H.Walk b₁ b₂)
    (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight
    else Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x b₂) w'.ofBoxProdRight ⋯)

Tactic:
simp [h₁.2.symm]

Premises used: And.right, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₂ : H.Adj b₁ c.2 ∧ a₁ = c.1
inr :
  w'.ofBoxProdLeft.length + (w'.ofBoxProdRight.length + 1) =
    length.{u_1} (V := α) (G := G) (u := a₁) (v := a₂)
        (if h : G.Adj c.1 c.1 ∧ b₁ = c.2 then cons ⋯ w'.ofBoxProdLeft
        else Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x a₂) w'.ofBoxProdLeft ⋯) +
      length.{u_2} (V := β) (G := H) (u := b₁) (v := b₂)
        (if h : True ∧ True then cons ⋯ w'.ofBoxProdRight
        else Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x b₂) w'.ofBoxProdRight ⋯)
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    length.{u_1} (V := α) (G := G) (u := (a₁, b₁).1) (v := (a₂, b₂).1)
        (Or.by_cases x (fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦ cons ⋯ w'.ofBoxProdLeft)
          fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦
          Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x (a₂, b₂).1) w'.ofBoxProdLeft ⋯) +
      length.{u_2} (V := β) (G := H) (u := (a₁, b₁).2) (v := (a₂, b₂).2)
        (⋯.by_cases (fun (hH : H.Adj (a₁, b₁).2 c.2 ∧ (a₁, b₁).1 = c.1) ↦ cons ⋯ w'.ofBoxProdRight)
          fun (hG : G.Adj (a₁, b₁).1 c.1 ∧ (a₁, b₁).2 = c.2) ↦
          Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x (a₂, b₂).2) w'.ofBoxProdRight ⋯)

Tactic:
simp only [h₂, add_assoc, Or.by_cases]

Premises used: add_assoc, Or.by_cases
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₂ : H.Adj b₁ c.2 ∧ a₁ = c.1
inr : c.1 = a₁
inr₁ :
  HEq w'.ofBoxProdLeft (β := G.Walk a₁ a₂)
    (if h : G.Adj c.1 c.1 ∧ b₁ = c.2 then cons ⋯ w'.ofBoxProdLeft
    else Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x a₂) w'.ofBoxProdLeft ⋯)
⊢ w'.ofBoxProdLeft.length + (w'.ofBoxProdRight.length + 1) =
    length.{u_1} (V := α) (G := G) (u := a₁) (v := a₂)
        (if h : G.Adj c.1 c.1 ∧ b₁ = c.2 then cons ⋯ w'.ofBoxProdLeft
        else Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x a₂) w'.ofBoxProdLeft ⋯) +
      length.{u_2} (V := β) (G := H) (u := b₁) (v := b₂)
        (if h : True ∧ True then cons ⋯ w'.ofBoxProdRight
        else Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x b₂) w'.ofBoxProdRight ⋯)

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₂ : H.Adj b₁ c.2 ∧ a₁ = c.1
⊢ c.1 = a₁

Tactic:
simp [h₂.2.symm]

Premises used: And.right, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂_1 : α
b₁ b₂_1 : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂_1, b₂_1)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₂ : H.Adj b₁ c.2 ∧ a₁ = c.1
⊢ HEq w'.ofBoxProdLeft (β := G.Walk a₁ a₂)
    (if h : G.Adj c.1 c.1 ∧ b₁ = c.2 then cons ⋯ w'.ofBoxProdLeft
    else Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x a₂) w'.ofBoxProdLeft ⋯)

Tactic:
simp [h₂.2.symm]

Premises used: And.right, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂ : α
b₁ b₂ : β
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂, b₂)
⊢ w.length = w.ofBoxProdLeft.length + w.ofBoxProdRight.length

Tactic:
match w with
  | .nil => simp [ofBoxProdLeft, ofBoxProdRight]
  | .cons x w' => next c =>
    unfold ofBoxProdLeft ofBoxProdRight
    rw [length_cons, length_boxProd w']
    have disj : (G.Adj a₁ c.1 ∧ b₁ = c.2) ∨ (H.Adj b₁ c.2 ∧ a₁ = c.1) := by simp_all
    rcases disj with h₁ | h₂
    · simp only [h₁, and_self, ↓reduceDIte, length_cons, Or.by_cases]
      rw [add_comm, add_comm w'.ofBoxProdLeft.length 1, add_assoc]
      congr <;> simp [h₁.2.symm]
    · simp only [h₂, add_assoc, Or.by_cases]
      congr <;> simp [h₂.2.symm]
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
x y : α × β
obtain : ∀ (w₁ : G.Walk x.1 y.1), (G □ H).Reachable x y
⊢ (G □ H).Reachable x y

Tactic:
obtain ⟨w₁⟩ := hG x.1 y.1

Premises used: Prod.fst
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
x y : α × β
w₁ : G.Walk x.1 y.1
obtain : ∀ (w₂ : H.Walk x.2 y.2), (G □ H).Reachable x y
⊢ (G □ H).Reachable x y

Tactic:
obtain ⟨w₂⟩ := hH x.2 y.2

Premises used: Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
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 β
hG : G.Preconnected
hH : H.Preconnected
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 β
inst : Nonempty β
h : (G □ H).Preconnected
a₁ a₂ : α
obtain : ∀ (w : (G □ H).Walk (a₁, Classical.arbitrary β) (a₂, Classical.arbitrary β)), G.Reachable a₁ a₂
⊢ G.Reachable a₁ a₂

Tactic:
obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)

Premises used: Prod.mk, Classical.arbitrary
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty β
h : (G □ H).Preconnected
a₁ a₂ : α
w : (G □ H).Walk (a₁, Classical.arbitrary β) (a₂, Classical.arbitrary β)
⊢ G.Reachable a₁ a₂

Tactic:
⟨w.ofBoxProdLeft⟩

Premises used: SimpleGraph.Walk.ofBoxProdLeft, Nonempty.intro, SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty β
h : (G □ H).Preconnected
a₁ a₂ : α
w : (G □ H).Walk (a₁, Classical.arbitrary β) (a₂, Classical.arbitrary β)
⊢ G.Reachable a₁ a₂

Tactic:
exact ⟨w.ofBoxProdLeft⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty β
h : (G □ H).Preconnected
rintro : ∀ (a₁ a₂ : α), G.Reachable a₁ a₂
rintro₁ : ∀ (a₁ a₂ : α) (w : (G □ H).Walk (a₁, Classical.arbitrary β) (a₂, Classical.arbitrary β)), G.Reachable a₁ a₂
⊢ G.Preconnected

Tactic:
classical
  rintro a₁ a₂
  obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)
  exact ⟨w.ofBoxProdLeft⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty α
h : (G □ H).Preconnected
b₁ b₂ : β
obtain : ∀ (w : (G □ H).Walk (Classical.arbitrary α, b₁) (Classical.arbitrary α, b₂)), H.Reachable b₁ b₂
⊢ H.Reachable b₁ b₂

Tactic:
obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)

Premises used: Prod.mk, Classical.arbitrary
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty α
h : (G □ H).Preconnected
b₁ b₂ : β
w : (G □ H).Walk (Classical.arbitrary α, b₁) (Classical.arbitrary α, b₂)
⊢ H.Reachable b₁ b₂

Tactic:
⟨w.ofBoxProdRight⟩

Premises used: Nonempty.intro, SimpleGraph.Walk.ofBoxProdRight, SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty α
h : (G □ H).Preconnected
b₁ b₂ : β
w : (G □ H).Walk (Classical.arbitrary α, b₁) (Classical.arbitrary α, b₂)
⊢ H.Reachable b₁ b₂

Tactic:
exact ⟨w.ofBoxProdRight⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty α
h : (G □ H).Preconnected
rintro : ∀ (b₁ b₂ : β), H.Reachable b₁ b₂
rintro₁ : ∀ (b₁ b₂ : β) (w : (G □ H).Walk (Classical.arbitrary α, b₁) (Classical.arbitrary α, b₂)), H.Reachable b₁ b₂
⊢ H.Preconnected

Tactic:
classical
  rintro b₁ b₂
  obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
  exact ⟨w.ofBoxProdRight⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
⊢ Nonempty α

Tactic:
haveI := hG.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
this : Nonempty α
⊢ Nonempty β

Tactic:
haveI := hH.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
this_1 : Nonempty α
this : Nonempty β
⊢ (G □ H).Connected

Tactic:
⟨hG.preconnected.boxProd hH.preconnected⟩

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

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

Tactic:
haveI := (nonempty_prod.1 h.nonempty).1
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this : Nonempty α
⊢ Nonempty β

Tactic:
haveI := (nonempty_prod.1 h.nonempty).2
-- 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:
⟨h.preconnected.ofBoxProdLeft⟩

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.Connected.mk, SimpleGraph.Preconnected.ofBoxProdLeft