awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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
⊢ 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 ⋯)
have 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 sorry w'.ofBoxProdRight
      else Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x b₂) w'.ofBoxProdRight sorry)
Tactic: simp only [h₁, and_self, ↓reduceDIte, length_cons, Or.by_cases]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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
⊢ 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 ⋯)
have 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 sorry w'.ofBoxProdRight
        else Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x b₂) w'.ofBoxProdRight sorry))
Tactic: rw [add_comm, add_comm w'.ofBoxProdLeft.length 1, add_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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
⊢ 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 ⋯))
have inl : c.2 = b₁
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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₁
⊢ 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 ⋯))
have inl₁ : HEq w'.ofBoxProdRight (β := H.Walk b₁ b₂)
  (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons sorry w'.ofBoxProdRight
  else Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x b₂) w'.ofBoxProdRight sorry)
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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
⊢ 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 ⋯)
have 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 sorry w'.ofBoxProdLeft
      else Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x a₂) w'.ofBoxProdLeft sorry) +
    length.{u_2} (V := β) (G := H) (u := b₁) (v := b₂)
      (if h : True ∧ True then cons sorry w'.ofBoxProdRight
      else Eq.rec (motive := fun (x : β) (h : c.2 = x) ↦ H.Walk x b₂) w'.ofBoxProdRight sorry)
Tactic: simp only [h₂, add_assoc, Or.by_cases]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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
⊢ 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 ⋯)
have inr : c.1 = a₁
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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₁
⊢ 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 ⋯)
have inr₁ : HEq w'.ofBoxProdLeft (β := G.Walk a₁ a₂)
  (if h : G.Adj c.1 c.1 ∧ b₁ = c.2 then cons sorry w'.ofBoxProdLeft
  else Eq.rec (motive := fun (x : α) (h : c.1 = x) ↦ G.Walk x a₂) w'.ofBoxProdLeft sorry)
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
x y : α × β
⊢ (G □ H).Reachable x y
have obtain : ∀ (w₁ : G.Walk x.1 y.1), (G □ H).Reachable x y
Tactic: obtain ⟨w₁⟩ := hG x.1 y.1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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
⊢ (G □ H).Reachable x y
have obtain : ∀ (w₂ : H.Walk x.2 y.2), (G □ H).Reachable x y
Tactic: obtain ⟨w₂⟩ := hH x.2 y.2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty β
h : (G □ H).Preconnected
a₁ a₂ : α
⊢ G.Reachable a₁ a₂
have obtain : ∀ (w : (G □ H).Walk (a₁, Classical.arbitrary β) (a₂, Classical.arbitrary β)), G.Reachable a₁ a₂
Tactic: obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty β
h : (G □ H).Preconnected
⊢ G.Preconnected
have rintro : ∀ (a₁ a₂ : α), G.Reachable a₁ a₂
Tactic: classical
  rintro a₁ a₂
  obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)
  exact ⟨w.ofBoxProdLeft⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty β
h : (G □ H).Preconnected
rintro : ∀ (a₁ a₂ : α), G.Reachable a₁ a₂
⊢ G.Preconnected
have rintro₁ : ∀ (a₁ a₂ : α) (w : (G □ H).Walk (a₁, Classical.arbitrary β) (a₂, Classical.arbitrary β)), G.Reachable a₁ a₂
Tactic: classical
  rintro a₁ a₂
  obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)
  exact ⟨w.ofBoxProdLeft⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty α
h : (G □ H).Preconnected
b₁ b₂ : β
⊢ H.Reachable b₁ b₂
have obtain : ∀ (w : (G □ H).Walk (Classical.arbitrary α, b₁) (Classical.arbitrary α, b₂)), H.Reachable b₁ b₂
Tactic: obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty α
h : (G □ H).Preconnected
⊢ H.Preconnected
have rintro : ∀ (b₁ b₂ : β), H.Reachable b₁ b₂
Tactic: classical
  rintro b₁ b₂
  obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
  exact ⟨w.ofBoxProdRight⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : Nonempty α
h : (G □ H).Preconnected
rintro : ∀ (b₁ b₂ : β), H.Reachable b₁ b₂
⊢ H.Preconnected
have rintro₁ : ∀ (b₁ b₂ : β) (w : (G □ H).Walk (Classical.arbitrary α, b₁) (Classical.arbitrary α, b₂)), H.Reachable b₁ b₂
Tactic: classical
  rintro b₁ b₂
  obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
  exact ⟨w.ofBoxProdRight⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
⊢ (G □ H).Connected
have this : Nonempty α
Tactic: haveI := hG.nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
this : Nonempty α
⊢ (G □ H).Connected
have this₁ : Nonempty β
Tactic: haveI := hH.nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
⊢ G.Connected
have this : Nonempty α
Tactic: haveI := (nonempty_prod.1 h.nonempty).1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this : Nonempty α
⊢ G.Connected
have this₁ : Nonempty β
Tactic: haveI := (nonempty_prod.1 h.nonempty).2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
⊢ H.Connected
have this : Nonempty α
Tactic: haveI := (nonempty_prod.1 h.nonempty).1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this : Nonempty α
⊢ H.Connected
have this₁ : Nonempty β
Tactic: haveI := (nonempty_prod.1 h.nonempty).2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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 : α × β
⊢ 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 : α × β)
have 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
Tactic: simp_rw [Finset.mem_disjUnion, Finset.mem_product, Finset.mem_singleton, mem_neighborFinset,
        mem_neighborSet, Equiv.refl_apply, boxProd_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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)) ⋯
have 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)) sorry
Tactic: convert_to (G □ H).neighborFinset x = _ using 2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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))
⊢ (G □ H).degree x = G.degree x.1 + H.degree x.2
have 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
Tactic: rw [degree, degree, degree, neighborFinset_boxProd, Finset.card_disjUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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))
⊢ (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
have 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
Tactic: simp_rw [Finset.card_product, Finset.card_singleton, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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
⊢ (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
have simp_rw₁ : (G.neighborFinset x.1).card * 1 + 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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
⊢ (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
have simp_rw₂ : (G.neighborFinset x.1).card + 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (G □ H).Reachable x y ↔ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2
have mp : (G □ H).Reachable x y → G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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
⊢ (G □ H).Reachable x y ↔ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2
have mpr : G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2 → (G □ H).Reachable x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (G □ H).Reachable x y ↔ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2
have mp : (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 _ _)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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
⊢ (G □ H).Reachable x y ↔ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2
have mpr : G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2 → (G □ H).Reachable x y
Tactic: classical
  constructor
  · intro ⟨w⟩
    exact ⟨⟨w.ofBoxProdLeft⟩, ⟨w.ofBoxProdRight⟩⟩
  · intro ⟨⟨w₁⟩, ⟨w₂⟩⟩
    exact ⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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 = ⊤
have simp_rw : ¬(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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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 ≠ ⊤
⊢ (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
have simp_rw₁ : ¬(G □ H).Reachable x y ↔ ¬G.Reachable x.1 y.1 ∨ ¬H.Reachable x.2 y.2
Tactic: simp_rw [← not_ne_iff, edist_ne_top_iff_reachable, reachable_boxProd, not_and_or]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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
⊢ (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
have 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
Tactic: simp_rw [← not_ne_iff, edist_ne_top_iff_reachable, reachable_boxProd, not_and_or]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (hypothesis)
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
have top_case : (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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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 = ⊤
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have pos : ∀ (h : (G □ H).edist x y = ⊤), (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 = ⊤
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (goal)
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
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have neg : ∀ (h : ¬(G □ H).edist x y = ⊤), (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 = ⊤
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (hypothesis)
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 □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have h₁ : G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
Tactic: rw [top_case] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (hypothesis)
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 ≠ ⊤
have h₁ : ¬(G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤)
Tactic: rw [top_case] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Prod (hypothesis)
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 □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
have rGH : 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