1. FormalConjectures
  2. ErdosProblems
  3. «742»
/- 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. -/ import FormalConjecturesUtil

Erdős Problem 742

References:

    erdosproblems.com/742

    [Pl75] Plesník, Ján, Critical graphs of given diameter. Acta Fac. Rerum Natur. Univ. Comenian. Math. 30 (1975), 71-93.

    [CaHa79] Caccetta, L. and Häggkvist, R., On diameter critical graphs. Discrete Math. 28 (1979), 223-229.

    [Fa87] Fan, Genghua, On diameter 2-critical graphs. Discrete Math. 67 (1987), 235-240.

    [Fü92] Füredi, Zoltán, The maximum number of edges in a minimal graph of diameter 2. J. Graph Theory 16 (1992), 81-98.

open SimpleGraph namespace Erdos742 variable {V : Type*} [Fintype V] [DecidableEq V]

A graph is diameter-2-critical if it has diameter $2$ and removing any edge increases the diameter beyond $2$.

def IsDiameter2Critical (G : SimpleGraph V) : Prop := G.diam = 2 ∧ ∀ e ∈ G.edgeSet, (G.deleteEdges {e}).diam ≠ 2

Murty-Simon Conjecture

Let $G$ be a graph on $n$ vertices with diameter $2$ such that deleting any edge increases the diameter. Is it true that $G$ has at most $\lfloor n^2 / 4 \rfloor$ edges? Equality is conjectured to hold for the complete balanced bipartite graph $K_{\lceil n/2 \rceil, \lfloor n/2 \rfloor}$.

The conjecture is resolved up to a finite check: Fan [Fa87] verified it for $n \leq 24$ and $n = 26$, and Füredi [Fü92] proved it for all sufficiently large $n$.

@[category research open, AMS 5] theorem declaration uses 'sorry'erdos_742 : answer(sorry) ↔ ∀ (V : Type*) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], IsDiameter2Critical G → G.edgeFinset.card ≤ (Fintype.card V) ^ 2 / 4 := ⊢ True ↔ ∀ (V : Type u_2) [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], IsDiameter2Critical G → G.edgeFinset.card ≤ Fintype.card V ^ 2 / 4 All goals completed! 🐙

The complete bipartite graph $K_{a, b}$ has exactly $a \cdot b$ edges. The bound $\lfloor n^2 / 4 \rfloor$ in the Murty-Simon conjecture is attained by the balanced case $K_{\lceil n/2 \rceil, \lfloor n/2 \rfloor}$.

@[category test, AMS 5] theorem complete_bipartite_edge_count (a b : ℕ) : (completeBipartiteGraph (Fin a) (Fin b)).edgeSet.ncard = a * b := a:ℕb:ℕ⊢ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet.ncard = a * b -- The edge set equals the image of `Fin a × Fin b` under the map -- `(i, j) ↦ s(Sum.inl i, Sum.inr j)`. a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)⊢ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet.ncard = a * b have hedge : (completeBipartiteGraph (Fin a) (Fin b)).edgeSet = φ '' Set.univ := a:ℕb:ℕ⊢ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet.ncard = a * b a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)e:Sym2 (Fin a ⊕ Fin b)⊢ e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet ↔ e ∈ φ '' Set.univ a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)e:Sym2 (Fin a ⊕ Fin b)⊢ e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet ↔ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = e a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)e:Sym2 (Fin a ⊕ Fin b)⊢ e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = ea:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)e:Sym2 (Fin a ⊕ Fin b)⊢ (∃ x, s(Sum.inl x.1, Sum.inr x.2) = e) → e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)e:Sym2 (Fin a ⊕ Fin b)⊢ e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = e a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)e:Sym2 (Fin a ⊕ Fin b)hadj:e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = e a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)a✝:(Fin a ⊕ Fin b) × (Fin a ⊕ Fin b)hadj:Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) a✝ ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) a✝ a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)p:(Fin a ⊕ Fin b) × (Fin a ⊕ Fin b)hadj:Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) a✝ ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) a✝ cases p with a✝:ℕb✝:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)a:Fin a✝ ⊕ Fin b✝b:Fin a✝ ⊕ Fin b✝hadj:Quot.mk (Sym2.Rel (Fin a✝ ⊕ Fin b✝)) (a, b) ∈ (completeBipartiteGraph (Fin a✝) (Fin b✝)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a✝ ⊕ Fin b✝)) (a, b) a:ℕb✝:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)b:Fin a✝ ⊕ Fin b✝val✝:Fin ahadj:Quot.mk (Sym2.Rel (Fin a ⊕ Fin b✝)) (Sum.inl val✝, b) ∈ (completeBipartiteGraph (Fin a) (Fin b✝)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b✝)) (Sum.inl val✝, b)a:ℕb✝:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)b:Fin a✝ ⊕ Fin b✝val✝:Fin b✝hadj:Quot.mk (Sym2.Rel (Fin a ⊕ Fin b✝)) (Sum.inr val✝, b) ∈ (completeBipartiteGraph (Fin a) (Fin b✝)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b✝)) (Sum.inr val✝, b) a:ℕb✝:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)b:Fin a✝ ⊕ Fin b✝val✝:Fin ahadj:Quot.mk (Sym2.Rel (Fin a ⊕ Fin b✝)) (Sum.inl val✝, b) ∈ (completeBipartiteGraph (Fin a) (Fin b✝)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b✝)) (Sum.inl val✝, b)a:ℕb✝:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)b:Fin a✝ ⊕ Fin b✝val✝:Fin b✝hadj:Quot.mk (Sym2.Rel (Fin a ⊕ Fin b✝)) (Sum.inr val✝, b) ∈ (completeBipartiteGraph (Fin a) (Fin b✝)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b✝)) (Sum.inr val✝, b) a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)val✝¹:Fin b✝val✝:Fin ahadj:Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val✝¹, Sum.inl val✝) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val✝¹, Sum.inl val✝)a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)val✝¹:Fin b✝val✝:Fin bhadj:Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val✝¹, Sum.inr val✝) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val✝¹, Sum.inr val✝) a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)val✝¹:Fin aval✝:Fin ahadj:Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val✝¹, Sum.inl val✝) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val✝¹, Sum.inl val✝)a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)val✝¹:Fin aval✝:Fin bhadj:Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val✝¹, Sum.inr val✝) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val✝¹, Sum.inr val✝)a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)val✝¹:Fin b✝val✝:Fin ahadj:Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val✝¹, Sum.inl val✝) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val✝¹, Sum.inl val✝)a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)val✝¹:Fin b✝val✝:Fin bhadj:Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val✝¹, Sum.inr val✝) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet⊢ ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val✝¹, Sum.inr val✝) All goals completed! 🐙 a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)e:Sym2 (Fin a ⊕ Fin b)⊢ (∃ x, s(Sum.inl x.1, Sum.inr x.2) = e) → e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)i:Fin aj:Fin b⊢ s(Sum.inl (i, j).1, Sum.inr (i, j).2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet All goals completed! 🐙 have hinj : Function.Injective φ := a:ℕb:ℕ⊢ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet.ncard = a * b intro ⟨i₁, j₁⟩ a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)hedge:(completeBipartiteGraph (Fin a) (Fin b)).edgeSet = φ '' Set.univ := Set.ext fun e => Eq.mpr (id (congrArg (Iff (e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet)) (Eq.trans (Eq.trans (congrArg (fun x => e ∈ x) (Set.image_congr fun a_1 a_2 => Eq.refl s(Sum.inl a_1.1, Sum.inr a_1.2))) (complete_bipartite_edge_count._simp_1 (fun a_1 => s(Sum.inl a_1.1, Sum.inr a_1.2)) Set.univ e)) (congrArg Exists (funext fun x => Eq.trans (congrArg (fun x_1 => x_1 ∧ s(Sum.inl x.1, Sum.inr x.2) = e) (complete_bipartite_edge_count._simp_2 x)) (true_and (s(Sum.inl x.1, Sum.inr x.2) = e))))))) { mp := fun hadj => Quot.ind (fun a_1 hadj => Prod.casesOn (motive := fun t => a_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) a_1) a_1 (fun a_2 b_1 h => Eq.ndrec (motive := fun p => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p) (fun hadj => Sum.casesOn (motive := fun t => a_2 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_2, b_1)) a_2 (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (or_self False))) hadj)) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val) (Sum.inr val_1)) (congr (congrArg And (Sum.inl.injEq x.1 val)) (Sum.inr.injEq x.2 val_1)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val_1) (Sum.inl val)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (or_false (x.1 = val ∧ x.2 = val_1)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val) (Sum.inl val_1)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val_1) (Sum.inr val)) (congr (congrArg And (Sum.inl.injEq x.1 val_1)) (Sum.inr.injEq x.2 val)))) (false_or (x.1 = val_1 ∧ x.2 = val)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (or_self False))) hadj)) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (Eq.refl a_2)) (Eq.symm h) hadj) (Eq.refl a_1)) e hadj, mpr := fun a_1 => Exists.casesOn a_1 fun w h => Prod.casesOn (motive := fun x => s(Sum.inl x.1, Sum.inr x.2) = e → e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet) w (fun i j h => h ▸ of_eq_true (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) (eq_self true)) (and_self True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) Bool.false_eq_true) (and_self False))) (or_false True)))) h }i₁:Fin aj₁:Fin bi₂:Fin aj₂:Fin b⊢ φ (i₁, j₁) = φ (i₂, j₂) → (i₁, j₁) = (i₂, j₂) a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)hedge:(completeBipartiteGraph (Fin a) (Fin b)).edgeSet = φ '' Set.univ := Set.ext fun e => Eq.mpr (id (congrArg (Iff (e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet)) (Eq.trans (Eq.trans (congrArg (fun x => e ∈ x) (Set.image_congr fun a_1 a_2 => Eq.refl s(Sum.inl a_1.1, Sum.inr a_1.2))) (complete_bipartite_edge_count._simp_1 (fun a_1 => s(Sum.inl a_1.1, Sum.inr a_1.2)) Set.univ e)) (congrArg Exists (funext fun x => Eq.trans (congrArg (fun x_1 => x_1 ∧ s(Sum.inl x.1, Sum.inr x.2) = e) (complete_bipartite_edge_count._simp_2 x)) (true_and (s(Sum.inl x.1, Sum.inr x.2) = e))))))) { mp := fun hadj => Quot.ind (fun a_1 hadj => Prod.casesOn (motive := fun t => a_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) a_1) a_1 (fun a_2 b_1 h => Eq.ndrec (motive := fun p => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p) (fun hadj => Sum.casesOn (motive := fun t => a_2 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_2, b_1)) a_2 (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (or_self False))) hadj)) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val) (Sum.inr val_1)) (congr (congrArg And (Sum.inl.injEq x.1 val)) (Sum.inr.injEq x.2 val_1)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val_1) (Sum.inl val)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (or_false (x.1 = val ∧ x.2 = val_1)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val) (Sum.inl val_1)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val_1) (Sum.inr val)) (congr (congrArg And (Sum.inl.injEq x.1 val_1)) (Sum.inr.injEq x.2 val)))) (false_or (x.1 = val_1 ∧ x.2 = val)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (or_self False))) hadj)) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (Eq.refl a_2)) (Eq.symm h) hadj) (Eq.refl a_1)) e hadj, mpr := fun a_1 => Exists.casesOn a_1 fun w h => Prod.casesOn (motive := fun x => s(Sum.inl x.1, Sum.inr x.2) = e → e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet) w (fun i j h => h ▸ of_eq_true (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) (eq_self true)) (and_self True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) Bool.false_eq_true) (and_self False))) (or_false True)))) h }i₁:Fin aj₁:Fin bi₂:Fin aj₂:Fin bh:φ (i₁, j₁) = φ (i₂, j₂)⊢ (i₁, j₁) = (i₂, j₂) a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)hedge:(completeBipartiteGraph (Fin a) (Fin b)).edgeSet = φ '' Set.univ := Set.ext fun e => Eq.mpr (id (congrArg (Iff (e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet)) (Eq.trans (Eq.trans (congrArg (fun x => e ∈ x) (Set.image_congr fun a_1 a_2 => Eq.refl s(Sum.inl a_1.1, Sum.inr a_1.2))) (complete_bipartite_edge_count._simp_1 (fun a_1 => s(Sum.inl a_1.1, Sum.inr a_1.2)) Set.univ e)) (congrArg Exists (funext fun x => Eq.trans (congrArg (fun x_1 => x_1 ∧ s(Sum.inl x.1, Sum.inr x.2) = e) (complete_bipartite_edge_count._simp_2 x)) (true_and (s(Sum.inl x.1, Sum.inr x.2) = e))))))) { mp := fun hadj => Quot.ind (fun a_1 hadj => Prod.casesOn (motive := fun t => a_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) a_1) a_1 (fun a_2 b_1 h => Eq.ndrec (motive := fun p => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p) (fun hadj => Sum.casesOn (motive := fun t => a_2 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_2, b_1)) a_2 (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (or_self False))) hadj)) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val) (Sum.inr val_1)) (congr (congrArg And (Sum.inl.injEq x.1 val)) (Sum.inr.injEq x.2 val_1)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val_1) (Sum.inl val)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (or_false (x.1 = val ∧ x.2 = val_1)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val) (Sum.inl val_1)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val_1) (Sum.inr val)) (congr (congrArg And (Sum.inl.injEq x.1 val_1)) (Sum.inr.injEq x.2 val)))) (false_or (x.1 = val_1 ∧ x.2 = val)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (or_self False))) hadj)) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (Eq.refl a_2)) (Eq.symm h) hadj) (Eq.refl a_1)) e hadj, mpr := fun a_1 => Exists.casesOn a_1 fun w h => Prod.casesOn (motive := fun x => s(Sum.inl x.1, Sum.inr x.2) = e → e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet) w (fun i j h => h ▸ of_eq_true (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) (eq_self true)) (and_self True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) Bool.false_eq_true) (and_self False))) (or_false True)))) h }i₁:Fin aj₁:Fin bi₂:Fin aj₂:Fin bh:Sum.inl i₁ = Sum.inl i₂ ∧ Sum.inr j₁ = Sum.inr j₂ ∨ Sum.inl i₁ = Sum.inr j₂ ∧ Sum.inr j₁ = Sum.inl i₂⊢ (i₁, j₁) = (i₂, j₂) a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)hedge:(completeBipartiteGraph (Fin a) (Fin b)).edgeSet = φ '' Set.univ := Set.ext fun e => Eq.mpr (id (congrArg (Iff (e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet)) (Eq.trans (Eq.trans (congrArg (fun x => e ∈ x) (Set.image_congr fun a_1 a_2 => Eq.refl s(Sum.inl a_1.1, Sum.inr a_1.2))) (complete_bipartite_edge_count._simp_1 (fun a_1 => s(Sum.inl a_1.1, Sum.inr a_1.2)) Set.univ e)) (congrArg Exists (funext fun x => Eq.trans (congrArg (fun x_1 => x_1 ∧ s(Sum.inl x.1, Sum.inr x.2) = e) (complete_bipartite_edge_count._simp_2 x)) (true_and (s(Sum.inl x.1, Sum.inr x.2) = e))))))) { mp := fun hadj => Quot.ind (fun a_1 hadj => Prod.casesOn (motive := fun t => a_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) a_1) a_1 (fun a_2 b_1 h => Eq.ndrec (motive := fun p => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p) (fun hadj => Sum.casesOn (motive := fun t => a_2 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_2, b_1)) a_2 (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (or_self False))) hadj)) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val) (Sum.inr val_1)) (congr (congrArg And (Sum.inl.injEq x.1 val)) (Sum.inr.injEq x.2 val_1)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val_1) (Sum.inl val)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (or_false (x.1 = val ∧ x.2 = val_1)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val) (Sum.inl val_1)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val_1) (Sum.inr val)) (congr (congrArg And (Sum.inl.injEq x.1 val_1)) (Sum.inr.injEq x.2 val)))) (false_or (x.1 = val_1 ∧ x.2 = val)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (or_self False))) hadj)) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (Eq.refl a_2)) (Eq.symm h) hadj) (Eq.refl a_1)) e hadj, mpr := fun a_1 => Exists.casesOn a_1 fun w h => Prod.casesOn (motive := fun x => s(Sum.inl x.1, Sum.inr x.2) = e → e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet) w (fun i j h => h ▸ of_eq_true (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) (eq_self true)) (and_self True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) Bool.false_eq_true) (and_self False))) (or_false True)))) h }i₁:Fin aj₁:Fin bi₂:Fin aj₂:Fin bh1:Sum.inl i₁ = Sum.inl i₂h2:Sum.inr j₁ = Sum.inr j₂⊢ (i₁, j₁) = (i₂, j₂)a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)hedge:(completeBipartiteGraph (Fin a) (Fin b)).edgeSet = φ '' Set.univ := Set.ext fun e => Eq.mpr (id (congrArg (Iff (e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet)) (Eq.trans (Eq.trans (congrArg (fun x => e ∈ x) (Set.image_congr fun a_1 a_2 => Eq.refl s(Sum.inl a_1.1, Sum.inr a_1.2))) (complete_bipartite_edge_count._simp_1 (fun a_1 => s(Sum.inl a_1.1, Sum.inr a_1.2)) Set.univ e)) (congrArg Exists (funext fun x => Eq.trans (congrArg (fun x_1 => x_1 ∧ s(Sum.inl x.1, Sum.inr x.2) = e) (complete_bipartite_edge_count._simp_2 x)) (true_and (s(Sum.inl x.1, Sum.inr x.2) = e))))))) { mp := fun hadj => Quot.ind (fun a_1 hadj => Prod.casesOn (motive := fun t => a_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) a_1) a_1 (fun a_2 b_1 h => Eq.ndrec (motive := fun p => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p) (fun hadj => Sum.casesOn (motive := fun t => a_2 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_2, b_1)) a_2 (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (or_self False))) hadj)) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val) (Sum.inr val_1)) (congr (congrArg And (Sum.inl.injEq x.1 val)) (Sum.inr.injEq x.2 val_1)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val_1) (Sum.inl val)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (or_false (x.1 = val ∧ x.2 = val_1)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val) (Sum.inl val_1)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val_1) (Sum.inr val)) (congr (congrArg And (Sum.inl.injEq x.1 val_1)) (Sum.inr.injEq x.2 val)))) (false_or (x.1 = val_1 ∧ x.2 = val)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (or_self False))) hadj)) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (Eq.refl a_2)) (Eq.symm h) hadj) (Eq.refl a_1)) e hadj, mpr := fun a_1 => Exists.casesOn a_1 fun w h => Prod.casesOn (motive := fun x => s(Sum.inl x.1, Sum.inr x.2) = e → e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet) w (fun i j h => h ▸ of_eq_true (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) (eq_self true)) (and_self True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) Bool.false_eq_true) (and_self False))) (or_false True)))) h }i₁:Fin aj₁:Fin bi₂:Fin aj₂:Fin bh1:Sum.inl i₁ = Sum.inr j₂right✝:Sum.inr j₁ = Sum.inl i₂⊢ (i₁, j₁) = (i₂, j₂) a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)hedge:(completeBipartiteGraph (Fin a) (Fin b)).edgeSet = φ '' Set.univ := Set.ext fun e => Eq.mpr (id (congrArg (Iff (e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet)) (Eq.trans (Eq.trans (congrArg (fun x => e ∈ x) (Set.image_congr fun a_1 a_2 => Eq.refl s(Sum.inl a_1.1, Sum.inr a_1.2))) (complete_bipartite_edge_count._simp_1 (fun a_1 => s(Sum.inl a_1.1, Sum.inr a_1.2)) Set.univ e)) (congrArg Exists (funext fun x => Eq.trans (congrArg (fun x_1 => x_1 ∧ s(Sum.inl x.1, Sum.inr x.2) = e) (complete_bipartite_edge_count._simp_2 x)) (true_and (s(Sum.inl x.1, Sum.inr x.2) = e))))))) { mp := fun hadj => Quot.ind (fun a_1 hadj => Prod.casesOn (motive := fun t => a_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) a_1) a_1 (fun a_2 b_1 h => Eq.ndrec (motive := fun p => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p) (fun hadj => Sum.casesOn (motive := fun t => a_2 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_2, b_1)) a_2 (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (or_self False))) hadj)) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val) (Sum.inr val_1)) (congr (congrArg And (Sum.inl.injEq x.1 val)) (Sum.inr.injEq x.2 val_1)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val_1) (Sum.inl val)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (or_false (x.1 = val ∧ x.2 = val_1)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val) (Sum.inl val_1)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val_1) (Sum.inr val)) (congr (congrArg And (Sum.inl.injEq x.1 val_1)) (Sum.inr.injEq x.2 val)))) (false_or (x.1 = val_1 ∧ x.2 = val)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (or_self False))) hadj)) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (Eq.refl a_2)) (Eq.symm h) hadj) (Eq.refl a_1)) e hadj, mpr := fun a_1 => Exists.casesOn a_1 fun w h => Prod.casesOn (motive := fun x => s(Sum.inl x.1, Sum.inr x.2) = e → e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet) w (fun i j h => h ▸ of_eq_true (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) (eq_self true)) (and_self True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) Bool.false_eq_true) (and_self False))) (or_false True)))) h }i₁:Fin aj₁:Fin bi₂:Fin aj₂:Fin bh1:Sum.inl i₁ = Sum.inl i₂h2:Sum.inr j₁ = Sum.inr j₂⊢ (i₁, j₁) = (i₂, j₂) All goals completed! 🐙 a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)hedge:(completeBipartiteGraph (Fin a) (Fin b)).edgeSet = φ '' Set.univ := Set.ext fun e => Eq.mpr (id (congrArg (Iff (e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet)) (Eq.trans (Eq.trans (congrArg (fun x => e ∈ x) (Set.image_congr fun a_1 a_2 => Eq.refl s(Sum.inl a_1.1, Sum.inr a_1.2))) (complete_bipartite_edge_count._simp_1 (fun a_1 => s(Sum.inl a_1.1, Sum.inr a_1.2)) Set.univ e)) (congrArg Exists (funext fun x => Eq.trans (congrArg (fun x_1 => x_1 ∧ s(Sum.inl x.1, Sum.inr x.2) = e) (complete_bipartite_edge_count._simp_2 x)) (true_and (s(Sum.inl x.1, Sum.inr x.2) = e))))))) { mp := fun hadj => Quot.ind (fun a_1 hadj => Prod.casesOn (motive := fun t => a_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) a_1) a_1 (fun a_2 b_1 h => Eq.ndrec (motive := fun p => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p) (fun hadj => Sum.casesOn (motive := fun t => a_2 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_2, b_1)) a_2 (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (or_self False))) hadj)) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val) (Sum.inr val_1)) (congr (congrArg And (Sum.inl.injEq x.1 val)) (Sum.inr.injEq x.2 val_1)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val_1) (Sum.inl val)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (or_false (x.1 = val ∧ x.2 = val_1)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val) (Sum.inl val_1)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val_1) (Sum.inr val)) (congr (congrArg And (Sum.inl.injEq x.1 val_1)) (Sum.inr.injEq x.2 val)))) (false_or (x.1 = val_1 ∧ x.2 = val)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (or_self False))) hadj)) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (Eq.refl a_2)) (Eq.symm h) hadj) (Eq.refl a_1)) e hadj, mpr := fun a_1 => Exists.casesOn a_1 fun w h => Prod.casesOn (motive := fun x => s(Sum.inl x.1, Sum.inr x.2) = e → e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet) w (fun i j h => h ▸ of_eq_true (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) (eq_self true)) (and_self True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) Bool.false_eq_true) (and_self False))) (or_false True)))) h }i₁:Fin aj₁:Fin bi₂:Fin aj₂:Fin bh1:Sum.inl i₁ = Sum.inr j₂right✝:Sum.inr j₁ = Sum.inl i₂⊢ (i₁, j₁) = (i₂, j₂) exact absurd h1 (a:ℕb:ℕφ:Fin a × Fin b → Sym2 (Fin a ⊕ Fin b) := fun p => s(Sum.inl p.1, Sum.inr p.2)hedge:(completeBipartiteGraph (Fin a) (Fin b)).edgeSet = φ '' Set.univ := Set.ext fun e => Eq.mpr (id (congrArg (Iff (e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet)) (Eq.trans (Eq.trans (congrArg (fun x => e ∈ x) (Set.image_congr fun a_1 a_2 => Eq.refl s(Sum.inl a_1.1, Sum.inr a_1.2))) (complete_bipartite_edge_count._simp_1 (fun a_1 => s(Sum.inl a_1.1, Sum.inr a_1.2)) Set.univ e)) (congrArg Exists (funext fun x => Eq.trans (congrArg (fun x_1 => x_1 ∧ s(Sum.inl x.1, Sum.inr x.2) = e) (complete_bipartite_edge_count._simp_2 x)) (true_and (s(Sum.inl x.1, Sum.inr x.2) = e))))))) { mp := fun hadj => Quot.ind (fun a_1 hadj => Prod.casesOn (motive := fun t => a_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) a_1) a_1 (fun a_2 b_1 h => Eq.ndrec (motive := fun p => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) p) (fun hadj => Sum.casesOn (motive := fun t => a_2 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_2, b_1)) a_2 (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (or_self False))) hadj)) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inl val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val) (Sum.inr val_1)) (congr (congrArg And (Sum.inl.injEq x.1 val)) (Sum.inr.injEq x.2 val_1)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val_1) (Sum.inl val)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (or_false (x.1 = val ∧ x.2 = val_1)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (fun val h => Eq.ndrec (motive := fun a_3 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (a_3, b_1)) (fun hadj => Sum.casesOn (motive := fun t => b_1 = t → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_1)) b_1 (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => of_eq_true (Eq.trans (Eq.trans (congrArg Exists (funext fun x => Eq.trans Sym2.eq._simp_1 (Eq.trans Sym2.rel_iff'._simp_1 (Eq.trans (congr (congrArg Or (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inr val) (Sum.inl val_1)) (Eq.trans (congr (congrArg And (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (eq_false' fun h => False.elim (noConfusion_of_Nat Sum.ctorIdx h))) (and_self False)))) (Eq.trans (Prod.mk.injEq (Sum.inl x.1) (Sum.inr x.2) (Sum.inl val_1) (Sum.inr val)) (congr (congrArg And (Sum.inl.injEq x.1 val_1)) (Sum.inr.injEq x.2 val)))) (false_or (x.1 = val_1 ∧ x.2 = val)))))) Prod.exists._simp_1) (Eq.trans (congrArg Exists (funext fun a_3 => exists_eq_right._simp_1)) exists_eq._simp_1))) (Eq.symm h) hadj) (fun val_1 h => Eq.ndrec (motive := fun b_2 => Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2) ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet → ∃ x, s(Sum.inl x.1, Sum.inr x.2) = Quot.mk (Sym2.Rel (Fin a ⊕ Fin b)) (Sum.inr val, b_2)) (fun hadj => False.elim (Eq.mp (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And Bool.false_eq_true) (eq_self true)) (and_true False))) (Eq.trans (congr (congrArg And (eq_self true)) Bool.false_eq_true) (and_false True))) (or_self False))) hadj)) (Eq.symm h) hadj) (Eq.refl b_1)) (Eq.symm h) hadj) (Eq.refl a_2)) (Eq.symm h) hadj) (Eq.refl a_1)) e hadj, mpr := fun a_1 => Exists.casesOn a_1 fun w h => Prod.casesOn (motive := fun x => s(Sum.inl x.1, Sum.inr x.2) = e → e ∈ (completeBipartiteGraph (Fin a) (Fin b)).edgeSet) w (fun i j h => h ▸ of_eq_true (Eq.trans (mem_edgeSet._simp_1 { Adj := fun v w => v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := fun v w => completeBipartiteGraph._proof_1 (Fin a) (Fin b) v w, loopless := fun v => completeBipartiteGraph._proof_2 (Fin a) (Fin b) v }) (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (eq_self true)) (eq_self true)) (and_self True))) (Eq.trans (congr (congrArg And Bool.false_eq_true) Bool.false_eq_true) (and_self False))) (or_false True)))) h }i₁:Fin aj₁:Fin bi₂:Fin aj₂:Fin bh1:Sum.inl i₁ = Sum.inr j₂right✝:Sum.inr j₁ = Sum.inl i₂⊢ ¬Sum.inl i₁ = Sum.inr j₂ All goals completed! 🐙) All goals completed! 🐙 namespace variants

Plesník [Pl75] proved the bound $|E(G)| < 3n(n-1)/8$ for any diameter-$2$-critical graph on $n$ vertices.

@[category research solved, AMS 5] theorem declaration uses 'sorry'plesnik_bound (G : SimpleGraph V) [DecidableRel G.Adj] (hG : IsDiameter2Critical G) : (G.edgeFinset.card : ℝ) < 3 * (Fintype.card V : ℝ) * ((Fintype.card V : ℝ) - 1) / 8 := V:Type u_1inst✝²:Fintype Vinst✝¹:DecidableEq VG:SimpleGraph Vinst✝:DecidableRel G.AdjhG:IsDiameter2Critical G⊢ ↑G.edgeFinset.card < 3 * ↑(Fintype.card V) * (↑(Fintype.card V) - 1) / 8 All goals completed! 🐙

Fan [Fa87] verified the Murty-Simon conjecture for all $n \leq 24$ and for $n = 26$.

@[category research solved, AMS 5] theorem declaration uses 'sorry'fan_bound (G : SimpleGraph V) [DecidableRel G.Adj] (hn : Fintype.card V ≤ 24 ∨ Fintype.card V = 26) (hG : IsDiameter2Critical G) : G.edgeFinset.card ≤ (Fintype.card V) ^ 2 / 4 := V:Type u_1inst✝²:Fintype Vinst✝¹:DecidableEq VG:SimpleGraph Vinst✝:DecidableRel G.Adjhn:Fintype.card V ≤ 24 ∨ Fintype.card V = 26hG:IsDiameter2Critical G⊢ G.edgeFinset.card ≤ Fintype.card V ^ 2 / 4 All goals completed! 🐙

Füredi [Fü92] proved the Murty-Simon conjecture for all sufficiently large $n$, that is, there exists $n_0$ such that every diameter-$2$-critical graph on $n \geq n_0$ vertices has at most $\lfloor n^2 / 4 \rfloor$ edges.

@[category research solved, AMS 5] theorem declaration uses 'sorry'furedi_bound : ∃ n₀ : ℕ, ∀ (V : Type*) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], n₀ ≤ Fintype.card V → IsDiameter2Critical G → G.edgeFinset.card ≤ (Fintype.card V) ^ 2 / 4 := ⊢ ∃ n₀, ∀ (V : Type u_2) [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], n₀ ≤ Fintype.card V → IsDiameter2Critical G → G.edgeFinset.card ≤ Fintype.card V ^ 2 / 4 All goals completed! 🐙 end variants end Erdos742