Merge remote-tracking branch 'origin/master' into bump/v4.22.0

mathlib4-bot · mathlib4-bot · commit 7e33fba32014 · 2025-06-17T07:00:01.000Z
diff --git a/Mathlib/Algebra/Order/Archimedean/Class.lean b/Mathlib/Algebra/Order/Archimedean/Class.lean
@@ -97,7 +97,7 @@ theorem le_def {a b : MulArchimedeanOrder M} : a ≤ b ↔ ∃ n, |b.val|ₘ ≤
 @[to_additive]
 theorem lt_def {a b : MulArchimedeanOrder M} : a < b ↔ ∀ n, |b.val|ₘ ^ n < |a.val|ₘ := .rfl
 
-variable {M: Type*}
+variable {M : Type*}
 variable [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M}
 
 @[to_additive]
@@ -299,7 +299,7 @@ theorem mk_mul_eq_mk_right (h : mk b < mk a) : mk (a * b) = mk b :=
 /-- The product over a set of an elements in distinct classes is in the lowest class. -/
 @[to_additive "The sum over a set of an elements in distinct classes is in the lowest class."]
 theorem mk_prod {ι : Type*} [LinearOrder ι] {s : Finset ι} (hnonempty : s.Nonempty)
-    {a : ι → M}  :
+    {a : ι → M} :
     StrictMonoOn (mk ∘ a) s → mk (∏ i ∈ s, (a i)) = mk (a (s.min' hnonempty)) := by
   induction hnonempty using Finset.Nonempty.cons_induction with
   | singleton i => simp
diff --git a/Mathlib/GroupTheory/RegularWreathProduct.lean b/Mathlib/GroupTheory/RegularWreathProduct.lean
@@ -236,7 +236,7 @@ lemma iteratedWreathToPermHomInj (G : Type*) [Group G] :
         (RegularWreathProduct.toPermInj (IteratedWreathProduct G n) G (Fin n → G))
 
 /-- The encoding of the Sylow `p`-subgroups of `Perm α` as an iterated wreath product. -/
-noncomputable def Sylow.mulEquivIteratedWreathProduct  (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ)
+noncomputable def Sylow.mulEquivIteratedWreathProduct (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ)
     (α : Type*) [Finite α] (hα : Nat.card α = p ^ n)
     (G : Type*) [Group G] [Finite G] (hG : Nat.card G = p)
     (P : Sylow p (Equiv.Perm α)) :
diff --git a/Mathlib/NumberTheory/RamificationInertia/Galois.lean b/Mathlib/NumberTheory/RamificationInertia/Galois.lean
@@ -38,7 +38,7 @@ Assume `B / A` is a finite extension of Dedekind domains, `K` is the fraction ri
 
 -/
 
-open Algebra
+open Algebra Pointwise
 
 attribute [local instance] FractionRing.liftAlgebra
 
@@ -64,19 +64,20 @@ noncomputable def inertiaDegIn {A : Type*} [CommRing A] (p : Ideal A)
 section MulAction
 
 variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A}
+  {G : Type*} [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
 
-instance : MulAction (B ≃ₐ[A] B) (primesOver p B) where
-  smul σ Q := primesOver.mk p (map σ Q.1)
-  one_smul Q := Subtype.val_inj.mp (map_id Q.1)
-  mul_smul σ τ Q := Subtype.val_inj.mp (Q.1.map_map τ.toRingHom σ.toRingHom).symm
+instance : MulAction G (primesOver p B) where
+  smul σ Q := primesOver.mk p (σ • Q.1)
+  one_smul Q := Subtype.ext (one_smul G Q.1)
+  mul_smul σ τ Q := Subtype.ext (mul_smul σ τ Q.1)
 
 @[simp]
-theorem coe_smul_primesOver (σ : B ≃ₐ[A] B) (P : primesOver p B): (σ • P).1 = map σ P :=
+theorem coe_smul_primesOver (σ : G) (P : primesOver p B) : (σ • P).1 = σ • P.1 :=
   rfl
 
 @[simp]
-theorem coe_smul_primesOver_mk (σ : B ≃ₐ[A] B) (P : Ideal B) [P.IsPrime] [P.LiesOver p] :
-    (σ • primesOver.mk p P).1 = map σ P :=
+theorem coe_smul_primesOver_mk (σ : G) (P : Ideal B) [P.IsPrime] [P.LiesOver p] :
+    (σ • primesOver.mk p P).1 = σ • P :=
   rfl
 
 variable (K L : Type*) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L]
diff --git a/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean b/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean
@@ -30,8 +30,8 @@ $\mathrm{H}^n(G, A) \cong \mathrm{Ext}^n(k, A),$ where $\mathrm{Ext}$ is taken i
 `Rep k G`.
 
 To talk about cohomology in low degree, please see the file
-`Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean`, which gives simpler
-expressions for `H⁰`, `H¹`, `H²` than the definition `groupCohomology` in this file.
+`Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean`, which provides API
+specialized to `H⁰`, `H¹`, `H²`.
 
 ## Main definitions
 
@@ -54,8 +54,6 @@ possible scalar action diamonds.
 
 ## TODO
 
-* API for cohomology in low degree: $\mathrm{H}^0, \mathrm{H}^1$ and $\mathrm{H}^2.$ For example,
-  the inflation-restriction exact sequence.
 * The long exact sequence in cohomology attached to a short exact sequence of representations.
 * Upgrading `groupCohomologyIsoExt` to an isomorphism of derived functors.
 * Profinite cohomology.
diff --git a/Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean b/Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean
@@ -231,51 +231,55 @@ section H0
 
 /-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
 this is induced map `Aᴴ ⟶ Bᴳ`. -/
-noncomputable abbrev H0Map : H0 A ⟶ H0 B :=
-  ModuleCat.ofHom <| LinearMap.codRestrict _ (φ.hom.hom ∘ₗ A.ρ.invariants.subtype)
-    fun ⟨c, hc⟩ g => by simpa [hc (f g)] using (hom_comm_apply φ g c).symm
+@[deprecated (since := "2025-06-09")]
+alias H0Map := map
 
-@[simp]
-theorem H0Map_id : H0Map (MonoidHom.id _) (𝟙 A) = 𝟙 _ := by
-  rfl
+@[deprecated (since := "2025-06-09")]
+alias H0Map_id := map_id
 
-@[reassoc]
-theorem H0Map_comp {G H K : Type u} [Group G] [Group H] [Group K]
-    {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H)
-    (φ : (Action.res _ f).obj A ⟶ B) (ψ : (Action.res _ g).obj B ⟶ C) :
-    H0Map (f.comp g) ((Action.res _ g).map φ ≫ ψ) = H0Map f φ ≫ H0Map g ψ :=
-  rfl
+@[deprecated (since := "2025-06-09")]
+alias H0Map_comp := map_comp
 
-@[reassoc]
-theorem H0Map_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) :
-    H0Map (MonoidHom.id G) (φ ≫ ψ) = H0Map (MonoidHom.id G) φ ≫ H0Map (MonoidHom.id G) ψ := rfl
+@[deprecated (since := "2025-06-09")]
+alias H0Map_id_comp := map_id_comp
 
-theorem H0Map_id_eq_invariantsFunctor_map {A B : Rep k G} (f : A ⟶ B) :
-    H0Map (MonoidHom.id G) f = (invariantsFunctor k G).map f := by
-  rfl
+variable [DecidableEq G] [DecidableEq H]
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
-lemma H0Map_comp_f :
-    H0Map f φ ≫ (shortComplexH0 B).f = (shortComplexH0 A).f ≫ φ.hom := by
-  ext
-  simp [shortComplexH0]
+theorem map_H0Iso_hom_f :
+    map f φ 0 ≫ (H0Iso B).hom ≫ (shortComplexH0 B).f =
+      (H0Iso A).hom ≫ (shortComplexH0 A).f ≫ φ.hom := by
+  simp [← cancel_epi (π _ _)]
 
-instance mono_H0Map_of_mono {A B : Rep k G} (f : A ⟶ B) [Mono f] :
-    Mono (H0Map (MonoidHom.id G) f) :=
-  (ModuleCat.mono_iff_injective _).2 fun _ _ hxy => Subtype.ext <|
-    (mono_iff_injective f).1 ‹_› (Subtype.ext_iff.1 hxy)
+@[deprecated (since := "2025-06-09")]
+alias H0Map_comp_f := map_H0Iso_hom_f
 
-variable [DecidableEq G] [DecidableEq H] in
 @[reassoc (attr := simp), elementwise (attr := simp)]
-theorem cocyclesMap_comp_isoZeroCocycles_hom :
-    cocyclesMap f φ 0 ≫ (isoZeroCocycles B).hom = (isoZeroCocycles A).hom ≫ H0Map f φ := by
-  simp [← cancel_mono (shortComplexH0 B).f]
+theorem map_id_comp_H0Iso_hom {A B : Rep k G} (f : A ⟶ B) :
+    map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom = (H0Iso A).hom ≫ (invariantsFunctor k G).map f := by
+  simp only [← cancel_mono (shortComplexH0 B).f, Category.assoc, map_H0Iso_hom_f]
+  rfl
 
-variable [DecidableEq G] [DecidableEq H] in
-@[reassoc (attr := simp), elementwise (attr := simp)]
-theorem map_comp_isoH0_hom :
-    map f φ 0 ≫ (isoH0 B).hom = (isoH0 A).hom ≫ H0Map f φ := by
-  simp [← cancel_epi (π _ _)]
+@[deprecated (since := "2025-06-09")]
+alias H0Map_id_eq_invariantsFunctor_map := map_id_comp_H0Iso_hom
+
+instance mono_map_0_of_mono {A B : Rep k G} (f : A ⟶ B) [Mono f] :
+    Mono (map (MonoidHom.id G) f 0) where
+  right_cancellation g h hgh := by
+    simp only [← cancel_mono (H0Iso B).hom, Category.assoc, map_id_comp_H0Iso_hom] at hgh
+    simp_all [cancel_mono]
+
+@[deprecated (since := "2025-06-09")]
+alias mono_H0Map_of_mono := mono_map_0_of_mono
+
+@[reassoc, elementwise]
+theorem cocyclesMap_zeroIsoCocycles_hom_f :
+    cocyclesMap f φ 0 ≫ (zeroCocyclesIso B).hom ≫ (shortComplexH0 B).f =
+      (zeroCocyclesIso A).hom ≫ (shortComplexH0 A).f ≫ φ.hom := by
+  simp
+
+@[deprecated (since := "2025-06-12")]
+alias cocyclesMap_comp_isoZeroCocycles_hom := cocyclesMap_zeroIsoCocycles_hom_f
 
 end H0
 section H1
@@ -356,74 +360,63 @@ theorem mapOneCocycles_one (φ : (Action.res _ 1).obj A ⟶ B) :
 
 /-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
 this is induced map `H¹(H, A) ⟶ H¹(G, B)`. -/
-noncomputable abbrev H1Map : H1 A ⟶ H1 B :=
-  ShortComplex.leftHomologyMap' (mapShortComplexH1 f φ)
-    (shortComplexH1 A).moduleCatLeftHomologyData (shortComplexH1 B).moduleCatLeftHomologyData
+@[deprecated (since := "2025-06-09")]
+alias H1Map := map
 
-@[simp]
-theorem H1Map_id : H1Map (MonoidHom.id _) (𝟙 A) = 𝟙 _ := by
-  simp only [H1Map, shortComplexH1, mapShortComplexH1_id, leftHomologyMap'_id]
-  rfl
+@[deprecated (since := "2025-6-09")]
+alias H1Map_id := map_id
 
-@[reassoc]
-theorem H1Map_comp {G H K : Type u} [Group G] [Group H] [Group K]
-    {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H)
-    (φ : (Action.res _ f).obj A ⟶ B) (ψ : (Action.res _ g).obj B ⟶ C) :
-    H1Map (f.comp g) ((Action.res _ g).map φ ≫ ψ) = H1Map f φ ≫ H1Map g ψ := by
-  simpa [H1Map, shortComplexH1, mapShortComplexH1_comp] using leftHomologyMap'_comp ..
+@[deprecated (since := "2025-06-09")]
+alias H1Map_comp := map_comp
 
-@[reassoc]
-theorem H1Map_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) :
-    H1Map (MonoidHom.id G) (φ ≫ ψ) = H1Map (MonoidHom.id G) φ ≫ H1Map (MonoidHom.id G) ψ :=
-  H1Map_comp (MonoidHom.id G) (MonoidHom.id G) _ _
+@[deprecated (since := "2025-06-09")]
+alias H1Map_id_comp := map_id_comp
 
-@[reassoc, elementwise]
-lemma H1π_comp_H1Map :
-    H1π A ≫ H1Map f φ = mapOneCocycles f φ ≫ H1π B := by
-  simp
+variable [DecidableEq G] [DecidableEq H]
 
-variable [DecidableEq G] [DecidableEq H] in
 @[reassoc (attr := simp), elementwise (attr := simp)]
-lemma map_comp_isoH1_hom :
-    map f φ 1 ≫ (isoH1 B).hom = (isoH1 A).hom ≫ H1Map f φ := by
-  simp [← cancel_epi (π _ _), H1Map, Category.assoc]
+lemma H1π_comp_map :
+    H1π A ≫ map f φ 1 = mapOneCocycles f φ ≫ H1π B := by
+  simp [H1π, Iso.inv_comp_eq, ← cocyclesMap_comp_isoOneCocycles_hom_assoc]
+
+@[deprecated (since := "2025-06-12")]
+alias H1π_comp_H1Map := H1π_comp_map
 
 @[simp]
-theorem H1Map_one (φ : (Action.res _ 1).obj A ⟶ B) :
-    H1Map 1 φ = 0 := by
+theorem map_1_one (φ : (Action.res _ 1).obj A ⟶ B) :
+    map 1 φ 1 = 0 := by
   simp [← cancel_epi (H1π _)]
 
+@[deprecated (since := "2025-06-09")]
+alias H1Map_one := map_1_one
+
 section InfRes
 
-variable (A : Rep k G) (S : Subgroup G) [S.Normal]
+variable (A : Rep k G) (S : Subgroup G) [S.Normal] [DecidableEq (G ⧸ S)]
 
 /-- The short complex `H¹(G ⧸ S, A^S) ⟶ H¹(G, A) ⟶ H¹(S, A)`. -/
 @[simps X₁ X₂ X₃ f g]
 noncomputable def H1InfRes :
     ShortComplex (ModuleCat k) where
-  X₁ := H1 (A.quotientToInvariants S)
-  X₂ := H1 A
-  X₃ := H1 ((Action.res _ S.subtype).obj A)
-  f := H1Map (QuotientGroup.mk' S) (subtype ..)
-  g := H1Map S.subtype (𝟙 _)
-  zero := by
-    rw [← H1Map_comp, Category.comp_id,
-      congr (QuotientGroup.mk'_comp_subtype S) H1Map, H1Map_one]
-    rintro g x hx ⟨s, hs⟩
-    simpa using congr(A.ρ g $(hx ⟨(g⁻¹ * s * g), Subgroup.Normal.conj_mem' ‹_› s hs g⟩))
+  X₁ := groupCohomology (A.quotientToInvariants S) 1
+  X₂ := groupCohomology A 1
+  X₃ := groupCohomology ((Action.res _ S.subtype).obj A) 1
+  f := map (QuotientGroup.mk' S) (subtype _ _ <| le_comap_invariants A.ρ S) 1
+  g := map S.subtype (𝟙 _) 1
+  zero := by rw [← map_comp, Category.comp_id, congr (QuotientGroup.mk'_comp_subtype S)
+    (fun f φ => map f φ 1), map_1_one]
 
 /-- The inflation map `H¹(G ⧸ S, A^S) ⟶ H¹(G, A)` is a monomorphism. -/
 instance : Mono (H1InfRes A S).f := by
   rw [ModuleCat.mono_iff_injective, injective_iff_map_eq_zero]
   intro x hx
   induction x using H1_induction_on with | @h x =>
-  simp_all only [H1InfRes_X₂, H1InfRes_X₁, H1InfRes_f, H1π_comp_H1Map_apply (QuotientGroup.mk' S),
-    Submodule.Quotient.mk_eq_zero, moduleCatLeftHomologyData_H]
-  rcases hx with ⟨y, hy⟩
-  refine ⟨⟨y, fun s => ?_⟩, Subtype.ext <| funext fun g => Quotient.inductionOn' g
-    fun g => Subtype.ext <| congr_fun (Subtype.ext_iff.1 hy) g⟩
-  simpa [coe_mapOneCocycles (x := x), sub_eq_zero, LinearMap.codRestrict, shortComplexH1,
-    (QuotientGroup.eq_one_iff s.1).2 s.2] using congr_fun (Subtype.ext_iff.1 hy) s.1
+  simp_all only [H1InfRes_X₂, H1InfRes_X₁, H1InfRes_f, H1π_comp_map_apply (QuotientGroup.mk' S)]
+  rcases (H1π_eq_zero_iff _).1 hx with ⟨y, hy⟩
+  refine (H1π_eq_zero_iff _).2 ⟨⟨y, fun s => ?_⟩, funext fun g => QuotientGroup.induction_on g
+    fun g => Subtype.ext <| by simpa [-SetLike.coe_eq_coe] using congr_fun hy g⟩
+  simpa [coe_mapOneCocycles (x := x), sub_eq_zero, (QuotientGroup.eq_one_iff s.1).2 s.2] using
+    congr_fun hy s.1
 
 /-- Given a `G`-representation `A` and a normal subgroup `S ≤ G`, the short complex
 `H¹(G ⧸ S, A^S) ⟶ H¹(G, A) ⟶ H¹(S, A)` is exact. -/
@@ -432,12 +425,11 @@ lemma H1InfRes_exact : (H1InfRes A S).Exact := by
   intro x hx
   induction x using H1_induction_on with | @h x =>
   simp_all only [H1InfRes_X₂, H1InfRes_X₃, H1InfRes_g, H1InfRes_X₁, LinearMap.mem_ker,
-    H1π_comp_H1Map_apply S.subtype, Submodule.Quotient.mk_eq_zero, H1InfRes_f,
-    moduleCatLeftHomologyData_H]
-  rcases hx with ⟨(y : A), hy⟩
+    H1π_comp_map_apply S.subtype, H1InfRes_f]
+  rcases (H1π_eq_zero_iff _).1 hx with ⟨(y : A), hy⟩
   have h1 := (mem_oneCocycles_iff x).1 x.2
   have h2 : ∀ s ∈ S, x s = A.ρ s y - y :=
-    fun s hs => (groupCohomology.oneCocycles_ext_iff.1 hy ⟨s, hs⟩).symm
+    fun s hs => funext_iff.1 hy.symm ⟨s, hs⟩
   refine ⟨H1π _ ⟨fun g => Quotient.liftOn' g (fun g => ⟨x.1 g - A.ρ g y + y, ?_⟩) ?_, ?_⟩, ?_⟩
   · intro s
     calc
@@ -460,12 +452,10 @@ lemma H1InfRes_exact : (H1InfRes A S).Exact := by
     apply Subtype.ext
     simp [← QuotientGroup.mk_mul, h1 g h, sub_add_eq_add_sub, add_assoc]
   · symm
-    simp only [moduleCatLeftHomologyData_H, moduleCatLeftHomologyData_π_hom,
-      Submodule.mkQ_apply, H1π_comp_H1Map_apply, Submodule.Quotient.eq]
+    simp only [H1π_comp_map_apply, H1π_eq_iff (A := A)]
     use y
-    refine Subtype.ext <| funext fun g => ?_
-    simp only [LinearMap.codRestrict_apply, AddSubgroupClass.coe_sub]
-    simp [shortComplexH1, coe_mapOneCocycles (QuotientGroup.mk' S),
+    ext g
+    simp [coe_mapOneCocycles (QuotientGroup.mk' S),
       oneCocycles.coe_mk (A := A.quotientToInvariants S), ← sub_sub]
 
 end InfRes
@@ -541,37 +531,26 @@ lemma cocyclesMap_comp_isoTwoCocycles_hom :
 
 /-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
 this is induced map `H²(H, A) ⟶ H²(G, B)`. -/
-noncomputable abbrev H2Map : H2 A ⟶ H2 B :=
-  ShortComplex.leftHomologyMap' (mapShortComplexH2 f φ)
-    (shortComplexH2 A).moduleCatLeftHomologyData (shortComplexH2 B).moduleCatLeftHomologyData
+@[deprecated (since := "2025-06-09")]
+alias H2Map := map
 
-@[simp]
-theorem H2Map_id : H2Map (MonoidHom.id _) (𝟙 A) = 𝟙 _ := by
-  simp only [H2Map, shortComplexH2, mapShortComplexH2_id, leftHomologyMap'_id]
-  rfl
+@[deprecated (since := "2025-06-09")]
+alias H2Map_id := map_id
 
-@[reassoc]
-theorem H2Map_comp {G H K : Type u} [Group G] [Group H] [Group K]
-    {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H)
-    (φ : (Action.res _ f).obj A ⟶ B) (ψ : (Action.res _ g).obj B ⟶ C) :
-    H2Map (f.comp g) ((Action.res _ g).map φ ≫ ψ) = H2Map f φ ≫ H2Map g ψ := by
-  simpa [H2Map, shortComplexH2, mapShortComplexH2_comp] using leftHomologyMap'_comp ..
+@[deprecated (since := "2025-06-09")]
+alias H2Map_comp := map_comp
 
-@[reassoc]
-theorem H2Map_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) :
-    H2Map (MonoidHom.id G) (φ ≫ ψ) = H2Map (MonoidHom.id G) φ ≫ H2Map (MonoidHom.id G) ψ :=
-  H2Map_comp (MonoidHom.id G) (MonoidHom.id G) _ _
-
-@[reassoc, elementwise]
-lemma H2π_comp_H2Map :
-    H2π A ≫ H2Map f φ = mapTwoCocycles f φ ≫ H2π B := by
-  simp
+@[deprecated (since := "2025-06-09")]
+alias H2Map_id_comp := map_id_comp
 
 variable [DecidableEq G] [DecidableEq H] in
 @[reassoc (attr := simp), elementwise (attr := simp)]
-lemma map_comp_isoH2_hom :
-    map f φ 2 ≫ (isoH2 B).hom = (isoH2 A).hom ≫ H2Map f φ := by
-  simp [← cancel_epi (π _ _), H2Map, Category.assoc]
+lemma H2π_comp_map :
+    H2π A ≫ map f φ 2 = mapTwoCocycles f φ ≫ H2π B := by
+  simp [H2π, Iso.inv_comp_eq, ← cocyclesMap_comp_isoTwoCocycles_hom_assoc]
+
+@[deprecated (since := "2025-06-12")]
+alias H2π_comp_H2Map := H2π_comp_map
 
 end H2
 
diff --git a/Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean b/Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean
@@ -99,9 +99,10 @@ variable (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
 
 /-- Noether's generalization of Hilbert's Theorem 90: given a finite extension of fields `L/K`, the
 first group cohomology `H¹(Aut_K(L), Lˣ)` is trivial. -/
-noncomputable instance H1ofAutOnUnitsUnique : Unique (H1 (Rep.ofAlgebraAutOnUnits K L)) where
+noncomputable instance H1ofAutOnUnitsUnique [DecidableEq (L ≃ₐ[K] L)] :
+    Unique (H1 (Rep.ofAlgebraAutOnUnits K L)) where
   default := 0
-  uniq := fun a => Quotient.inductionOn' a fun x => (H1π_eq_zero_iff _).2 <| by
+  uniq := fun a => H1_induction_on a fun x => (H1π_eq_zero_iff _).2 <| by
     refine (oneCoboundariesOfIsMulOneCoboundary ?_).2
     rcases isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units x.1
       (isMulOneCocycle_of_mem_oneCocycles _ x.2) with ⟨β, hβ⟩
diff --git a/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean b/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean
diff --git a/Mathlib/RingTheory/Ideal/Over.lean b/Mathlib/RingTheory/Ideal/Over.lean
diff --git a/Mathlib/Topology/CWComplex/Classical/Basic.lean b/Mathlib/Topology/CWComplex/Classical/Basic.lean
