FormalConjectures.Wikipedia.PebblingNumberConjecture

FormalConjectures
Wikipedia
PebblingNumberConjecture

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Pebbling number conjecture

References:

Wikipedia

Pebbling on Graph Products and Other Binary Graph Constructions

variable {V : Type} {G : SimpleGraph V} [DecidableEq V]


namespace PebblingNumberConjecture

A Pebble distribution is an assigment of zero or more pebbles to each of the vertices.

def PebbleDistribution (V : Type) := V → ℕ

The number of pebbles of a distribution is the total number summed over all vertices.

def NumberOfPebbles [Fintype V] : (PebbleDistribution V) → ℕ := fun D => ∑ v, D v

A pebbling move on a graph consists of choosing a vertex with at least two pebbles, removing two pebbles from it, and adding one to an adjacent vertex (the second removed pebble is discarded from play).

def IsPebblingMove (G : SimpleGraph V) (A B : PebbleDistribution V) : Prop :=
    ∃ v w : V, (A v) ≥ 2 ∧ G.Adj v w ∧
    B = (fun u =>
      if u = w then A u + 1
      else if u = v then A u - 2
      else A u)


@[category API, AMS 5]
theorem IsPebblingMove.refl (G : SimpleGraph V) (A : PebbleDistribution V) {v w : V} (hv : 2 ≤ A v)
    (hvw : G.Adj v w) :
    IsPebblingMove G A fun u =>
      if u = w then A u + 1
      else if u = v then A u - 2
      else A u :=
  ⟨v, w, hv, hvw, rfl⟩

A pebble path is a series of pebbling moves.

inductive PebblePath {α : Type} (r : α → α → Prop) : α → α → Type
  | refl (a : α) : PebblePath r a a
  | step {a b c : α} (p : PebblePath r a b) (h : r b c) : PebblePath r a c

Indicates whether there exists a sequence of pebbling moves transforming one pebble distribution to another.

def ExistsPebblePath {α : Type} (r : α → α → Prop) (a b : α) : Prop :=
  Nonempty (PebblePath r a b)

A pebble distribution B is reachable from another pebble distribution A, if there exists a sequence of pebbling moves transforming the first into the second.

def IsReachable (G : SimpleGraph V) (A B : PebbleDistribution V) : Prop :=
  ExistsPebblePath (IsPebblingMove G) A B


@[simp, category API, AMS 5]
theorem IsReachable.refl (G : SimpleGraph V) (A : PebbleDistribution V) : IsReachable G A A := byV:Typeinst✝:DecidableEq VG:SimpleGraph VA:PebbleDistribution V⊢ IsReachable G A A
  tautoAll goals completed! 🐙

The pebbling number of a graph G, is the lowest natural number n that satisfies the following condition: Given any target or 'root' vertex in the graph and any initial pebbles distribution with n pebbles on the graph, another pebble distribution is reachable in which the designated root vertex has one or more pebbles.

noncomputable def PebblingNumber [Fintype V] (G : SimpleGraph V) : ℕ :=
  sInf { n | ∀ D, NumberOfPebbles D = n → ∀ v, ∃ D', IsReachable G D D' ∧ 1 ≤ D' v }

The pebbling number of the complete graph on n vertices is n.

@[category API, AMS 5]
theorem PebblingNumber_completeGraph [Fintype V] :
    PebblingNumber (SimpleGraph.completeGraph V) = Fintype.card V := byV:Typeinst✝¹:DecidableEq Vinst✝:Fintype V⊢ PebblingNumber (SimpleGraph.completeGraph V) = Fintype.card V
  refine IsLeast.csInf_eq ⟨fun D hD v => ?_, fun a ha => not_lt.1 fun ha_lt => ?_⟩refine_1V:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:V⊢ ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' vrefine_2V:Typeinst✝¹:DecidableEq Vinst✝:Fintype Va:ℕha:a ∈
  {n |
    ∀ (D : PebbleDistribution V),
      NumberOfPebbles D = n → ∀ (v : V), ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v}ha_lt:a < Fintype.card V⊢ False
  ·refine_1V:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:V⊢ ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v by_cases h : ∃ w, 2 ≤ D wposV:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:Vh:∃ w, 2 ≤ D w⊢ ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' vnegV:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:Vh:¬∃ w, 2 ≤ D w⊢ ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v
    ·posV:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:Vh:∃ w, 2 ≤ D w⊢ ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v obtain ⟨w, hw⟩ := hposV:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:Vw:Vhw:2 ≤ D w⊢ ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v
      by_cases hwv : w = vposV:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:Vw:Vhw:2 ≤ D whwv:w = v⊢ ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' vnegV:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:Vw:Vhw:2 ≤ D whwv:¬w = v⊢ ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v
      ·posV:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:Vw:Vhw:2 ≤ D whwv:w = v⊢ ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v exact ⟨D, .refl _ _, hwv ▸ Nat.one_le_of_lt hw⟩All goals completed! 🐙
      ·negV:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:Vw:Vhw:2 ≤ D whwv:¬w = v⊢ ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v exact ⟨fun u => if u = v then D u + 1 else if u = w then D u - 2 else D u,
          ⟨.step (.refl _) (.refl _ _ hw (byV:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:Vw:Vhw:2 ≤ D whwv:¬w = v⊢ (SimpleGraph.completeGraph V).Adj w v simpaAll goals completed! 🐙))⟩, byV:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:Vw:Vhw:2 ≤ D whwv:¬w = v⊢ 1 ≤ (fun u => if u = v then D u + 1 else if u = w then D u - 2 else D u) v simpAll goals completed! 🐙⟩
    ·negV:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:Vh:¬∃ w, 2 ≤ D w⊢ ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v refine ⟨D, byV:Typeinst✝¹:DecidableEq Vinst✝:Fintype VD:PebbleDistribution VhD:NumberOfPebbles D = Fintype.card Vv:Vh:¬∃ w, 2 ≤ D w⊢ IsReachable (SimpleGraph.completeGraph V) D D tautoAll goals completed! 🐙, not_lt.1 fun hD' => ?_⟩
      exact Finset.sum_lt_sum (fun a s => Nat.le_of_lt_succ <| not_le.1 (h ⟨a, · ⟩))
        ⟨_, Finset.mem_univ _, hD'⟩ |>.trans_eq Fintype.card_eq_sum_ones.symm |>.ne hDAll goals completed! 🐙
  ·refine_2V:Typeinst✝¹:DecidableEq Vinst✝:Fintype Va:ℕha:a ∈
  {n |
    ∀ (D : PebbleDistribution V),
      NumberOfPebbles D = n → ∀ (v : V), ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v}ha_lt:a < Fintype.card V⊢ False let R := Finset.equivFinOfCardEq (Finset.card_univ (α := V))refine_2V:Typeinst✝¹:DecidableEq Vinst✝:Fintype Va:ℕha:a ∈
  {n |
    ∀ (D : PebbleDistribution V),
      NumberOfPebbles D = n → ∀ (v : V), ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v}ha_lt:a < Fintype.card VR:↥Finset.univ ≃ Fin (Fintype.card V) := Finset.equivFinOfCardEq ⋯⊢ False
    let D : PebbleDistribution V := fun x ↦ if R ⟨_, Finset.mem_univ x⟩ < a then 1 else 0refine_2V:Typeinst✝¹:DecidableEq Vinst✝:Fintype Va:ℕha:a ∈
  {n |
    ∀ (D : PebbleDistribution V),
      NumberOfPebbles D = n → ∀ (v : V), ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v}ha_lt:a < Fintype.card VR:↥Finset.univ ≃ Fin (Fintype.card V) := Finset.equivFinOfCardEq ⋯D:PebbleDistribution V := fun x => if ↑(R ⟨x, ⋯⟩) < a then 1 else 0⊢ False
    have hD : NumberOfPebbles D = a :=
      (Finset.sum_attach _ _).symm.trans ((R.sum_comp (if · < a then 1 else 0)).trans
        (.trans ( Finset.sum_fin_eq_sum_range _)
          (byV:Typeinst✝¹:DecidableEq Vinst✝:Fintype Va:ℕha:a ∈
  {n |
    ∀ (D : PebbleDistribution V),
      NumberOfPebbles D = n → ∀ (v : V), ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v}ha_lt:a < Fintype.card VR:↥Finset.univ ≃ Fin (Fintype.card V) := Finset.equivFinOfCardEq ⋯D:PebbleDistribution V := fun x => if ↑(R ⟨x, ⋯⟩) < a then 1 else 0⊢ (∑ i ∈ Finset.range (Fintype.card V), if h : i < Fintype.card V then if ↑⟨i, h⟩ < a then 1 else 0 else 0) = a norm_num [← Finset.mem_range, Finset.inter_eq_right.2, ha_lt.le]All goals completed! 🐙)))
    obtain ⟨D', ⟨P⟩, h⟩ := ha D hD (R.symm ⟨a, ha_lt⟩)refine_2V:Typeinst✝¹:DecidableEq Vinst✝:Fintype Va:ℕha:a ∈
  {n |
    ∀ (D : PebbleDistribution V),
      NumberOfPebbles D = n → ∀ (v : V), ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v}ha_lt:a < Fintype.card VR:↥Finset.univ ≃ Fin (Fintype.card V) := Finset.equivFinOfCardEq ⋯D:PebbleDistribution V := fun x => if ↑(R ⟨x, ⋯⟩) < a then 1 else 0hD:NumberOfPebbles D = a := 
  Eq.trans (Eq.symm (Finset.sum_attach Finset.univ D))
    (Eq.trans (Equiv.sum_comp R fun x => if ↑x < a then 1 else 0)
      (Eq.trans (Finset.sum_fin_eq_sum_range fun i => if ↑i < a then 1 else 0)
        (of_eq_true
          (Eq.trans
            (Eq.trans
              (congrArg (fun x => x = a)
                (Eq.trans
                  (Eq.trans
                    (Finset.sum_congr (Eq.refl (Finset.range (Fintype.card V))) fun x a_1 =>
                      dite_congr PebblingNumber_completeGraph._simp_1
                        (fun h => ite_congr PebblingNumber_completeGraph._simp_1 (fun a => Eq.refl 1) fun a => Eq.refl 0)
                        fun h => Eq.refl 0)
                    (Finset.sum_ite_mem (Finset.range (Fintype.card V)) (Finset.range (Fintype.card V)) fun i =>
                      if i ∈ Finset.range a then 1 else 0))
                  (Eq.trans
                    (Eq.trans
                      (Finset.sum_congr
                        ((fun x_0 x_1 x_2 x_3 a => (fun x_0 x_1 x_2 x_3 => Finset.inter_eq_right.mpr) x_0 x_1 x_2 x_3 a) ℕ
                          instDecidableEqNat (Finset.range (Fintype.card V)) (Finset.range (Fintype.card V))
                          (of_eq_true
                            (Eq.trans (subset_refl._simp_1 (Finset.range (Fintype.card V))) (eq_true True.intro))))
                        fun x a_1 => Eq.refl (if x ∈ Finset.range a then 1 else 0))
                      (Finset.sum_ite_mem (Finset.range (Fintype.card V)) (Finset.range a) fun i => 1))
                    (Eq.trans
                      (Eq.trans
                        (Finset.sum_congr
                          ((fun x_0 x_1 x_2 x_3 a => (fun x_0 x_1 x_2 x_3 => Finset.inter_eq_right.mpr) x_0 x_1 x_2 x_3 a)
                            ℕ instDecidableEqNat (Finset.range (Fintype.card V)) (Finset.range a)
                            (of_eq_true
                              (Eq.trans Finset.range_subset_range._simp_1
                                (Eq.trans (eq_true (LT.lt.le ha_lt)) (eq_true True.intro)))))
                          fun x a => Eq.refl 1)
                        (Finset.sum_const 1))
                      (Eq.trans (congrArg (fun x => x • 1) (Finset.card_range a)) (mul_one a))))))
              (eq_self a))
            (eq_true True.intro)))))D':PebbleDistribution Vh:1 ≤ D' ↑(R.symm ⟨a, ha_lt⟩)P:PebblePath (IsPebblingMove (SimpleGraph.completeGraph V)) D D'⊢ False
    cases P with
    | refl =>refine_2.reflV:Typeinst✝¹:DecidableEq Vinst✝:Fintype Va:ℕha:a ∈
  {n |
    ∀ (D : PebbleDistribution V),
      NumberOfPebbles D = n → ∀ (v : V), ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v}ha_lt:a < Fintype.card VR:↥Finset.univ ≃ Fin (Fintype.card V) := Finset.equivFinOfCardEq ⋯D:PebbleDistribution V := fun x => if ↑(R ⟨x, ⋯⟩) < a then 1 else 0hD:NumberOfPebbles D = a := 
  Eq.trans (Eq.symm (Finset.sum_attach Finset.univ D))
    (Eq.trans (Equiv.sum_comp R fun x => if ↑x < a then 1 else 0)
      (Eq.trans (Finset.sum_fin_eq_sum_range fun i => if ↑i < a then 1 else 0)
        (of_eq_true
          (Eq.trans
            (Eq.trans
              (congrArg (fun x => x = a)
                (Eq.trans
                  (Eq.trans
                    (Finset.sum_congr (Eq.refl (Finset.range (Fintype.card V))) fun x a_1 =>
                      dite_congr PebblingNumber_completeGraph._simp_1
                        (fun h => ite_congr PebblingNumber_completeGraph._simp_1 (fun a => Eq.refl 1) fun a => Eq.refl 0)
                        fun h => Eq.refl 0)
                    (Finset.sum_ite_mem (Finset.range (Fintype.card V)) (Finset.range (Fintype.card V)) fun i =>
                      if i ∈ Finset.range a then 1 else 0))
                  (Eq.trans
                    (Eq.trans
                      (Finset.sum_congr
                        ((fun x_0 x_1 x_2 x_3 a => (fun x_0 x_1 x_2 x_3 => Finset.inter_eq_right.mpr) x_0 x_1 x_2 x_3 a) ℕ
                          instDecidableEqNat (Finset.range (Fintype.card V)) (Finset.range (Fintype.card V))
                          (of_eq_true
                            (Eq.trans (subset_refl._simp_1 (Finset.range (Fintype.card V))) (eq_true True.intro))))
                        fun x a_1 => Eq.refl (if x ∈ Finset.range a then 1 else 0))
                      (Finset.sum_ite_mem (Finset.range (Fintype.card V)) (Finset.range a) fun i => 1))
                    (Eq.trans
                      (Eq.trans
                        (Finset.sum_congr
                          ((fun x_0 x_1 x_2 x_3 a => (fun x_0 x_1 x_2 x_3 => Finset.inter_eq_right.mpr) x_0 x_1 x_2 x_3 a)
                            ℕ instDecidableEqNat (Finset.range (Fintype.card V)) (Finset.range a)
                            (of_eq_true
                              (Eq.trans Finset.range_subset_range._simp_1
                                (Eq.trans (eq_true (LT.lt.le ha_lt)) (eq_true True.intro)))))
                          fun x a => Eq.refl 1)
                        (Finset.sum_const 1))
                      (Eq.trans (congrArg (fun x => x • 1) (Finset.card_range a)) (mul_one a))))))
              (eq_self a))
            (eq_true True.intro)))))h:1 ≤ D ↑(R.symm ⟨a, ha_lt⟩)⊢ False aesopAll goals completed! 🐙
    | step p h =>refine_2.stepV:Typeinst✝¹:DecidableEq Vinst✝:Fintype Va:ℕha:a ∈
  {n |
    ∀ (D : PebbleDistribution V),
      NumberOfPebbles D = n → ∀ (v : V), ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v}ha_lt:a < Fintype.card VR:↥Finset.univ ≃ Fin (Fintype.card V) := Finset.equivFinOfCardEq ⋯D:PebbleDistribution V := fun x => if ↑(R ⟨x, ⋯⟩) < a then 1 else 0hD:NumberOfPebbles D = a := 
  Eq.trans (Eq.symm (Finset.sum_attach Finset.univ D))
    (Eq.trans (Equiv.sum_comp R fun x => if ↑x < a then 1 else 0)
      (Eq.trans (Finset.sum_fin_eq_sum_range fun i => if ↑i < a then 1 else 0)
        (of_eq_true
          (Eq.trans
            (Eq.trans
              (congrArg (fun x => x = a)
                (Eq.trans
                  (Eq.trans
                    (Finset.sum_congr (Eq.refl (Finset.range (Fintype.card V))) fun x a_1 =>
                      dite_congr PebblingNumber_completeGraph._simp_1
                        (fun h => ite_congr PebblingNumber_completeGraph._simp_1 (fun a => Eq.refl 1) fun a => Eq.refl 0)
                        fun h => Eq.refl 0)
                    (Finset.sum_ite_mem (Finset.range (Fintype.card V)) (Finset.range (Fintype.card V)) fun i =>
                      if i ∈ Finset.range a then 1 else 0))
                  (Eq.trans
                    (Eq.trans
                      (Finset.sum_congr
                        ((fun x_0 x_1 x_2 x_3 a => (fun x_0 x_1 x_2 x_3 => Finset.inter_eq_right.mpr) x_0 x_1 x_2 x_3 a) ℕ
                          instDecidableEqNat (Finset.range (Fintype.card V)) (Finset.range (Fintype.card V))
                          (of_eq_true
                            (Eq.trans (subset_refl._simp_1 (Finset.range (Fintype.card V))) (eq_true True.intro))))
                        fun x a_1 => Eq.refl (if x ∈ Finset.range a then 1 else 0))
                      (Finset.sum_ite_mem (Finset.range (Fintype.card V)) (Finset.range a) fun i => 1))
                    (Eq.trans
                      (Eq.trans
                        (Finset.sum_congr
                          ((fun x_0 x_1 x_2 x_3 a => (fun x_0 x_1 x_2 x_3 => Finset.inter_eq_right.mpr) x_0 x_1 x_2 x_3 a)
                            ℕ instDecidableEqNat (Finset.range (Fintype.card V)) (Finset.range a)
                            (of_eq_true
                              (Eq.trans Finset.range_subset_range._simp_1
                                (Eq.trans (eq_true (LT.lt.le ha_lt)) (eq_true True.intro)))))
                          fun x a => Eq.refl 1)
                        (Finset.sum_const 1))
                      (Eq.trans (congrArg (fun x => x • 1) (Finset.card_range a)) (mul_one a))))))
              (eq_self a))
            (eq_true True.intro)))))D':PebbleDistribution Vh✝:1 ≤ D' ↑(R.symm ⟨a, ha_lt⟩)b✝:PebbleDistribution Vp:PebblePath (IsPebblingMove (SimpleGraph.completeGraph V)) D b✝h:IsPebblingMove (SimpleGraph.completeGraph V) b✝ D'⊢ False
      obtain ⟨v, _, h, _, _⟩ := hrefine_2.stepV:Typeinst✝¹:DecidableEq Vinst✝:Fintype Va:ℕha:a ∈
  {n |
    ∀ (D : PebbleDistribution V),
      NumberOfPebbles D = n → ∀ (v : V), ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v}ha_lt:a < Fintype.card VR:↥Finset.univ ≃ Fin (Fintype.card V) := Finset.equivFinOfCardEq ⋯D:PebbleDistribution V := fun x => if ↑(R ⟨x, ⋯⟩) < a then 1 else 0hD:NumberOfPebbles D = a := 
  Eq.trans (Eq.symm (Finset.sum_attach Finset.univ D))
    (Eq.trans (Equiv.sum_comp R fun x => if ↑x < a then 1 else 0)
      (Eq.trans (Finset.sum_fin_eq_sum_range fun i => if ↑i < a then 1 else 0)
        (of_eq_true
          (Eq.trans
            (Eq.trans
              (congrArg (fun x => x = a)
                (Eq.trans
                  (Eq.trans
                    (Finset.sum_congr (Eq.refl (Finset.range (Fintype.card V))) fun x a_1 =>
                      dite_congr PebblingNumber_completeGraph._simp_1
                        (fun h => ite_congr PebblingNumber_completeGraph._simp_1 (fun a => Eq.refl 1) fun a => Eq.refl 0)
                        fun h => Eq.refl 0)
                    (Finset.sum_ite_mem (Finset.range (Fintype.card V)) (Finset.range (Fintype.card V)) fun i =>
                      if i ∈ Finset.range a then 1 else 0))
                  (Eq.trans
                    (Eq.trans
                      (Finset.sum_congr
                        ((fun x_0 x_1 x_2 x_3 a => (fun x_0 x_1 x_2 x_3 => Finset.inter_eq_right.mpr) x_0 x_1 x_2 x_3 a) ℕ
                          instDecidableEqNat (Finset.range (Fintype.card V)) (Finset.range (Fintype.card V))
                          (of_eq_true
                            (Eq.trans (subset_refl._simp_1 (Finset.range (Fintype.card V))) (eq_true True.intro))))
                        fun x a_1 => Eq.refl (if x ∈ Finset.range a then 1 else 0))
                      (Finset.sum_ite_mem (Finset.range (Fintype.card V)) (Finset.range a) fun i => 1))
                    (Eq.trans
                      (Eq.trans
                        (Finset.sum_congr
                          ((fun x_0 x_1 x_2 x_3 a => (fun x_0 x_1 x_2 x_3 => Finset.inter_eq_right.mpr) x_0 x_1 x_2 x_3 a)
                            ℕ instDecidableEqNat (Finset.range (Fintype.card V)) (Finset.range a)
                            (of_eq_true
                              (Eq.trans Finset.range_subset_range._simp_1
                                (Eq.trans (eq_true (LT.lt.le ha_lt)) (eq_true True.intro)))))
                          fun x a => Eq.refl 1)
                        (Finset.sum_const 1))
                      (Eq.trans (congrArg (fun x => x • 1) (Finset.card_range a)) (mul_one a))))))
              (eq_self a))
            (eq_true True.intro)))))D':PebbleDistribution Vh✝:1 ≤ D' ↑(R.symm ⟨a, ha_lt⟩)b✝:PebbleDistribution Vp:PebblePath (IsPebblingMove (SimpleGraph.completeGraph V)) D b✝v:Vw✝:Vh:b✝ v ≥ 2left✝:(SimpleGraph.completeGraph V).Adj v w✝right✝:D' = fun u => if u = w✝ then b✝ u + 1 else if u = v then b✝ u - 2 else b✝ u⊢ False
      exact absurd h (p.rec (byV:Typeinst✝¹:DecidableEq Vinst✝:Fintype Va:ℕha:a ∈
  {n |
    ∀ (D : PebbleDistribution V),
      NumberOfPebbles D = n → ∀ (v : V), ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v}ha_lt:a < Fintype.card VR:↥Finset.univ ≃ Fin (Fintype.card V) := Finset.equivFinOfCardEq ⋯D:PebbleDistribution V := fun x => if ↑(R ⟨x, ⋯⟩) < a then 1 else 0hD:NumberOfPebbles D = a := 
  Eq.trans (Eq.symm (Finset.sum_attach Finset.univ D))
    (Eq.trans (Equiv.sum_comp R fun x => if ↑x < a then 1 else 0)
      (Eq.trans (Finset.sum_fin_eq_sum_range fun i => if ↑i < a then 1 else 0)
        (of_eq_true
          (Eq.trans
            (Eq.trans
              (congrArg (fun x => x = a)
                (Eq.trans
                  (Eq.trans
                    (Finset.sum_congr (Eq.refl (Finset.range (Fintype.card V))) fun x a_1 =>
                      dite_congr PebblingNumber_completeGraph._simp_1
                        (fun h => ite_congr PebblingNumber_completeGraph._simp_1 (fun a => Eq.refl 1) fun a => Eq.refl 0)
                        fun h => Eq.refl 0)
                    (Finset.sum_ite_mem (Finset.range (Fintype.card V)) (Finset.range (Fintype.card V)) fun i =>
                      if i ∈ Finset.range a then 1 else 0))
                  (Eq.trans
                    (Eq.trans
                      (Finset.sum_congr
                        ((fun x_0 x_1 x_2 x_3 a => (fun x_0 x_1 x_2 x_3 => Finset.inter_eq_right.mpr) x_0 x_1 x_2 x_3 a) ℕ
                          instDecidableEqNat (Finset.range (Fintype.card V)) (Finset.range (Fintype.card V))
                          (of_eq_true
                            (Eq.trans (subset_refl._simp_1 (Finset.range (Fintype.card V))) (eq_true True.intro))))
                        fun x a_1 => Eq.refl (if x ∈ Finset.range a then 1 else 0))
                      (Finset.sum_ite_mem (Finset.range (Fintype.card V)) (Finset.range a) fun i => 1))
                    (Eq.trans
                      (Eq.trans
                        (Finset.sum_congr
                          ((fun x_0 x_1 x_2 x_3 a => (fun x_0 x_1 x_2 x_3 => Finset.inter_eq_right.mpr) x_0 x_1 x_2 x_3 a)
                            ℕ instDecidableEqNat (Finset.range (Fintype.card V)) (Finset.range a)
                            (of_eq_true
                              (Eq.trans Finset.range_subset_range._simp_1
                                (Eq.trans (eq_true (LT.lt.le ha_lt)) (eq_true True.intro)))))
                          fun x a => Eq.refl 1)
                        (Finset.sum_const 1))
                      (Eq.trans (congrArg (fun x => x • 1) (Finset.card_range a)) (mul_one a))))))
              (eq_self a))
            (eq_true True.intro)))))D':PebbleDistribution Vh✝:1 ≤ D' ↑(R.symm ⟨a, ha_lt⟩)b✝:PebbleDistribution Vp:PebblePath (IsPebblingMove (SimpleGraph.completeGraph V)) D b✝v:Vw✝:Vh:b✝ v ≥ 2left✝:(SimpleGraph.completeGraph V).Adj v w✝right✝:D' = fun u => if u = w✝ then b✝ u + 1 else if u = v then b✝ u - 2 else b✝ u⊢ ∀ (x : V), ¬D x ≥ 2 aesopAll goals completed! 🐙) (byV:Typeinst✝¹:DecidableEq Vinst✝:Fintype Va:ℕha:a ∈
  {n |
    ∀ (D : PebbleDistribution V),
      NumberOfPebbles D = n → ∀ (v : V), ∃ D', IsReachable (SimpleGraph.completeGraph V) D D' ∧ 1 ≤ D' v}ha_lt:a < Fintype.card VR:↥Finset.univ ≃ Fin (Fintype.card V) := Finset.equivFinOfCardEq ⋯D:PebbleDistribution V := fun x => if ↑(R ⟨x, ⋯⟩) < a then 1 else 0hD:NumberOfPebbles D = a := 
  Eq.trans (Eq.symm (Finset.sum_attach Finset.univ D))
    (Eq.trans (Equiv.sum_comp R fun x => if ↑x < a then 1 else 0)
      (Eq.trans (Finset.sum_fin_eq_sum_range fun i => if ↑i < a then 1 else 0)
        (of_eq_true
          (Eq.trans
            (Eq.trans
              (congrArg (fun x => x = a)
                (Eq.trans
                  (Eq.trans
                    (Finset.sum_congr (Eq.refl (Finset.range (Fintype.card V))) fun x a_1 =>
                      dite_congr PebblingNumber_completeGraph._simp_1
                        (fun h => ite_congr PebblingNumber_completeGraph._simp_1 (fun a => Eq.refl 1) fun a => Eq.refl 0)
                        fun h => Eq.refl 0)
                    (Finset.sum_ite_mem (Finset.range (Fintype.card V)) (Finset.range (Fintype.card V)) fun i =>
                      if i ∈ Finset.range a then 1 else 0))
                  (Eq.trans
                    (Eq.trans
                      (Finset.sum_congr
                        ((fun x_0 x_1 x_2 x_3 a => (fun x_0 x_1 x_2 x_3 => Finset.inter_eq_right.mpr) x_0 x_1 x_2 x_3 a) ℕ
                          instDecidableEqNat (Finset.range (Fintype.card V)) (Finset.range (Fintype.card V))
                          (of_eq_true
                            (Eq.trans (subset_refl._simp_1 (Finset.range (Fintype.card V))) (eq_true True.intro))))
                        fun x a_1 => Eq.refl (if x ∈ Finset.range a then 1 else 0))
                      (Finset.sum_ite_mem (Finset.range (Fintype.card V)) (Finset.range a) fun i => 1))
                    (Eq.trans
                      (Eq.trans
                        (Finset.sum_congr
                          ((fun x_0 x_1 x_2 x_3 a => (fun x_0 x_1 x_2 x_3 => Finset.inter_eq_right.mpr) x_0 x_1 x_2 x_3 a)
                            ℕ instDecidableEqNat (Finset.range (Fintype.card V)) (Finset.range a)
                            (of_eq_true
                              (Eq.trans Finset.range_subset_range._simp_1
                                (Eq.trans (eq_true (LT.lt.le ha_lt)) (eq_true True.intro)))))
                          fun x a => Eq.refl 1)
                        (Finset.sum_const 1))
                      (Eq.trans (congrArg (fun x => x • 1) (Finset.card_range a)) (mul_one a))))))
              (eq_self a))
            (eq_true True.intro)))))D':PebbleDistribution Vh✝:1 ≤ D' ↑(R.symm ⟨a, ha_lt⟩)b✝:PebbleDistribution Vp:PebblePath (IsPebblingMove (SimpleGraph.completeGraph V)) D b✝v:Vw✝:Vh:b✝ v ≥ 2left✝:(SimpleGraph.completeGraph V).Adj v w✝right✝:D' = fun u => if u = w✝ then b✝ u + 1 else if u = v then b✝ u - 2 else b✝ u⊢ ∀ {b c : PebbleDistribution V} (p : PebblePath (IsPebblingMove (SimpleGraph.completeGraph V)) D b),
  IsPebblingMove (SimpleGraph.completeGraph V) b c → (∀ (x : V), ¬b x ≥ 2) → ∀ (x : V), ¬c x ≥ 2 simp_all only [IsReachable, IsPebblingMove]V:Typeinst✝¹:DecidableEq Vinst✝:Fintype Va:ℕha_lt:a < Fintype.card VR:↥Finset.univ ≃ Fin (Fintype.card V) := Finset.equivFinOfCardEq ⋯D:PebbleDistribution V := fun x => if ↑(R ⟨x, ⋯⟩) < a then 1 else 0D':PebbleDistribution Vb✝:PebbleDistribution Vp:PebblePath (IsPebblingMove (SimpleGraph.completeGraph V)) D b✝v:Vw✝:Vha:a ∈
  {n |
    ∀ (D : PebbleDistribution V),
      NumberOfPebbles D = n →
        ∀ (v : V), ∃ D', ExistsPebblePath (IsPebblingMove (SimpleGraph.completeGraph V)) D D' ∧ 1 ≤ D' v}hD:NumberOfPebbles D = ah✝:1 ≤
  if ↑(R.symm ⟨a, ha_lt⟩) = w✝ then b✝ w✝ + 1
  else if ↑(R.symm ⟨a, ha_lt⟩) = v then b✝ v - 2 else b✝ ↑(R.symm ⟨a, ha_lt⟩)h:b✝ v ≥ 2left✝:(SimpleGraph.completeGraph V).Adj v w✝right✝:D' = fun u => if u = w✝ then b✝ w✝ + 1 else if u = v then b✝ v - 2 else b✝ u⊢ ∀ {b c : PebbleDistribution V} (p : PebblePath (IsPebblingMove (SimpleGraph.completeGraph V)) D b),
  (∃ v w,
      b v ≥ 2 ∧
        (SimpleGraph.completeGraph V).Adj v w ∧
          c = fun u => if u = w then b w + 1 else if u = v then b v - 2 else b u) →
    (∀ (x : V), ¬b x ≥ 2) → ∀ (x : V), ¬c x ≥ 2; aesopAll goals completed! 🐙) v)

The pebbling number conjecture: the pebbling number of a Cartesian product of connected graphs is at most equal to the product of the pebbling numbers of the factors. See Asplund, Hurlbert, and Kenter.

@[category research open, AMS 5]
theorem declaration uses 'sorry'pebbling_number_conjecture {W : Type} [Fintype V] [Fintype W] [DecidableEq W]
    (G : SimpleGraph V) (H : SimpleGraph W) (hG : G.Connected) (hH : H.Connected) :
    PebblingNumber (G □ H) ≤ PebblingNumber G * PebblingNumber H := byV:Typeinst✝³:DecidableEq VW:Typeinst✝²:Fintype Vinst✝¹:Fintype Winst✝:DecidableEq WG:SimpleGraph VH:SimpleGraph WhG:G.ConnectedhH:H.Connected⊢ PebblingNumber (G □ H) ≤ PebblingNumber G * PebblingNumber H
  sorryAll goals completed! 🐙


end PebblingNumberConjecture