.

leanprover-community · May 30, 2024 · ca68259 · ca68259
1 parent 6ab75df
commit ca68259
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
@@ -123,7 +123,7 @@ lemma triangle_counting'
     refine (Nat.cast_le.2 $ card_union_le _ _).trans ?_
     rw [Nat.cast_add]
     exact add_le_add h₁ h₂
-  rintro a ha b hy t
+  rintro a _ b hy t
   rw [disjoint_left]
   simp only [Prod.forall, mem_image, not_exists, exists_prop, mem_filter, Prod.mk.inj_iff,
     exists_imp, and_imp, not_and, mem_product, or_assoc]