From ca68259786c42a52858e8984a4d06a6ad8a1cad4 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 30 May 2024 22:15:04 +1000 Subject: [PATCH] . --- Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean index fac40fed82615..0999b92cbb993 100644 --- 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]