[#15066] feat: virtual one-field structures

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-09-06
+leanprover/lean4-pr-releases:pr-release-15066-2214407

mathlib4/Mathlib/Algebra/AddConstMap/Basic.lean

@@ -292,8 +292,9 @@ theorem monotone_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G]
 theorem antitone_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G]
     [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H]
     [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :
-    Antitone f ↔ AntitoneOn f (Icc l (l + a)) :=
-  monotone_iff_Icc (H := Hᵒᵈ) ha l
+    Antitone f ↔ AntitoneOn f (Icc l (l + a)) := by
+  unsealing_newtype OrderDual =>
+    exact monotone_iff_Icc (H := Hᵒᵈ) ha l
 
 theorem strictMono_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G]
     [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H]
@@ -304,8 +305,9 @@ theorem strictMono_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid
 theorem strictAnti_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G]
     [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H]
     [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :
-    StrictAnti f ↔ StrictAntiOn f (Icc l (l + a)) :=
-  strictMono_iff_Icc (H := Hᵒᵈ) ha l
+    StrictAnti f ↔ StrictAntiOn f (Icc l (l + a)) := by
+  unsealing_newtype OrderDual =>
+    exact strictMono_iff_Icc (H := Hᵒᵈ) ha l
 
 end AddConstMapClass
 

mathlib4/Mathlib/Algebra/Field/Basic.lean

@@ -297,12 +297,30 @@ end Function.Injective
 
 namespace OrderDual
 
-instance [RatCast K] : RatCast Kᵒᵈ := inferInstanceAs <| RatCast K
-instance [NNRatCast K] : NNRatCast Kᵒᵈ := inferInstanceAs <| NNRatCast K
-instance [DivisionSemiring K] : DivisionSemiring Kᵒᵈ := inferInstanceAs <| DivisionSemiring K
-instance [DivisionRing K] : DivisionRing Kᵒᵈ := inferInstanceAs <| DivisionRing K
-instance [Semifield K] : Semifield Kᵒᵈ := inferInstanceAs <| Semifield K
-instance [Field K] : Field Kᵒᵈ := inferInstanceAs <| Field K
+instance [RatCast K] : RatCast Kᵒᵈ := ⟨fun q ↦ OrderDual.mk q⟩
+instance [NNRatCast K] : NNRatCast Kᵒᵈ := ⟨fun q ↦ OrderDual.mk q⟩
+
+instance [DivisionSemiring K] : DivisionSemiring Kᵒᵈ :=
+  ofDual.injective.divisionSemiring _ rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
+    fun _ ↦ rfl
+
+instance [DivisionRing K] : DivisionRing Kᵒᵈ :=
+  ofDual.injective.divisionRing _ rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)
+    fun _ ↦ rfl
+
+instance [Semifield K] : Semifield Kᵒᵈ :=
+  ofDual.injective.semifield _ rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
+    fun _ ↦ rfl
+
+instance [Field K] : Field Kᵒᵈ :=
+  ofDual.injective.field _ rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)
+    fun _ ↦ rfl
 
 end OrderDual
 

mathlib4/Mathlib/Algebra/Group/Finsupp.lean

@@ -307,8 +307,9 @@ lemma induction_on_max (f : ι →₀ M) (zero : motive 0)
 The lemma `induction_on_min₂` swaps the argument order in the sum. -/
 lemma induction_on_min (f : ι →₀ M) (zero : motive 0)
     (single_add : ∀ a b (f : ι →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 →
-      motive f → motive (single a b + f)) : motive f :=
-  induction_on_max (ι := ιᵒᵈ) f zero single_add
+      motive f → motive (single a b + f)) : motive f := by
+  unsealing_newtype OrderDual =>
+    exact induction_on_max (ι := ιᵒᵈ) f zero single_add
 
 /-- A finitely supported function can be built by adding up `single a b` for increasing `a`.
 
@@ -327,8 +328,9 @@ lemma induction_on_max₂ (f : ι →₀ M) (zero : motive 0)
 The lemma `induction_on_min` swaps the argument order in the sum. -/
 lemma induction_on_min₂ (f : ι →₀ M) (zero : motive 0)
     (add_single : ∀ a b (f : ι →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 →
-      motive f → motive (f + single a b)) : motive f :=
-  induction_on_max₂ (ι := ιᵒᵈ) f zero add_single
+      motive f → motive (f + single a b)) : motive f := by
+  unsealing_newtype OrderDual =>
+    exact induction_on_max₂ (ι := ιᵒᵈ) f zero add_single
 
 end LinearOrder
 

mathlib4/Mathlib/Algebra/Lie/Nilpotent.lean

@@ -181,14 +181,16 @@ theorem antitone_lowerCentralSeries : Antitone <| lowerCentralSeries R L M := by
 
 theorem eventually_iInf_lowerCentralSeries_eq [IsArtinian R M] :
     ∀ᶠ l in Filter.atTop, ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l := by
-  have h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ :=
-    LieSubmodule.wellFoundedLT_of_isArtinian R L M
-  obtain ⟨n, hn : ∀ m, n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m⟩ :=
-    h_wf.monotone_chain_condition ⟨_, antitone_lowerCentralSeries R L M⟩
-  refine Filter.eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩
-  rcases le_or_gt l m with h | h
-  · rw [← hn _ hl, ← hn _ (hl.trans h)]
-  · exact antitone_lowerCentralSeries R L M (le_of_lt h)
+  unsealing_newtype OrderDual =>
+    have h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ :=
+      LieSubmodule.wellFoundedLT_of_isArtinian R L M
+    obtain ⟨n, hn : ∀ m, n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m⟩ :=
+      h_wf.monotone_chain_condition ⟨_, antitone_lowerCentralSeries R L M⟩
+    refine Filter.eventually_atTop.mpr
+      ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩
+    rcases le_or_gt l m with h | h
+    · rw [← hn _ hl, ← hn _ (hl.trans h)]
+    · exact antitone_lowerCentralSeries R L M (le_of_lt h)
 
 theorem trivial_iff_lower_central_eq_bot : IsTrivial L M ↔ lowerCentralSeries R L M 1 = ⊥ := by
   constructor <;> intro h

mathlib4/Mathlib/Algebra/Lie/Submodule.lean

@@ -519,7 +519,8 @@ variable (R L M)
     map_rel_iff' := Iff.rfl }
 
 instance wellFoundedGT_of_noetherian [IsNoetherian R M] : WellFoundedGT (LieSubmodule R L M) :=
-  RelHomClass.isWellFounded (toSubmodule_orderEmbedding R L M).dual.ltEmbedding
+  (wellFoundedLT_dual_iff _).1 <|
+    RelHomClass.isWellFounded (toSubmodule_orderEmbedding R L M).dual.ltEmbedding
 
 instance wellFoundedLT_of_isArtinian [IsArtinian R M] : WellFoundedLT (LieSubmodule R L M) :=
   RelHomClass.isWellFounded (toSubmodule_orderEmbedding R L M).ltEmbedding

mathlib4/Mathlib/Algebra/Module/Submodule/Range.lean

@@ -141,13 +141,14 @@ end
 -/
 @[simps]
 def iterateRange (f : M →ₗ[R] M) : ℕ →o (Submodule R M)ᵒᵈ where
-  toFun n := LinearMap.range (f ^ n)
+  toFun n := OrderDual.toDual (LinearMap.range (f ^ n))
   monotone' := monotone_nat_of_le_succ fun | n, _, ⟨x, rfl⟩ => ⟨f x, rfl⟩
 
-set_option backward.isDefEq.respectTransparency false in
 lemma iterateRange_succ {f : M →ₗ[R] M} {n : ℕ} :
-    iterateRange f (n + 1) = (iterateRange f n).map f := by
-  simp only [iterateRange_coe, range_eq_map, ← map_comp, Module.End.iterate_succ']
+    OrderDual.ofDual (iterateRange f (n + 1)) =
+      (OrderDual.ofDual (iterateRange f n)).map f := by
+  simp only [iterateRange_coe, OrderDual.ofDual_toDual, range_eq_map, ← map_comp,
+    Module.End.iterate_succ']
 
 /-- Restrict the codomain of a linear map `f` to `f.range`.
 

mathlib4/Mathlib/Algebra/Module/Torsion/Basic.lean

@@ -405,7 +405,8 @@ theorem torsionBySet_torsionBySet_eq_top : torsionBySet R (torsionBySet R M s) s
 variable (R M)
 
 theorem torsion_gc :
-    @GaloisConnection (Submodule R M) (Ideal R)ᵒᵈ _ _ annihilator fun I =>
+    @GaloisConnection (Submodule R M) (Ideal R)ᵒᵈ _ _
+      (fun N => OrderDual.toDual (annihilator N)) fun I =>
       torsionBySet R M ↑(OrderDual.ofDual I) :=
   fun _ _ =>
   ⟨fun h x hx => (mem_torsionBySet_iff _ _).mpr fun ⟨_, ha⟩ => mem_annihilator.mp (h ha) x hx,

mathlib4/Mathlib/Algebra/MonoidAlgebra/Degree.lean

@@ -71,6 +71,11 @@ section GeneralResultsAssumingSemilatticeSup
 
 variable [SemilatticeSup B] [OrderBot B] [SemilatticeInf T] [OrderTop T]
 
+/-- Transport a finite infimum to the supremum in the order dual. -/
+private lemma toDual_support_inf (s : Finset A) (degt : A → T) :
+    OrderDual.toDual (s.inf degt) = s.sup fun a ↦ OrderDual.toDual (degt a) :=
+  Finset.toDual_inf s degt
+
 section Semiring
 
 variable [Semiring R]
@@ -94,8 +99,9 @@ theorem sup_support_coeff_add_le :
 @[deprecated (since := "2026-06-18")] alias sup_support_add_le := sup_support_coeff_add_le
 
 theorem le_inf_support_coeff_add :
-    f.coeff.support.inf degt ⊓ g.coeff.support.inf degt ≤ (f + g).coeff.support.inf degt :=
-  sup_support_coeff_add_le (fun a : A => OrderDual.toDual (degt a)) f g
+    f.coeff.support.inf degt ⊓ g.coeff.support.inf degt ≤ (f + g).coeff.support.inf degt := by
+  unsealing_newtype OrderDual =>
+    exact sup_support_coeff_add_le (fun a : A => OrderDual.toDual (degt a)) f g
 
 @[deprecated (since := "2026-06-18")] alias le_inf_support_add := le_inf_support_coeff_add
 
@@ -118,8 +124,10 @@ theorem sup_support_coeff_mul_le {degb : A → B} (degbm : ∀ a b, degb (a + b)
 
 theorem le_inf_support_coeff_mul {degt : A → T} (degtm : ∀ a b, degt a + degt b ≤ degt (a + b))
     (f g : R[A]) :
-    f.coeff.support.inf degt + g.coeff.support.inf degt ≤ (f * g).coeff.support.inf degt :=
-  sup_support_coeff_mul_le (B := Tᵒᵈ) degtm f g
+    f.coeff.support.inf degt + g.coeff.support.inf degt ≤ (f * g).coeff.support.inf degt := by
+  have h := sup_support_coeff_mul_le (B := Tᵒᵈ)
+    (degb := fun a ↦ OrderDual.toDual (degt a)) degtm f g
+  simpa only [← toDual_support_inf, ← toDual_add, OrderDual.toDual_le_toDual] using h
 
 @[deprecated (since := "2026-06-18")] alias le_inf_support_mul := le_inf_support_coeff_mul
 
@@ -145,12 +153,13 @@ theorem sup_support_list_prod_le (degb0 : degb 0 ≤ 0)
 theorem le_inf_support_list_prod (degt0 : 0 ≤ degt 0)
     (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (l : List R[A]) :
     (l.map fun f : R[A] => f.coeff.support.inf degt).sum ≤ l.prod.coeff.support.inf degt := by
-  refine OrderDual.ofDual_le_ofDual.mpr ?_
-  refine sup_support_list_prod_le ?_ ?_ l
-  · refine (OrderDual.ofDual_le_ofDual.mp ?_)
-    exact degt0
-  · refine (fun a b => OrderDual.ofDual_le_ofDual.mp ?_)
-    exact degtm a b
+  unsealing_newtype OrderDual =>
+    refine OrderDual.ofDual_le_ofDual.mpr ?_
+    refine sup_support_list_prod_le ?_ ?_ l
+    · refine (OrderDual.ofDual_le_ofDual.mp ?_)
+      exact degt0
+    · refine (fun a b => OrderDual.ofDual_le_ofDual.mp ?_)
+      exact degtm a b
 
 theorem sup_support_pow_le (degb0 : degb 0 ≤ 0) (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b)
     (n : ℕ) (f : R[A]) : (f ^ n).coeff.support.sup degb ≤ n • f.coeff.support.sup degb := by
@@ -160,10 +169,12 @@ theorem sup_support_pow_le (degb0 : degb 0 ≤ 0) (degbm : ∀ a b, degb (a + b)
 
 theorem le_inf_support_pow (degt0 : 0 ≤ degt 0) (degtm : ∀ a b, degt a + degt b ≤ degt (a + b))
     (n : ℕ) (f : R[A]) : n • f.coeff.support.inf degt ≤ (f ^ n).coeff.support.inf degt := by
-  refine OrderDual.ofDual_le_ofDual.mpr <| sup_support_pow_le (OrderDual.ofDual_le_ofDual.mp ?_)
-      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) n f
-  · exact degt0
-  · exact degtm _ _
+  unsealing_newtype OrderDual =>
+    refine OrderDual.ofDual_le_ofDual.mpr <|
+      sup_support_pow_le (B := Tᵒᵈ) (degb := degt) (OrderDual.ofDual_le_ofDual.mp ?_)
+        (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) n f
+    · exact degt0
+    · exact degtm _ _
 
 end AddMonoids
 
@@ -188,11 +199,12 @@ alias sup_support_multiset_prod_le := sup_support_coeff_multisetProd_le
 theorem le_inf_support_coeff_multisetProd (degt0 : 0 ≤ degt 0)
     (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (m : Multiset R[A]) :
     (m.map fun f : R[A] => f.coeff.support.inf degt).sum ≤ m.prod.coeff.support.inf degt := by
-  refine OrderDual.ofDual_le_ofDual.mpr <|
-    sup_support_coeff_multisetProd_le (OrderDual.ofDual_le_ofDual.mp ?_)
-      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) m
-  · exact degt0
-  · exact degtm _ _
+  unsealing_newtype OrderDual =>
+    refine OrderDual.ofDual_le_ofDual.mpr <|
+      sup_support_coeff_multisetProd_le (B := Tᵒᵈ) (degb := degt) (OrderDual.ofDual_le_ofDual.mp ?_)
+        (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) m
+    · exact degt0
+    · exact degtm _ _
 
 @[deprecated (since := "2026-06-18")]
 alias le_inf_support_multiset_prod := le_inf_support_coeff_multisetProd

mathlib4/Mathlib/Algebra/Order/Archimedean/Class.lean

@@ -595,12 +595,13 @@ def subsemigroup (s : UpperSet (MulArchimedeanClass M)) : Subsemigroup M where
 
 @[to_additive]
 theorem subsemigroup_strictAnti : StrictAnti (subsemigroup (M := M)) := by
-  intro s t hst
-  rw [← SetLike.coe_ssubset_coe]
-  refine Set.ssubset_iff_subset_ne.mpr ⟨fun _ h ↦ hst.le h, ?_⟩
-  contrapose! hst with heq
-  apply le_of_eq
-  simpa [MulArchimedeanClass.mk_surjective, MulArchimedeanClass.subsemigroup] using heq
+  unsealing_newtype OrderDual =>
+    intro s t hst
+    rw [← SetLike.coe_ssubset_coe]
+    refine Set.ssubset_iff_subset_ne.mpr ⟨fun _ h ↦ hst.le h, ?_⟩
+    contrapose! hst with heq
+    apply le_of_eq
+    simpa [MulArchimedeanClass.mk_surjective, MulArchimedeanClass.subsemigroup] using heq
 
 /-- Make `MulArchimedeanClass.subsemigroup` a subgroup by assigning
 s = ⊤ with a junk value ⊥. -/

mathlib4/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

@@ -179,8 +179,9 @@ alias prod_le_prod_of_subset_of_one_le' := prod_le_prod_of_subset_of_one_le
 
 @[to_additive]
 lemma prod_le_prod_of_subset_of_le_one [MulLeftMono N] (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → f i ≤ 1) :
-    ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i :=
-  prod_le_prod_of_subset_of_one_le (N := Nᵒᵈ) h hf
+    ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i := by
+  unsealing_newtype OrderDual =>
+    exact prod_le_prod_of_subset_of_one_le (N := Nᵒᵈ) h hf
 
 @[deprecated (since := "2026-09-01")]
 alias prod_le_prod_of_subset_of_le_one' := prod_le_prod_of_subset_of_le_one
@@ -249,16 +250,18 @@ lemma one_lt_prod_iff_of_one_le {ι : Type u_1} {N : Type u_5} [CommMonoid N] [P
 @[to_additive]
 theorem prod_eq_one_iff_of_le_one {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
     {f : ι → N} {s : Finset ι} [MulLeftMono N] :
-    (∀ i ∈ s, f i ≤ 1) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) :=
-  prod_eq_one_iff_of_one_le (N := Nᵒᵈ)
+    (∀ i ∈ s, f i ≤ 1) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) := by
+  unsealing_newtype OrderDual =>
+    exact prod_eq_one_iff_of_one_le (N := Nᵒᵈ)
 
 @[deprecated (since := "2026-09-01")] alias prod_eq_one_iff_of_le_one' := prod_eq_one_iff_of_le_one
 
 @[to_additive]
 lemma prod_lt_one_iff_of_le_one {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
     {f : ι → N} {s : Finset ι} [MulLeftMono N] (hf : ∀ x ∈ s, f x ≤ 1) :
-    ∏ x ∈ s, f x < 1 ↔ ∃ x ∈ s, f x < 1 :=
-  one_lt_prod_iff_of_one_le (N := Nᵒᵈ) hf
+    ∏ x ∈ s, f x < 1 ↔ ∃ x ∈ s, f x < 1 := by
+  unsealing_newtype OrderDual =>
+    exact one_lt_prod_iff_of_one_le (N := Nᵒᵈ) hf
 
 @[to_additive]
 theorem single_le_prod [MulLeftMono N] (hf : ∀ i ∈ s, 1 ≤ f i) {a} (h : a ∈ s) :
@@ -289,7 +292,9 @@ theorem prod_le_pow_card [MulLeftMono N] (s : Finset ι) (f : ι → N) (n : N)
 
 @[to_additive card_nsmul_le_sum]
 theorem pow_card_le_prod [MulLeftMono N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, n ≤ f x) :
-    n ^ #s ≤ s.prod f := Finset.prod_le_pow_card (N := Nᵒᵈ) _ _ _ h
+    n ^ #s ≤ s.prod f := by
+  unsealing_newtype OrderDual =>
+    exact Finset.prod_le_pow_card (N := Nᵒᵈ) _ _ _ h
 
 theorem card_biUnion_le_card_mul [DecidableEq β] (s : Finset ι) (f : ι → Finset β) (n : ℕ)
     (h : ∀ a ∈ s, #(f a) ≤ n) : #(s.biUnion f) ≤ #s * n :=
@@ -314,8 +319,9 @@ alias prod_fiberwise_le_prod_of_one_le_prod_fiber' := prod_fiberwise_le_prod_of_
 @[to_additive]
 theorem prod_le_prod_fiberwise_of_prod_fiber_le_one [MulLeftMono N] {t : Finset ι'} {g : ι → ι'}
     {f : ι → N} (h : ∀ y ∉ t, ∏ x ∈ s with g x = y, f x ≤ 1) :
-    ∏ x ∈ s, f x ≤ ∏ y ∈ t, ∏ x ∈ s with g x = y, f x :=
-  prod_fiberwise_le_prod_of_one_le_prod_fiber (N := Nᵒᵈ) h
+    ∏ x ∈ s, f x ≤ ∏ y ∈ t, ∏ x ∈ s with g x = y, f x := by
+  unsealing_newtype OrderDual =>
+    exact prod_fiberwise_le_prod_of_one_le_prod_fiber (N := Nᵒᵈ) h
 
 @[deprecated (since := "2026-09-01")]
 alias prod_le_prod_fiberwise_of_prod_fiber_le_one' := prod_le_prod_fiberwise_of_prod_fiber_le_one
@@ -344,8 +350,9 @@ theorem apply_prod_le_sum_apply (h_one : g 1 ≤ 0) (h_mul : ∀ (a b : α), g (
   rw [Multiset.map_map, Function.comp_def, Finset.sum_map_val]
 
 theorem sum_apply_le_apply_prod (h_one : 0 ≤ g 1) (h_mul : ∀ (a b : α), g a + g b ≤ g (a * b)) :
-    ∑ x ∈ s, g (f x) ≤ g (∏ x ∈ s, f x) :=
-  s.apply_prod_le_sum_apply (β := βᵒᵈ) g h_one h_mul
+    ∑ x ∈ s, g (f x) ≤ g (∏ x ∈ s, f x) := by
+  unsealing_newtype OrderDual =>
+    exact s.apply_prod_le_sum_apply (β := βᵒᵈ) g h_one h_mul
 
 end ProdSum
 
@@ -684,8 +691,9 @@ theorem exists_one_lt_of_prod_one_of_exists_ne_one [MulLeftMono M] (f : ι → M
 
 @[to_additive exists_neg_of_sum_zero_of_exists_nonzero]
 theorem exists_lt_one_of_prod_one_of_exists_ne_one [MulLeftMono M] (f : ι → M)
-    (h₁ : ∏ i ∈ s, f i = 1) (h₂ : ∃ i ∈ s, f i ≠ 1) : ∃ i ∈ s, f i < 1 :=
-  exists_one_lt_of_prod_one_of_exists_ne_one (M := Mᵒᵈ) f h₁ h₂
+    (h₁ : ∏ i ∈ s, f i = 1) (h₂ : ∃ i ∈ s, f i ≠ 1) : ∃ i ∈ s, f i < 1 := by
+  unsealing_newtype OrderDual =>
+    exact exists_one_lt_of_prod_one_of_exists_ne_one (M := Mᵒᵈ) f h₁ h₂
 
 variable [IsOrderedCancelMonoid M]
 

mathlib4/Mathlib/Algebra/Order/BigOperators/Group/List.lean

@@ -110,8 +110,9 @@ alias prod_le_pow_card := prod_le_pow_length
 @[to_additive length_nsmul_le_sum]
 lemma pow_length_le_prod [Preorder M] [MulRightMono M]
     [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, n ≤ x) :
-    n ^ l.length ≤ l.prod :=
-  @prod_le_pow_length Mᵒᵈ _ _ _ _ l n h
+    n ^ l.length ≤ l.prod := by
+  unsealing_newtype OrderDual =>
+    exact @prod_le_pow_length Mᵒᵈ _ _ _ _ l n h
 
 @[to_additive (attr := deprecated (since := "2026-08-26")) card_nsmul_le_sum]
 alias pow_card_le_prod := pow_length_le_prod
@@ -288,8 +289,9 @@ theorem apply_prod_le_sum_map (h_one : f 1 ≤ 0) (h_mul : ∀ (a b : α), f (a
   | cons hd tl IH => grw [prod_cons, h_mul, IH]; simp
 
 theorem sum_map_le_apply_prod (h_one : 0 ≤ f 1) (h_mul : ∀ (a b : α), f a + f b ≤ f (a * b)) :
-    (l.map f).sum ≤ f l.prod :=
-  apply_prod_le_sum_map (β := βᵒᵈ) l f h_one h_mul
+    (l.map f).sum ≤ f l.prod := by
+  unsealing_newtype OrderDual =>
+    exact apply_prod_le_sum_map (β := βᵒᵈ) l f h_one h_mul
 
 end ProdSum
 

mathlib4/Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

@@ -70,8 +70,9 @@ lemma prod_map_le_prod [MulLeftMono α] (f : α → α) (h : ∀ x, x ∈ s →
 
 @[to_additive]
 lemma prod_le_prod_map [MulLeftMono α] (f : α → α) (h : ∀ x, x ∈ s → x ≤ f x) :
-    s.prod ≤ (s.map f).prod :=
-  prod_map_le_prod (α := αᵒᵈ) f h
+    s.prod ≤ (s.map f).prod := by
+  unsealing_newtype OrderDual =>
+    exact prod_map_le_prod (α := αᵒᵈ) f h
 
 @[to_additive card_nsmul_le_sum]
 lemma pow_card_le_prod [MulLeftMono α] (h : ∀ x ∈ s, a ≤ x) : a ^ card s ≤ s.prod := by
@@ -187,8 +188,9 @@ lemma apply_prod_le_sum_map (h_one : f 1 ≤ 0) (h_mul : ∀ (a b : α), f (a *
   | h l => simp [l.apply_prod_le_sum_map _ h_one h_mul]
 
 lemma sum_map_le_apply_prod (h_one : 0 ≤ f 1) (h_mul : ∀ (a b : α), f a + f b ≤ f (a * b)) :
-    (m.map f).sum ≤ f m.prod :=
-  m.apply_prod_le_sum_map (β := βᵒᵈ) f h_one h_mul
+    (m.map f).sum ≤ f m.prod := by
+  unsealing_newtype OrderDual =>
+    exact m.apply_prod_le_sum_map (β := βᵒᵈ) f h_one h_mul
 
 end ProdSum