Minor refactoring

Author: mitchell-horner

Mathlib/Combinatorics/SimpleGraph/Bipartite.lean

@@ -289,8 +289,7 @@ lemma between_adj : (G.between s t).Adj v w ↔ G.Adj v w ∧ (v ∈ s ∧ w ∈
 
 lemma between_le : G.between s t ≤ G := fun _ _ h ↦ h.1
 
-lemma between_comm : G.between s t = G.between t s := by
-  ext v w; simp [between_adj, or_comm]
+lemma between_comm : G.between s t = G.between t s := by simp [between, or_comm]
 
 instance [DecidableRel G.Adj] [DecidablePred (· ∈ s)] [DecidablePred (· ∈ t)] :
     DecidableRel (G.between s t).Adj :=
@@ -299,9 +298,7 @@ instance [DecidableRel G.Adj] [DecidablePred (· ∈ s)] [DecidablePred (· ∈
 /-- `G.between s t` is bipartite if the sets `s` and `t` are disjoint. -/
 theorem between_isBipartiteWith (h : Disjoint s t) : (G.between s t).IsBipartiteWith s t where
   disjoint := h
-  mem_of_adj v w := by
-    rw [between_adj]
-    tauto
+  mem_of_adj _ _ h := h.2
 
 /-- `G.between s t` is bipartite if the sets `s` and `t` are disjoint. -/
 theorem between_isBipartite (h : Disjoint s t) : (G.between s t).IsBipartite :=
@@ -311,37 +308,36 @@ theorem between_isBipartite (h : Disjoint s t) : (G.between s t).IsBipartite :=
 in `G`. -/
 lemma neighborSet_subset_between_union (hv : v ∈ s) :
     G.neighborSet v ⊆ (G.between s sᶜ).neighborSet v ∪ s := by
-  simp_rw [neighborSet, between_adj, Set.setOf_subset, Set.mem_union, Set.mem_setOf]
   intro w hadj
+  rw [neighborSet, Set.mem_union, Set.mem_setOf, between_adj]
   by_cases hw : w ∈ s
-  all_goals tauto
+  · exact Or.inr hw
+  · exact Or.inl ⟨hadj, Or.inl ⟨hv, hw⟩⟩
 
 /-- The neighbor set of `w ∈ sᶜ` in `G.between s sᶜ` excludes the vertices in `sᶜ` adjacent to `w`
 in `G`. -/
 lemma neighborSet_subset_between_union' (hw : w ∈ sᶜ) :
     G.neighborSet w ⊆ (G.between s sᶜ).neighborSet w ∪ sᶜ := by
-  simp_rw [neighborSet, between_adj, Set.setOf_subset, Set.mem_union, Set.mem_setOf]
   intro v hadj
+  rw [neighborSet, Set.mem_union, Set.mem_setOf, between_adj]
   by_cases hv : v ∈ s
-  all_goals tauto
+  · exact Or.inl ⟨hadj, Or.inr ⟨hw, hv⟩⟩
+  · exact Or.inr hv
 
 variable [DecidableEq V] [Fintype V] {s t : Finset V} [DecidableRel G.Adj]
 
 /-- The neighbor finset of `v ∈ s` in `G.between s sᶜ` excludes the vertices in `s` adjacent to `v`
 in `G`. -/
 lemma neighborFinset_subset_between_union (hv : v ∈ s) :
     G.neighborFinset v ⊆ (G.between s sᶜ).neighborFinset v ∪ s := by
-  conv_rhs =>
-    rhs; rw [← toFinset_coe s]
-  simp_rw [neighborFinset_def, ← Set.toFinset_union, Set.toFinset_subset_toFinset]
-  exact neighborSet_subset_between_union hv
+  simpa [neighborFinset_def] using neighborSet_subset_between_union hv
 
 /-- The degree of `v ∈ s` in `G` is at most the degree in `G.between s sᶜ` plus the excluded
 vertices from `s`. -/
 theorem degree_le_between_plus (hv : v ∈ s) :
     G.degree v ≤ (G.between s sᶜ).degree v + s.card := by
   have h_bipartite : (G.between s sᶜ).IsBipartiteWith s ↑(sᶜ) := by
-    simpa [coe_compl] using between_isBipartiteWith disjoint_compl_right
+    simpa using between_isBipartiteWith disjoint_compl_right
   simp_rw [← card_neighborFinset_eq_degree,
     ← card_union_of_disjoint (isBipartiteWith_neighborFinset_disjoint h_bipartite hv)]
   exact card_le_card (neighborFinset_subset_between_union hv)
@@ -350,19 +346,14 @@ theorem degree_le_between_plus (hv : v ∈ s) :
 `w` in `G`. -/
 lemma neighborFinset_subset_between_union' (hw : w ∈ sᶜ) :
     G.neighborFinset w ⊆ (G.between s sᶜ).neighborFinset w ∪ sᶜ := by
-  conv_rhs =>
-    rhs; rw [← toFinset_coe s]
-  simp_rw [neighborFinset_def, ← Set.toFinset_compl, ← Set.toFinset_union,
-    Set.toFinset_subset_toFinset]
-  apply neighborSet_subset_between_union'
-  rwa [← mem_coe, coe_compl] at hw
+  simpa [neighborFinset_def] using G.neighborSet_subset_between_union' (by simpa using hw)
 
 /-- The degree of `w ∈ sᶜ` in `G` is at most the degree in `G.between s sᶜ` plus the excluded
 vertices from `sᶜ`. -/
 theorem degree_le_between_plus' (hw : w ∈ sᶜ) :
     G.degree w ≤ (G.between s sᶜ).degree w + sᶜ.card := by
   have h_bipartite : (G.between s sᶜ).IsBipartiteWith s ↑(sᶜ) := by
-    simpa [coe_compl] using between_isBipartiteWith disjoint_compl_right
+    simpa using between_isBipartiteWith disjoint_compl_right
   simp_rw [← card_neighborFinset_eq_degree,
     ← card_union_of_disjoint (isBipartiteWith_neighborFinset_disjoint' h_bipartite hw)]
   exact card_le_card (neighborFinset_subset_between_union' hw)