feat(SimpleGraph/Acyclic): a graph is acyclic iff it is free of cycle graphs (leanprover-community#41363)

- `G.IsAcyclic ↔ ∀ n ≥ 3, (cycleGraph n).Free G`
- `G.IsAcyclic → 3 ≤ n → G.CliqueFree n`

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Combinatorics.SimpleGraph.Bipartite
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
+public import Mathlib.Combinatorics.SimpleGraph.CycleGraph
 public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
 public import Mathlib.Combinatorics.SimpleGraph.Metric
 
@@ -649,4 +650,14 @@ lemma isAcyclic_iff_pairwise_not_isEdgeReachable_two :
     rintro ⟨u, v⟩ huv
     exact (isBridge_iff_not_isEdgeReachable_two huv).mpr (h huv.ne)
 
+theorem isAcyclic_iff_free_cycleGraph : G.IsAcyclic ↔ ∀ n ≥ 3, (cycleGraph n).Free G := by
+  refine ⟨fun h n hn hle ↦ ?_, fun h v p hcyc ↦ h p.length hcyc.three_le_length ?_⟩
+  · have ⟨v, p, hcyc, hlen⟩ := cycleGraph_isContained_iff hn |>.mp hle
+    exact h p hcyc
+  · exact cycleGraph_isContained_iff hcyc.three_le_length |>.mpr ⟨v, p, hcyc, rfl⟩
+
+theorem IsAcyclic.cliqueFree (h : G.IsAcyclic) {n : ℕ} (hn : 3 ≤ n) : G.CliqueFree n := by
+  refine not_cliqueFree_iff_top_isContained n |>.not_right.mpr fun hle ↦ ?_
+  exact isAcyclic_iff_free_cycleGraph.mp h n hn <| hle.trans' <| .of_le le_top
+
 end SimpleGraph