1. FormalConjectures
  2. Wikipedia
  3. DiameterSimpleFiniteGroups
/- 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

Babai–Seress Conjectures on the Diameter of Finite Groups

References:

This file contains two conjectures from the Babai–Seress paper:

    Conjecture 1.5: $\operatorname{diam}(A_n) < n^C$ for some absolute constant $C$, where $A_n$ is the alternating group on $n$ elements.

    Conjecture 1.7: $\operatorname{diam}(G) < (\log |G|)^C$ for some absolute constant $C$, where $G$ ranges over all non-abelian finite simple groups.

Conjecture 1.7 generalises Conjecture 1.5, since for $G = A_n$ we have $\log |A_n| \approx n \log n$, so a polylogarithmic bound in $|G|$ implies a polynomial bound in $n$.

namespace BabaiSeressConjectures

The (undirected) Cayley graph of a group $G$ with respect to a generating set $S$. Two elements $g, h \in G$ are adjacent iff $g \neq h$ and $g^{-1} h \in S$ or $h^{-1} g \in S$.

This is constructed using SimpleGraph.fromRel, which takes the relation $g \sim h \iff g^{-1} h \in S$ and automatically symmetrizes it (via disjunction with the reverse relation) and enforces irreflexivity (via $g \neq h$). In particular, this definition effectively uses the symmetrization $S \cup S^{-1}$, so it produces a standard undirected Cayley graph even when $S$ is not itself symmetric.

def cayleyGraph {G : Type*} [Group G] (S : Set G) : SimpleGraph G := SimpleGraph.fromRel (fun g h => g⁻¹ * h ∈ S)

The diameter of a finite group $G$, defined as the maximum diameter of the Cayley graphs $\Gamma(G, A)$ over all generating sets $A$ of $G$.

noncomputable def groupDiam (G : Type*) [Group G] [Fintype G] : ℕ := sSup { d : ℕ | ∃ S : Set G, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d }

For the trivial group (with one element), the group diameter is zero, since every Cayley graph has only one vertex and hence diameter zero.

@[category test, AMS 20] theorem groupDiam_fin_one : groupDiam (alternatingGroup (Fin 0)) = 0 := ⊢ groupDiam ↥(alternatingGroup (Fin 0)) = 0 ⊢ sSup {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d} = 0 ⊢ sSup {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d} ≤ 0 ⊢ {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d}.Nonempty⊢ ∀ b ∈ {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d}, b ≤ 0 ⊢ {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d}.Nonempty All goals completed! 🐙 ⊢ ∀ b ∈ {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d}, b ≤ 0 d:ℕS:Set ↥(alternatingGroup (Fin 0))left✝:Subgroup.closure S = ⊤hd:(cayleyGraph S).diam = d⊢ d ≤ 0 All goals completed! 🐙

The alternating group $A_3 \cong \mathbb{Z}/3\mathbb{Z}$ has group diameter $1$: every non-trivial generating set produces a complete Cayley graph $K_3$, since any single non-identity element and its inverse already reach the entire group.

@[category test, AMS 20] theorem groupDiam_alternating_three : groupDiam (alternatingGroup (Fin 3)) = 1 := ⊢ groupDiam ↥(alternatingGroup (Fin 3)) = 1 have hnt : Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (⊢ 1 < Fintype.card ↥(alternatingGroup (Fin 3)) All goals completed! 🐙) -- Key: for any generating set S of A₃, cayleyGraph S is the complete graph have key : ∀ S : Set ↥(alternatingGroup (Fin 3)), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := ⊢ groupDiam ↥(alternatingGroup (Fin 3)) = 1 intro S hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤⊢ cayleyGraph S = ⊤ hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤⊢ ∀ (a b : ↥(alternatingGroup (Fin 3))), a ≠ b → (cayleyGraph S).Adj a b intro u hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))⊢ u ≠ v → (cayleyGraph S).Adj u v hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ v⊢ (cayleyGraph S).Adj u v hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ v⊢ u ≠ v ∧ (u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ v⊢ u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S -- S must contain a non-identity element obtain ⟨y, hy, hy1⟩ : ∃ y ∈ S, y ≠ 1 := hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ v⊢ ∃ y ∈ S, y ≠ 1 hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ vh:∀ y ∈ S, y = 1⊢ False hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ vh:∀ y ∈ S, y = 1this:Subgroup.closure S ≤ ⊥ := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (h x hx)⊢ False All goals completed! 🐙 -- In A₃ (order 3), any two non-identity elements are equal or inverses have h3 : ∀ x y : ↥(alternatingGroup (Fin 3)), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := ⊢ groupDiam ↥(alternatingGroup (Fin 3)) = 1 All goals completed! 🐙 have hg1 : u⁻¹ * v ≠ 1 := ⊢ groupDiam ↥(alternatingGroup (Fin 3)) = 1 rwa [ne_eq, inv_mul_eq_onehnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ vy:↥(alternatingGroup (Fin 3))hy:y ∈ Shy1:y ≠ 1h3:∀ (x y : ↥(alternatingGroup (Fin 3))), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))⊢ ¬u = v hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ vh3:∀ (x y : ↥(alternatingGroup (Fin 3))), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)hy:u⁻¹ * v ∈ Shy1:u⁻¹ * v ≠ 1⊢ u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ Shnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ vy:↥(alternatingGroup (Fin 3))hy:y ∈ Shy1:y ≠ 1h3:∀ (x y : ↥(alternatingGroup (Fin 3))), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)h:u⁻¹ * v = y⁻¹⊢ u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ vh3:∀ (x y : ↥(alternatingGroup (Fin 3))), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)hy:u⁻¹ * v ∈ Shy1:u⁻¹ * v ≠ 1⊢ u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S All goals completed! 🐙 hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ vy:↥(alternatingGroup (Fin 3))hy:y ∈ Shy1:y ≠ 1h3:∀ (x y : ↥(alternatingGroup (Fin 3))), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)h:u⁻¹ * v = y⁻¹⊢ u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S exact Or.inr (hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ vy:↥(alternatingGroup (Fin 3))hy:y ∈ Shy1:y ≠ 1h3:∀ (x y : ↥(alternatingGroup (Fin 3))), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)h:u⁻¹ * v = y⁻¹⊢ v⁻¹ * u ∈ S rwa [show v⁻¹ * u = (u⁻¹ * v)⁻¹ from hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ vy:↥(alternatingGroup (Fin 3))hy:y ∈ Shy1:y ≠ 1h3:∀ (x y : ↥(alternatingGroup (Fin 3))), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)h:u⁻¹ * v = y⁻¹⊢ v⁻¹ * u = (u⁻¹ * v)⁻¹ All goals completed! 🐙, h, inv_invhnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤u:↥(alternatingGroup (Fin 3))v:↥(alternatingGroup (Fin 3))hne:u ≠ vy:↥(alternatingGroup (Fin 3))hy:y ∈ Shy1:y ≠ 1h3:∀ (x y : ↥(alternatingGroup (Fin 3))), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)h:u⁻¹ * v = y⁻¹⊢ y ∈ S) -- The set of diameters equals {1}, so sSup = 1 hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set ↥(alternatingGroup (Fin 3))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h3 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h3 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩⊢ sSup {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d} = 1 have h_eq : { d | ∃ S : Set ↥(alternatingGroup (Fin 3)), Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d } = {1} := ⊢ groupDiam ↥(alternatingGroup (Fin 3)) = 1 hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set ↥(alternatingGroup (Fin 3))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h3 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h3 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩d:ℕ⊢ d ∈ {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d} ↔ d ∈ {1}; hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set ↥(alternatingGroup (Fin 3))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h3 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h3 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩d:ℕ⊢ (∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d) ↔ d = 1; hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set ↥(alternatingGroup (Fin 3))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h3 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h3 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩d:ℕ⊢ (∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d) → d = 1hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set ↥(alternatingGroup (Fin 3))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h3 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h3 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩d:ℕ⊢ d = 1 → ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set ↥(alternatingGroup (Fin 3))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h3 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h3 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩d:ℕ⊢ (∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d) → d = 1 hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set ↥(alternatingGroup (Fin 3))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h3 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h3 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩S:Set ↥(alternatingGroup (Fin 3))hS:Subgroup.closure S = ⊤⊢ (cayleyGraph S).diam = 1; All goals completed! 🐙 hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set ↥(alternatingGroup (Fin 3))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h3 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h3 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩d:ℕ⊢ d = 1 → ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set ↥(alternatingGroup (Fin 3))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h3 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h3 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩⊢ ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = 1 exact ⟨Set.univ, Subgroup.closure_univ, hnt:Nontrivial ↥(alternatingGroup (Fin 3)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set ↥(alternatingGroup (Fin 3))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h3 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h3 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩⊢ (cayleyGraph Set.univ).diam = 1 All goals completed! 🐙⟩ All goals completed! 🐙

The symmetric group $S_2 \cong \mathbb{Z}/2\mathbb{Z}$ has group diameter $1$: the unique generating set ${(01)}$ produces the complete graph $K_2$, since the single non-identity element and its inverse (which are equal) cover the only other vertex.

@[category test, AMS 20] theorem groupDiam_perm_two : groupDiam (Equiv.Perm (Fin 2)) = 1 := ⊢ groupDiam (Equiv.Perm (Fin 2)) = 1 have hnt : Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (⊢ 1 < Fintype.card (Equiv.Perm (Fin 2)) All goals completed! 🐙) have key : ∀ S : Set (Equiv.Perm (Fin 2)), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := ⊢ groupDiam (Equiv.Perm (Fin 2)) = 1 intro S hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤⊢ cayleyGraph S = ⊤ hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤⊢ ∀ (a b : Equiv.Perm (Fin 2)), a ≠ b → (cayleyGraph S).Adj a b intro u hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)⊢ u ≠ v → (cayleyGraph S).Adj u v hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ v⊢ (cayleyGraph S).Adj u v hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ v⊢ u ≠ v ∧ (u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ v⊢ u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S obtain ⟨y, hy, hy1⟩ : ∃ y ∈ S, y ≠ 1 := hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ v⊢ ∃ y ∈ S, y ≠ 1 hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ vh:∀ y ∈ S, y = 1⊢ False hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ vh:∀ y ∈ S, y = 1this:Subgroup.closure S ≤ ⊥ := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (h x hx)⊢ False All goals completed! 🐙 have h2 : ∀ x y : Equiv.Perm (Fin 2), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := ⊢ groupDiam (Equiv.Perm (Fin 2)) = 1 All goals completed! 🐙 have hg1 : u⁻¹ * v ≠ 1 := ⊢ groupDiam (Equiv.Perm (Fin 2)) = 1 rwa [ne_eq, inv_mul_eq_onehnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ vy:Equiv.Perm (Fin 2)hy:y ∈ Shy1:y ≠ 1h2:∀ (x y : Equiv.Perm (Fin 2)), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))⊢ ¬u = v hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ vh2:∀ (x y : Equiv.Perm (Fin 2)), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)hy:u⁻¹ * v ∈ Shy1:u⁻¹ * v ≠ 1⊢ u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ Shnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ vy:Equiv.Perm (Fin 2)hy:y ∈ Shy1:y ≠ 1h2:∀ (x y : Equiv.Perm (Fin 2)), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)h:u⁻¹ * v = y⁻¹⊢ u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ vh2:∀ (x y : Equiv.Perm (Fin 2)), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)hy:u⁻¹ * v ∈ Shy1:u⁻¹ * v ≠ 1⊢ u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S All goals completed! 🐙 hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ vy:Equiv.Perm (Fin 2)hy:y ∈ Shy1:y ≠ 1h2:∀ (x y : Equiv.Perm (Fin 2)), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)h:u⁻¹ * v = y⁻¹⊢ u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S exact Or.inr (hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ vy:Equiv.Perm (Fin 2)hy:y ∈ Shy1:y ≠ 1h2:∀ (x y : Equiv.Perm (Fin 2)), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)h:u⁻¹ * v = y⁻¹⊢ v⁻¹ * u ∈ S rwa [show v⁻¹ * u = (u⁻¹ * v)⁻¹ from hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ vy:Equiv.Perm (Fin 2)hy:y ∈ Shy1:y ≠ 1h2:∀ (x y : Equiv.Perm (Fin 2)), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)h:u⁻¹ * v = y⁻¹⊢ v⁻¹ * u = (u⁻¹ * v)⁻¹ All goals completed! 🐙, h, inv_invhnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤u:Equiv.Perm (Fin 2)v:Equiv.Perm (Fin 2)hne:u ≠ vy:Equiv.Perm (Fin 2)hy:y ∈ Shy1:y ≠ 1h2:∀ (x y : Equiv.Perm (Fin 2)), x ≠ 1 → y ≠ 1 → x = y ∨ x = y⁻¹ := of_decide_eq_true (id (Eq.refl true))hg1:u⁻¹ * v ≠ 1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne)h:u⁻¹ * v = y⁻¹⊢ y ∈ S) hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set (Equiv.Perm (Fin 2))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h2 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h2 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩⊢ sSup {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d} = 1 have h_eq : { d | ∃ S : Set (Equiv.Perm (Fin 2)), Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d } = {1} := ⊢ groupDiam (Equiv.Perm (Fin 2)) = 1 hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set (Equiv.Perm (Fin 2))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h2 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h2 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩d:ℕ⊢ d ∈ {d | ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d} ↔ d ∈ {1}; hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set (Equiv.Perm (Fin 2))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h2 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h2 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩d:ℕ⊢ (∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d) ↔ d = 1; hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set (Equiv.Perm (Fin 2))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h2 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h2 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩d:ℕ⊢ (∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d) → d = 1hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set (Equiv.Perm (Fin 2))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h2 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h2 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩d:ℕ⊢ d = 1 → ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set (Equiv.Perm (Fin 2))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h2 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h2 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩d:ℕ⊢ (∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d) → d = 1 hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set (Equiv.Perm (Fin 2))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h2 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h2 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩S:Set (Equiv.Perm (Fin 2))hS:Subgroup.closure S = ⊤⊢ (cayleyGraph S).diam = 1; All goals completed! 🐙 hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set (Equiv.Perm (Fin 2))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h2 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h2 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩d:ℕ⊢ d = 1 → ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = d hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set (Equiv.Perm (Fin 2))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h2 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h2 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩⊢ ∃ S, Subgroup.closure S = ⊤ ∧ (cayleyGraph S).diam = 1 exact ⟨Set.univ, Subgroup.closure_univ, hnt:Nontrivial (Equiv.Perm (Fin 2)) := Fintype.one_lt_card_iff_nontrivial.mp (of_decide_eq_true (id (Eq.refl true)))key:∀ (S : Set (Equiv.Perm (Fin 2))), Subgroup.closure S = ⊤ → cayleyGraph S = ⊤ := fun S hS => Eq.mpr (id (congrArg (fun _a => _a) (propext SimpleGraph.eq_top_iff_forall_ne_adj))) fun u v hne => Eq.mpr (id (groupDiam_alternating_three._simp_2 (fun g h => g⁻¹ * h ∈ S) u v)) ⟨hne, Exists.casesOn (Classical.byContradiction fun h => have this := (Subgroup.closure_le ⊥).mpr fun x hx => Subgroup.mem_bot.mpr (Eq.mp (Eq.trans (Mathlib.Tactic.Push.not_exists._simp_1 fun y => y ∈ S ∧ y ≠ 1) (forall_congr fun y => Eq.trans (Mathlib.Tactic.Push.not_and_eq (y ∈ S) (y ≠ 1)) (implies_congr (Eq.refl (y ∈ S)) Classical.not_not._simp_3))) h x hx); absurd (Eq.symm (Eq.symm (le_antisymm this bot_le)) ▸ hS) bot_ne_top) fun y h => And.casesOn h fun hy hy1 => have h2 := of_decide_eq_true (id (Eq.refl true)); have hg1 := Eq.mpr (id (congrArg (fun _a => _a) (ne_eq (u⁻¹ * v) 1))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext inv_mul_eq_one))) hne); Or.casesOn (h2 (u⁻¹ * v) y hg1 hy1) (fun h => Eq.ndrec (motive := fun y => y ∈ S → y ≠ 1 → u⁻¹ * v ∈ S ∨ v⁻¹ * u ∈ S) (fun hy hy1 => Or.inl hy) h hy hy1) fun h => Or.inr (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (have this := of_eq_true (Eq.trans (congr (congrArg (fun x => Eq (x * u)) (groupDiam_alternating_three._simp_3 v)) (Eq.trans (Eq.trans (congrArg (fun x => (x * v)⁻¹) (groupDiam_alternating_three._simp_3 u)) (groupDiam_alternating_three._simp_3 (u ^ (-1) * v))) (Eq.trans (mul_zpow_neg_one (u ^ (-1)) v) (congrArg (HMul.hMul (v ^ (-1))) (Eq.trans (groupDiam_alternating_three._simp_5 u (-1) (-1)) (Eq.trans (congrArg (HPow.hPow u) (Eq.trans (Int.mul_neg (-1) 1) (Eq.trans (congrArg Neg.neg (mul_one (-1))) (neg_neg 1)))) (zpow_one u))))))) (eq_self (v ^ (-1) * u))); this))) (Eq.mpr (id (congrArg (fun _a => _a⁻¹ ∈ S) h)) (Eq.mpr (id (congrArg (fun _a => _a ∈ S) (inv_inv y))) hy)))⟩⊢ (cayleyGraph Set.univ).diam = 1 All goals completed! 🐙⟩ All goals completed! 🐙

Babai–Seress Conjecture (Conjecture 1.5): There exists an absolute constant $C$ such that the diameter of the alternating group $A_n$ satisfies $$\operatorname{diam}(A_n) \leq n^C.$$

Reference: L. Babai and Á. Seress, On the diameter of permutation groups, European Journal of Combinatorics 13 (1992), Conjecture 1.5

@[category research open, AMS 5 20 68] theorem declaration uses 'sorry'babai_seress_conjecture_alternating : ∃ C : ℕ, ∀ n : ℕ, (groupDiam (alternatingGroup (Fin n)) : ℝ) ≤ (n : ℝ) ^ C := ⊢ ∃ C, ∀ (n : ℕ), ↑(groupDiam ↥(alternatingGroup (Fin n))) ≤ ↑n ^ C All goals completed! 🐙

Babai–Seress Conjecture (Conjecture 1.7): There exists an absolute constant $C$ such that every finite simple non-abelian group $G$ satisfies $$\operatorname{diam}(G) \leq (\log |G|)^C.$$

Reference: L. Babai and Á. Seress, On the diameter of permutation groups, European Journal of Combinatorics 13 (1992), Conjecture 1.7

@[category research open, AMS 5 20 68] theorem declaration uses 'sorry'babai_seress_conjecture : ∃ C : ℕ, ∀ (G : Type) [Group G] [Fintype G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) → (groupDiam G : ℝ) ≤ (Real.log (Fintype.card G : ℝ)) ^ C := ⊢ ∃ C, ∀ (G : Type) [inst : Group G] [inst_1 : Fintype G] [IsSimpleGroup G], (∃ a b, a * b ≠ b * a) → ↑(groupDiam G) ≤ Real.log ↑(Fintype.card G) ^ C All goals completed! 🐙 end BabaiSeressConjectures