From 1d4a722576d4d396076b108966fb07ea58d87d67 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 19 Apr 2024 03:12:51 +0000 Subject: [PATCH] chore: remove unnecessary classical! (#12255) `classical!` appears to never actually be necessary, and is just being used out of habit, and we can get rid of it to reduce the number of ways to say the same thing. Co-authored-by: Scott Morrison --- Mathlib/Data/Set/Pointwise/Finite.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Set/Pointwise/Finite.lean b/Mathlib/Data/Set/Pointwise/Finite.lean index ed96427ec4215..31d84e0b5ad6d 100644 --- a/Mathlib/Data/Set/Pointwise/Finite.lean +++ b/Mathlib/Data/Set/Pointwise/Finite.lean @@ -194,7 +194,7 @@ theorem card_pow_eq_card_pow_card_univ [∀ k : ℕ, DecidablePred (· ∈ S ^ k fun n h ↦ le_antisymm (mono (n + 1).le_succ) (key a⁻¹ (S ^ (n + 2)) (S ^ (n + 1)) _) replace h₂ : S ^ n * {a} = S ^ (n + 1) := by have : Fintype (S ^ n * Set.singleton a) := by - classical! + classical apply fintypeMul refine' Set.eq_of_subset_of_card_le _ (le_trans (ge_of_eq h) _) · exact mul_subset_mul Set.Subset.rfl (Set.singleton_subset_iff.mpr ha)