From 069828c2189a75834d7fda75830c5d938eb2c3cf Mon Sep 17 00:00:00 2001 From: damiano Date: Sat, 11 May 2024 02:49:06 +0000 Subject: [PATCH] chore: remove a save (#12805) --- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean index 64b5438263a2db..9db58170e5eca8 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean @@ -127,7 +127,6 @@ lemma edgeDisjointTriangles_iff_mem_sym2_subsingleton : forall_exists_index, and_imp, ← Set.not_nontrivial_iff (s := _ ∩ _), not_imp_not, Set.Nontrivial, Set.mem_inter_iff, mem_coe] rintro hG _ a b c hab hac hbc rfl _ d e f hde hdf hef rfl g hg₁ hg₂ h hh₁ hh₂ hgh - save refine hG (Sym2.mk_isDiag_iff.not.2 hgh) ⟨⟨a, b, c, ?_⟩, by simpa using And.intro hg₁ hh₁⟩ ⟨⟨d, e, f, ?_⟩, by simpa using And.intro hg₂ hh₂⟩ <;> simp [is3Clique_triple_iff, *]