chore: Rename Dart.is_adj to Dart.adj (#12574)

The `is` doesn't bring any information and `is_adj` really looks like a Lean 3-ism (even though it technically follows the Lean 4 naming convention).

Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

@@ -899,7 +899,7 @@ def tail (p : G.Walk u v) (hp : ¬ p.Nil) : G.Walk (p.sndOfNotNil hp) v :=
 def firstDart (p : G.Walk v w) (hp : ¬ p.Nil) : G.Dart where
   fst := v
   snd := p.sndOfNotNil hp
-  is_adj := p.adj_sndOfNotNil hp
+  adj := p.adj_sndOfNotNil hp
 
 lemma edge_firstDart (p : G.Walk v w) (hp : ¬ p.Nil) :
     (p.firstDart hp).edge = s(v, p.sndOfNotNil hp) := rfl

Mathlib/Combinatorics/SimpleGraph/Dart.lean

@@ -20,7 +20,7 @@ variable {V : Type*} (G : SimpleGraph V)
 This terminology comes from combinatorial maps, and they are also known as "half-edges"
 or "bonds." -/
 structure Dart extends V × V where
-  is_adj : G.Adj fst snd
+  adj : G.Adj fst snd
   deriving DecidableEq
 #align simple_graph.dart SimpleGraph.Dart
 
@@ -47,7 +47,7 @@ theorem Dart.toProd_injective : Function.Injective (Dart.toProd : G.Dart → V 
 instance Dart.fintype [Fintype V] [DecidableRel G.Adj] : Fintype G.Dart :=
   Fintype.ofEquiv (Σ v, G.neighborSet v)
     { toFun := fun s => ⟨(s.fst, s.snd), s.snd.property⟩
-      invFun := fun d => ⟨d.fst, d.snd, d.is_adj⟩
+      invFun := fun d => ⟨d.fst, d.snd, d.adj⟩
       left_inv := fun s => by ext <;> simp
       right_inv := fun d => by ext <;> simp }
 #align simple_graph.dart.fintype SimpleGraph.Dart.fintype
@@ -64,13 +64,13 @@ theorem Dart.edge_mk {p : V × V} (h : G.Adj p.1 p.2) : (Dart.mk p h).edge = Sym
 
 @[simp]
 theorem Dart.edge_mem (d : G.Dart) : d.edge ∈ G.edgeSet :=
-  d.is_adj
+  d.adj
 #align simple_graph.dart.edge_mem SimpleGraph.Dart.edge_mem
 
 /-- The dart with reversed orientation from a given dart. -/
 @[simps]
 def Dart.symm (d : G.Dart) : G.Dart :=
-  ⟨d.toProd.swap, G.symm d.is_adj⟩
+  ⟨d.toProd.swap, G.symm d.adj⟩
 #align simple_graph.dart.symm SimpleGraph.Dart.symm
 
 @[simp]
@@ -99,7 +99,7 @@ theorem Dart.symm_involutive : Function.Involutive (Dart.symm : G.Dart → G.Dar
 #align simple_graph.dart.symm_involutive SimpleGraph.Dart.symm_involutive
 
 theorem Dart.symm_ne (d : G.Dart) : d.symm ≠ d :=
-  ne_of_apply_ne (Prod.snd ∘ Dart.toProd) d.is_adj.ne
+  ne_of_apply_ne (Prod.snd ∘ Dart.toProd) d.adj.ne
 #align simple_graph.dart.symm_ne SimpleGraph.Dart.symm_ne
 
 theorem dart_edge_eq_iff : ∀ d₁ d₂ : G.Dart, d₁.edge = d₂.edge ↔ d₁ = d₂ ∨ d₁ = d₂.symm := by

Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

@@ -62,7 +62,7 @@ theorem dart_fst_fiber [DecidableEq V] (v : V) :
   simp only [mem_image, true_and_iff, mem_filter, SetCoe.exists, mem_univ, exists_prop_of_true]
   constructor
   · rintro rfl
-    exact ⟨_, d.is_adj, by ext <;> rfl⟩
+    exact ⟨_, d.adj, by ext <;> rfl⟩
   · rintro ⟨e, he, rfl⟩
     rfl
 #align simple_graph.dart_fst_fiber SimpleGraph.dart_fst_fiber