/-
 - Created in 2024 by Gaëtan Serré
 -/

import Mathlib.Algebra.Group.Subgroup.Defs
import CayleyGraph.FinGroup

set_option maxHeartbeats 600000

structure Graph (G : Type*) where
  Adj : Set (G × G)
  Connected : Prop
  Acyclic : Prop

namespace Graph
def is_tree {α : Type*} (G : Graph α) := G.Connected ∧ G.Acyclic
end Graph

def CayleyGraph {G : Type*} [Fintype G] [FinGroup G] (X : Set G) : Graph G :=
  {
    Adj := {(g1, g2) | ∃ g ∈ X, g1 * g = g2 ∨ g1 * g⁻¹ = g2}
    Connected := ∀ g1 g2, g1 ≠ g2 → ∃ (F : Formula G X), 0 < F.length ∧ g1 * F.val = g2
    /-
    For any node `g`, there is no path ((g, g1), ..., (gn, g)) from `g` to `g`. Paths are represented by irreducible Formulas of size >= 1. We use the irreducible property to avoid looking at such Formula: `∀ g' ∈ CG.X, g * [g', g'⁻¹].prod = g`. This kind of Formula gives a trivial path that leads `g` to itself, for any subset `X`. This does not represented a cycle, as reducible Formulas contain steps that cancel each other out in pairs.
    -/
    Acyclic := ∀ g, ∀ (F : Formula G X), 0 < F.length ∧ F.irreducible → g * F.val ≠ g
  }

variable {G : Type*} [Fintype G] [FinGroup G] (X : Set G)
variable (G' : Subgroup G)

/--
We show that, given an irreducible Formula (a path) of size `> 1`, then two consecutive steps never cancel each other out, i.e., given any node `g`, we never go back to `g` directly after moving from it.
-/
example (F : Formula G X) (F_len : 1 < F.length) (F_irr : F.irreducible) : ∀ (g : G), ∀ (i : Fin F.length), g * F.get i * F.get (i + {val:=1, isLt:=F_len}) ≠ g := by
Goals accomplished! 🐙
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
F_irr: F.irreducible
∀ (g : G) (i : Fin F.length), g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ gintro g i
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
F_irr: F.irreducible
g: G
i: Fin F.length
g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ g
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
F_irr: F.irreducible
∀ (g : G) (i : Fin F.length), g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ gunfold Formula.irreducible at F_irr
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
F_irr: if h : 1 < F.length then ∀ (i : Fin F.length), F.get i * F.get (i + ⟨1, h⟩) ≠ 1
else if h : F.length = 1 then F.get ⟨0, ⋯⟩ ≠ 1 else F.elems = []
g: G
i: Fin F.length
g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ g
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
F_irr: F.irreducible
∀ (g : G) (i : Fin F.length), g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ gsplit at F_irr
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: 1 < F.length
F_irr: ∀ (i : Fin F.length), F.get i * F.get (i + ⟨1, h✝⟩) ≠ 1
isTrue
g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ g
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: ¬1 < F.length
F_irr: ∀ (i : Fin F.length), F.get i * F.get (i + ⟨1, F_len⟩) ≠ 1
isFalse
g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ g
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
F_irr: F.irreducible
∀ (g : G) (i : Fin F.length), g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ g·
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: 1 < F.length
F_irr: ∀ (i : Fin F.length), F.get i * F.get (i + ⟨1, h✝⟩) ≠ 1
isTrue
g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ g 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: 1 < F.length
F_irr: ∀ (i : Fin F.length), F.get i * F.get (i + ⟨1, h✝⟩) ≠ 1
isTrue
g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ g
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: ¬1 < F.length
F_irr: ∀ (i : Fin F.length), F.get i * F.get (i + ⟨1, F_len⟩) ≠ 1
isFalse
g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ gspecialize F_irr i
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: 1 < F.length
F_irr: F.get i * F.get (i + ⟨1, h✝⟩) ≠ 1
isTrue
g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ g
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: 1 < F.length
F_irr: ∀ (i : Fin F.length), F.get i * F.get (i + ⟨1, h✝⟩) ≠ 1
isTrue
g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ gby_contra h_contra
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: 1 < F.length
F_irr: F.get i * F.get (i + ⟨1, h✝⟩) ≠ 1
h_contra: g * F.get i * F.get (i + ⟨1, F_len⟩) = g
isTrue
False
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: 1 < F.length
F_irr: ∀ (i : Fin F.length), F.get i * F.get (i + ⟨1, h✝⟩) ≠ 1
isTrue
g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ grw [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: 1 < F.length
F_irr: F.get i * F.get (i + ⟨1, h✝⟩) ≠ 1
h_contra: g * F.get i * F.get (i + ⟨1, F_len⟩) = g
isTrue
Falseshow g * F.get i * F.get (i + {val:=1, isLt:=F_len}) = g * (F.get i * F.get (i + {val:=1, isLt:=F_len})) by 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: 1 < F.length
F_irr: F.get i * F.get (i + ⟨1, h✝⟩) ≠ 1
h_contra: g * F.get i * F.get (i + ⟨1, F_len⟩) = g
isTrue
Falseexact mul_assoc _ _ _
Goals accomplished! 🐙]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: 1 < F.length
F_irr: F.get i * F.get (i + ⟨1, h✝⟩) ≠ 1
h_contra: g * (F.get i * F.get (i + ⟨1, F_len⟩)) = g
isTrue
False at h_contra
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: 1 < F.length
F_irr: F.get i * F.get (i + ⟨1, h✝⟩) ≠ 1
h_contra: g * (F.get i * F.get (i + ⟨1, F_len⟩)) = g
isTrue
False
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
g: G
i: Fin F.length
h✝: 1 < F.length
F_irr: ∀ (i : Fin F.length), F.get i * F.get (i + ⟨1, h✝⟩) ≠ 1
isTrue
g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ gexact F_irr (mul_right_eq_self.mp h_contra)
Goals accomplished! 🐙
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
F: Formula G X
F_len: 1 < F.length
F_irr: F.irreducible
∀ (g : G) (i : Fin F.length), g * F.get i * F.get (i + ⟨1, F_len⟩) ≠ gcontradiction
Goals accomplished! 🐙

/--
The action of a Subgroup `G'` of `G` on the Cayley graph formed by `G` and `X`
-/
def group_action {G : Type*} [Fintype G] [FinGroup G] {G' : Subgroup G}
  (X : Set G) (g' : G') : Graph G :=
    {
      Adj := {(g1, g2) | ∃ g ∈ X, g1 * g' * g = g2 * g' ∨ g1 * g' * g⁻¹ = g2 * g'}
      Connected := ∀ g1 g2, g1 ≠ g2 → ∃ (F : Formula G X), 0 < F.length ∧ g1 * g' * F.val = g2 * g'
      Acyclic := ∀ g, ∀ (F : Formula G X), 0 < F.length ∧ F.irreducible → g * g' * F.val ≠ g * g'
    }

def CG := CayleyGraph X

/-
We show that our definition of graph action is consistent, that is, CG (G, X) is connected (acyclic) iff any resulting CG graph from our definition is connected (acyclic).
-/
example (g' : G') : (CG X).Connected ↔ (group_action X g').Connected := by
Goals accomplished! 🐙
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(CG X).Connected ↔ (group_action X g').Connectedconstructor
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
mp
(CG X).Connected → (group_action X g').Connected
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
mpr
(group_action X g').Connected → (CG X).Connected
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(CG X).Connected ↔ (group_action X g').Connected·
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
mp
(CG X).Connected → (group_action X g').Connected 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
mp
(CG X).Connected → (group_action X g').Connected
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
mpr
(group_action X g').Connected → (CG X).Connectedintro CG_connected
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
CG_connected: (CG X).Connected
mp
(group_action X g').Connected
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
mp
(CG X).Connected → (group_action X g').Connectedintro g1 g2 g1_neq_g2
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
CG_connected: (CG X).Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
mp
∃ F, 0 < F.length ∧ g1 * ↑g' * F.val = g2 * ↑g'
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
mp
(CG X).Connected → (group_action X g').Connectedhave g1_neq_g2_prod : g1 * g' ≠ g2 * g' := 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
CG_connected: (CG X).Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
mp
∃ F, 0 < F.length ∧ g1 * ↑g' * F.val = g2 * ↑g'by
Goals accomplished! 🐙 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
CG_connected: (CG X).Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
mp
∃ F, 0 < F.length ∧ g1 * ↑g' * F.val = g2 * ↑g'simp only [
        ne_eq, mul_left_inj,
        g1_neq_g2,
        not_false_eq_true
      ]
Goals accomplished! 🐙
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
mp
(CG X).Connected → (group_action X g').Connectedexact CG_connected (g1 * g') (g2 * g') g1_neq_g2_prod
Goals accomplished! 🐙
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(CG X).Connected ↔ (group_action X g').Connectedintro g'CG_connected
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
mpr
(CG X).Connected
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(CG X).Connected ↔ (group_action X g').Connectedintro g1 g2 g1_neq_g2
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
mpr
∃ F, 0 < F.length ∧ g1 * F.val = g2

  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(CG X).Connected ↔ (group_action X g').Connectedhave g1_neq_g2_prod : g1 * g'⁻¹ ≠ g2 * g'⁻¹ := 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
mpr
∃ F, 0 < F.length ∧ g1 * F.val = g2by
Goals accomplished! 🐙 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
mpr
∃ F, 0 < F.length ∧ g1 * F.val = g2simp only [
        ne_eq, mul_left_inj,
        g1_neq_g2,
        not_false_eq_true
      ]
Goals accomplished! 🐙

  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(CG X).Connected ↔ (group_action X g').Connectedrcases g'CG_connected (g1 * g'⁻¹) (g2 * g'⁻¹) g1_neq_g2_prod with ⟨F, F_len, F_val⟩
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * ↑g'⁻¹ * ↑g' * F.val = g2 * ↑g'⁻¹ * ↑g'
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(CG X).Connected ↔ (group_action X g').Connectedrw [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * ↑g'⁻¹ * ↑g' * F.val = g2 * ↑g'⁻¹ * ↑g'
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2mul_assoc g1 ↑g'⁻¹ g',
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * (↑g'⁻¹ * ↑g') * F.val = g2 * ↑g'⁻¹ * ↑g'
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * ↑g'⁻¹ * ↑g' * F.val = g2 * ↑g'⁻¹ * ↑g'
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2mul_assoc g2 ↑g'⁻¹ g'
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * (↑g'⁻¹ * ↑g') * F.val = g2 * (↑g'⁻¹ * ↑g')
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * (↑g'⁻¹ * ↑g') * F.val = g2 * (↑g'⁻¹ * ↑g')
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2 at F_val
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * (↑g'⁻¹ * ↑g') * F.val = g2 * (↑g'⁻¹ * ↑g')
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(CG X).Connected ↔ (group_action X g').Connectedrepeat 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * (↑g'⁻¹ * ↑g') * F.val = g2 * (↑g'⁻¹ * ↑g')
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2rw [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * (↑g'⁻¹ * ↑g') * F.val = g2 * (↑g'⁻¹ * ↑g')
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2show ↑g'⁻¹ * ↑g' = (1 : G) by 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * (↑g'⁻¹ * ↑g') * F.val = g2 * (↑g'⁻¹ * ↑g')
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2exact inv_mul_cancel _
Goals accomplished! 🐙]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * 1 * F.val = g2 * 1
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2 at F_val
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * 1 * F.val = g2 * 1
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(CG X).Connected ↔ (group_action X g').Connectedrw [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * 1 * F.val = g2 * 1
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2mul_one g1,
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * F.val = g2 * 1
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * 1 * F.val = g2 * 1
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2mul_one g2
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * F.val = g2
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * F.val = g2
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2 at F_val
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_connected: (group_action X g').Connected
g1, g2: G
g1_neq_g2: g1 ≠ g2
g1_neq_g2_prod: g1 * ↑g'⁻¹ ≠ g2 * ↑g'⁻¹
F: Formula G X
F_len: 0 < F.length
F_val: g1 * F.val = g2
mpr.intro.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(CG X).Connected ↔ (group_action X g').Connecteduse F, F_len
Goals accomplished! 🐙

example (g' : G') : (CG X).Acyclic ↔ (group_action X g').Acyclic :=
  Iff.intro
  (λ CG_acyclic g F hF ↦ CG_acyclic (g * g') F hF)
  (
    by
Goals accomplished! 🐙
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(group_action X g').Acyclic → (CG X).Acyclicintro g'CG_acyclic g F ⟨F_len, F_irr⟩
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g'CG_acyclic: (group_action X g').Acyclic
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g * F.val ≠ g
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(group_action X g').Acyclic → (CG X).Acyclicspecialize g'CG_acyclic (g * g'⁻¹) F ⟨F_len, F_irr⟩
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * ↑g'⁻¹ * ↑g' * F.val ≠ g * ↑g'⁻¹ * ↑g'
g * F.val ≠ g
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(group_action X g').Acyclic → (CG X).Acyclicrw [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * ↑g'⁻¹ * ↑g' * F.val ≠ g * ↑g'⁻¹ * ↑g'
g * F.val ≠ gmul_assoc g ↑g'⁻¹ g'
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * (↑g'⁻¹ * ↑g') * F.val ≠ g * (↑g'⁻¹ * ↑g')
g * F.val ≠ g]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * (↑g'⁻¹ * ↑g') * F.val ≠ g * (↑g'⁻¹ * ↑g')
g * F.val ≠ g at g'CG_acyclic
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * (↑g'⁻¹ * ↑g') * F.val ≠ g * (↑g'⁻¹ * ↑g')
g * F.val ≠ g
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(group_action X g').Acyclic → (CG X).Acyclicrepeat 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * (↑g'⁻¹ * ↑g') * F.val ≠ g * (↑g'⁻¹ * ↑g')
g * F.val ≠ grw [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * (↑g'⁻¹ * ↑g') * F.val ≠ g * (↑g'⁻¹ * ↑g')
g * F.val ≠ gshow ↑g'⁻¹ * ↑g' = (1 : G) by 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * (↑g'⁻¹ * ↑g') * F.val ≠ g * (↑g'⁻¹ * ↑g')
g * F.val ≠ gexact inv_mul_cancel _
Goals accomplished! 🐙]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * 1 * F.val ≠ g * 1
g * F.val ≠ g at g'CG_acyclic
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * 1 * F.val ≠ g * 1
g * F.val ≠ g
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
(group_action X g').Acyclic → (CG X).Acyclicrwa [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * 1 * F.val ≠ g * 1
g * F.val ≠ gmul_one g
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * F.val ≠ g
g * F.val ≠ g]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
G': Subgroup G
g': ↥G'
g: G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
g'CG_acyclic: g * F.val ≠ g
g * F.val ≠ g at g'CG_acyclic
Goals accomplished! 🐙
  )

-------- Equivalence between properties of Cayley graph and groups --------

theorem generative_connected_iff : generative_family X ↔ (CG X).Connected := by
Goals accomplished! 🐙
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
generative_family X ↔ (CG X).Connectedconstructor
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
generative_family X → (CG X).Connected
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mpr
(CG X).Connected → generative_family X
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
generative_family X ↔ (CG X).Connected·
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
generative_family X → (CG X).Connected 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
generative_family X → (CG X).Connected
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mpr
(CG X).Connected → generative_family Xintro h g1 g2 g1_neq_g2
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
mp
∃ F, 0 < F.length ∧ g1 * F.val = g2
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
generative_family X → (CG X).Connectedrcases h (g1⁻¹ * g2) with ⟨F, F_val⟩
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
mp.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
generative_family X → (CG X).Connectedhave cancel_prod : g1 * F.val = g2 := 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
mp.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2by
Goals accomplished! 🐙 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
mp.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2rw[
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
g1 * F.val = g2F_val,
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
g1 * (g1⁻¹ * g2) = g2 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
g1 * F.val = g2mul_inv_cancel_left
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
g2 = g2]
Goals accomplished! 🐙

    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
generative_family X → (CG X).Connectedhave F_length : 0 < F.length := 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
mp.intro
∃ F, 0 < F.length ∧ g1 * F.val = g2by
Goals accomplished! 🐙 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
0 < F.length{
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
0 < F.length
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
0 < F.lengthby_contra h
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: ¬0 < F.length
False
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
0 < F.lengthpush_neg at h
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
False
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
0 < F.lengthhave F_eq_nil : F.elems = [] := List.length_eq_zero.mp (Nat.eq_zero_of_le_zero h)
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
False
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
0 < F.lengthhave F_val_eq_1 : F.val = 1 := 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
Falseby
Goals accomplished! 🐙 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
Falseunfold Formula.val
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
F.elems.prod = 1;
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
F.elems.prod = 1 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
Falserw [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
F.elems.prod = 1F_eq_nil
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
[].prod = 1]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
[].prod = 1;
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
[].prod = 1 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
Falserfl
Goals accomplished! 🐙
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
0 < F.lengthrw [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
F_val_eq_1: F.val = 1
FalseF_val_eq_1
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * 1 = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
F_val_eq_1: F.val = 1
False]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * 1 = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
F_val_eq_1: F.val = 1
False at cancel_prod
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * 1 = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
F_val_eq_1: F.val = 1
False
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
0 < F.lengthrw [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * 1 = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
F_val_eq_1: F.val = 1
Falseshow g1 * 1 = g1 by 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * 1 = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
F_val_eq_1: F.val = 1
Falseexact mul_one _
Goals accomplished! 🐙]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
F_val_eq_1: F.val = 1
False at cancel_prod
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h✝: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 = g2
h: F.length ≤ 0
F_eq_nil: F.elems = []
F_val_eq_1: F.val = 1
False
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: generative_family X
g1, g2: G
g1_neq_g2: g1 ≠ g2
F: Formula G X
F_val: F.val = g1⁻¹ * g2
cancel_prod: g1 * F.val = g2
0 < F.lengthexact g1_neq_g2 cancel_prod
Goals accomplished! 🐙
    }
Goals accomplished! 🐙
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
generative_family X → (CG X).Connectedexact ⟨F, ⟨F_length, cancel_prod⟩⟩
Goals accomplished! 🐙

  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
generative_family X ↔ (CG X).Connectedintro h g
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
mpr
∃ F, F.val = g
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
generative_family X ↔ (CG X).Connectedby_cases hg : g = 1
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
pos
∃ F, F.val = g
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: ¬g = 1
neg
∃ F, F.val = g
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
generative_family X ↔ (CG X).Connected·
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
pos
∃ F, F.val = g 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
pos
∃ F, F.val = g
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: ¬g = 1
neg
∃ F, F.val = glet F : Formula G X := {
      elems := []
      elems_in_X := λ e e_in ↦ (List.not_mem_nil e).elim e_in
    }
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
pos
∃ F, F.val = g
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
pos
∃ F, F.val = guse F
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
h
F.val = g
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
pos
∃ F, F.val = grw [
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
h
F.val = gshow F.val = F.elems.prod by 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
h
F.val = grfl
Goals accomplished! 🐙,
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
h
F.elems.prod = g
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
h
F.val = gshow F.elems = [] by 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
h
F.elems.prod = grfl
Goals accomplished! 🐙,
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
h
[].prod = g
      
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
h
F.val = ghg,
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
h
[].prod = 1 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
h
F.val = gshow [].prod = (1 : G) by 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
h
[].prod = 1rfl
Goals accomplished! 🐙
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g = 1
F:= { elems := [], elems_in_X := ⋯ }: Formula G X
h
F.val = g]
Goals accomplished! 🐙
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
generative_family X ↔ (CG X).Connectedpush_neg at hg
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g ≠ 1
neg
∃ F, F.val = g
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
generative_family X ↔ (CG X).Connectedrcases h 1 g hg.symm with ⟨F, _, F_val⟩
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g ≠ 1
F: Formula G X
left✝: 0 < F.length
F_val: 1 * F.val = g
neg.intro.intro
∃ F, F.val = g
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
generative_family X ↔ (CG X).Connecteduse F
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g ≠ 1
F: Formula G X
left✝: 0 < F.length
F_val: 1 * F.val = g
h
F.val = g
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
generative_family X ↔ (CG X).Connectedrwa [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g ≠ 1
F: Formula G X
left✝: 0 < F.length
F_val: 1 * F.val = g
h
F.val = g←one_mul F.val
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g ≠ 1
F: Formula G X
left✝: 0 < F.length
F_val: 1 * F.val = g
h
1 * F.val = g]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Connected
g: G
hg: g ≠ 1
F: Formula G X
left✝: 0 < F.length
F_val: 1 * F.val = g
h
1 * F.val = g

theorem free_acyclic_iff : free_family X ↔ (CG X).Acyclic := by
Goals accomplished! 🐙
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
free_family X ↔ (CG X).Acyclicconstructor
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
free_family X → (CG X).Acyclic
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mpr
(CG X).Acyclic → free_family X
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
free_family X ↔ (CG X).Acyclic·
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
free_family X → (CG X).Acyclic 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
free_family X → (CG X).Acyclic
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mpr
(CG X).Acyclic → free_family Xintro h
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: free_family X
mp
(CG X).Acyclic
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
free_family X → (CG X).Acyclicby_contra h_acyclic
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: free_family X
h_acyclic: ¬(CG X).Acyclic
mp
False
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
free_family X → (CG X).Acyclicrw [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: free_family X
h_acyclic: ¬(CG X).Acyclic
mp
Falseshow (CG X).Acyclic = ∀ g, ∀ (F : Formula G X), 0 < F.length ∧ F.irreducible → g * F.val ≠ g by 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: free_family X
h_acyclic: ¬(CG X).Acyclic
mp
Falserfl
Goals accomplished! 🐙]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: free_family X
h_acyclic: ¬∀ (g : G) (F : Formula G X), 0 < F.length ∧ F.irreducible → g * F.val ≠ g
mp
False at h_acyclic
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: free_family X
h_acyclic: ¬∀ (g : G) (F : Formula G X), 0 < F.length ∧ F.irreducible → g * F.val ≠ g
mp
False
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
free_family X → (CG X).Acyclicpush_neg at h_acyclic
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: free_family X
h_acyclic: ∃ g F, (0 < F.length ∧ F.irreducible) ∧ g * F.val = g
mp
False
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
free_family X → (CG X).Acyclicrcases h_acyclic with ⟨g, F, ⟨F_len, F_irr⟩, F_val⟩
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: free_family X
g: G
F: Formula G X
F_val: g * F.val = g
F_len: 0 < F.length
F_irr: F.irreducible
mp.intro.intro.intro.intro
False
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
free_family X → (CG X).Acyclichave F_val_eq_1 := mul_right_eq_self.mp F_val
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: free_family X
g: G
F: Formula G X
F_val: g * F.val = g
F_len: 0 < F.length
F_irr: F.irreducible
F_val_eq_1: F.val = 1
mp.intro.intro.intro.intro
False
    
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
mp
free_family X → (CG X).Acyclicexact (h F F_len F_irr) F_val_eq_1
Goals accomplished! 🐙
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
free_family X ↔ (CG X).Acyclicintro h
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Acyclic
mpr
free_family X
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
free_family X ↔ (CG X).Acyclicintro F F_len F_irr
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Acyclic
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
mpr
F.val ≠ 1
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
free_family X ↔ (CG X).Acyclicby_contra F_val_eq_1
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
h: (CG X).Acyclic
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
F_val_eq_1: F.val = 1
mpr
False
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
free_family X ↔ (CG X).Acyclicspecialize h 1 F ⟨F_len, F_irr⟩
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
F_val_eq_1: F.val = 1
h: 1 * F.val ≠ 1
mpr
False
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
free_family X ↔ (CG X).Acyclicrw [
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
F_val_eq_1: F.val = 1
h: 1 * F.val ≠ 1
mpr
FalseF_val_eq_1,
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
F_val_eq_1: F.val = 1
h: 1 * 1 ≠ 1
mpr
False 
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
F_val_eq_1: F.val = 1
h: 1 * F.val ≠ 1
mpr
Falseone_mul 1
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
F_val_eq_1: F.val = 1
h: 1 ≠ 1
mpr
False]
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
F_val_eq_1: F.val = 1
h: 1 ≠ 1
mpr
False at h
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
F: Formula G X
F_len: 0 < F.length
F_irr: F.irreducible
F_val_eq_1: F.val = 1
h: 1 ≠ 1
mpr
False
  
G: Type u_1
inst✝¹: Fintype G
inst✝: FinGroup G
X: Set G
free_family X ↔ (CG X).Acycliccontradiction
Goals accomplished! 🐙

theorem tree_free_iff [Inhabited G] :
    is_free_group G ↔ (∃ (X : Set G), (CG X).is_tree) := by
Goals accomplished! 🐙
  
G: Type u_1
inst✝²: Fintype G
inst✝¹: FinGroup G
inst✝: Inhabited G
is_free_group G ↔ ∃ X, (CG X).is_treeconstructor
G: Type u_1
inst✝²: Fintype G
inst✝¹: FinGroup G
inst✝: Inhabited G
mp
is_free_group G → ∃ X, (CG X).is_tree
G: Type u_1
inst✝²: Fintype G
inst✝¹: FinGroup G
inst✝: Inhabited G
mpr
(∃ X, (CG X).is_tree) → is_free_group G
  
G: Type u_1
inst✝²: Fintype G
inst✝¹: FinGroup G
inst✝: Inhabited G
is_free_group G ↔ ∃ X, (CG X).is_tree·
G: Type u_1
inst✝²: Fintype G
inst✝¹: FinGroup G
inst✝: Inhabited G
mp
is_free_group G → ∃ X, (CG X).is_tree 
G: Type u_1
inst✝²: Fintype G
inst✝¹: FinGroup G
inst✝: Inhabited G
mp
is_free_group G → ∃ X, (CG X).is_tree
G: Type u_1
inst✝²: Fintype G
inst✝¹: FinGroup G
inst✝: Inhabited G
mpr
(∃ X, (CG X).is_tree) → is_free_group Gintro ⟨X, X_gen, X_free⟩
G: Type u_1
inst✝²: Fintype G
inst✝¹: FinGroup G
inst✝: Inhabited G
X: Set G
X_gen: generative_family X
X_free: free_family X
mp
∃ X, (CG X).is_tree
    
G: Type u_1
inst✝²: Fintype G
inst✝¹: FinGroup G
inst✝: Inhabited G
mp
is_free_group G → ∃ X, (CG X).is_treeexact ⟨X, (generative_connected_iff X).mp X_gen, (free_acyclic_iff X).mp X_free⟩
Goals accomplished! 🐙
  
G: Type u_1
inst✝²: Fintype G
inst✝¹: FinGroup G
inst✝: Inhabited G
is_free_group G ↔ ∃ X, (CG X).is_treeintro ⟨X, CG_connected, CG_acyclic⟩
G: Type u_1
inst✝²: Fintype G
inst✝¹: FinGroup G
inst✝: Inhabited G
X: Set G
CG_connected: (CG X).Connected
CG_acyclic: (CG X).Acyclic
mpr
is_free_group G
  
G: Type u_1
inst✝²: Fintype G
inst✝¹: FinGroup G
inst✝: Inhabited G
is_free_group G ↔ ∃ X, (CG X).is_treeexact ⟨X, (generative_connected_iff X).mpr CG_connected, (free_acyclic_iff X).mpr CG_acyclic⟩
Goals accomplished! 🐙