feat(SimpleGraph): independent sets

[FordUniver]

feat: SimpleGraph independent sets

---

[github-actions]

PR summary e2f3d3f070

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Clique	553	561	+8 (+1.45%)

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Combinatorics.SimpleGraph.Turan	6
Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite	7
Mathlib.Combinatorics.SimpleGraph.Clique	8
Mathlib.Combinatorics.SimpleGraph.IndependentSet	562

---

Declarations diff

+ IndependentSetFree
+ IndependentSetFree.cliqueFreeOn
+ IndependentSetFree.comap
+ IndependentSetFree.mono
+ IndependentSetFree.mono'
+ IndependentSetFree.sup_edge
+ IndependentSetFreeOn
+ IndependentSetFreeOn.anti
+ IndependentSetFreeOn.mono
+ IndependentSetFreeOn.of_succ
+ IndependentSetFreeOn.subset
+ IsIndependentSet
+ IsIndependentSet.anti
+ IsIndependentSet.finsetMap
+ IsIndependentSet.insert
+ IsIndependentSet.map
+ IsIndependentSet.of_subsingleton
+ IsIndependentSet.subset
+ IsIndependentSet.subsingleton
+ IsNIndependentSet
+ IsNIndependentSet.anti
+ IsNIndependentSet.insert
+ IsNIndependentSet.map
+ IsNIndependentSet.not_independentSetFree
+ _
+ botEmbeddingOfNotIndependentSetFree
+ card_independentSetFinset_le
+ cliqueFreeOn_empty
+ cliqueFreeOn_of_card_lt
+ cliqueFreeOn_singleton
+ cliqueFreeOn_two
+ cliqueFreeOn_univ
+ cliqueNum
+ clique_card_le_cliqueNum
+ cocliqueNum
+ cocliqueNum_eq_compl_cliqueNum
+ coe_independentSetFinset
+ fintype_cliqueNum_bddAbove
+ fintype_cocliqueNum_bddAbove
+ independentSetFinset
+ independentSetFinset_anti
+ independentSetFinset_eq_empty_iff
+ independentSetFinset_map
+ independentSetFinset_map_of_equiv
+ independentSetFree_iff
+ independentSetFree_map_if
+ independentSetFree_of_card_lt
+ independentSetFree_top
+ independentSetFree_two
+ independentSetSet
+ independentSetSet_anti
+ independentSetSet_anti'
+ independentSetSet_eq_empty_iff
+ independentSetSet_map
+ independentSetSet_map_of_equiv
+ independentSetSet_one
+ independentSetSet_top
+ independentSetSet_zero
+ independentSet_card_le_cocliqueNum
+ induce_compl_eq_compl_induce
+ instance [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} {s : Finset α} :
+ instance [DecidableEq α] [DecidableRel G.Adj] {s : Finset α} : Decidable (G.IsIndependentSet s)
+ is3IndependentSet_iff
+ is3IndependentSet_triple_iff
+ isClique_compl_map_iff_isClique_map_compl
+ isIndependentSetFree_iff_isCliqueFree_of_complement
+ isIndependentSet_empty
+ isIndependentSet_iff
+ isIndependentSet_iff_induce_eq
+ isIndependentSet_iff_isClique_of_complement
+ isIndependentSet_insert
+ isIndependentSet_map_image_iff
+ isIndependentSet_pair
+ isIndependentSet_singleton
+ isIndependentSet_top_iff
+ isMaximalClique
+ isMaximalIndependentSet
+ isMaximalIndependentSet_iff_compl_isMaximalClique
+ isMaximumClique
+ isMaximumIndependentSet
+ isMaximumIndependentSet_iff_compl_isMaximumClique
+ isNIndependentSet_empty
+ isNIndependentSet_iff
+ isNIndependentSet_iff_isNClique_of_complement
+ isNIndependentSet_one
+ isNIndependentSet_singleton
+ isNIndependentSet_top_iff
+ isNIndependentSet_zero
+ map_compl_le_compl_map
+ maximalClique_if_maximumClique
+ maximalIndependentSet_if_maximumIndependentSet
+ maximumClique_card_eq_cliqueNum
+ maximumIndependentSet_card_eq_cocliqueNum
+ mem_independentSetFinset_iff
+ mem_independentSetSet_iff
+ not_independentSetFree_card_of_bot_embedding
+ not_independentSetFree_iff
+ not_independentSetFree_of_bot_embedding
++ ⟨_,

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[FordUniver]

bot fix style

[github-actions]

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

	rw [←imp_congr_right]; intro hab
	rw [← imp_congr_right]; intro hab