Vilin97 · github-actions · Sep 25, 2026 · Sep 25, 2026 · Sep 25, 2026 · Sep 25, 2026
diff --git a/LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/WinAsap.lean b/LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/WinAsap.lean
@@ -83,7 +83,8 @@ lemma num_spec : (G.residual (x.take h.num)).ExistsWinning (p.residual (x.take h
   rw [← _root_.not_imp_self (a := _ ≤ _)] --change after update
   intro hn; apply Nat.find_le
   have h' := h.num_spec
-  rwa [List.take_of_length_le] at * <;> omega
+  simpa only [List.take_of_length_le (by omega : x.length ≤ h.num),
+    List.take_length] using h'
 --the choices of Exists.choose here just depend on x|n, not x
 lemma take_num {y} : (x ++ y).take h.num = x.take h.num := by simp
 lemma extend (y : List A) (h : WinningPrefix G p x) : WinningPrefix G p (x ++ y) :=

diff --git a/LeanPool/AndersonConjecture/CompleteDomain/Domain.lean b/LeanPool/AndersonConjecture/CompleteDomain/Domain.lean
@@ -66,8 +66,8 @@ lemma ψ_kills_gen : ψHom ((X 0) ^ 2 - (X 1) * (X 2)) = 0 := by
   ring
 
 lemma conjI_le_ker_ψ : conjI ≤ RingHom.ker ψHom.toRingHom := by
-  rw [show conjI = Ideal.span {(X (0 : Fin 3) : MvPowerSeries (Fin 3) ℂ) ^ 2 -
-    X 1 * X 2} from rfl, Ideal.span_le]
+  rw [show conjI = Ideal.span {((X (0 : Fin 3) : MvPowerSeries (Fin 3) ℂ) ^ 2 -
+    X 1 * X 2)} from rfl, Ideal.span_le]
   intro x hx
   simp only [Set.mem_singleton_iff] at hx
   subst hx

diff --git a/LeanPool/BrauerGroupNew/BrauerOverR.lean b/LeanPool/BrauerGroupNew/BrauerOverR.lean
@@ -151,7 +151,7 @@ lemma BrauerOverR (A : CSA.{0, 0} ℝ) :
           rw [← e'.symm_apply_apply d, ← e'.symm_apply_apply d']
           conv_lhs => rw [← _root_.map_mul e'.symm, mul_comm, map_mul]
       rw [this]
-      exact SetLike.lt_iff_le_and_exists.2 ⟨fun _ _ ↦ ⟨⟩, ⟨e'.symm Complex.I, ⟨⟨⟩, by
+      exact IsConcreteLE.lt_iff_le_and_exists.2 ⟨fun _ _ ↦ ⟨⟩, ⟨e'.symm Complex.I, ⟨⟨⟩, by
         by_contra! mem
         change ∃(_ : _), _ = _ at mem
         obtain ⟨r, eq⟩ := mem

diff --git a/LeanPool/BrauerGroupNew/CrossProductAlgebra.lean b/LeanPool/BrauerGroupNew/CrossProductAlgebra.lean
@@ -327,7 +327,7 @@ lemma of_mul_incl (σ : Gal(K, F)) (c : K) : of f σ * incl f c = incl f (σ c)
   simp only [incl_apply, val_mul, val_of_val, val_smul, val_one, Finsupp.smul_single, smul_eq_mul,
     mulLinearMap_single_single, mul_one, map_mul, map_inv₀, one_mul,
     map_one_snd_of_isMulCocycle₂ Fact.out σ, AlgEquiv.smul_units_def, Units.coe_map,
-    MonoidHom.coe_coe, ne_eq, EmbeddingLike.map_eq_zero_iff, Units.ne_zero, not_false_eq_true,
+    MonoidHom.coe_ofClass, ne_eq, EmbeddingLike.map_eq_zero_iff, Units.ne_zero, not_false_eq_true,
     inv_mul_cancel_right₀, smul_one_mul]
 
 lemma sum_of (x : CrossProductAlgebra f) : x.val.sum (fun σ c ↦ c • (of f σ).val) = x := by

diff --git a/LeanPool/BrauerGroupNew/Morita/TensorProduct.lean b/LeanPool/BrauerGroupNew/Morita/TensorProduct.lean
@@ -301,7 +301,7 @@ abbrev e01 (M : TensorModule R A C) :
       · exact AddHom.id _
       · intro a m
         change a • m = (moduleAux R A C M (a ⊗ₜ[R] (1 : C))) m
-        simp
+        rw [moduleAux_apply, map_one, Module.End.one_apply]
     · exact id
     · exact congrFun rfl
     · exact congrFun rfl)) fun c ↦ by

diff --git a/LeanPool/BrauerGroupNew/Subfield/Defs.lean b/LeanPool/BrauerGroupNew/Subfield/Defs.lean
@@ -43,7 +43,7 @@ instance : SetLike (SubField R A) A where
   coe L := L.1
   coe_injective := SetLike.coe_injective.comp toSubalgebra_injective
 
-instance : PartialOrder (SubField R A) := .ofSetLike (SubField R A) A
+instance : PartialOrder (SubField R A) := .ofSetLike (SubField R A)
 
 lemma mem_carrier : a ∈ L.carrier ↔ a ∈ L := .rfl
 @[simp] lemma mem_toSubalgebra : a ∈ L.toSubalgebra ↔ a ∈ L := .rfl

diff --git a/LeanPool/BrauerGroupNew/ToSecond.lean b/LeanPool/BrauerGroupNew/ToSecond.lean
@@ -254,7 +254,7 @@ lemma conjFactorCompCoeff_inv (x : A.conjFactor σ) (y : A.conjFactor τ) (z : A
     A.ι ((conjFactorCompCoeff x y z)⁻¹) = z.1 * (y.1⁻¹ * x.1⁻¹) := by
   suffices eq : Units.map A.ι (conjFactorCompCoeffAsUnit x y z)⁻¹ = z.1 * (y.1⁻¹ * x.1⁻¹) by
     rw [Units.ext_iff] at eq
-    simp only [conjFactorCompCoeffAsUnit, Units.inv_mk, Units.coe_map, MonoidHom.coe_coe,
+    simp only [conjFactorCompCoeffAsUnit, Units.inv_mk, Units.coe_map, MonoidHom.coe_ofClass,
       AlgEquiv.mul_apply, Units.val_mul] at eq
     rw [← eq]
     congr 1
@@ -854,7 +854,7 @@ noncomputable def fromSnd :
             congr 1
             specialize hc σ τ
             simp only [AlgEquiv.smul_units_def, Pi.div_apply, Units.ext_iff, Units.val_mul,
-              Units.val_div_eq_div_val, Units.coe_map, MonoidHom.coe_coe] at hc
+              Units.val_div_eq_div_val, Units.coe_map, MonoidHom.coe_ofClass] at hc
             simp only [_root_.mul_assoc]
             congr 1
             rw [mul_comm (c σ).1, _root_.mul_assoc]

diff --git a/LeanPool/BruhatTits/Graph/GroupAction.lean b/LeanPool/BruhatTits/Graph/GroupAction.lean
@@ -268,8 +268,8 @@ lemma _root_.BruhatTits.Lattice.valuation_det_eq_one_of_mem_stabilizer
   obtain ⟨h, rfl⟩ := MulAction.exists_smul_eq (GL (Fin 2) K) (Lattice.standard R) L
   rw [stabilizer_smul_standard_eq_map_conj_subtype_range] at hg
   obtain ⟨k, ⟨k, rfl⟩, rfl⟩ := hg
-  simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulAut.conj_apply, map_mul, map_inv,
-    mul_inv_cancel_comm, Matrix.GeneralLinearGroup.val_det_apply,
+  simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_ofClass, MulAut.conj_apply, map_mul,
+    map_inv, mul_inv_cancel_comm, Matrix.GeneralLinearGroup.val_det_apply,
     Matrix.GeneralLinearGroup.val_map_apply, Subring.coe_subtype, Subring.coe_det]
   rw [← valuation_eq_one_iff]
   exact Matrix.isUnits_det_units k

diff --git a/LeanPool/BruhatTits/Lattice/Distance.lean b/LeanPool/BruhatTits/Lattice/Distance.lean
@@ -426,15 +426,15 @@ lemma unit_smul_eq (u : Rˣ) (M : BruhatTits.Lattice R) : (Units.map R.subtype u
   · intro hx
     simp only [Lattice.smul_module] at hx
     obtain ⟨y, hy, rfl⟩ := hx
-    simp only [Units.coe_map, MonoidHom.coe_coe, Subring.coe_subtype,
+    simp only [Units.coe_map, MonoidHom.coe_ofClass, Subring.coe_subtype,
       DistribSMul.toLinearMap_apply]
     exact Submodule.smul_mem _ u.val hy
   · intro hx
     simp only [Lattice.smul_module]
     refine ⟨u⁻¹ • x, ?_, ?_⟩
     · exact Submodule.smul_mem _ u.inv hx
-    · simp only [Units.coe_map, MonoidHom.coe_coe, Subring.coe_subtype, LinearMap.map_smul_of_tower,
-        DistribSMul.toLinearMap_apply]
+    · simp only [Units.coe_map, MonoidHom.coe_ofClass, Subring.coe_subtype,
+        LinearMap.map_smul_of_tower, DistribSMul.toLinearMap_apply]
       rw [← Subring.smul_def, Units.smul_def, smul_smul]
       simp
 

diff --git a/LeanPool/BruhatTits/Lattice/Quotient.lean b/LeanPool/BruhatTits/Lattice/Quotient.lean
@@ -300,7 +300,8 @@ lemma _root_.BruhatTits.Lattice.mapIntermediateSubmodule_inj_of
     apply Submodule.comap_mono
     exact hge₂
   have h' : Q₁.map p.mkQ = Q₂.map p.mkQ := by
-    rwa [← SetLike.coe_set_eq] at h ⊢
+    rw [← SetLike.coe_set_eq] at h ⊢
+    assumption
   have h'' : p.comapMkQRelIso.symm ⟨Q₁, hQ₁⟩ = p.comapMkQRelIso.symm ⟨Q₂, hQ₂⟩ := h'
   have h1 := p.comapMkQRelIso.symm.injective h''
   replace h1 : Q₁ = Q₂ := congrArg Subtype.val h1

diff --git a/LeanPool/BruhatTits/Utils/RingHom.lean b/LeanPool/BruhatTits/Utils/RingHom.lean
@@ -55,7 +55,7 @@ lemma GL.map_det (g : GL α R) : Matrix.GeneralLinearGroup.det (GL.map f g) =
     Units.map f (Matrix.GeneralLinearGroup.det g) := by
   ext
   simp only [map, RingHom.mapMatrix_apply, Units.inv_eq_val_inv, Matrix.coe_units_inv,
-    Matrix.GeneralLinearGroup.val_det_apply, Units.coe_map, MonoidHom.coe_coe]
+    Matrix.GeneralLinearGroup.val_det_apply, Units.coe_map, MonoidHom.coe_ofClass]
   symm
   apply RingHom.map_det
 

diff --git a/LeanPool/BruhatTits/Utils/ValuationRings.lean b/LeanPool/BruhatTits/Utils/ValuationRings.lean
@@ -285,7 +285,7 @@ lemma zaddVal'_eq_iff (n : ℤ) (x : Kˣ) :
     obtain ⟨y, hy⟩ := zaddVal'_spec ϖ hϖ x
     nth_rw 1 [← hu] at hy
     rw [Units.ext_iff] at hy
-    simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_coe, Subring.coe_subtype,
+    simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_ofClass, Subring.coe_subtype,
       Units.val_zpow_eq_zpow_val, Units.val_mk0] at hy
     apply unit_mul_zpow_congr_zpow hϖ hϖ y u
     exact hy.symm
@@ -306,7 +306,7 @@ lemma zaddVal_eq_iff (n : ℤ) (x : Kˣ) :
     obtain ⟨p, hp, y, hy⟩ := zaddVal_spec (R := R) x
     nth_rw 1 [← hu] at hy
     rw [Units.ext_iff] at hy
-    simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_coe, Subring.coe_subtype,
+    simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_ofClass, Subring.coe_subtype,
       Units.val_zpow_eq_zpow_val, Units.val_mk0] at hy
     apply unit_mul_zpow_congr_zpow hp hϖ y u
     exact hy.symm

diff --git a/LeanPool/CircuitComplexity/Internal/NF.lean b/LeanPool/CircuitComplexity/Internal/NF.lean
@@ -323,7 +323,7 @@ theorem card_true_of_flip_sensitive {N : Nat} (hN : 1 ≤ N)
       rw [Fintype.card_fun, Fintype.card_bool, Fintype.card_fin]] at h
     convert h using 2
     simp only [S_false]
-    congr 1; ext x; cases f x <;> simp
+    congr 1
   -- 2 * S_true.card = 2^N, so S_true.card = 2^{N-1}
   have : 2 ^ N = 2 * 2 ^ (N - 1) := by
     cases N with

diff --git a/LeanPool/ClassificationOfSurfaces/Moise/PolygonalArc.lean b/LeanPool/ClassificationOfSurfaces/Moise/PolygonalArc.lean
@@ -1676,8 +1676,8 @@ theorem resolvedSegment_inter_of_succ_eq (i j : Fin B.resolvedWalk.length)
     ext x
     simp []
   rw [himage, convexHull_singleton]
-  change {B.arrangementMesh.toPlaneComplex.position
-      (B.resolvedWalk.getVert (i.val + 1))} = {B.resolvedVertex i.succ}
+  change {(B.arrangementMesh.toPlaneComplex.position
+      (B.resolvedWalk.getVert (i.val + 1)))} = {B.resolvedVertex i.succ}
   rfl
 
 /-- The shifted affine edge parameters agree wherever two selected path edges meet. -/

diff --git a/LeanPool/Computability/Oracle.lean b/LeanPool/Computability/Oracle.lean
@@ -129,7 +129,10 @@ If a function is partial recursive, then it is recursive in every partial functi
 -/
 lemma recursiveIn_of_partrec (pF : Nat.Partrec f) : RecursiveIn O f := by
   induction pF with
-  | zero | succ | left | right => constructor
+  | zero => exact RecursiveIn.zero
+  | succ => exact RecursiveIn.succ
+  | left => exact RecursiveIn.left
+  | right => exact RecursiveIn.right
   | pair _ _ ih₁ ih₂ => exact RecursiveIn.pair ih₁ ih₂
   | comp _ _ ih₁ ih₂ => exact RecursiveIn.comp ih₁ ih₂
   | prec _ _ ih₁ ih₂ => exact RecursiveIn.prec ih₁ ih₂
@@ -252,7 +255,10 @@ theorem recursiveIn_mono {O₁ O₂ : Set (ℕ →. ℕ)} (hsub : O₁ ⊆ O₂)
       RecursiveIn O₁ g → RecursiveIn O₂ g := by
   intro hg
   induction hg with
-  | zero | succ | left | right => constructor
+  | zero => exact RecursiveIn.zero
+  | succ => exact RecursiveIn.succ
+  | left => exact RecursiveIn.left
+  | right => exact RecursiveIn.right
   | oracle g hg => exact RecursiveIn.oracle g (hsub hg)
   | pair _ _ ih₁ ih₂ => exact RecursiveIn.pair ih₁ ih₂
   | comp _ _ ih₁ ih₂ => exact RecursiveIn.comp ih₁ ih₂
@@ -262,7 +268,10 @@ theorem recursiveIn_mono {O₁ O₂ : Set (ℕ →. ℕ)} (hsub : O₁ ⊆ O₂)
 theorem RecursiveIn_subst {O O' : Set (ℕ →. ℕ)} {f : ℕ →. ℕ} (hf : RecursiveIn O f)
     (hO : ∀ g, g ∈ O → RecursiveIn O' g) : RecursiveIn O' f := by
   induction hf with
-  | zero | succ | left | right => constructor
+  | zero => exact RecursiveIn.zero
+  | succ => exact RecursiveIn.succ
+  | left => exact RecursiveIn.left
+  | right => exact RecursiveIn.right
   | oracle g hg => exact hO g hg
   | pair _ _ ihf ihg => exact .pair ihf ihg
   | comp _ _ ihf ihg => exact .comp ihf ihg

diff --git a/LeanPool/Computability/TuringDegree.lean b/LeanPool/Computability/TuringDegree.lean
@@ -91,7 +91,10 @@ instance : Std.Refl TuringReducible where refl _ := .rfl
 
 theorem TuringReducible.trans (hg : f ≤ᵀ g) (hh : g ≤ᵀ h) : f ≤ᵀ h := by
   induction hg with
-  | zero | succ | left | right => constructor
+  | zero => exact RecursiveIn.zero
+  | succ => exact RecursiveIn.succ
+  | left => exact RecursiveIn.left
+  | right => exact RecursiveIn.right
   | oracle g' hg => rw [hg]; exact hh
   | pair _ _ ih₁ ih₂ => exact RecursiveIn.pair ih₁ ih₂
   | comp _ _ ih₁ ih₂ => exact RecursiveIn.comp ih₁ ih₂

diff --git a/LeanPool/DemazureProduct/Avoiding321.lean b/LeanPool/DemazureProduct/Avoiding321.lean
@@ -785,7 +785,7 @@ theorem eq_s_of_lel
     rw [v_eq_x]; simp
   suffices ⟨x, v⟩ ∈ invSet β ↔ ⟨x, v⟩ ∈ invSet τ by
     rw [β.inv_iff_le x_lt_v, τ.inv_iff_le x_lt_v] at this
-    constructor <;> (intro h; contrapose! h; rwa [this] at *)
+    constructor <;> (intro h; contrapose! h; rw [this] at *; assumption)
   have nested : ⟨x, v⟩ ≼ ⟨u, v⟩ := by constructor <;> linarith
   exact inv_of_lel_iff h_321a h_L uv_inv nested
 
@@ -808,7 +808,7 @@ lemma eq_s'_of_lel
     constructor <;> (intro h; linarith)
   suffices ⟨u, x⟩ ∈ invSet β ↔ ⟨u, x⟩ ∈ invSet τ by
     rw [β.inv_iff_lt u_le_x, τ.inv_iff_lt u_le_x] at this
-    constructor <;> (intro h; contrapose! h; rwa [this] at *)
+    constructor <;> (intro h; contrapose! h; rw [this] at *; assumption)
   have nested : ⟨u, x⟩ ≼ ⟨u, v⟩ := by constructor <;> linarith
   exact inv_of_lel_iff h_321a h_L uv_inv nested
 

diff --git a/LeanPool/Dilatations/IteratedRings.lean b/LeanPool/Dilatations/IteratedRings.lean
@@ -187,8 +187,8 @@ lemma hgen_rho (i : M.index) :
           rw [Ideal.map_span, Set.image_singleton]
   · have h : Ideal.map (algebraMap B224 C224)
         ((Multicenter.complement M K).ideal (⟨i, hi⟩ : (Kᶜ : Set M.index))) ≤
-          Ideal.span {(algebraMap B224 C224)
-            ((Multicenter.complement M K).elem (⟨i, hi⟩ : (Kᶜ : Set M.index)))} :=
+          Ideal.span {((algebraMap B224 C224)
+            ((Multicenter.complement M K).elem (⟨i, hi⟩ : (Kᶜ : Set M.index))))} :=
       (gen_iff_le (Multicenter.complement M K) (⟨i, hi⟩ : (Kᶜ : Set M.index))).mp
         (reciprocal_for_univ (Multicenter.complement M K) (AlgHom.id B224 C224)
           (⟨i, hi⟩ : (Kᶜ : Set M.index)))

diff --git a/LeanPool/DomainTheory/ContinuousLattice/ScottMaps.lean b/LeanPool/DomainTheory/ContinuousLattice/ScottMaps.lean
@@ -67,8 +67,7 @@ theorem continuous_preservesDirectedSup {f : D → D'}
       (Topology.IsScott.scottContinuousOn_iff_continuous (α := WithScott D) (D := univ)
         (fun _ _ _ => trivial)).2 hf'
   intro S hS hSdir
-  have h := hsc hS hSdir (isLUB_sSup S)
-  simp only [Function.comp_def, WithScott.toScott, WithScott.ofScott] at h
+  have h : IsLUB (f '' S) (f (sSup S)) := hsc hS hSdir (isLUB_sSup S)
   exact h.sSup_eq.symm
 
 /-- **Scott 1972, Proposition 2.5.** Scott continuity ↔ preservation of directed

diff --git a/LeanPool/DomainTheory/Neighborhood/Exercise221.lean b/LeanPool/DomainTheory/Neighborhood/Exercise221.lean
@@ -113,9 +113,9 @@ theorem singleton_cone_nd (σ τ : Str) :
 theorem singleton_singleton_nd (σ τ : Str) :
     ({σ} : Set Str) ⊆ ({τ} : Set Str) ∨ ({τ} : Set Str) ⊆ ({σ} : Set Str) ∨
       ({σ} : Set Str) ∩ ({τ} : Set Str) = ∅ := by
-  rcases (inferInstance : Decidable (σ = τ)) with h | h
-  · simp_all
+  by_cases h : σ = τ
   · subst h; exact Or.inl subset_rfl
+  · simp_all
 
 /-- **`𝒞` is pairwise nested-or-disjoint.** Cone/cone is the `𝔹` trichotomy; the
 mixed and

diff --git a/LeanPool/DomainTheory/Neighborhood/Recursive.lean b/LeanPool/DomainTheory/Neighborhood/Recursive.lean
@@ -431,9 +431,9 @@ theorem RecDecidable.not {p : ℕ → Prop} (hp : RecDecidable p) : RecDecidable
 equality on `ℕ`); useful for choice-free De Morgan. -/
 theorem RecDecidable.em {p : ℕ → Prop} (hp : RecDecidable p) (n : ℕ) : p n ∨ ¬ p n := by
   obtain ⟨f, _, hfe⟩ := hp
-  rcases Nat.decEq (f n) 1 with h | h
-  · exact Or.inr (fun hp => h ((hfe n).mp hp))
+  by_cases h : f n = 1
   · exact Or.inl ((hfe n).mpr h)
+  · exact Or.inr (fun hp => h ((hfe n).mp hp))
 
 /-- **Disjunction.** Recursive decidability is closed under `∨`, via choice-free
 De Morgan

diff --git a/LeanPool/DomainTheory/Neighborhood/Theorem74.lean b/LeanPool/DomainTheory/Neighborhood/Theorem74.lean
@@ -241,11 +241,11 @@ master. -/
 /-- Choice-free three-way split of a tag `n ∈ {0, 1, ≥2}` (via `Nat.decEq`, not
 classical `em`). -/
 theorem tag_trichotomy (n : ℕ) : n = 0 ∨ n = 1 ∨ (n ≠ 0 ∧ n ≠ 1) := by
-  rcases Nat.decEq n 0 with h | h
-  · rcases Nat.decEq n 1 with h' | h'
-    · exact Or.inr (Or.inr ⟨h, h'⟩)
-    · exact Or.inr (Or.inl h')
+  by_cases h : n = 0
   · exact Or.inl h
+  · by_cases h' : n = 1
+    · exact Or.inr (Or.inl h')
+    · exact Or.inr (Or.inr ⟨h, h'⟩)
 
 section Sum
 

diff --git a/LeanPool/Duality/LinearProgramming.lean b/LeanPool/Duality/LinearProgramming.lean
@@ -623,7 +623,8 @@ lemma ValidELP.unbounded_of_feasible_of_neg (P : ValidELP I J F) (hP : P.IsFeasi
       | ⊥ =>
         refine ⟨⊥, ⟨xₚ, hxₚ, ?_⟩, bot_le⟩
         change hcx₀ to P.c ᵥ⬝ x₀ = ⊥
-        rwa [←dotWeig_eq_bot] at hcx₀ ⊢
+        rw [←dotWeig_eq_bot] at hcx₀ ⊢
+        assumption
       | ⊤ =>
         exfalso
         rw [hcx₀] at hx₀

diff --git a/LeanPool/FelConjecture/Solution.lean b/LeanPool/FelConjecture/Solution.lean
@@ -188,17 +188,18 @@ lemma partition_sum {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S
     ∑ k ∈ (Finset.range (n +
       1)).filter (fun k => !(Classical.propDecidable (k ∈ S.carrier)).decide),
       (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) := by
-  have h := @Finset.sum_filter_add_sum_filter_not _ _ _ (Finset.range (n + 1))
-    (fun k => k ∈ S.carrier) (Classical.decPred _) (fun x => Classical.dec _)
-    (fun k => (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)))
-  rw [← h]
-  congr 1
-  · congr 1
+  classical
+  have hmem : (Finset.range (n + 1)).filter
+      (fun k => (Classical.propDecidable (k ∈ S.carrier)).decide) =
+      (Finset.range (n + 1)).filter (fun k => k ∈ S.carrier) := by
     ext k
     simp only [Finset.mem_filter, decide_eq_true_eq]
-  · congr 1
+  have hnotmem : (Finset.range (n + 1)).filter
+      (fun k => !(Classical.propDecidable (k ∈ S.carrier)).decide) =
+      (Finset.range (n + 1)).filter (fun k => k ∉ S.carrier) := by
     ext k
     simp only [Finset.mem_filter, Bool.not_eq_true', decide_eq_false_iff_not]
+  rw [hmem, hnotmem, Finset.sum_filter_add_sum_filter_not]
 
 lemma filter_not_carrier_eq_gaps {S : NumericalSemigroup} (n : ℕ) :
     (Finset.range (n + 1)).filter (fun k => !(Classical.propDecidable (k ∈ S.carrier)).decide) =

diff --git a/LeanPool/Flean/Subnorm.lean b/LeanPool/Flean/Subnorm.lean
@@ -119,7 +119,6 @@ lemma subnormal_round_coe (r : IntRounder) [rh : ValidRounder r]
   · exact this
   nth_rw 4 [show m = r false m by symm; apply ValidRounder.leftInverse]
   congr
-  · simp_all
   have hprec : (C.prec : ℚ) ≠ 0 := by
     norm_cast; linarith [C.prec_pos]
   rw [abs_of_nonneg (by positivity), mul_assoc, mul_assoc, <-mul_assoc (2 ^ _),

diff --git a/LeanPool/FltRegular/CaseII/AuxLemmas.lean b/LeanPool/FltRegular/CaseII/AuxLemmas.lean
@@ -90,7 +90,6 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDedekindDomain
               · exact hx.ne_zero
               · rw [Ne, Ideal.span_singleton_eq_bot]
                 exact hx.ne_zero
-            · rwa [Nat.pos_iff_ne_zero, ← Nat.one_le_iff_ne_zero]
           rwa [← e, mul_comm, ← dvd_gcd_mul_iff_dvd_mul, this, one_mul] at hb
   rw [isPrincipal_iff] at h
   obtain ⟨a, ha⟩ := h

diff --git a/LeanPool/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/LeanPool/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
@@ -71,8 +71,8 @@ lemma unit_inv_conj_not_neg_zeta_runity_aux (u : (𝓞 K)ˣ) [Fact (p.Prime)] (h
   let _ := IsCyclotomicExtension.Rat.isCMField (S := {p}) K ⟨p, rfl, hp⟩
   have hmap := Units.coe_map_inv (N := 𝓞 K ⧸ I) (algebraMap (𝓞 K) (𝓞 K ⧸ I))
     (unitsComplexConj K u)
-  rw [unitsMulComplexConjInv_apply, Units.val_mul, map_mul, ← MonoidHom.coe_coe, ← hmap,
-    Units.mul_inv_eq_one, Units.coe_map, MonoidHom.coe_coe]
+  rw [unitsMulComplexConjInv_apply, Units.val_mul, map_mul, ← MonoidHom.coe_ofClass, ← hmap,
+    Units.mul_inv_eq_one, Units.coe_map, MonoidHom.coe_ofClass]
   exact (RingHom.congr_fun (quotient_zero_sub_one_comp_aut hζ
     (ringOfIntegersComplexConj K).toRingEquiv.toRingHom) (u : 𝓞 K)).symm