FormalConjecturesForMathlib.Combinatorics.SimpleGraph.WienerIndex

/-
Copyright 2026 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.
-/
module

public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.VertexDistance

@[expose] public sectionnamespace SimpleGraphvariable {α : Type*} [Fintype α] [DecidableEq α]

The Wiener index of G, which is the sum of distances between all pairs of vertices.

noncomputable def wienerIndex (G : SimpleGraph α) : ℕ :=
  ∑ uv : Sym2 α, uv.lift ⟨fun u v ↦ G.dist u v, byα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αG:SimpleGraph αuv:Sym2 α⊢ ∀ (a₁ a₂ : α), (fun u v ↦ G.dist u v) a₁ a₂ = (fun u v ↦ G.dist u v) a₂ a₁ simp [dist_comm]All goals completed! 🐙⟩

Computable Wiener index: half the sum of all ordered pairwise distances.

def computable_wiener (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
  (∑ u ∈ Finset.univ, ∑ v ∈ Finset.univ, computable_dist G u v) / 2




-- Helper: ∑∑ f = 2 * ∑ Sym2 (lift f) when f symmetric with f(a,a) = 0
private lemma double_sum_eq_two_mul_sym2_sum {f : α → α → ℕ}
    (hf : ∀ a b, f a b = f b a) (hd : ∀ a, f a a = 0) :
    ∑ u : α, ∑ v : α, f u v =
    2 * ∑ x : Sym2 α, Sym2.lift ⟨f, fun a b => hf a b⟩ x := byα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0⊢ ∑ u, ∑ v, f u v = 2 * ∑ x, Sym2.lift ⟨f, ⋯⟩ x
  -- Use fiberwise decomposition over Sym2 quotient map
  have h_fiber := Fintype.sum_fiberwise
    (fun (p : α × α) => s(p.1, p.2))
    (fun (p : α × α) => f p.1 p.2)α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ u, ∑ v, f u v = 2 * ∑ x, Sym2.lift ⟨f, ⋯⟩ x
  -- h_fiber : ∑ q : Sym2 α, ∑ p : {p // Sym2.mk p = q}, f (↑p).1 (↑p).2
  --         = ∑ p : α × α, f p.1 p.2
  -- RHS = ∑ u, ∑ v, f u v (by Finset.sum_product')
  -- LHS = ∑ q, (fiber sum) = ∑ q, 2 * lift f q = 2 * ∑ q, lift f q
  -- So: ∑ u, ∑ v, f u v = 2 * ∑ q, lift f q
  rw [show (∑ u : α, ∑ v : α, f u v) = ∑ p : α × α, f p.1 p.2 from byα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ u, ∑ v, f u v = ∑ p, f p.1 p.2α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ p, f p.1 p.2 = 2 * ∑ x, Sym2.lift ⟨f, ⋯⟩ x
    rw [← Finset.univ_product_univ,α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ u, ∑ v, f u v = ∑ p ∈ Finset.univ ×ˢ Finset.univ, f p.1 p.2All goals completed! 🐙α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ p, f p.1 p.2 = 2 * ∑ x, Sym2.lift ⟨f, ⋯⟩ x Finset.sum_product'α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ u, ∑ v, f u v = ∑ x, ∑ y, f x yAll goals completed! 🐙α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ p, f p.1 p.2 = 2 * ∑ x, Sym2.lift ⟨f, ⋯⟩ x]All goals completed! 🐙α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ p, f p.1 p.2 = 2 * ∑ x, Sym2.lift ⟨f, ⋯⟩ x]α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ p, f p.1 p.2 = 2 * ∑ x, Sym2.lift ⟨f, ⋯⟩ x
  rw [← h_fiber,α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ j, ∑ i, f (↑i).1 (↑i).2 = 2 * ∑ x, Sym2.lift ⟨f, ⋯⟩ xα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, 2 * Sym2.lift ⟨f, ⋯⟩ i Finset.mul_sumα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, 2 * Sym2.lift ⟨f, ⋯⟩ iα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, 2 * Sym2.lift ⟨f, ⋯⟩ i]α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, 2 * Sym2.lift ⟨f, ⋯⟩ i
  apply Finset.sum_congr rflα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2⊢ ∀ x ∈ Finset.univ, ∑ i, f (↑i).1 (↑i).2 = 2 * Sym2.lift ⟨f, ⋯⟩ x
  intro q _α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univ⊢ ∑ i, f (↑i).1 (↑i).2 = 2 * Sym2.lift ⟨f, ⋯⟩ q
  -- For each q : Sym2 α, show fiber sum = 2 * lift f q
  refine Sym2.ind (fun a b => ?_) qα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:α⊢ ∑ i, f (↑i).1 (↑i).2 = 2 * Sym2.lift ⟨f, ⋯⟩ s(a, b)
  simp only [Sym2.lift_mk]α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:α⊢ ∑ i, f (↑i).1 (↑i).2 = 2 * f a b
  -- Need: ∑ (p : {p : α × α // Sym2.mk p = s(a, b)}), f (↑p).1 (↑p).2 = 2 * f a b
  -- Convert subtype sum to filter sum
  rw [← Finset.sum_subtype (Finset.univ.filter (fun p : α × α => s(p.1, p.2) = s(a, b)))
    (fun x => byα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αx:α × α⊢ x ∈ {p | s(p.1, p.2) = s(a, b)} ↔ s(x.1, x.2) = s(a, b)α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:α⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b simp [Finset.mem_filter]All goals completed! 🐙α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:α⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b) (fun p => f p.1 p.2)]α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:α⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b
  -- Characterize the filter: Sym2.mk (x,y) = s(a,b) ↔ (x,y) = (a,b) ∨ (x,y) = (b,a)
  have h_filter : Finset.univ.filter (fun p : α × α => s(p.1, p.2) = s(a, b)) =
      {(a, b), (b, a)} := byα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0⊢ ∑ u, ∑ v, f u v = 2 * ∑ x, Sym2.lift ⟨f, ⋯⟩ xα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b
    ext ⟨x, y⟩α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αx:αy:α⊢ (x, y) ∈ {p | s(p.1, p.2) = s(a, b)} ↔ (x, y) ∈ {(a, b), (b, a)}α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b
    simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_insert,
      Finset.mem_singleton, Prod.mk.injEq]α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αx:αy:α⊢ s(x, y) = s(a, b) ↔ x = a ∧ y = b ∨ x = b ∧ y = aα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b
    constructormpα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αx:αy:α⊢ s(x, y) = s(a, b) → x = a ∧ y = b ∨ x = b ∧ y = amprα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αx:αy:α⊢ x = a ∧ y = b ∨ x = b ∧ y = a → s(x, y) = s(a, b)α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b
    ·mpα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αx:αy:α⊢ s(x, y) = s(a, b) → x = a ∧ y = b ∨ x = b ∧ y = aα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b intro hmpα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αx:αy:αh:s(x, y) = s(a, b)⊢ x = a ∧ y = b ∨ x = b ∧ y = aα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b
      rw [Sym2.eqmpα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αx:αy:αh:Sym2.Rel α (x, y) (a, b)⊢ x = a ∧ y = b ∨ x = b ∧ y = ampα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αx:αy:αh:Sym2.Rel α (x, y) (a, b)⊢ x = a ∧ y = b ∨ x = b ∧ y = aα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b] at hmpα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αx:αy:αh:Sym2.Rel α (x, y) (a, b)⊢ x = a ∧ y = b ∨ x = b ∧ y = aα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b
      cases h with
      | refl =>mp.reflα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:α⊢ a = a ∧ b = b ∨ a = b ∧ b = aα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b leftmp.reflα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:α⊢ a = a ∧ b = bα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b; exact ⟨rfl, rfl⟩All goals completed! 🐙α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b
      | swap =>mp.swapα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:α⊢ b = a ∧ a = b ∨ b = b ∧ a = aα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b rightmp.swapα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:α⊢ b = b ∧ a = aα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b; exact ⟨rfl, rfl⟩All goals completed! 🐙α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b
    ·mprα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αx:αy:α⊢ x = a ∧ y = b ∨ x = b ∧ y = a → s(x, y) = s(a, b)α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)mpr.inlα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univx:αy:α⊢ s(x, y) = s(x, y)mpr.inrα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univx:αy:α⊢ s(x, y) = s(y, x)α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b
      ·mpr.inlα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univx:αy:α⊢ s(x, y) = s(x, y)α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b rflAll goals completed! 🐙α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b
      ·mpr.inrα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univx:αy:α⊢ s(x, y) = s(y, x)α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b exact Sym2.sound (.swap _ _)α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a bα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a with s(a.1, a.2) = s(a, b), f a.1 a.2 = 2 * f a b
  rw [h_filterα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a ∈ {(a, b), (b, a)}, f a.1 a.2 = 2 * f a bα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a ∈ {(a, b), (b, a)}, f a.1 a.2 = 2 * f a b]α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}⊢ ∑ a ∈ {(a, b), (b, a)}, f a.1 a.2 = 2 * f a b
  by_cases hab : a = bposα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}hab:a = b⊢ ∑ a ∈ {(a, b), (b, a)}, f a.1 a.2 = 2 * f a bnegα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}hab:¬a = b⊢ ∑ a ∈ {(a, b), (b, a)}, f a.1 a.2 = 2 * f a b
  ·posα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}hab:a = b⊢ ∑ a ∈ {(a, b), (b, a)}, f a.1 a.2 = 2 * f a b subst habposα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αh_filter:{p | s(p.1, p.2) = s(a, a)} = {(a, a), (a, a)}⊢ ∑ a ∈ {(a, a), (a, a)}, f a.1 a.2 = 2 * f a a; simp [hd]All goals completed! 🐙
  ·negα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}hab:¬a = b⊢ ∑ a ∈ {(a, b), (b, a)}, f a.1 a.2 = 2 * f a b rw [Finset.sum_pair (show (a, b) ≠ (b, a) byα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0⊢ ∑ u, ∑ v, f u v = 2 * ∑ x, Sym2.lift ⟨f, ⋯⟩ xnegα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}hab:¬a = b⊢ f (a, b).1 (a, b).2 + f (b, a).1 (b, a).2 = 2 * f a b simp [hab]All goals completed! 🐙negα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}hab:¬a = b⊢ f (a, b).1 (a, b).2 + f (b, a).1 (b, a).2 = 2 * f a b)]negα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}hab:¬a = b⊢ f (a, b).1 (a, b).2 + f (b, a).1 (b, a).2 = 2 * f a b
    rw [hf b anegα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}hab:¬a = b⊢ f (a, b).1 (a, b).2 + f a b = 2 * f a bnegα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}hab:¬a = b⊢ f (a, b).1 (a, b).2 + f a b = 2 * f a b]negα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αf:α → α → ℕhf:∀ (a b : α), f a b = f b ahd:∀ (a : α), f a a = 0h_fiber:∑ j, ∑ i, f (↑i).1 (↑i).2 = ∑ i, f i.1 i.2q:Sym2 αa✝:q ∈ Finset.univa:αb:αh_filter:{p | s(p.1, p.2) = s(a, b)} = {(a, b), (b, a)}hab:¬a = b⊢ f (a, b).1 (a, b).2 + f a b = 2 * f a b; ringAll goals completed! 🐙




theorem wiener_eq_computable (G : SimpleGraph α) [DecidableRel G.Adj] :
    wienerIndex G = computable_wiener G := byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ G.wienerIndex = G.computable_wiener
  unfold wienerIndex computable_wienerα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2
  -- Goal: ∑ uv, Sym2.lift ⟨dist, _⟩ uv = (∑ u, ∑ v, computable_dist u v) / 2
  have hcomm : ∀ a b, computable_dist G a b = computable_dist G b a := byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ G.wienerIndex = G.computable_wienerα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b a⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2
    intro a bα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adja:αb:α⊢ G.computable_dist a b = G.computable_dist b aα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b a⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2; rw [← dist_eq_computable,α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adja:αb:α⊢ G.dist a b = G.computable_dist b aα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b a⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2 ← dist_eq_computable,α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adja:αb:α⊢ G.dist a b = G.dist b aα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b a⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2 dist_commα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adja:αb:α⊢ G.dist b a = G.dist b aα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b a⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2]α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b a⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b a⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2
  have hdiag : ∀ a, computable_dist G a a = 0 := byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ G.wienerIndex = G.computable_wienerα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2
    intro aα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b aa:α⊢ G.computable_dist a a = 0α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2; rw [← dist_eq_computableα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b aa:α⊢ G.dist a a = 0α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b aa:α⊢ G.dist a a = 0α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2]α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b aa:α⊢ G.dist a a = 0α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2; simpα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2
  -- Sum over Sym2 using dist = sum over Sym2 using computable_dist
  have h_sum : (∑ uv : Sym2 α, Sym2.lift ⟨fun u v ↦ G.dist u v,
      byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0uv:Sym2 α⊢ ∀ (a₁ a₂ : α), (fun u v ↦ G.dist u v) a₁ a₂ = (fun u v ↦ G.dist u v) a₂ a₁α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2 intro a bα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0uv:Sym2 αa:αb:α⊢ (fun u v ↦ G.dist u v) a b = (fun u v ↦ G.dist u v) b aα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2; simp [dist_comm]All goals completed! 🐙α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2⟩ uv) =
      ∑ uv : Sym2 α, Sym2.lift ⟨fun u v ↦ computable_dist G u v,
      fun a b => hcomm a b⟩ uv := byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ G.wienerIndex = G.computable_wienerα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2
    apply Finset.sum_congr rflα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0⊢ ∀ x ∈ Finset.univ, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ x = Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ xα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2; intro x _α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0x:Sym2 αa✝:x ∈ Finset.univ⊢ Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ x = Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ xα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2
    refine Sym2.ind (fun a b => ?_) xα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0x:Sym2 αa✝:x ∈ Finset.univa:αb:α⊢ Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ s(a, b) = Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ s(a, b)α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2
    simp only [Sym2.lift_mk, dist_eq_computable]α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2
  rw [h_sumα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2]α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2
  have h2 := double_sum_eq_two_mul_sym2_sum hcomm hdiagα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uvh2:∑ u, ∑ v, G.computable_dist u v = 2 * ∑ x, Sym2.lift ⟨G.computable_dist, ⋯⟩ x⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv = (∑ u, ∑ v, G.computable_dist u v) / 2
  -- h2 : ∑∑ f = 2 * ∑ Sym2 lift f
  -- goal: ∑ Sym2 lift f = ∑∑ f / 2
  rw [h2,α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uvh2:∑ u, ∑ v, G.computable_dist u v = 2 * ∑ x, Sym2.lift ⟨G.computable_dist, ⋯⟩ x⊢ ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uv = (2 * ∑ x, Sym2.lift ⟨G.computable_dist, ⋯⟩ x) / 2All goals completed! 🐙 Nat.mul_div_cancel_left _ (byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhcomm:∀ (a b : α), G.computable_dist a b = G.computable_dist b ahdiag:∀ (a : α), G.computable_dist a a = 0h_sum:∑ uv, Sym2.lift ⟨fun u v ↦ G.dist u v, ⋯⟩ uv = ∑ uv, Sym2.lift ⟨fun u v ↦ G.computable_dist u v, ⋯⟩ uvh2:∑ u, ∑ v, G.computable_dist u v = 2 * ∑ x, Sym2.lift ⟨G.computable_dist, ⋯⟩ x⊢ 0 < 2All goals completed! 🐙 omegaAll goals completed! 🐙All goals completed! 🐙 : 0 < 2)]All goals completed! 🐙

end SimpleGraph