diff --git a/Mathlib.lean b/Mathlib.lean index 638124f2103..624f35d65fc 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1101,6 +1101,7 @@ public import Mathlib.Algebra.Order.Ring.InjSurj public import Mathlib.Algebra.Order.Ring.Int public import Mathlib.Algebra.Order.Ring.Interval public import Mathlib.Algebra.Order.Ring.IsNonarchimedean +public import Mathlib.Algebra.Order.Ring.NNRat public import Mathlib.Algebra.Order.Ring.Nat public import Mathlib.Algebra.Order.Ring.Opposite public import Mathlib.Algebra.Order.Ring.Ordering.Basic @@ -7321,7 +7322,6 @@ public import Mathlib.Tactic.DeriveCountable public import Mathlib.Tactic.DeriveEncodable public import Mathlib.Tactic.DeriveFintype public import Mathlib.Tactic.DeriveTraversable -public import Mathlib.Tactic.Determinant.Bird public import Mathlib.Tactic.Determinant.Bird.Cert public import Mathlib.Tactic.Determinant.Bird.Meta public import Mathlib.Tactic.DuplicateDecls @@ -7446,6 +7446,7 @@ public import Mathlib.Tactic.MoveAdd public import Mathlib.Tactic.NoncommRing public import Mathlib.Tactic.Nontriviality public import Mathlib.Tactic.Nontriviality.Core +public import Mathlib.Tactic.NormDet public import Mathlib.Tactic.NormNum public import Mathlib.Tactic.NormNum.Abs public import Mathlib.Tactic.NormNum.Basic diff --git a/Mathlib/Algebra/Central/End.lean b/Mathlib/Algebra/Central/End.lean index d7317e1f219..3deeaa99142 100644 --- a/Mathlib/Algebra/Central/End.lean +++ b/Mathlib/Algebra/Central/End.lean @@ -60,7 +60,7 @@ public theorem LinearEquiv.conjAlgEquiv_ext_iff' {S M₂ : Type*} [CommRing S] [ (f g : M ≃ₗ[R] M₂) : f.conjAlgEquiv S = g.conjAlgEquiv S ↔ ∃ α : Sˣ, f = α • g := by refine ⟨fun h ↦ ?_, fun ⟨y, h⟩ ↦ conjAlgEquiv_ext_iff.mpr ⟨(y : S), congr($h)⟩⟩ by_cases! Subsingleton M - · exact ⟨1, by ext; simp [Subsingleton.eq_zero]⟩ + · exact ⟨1, by ext; simp [Subsingleton.eq_zero (α := M)]⟩ obtain ⟨α, hα⟩ := conjAlgEquiv_ext_iff.mp h obtain ⟨β, hβ⟩ := conjAlgEquiv_ext_iff.mp h.symm obtain ⟨x, hx⟩ := exists_ne (0 : M) diff --git a/Mathlib/Algebra/FreeMonoid/Basic.lean b/Mathlib/Algebra/FreeMonoid/Basic.lean index bc1c911462c..b5e85acc3ed 100644 --- a/Mathlib/Algebra/FreeMonoid/Basic.lean +++ b/Mathlib/Algebra/FreeMonoid/Basic.lean @@ -236,16 +236,18 @@ end Mem /-- Recursor for `FreeAddMonoid` using `0` and `FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`. -/] -- Porting note: change from `List.recOn` to `List.rec` since only the latter is computable -def recOn {C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1) - (ih : ∀ x xs, C xs → C (of x * xs)) : C xs := List.rec h0 ih xs +def recOn {motive : FreeMonoid α → Sort*} (xs : FreeMonoid α) (one : motive 1) + (of_mul : ∀ x xs, motive xs → motive (of x * xs)) : motive xs := List.rec one of_mul xs @[to_additive (attr := simp)] -theorem recOn_one {C : FreeMonoid α → Sort*} (h0 : C 1) (ih : ∀ x xs, C xs → C (of x * xs)) : - @recOn α C 1 h0 ih = h0 := rfl +theorem recOn_one {motive : FreeMonoid α → Sort*} (one : motive 1) + (of_mul : ∀ x xs, motive xs → motive (of x * xs)) : + @recOn α motive 1 one of_mul = one := rfl @[to_additive (attr := simp)] -theorem recOn_of_mul {C : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (h0 : C 1) - (ih : ∀ x xs, C xs → C (of x * xs)) : @recOn α C (of x * xs) h0 ih = ih x xs (recOn xs h0 ih) := +theorem recOn_of_mul {motive : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (one : motive 1) + (of_mul : ∀ x xs, motive xs → motive (of x * xs)) : + @recOn α motive (of x * xs) one of_mul = of_mul x xs (recOn xs one of_mul) := rfl /-! ### Induction -/ @@ -255,18 +257,19 @@ section induction_principles /-- An induction principle on free monoids, with cases for `1`, `FreeMonoid.of` and `*`. -/ @[to_additive (attr := elab_as_elim, induction_eliminator) /-- An induction principle on free monoids, with cases for `0`, `FreeAddMonoid.of` and `+`. -/] -protected theorem inductionOn {C : FreeMonoid α → Prop} (z : FreeMonoid α) (one : C 1) - (of : ∀ (x : α), C (FreeMonoid.of x)) (mul : ∀ (x y : FreeMonoid α), C x → C y → C (x * y)) : - C z := - List.rec one (fun _ _ ih => mul [_] _ (of _) ih) z +protected theorem inductionOn {motive : FreeMonoid α → Prop} (z : FreeMonoid α) (one : motive 1) + (of : ∀ (x : α), motive (FreeMonoid.of x)) + (mul : ∀ (x y : FreeMonoid α), motive x → motive y → motive (x * y)) : + motive z := + recOn z one fun x xs ih => mul (.of x) xs (of x) ih /-- An induction principle for free monoids which mirrors induction on lists, with cases analogous to the empty list and cons -/ @[to_additive (attr := elab_as_elim) /-- An induction principle for free monoids which mirrors induction on lists, with cases analogous to the empty list and cons -/] -protected theorem inductionOn' {p : FreeMonoid α → Prop} (a : FreeMonoid α) - (one : p (1 : FreeMonoid α)) (mul_of : ∀ b a, p a → p (of b * a)) : p a := - List.rec one (fun _ _ tail_ih => mul_of _ _ tail_ih) a +protected theorem inductionOn' {motive : FreeMonoid α → Prop} (a : FreeMonoid α) + (one : motive (1 : FreeMonoid α)) (of_mul : ∀ b a, motive a → motive (of b * a)) : motive a := + recOn a one of_mul end induction_principles @@ -275,16 +278,18 @@ end induction_principles @[to_additive (attr := elab_as_elim, cases_eliminator) /-- A version of `List.casesOn` for `FreeAddMonoid` using `0` and `FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`. -/] -def casesOn {C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1) - (ih : ∀ x xs, C (of x * xs)) : C xs := List.casesOn xs h0 ih +def casesOn {motive : FreeMonoid α → Sort*} (xs : FreeMonoid α) (one : motive 1) + (of_mul : ∀ x xs, motive (of x * xs)) : motive xs := List.casesOn xs one of_mul @[to_additive (attr := simp)] -theorem casesOn_one {C : FreeMonoid α → Sort*} (h0 : C 1) (ih : ∀ x xs, C (of x * xs)) : - @casesOn α C 1 h0 ih = h0 := rfl +theorem casesOn_one {motive : FreeMonoid α → Sort*} (one : motive 1) + (of_mul : ∀ x xs, motive (of x * xs)) : + @casesOn α motive 1 one of_mul = one := rfl @[to_additive (attr := simp)] -theorem casesOn_of_mul {C : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (h0 : C 1) - (ih : ∀ x xs, C (of x * xs)) : @casesOn α C (of x * xs) h0 ih = ih x xs := rfl +theorem casesOn_of_mul {motive : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (one : motive 1) + (of_mul : ∀ x xs, motive (of x * xs)) : + @casesOn α motive (of x * xs) one of_mul = of_mul x xs := rfl @[to_additive (attr := ext)] theorem hom_eq ⦃f g : FreeMonoid α →* M⦄ (h : ∀ x, f (of x) = g (of x)) : f = g := @@ -431,7 +436,7 @@ theorem map_surjective {f : α → β} : Function.Surjective (map f) ↔ Functio | one => have H := congr_arg length hb simp only [length_one, length_of, Nat.zero_ne_one, map_one] at H - | mul_of head _ _ => + | of_mul head _ _ => simp only [map_mul, map_of] at hb use head have H := congr_arg length hb @@ -441,7 +446,7 @@ theorem map_surjective {f : α → β} : Function.Surjective (map f) ↔ Functio intro fs d induction d using FreeMonoid.inductionOn' with | one => use 1; rfl - | mul_of head tail ih => + | of_mul head tail ih => specialize fs head rcases fs with ⟨a, rfl⟩ rcases ih with ⟨b, rfl⟩ diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index d948baeee2b..3111721ff63 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -1068,9 +1068,13 @@ variable [DivInvMonoid G] ZPow.zpow n x = x ^ n := rfl -@[to_additive (attr := simp) zero_zsmul] theorem zpow_zero (a : G) : a ^ (0 : ℤ) = 1 := +@[to_additive zero_zsmul] theorem zpow_zero (a : G) : a ^ (0 : ℤ) = 1 := DivInvMonoid.zpow_zero' a +-- `zpow_zero` is provable by `simp` (via `zpow_ofNat`), so the `simpNF` linter rejects tagging it. +-- We still want the additive `zero_zsmul` to be `simp`, so we tag that one manually. +attribute [simp] zero_zsmul + @[to_additive (attr := simp, norm_cast) natCast_zsmul] theorem zpow_natCast (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n | 0 => (zpow_zero _).trans (pow_zero _).symm @@ -1080,7 +1084,9 @@ theorem zpow_natCast (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n _ = a ^ (n + 1) := (pow_succ _ _).symm -@[to_additive ofNat_zsmul] +-- TODO: consider also making `ofNat_zsmul` a `simp` lemma; it is currently not, because it breaks +-- `simp`-normal forms involving `(2 : ℤ) • ·` used in the theory of oriented angles. +@[to_additive ofNat_zsmul, simp] lemma zpow_ofNat (a : G) (n : ℕ) : a ^ (ofNat(n) : ℤ) = a ^ OfNat.ofNat n := zpow_natCast .. @@ -1117,9 +1123,13 @@ theorem mul_div_assoc (a b c : G) : a * b / c = a * (b / c) := by theorem one_div (a : G) : 1 / a = a⁻¹ := (inv_eq_one_div a).symm -@[to_additive (attr := simp) one_zsmul] +@[to_additive one_zsmul] lemma zpow_one (a : G) : a ^ (1 : ℤ) = a := by rw [zpow_ofNat, pow_one] +-- `zpow_one` is provable by `simp` (via `zpow_ofNat`), so the `simpNF` linter rejects tagging it. +-- We still want the additive `one_zsmul` to be `simp`, so we tag that one manually. +attribute [simp] one_zsmul + @[to_additive two_zsmul] lemma zpow_two (a : G) : a ^ (2 : ℤ) = a * a := by rw [zpow_ofNat, pow_two] @[to_additive neg_one_zsmul] diff --git a/Mathlib/Algebra/Group/End.lean b/Mathlib/Algebra/Group/End.lean index d097f727d00..f2ad7a65fba 100644 --- a/Mathlib/Algebra/Group/End.lean +++ b/Mathlib/Algebra/Group/End.lean @@ -11,7 +11,6 @@ public import Mathlib.Algebra.Group.Prod public import Mathlib.Algebra.Group.Units.Equiv public import Mathlib.Data.Set.Basic public import Mathlib.Tactic.Common - public import Mathlib.Tactic.Attr.Register /-! diff --git a/Mathlib/Algebra/Group/Submonoid/Membership.lean b/Mathlib/Algebra/Group/Submonoid/Membership.lean index e9e109c8842..01e73b2c7a7 100644 --- a/Mathlib/Algebra/Group/Submonoid/Membership.lean +++ b/Mathlib/Algebra/Group/Submonoid/Membership.lean @@ -277,7 +277,7 @@ theorem closure_induction_left obtain ⟨l, rfl⟩ := h induction l using FreeMonoid.inductionOn' with | one => exact one - | mul_of x y ih => + | of_mul x y ih => simp only [map_mul, FreeMonoid.lift_eval_of] refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_) simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply] diff --git a/Mathlib/Algebra/Homology/EulerCharacteristic.lean b/Mathlib/Algebra/Homology/EulerCharacteristic.lean index 9c2852324d0..ec0524f0388 100644 --- a/Mathlib/Algebra/Homology/EulerCharacteristic.lean +++ b/Mathlib/Algebra/Homology/EulerCharacteristic.lean @@ -103,7 +103,9 @@ variable (c : ComplexShape ι) [c.EulerCharSigns] /-- The support of a graded object with respect to finite rank: the set of indices where the rank is nonzero. -/ -def finrankSupport (X : CategoryTheory.GradedObject ι (ModuleCat R)) : Set ι := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def finrankSupport (X : CategoryTheory.GradedObject ι (ModuleCat R)) : Set ι := Function.support (fun i => Module.finrank R (X i)) /-- The finite rank support is contained in a set if and only if diff --git a/Mathlib/Algebra/Lie/Semisimple/Basic.lean b/Mathlib/Algebra/Lie/Semisimple/Basic.lean index 8775195af32..a4cb98dc4eb 100644 --- a/Mathlib/Algebra/Lie/Semisimple/Basic.lean +++ b/Mathlib/Algebra/Lie/Semisimple/Basic.lean @@ -277,11 +277,11 @@ lemma booleanGenerators : BooleanGenerators {I : LieIdeal R L | IsAtom I} where finitelyAtomistic _ _ hs _ hIs := finitelyAtomistic _ hs _ hIs instance (priority := 100) instDistribLattice : DistribLattice (LieIdeal R L) := - (booleanGenerators R L).distribLattice_of_sSup_eq_top sSup_atoms_eq_top + (booleanGenerators R L).distribLatticeOfSSupEqTop sSup_atoms_eq_top noncomputable instance (priority := 100) instBooleanAlgebra : BooleanAlgebra (LieIdeal R L) := - (booleanGenerators R L).booleanAlgebra_of_sSup_eq_top sSup_atoms_eq_top + (booleanGenerators R L).booleanAlgebraOfSSupEqTop sSup_atoms_eq_top /-- A semisimple Lie algebra has trivial radical. -/ instance (priority := 100) instHasTrivialRadical : HasTrivialRadical R L := by diff --git a/Mathlib/Algebra/Module/Torsion/Basic.lean b/Mathlib/Algebra/Module/Torsion/Basic.lean index b270a3c789e..9d69c7470c6 100644 --- a/Mathlib/Algebra/Module/Torsion/Basic.lean +++ b/Mathlib/Algebra/Module/Torsion/Basic.lean @@ -938,10 +938,8 @@ theorem torsionBy_eq_span_singleton {R : Type w} [CommRing R] (a b : R) (ha : a end Ideal.Quotient -namespace AddMonoid - -theorem isTorsion_iff_isTorsion_nat [AddCommMonoid M] : - AddMonoid.IsTorsion M ↔ Module.IsTorsion ℕ M := by +theorem isAddTorsion_iff_isTorsion_nat [AddCommMonoid M] : + IsAddTorsion M ↔ Module.IsTorsion ℕ M := by refine ⟨fun h x => ?_, fun h x => ?_⟩ · obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero exact ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt h0⟩, hn⟩ @@ -949,8 +947,11 @@ theorem isTorsion_iff_isTorsion_nat [AddCommMonoid M] : obtain ⟨n, hn⟩ := @h x exact ⟨n, Nat.pos_of_ne_zero (nonZeroDivisors.coe_ne_zero _), hn⟩ -theorem isTorsion_iff_isTorsion_int [AddCommGroup M] : - AddMonoid.IsTorsion M ↔ Module.IsTorsion ℤ M := by +@[deprecated (since := "2026-07-01")] alias AddMonoid.isTorsion_iff_isTorsion_nat := + isAddTorsion_iff_isTorsion_nat + +theorem isAddTorsion_iff_isTorsion_int [AddCommGroup M] : + IsAddTorsion M ↔ Module.IsTorsion ℤ M := by refine ⟨fun h x => ?_, fun h x => ?_⟩ · obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero exact @@ -960,7 +961,8 @@ theorem isTorsion_iff_isTorsion_int [AddCommGroup M] : obtain ⟨n, hn⟩ := @h x exact ⟨_, Int.natAbs_pos.2 (nonZeroDivisors.coe_ne_zero n), natAbs_nsmul_eq_zero.2 hn⟩ -end AddMonoid +@[deprecated (since := "2026-07-01")] alias AddMonoid.isTorsion_iff_isTorsion_int := + isAddTorsion_iff_isTorsion_int namespace AddSubgroup diff --git a/Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean b/Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean index df972cdccea..9edb22e301b 100644 --- a/Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean +++ b/Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean @@ -50,7 +50,7 @@ lemma degreeOf_prod_eq {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ (h : ∀ i ∈ s, f i ≠ 0) : degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i) := by rcases subsingleton_or_nontrivial (MvPolynomial σ R) with nontrivial | nontrivial - · simp [Subsingleton.eq_zero] + · simp [Subsingleton.eq_zero (α := MvPolynomial σ R)] · classical induction s using Finset.induction_on with | empty => simp diff --git a/Mathlib/Algebra/Notation/Indicator.lean b/Mathlib/Algebra/Notation/Indicator.lean index ba717879840..cf61481ca68 100644 --- a/Mathlib/Algebra/Notation/Indicator.lean +++ b/Mathlib/Algebra/Notation/Indicator.lean @@ -228,6 +228,13 @@ lemma comp_mulIndicator_const (c : M) (f : M → N) (hf : f 1 = 1) : (fun x => f (s.mulIndicator (fun _ => c) x)) = s.mulIndicator fun _ => f c := (mulIndicator_comp_of_one hf).symm +/-- Evaluating the indicator of a family of functions at a point commutes with the indicator: +`s.mulIndicator f a b = s.mulIndicator (f · b) a`. -/ +@[to_additive] +lemma mulIndicator_apply_apply (f : α → β → M) (b : β) : + s.mulIndicator f a b = s.mulIndicator (fun i ↦ f i b) a := by + by_cases h : a ∈ s <;> simp [h] + @[to_additive] lemma mulIndicator_preimage (s : Set α) (f : α → M) (B : Set M) : mulIndicator s f ⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B) := diff --git a/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean b/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean index 7caaf3ed13c..04b1a4dacc8 100644 --- a/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean +++ b/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean @@ -185,7 +185,7 @@ omit [Nontrivial R] in /-- An absolute value satisfies `f (n : R) ≤ n` for every `n : ℕ`. -/ lemma apply_nat_le_self [IsOrderedRing S] (n : ℕ) : abv n ≤ n := by cases subsingleton_or_nontrivial R - · simp [Subsingleton.eq_zero (n : R)] + · simp [Subsingleton.eq_zero (α := R)] induction n with | zero => simp | succ n ih => diff --git a/Mathlib/Algebra/Order/Antidiag/Pi.lean b/Mathlib/Algebra/Order/Antidiag/Pi.lean index ce8416da368..10dfd75c03a 100644 --- a/Mathlib/Algebra/Order/Antidiag/Pi.lean +++ b/Mathlib/Algebra/Order/Antidiag/Pi.lean @@ -9,6 +9,7 @@ module public import Mathlib.Algebra.Group.Pointwise.Finset.Scalar public import Mathlib.Data.Fin.Tuple.NatAntidiagonal public import Mathlib.Data.Finset.Sym +public import Mathlib.Algebra.Group.Pi.Lemmas /-! # Antidiagonal of functions as finsets @@ -58,7 +59,6 @@ In this section, we define the antidiagonals in `Fin d → μ` by recursion on ` computationally efficient, although probably not as efficient as `Finset.Nat.antidiagonalTuple`. -/ -set_option backward.isDefEq.respectTransparency.types false in /-- Auxiliary construction for `finAntidiagonal` that bundles a proof of lawfulness (`mem_finAntidiagonal`), as this is needed to invoke `disjiUnion`. Using `Finset.disjiUnion` makes this computationally much more efficient than using `Finset.biUnion`. -/ @@ -73,16 +73,10 @@ def finAntidiagonal.aux (d : ℕ) (n : μ) : {s : Finset (Fin d → μ) // ∀ f { val := (antidiagonal n).disjiUnion (fun ab => (aux d ab.2).1.map { toFun := Fin.cons (ab.1) - inj' := Fin.cons_right_injective _ }) - (fun i _hi j _hj hij => Finset.disjoint_left.2 fun t hti htj => hij <| by - simp_rw [Finset.mem_map, Embedding.coeFn_mk] at hti htj - obtain ⟨ai, hai, hij'⟩ := hti - obtain ⟨aj, haj, rfl⟩ := htj - rw [Fin.cons_inj] at hij' - ext - · exact hij'.1 - · obtain ⟨-, rfl⟩ := hij' - rw [← (aux d i.2).prop ai |>.mp hai, ← (aux d j.2).prop ai |>.mp haj]) + inj' := Fin.cons_right_injective _ }) <| by + intro i _ j _ hij + simp only [Finset.disjoint_left, Finset.mem_map, Embedding.coeFn_mk] + grind [Fin.cons_inj] property := fun f => by simp_rw [mem_disjiUnion, mem_antidiagonal, mem_map, Embedding.coeFn_mk, Prod.exists, (aux d _).prop, Fin.sum_univ_succ] @@ -92,7 +86,6 @@ def finAntidiagonal.aux (d : ℕ) (n : μ) : {s : Finset (Fin d → μ) // ∀ f · intro hf exact ⟨_, _, hf, _, rfl, Fin.cons_self_tail f⟩ } -set_option backward.isDefEq.respectTransparency false in /-- `finAntidiagonal d n` is the type of `d`-tuples with sum `n`. TODO: deduplicate with the less general `Finset.Nat.antidiagonalTuple`. -/ @@ -109,13 +102,13 @@ choosing an identification `s ≃ Fin s.card` and proving that the end result do choice. -/ -set_option backward.isDefEq.respectTransparency false in /-- The finset of functions `ι → μ` with support contained in `s` and sum `n`. -/ def piAntidiag (s : Finset ι) (n : μ) : Finset (ι → μ) := by refine (Fintype.truncEquivFinOfCardEq <| Fintype.card_coe s).lift (fun e ↦ (finAntidiagonal s.card n).map ⟨fun f i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, ?_⟩) fun e₁ e₂ ↦ ?_ - · rintro f g hfg + · rw [Injective] + rintro f g hfg ext i simpa using congr_fun hfg (e.symm i) · ext f @@ -126,7 +119,6 @@ def piAntidiag (s : Finset ι) (n : μ) : Finset (ι → μ) := by variable {s : Finset ι} {n : μ} {f : ι → μ} -set_option backward.isDefEq.respectTransparency false in @[simp] lemma mem_piAntidiag : f ∈ piAntidiag s n ↔ s.sum f = n ∧ ∀ i, f i ≠ 0 → i ∈ s := by rw [piAntidiag] induction Fintype.truncEquivFinOfCardEq (Fintype.card_coe s) using Trunc.ind with | _ e @@ -181,8 +173,7 @@ lemma piAntidiag_cons (hi : i ∉ s) (n : μ) : constructor · rintro ⟨hn, hf⟩ refine ⟨_, _, hn, update f i 0, ⟨sum_update_of_notMem hi _ _, fun j ↦ ?_⟩, by aesop⟩ - have := fun h₁ h₂ ↦ (hf j h₁).resolve_left h₂ - aesop (add simp [update]) + grind · rintro ⟨a, _, hn, g, ⟨rfl, hg⟩, rfl⟩ have := hg i aesop (add simp [sum_add_distrib]) @@ -206,16 +197,14 @@ end CanonicallyOrderedAddCommMonoid section Nat variable [DecidableEq ι] -/-- Local notation for the pointwise operation `n • s := {n • a | a ∈ s}` to avoid conflict with the -pointwise operation `n • s := s + ... + s` (`n` times). -/ -local infixr:73 " •ℕ " => @SMul.smul _ _ Finset.smulFinset +open Pointwise lemma piAntidiag_univ_fin_eq_antidiagonalTuple (n k : ℕ) : piAntidiag univ n = Nat.antidiagonalTuple k n := by ext; simp [Nat.mem_antidiagonalTuple] lemma nsmul_piAntidiag [DecidableEq (ι → ℕ)] (s : Finset ι) (m : ℕ) {n : ℕ} (hn : n ≠ 0) : - n •ℕ piAntidiag s m = {f ∈ piAntidiag s (n * m) | ∀ i ∈ s, n ∣ f i} := by + n • piAntidiag s m = {f ∈ piAntidiag s (n * m) | ∀ i ∈ s, n ∣ f i} := by ext f refine mem_smul_finset.trans ?_ simp only [mem_filter, mem_piAntidiag, and_assoc] @@ -233,18 +222,16 @@ lemma nsmul_piAntidiag [DecidableEq (ι → ℕ)] (s : Finset ι) (m : ℕ) {n : grind lemma map_nsmul_piAntidiag (s : Finset ι) (m : ℕ) {n : ℕ} (hn : n ≠ 0) : - (piAntidiag s m).map - ⟨(n • ·), fun _ _ h ↦ funext fun i ↦ mul_right_injective₀ hn (congr_fun h i)⟩ = + (piAntidiag s m).map ⟨(n • ·), nsmul_right_injective hn⟩ = {f ∈ piAntidiag s (n * m) | ∀ i ∈ s, n ∣ f i} := by classical rw [map_eq_image]; exact nsmul_piAntidiag _ _ hn lemma nsmul_piAntidiag_univ [Fintype ι] (m : ℕ) {n : ℕ} (hn : n ≠ 0) : - n •ℕ (piAntidiag univ m) = {f ∈ piAntidiag (univ : Finset ι) (n * m) | ∀ i, n ∣ f i} := by + n • piAntidiag univ m = {f ∈ piAntidiag (univ : Finset ι) (n * m) | ∀ i, n ∣ f i} := by simpa using nsmul_piAntidiag (univ : Finset ι) m hn lemma map_nsmul_piAntidiag_univ [Fintype ι] (m : ℕ) {n : ℕ} (hn : n ≠ 0) : - (piAntidiag (univ : Finset ι) m).map - ⟨(n • ·), fun _ _ h ↦ funext fun i ↦ mul_right_injective₀ hn (congr_fun h i)⟩ = + (piAntidiag (univ : Finset ι) m).map ⟨(n • ·), nsmul_right_injective hn⟩ = {f ∈ piAntidiag (univ : Finset ι) (n * m) | ∀ i, n ∣ f i} := by simpa using map_nsmul_piAntidiag (univ : Finset ι) m hn diff --git a/Mathlib/Algebra/Order/Ring/NNRat.lean b/Mathlib/Algebra/Order/Ring/NNRat.lean new file mode 100644 index 00000000000..2216eed6895 --- /dev/null +++ b/Mathlib/Algebra/Order/Ring/NNRat.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2019 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl, Mario Carneiro +-/ +module + +public import Mathlib.Algebra.Order.Ring.Rat +public import Mathlib.Algebra.Order.Nonneg.Ring +public import Mathlib.Data.NNRat.Defs + +/-! +# The nonnegative rational numbers form a linear ordered commutative semiring + +This file proves that the linear order on `ℚ≥0` makes it into an ordered semiring. + +`ℚ≥0` is in fact a linearly ordered semifield. To access this fact, one must also import +`Mathlib/Algebra/Field/Rat.lean`. + +## Tags + +rat, rationals, field, ℚ, numerator, denominator, num, denom, order, ordering +-/ + +assert_not_exists Field Finset + +public section + +namespace NNRat + +instance : IsStrictOrderedRing ℚ≥0 := Nonneg.isStrictOrderedRing + +deriving instance OrderedSub, CanonicallyOrderedAdd for NNRat + +end NNRat diff --git a/Mathlib/Algebra/Order/Ring/Rat.lean b/Mathlib/Algebra/Order/Ring/Rat.lean index c8c8ad5ae0b..58c6fa105e4 100644 --- a/Mathlib/Algebra/Order/Ring/Rat.lean +++ b/Mathlib/Algebra/Order/Ring/Rat.lean @@ -10,13 +10,12 @@ public import Mathlib.Algebra.Order.Ring.Unbundled.Rat public import Mathlib.Algebra.Ring.Rat /-! -# The rational numbers form a linear ordered field +# The rational numbers form a linear ordered commutative ring -This file constructs the order on `ℚ` and proves that `ℚ` is a discrete, linearly ordered -commutative ring. +This file proves that the linear order on `ℚ` makes it into an ordered ring. -`ℚ` is in fact a linearly ordered field, but this fact is located in `Data.Rat.Field` instead of -here because we need the order on `ℚ` to define `ℚ≥0`, which we itself need to define `Field`. +`ℚ` is in fact a linearly ordered field. To access this fact, one must also import +`Mathlib/Algebra/Field/Rat.lean`. ## Tags diff --git a/Mathlib/Algebra/Ring/BooleanRing.lean b/Mathlib/Algebra/Ring/BooleanRing.lean index 9f3f9f7c541..b4089404607 100644 --- a/Mathlib/Algebra/Ring/BooleanRing.lean +++ b/Mathlib/Algebra/Ring/BooleanRing.lean @@ -205,7 +205,6 @@ theorem le_sup_inf (a b c : α) : (a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = dsimp only [(· ⊔ ·), (· ⊓ ·)] rw [le_sup_inf_aux, add_self, mul_self, zero_add] -set_option linter.flexible false in -- TODO: fix non-terminal simp /-- The Boolean algebra structure on a Boolean ring. The data is defined so that: @@ -233,8 +232,7 @@ def toBooleanAlgebra : BooleanAlgebra α := change 1 + (a + (1 + a) + a * (1 + a)) + 1 * (a + (1 + a) + a * (1 + a)) = a + (1 + a) + a * (1 + a) - simp [mul_add, mul_self, add_self] - rw [← add_assoc, add_self] } + simp [mul_add, mul_self, add_self, ← add_assoc 1 a] } scoped[BooleanAlgebraOfBooleanRing] attribute [instance 100] BooleanRing.toBooleanAlgebra diff --git a/Mathlib/Algebra/Ring/Divisibility/Basic.lean b/Mathlib/Algebra/Ring/Divisibility/Basic.lean index 05bb2b130d1..0d86efaaf2e 100644 --- a/Mathlib/Algebra/Ring/Divisibility/Basic.lean +++ b/Mathlib/Algebra/Ring/Divisibility/Basic.lean @@ -39,10 +39,9 @@ theorem MulEquiv.decompositionMonoid (f : F) [DecompositionMonoid β] : Decompos primal a b c h := by rw [← map_dvd_iff f, map_mul] at h obtain ⟨a₁, a₂, h⟩ := DecompositionMonoid.primal _ h - refine ⟨symm f a₁, symm f a₂, ?_⟩ - simp_rw [← map_dvd_iff f, ← map_mul, eq_symm_apply] - iterate 2 erw [(f : α ≃* β).apply_symm_apply] - exact h + refine ⟨EquivLike.inv f a₁, EquivLike.inv f a₂, ?_⟩ + simp_rw [← map_dvd_iff f, EquivLike.apply_inv_apply, h, true_and, ← EquivLike.apply_eq_iff_eq f, + h.2.2, map_mul, EquivLike.apply_inv_apply] /-- If `G` is a `LeftCancelSemiGroup`, left multiplication by `g` yields an equivalence between `G` diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean index a65a2ff44f8..b5bc73430cc 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean @@ -266,8 +266,6 @@ section slope variable [DecidableEq F] --- Non-terminal simps, used to be field_simp -set_option linter.flexible false in lemma addPolynomial_slope {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) = -((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂))) := by @@ -359,8 +357,6 @@ lemma nonsingular_add {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y₁) W.Nonsingular (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) (W.addY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂) := (nonsingular_neg ..).mpr <| nonsingular_negAdd h₁ h₂ hxy --- Non-terminal simp, used to be field_simp -set_option linter.flexible false in /-- The formula `x(P₁ + P₂) = x(P₁ - P₂) - ψ(P₁)ψ(P₂) / (x(P₂) - x(P₁))²`, where `ψ(x,y) = 2y + a₁x + a₃`. -/ lemma addX_eq_addX_negY_sub {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) : @@ -370,8 +366,6 @@ lemma addX_eq_addX_negY_sub {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) simp [field] ring1 --- Non-terminal simp, used to be field_simp -set_option linter.flexible false in /-- The formula `y(P₁)(x(P₂) - x(P₃)) + y(P₂)(x(P₃) - x(P₁)) + y(P₃)(x(P₁) - x(P₂)) = 0`, assuming that `P₁ + P₂ + P₃ = O`. -/ lemma cyclic_sum_Y_mul_X_sub_X {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) : diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean index e7775b65300..ee1f7fef794 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean @@ -261,8 +261,6 @@ lemma dblX_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0) rw [dblX, Y_eq_negY_of_Y_eq hQz hx hy hy'] ring1 --- Non-terminal simp, used to be field_simp -set_option linter.flexible false in private lemma toAffine_addX_of_eq {P : Fin 3 → F} (hPz : P z ≠ 0) {n d : F} (hd : d ≠ 0) : W.toAffine.addX (P x / P z ^ 2) (P x / P z ^ 2) (-n / (P z * d)) = (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) / (P z * d) ^ 2 := by diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean index e2490e681b4..703a6039c43 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean @@ -292,8 +292,6 @@ lemma dblX_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) ( rw [dblX_eq' hP, Y_eq_negY_of_Y_eq hQz hx hy hy'] ring1 --- Non-terminal simp, used to be field_simp -set_option linter.flexible false in private lemma toAffine_addX_of_eq {P : Fin 3 → F} (hPz : P z ≠ 0) {n d : F} (hd : d ≠ 0) : W.toAffine.addX (P x / P z) (P x / P z) (-n / P z / d) = (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d / P z diff --git a/Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean b/Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean index 080431e4470..0bbd1ed50c6 100644 --- a/Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean +++ b/Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean @@ -10,7 +10,6 @@ public import Mathlib.AlgebraicGeometry.Sites.AffineEtale public import Mathlib.CategoryTheory.Functor.TypeValuedFlat public import Mathlib.CategoryTheory.Limits.Elements public import Mathlib.CategoryTheory.Sites.Point.Conservative - public import Mathlib.FieldTheory.SeparableClosure /-! diff --git a/Mathlib/Analysis/Analytic/OfScalars.lean b/Mathlib/Analysis/Analytic/OfScalars.lean index b1465974ddf..f9f06964d5e 100644 --- a/Mathlib/Analysis/Analytic/OfScalars.lean +++ b/Mathlib/Analysis/Analytic/OfScalars.lean @@ -143,7 +143,7 @@ theorem ofScalarsSum_zero : ofScalarsSum c (0 : E) = c 0 • 1 := by @[simp] theorem ofScalarsSum_of_subsingleton [Subsingleton E] {x : E} : ofScalarsSum c x = 0 := by - simp [Subsingleton.eq_zero x, Subsingleton.eq_zero (1 : E)] + simp [Subsingleton.eq_zero (α := E)] @[simp] theorem ofScalarsSum_op [T2Space E] (x : E) : diff --git a/Mathlib/Analysis/LocallyConvex/Basic.lean b/Mathlib/Analysis/LocallyConvex/Basic.lean index cdfd69065a2..4ce40495bb0 100644 --- a/Mathlib/Analysis/LocallyConvex/Basic.lean +++ b/Mathlib/Analysis/LocallyConvex/Basic.lean @@ -230,8 +230,7 @@ variable [TopologicalSpace E] [ContinuousSMul 𝕜 E] /-- Every neighbourhood of the origin is absorbent. -/ theorem absorbent_nhds_zero (hA : A ∈ 𝓝 (0 : E)) : Absorbent 𝕜 A := - absorbent_iff_inv_smul.2 fun x ↦ Filter.tendsto_inv₀_cobounded.smul tendsto_const_nhds <| by - rwa [zero_smul] + absorbent_iff_inv_smul.2 fun _ ↦ Filter.tendsto_inv₀_cobounded.zero_smul_const _ hA /-- The union of `{0}` with the interior of a balanced set is balanced. -/ theorem Balanced.zero_insert_interior (hA : Balanced 𝕜 A) : diff --git a/Mathlib/Analysis/Meromorphic/FactorizedRational.lean b/Mathlib/Analysis/Meromorphic/FactorizedRational.lean index 22febde0beb..a2d9a2215c0 100644 --- a/Mathlib/Analysis/Meromorphic/FactorizedRational.lean +++ b/Mathlib/Analysis/Meromorphic/FactorizedRational.lean @@ -55,7 +55,7 @@ lemma mulSupport (d : 𝕜 → ℤ) : constructor <;> intro h · simp_all only [mem_mulSupport, ne_eq, mem_support] by_contra hCon - simp_all [zpow_zero] + simp_all · simp_all only [mem_mulSupport, ne_eq, ne_iff] use u simp_all [zero_zpow_eq_one₀] diff --git a/Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean b/Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean index 1f7c54af755..aa557fde431 100644 --- a/Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean +++ b/Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean @@ -164,7 +164,8 @@ public theorem StarAlgEquiv.eq_linearIsometryEquivConjStarAlgEquiv -- Assume nontriviality of `V`. by_cases! Subsingleton V · by_cases! Subsingleton W - · use { toLinearEquiv := 0, norm_map' _ := by simp [Subsingleton.eq_zero] } + · use { toLinearEquiv := 0, + norm_map' _ := by simp [Subsingleton.eq_zero (α := V), Subsingleton.eq_zero (α := W)] } exact ext fun _ ↦ Subsingleton.allEq _ _ simpa using congr(f $(Subsingleton.allEq 0 1)) /- By `ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv`, diff --git a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean index c6806b5a510..fc839187ae9 100644 --- a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean +++ b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean @@ -629,6 +629,8 @@ instance instInhabited : Inhabited (E ≃ₗᵢ[R] E) := ⟨refl R E⟩ theorem coe_refl : ⇑(refl R E) = id := rfl +@[simp] theorem toLinearEquiv_refl : (refl R E).toLinearEquiv = .refl R E := rfl + @[simp] theorem toContinuousLinearEquiv_refl : (refl R E).toContinuousLinearEquiv = .refl R E := rfl /-- The inverse `LinearIsometryEquiv`. -/ diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index 47d2ab09a82..de73674c439 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -117,7 +117,9 @@ lemma exp_injOn_Ioc {a b : ℝ} (h : b - a ≤ 2 * π) : InjOn exp (Ioc a b) := exp_injOn_of_forall_sub_mem_Ioo <| fun x ⟨hx1, hx2⟩ y ⟨hy1, hy2⟩ ↦ by constructor <;> linarith /-- The image under `Circle.exp` of the interval of angles `(-r, r)`. -/ -def centeredArc (r : ℝ) : Set Circle := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def centeredArc (r : ℝ) : Set Circle := exp '' {x | |x| < r} theorem bijOn_exp_Ioo_centeredArc {r : ℝ} (hr : r ≤ π) : diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Basic.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Basic.lean index 2af2e998881..c3b553a997d 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Basic.lean @@ -211,7 +211,6 @@ open ContinuousMapZero variable [IsSemitopologicalRing A] [T2Space A] set_option backward.isDefEq.respectTransparency false in -set_option linter.flexible false in -- simp followed by `exact le_rfl` open NonUnitalContinuousFunctionalCalculus in /-- The positive and negative parts of a selfadjoint element `a` are unique. That is, if `a = b - c` is the difference of nonnegative elements whose product is zero, then these are @@ -276,7 +275,7 @@ lemma posPart_negPart_unique {a b c : A} (habc : a = b - c) (hbc : b * c = 0) `b = cfcₙ id b + cfcₙ 0 (-c) = cfcₙ (·⁺) b - cfcₙ (·⁺) (-c) = cfcₙ (·⁺) a = a⁺`, where the second equality follows because these functions are equal on the spectra of `b` and `-c`, respectively, since `0 ≤ b` and `-c ≤ 0`. -/ - let f : C(s, ℝ)₀ := ⟨⟨(·⁺), by fun_prop⟩, by simp; exact le_rfl⟩ + let f : C(s, ℝ)₀ := ⟨⟨(·⁺), by fun_prop⟩, by simp; norm_cast⟩ replace key := congr($key f) simp only [cfcₙHomSuperset_apply, NonUnitalStarAlgHom.coe_mk', NonUnitalAlgHom.coe_mk, ψ, Pi.add_apply, cfcₙHom_eq_cfcₙ_extend (·⁺)] at key diff --git a/Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean b/Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean index 59061499ba9..8f444fe996e 100644 --- a/Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean +++ b/Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean @@ -346,7 +346,7 @@ lemma hasSumLocallyUniformly_derivWeierstrassPExcept (l₀ : ℂ) : Filter.eventually_atTop.mpr ⟨2 * r, ?_⟩ rintro _ h s hs l rfl split_ifs - · simpa using! show 0 ≤ ‖↑l‖ ^ 3 by positivity + · simp have : s ≠ ↑l := by rintro rfl; exfalso; linarith have : l ≠ 0 := by rintro rfl; simp_all; linarith simp only [Complex.norm_div, norm_neg, Complex.norm_ofNat, norm_pow] diff --git a/Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean index e77c76e334d..ffc41995668 100644 --- a/Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean @@ -223,7 +223,6 @@ hypothesis on the interval, but assuming the measure is the volume. theorem intervalIntegrable_log (h : (0 : ℝ) ∉ [[a, b]]) : IntervalIntegrable log μ a b := IntervalIntegrable.log continuousOn_id fun _ hx => ne_of_mem_of_not_mem hx h -set_option linter.flexible false in -- TODO: fix non-terminal simp /-- The real logarithm is interval integrable (with respect to the volume measure) on every interval. See `intervalIntegrable_log` for a version applying to any locally finite measure, but with an @@ -245,8 +244,7 @@ theorem intervalIntegrable_log' : IntervalIntegrable log volume a b := by norm_num at * simpa using! (hasDerivAt_id s).sub (hasDerivAt_mul_log hs.ne.symm) · intro s ⟨hs₁, hs₂⟩ - simp at * - exact (log_nonpos_iff hs₁.le).mpr hs₂.le + grind [Pi.neg_apply, log_nonpos_iff] · -- Show integrability on [1…t] by continuity apply ContinuousOn.intervalIntegrable apply Real.continuousOn_log.mono diff --git a/Mathlib/CategoryTheory/Localization/Predicate.lean b/Mathlib/CategoryTheory/Localization/Predicate.lean index 573923a4041..0c9be1a2c34 100644 --- a/Mathlib/CategoryTheory/Localization/Predicate.lean +++ b/Mathlib/CategoryTheory/Localization/Predicate.lean @@ -69,9 +69,9 @@ end Functor namespace Localization -/-- This universal property states that a functor `L : C ⥤ D` inverts morphisms -in `W` and that all functors `D ⥤ E` (for a fixed category `E`) uniquely factor -through `L`. -/ +/-- This universal property states that a functor `L : C ⥤ D` inverts the morphisms +in `W` and every functor `F : C ⥤ E` (for a fixed category `E`) inverting `W` admits +a unique factorisation through `L`. -/ structure StrictUniversalPropertyFixedTarget where /-- the functor `L` inverts `W` -/ inverts : W.IsInvertedBy L diff --git a/Mathlib/CategoryTheory/Presentable/SharplyLT/Basic.lean b/Mathlib/CategoryTheory/Presentable/SharplyLT/Basic.lean index 2574454c5de..6145f498b08 100644 --- a/Mathlib/CategoryTheory/Presentable/SharplyLT/Basic.lean +++ b/Mathlib/CategoryTheory/Presentable/SharplyLT/Basic.lean @@ -145,7 +145,9 @@ lemma hφ₀ (B : Set X) (hB : HasCardinalLT B κ₂) {T : Type w} (f : T → B) open scoped Classical in /-- This coincides with `φ₀` when `HasCardinalLT B κ₂` holds. -/ -def φ (B : Set X) : Set X := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def φ (B : Set X) : Set X := if hB : HasCardinalLT B κ₂ then φ₀ Y m B hB else B omit [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] [PartialOrder X] in diff --git a/Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean b/Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean index 1501e34ebc3..1e6c4ad8408 100644 --- a/Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean +++ b/Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean @@ -69,7 +69,7 @@ theorem tendsto_order_genFun_term_atTop_nhds_top (f : ℕ → ℕ → R) (i : intro m hm grw [PowerSeries.smul_eq_C_mul, ← le_order_mul] refine lt_add_of_nonneg_of_lt (by simp) ?_ - nontriviality R using Subsingleton.eq_zero + nontriviality R using Subsingleton.eq_zero (α := R⟦X⟧) rw [order_X_pow] norm_cast grind diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean b/Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean index fbe261a305a..ab91795d4ac 100644 --- a/Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean +++ b/Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean @@ -80,7 +80,7 @@ $$ -/ theorem hasProd_powerSeriesMk_card_countRestricted {m : ℕ} (hm : 0 < m) : HasProd (fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j)) (PowerSeries.mk fun n ↦ (#(countRestricted n m) : R)) := by - nontriviality R using Subsingleton.eq_one + nontriviality R using Subsingleton.eq_one (α := R⟦X⟧) convert! hasProd_genFun (fun i c ↦ if c < m then (1 : R) else 0) using 1 · ext1 i rw [sum_range_eq_add_Ico _ hm, sum_Ico_eq_sum_range] diff --git a/Mathlib/Combinatorics/Enumerative/Pentagonal/PowerSeries.lean b/Mathlib/Combinatorics/Enumerative/Pentagonal/PowerSeries.lean index 8a72260798f..329a690d007 100644 --- a/Mathlib/Combinatorics/Enumerative/Pentagonal/PowerSeries.lean +++ b/Mathlib/Combinatorics/Enumerative/Pentagonal/PowerSeries.lean @@ -43,7 +43,7 @@ namespace Pentagonal theorem tendsto_order_pow_mul_prod_one_sub_pow (k : ℕ) : Tendsto (fun n ↦ (X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1)) : R⟦X⟧).order) atTop (𝓝 ⊤) := by - nontriviality R using Subsingleton.eq_zero + nontriviality R using Subsingleton.eq_zero (α := R⟦X⟧) refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr fun n ↦ eventually_atTop.mpr ⟨n + 1, ?_⟩ intro m hm grw [← le_order_mul, order_X_pow] @@ -53,7 +53,7 @@ theorem tendsto_order_pow_mul_prod_one_sub_pow (k : ℕ) : theorem tendsto_order_neg_X_pow (k : ℕ) : Tendsto (fun i ↦ (-(X : R⟦X⟧) ^ (i + k + 1)).order) atTop (𝓝 ⊤) := by - nontriviality R using Subsingleton.eq_zero + nontriviality R using Subsingleton.eq_zero (α := R⟦X⟧) simp_rw [order_neg, order_X_pow, add_assoc] exact ENat.tendsto_natCast_nhds_top.comp (tendsto_add_atTop_nat _) diff --git a/Mathlib/Combinatorics/SetFamily/FourFunctions.lean b/Mathlib/Combinatorics/SetFamily/FourFunctions.lean index 210d4d8c7d6..b966aa3b362 100644 --- a/Mathlib/Combinatorics/SetFamily/FourFunctions.lean +++ b/Mathlib/Combinatorics/SetFamily/FourFunctions.lean @@ -261,8 +261,6 @@ lemma sum_collapse (h𝒜 : 𝒜 ⊆ (insert a u).powerset) (hu : a ∉ u) : variable [ExistsAddOfLE β] --- In the non-terminal simp below, simp runs on four goals, but only needs `exact` once. -set_option linter.flexible false in /-- The **Four Functions Theorem** on a powerset algebra. See `four_functions_theorem` for the finite distributive lattice generalisation. -/ protected lemma Finset.four_functions_theorem (u : Finset α) @@ -273,7 +271,11 @@ protected lemma Finset.four_functions_theorem (u : Finset α) induction u using Finset.induction generalizing f₁ f₂ f₃ f₄ 𝒜 ℬ with | empty => simp only [Finset.powerset_empty, Finset.subset_singleton_iff] at h𝒜 hℬ - obtain rfl | rfl := h𝒜 <;> obtain rfl | rfl := hℬ <;> simp; exact h (subset_refl ∅) subset_rfl + obtain rfl | rfl := h𝒜 + · simp + obtain rfl | rfl := hℬ + · simp + simpa using h (subset_refl ∅) subset_rfl | insert a u hu ih => specialize ih (collapse_nonneg h₁) (collapse_nonneg h₂) (collapse_nonneg h₃) (collapse_nonneg h₄) (collapse_modular hu h₁ h₂ h₃ h₄ h 𝒜 ℬ) Subset.rfl Subset.rfl diff --git a/Mathlib/Combinatorics/SetFamily/LYM.lean b/Mathlib/Combinatorics/SetFamily/LYM.lean index 86cefa4a22f..a5d537a2359 100644 --- a/Mathlib/Combinatorics/SetFamily/LYM.lean +++ b/Mathlib/Combinatorics/SetFamily/LYM.lean @@ -7,9 +7,9 @@ module public import Mathlib.Algebra.Field.Basic public import Mathlib.Algebra.Field.Rat +public import Mathlib.Algebra.Order.Ring.NNRat public import Mathlib.Combinatorics.Enumerative.DoubleCounting public import Mathlib.Combinatorics.SetFamily.Shadow -public import Mathlib.Data.NNRat.Order public import Mathlib.Data.Nat.Cast.Order.Ring /-! diff --git a/Mathlib/Combinatorics/SimpleGraph/Partition.lean b/Mathlib/Combinatorics/SimpleGraph/Partition.lean index e4f586ed8d8..b929a2d9603 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Partition.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Partition.lean @@ -82,7 +82,9 @@ variable {G} variable (P : G.Partition) /-- The part in the partition that `v` belongs to. -/ -def partOfVertex (v : V) : Set V := Classical.choose (P.isPartition.2 v) +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def partOfVertex (v : V) : Set V := Classical.choose (P.isPartition.2 v) theorem partOfVertex_mem (v : V) : P.partOfVertex v ∈ P.parts := by obtain ⟨h, -⟩ := (P.isPartition.2 v).choose_spec.1 @@ -100,13 +102,17 @@ theorem partOfVertex_ne_of_adj {v w : V} (h : G.Adj v w) : P.partOfVertex v ≠ /-- Create a coloring using the parts themselves as the colors. Each vertex is colored by the part it's contained in. -/ -def toColoring : G.Coloring P.parts := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def toColoring : G.Coloring P.parts := Coloring.mk (fun v ↦ ⟨P.partOfVertex v, P.partOfVertex_mem v⟩) fun hvw ↦ by rw [Ne, Subtype.mk_eq_mk] exact P.partOfVertex_ne_of_adj hvw /-- Like `SimpleGraph.Partition.toColoring` but uses `Set V` as the coloring type. -/ -def toColoring' : G.Coloring (Set V) := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def toColoring' : G.Coloring (Set V) := Coloring.mk P.partOfVertex fun hvw ↦ P.partOfVertex_ne_of_adj hvw theorem colorable [Fintype P.parts] : G.Colorable (Fintype.card P.parts) := diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean index a5757901105..ec1a2b83b6d 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean @@ -449,7 +449,6 @@ private theorem edgeDensity_star_not_uniform [Nonempty α] simpa using pow_le_pow_of_le_one (by sz_positivity) hε₁ (show 1 ≤ 5 by simp) grind -set_option linter.flexible false in -- TODO: fix non-terminal simp /-- Lower bound on the edge densities between non-uniform parts of `SzemerediRegularity.increment`. -/ theorem edgeDensity_chunk_not_uniform [Nonempty α] (hPα : #P.parts * 16 ^ #P.parts ≤ card α) @@ -478,8 +477,7 @@ theorem edgeDensity_chunk_not_uniform [Nonempty α] (hPα : #P.parts * 16 ^ #P.p refine le_trans ?_ (mul_le_mul_of_nonneg_right UVl ?_) · norm_num nlinarith - · simp - positivity + · simp [pow_two_nonneg] _ ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (G.edgeDensity ab.1 ab.2 : ℝ) ^ 2) / ↑16 ^ #P.parts := by have t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ diff --git a/Mathlib/Computability/TuringMachine/Config.lean b/Mathlib/Computability/TuringMachine/Config.lean index dd621371498..96491b4d837 100644 --- a/Mathlib/Computability/TuringMachine/Config.lean +++ b/Mathlib/Computability/TuringMachine/Config.lean @@ -269,8 +269,6 @@ theorem exists_code.comp {m n} {f : List.Vector ℕ n →. ℕ} {g : Fin n → L rfl⟩ set_option backward.isDefEq.respectTransparency false in --- TODO: fix non-terminal simp (operates on two goals, with long simp sets) -set_option linter.flexible false in theorem exists_code {n} {f : List.Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) : ∃ c : Code, ∀ v : List.Vector ℕ n, c.eval v.1 = pure <$> f v := by induction hf with @@ -294,11 +292,10 @@ theorem exists_code {n} {f : List.Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) : specialize hf v.tail replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail) simp only [Vector.cons_val, Vector.tail_val] at hf hg - simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, Vector.tail_cons, - Vector.head_cons, PFun.coe_val, Vector.tail_val] + simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, PFun.coe_val, Vector.tail_val] simp only [← Part.pure_eq_some] at hf hg ⊢ induction v.head with - simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, Bind.bind] + | zero => simp [prec, hf, Bind.bind] | succ n _ => suffices ∀ a b, a + b = n → (n.succ :: 0 :: @@ -313,6 +310,7 @@ theorem exists_code {n} {f : List.Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) : (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))) (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by have := Part.eq_some_iff.mpr (this _ _ (zero_add _)) + simp [prec, Part.bind_assoc, Bind.bind] simp_all intro a b e induction b generalizing a with diff --git a/Mathlib/Control/EquivFunctor/Instances.lean b/Mathlib/Control/EquivFunctor/Instances.lean index 9ea26164668..ad99a872ce4 100644 --- a/Mathlib/Control/EquivFunctor/Instances.lean +++ b/Mathlib/Control/EquivFunctor/Instances.lean @@ -29,22 +29,12 @@ instance EquivFunctorPerm : EquivFunctor Perm where map_refl' α := by ext; simp map_trans' _ _ := by ext; simp --- TODO: find a good way to fix the linter --- squeezing the simp makes the second subgoal fail -set_option linter.flexible false in -- There is a classical instance of `LawfulFunctor Finset` available, -- but we provide this computable alternative separately. instance EquivFunctorFinset : EquivFunctor Finset where map e s := s.map e.toEmbedding map_refl' α := by ext; simp - map_trans' k h := by - ext _ a - simp - constructor <;> intro h' - · let ⟨a, ha₁, ha₂⟩ := h' - rw [← ha₂]; simpa - · exists (Equiv.symm k) ((Equiv.symm h) a) - simp [h'] + map_trans' k h := by ext; simp [-trans_toEmbedding] instance EquivFunctorFintype : EquivFunctor Fintype where map e _ := Fintype.ofBijective e e.bijective diff --git a/Mathlib/Data/Complex/Basic.lean b/Mathlib/Data/Complex/Basic.lean index 751a401d267..05d0f1c424d 100644 --- a/Mathlib/Data/Complex/Basic.lean +++ b/Mathlib/Data/Complex/Basic.lean @@ -11,6 +11,7 @@ public import Mathlib.Algebra.Star.Basic public import Mathlib.Data.Real.Basic public import Mathlib.Order.Interval.Set.UnorderedInterval public import Mathlib.Tactic.Ring +public import Mathlib.Util.Qq /-! # The complex numbers @@ -635,6 +636,19 @@ lemma I_pow_eq_pow_mod (n : ℕ) : I ^ n = I ^ (n % 4) := by conv_lhs => rw [← Nat.div_add_mod n 4] simp [pow_add, pow_mul, I_pow_four] +open Qq in +/-- Reduce `Complex.I ^ n` to `Complex.I ^ (n % 4)` when `n` is a literal natural number at +least `4`. Combined with `Nat.reduceMod` this normalises every literal power of `I` to one of +`I ^ 0`, `I ^ 1`, `I ^ 2`, `I ^ 3`, which the existing `@[simp]` lemmas dispatch. -/ +simproc I_pow_eq_pow_mod' (I ^ _) := .ofQ fun u a e => + match u, a, e with + | 1, ~q(ℂ), ~q(I ^ ($n : ℕ)) => do + let some n' := n.nat? | return .continue + if n' < 4 then return .continue + -- we don't reduce `n % 4`, further, since `Nat.reduceMod` will handle that + return .visit <| .mk q(I ^ ($n % 4)) <| .some q(I_pow_eq_pow_mod $n) + | _, _, _ => return .continue + @[simp] theorem sub_re (z w : ℂ) : (z - w).re = z.re - w.re := rfl @@ -729,6 +743,10 @@ theorem div_I (z : ℂ) : z / I = -(z * I) := theorem inv_I : I⁻¹ = -I := by rw [inv_eq_one_div, div_I, one_mul] +lemma I_zpow_eq_zpow_mod (m : ℤ) : I ^ m = I ^ (m % 4) := by + conv_lhs => rw [← Int.mul_ediv_add_emod m 4] + simp [zpow_add₀, zpow_mul, zpow_ofNat] + theorem normSq_inv (z : ℂ) : normSq z⁻¹ = (normSq z)⁻¹ := by simp theorem normSq_div (z w : ℂ) : normSq (z / w) = normSq z / normSq w := by simp diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean index 7bdf67e11ea..5e032bdacc7 100644 --- a/Mathlib/Data/Finset/Basic.lean +++ b/Mathlib/Data/Finset/Basic.lean @@ -511,6 +511,9 @@ theorem toFinset_filter (s : List α) (p : α → Bool) : (s.filter p).toFinset = s.toFinset.filter (p ·) := by ext; simp [List.mem_filter] +theorem filter_toFinset (s : List α) (p : α → Prop) [DecidablePred p] : + s.toFinset.filter p = (s.filter p).toFinset := by simp + end List namespace Finset diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean index 7018b37de1f..4e5dc19df67 100644 --- a/Mathlib/Data/Finset/Card.lean +++ b/Mathlib/Data/Finset/Card.lean @@ -212,6 +212,11 @@ theorem List.toFinset_card_le : #l.toFinset ≤ l.length := theorem List.toFinset_card_of_nodup {l : List α} (h : l.Nodup) : #l.toFinset = l.length := Multiset.toFinset_card_of_nodup h +lemma List.Nodup.card_eq_countP {l : List α} {P : α → Prop} [DecidablePred P] (h : l.Nodup) : + (l.toFinset.filter P).card = countP P l := by + rw [l.countP_eq_length_filter, l.filter_toFinset P] + exact toFinset_card_of_nodup (h.filter P) + end ToMultiset namespace Finset diff --git a/Mathlib/Data/Finset/Density.lean b/Mathlib/Data/Finset/Density.lean index bd7d5064b00..847080985a9 100644 --- a/Mathlib/Data/Finset/Density.lean +++ b/Mathlib/Data/Finset/Density.lean @@ -6,8 +6,8 @@ Authors: Yaël Dillies module public import Mathlib.Algebra.Order.Field.Rat +public import Mathlib.Algebra.Order.Ring.NNRat public import Mathlib.Data.Fintype.Card -public import Mathlib.Data.NNRat.Order public import Mathlib.Data.Rat.Cast.CharZero public import Mathlib.Tactic.Positivity.Basic diff --git a/Mathlib/Data/Finset/Prod.lean b/Mathlib/Data/Finset/Prod.lean index 26c600c391e..d74db48d69e 100644 --- a/Mathlib/Data/Finset/Prod.lean +++ b/Mathlib/Data/Finset/Prod.lean @@ -8,6 +8,7 @@ module public import Mathlib.Data.Finset.Card public import Mathlib.Data.Finset.Union public import Mathlib.Data.List.OffDiag +public import Mathlib.Data.Nat.Choose.Basic /-! # Finsets in product types @@ -366,6 +367,16 @@ theorem offDiag_filter_lt_eq_filter_le {ι} [PartialOrder ι] [DecidableLE ι] [ ext simpa using fun _ _ a ↦ (Ne.le_iff_lt a).symm +/-- The number of strictly ordered pairs `(a, b)` with `a, b ∈ s` is `(#s).choose 2`. -/ +lemma card_product_filter_lt [LinearOrder α] : + #{x ∈ s ×ˢ s | x.1 < x.2} = (#s).choose 2 := by + set u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2} + set v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1} + have disj : Disjoint u v := by grind [disjoint_left] + have union : u.disjUnion v disj = s.offDiag := by grind + have swap : #u = #v := Finset.card_equiv (Equiv.prodComm α α) (by grind) + grind [Nat.mul_sub_one, offDiag_card, Nat.choose_two_right] + end Diag end Finset diff --git a/Mathlib/Data/Finsupp/MonomialOrder.lean b/Mathlib/Data/Finsupp/MonomialOrder.lean index 859628c5d6b..551bdf44f3d 100644 --- a/Mathlib/Data/Finsupp/MonomialOrder.lean +++ b/Mathlib/Data/Finsupp/MonomialOrder.lean @@ -21,7 +21,7 @@ get them as instances. In this formalization, they are presented as a structure `MonomialOrder` which encapsulates `MonomialOrder.toSyn`, an additive and monotone isomorphism to a linearly ordered cancellative additive commutative monoid. -The entry `MonomialOrder.wf` asserts that `MonomialOrder.syn` is well founded. +The entry `MonomialOrder.wellFoundedLT_syn` asserts that `MonomialOrder.syn` is well founded. The terminology comes from commutative algebra and algebraic geometry, especially Gröbner bases, where `c : σ →₀ ℕ` are exponents of monomials. @@ -77,16 +77,16 @@ structure MonomialOrder (σ : Type*) where attribute [instance] MonomialOrder.addCommMonoidSyn MonomialOrder.linearOrderSyn MonomialOrder.isOrderedAddMonoid_syn MonomialOrder.wellFoundedLT_syn +namespace MonomialOrder + +variable {σ : Type*} (m : MonomialOrder σ) + @[deprecated (since := "2026-07-07")] alias acm := MonomialOrder.addCommMonoidSyn @[deprecated (since := "2026-07-07")] alias lo := MonomialOrder.linearOrderSyn @[deprecated (since := "2026-07-07")] alias wf := MonomialOrder.wellFoundedLT_syn -namespace MonomialOrder - -variable {σ : Type*} (m : MonomialOrder σ) - instance : AddCancelCommMonoid m.syn where add_left_cancel := m.toSyn.symm.injective.isLeftCancelAdd _ (map_add _) |>.add_left_cancel diff --git a/Mathlib/Data/Fintype/Prod.lean b/Mathlib/Data/Fintype/Prod.lean index 3af498bdeb3..d385ab7979e 100644 --- a/Mathlib/Data/Fintype/Prod.lean +++ b/Mathlib/Data/Fintype/Prod.lean @@ -60,6 +60,11 @@ theorem Fintype.card_prod (α β : Type*) [Fintype α] [Fintype β] : Fintype.card (α × β) = Fintype.card α * Fintype.card β := card_product _ _ +/-- The number of strictly ordered pairs `(a, b)` in `α` is `(Fintype.card α).choose 2`. -/ +lemma Fintype.card_product_filter_lt [Fintype α] [LinearOrder α] : + #{x : α × α | x.1 < x.2} = (Fintype.card α).choose 2 := by + simpa using Finset.card_product_filter_lt (s := univ) + section attribute [local instance] Fintype.ofFinite in diff --git a/Mathlib/Data/List/Nodup.lean b/Mathlib/Data/List/Nodup.lean index b4a80de0e66..6679355bbc2 100644 --- a/Mathlib/Data/List/Nodup.lean +++ b/Mathlib/Data/List/Nodup.lean @@ -121,6 +121,10 @@ theorem not_nodup_of_get_eq_of_ne (xs : List α) (n m : Fin xs.length) rw [nodup_iff_injective_get] exact fun hinj => hne (hinj h) +lemma Nodup.head_eq_getLast_iff (hne : l ≠ []) (hnd : l.Nodup) : + l.head hne = l.getLast hne ↔ ∃ x, l = [x] := by + cases l <;> grind + -- This is incorrectly named and should be `idxOf_get`; -- this already exists, so will require a deprecation dance. theorem get_idxOf [BEq α] [LawfulBEq α] {l : List α} (H : Nodup l) (i : Fin l.length) : @@ -252,6 +256,26 @@ lemma nodup_tail_reverse (l : List α) (h : l[0]? = l.getLast?) : List.nodup_append_comm] simp [List.getLast_eq_getElem] +lemma Nodup.eq_of_head_mem_of_suffix (h : l₁ <:+ l₂) {hne : l₂ ≠ []} (hl : l₂.head hne ∈ l₁) + (hnd : l₂.Nodup) : l₁ = l₂ := by + grind [List.IsSuffix] + +lemma Nodup.eq_of_getLast_mem_of_prefix (h : l₁ <+: l₂) {hne : l₂ ≠ []} (hl : l₂.getLast hne ∈ l₁) + (hnd : l₂.Nodup) : l₁ = l₂ := by + grind [List.IsPrefix] + +lemma Nodup.prefix_of_head_mem_of_infix (h : l₁ <:+: l₂) {hne : l₂ ≠ []} (hl : l₂.head hne ∈ l₁) + (hnd : l₂.Nodup) : l₁ <+: l₂ := by + grind [List.IsInfix] + +lemma Nodup.suffix_of_getLast_mem_of_infix (h : l₁ <:+: l₂) {hne : l₂ ≠ []} + (hl : l₂.getLast hne ∈ l₁) (hnd : l₂.Nodup) : l₁ <:+ l₂ := by + grind [List.IsInfix] + +lemma Nodup.eq_of_head_mem_of_getLast_mem_of_infix (h : l₁ <:+: l₂) {hne : l₂ ≠ []} + (hlh : l₂.head hne ∈ l₁) (hlg : l₂.getLast hne ∈ l₁) (hnd : l₂.Nodup) : l₁ = l₂ := by + grind [List.IsInfix] + theorem Nodup.erase_getElem [BEq α] [LawfulBEq α] {l : List α} (hl : l.Nodup) (i : Nat) (h : i < l.length) : l.erase l[i] = l.eraseIdx ↑i := by induction l generalizing i with diff --git a/Mathlib/Data/NNRat/Floor.lean b/Mathlib/Data/NNRat/Floor.lean index f7ec482a29d..eb35bbb93f5 100644 --- a/Mathlib/Data/NNRat/Floor.lean +++ b/Mathlib/Data/NNRat/Floor.lean @@ -5,10 +5,11 @@ Authors: Eric Wieser -/ module +public meta import Mathlib.Data.Rat.Floor + public import Mathlib.Algebra.Order.Floor.Semiring -public import Mathlib.Data.NNRat.Order +public import Mathlib.Algebra.Order.Ring.NNRat public import Mathlib.Data.Rat.Floor -public meta import Mathlib.Data.Rat.Floor /-! # Floor Function for Non-negative Rational Numbers diff --git a/Mathlib/Data/NNRat/Order.lean b/Mathlib/Data/NNRat/Order.lean index 84d67a31538..21027d5f34e 100644 --- a/Mathlib/Data/NNRat/Order.lean +++ b/Mathlib/Data/NNRat/Order.lean @@ -5,19 +5,6 @@ Authors: Yaël Dillies, Bhavik Mehta -/ module -public import Mathlib.Data.NNRat.Defs public import Mathlib.Algebra.Order.Ring.Rat -public import Mathlib.Algebra.Order.Nonneg.Ring -/-! -# Bundled ordered algebra structures on `ℚ≥0` - --/ - -public section - -instance : IsStrictOrderedRing ℚ≥0 := Nonneg.isStrictOrderedRing - --- TODO: `deriving instance OrderedSub for NNRat` doesn't work yet, so we add the instance manually -instance NNRat.instOrderedSub : OrderedSub ℚ≥0 := Nonneg.orderedSub -instance NNRat.instCanonicallyOrderedAdd : CanonicallyOrderedAdd ℚ≥0 := Nonneg.canonicallyOrderedAdd +deprecated_module (since := "2026-04-29") diff --git a/Mathlib/Data/Rat/Star.lean b/Mathlib/Data/Rat/Star.lean index 0e10b183895..dfbd8497525 100644 --- a/Mathlib/Data/Rat/Star.lean +++ b/Mathlib/Data/Rat/Star.lean @@ -8,8 +8,8 @@ module public import Mathlib.Algebra.GroupWithZero.Commute public import Mathlib.Algebra.Order.Monoid.Submonoid public import Mathlib.Algebra.Order.Ring.Abs +public import Mathlib.Algebra.Order.Ring.NNRat public import Mathlib.Algebra.Order.Star.Basic -public import Mathlib.Data.NNRat.Order /-! # Star ordered ring structures on `ℚ` and `ℚ≥0` diff --git a/Mathlib/Data/Real/Embedding.lean b/Mathlib/Data/Real/Embedding.lean index 01c3a583913..7f0078f4681 100644 --- a/Mathlib/Data/Real/Embedding.lean +++ b/Mathlib/Data/Real/Embedding.lean @@ -77,7 +77,9 @@ theorem mkRat_mem_ratLt {num : ℤ} {den : ℕ} (hden : den ≠ 0) {x : M} : exact (smul_lt_smul_iff_of_pos_left (Nat.zero_lt_of_ne_zero hm0)).symm /-- `ratLt` as a set of real numbers. -/ -abbrev ratLt' (x : M) : Set ℝ := (Rat.castHom ℝ) '' (ratLt x) +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable abbrev ratLt' (x : M) : Set ℝ := (Rat.castHom ℝ) '' (ratLt x) /-- Mapping `M` to `ℝ`, defined as the supremum of `ratLt' x`. -/ noncomputable diff --git a/Mathlib/Data/Set/Lattice.lean b/Mathlib/Data/Set/Lattice.lean index f93f4440df8..57cde84ea75 100644 --- a/Mathlib/Data/Set/Lattice.lean +++ b/Mathlib/Data/Set/Lattice.lean @@ -884,7 +884,7 @@ theorem sUnion_powerset_gc : /-- `⋃₀` and `𝒫` form a Galois insertion. -/ def sUnionPowersetGI : GaloisInsertion (⋃₀ · : Set (Set α) → Set α) (𝒫 · : Set α → Set (Set α)) := - gi_sSup_Iic + giSSupIic /-- If all sets in a collection are either `∅` or `Set.univ`, then so is their union. -/ theorem sUnion_mem_empty_univ {S : Set (Set α)} (h : S ⊆ {∅, univ}) : diff --git a/Mathlib/Data/Set/MemPartition.lean b/Mathlib/Data/Set/MemPartition.lean index 715e42feb60..6187c7c49ef 100644 --- a/Mathlib/Data/Set/MemPartition.lean +++ b/Mathlib/Data/Set/MemPartition.lean @@ -110,7 +110,9 @@ instance instFintype_memPartition (f : ℕ → Set α) (n : ℕ) : Fintype (memP open scoped Classical in /-- The set in `memPartition f n` to which `a : α` belongs. -/ -def memPartitionSet (f : ℕ → Set α) : ℕ → α → Set α +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def memPartitionSet (f : ℕ → Set α) : ℕ → α → Set α | 0 => fun _ ↦ univ | n + 1 => fun a ↦ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n diff --git a/Mathlib/FieldTheory/CardinalEmb.lean b/Mathlib/FieldTheory/CardinalEmb.lean index d634d57c24f..6156a70cec5 100644 --- a/Mathlib/FieldTheory/CardinalEmb.lean +++ b/Mathlib/FieldTheory/CardinalEmb.lean @@ -179,13 +179,10 @@ def succEquiv (i : ι) : (E⟮ ⟨toLp 2 fun _ ↦ z.val - x, sub_nonneg.mpr z.property.1⟩ invFun z := ⟨min (z.val 0 + x) y, by simp [z.prop, h.out.le]⟩ - map_source' := by simp only [mem_ofPred_eq, Fin.isValue, sub_lt_sub_iff_right, - imp_self, implies_true] + map_source' := by simp map_target' := by simp only [min_lt_iff, mem_ofPred_eq]; intro z hz; left linarith @@ -309,7 +307,6 @@ end Fact.Manifold open Fact.Manifold -set_option backward.isDefEq.respectTransparency false in lemma IccLeftChart_extend_bot : (IccLeftChart x y).extend (𝓡∂ 1) ⊥ = 0 := by norm_num [IccLeftChart, modelWithCornersEuclideanHalfSpace_zero] congr @@ -327,7 +324,6 @@ lemma IccLeftChart_extend_bot_mem_frontier : rw [IccLeftChart_extend_bot, frontier_range_modelWithCornersEuclideanHalfSpace, mem_ofPred, PiLp.zero_apply] -set_option backward.isDefEq.respectTransparency false in /-- The right chart for the topological space `[x, y]`, defined on `(x,y]` and sending `y` to `0` in `EuclideanHalfSpace 1`. -/ @@ -338,8 +334,7 @@ def IccRightChart (x y : ℝ) [h : Fact (x < y)] : toFun z := ⟨toLp 2 fun _ ↦ y - z.val, sub_nonneg.mpr z.property.2⟩ invFun z := ⟨max (y - z.val 0) x, by simp [z.prop, h.out.le, sub_eq_add_neg]⟩ - map_source' := by simp only [mem_ofPred_eq, Fin.isValue, sub_lt_sub_iff_left, - imp_self, implies_true] + map_source' := by simp map_target' := by simp only [lt_max_iff, mem_ofPred_eq]; intro z hz; left linarith @@ -367,7 +362,6 @@ def IccRightChart (x y : ℝ) [h : Fact (x < y)] : continuousOn_toFun := by fun_prop continuousOn_invFun := by fun_prop -set_option backward.isDefEq.respectTransparency false in lemma IccRightChart_extend_top : (IccRightChart x y).extend (𝓡∂ 1) ⊤ = 0 := by norm_num [IccRightChart, modelWithCornersEuclideanHalfSpace_zero] @@ -445,7 +439,6 @@ lemma boundary_product [I.Boundaryless] : (I.prod (𝓡∂ 1)).boundary (M × Icc x y) = Set.prod univ {⊥, ⊤} := by rw [I.boundary_of_boundaryless_left, boundary_Icc] -set_option backward.isDefEq.respectTransparency false in /-- The manifold structure on `[x, y]` is smooth. -/ instance instIsManifoldIcc (x y : ℝ) [Fact (x < y)] {n : ℕ∞ω} : IsManifold (𝓡∂ 1) n (Icc x y) := by diff --git a/Mathlib/GroupTheory/Commutator/Basic.lean b/Mathlib/GroupTheory/Commutator/Basic.lean index bae1b8b7e53..9a0b563f52d 100644 --- a/Mathlib/GroupTheory/Commutator/Basic.lean +++ b/Mathlib/GroupTheory/Commutator/Basic.lean @@ -461,13 +461,17 @@ open Subgroup /-- Representatives `(g₁, g₂) : G × G` of commutators `⁅g₁, g₂⁆ ∈ G`. -/ @[to_additive /-- Representatives `(g₁, g₂) : G × G` of additive commutators `⁅g₁, g₂⁆ ∈ G`. -/] -def commutatorRepresentatives : Set (G × G) := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def commutatorRepresentatives : Set (G × G) := Set.range fun g : commutatorSet G => (g.2.choose, g.2.choose_spec.choose) /-- Subgroup generated by representatives `g₁ g₂ : G` of commutators `⁅g₁, g₂⁆ ∈ G`. -/ @[to_additive /-- Additive subgroup generated by representatives `g₁ g₂ : G` of additive commutators `⁅g₁, g₂⁆ ∈ G`. -/] -def closureCommutatorRepresentatives : Subgroup G := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def closureCommutatorRepresentatives : Subgroup G := closure (Prod.fst '' commutatorRepresentatives G ∪ Prod.snd '' commutatorRepresentatives G) @[to_additive] diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean index 3d9c324060a..e349da7968f 100644 --- a/Mathlib/GroupTheory/Complement.lean +++ b/Mathlib/GroupTheory/Complement.lean @@ -611,11 +611,15 @@ theorem smul_apply_eq_smul_apply_inv_smul (f : F) (S : H.LeftTransversal) (q : G end Action @[to_additive] -instance : Inhabited H.LeftTransversal := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable instance : Inhabited H.LeftTransversal := ⟨⟨Set.range Quotient.out, isComplement_range_left Quotient.out_eq'⟩⟩ @[to_additive] -instance : Inhabited H.RightTransversal := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable instance : Inhabited H.RightTransversal := ⟨⟨Set.range Quotient.out, isComplement_range_right Quotient.out_eq'⟩⟩ theorem IsComplement'.isCompl (h : IsComplement' H K) : IsCompl H K := by diff --git a/Mathlib/GroupTheory/Coprod/Basic.lean b/Mathlib/GroupTheory/Coprod/Basic.lean index c831e8580d9..eb2be828212 100644 --- a/Mathlib/GroupTheory/Coprod/Basic.lean +++ b/Mathlib/GroupTheory/Coprod/Basic.lean @@ -200,7 +200,7 @@ theorem induction_on' {motive : M ∗ N → Prop} (m : M ∗ N) rcases mk_surjective m with ⟨x, rfl⟩ induction x using FreeMonoid.inductionOn' with | one => exact one - | mul_of x xs ih => + | of_mul x xs ih => cases x with | inl m => simpa using inl_mul m _ ih | inr n => simpa using inr_mul n _ ih @@ -582,7 +582,7 @@ theorem con_inv_mul_cancel (x : FreeMonoid (G ⊕ H)) : rw [← mk_eq_mk, map_mul, map_one] induction x using FreeMonoid.inductionOn' with | one => simp - | mul_of x xs ihx => + | of_mul x xs ihx => simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ofList_singleton] rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul] diff --git a/Mathlib/GroupTheory/Coset/Basic.lean b/Mathlib/GroupTheory/Coset/Basic.lean index 5fce88bf808..068c187fb61 100644 --- a/Mathlib/GroupTheory/Coset/Basic.lean +++ b/Mathlib/GroupTheory/Coset/Basic.lean @@ -144,11 +144,11 @@ variable [Group α] {s : Set α} {x : α} @[to_additive mem_leftAddCoset_iff] theorem mem_leftCoset_iff (a : α) : x ∈ a • s ↔ a⁻¹ * x ∈ s := - Iff.intro (fun ⟨b, hb, Eq⟩ => by simp [Eq.symm, hb]) fun h => ⟨a⁻¹ * x, h, by simp⟩ + Iff.intro (fun ⟨b, hb, h⟩ => by simp [h.symm, hb]) fun h => ⟨a⁻¹ * x, h, by simp⟩ @[to_additive mem_rightAddCoset_iff] theorem mem_rightCoset_iff (a : α) : x ∈ op a • s ↔ x * a⁻¹ ∈ s := - Iff.intro (fun ⟨b, hb, Eq⟩ => by simp [Eq.symm, hb]) fun h => ⟨x * a⁻¹, h, by simp⟩ + Iff.intro (fun ⟨b, hb, h⟩ => by simp [h.symm, hb]) fun h => ⟨x * a⁻¹, h, by simp⟩ end CosetGroup diff --git a/Mathlib/GroupTheory/DoubleCoset.lean b/Mathlib/GroupTheory/DoubleCoset.lean index d6e8aeecbd9..c3945c8e429 100644 --- a/Mathlib/GroupTheory/DoubleCoset.lean +++ b/Mathlib/GroupTheory/DoubleCoset.lean @@ -106,7 +106,9 @@ lemma rel_bot_eq_right_group_rel (H : Subgroup G) : exact ⟨b * a⁻¹, h, 1, rfl, by rw [mul_one, inv_mul_cancel_right]⟩ /-- Create a double coset out of an element of `H \ G / K` -/ -def quotToDoubleCoset (H K : Subgroup G) (q : Quotient (H : Set G) K) : Set G := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def quotToDoubleCoset (H K : Subgroup G) (q : Quotient (H : Set G) K) : Set G := doubleCoset q.out H K /-- Map from `G` to `H \ G / K` -/ diff --git a/Mathlib/GroupTheory/FiniteAbelian/Basic.lean b/Mathlib/GroupTheory/FiniteAbelian/Basic.lean index cdbd825b6e0..6ae6c08bf50 100644 --- a/Mathlib/GroupTheory/FiniteAbelian/Basic.lean +++ b/Mathlib/GroupTheory/FiniteAbelian/Basic.lean @@ -158,19 +158,24 @@ lemma equiv_directSum_zmod_of_finite' (G : Type*) [AddCommGroup G] [Finite G] : rintro ⟨i, hi⟩ exact one_lt_pow₀ (hp _).one_lt hi -theorem finite_of_fg_torsion [hG' : AddGroup.FG G] (hG : AddMonoid.IsTorsion G) : Finite G := +theorem finite_of_fg_isAddTorsion [hG' : AddGroup.FG G] (hG : IsAddTorsion G) : Finite G := @Module.finite_of_fg_torsion _ _ _ (Module.Finite.iff_addGroup_fg.mpr hG') <| - AddMonoid.isTorsion_iff_isTorsion_int.mp hG + isAddTorsion_iff_isTorsion_int.mp hG + +@[deprecated (since := "2026-07-01")] alias finite_of_fg_torsion := finite_of_fg_isAddTorsion end AddCommGroup namespace CommGroup -theorem finite_of_fg_torsion [CommGroup G] [Group.FG G] (hG : Monoid.IsTorsion G) : Finite G := - @Finite.of_equiv _ _ (AddCommGroup.finite_of_fg_torsion (Additive G) hG) Multiplicative.ofAdd +@[to_additive existing] +theorem finite_of_fg_isMulTorsion [CommGroup G] [Group.FG G] (hG : IsMulTorsion G) : Finite G := + @Finite.of_equiv _ _ (AddCommGroup.finite_of_fg_isAddTorsion (Additive G) hG) Multiplicative.ofAdd + +@[deprecated (since := "2026-07-01")] alias finite_of_fg_torsion := finite_of_fg_isMulTorsion /-- The **Structure Theorem For Finite Abelian Groups** in a multiplicative version: -A finite commutative group `G` is isomorphic to a finite product of finite cyclic groups. -/ +A finite abelian group `G` is isomorphic to a finite product of finite cyclic groups. -/ theorem equiv_prod_multiplicative_zmod_of_finite (G : Type*) [CommGroup G] [Finite G] : ∃ (ι : Type) (_ : Fintype ι) (n : ι → ℕ), (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i)))) := by @@ -178,9 +183,9 @@ theorem equiv_prod_multiplicative_zmod_of_finite (G : Type*) [CommGroup G] [Fini exact ⟨ι, inst, n, h₁, ⟨MulEquiv.toAdditive.symm <| h₂.some.trans <| (DirectSum.addEquivProd _).trans (MulEquiv.piMultiplicative _).toAdditiveRight⟩⟩ -/-- The **Structure theorem of finitely generated abelian groups** in a multiplicative version : - Any finitely generated abelian group is the product of a power of `ℤ` - and a direct product of some `ZMod (p i ^ e i)` for some prime powers `p i ^ e i`. -/ +/-- The **Structure theorem of finitely generated abelian groups** in a multiplicative version: +Any finitely generated abelian group is the product of a power of `ℤ` +and a direct product of some `ZMod (p i ^ e i)` for some prime powers `p i ^ e i`. -/ theorem equiv_free_prod_prod_multiplicative_zmod (G : Type*) [CommGroup G] [hG : Group.FG G] : ∃ (ι j : Type) (_ : Fintype ι) (_ : Fintype j) (p : ι → ℕ) (_ : ∀ i, Nat.Prime <| p i) (e : ι → ℕ), @@ -199,8 +204,8 @@ namespace Subgroup lemma finiteIndex_range_powMonoidHom_of_fg (A : Type*) [CommGroup A] [Group.FG A] {n : ℕ} (hn : n ≠ 0) : (powMonoidHom (α := A) n).range.FiniteIndex := - finiteIndex_iff_finite_quotient.mpr <| CommGroup.finite_of_fg_torsion _ <| - CommGroup.isTorsion_quotient_range_powMonoidHom A hn + finiteIndex_iff_finite_quotient.mpr <| CommGroup.finite_of_fg_isMulTorsion _ <| + CommGroup.isMulTorsion_quotient_range_powMonoidHom A hn @[to_additive] lemma isFiniteRelIndex_map_powMonoidHom_of_fg {A : Type*} [CommGroup A] {B : Subgroup A} diff --git a/Mathlib/GroupTheory/GroupAction/Defs.lean b/Mathlib/GroupTheory/GroupAction/Defs.lean index caf5017f31e..1e8459e5c76 100644 --- a/Mathlib/GroupTheory/GroupAction/Defs.lean +++ b/Mathlib/GroupTheory/GroupAction/Defs.lean @@ -476,7 +476,9 @@ def selfEquivSigmaOrbits' : α ≃ Σ ω : Ω, ω.orbit := /-- Decomposition of a type `X` as a disjoint union of its orbits under a group action. -/ @[to_additive /-- Decomposition of a type `X` as a disjoint union of its orbits under an additive group action. -/] -def selfEquivSigmaOrbits : α ≃ Σ ω : Ω, orbit G ω.out := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def selfEquivSigmaOrbits : α ≃ Σ ω : Ω, orbit G ω.out := (selfEquivSigmaOrbits' G α).trans <| Equiv.sigmaCongrRight fun _ => Equiv.setCongr <| orbitRel.Quotient.orbit_eq_orbit_out _ Quotient.out_eq' diff --git a/Mathlib/GroupTheory/SchurZassenhaus.lean b/Mathlib/GroupTheory/SchurZassenhaus.lean index 0052fbe5e7c..96c099be0b0 100644 --- a/Mathlib/GroupTheory/SchurZassenhaus.lean +++ b/Mathlib/GroupTheory/SchurZassenhaus.lean @@ -42,7 +42,9 @@ def QuotientDiff := ⟨fun α => diff_self (MonoidHom.id H) α, fun h => by rw [← diff_inv, h, inv_one], fun h h' => by rw [← diff_mul_diff, h, h', one_mul]⟩) -instance : Inhabited H.QuotientDiff := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable instance : Inhabited H.QuotientDiff := inferInstanceAs (Inhabited <| Quotient _) theorem smul_diff_smul' [hH : Normal H] (g : Gᵐᵒᵖ) : diff --git a/Mathlib/GroupTheory/Torsion.lean b/Mathlib/GroupTheory/Torsion.lean index e8bb7939eff..3965c8503da 100644 --- a/Mathlib/GroupTheory/Torsion.lean +++ b/Mathlib/GroupTheory/Torsion.lean @@ -46,58 +46,73 @@ periodic group, aperiodic group, torsion subgroup, torsion abelian group variable {G H : Type*} -namespace Monoid +section variable (G) [Monoid G] /-- A predicate on a monoid saying that all elements are of finite order. -/ @[to_additive /-- A predicate on an additive monoid saying that all elements are of finite order. -/] -def IsTorsion := +def IsMulTorsion := ∀ g : G, IsOfFinOrder g +@[deprecated (since := "2026-07-01")] alias Monoid.IsTorsion := IsMulTorsion +@[deprecated (since := "2026-07-01")] alias AddMonoid.IsTorsion := IsAddTorsion + /-- A monoid is not a torsion monoid if it has an element of infinite order. -/ @[to_additive (attr := simp) -/-- An additive monoid is not a torsion monoid if it has an element of infinite order. -/] -theorem not_isTorsion_iff : ¬IsTorsion G ↔ ∃ g : G, ¬IsOfFinOrder g := +/-- An additive monoid is not a torsion additive monoid if it has an element of infinite order. -/] +theorem not_isMulTorsion_iff : ¬IsMulTorsion G ↔ ∃ g : G, ¬IsOfFinOrder g := not_forall -end Monoid +@[deprecated (since := "2026-07-01")] alias Monoid.not_isTorsion_iff := not_isMulTorsion_iff +@[deprecated (since := "2026-07-01")] alias AddMonoid.not_isTorsion_iff := not_isAddTorsion_iff + +end open Monoid /-- Torsion monoids are really groups. -/ @[to_additive (attr := instance_reducible) -/-- Torsion additive monoids are really additive groups -/] -noncomputable def IsTorsion.group [Monoid G] (tG : IsTorsion G) : Group G := +/-- Torsion additive monoids are really additive groups. -/] +noncomputable def IsMulTorsion.group [Monoid G] (tG : IsMulTorsion G) : Group G := { ‹Monoid G› with inv g := g ^ (orderOf g - 1) inv_mul_cancel g := by rw [← pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one] exact (tG g).orderOf_pos } +@[deprecated (since := "2026-07-01")] alias IsTorsion.group := IsMulTorsion.group +@[deprecated (since := "2026-07-01")] alias IsTorsion.addGroup := IsAddTorsion.addGroup + section Group variable [Group G] {N : Subgroup G} [Group H] /-- Subgroups of torsion groups are torsion groups. -/ -@[to_additive /-- Subgroups of additive torsion groups are additive torsion groups. -/] -theorem IsTorsion.subgroup (tG : IsTorsion G) (H : Subgroup G) : IsTorsion H := fun h ↦ +@[to_additive /-- Additive subgroups of torsion additive groups are torsion additive groups. -/] +theorem IsMulTorsion.subgroup (tG : IsMulTorsion G) (H : Subgroup G) : IsMulTorsion H := fun h ↦ Submonoid.isOfFinOrder_coe.1 <| tG h +@[deprecated (since := "2026-07-01")] alias IsTorsion.subgroup := IsMulTorsion.subgroup +@[deprecated (since := "2026-07-01")] alias IsTorsion.addSubgroup := IsAddTorsion.addSubgroup + /-- The image of a surjective torsion group homomorphism is torsion. -/ -@[to_additive AddIsTorsion.of_surjective -/-- The image of a surjective additive torsion group homomorphism is torsion. -/] -theorem IsTorsion.of_surjective {f : G →* H} (hf : Function.Surjective f) (tG : IsTorsion G) : - IsTorsion H := fun h ↦ by +@[to_additive +/-- The image of a surjective torsion additive group homomorphism is torsion. -/] +theorem IsMulTorsion.of_surjective {f : G →* H} (hf : Function.Surjective f) (tG : IsMulTorsion G) : + IsMulTorsion H := fun h ↦ by obtain ⟨g, rfl⟩ := hf h exact f.isOfFinOrder (tG g) +@[deprecated (since := "2026-06-30")] alias IsTorsion.of_surjective := IsMulTorsion.of_surjective +@[deprecated (since := "2026-06-30")] alias AddIsTorsion.of_surjective := IsAddTorsion.of_surjective + /-- Torsion groups are closed under extensions. -/ -@[to_additive AddIsTorsion.extension_closed -/-- Additive torsion groups are closed under extensions. -/] -theorem IsTorsion.extension_closed {f : G →* H} (hN : N = f.ker) (tH : IsTorsion H) - (tN : IsTorsion N) : IsTorsion G := fun g ↦ by +@[to_additive +/-- Torsion additive groups are closed under extensions. -/] +theorem IsMulTorsion.extension_closed {f : G →* H} (hN : N = f.ker) (tH : IsMulTorsion H) + (tN : IsMulTorsion N) : IsMulTorsion G := fun g ↦ by obtain ⟨ngn, ngnpos, hngn⟩ := (tH <| f g).exists_pow_eq_one have hmem := MonoidHom.mem_ker.mpr ((f.map_pow g ngn).trans hngn) lift g ^ ngn to N using hN.symm ▸ hmem with gn h @@ -105,32 +120,49 @@ theorem IsTorsion.extension_closed {f : G →* H} (hN : N = f.ker) (tH : IsTorsi exact isOfFinOrder_iff_pow_eq_one.mpr <| ⟨ngn * nn, mul_pos ngnpos nnpos, by rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]⟩ +@[deprecated (since := "2026-06-30")] alias IsTorsion.extension_closed := + IsMulTorsion.extension_closed +@[deprecated (since := "2026-06-30")] alias AddIsTorsion.extension_closed := + IsAddTorsion.extension_closed + /-- The image of a quotient is torsion iff the group is torsion. -/ -@[to_additive AddIsTorsion.quotient_iff -/-- The image of a quotient is additively torsion iff the group is torsion. -/] -theorem IsTorsion.quotient_iff {f : G →* H} (hf : Function.Surjective f) (hN : N = f.ker) - (tN : IsTorsion N) : IsTorsion H ↔ IsTorsion G := - ⟨fun tH ↦ IsTorsion.extension_closed hN tH tN, fun tG ↦ IsTorsion.of_surjective hf tG⟩ +@[to_additive +/-- The image of a quotient is torsion iff the additive group is torsion. -/] +theorem IsMulTorsion.quotient_iff {f : G →* H} (hf : Function.Surjective f) (hN : N = f.ker) + (tN : IsMulTorsion N) : IsMulTorsion H ↔ IsMulTorsion G := + ⟨fun tH ↦ IsMulTorsion.extension_closed hN tH tN, fun tG ↦ IsMulTorsion.of_surjective hf tG⟩ + +@[deprecated (since := "2026-06-30")] alias IsTorsion.quotient_iff := IsMulTorsion.quotient_iff +@[deprecated (since := "2026-06-30")] alias AddIsTorsion.quotient_iff := IsAddTorsion.quotient_iff /-- If a group exponent exists, the group is torsion. -/ -@[to_additive ExponentExists.is_add_torsion -/-- If a group exponent exists, the group is additively torsion. -/] -theorem ExponentExists.isTorsion (h : ExponentExists G) : IsTorsion G := fun g ↦ by +@[to_additive +/-- If a group exponent exists, the additive group is torsion. -/] +theorem ExponentExists.isMulTorsion (h : ExponentExists G) : IsMulTorsion G := fun g ↦ by obtain ⟨n, npos, hn⟩ := h exact isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, hn g⟩ +@[deprecated (since := "2026-06-30")] alias ExponentExists.isTorsion := ExponentExists.isMulTorsion +@[deprecated (since := "2026-06-30")] alias ExponentExists.is_add_torsion := + ExponentExists.isAddTorsion + /-- The group exponent exists for any bounded torsion group. -/ -@[to_additive IsAddTorsion.exponentExists -/-- The group exponent exists for any bounded additive torsion group. -/] -theorem IsTorsion.exponentExists (tG : IsTorsion G) +@[to_additive +/-- The group exponent exists for any bounded torsion additive group. -/] +theorem IsMulTorsion.exponentExists (tG : IsMulTorsion G) (bounded : (Set.range fun g : G ↦ orderOf g).Finite) : ExponentExists G := exponent_ne_zero.mp <| (exponent_ne_zero_iff_range_orderOf_finite fun g ↦ (tG g).orderOf_pos).mpr bounded +@[deprecated (since := "2026-07-01")] alias IsTorsion.exponentExists := IsMulTorsion.exponentExists + /-- Finite groups are torsion groups. -/ -@[to_additive is_add_torsion_of_finite /-- Finite additive groups are additive torsion groups. -/] -theorem isTorsion_of_finite [Finite G] : IsTorsion G := - ExponentExists.isTorsion .of_finite +@[to_additive /-- Finite additive groups are torsion additive groups. -/] +theorem isMulTorsion_of_finite [Finite G] : IsMulTorsion G := + ExponentExists.isMulTorsion .of_finite + +@[deprecated (since := "2026-06-30")] alias isTorsion_of_finite := isMulTorsion_of_finite +@[deprecated (since := "2026-06-30")] alias is_add_torsion_of_finite := isAddTorsion_of_finite end Group @@ -138,14 +170,25 @@ section CommGroup variable [CommGroup G] /-- A nontrivial torsion abelian group is not torsion-free. -/ -@[to_additive /-- A nontrivial additive torsion abelian group is not torsion-free. -/] -lemma not_isMulTorsionFree_of_isTorsion [Nontrivial G] (hG : IsTorsion G) : ¬ IsMulTorsionFree G := +@[to_additive /-- A nontrivial torsion additive abelian group is not torsion-free. -/] +lemma not_isMulTorsionFree_of_isMulTorsion [Nontrivial G] (hG : IsMulTorsion G) : + ¬ IsMulTorsionFree G := not_isMulTorsionFree_iff_isOfFinOrder.2 <| let ⟨x, hx⟩ := exists_ne (1 : G); ⟨x, hx, hG x⟩ +@[deprecated (since := "2026-07-01")] alias not_isMulTorsionFree_of_isTorsion := + not_isMulTorsionFree_of_isMulTorsion +@[deprecated (since := "2026-07-01")] alias not_isAddTorsionFree_of_isTorsion := + not_isAddTorsionFree_of_isAddTorsion + /-- A nontrivial torsion-free abelian group is not torsion. -/ -@[to_additive /-- A nontrivial additive torsion-free abelian group is not torsion. -/] -lemma not_isTorsion_of_isMulTorsionFree [Nontrivial G] [IsMulTorsionFree G] : ¬ IsTorsion G := - (not_isMulTorsionFree_of_isTorsion · ‹_›) +@[to_additive /-- A nontrivial torsion-free additive abelian group is not torsion. -/] +lemma not_isMulTorsion_of_isMulTorsionFree [Nontrivial G] [IsMulTorsionFree G] : ¬ IsMulTorsion G := + (not_isMulTorsionFree_of_isMulTorsion · ‹_›) + +@[deprecated (since := "2026-07-01")] alias not_isTorsion_of_isMulTorsionFree := + not_isMulTorsion_of_isMulTorsionFree +@[deprecated (since := "2026-07-01")] alias not_isTorsion_of_isAddTorsionFree := + not_isAddTorsion_of_isAddTorsionFree end CommGroup @@ -154,19 +197,22 @@ section Module -- A (semi/)ring of scalars and a commutative monoid of elements variable (R M : Type*) [AddCommMonoid M] -namespace AddMonoid - -/-- A module whose scalars are additively torsion is additively torsion. -/ -theorem IsTorsion.module_of_torsion [Semiring R] [Module R M] (tR : IsTorsion R) : IsTorsion M := +/-- A module whose scalars are torsion is torsion. -/ +theorem IsAddTorsion.module_of_torsion [Semiring R] [Module R M] (tR : IsAddTorsion R) : + IsAddTorsion M := fun f ↦ isOfFinAddOrder_iff_nsmul_eq_zero.mpr <| by obtain ⟨n, npos, hn⟩ := (tR 1).exists_nsmul_eq_zero exact ⟨n, npos, by simp only [← Nat.cast_smul_eq_nsmul R _ f, ← nsmul_one, hn, zero_smul]⟩ -/-- A module with a finite ring of scalars is additively torsion. -/ -theorem IsTorsion.module_of_finite [Ring R] [Finite R] [Module R M] : IsTorsion M := - (is_add_torsion_of_finite : IsTorsion R).module_of_torsion _ _ +@[deprecated (since := "2026-07-01")] alias AddMonoid.IsTorsion.module_of_torsion := + IsAddTorsion.module_of_torsion + +/-- A module with a finite ring of scalars is torsion. -/ +theorem IsAddTorsion.module_of_finite [Ring R] [Finite R] [Module R M] : IsAddTorsion M := + (isAddTorsion_of_finite : IsAddTorsion R).module_of_torsion _ _ -end AddMonoid +@[deprecated (since := "2026-07-01")] alias AddMonoid.IsTorsion.module_of_finite := + IsAddTorsion.module_of_finite end Module @@ -178,9 +224,9 @@ namespace CommMonoid /-- The torsion submonoid of a commutative monoid. -(Note that by `Monoid.IsTorsion.group` torsion monoids are truthfully groups.) +(Note that by `IsMulTorsion.group` torsion monoids are truthfully groups.) -/ -@[to_additive addTorsion /-- The torsion submonoid of an additive commutative monoid. -/] +@[to_additive addTorsion /-- The torsion additive submonoid of an additive commutative monoid. -/] def torsion : Submonoid G where carrier := { x | IsOfFinOrder x } one_mem' := IsOfFinOrder.one @@ -197,8 +243,8 @@ variable {G} set_option backward.isDefEq.respectTransparency false in /-- Torsion submonoids are torsion. -/ -@[to_additive /-- Additive torsion submonoids are additively torsion. -/] -theorem torsion.isTorsion : IsTorsion <| torsion G := fun ⟨x, n, npos, hn⟩ ↦ +@[to_additive /-- Torsion additive submonoids are torsion. -/] +theorem torsion.isMulTorsion : IsMulTorsion <| torsion G := fun ⟨x, n, npos, hn⟩ ↦ ⟨n, npos, Subtype.ext <| by dsimp @@ -207,6 +253,10 @@ theorem torsion.isTorsion : IsTorsion <| torsion G := fun ⟨x, n, npos, hn⟩ rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk, (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]⟩ +@[deprecated (since := "2026-07-01")] alias torsion.isTorsion := torsion.isMulTorsion +@[deprecated (since := "2026-07-01")] alias _root_.AddCommMonoid.addTorsion.isTorsion := + AddCommMonoid.addTorsion.isAddTorsion + variable (G) (p : ℕ) /-- The `p`-primary component is the submonoid of elements `g` such that `g ^ p ^ k = 1` @@ -262,38 +312,51 @@ end CommMonoid open CommMonoid (torsion) -namespace Monoid.IsTorsion +namespace IsMulTorsion variable {G} /-- The torsion submonoid of a torsion monoid is `⊤`. -/ @[to_additive (attr := simp) -/-- The additive torsion submonoid of an additive torsion monoid is `⊤`. -/] -theorem torsion_eq_top (tG : IsTorsion G) : torsion G = ⊤ := by ext; tauto +/-- The torsion additive submonoid of a torsion additive monoid is `⊤`. -/] +theorem torsion_eq_top (tG : IsMulTorsion G) : torsion G = ⊤ := by ext; tauto /-- A torsion monoid is isomorphic to its torsion submonoid. -/ -@[to_additive /-- An additive torsion monoid is isomorphic to its torsion submonoid. -/] -def torsionMulEquiv (tG : IsTorsion G) : torsion G ≃* G := +@[to_additive (attr := simps!) +/-- A torsion additive monoid is isomorphic to its torsion additive submonoid. -/] +def torsionMulEquiv (tG : IsMulTorsion G) : torsion G ≃* G := (MulEquiv.submonoidCongr tG.torsion_eq_top).trans Submonoid.topEquiv -@[to_additive] -theorem torsionMulEquiv_apply (tG : IsTorsion G) (a : torsion G) : - tG.torsionMulEquiv a = MulEquiv.submonoidCongr tG.torsion_eq_top a := - rfl +end IsMulTorsion -@[to_additive] -theorem torsionMulEquiv_symm_apply_coe (tG : IsTorsion G) (a : G) : - tG.torsionMulEquiv.symm a = ⟨Submonoid.topEquiv.symm a, tG _⟩ := - rfl +@[deprecated (since := "2026-07-01")] alias Monoid.IsTorsion.torsion_eq_top := + IsMulTorsion.torsion_eq_top +@[deprecated (since := "2026-07-01")] alias AddMonoid.IsTorsion.torsion_eq_top := + IsAddTorsion.torsion_eq_top + +@[deprecated (since := "2026-07-01")] alias Monoid.IsTorsion.torsionMulEquiv := + IsMulTorsion.torsionMulEquiv +@[deprecated (since := "2026-07-01")] alias AddMonoid.IsTorsion.torsionAddEquiv := + IsAddTorsion.torsionAddEquiv -end Monoid.IsTorsion +@[deprecated (since := "2026-07-01")] alias Monoid.IsTorsion.torsionMulEquiv_apply := + IsMulTorsion.torsionMulEquiv_apply +@[deprecated (since := "2026-07-01")] alias AddMonoid.IsTorsion.torsionAddEquiv_apply := + IsAddTorsion.torsionAddEquiv_apply + +@[deprecated (since := "2026-07-01")] alias Monoid.IsTorsion.torsionMulEquiv_symm_apply_coe := + IsMulTorsion.torsionMulEquiv_symm_apply_coe +@[deprecated (since := "2026-07-01")] alias AddMonoid.IsTorsion.torsionAddEquiv_symm_apply_coe := + IsAddTorsion.torsionAddEquiv_symm_apply_coe /-- Torsion submonoids of a torsion submonoid are isomorphic to the submonoid. -/ -@[to_additive (attr := simp) AddCommMonoid.Torsion.ofTorsion -/-- Additive torsion submonoids of an additive torsion submonoid are -isomorphic to the submonoid. -/] -def Torsion.ofTorsion : torsion (torsion G) ≃* torsion G := - Monoid.IsTorsion.torsionMulEquiv CommMonoid.torsion.isTorsion +@[to_additive (attr := simp) +/-- Torsion additive submonoids of a torsion additive submonoid are +isomorphic to the additive submonoid. -/] +def CommMonoid.Torsion.ofTorsion : torsion (torsion G) ≃* torsion G := + IsMulTorsion.torsionMulEquiv CommMonoid.torsion.isMulTorsion + +@[deprecated (since := "2026-07-01")] alias Torsion.ofTorsion := CommMonoid.Torsion.ofTorsion end CommMonoid @@ -304,24 +367,28 @@ variable (G) [CommGroup G] [CommGroup H] namespace CommGroup /-- The torsion subgroup of an abelian group. -/ -@[to_additive /-- The torsion subgroup of an additive abelian group. -/] +@[to_additive /-- The torsion additive subgroup of an additive abelian group. -/] def torsion : Subgroup G := { CommMonoid.torsion G with inv_mem' := fun hx ↦ IsOfFinOrder.inv hx } /-- The torsion submonoid of an abelian group equals the torsion subgroup as a submonoid. -/ -@[to_additive add_torsion_eq_add_torsion_submonoid -/-- The additive torsion submonoid of an abelian group equals the torsion -subgroup as a submonoid. -/] +@[to_additive +/-- The torsion additive submonoid of an abelian group equals the torsion +additive subgroup as an additive submonoid. -/] theorem torsion_eq_torsion_submonoid : CommMonoid.torsion G = (torsion G).toSubmonoid := rfl +@[deprecated (since := "2026-07-01")] alias + _root_.AddCommGroup.add_torsion_eq_add_torsion_submonoid := + AddCommGroup.torsion_eq_torsion_addSubmonoid + variable {G} @[to_additive] theorem mem_torsion (g : G) : g ∈ torsion G ↔ IsOfFinOrder g := Iff.rfl @[to_additive] -lemma torsion_eq_top_iff : torsion G = ⊤ ↔ IsTorsion G := +lemma torsion_eq_top_iff : torsion G = ⊤ ↔ IsMulTorsion G := (torsion G).eq_top_iff' @[to_additive] @@ -359,13 +426,19 @@ lemma torsion_prod : torsion (G × H) = (torsion G).prod (torsion H) := by variable (G) @[to_additive] -lemma isTorsion_quotient_range_powMonoidHom {n : ℕ} (hn : n ≠ 0) : - Monoid.IsTorsion (G ⧸ (powMonoidHom (α := G) n).range) := by - simp only [Monoid.IsTorsion, isOfFinOrder_iff_pow_eq_one] +lemma isMulTorsion_quotient_range_powMonoidHom {n : ℕ} (hn : n ≠ 0) : + IsMulTorsion (G ⧸ (powMonoidHom (α := G) n).range) := by + simp only [IsMulTorsion, isOfFinOrder_iff_pow_eq_one] refine fun g ↦ QuotientGroup.induction_on g fun a ↦ ⟨n, hn.pos, ?_⟩ rw [← QuotientGroup.mk_pow, QuotientGroup.eq_one_iff] simp +@[deprecated (since := "2026-07-01")] alias isTorsion_quotient_range_powMonoidHom := + isMulTorsion_quotient_range_powMonoidHom +@[deprecated (since := "2026-07-01")] alias + _root_.AddCommGroup.isTorsion_quotient_range_nsmulAddMonoidHom := + AddCommGroup.isAddTorsion_quotient_range_nsmulAddMonoidHom + variable (p : ℕ) /-- The `p`-primary component is the subgroup of elements `g` such that `g ^ p ^ k = 1` @@ -411,16 +484,16 @@ theorem freeRank_def [Group.FG G] : freeRank G = Group.rank (G ⧸ torsion G) := variable {G H} @[to_additive] -theorem freeRank_eq_zero_iff [Group.FG G] : freeRank G = 0 ↔ IsTorsion G := by +theorem freeRank_eq_zero_iff [Group.FG G] : freeRank G = 0 ↔ IsMulTorsion G := by rw [freeRank, Group.rank_eq_zero_iff, QuotientGroup.subsingleton_iff, torsion_eq_top_iff] @[to_additive] -theorem freeRank_eq_zero (hG : IsTorsion G) [Group.FG G] : freeRank G = 0 := +theorem freeRank_eq_zero (hG : IsMulTorsion G) [Group.FG G] : freeRank G = 0 := freeRank_eq_zero_iff.mpr hG @[to_additive] theorem freeRank_eq_zero_of_finite [Finite G] : freeRank G = 0 := - freeRank_eq_zero isTorsion_of_finite + freeRank_eq_zero isMulTorsion_of_finite @[to_additive] theorem freeRank_congr [Group.FG G] [Group.FG H] (e : G ≃* H) : freeRank G = freeRank H := @@ -440,7 +513,8 @@ open CommGroup (torsion) /-- Quotienting a group by its torsion subgroup yields a torsion-free group. -/ @[to_additive -/-- Quotienting a group by its additive torsion subgroup yields an additive torsion-free group. -/] +/-- Quotienting an additive group by its torsion additive subgroup yields a torsion-free additive +group. -/] instance _root_.QuotientGroup.instIsMulTorsionFree : IsMulTorsionFree <| G ⧸ torsion G := by refine .of_not_isOfFinOrder fun g hne hfin ↦ hne ?_ obtain ⟨g⟩ := g diff --git a/Mathlib/GroupTheory/Transfer.lean b/Mathlib/GroupTheory/Transfer.lean index eef6c92a2cc..ff5a8110579 100644 --- a/Mathlib/GroupTheory/Transfer.lean +++ b/Mathlib/GroupTheory/Transfer.lean @@ -27,7 +27,7 @@ In this file we construct the transfer homomorphism. If `hP : N(P) ≤ C(P)`, then `(transfer P hP).ker` is a normal `p`-complement. -/ -@[expose] public section +@[expose] public noncomputable section variable {G : Type*} [Group G] {H : Subgroup G} {A : Type*} [CommGroup A] (ϕ : H →* A) @@ -44,7 +44,7 @@ variable (R S T : H.LeftTransversal) [FiniteIndex H] /-- The difference of two left transversals -/ @[to_additive /-- The difference of two left transversals -/] -noncomputable def diff : A := +def diff : A := let α := S.2.leftQuotientEquiv let β := T.2.leftQuotientEquiv let _ := H.fintypeQuotientOfFiniteIndex @@ -86,7 +86,7 @@ variable (H) in /-- The transfer transversal as a function. Given a `⟨g⟩`-orbit `q₀, g • q₀, ..., g ^ (m - 1) • q₀` in `G ⧸ H`, an element `g ^ k • q₀` is mapped to `g ^ k • g₀` for a fixed choice of representative `g₀` of `q₀`. -/ -noncomputable def transferFunction : G ⧸ H → G := fun q => +def transferFunction : G ⧸ H → G := fun q => g ^ (cast (quotientEquivSigmaZMod H g q).2 : ℤ) * (quotientEquivSigmaZMod H g q).1.out.out lemma transferFunction_apply (q : G ⧸ H) : @@ -145,7 +145,7 @@ open MulAction Subgroup Subgroup.leftTransversals the transfer homomorphism is `transfer ϕ : G →* A`. -/ @[to_additive /-- Given `ϕ : H →+ A` from `H : AddSubgroup G` to an additive commutative group `A`, the transfer homomorphism is `transfer ϕ : G →+ A`. -/] -noncomputable def transfer [FiniteIndex H] : G →* A := +def transfer [FiniteIndex H] : G →* A := let T : H.LeftTransversal := default { toFun := fun g => diff ϕ T (g • T) map_one' := by rw [one_smul, diff_self] @@ -228,7 +228,7 @@ theorem transfer_center_eq_pow [FiniteIndex (center G)] (g : G) : variable (G) in /-- The transfer homomorphism `G →* center G`. -/ -noncomputable def transferCenterPow [FiniteIndex (center G)] : G →* center G where +def transferCenterPow [FiniteIndex (center G)] : G →* center G where toFun g := ⟨g ^ (center G).index, (center G).pow_index_mem g⟩ map_one' := Subtype.ext (one_pow (center G).index) map_mul' a b := by simp_rw [← show ∀ _, (_ : center G) = _ from transfer_center_eq_pow, map_mul] @@ -245,7 +245,7 @@ include hP open scoped IsMulCommutative in /-- The homomorphism `G →* P` in Burnside's transfer theorem. -/ -noncomputable def transferSylow [P.FiniteIndex] : G →* P := +def transferSylow [P.FiniteIndex] : G →* P := haveI : IsMulCommutative P := ⟨⟨fun a b => Subtype.ext (hP (le_normalizer b.2) a a.2)⟩⟩ transfer (MonoidHom.id P) diff --git a/Mathlib/InformationTheory/Coding/KraftMcMillan.lean b/Mathlib/InformationTheory/Coding/KraftMcMillan.lean index e960a8b2de9..93f45d0b966 100644 --- a/Mathlib/InformationTheory/Coding/KraftMcMillan.lean +++ b/Mathlib/InformationTheory/Coding/KraftMcMillan.lean @@ -90,7 +90,6 @@ private lemma concatFn_length_mem_Icc {S : Finset (List α)} · -- upper bound exact (Finset.sum_le_sum (fun i _ => Finset.le_sup (w i).prop)).trans_eq (by simp) -set_option linter.flexible false in -- TODO: fix non-terminal simp /-- Auxiliary bound for Kraft–McMillan. If `S` is a finite uniquely decodable code and `1 ≤ r`, then the `r`-th power of its Kraft sum @@ -137,9 +136,7 @@ private lemma kraft_mcmillan_inequality_aux {S : Finset (List α)} [Fintype α] -- Summing these bounds over the interval s ∈ [r, r * maxLen] multiplies the term -- by the number of lengths. Since r ≥ 1, this count is at most r * maxLen. rcases r with (_ | _ | r) <;> rcases maxLen with (_ | _ | maxLen) - all_goals try simp at * - · positivity - · rw [Nat.cast_sub] <;> push_cast <;> nlinarith only + <;> simp at * <;> norm_cast <;> simp open Filter diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean index 8aa500bba2a..199ab8efa60 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean @@ -7,7 +7,6 @@ module public import Mathlib.LinearAlgebra.AffineSpace.AffineEquiv public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs - public import Mathlib.Algebra.NoZeroSMulDivisors.Basic /-! diff --git a/Mathlib/LinearAlgebra/Basis/Flag.lean b/Mathlib/LinearAlgebra/Basis/Flag.lean index 13d132de028..6659869cbbd 100644 --- a/Mathlib/LinearAlgebra/Basis/Flag.lean +++ b/Mathlib/LinearAlgebra/Basis/Flag.lean @@ -19,7 +19,10 @@ to be the subspace spanned by the first `k` vectors of the basis `b`. We also prove some lemmas about this definition. -/ -@[expose] public section +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- This is why this section is `noncomputable`. +-- See https://github.com/leanprover/lean4/issues/14084. +@[expose] public noncomputable section open Set Submodule diff --git a/Mathlib/LinearAlgebra/Basis/VectorSpace.lean b/Mathlib/LinearAlgebra/Basis/VectorSpace.lean index 967d8c9c2e7..da1e7bed2f4 100644 --- a/Mathlib/LinearAlgebra/Basis/VectorSpace.lean +++ b/Mathlib/LinearAlgebra/Basis/VectorSpace.lean @@ -69,7 +69,9 @@ theorem range_extend (hs : LinearIndepOn K id s) : /-- Auxiliary definition: the index for the new basis vectors in `Basis.sumExtend`. The specific value of this definition should be considered an implementation detail. -/ -def sumExtendIndex (hs : LinearIndependent K v) : Set V := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def sumExtendIndex (hs : LinearIndependent K v) : Set V := LinearIndepOn.extend hs.linearIndepOn_id (subset_univ _) \ range v /-- If `v` is a linear independent family of vectors, extend it to a basis indexed by a sum type. -/ diff --git a/Mathlib/LinearAlgebra/Matrix/Defs.lean b/Mathlib/LinearAlgebra/Matrix/Defs.lean index f0c9653717e..e5c634e31ac 100644 --- a/Mathlib/LinearAlgebra/Matrix/Defs.lean +++ b/Mathlib/LinearAlgebra/Matrix/Defs.lean @@ -104,6 +104,14 @@ def ofArray {m n : ℕ} (A : Array R) (hA : A.size = m * n) : Matrix (Fin m) (Fi theorem ofArray_apply {m n : ℕ} (A : Array R) (hA : A.size = m * n) (i : Fin m) (j : Fin n) : ofArray A hA i j = A[Fin.mkDivMod i j] := rfl +/-- The matrix constructed from the row-major array of `A`'s entries is `A`. -/ +@[simp] +theorem ofArray_ofFn {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) : + ofArray (.ofFn fun k : Fin (m * n) ↦ A k.divNat k.modNat) Array.size_ofFn = A := by + ext i j + rw [ofArray_apply, Fin.getElem_fin, Array.getElem_ofFn, Fin.divNat_mkDivMod, + Fin.modNat_mkDivMod] + lemma ofArray_eq_of_getD [Zero R] {m n : ℕ} (A : Array R) (hA : A.size = m * n) : ofArray A hA = .of fun i j ↦ A.getD (n * i.val + j.val) 0 := by ext i j diff --git a/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean b/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean index 405485f7461..30f274638e5 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean @@ -301,7 +301,7 @@ lemma _root_.FreeAddMonoid.toPiTensorProduct (p : FreeAddMonoid (R × Π i, s i) List.sum (List.map (fun x ↦ x.1 • ⨂ₜ[R] i, x.2 i) p.toList) := by induction p using FreeAddMonoid.inductionOn' with | zero => rfl - | add_of b a ih => + | of_add b a ih => rw [FreeAddMonoid.toList_of_add, List.map_cons, List.sum_cons, ← ih, ← tprodCoeff_eq_smul_tprod] rfl diff --git a/Mathlib/LinearAlgebra/StdBasis.lean b/Mathlib/LinearAlgebra/StdBasis.lean index 6e83f65a5ce..173420427c5 100644 --- a/Mathlib/LinearAlgebra/StdBasis.lean +++ b/Mathlib/LinearAlgebra/StdBasis.lean @@ -137,7 +137,9 @@ theorem basisFun_equivFun : (Pi.basisFun R η).equivFun = LinearEquiv.refl _ _ : variable {η} /-- The `R`-submodule of `η → R` consisting of functions supported in the subset `s`. -/ -def spanSubset (s : Set η) : Submodule R (η → R) := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def spanSubset (s : Set η) : Submodule R (η → R) := .span R (Pi.basisFun R η '' s) variable {R} {s : Set η} diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean index ebcd43198e0..ddf2c7599e4 100644 --- a/Mathlib/Logic/Basic.lean +++ b/Mathlib/Logic/Basic.lean @@ -8,7 +8,6 @@ module public import Mathlib.Lean.Meta.Simp public import Batteries.Logic public import Batteries.Util.LibraryNote - public import Mathlib.Tactic.Attr.Register /-! diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean index 62d08038e1f..0cf4995802c 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean @@ -1018,7 +1018,7 @@ theorem Measurable.liminf' {ι ι'} {f : ι → δ → α} {v : Filter ι} (hf : rw [ofPred_forall] exact MeasurableSet.iInter (fun j ↦ (m_meas j).compl) refine measurable_const.piecewise mc_meas <| .iSup fun j ↦ ?_ - let reparam : δ → Subtype p → Subtype p := fun x ↦ liminf_reparam (fun i ↦ f i x) s p + let reparam : δ → Subtype p → Subtype p := fun x ↦ liminfReparam (fun i ↦ f i x) s p let F0 : Subtype p → δ → α := fun j x ↦ ⨅ (i : s j), f i x have F0_meas : ∀ j, Measurable (F0 j) := fun j ↦ .iInf (fun (i : s j) ↦ hf i) set F1 : δ → α := fun x ↦ F0 (reparam x j) x with hF1 diff --git a/Mathlib/MeasureTheory/Constructions/ClosedCompactCylinders.lean b/Mathlib/MeasureTheory/Constructions/ClosedCompactCylinders.lean index 2321bf6e04a..ae61a053e05 100644 --- a/Mathlib/MeasureTheory/Constructions/ClosedCompactCylinders.lean +++ b/Mathlib/MeasureTheory/Constructions/ClosedCompactCylinders.lean @@ -55,7 +55,9 @@ noncomputable def closedCompactCylinders.finset (ht : t ∈ closedCompactCylinde ((mem_closedCompactCylinders t).mp ht).choose /-- A set `S` such that `t = cylinder s S`. `s` is given by `closedCompactCylinders.finset`. -/ -def closedCompactCylinders.set (ht : t ∈ closedCompactCylinders X) : +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def closedCompactCylinders.set (ht : t ∈ closedCompactCylinders X) : Set (Π i : closedCompactCylinders.finset ht, X i) := ((mem_closedCompactCylinders t).mp ht).choose_spec.choose diff --git a/Mathlib/MeasureTheory/Constructions/Cylinders.lean b/Mathlib/MeasureTheory/Constructions/Cylinders.lean index e75df0ba659..1e28d660c5a 100644 --- a/Mathlib/MeasureTheory/Constructions/Cylinders.lean +++ b/Mathlib/MeasureTheory/Constructions/Cylinders.lean @@ -294,7 +294,9 @@ noncomputable def measurableCylinders.finset (ht : t ∈ measurableCylinders α) ((mem_measurableCylinders t).mp ht).choose /-- A set `S` such that `t = cylinder s S`. `s` is given by `measurableCylinders.finset`. -/ -def measurableCylinders.set (ht : t ∈ measurableCylinders α) : +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def measurableCylinders.set (ht : t ∈ measurableCylinders α) : Set (∀ i : measurableCylinders.finset ht, α i) := ((mem_measurableCylinders t).mp ht).choose_spec.choose diff --git a/Mathlib/MeasureTheory/Covering/VitaliFamily.lean b/Mathlib/MeasureTheory/Covering/VitaliFamily.lean index 90dd8d16596..39f485fac5c 100644 --- a/Mathlib/MeasureTheory/Covering/VitaliFamily.lean +++ b/Mathlib/MeasureTheory/Covering/VitaliFamily.lean @@ -117,7 +117,9 @@ theorem exists_disjoint_covering_ae : /-- Given `h : v.FineSubfamilyOn f s`, then `h.index` is a set parametrizing a disjoint covering of almost every `s`. -/ -protected def index : Set (X × Set X) := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +protected noncomputable def index : Set (X × Set X) := h.exists_disjoint_covering_ae.choose /-- Given `h : v.FineSubfamilyOn f s`, then `h.covering p` is a set in the family, diff --git a/Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean b/Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean index 857b7734857..7d9cc492ad5 100644 --- a/Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean +++ b/Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean @@ -21,7 +21,7 @@ and a measurable set `aeSeqSet hf p`, such that * `x ∈ aeSeqSet hf p → p x (fun n ↦ f n x)` -/ -@[expose] public section +@[expose] public noncomputable section open MeasureTheory @@ -38,7 +38,7 @@ def aeSeqSet (hf : ∀ i, AEMeasurable (f i) μ) (p : α → (ι → β) → Pro open scoped Classical in /-- A sequence of measurable functions that are equal to `f` and verify property `p` on the measurable set `aeSeqSet hf p`. -/ -noncomputable def aeSeq (hf : ∀ i, AEMeasurable (f i) μ) (p : α → (ι → β) → Prop) : ι → α → β := +def aeSeq (hf : ∀ i, AEMeasurable (f i) μ) (p : α → (ι → β) → Prop) : ι → α → β := fun i x => ite (x ∈ aeSeqSet hf p) ((hf i).mk (f i) x) (⟨f i x⟩ : Nonempty β).some namespace aeSeq diff --git a/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean b/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean index 9c0a2c36600..ca5624ada9c 100644 --- a/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean +++ b/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean @@ -811,4 +811,31 @@ theorem smul_continuousOn [LocallyCompactSpace X] [T2Space X] {𝕜 : Type*} [No end LocallyIntegrableOn +namespace LocallyIntegrable + +variable [LocallyCompactSpace X] [T2Space X] [NormedRing R] [SecondCountableTopologyEither X R] + {𝕜 : Type*} [NormedRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] + +theorem continuous_mul {f g : X → R} (hg : Continuous g) + (hf : LocallyIntegrable f μ) : LocallyIntegrable (fun x => g x * f x) μ := + locallyIntegrableOn_univ.1 ((hf.locallyIntegrableOn univ).continuousOn_mul + hg.continuousOn isOpen_univ.isLocallyClosed) + +theorem mul_continuous {f g : X → R} (hg : Continuous g) + (hf : LocallyIntegrable f μ) : LocallyIntegrable (fun x => f x * g x) μ := + locallyIntegrableOn_univ.1 ((hf.locallyIntegrableOn univ).mul_continuousOn + hg.continuousOn isOpen_univ.isLocallyClosed) + +theorem continuous_smul [SecondCountableTopologyEither X 𝕜] {f : X → E} {g : X → 𝕜} + (hg : Continuous g) (hf : LocallyIntegrable f μ) : LocallyIntegrable (fun x => g x • f x) μ := + locallyIntegrableOn_univ.1 ((hf.locallyIntegrableOn univ).continuousOn_smul + isOpen_univ.isLocallyClosed hg.continuousOn) + +theorem smul_continuous [SecondCountableTopologyEither X E] {f : X → 𝕜} {g : X → E} + (hg : Continuous g) (hf : LocallyIntegrable f μ) : LocallyIntegrable (fun x => f x • g x) μ := + locallyIntegrableOn_univ.1 ((hf.locallyIntegrableOn univ).smul_continuousOn + isOpen_univ.isLocallyClosed hg.continuousOn) + +end LocallyIntegrable + end MeasureTheory diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean index 2bd25eb785e..e668c596342 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean +++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean @@ -947,7 +947,9 @@ theorem exists_set_sigmaFinite (hf : AEFinStronglyMeasurable f μ) : exact Eventually.of_forall hgt_zero /-- A measurable set `t` such that `f =ᵐ[μ.restrict tᶜ] 0` and `sigma_finite (μ.restrict t)`. -/ -def sigmaFiniteSet (hf : AEFinStronglyMeasurable f μ) : Set α := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def sigmaFiniteSet (hf : AEFinStronglyMeasurable f μ) : Set α := hf.exists_set_sigmaFinite.choose protected theorem measurableSet (hf : AEFinStronglyMeasurable f μ) : diff --git a/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean b/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean index 3e8032d0ffd..7782e46859e 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean @@ -57,6 +57,9 @@ class CountablyGenerated (α : Type*) [m : MeasurableSpace α] : Prop where /-- A countable set of sets that generate the measurable space. We insert `∅` to ensure it is nonempty. -/ +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def countableGeneratingSet (α : Type*) [MeasurableSpace α] [h : CountablyGenerated α] : Set (Set α) := insert ∅ h.isCountablyGenerated.choose @@ -83,6 +86,9 @@ lemma measurableSet_countableGeneratingSet [MeasurableSpace α] [CountablyGenera exact measurableSet_generateFrom hs /-- A countable sequence of sets generating the measurable space. -/ +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def natGeneratingSequence (α : Type*) [MeasurableSpace α] [CountablyGenerated α] : ℕ → (Set α) := enumerateCountable (countable_countableGeneratingSet (α := α)) ∅ @@ -143,6 +149,9 @@ open scoped Classical in Some of those sets may be empty, but the nonempty ones are the atoms of the measurable space. See `measurableAtom_eq_countablyGeneratedAtom_natGeneratingSequence`. -/ +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def countablyGeneratedAtom (α : Type*) [MeasurableSpace α] [CountablyGenerated α] : (ℕ → Prop) → Set α := fun p ↦ ⋂ n, if p n then natGeneratingSequence α n else (natGeneratingSequence α n)ᶜ @@ -570,7 +579,10 @@ variable [m : MeasurableSpace α] [h : CountablyGenerated α] /-- For each `n : ℕ`, `countablePartition α n` is a partition of the space in at most `2^n` sets. Each partition is finer than the preceding one. The measurable space generated by the union of all those partitions is the measurable space on `α`. -/ -def countablePartition (α : Type*) [MeasurableSpace α] [CountablyGenerated α] : ℕ → Set (Set α) := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def countablePartition (α : Type*) [MeasurableSpace α] [CountablyGenerated α] : + ℕ → Set (Set α) := memPartition (enumerateCountable countable_countableGeneratingSet ∅) lemma measurableSet_enumerateCountable_countableGeneratingSet @@ -626,7 +638,9 @@ lemma measurableSet_countablePartition (n : ℕ) {s : Set α} (hs : s ∈ counta generateFrom_countablePartition_le α n _ (measurableSet_generateFrom hs) /-- The set in `countablePartition α n` to which `a : α` belongs. -/ -def countablePartitionSet (n : ℕ) (a : α) : Set α := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def countablePartitionSet (n : ℕ) (a : α) : Set α := memPartitionSet (enumerateCountable countable_countableGeneratingSet ∅) n a lemma countablePartitionSet_mem (n : ℕ) (a : α) : diff --git a/Mathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean b/Mathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean index 0bc097a039a..61fe8b8a048 100644 --- a/Mathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean +++ b/Mathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean @@ -62,7 +62,9 @@ variable {α : Type*} {mα : MeasurableSpace α} {μ ν : Measure α} {s t : Set open scoped Classical in /-- A measurable set such that `μ.restrict (μ.sigmaFiniteSetWRT ν)` is sigma-finite and for all measurable sets `t ⊆ sᶜ`, either `ν t = 0` or `μ t = ∞`. -/ -def Measure.sigmaFiniteSetWRT (μ ν : Measure α) : Set α := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def Measure.sigmaFiniteSetWRT (μ ν : Measure α) : Set α := if h : ∃ s : Set α, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ (∀ t, t ⊆ sᶜ → ν t ≠ 0 → μ t = ∞) then h.choose @@ -123,7 +125,9 @@ lemma exists_isSigmaFiniteSet_measure_ge (μ ν : Measure α) [IsFiniteMeasure /-- A measurable set such that `μ.restrict (μ.sigmaFiniteSetGE ν n)` is sigma-finite and for `C` the supremum of `ν s` over all measurable sets `s` with `μ.restrict s` sigma-finite, `ν (μ.sigmaFiniteSetGE ν n) ≥ C - 1/n`. -/ -def Measure.sigmaFiniteSetGE (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) : Set α := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def Measure.sigmaFiniteSetGE (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) : Set α := (exists_isSigmaFiniteSet_measure_ge μ ν n).choose lemma measurableSet_sigmaFiniteSetGE [IsFiniteMeasure ν] (n : ℕ) : @@ -159,7 +163,9 @@ lemma tendsto_measure_sigmaFiniteSetGE (μ ν : Measure α) [IsFiniteMeasure ν] /-- A measurable set such that `μ.restrict (μ.sigmaFiniteSetWRT' ν)` is sigma-finite and `ν (μ.sigmaFiniteSetWRT' ν)` has maximal measure among such sets. -/ -def Measure.sigmaFiniteSetWRT' (μ ν : Measure α) [IsFiniteMeasure ν] : Set α := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def Measure.sigmaFiniteSetWRT' (μ ν : Measure α) [IsFiniteMeasure ν] : Set α := ⋃ n, μ.sigmaFiniteSetGE ν n lemma measurableSet_sigmaFiniteSetWRT' [IsFiniteMeasure ν] : @@ -304,7 +310,9 @@ section SigmaFiniteSet /-- A measurable set such that `μ.restrict μ.sigmaFiniteSet` is sigma-finite, and for all measurable sets `s ⊆ μ.sigmaFiniteSetᶜ`, either `μ s = 0` or `μ s = ∞`. -/ -def Measure.sigmaFiniteSet (μ : Measure α) : Set α := μ.sigmaFiniteSetWRT μ +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def Measure.sigmaFiniteSet (μ : Measure α) : Set α := μ.sigmaFiniteSetWRT μ @[measurability] lemma measurableSet_sigmaFiniteSet : MeasurableSet μ.sigmaFiniteSet := diff --git a/Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean b/Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean index 090e050b682..ebed3321528 100644 --- a/Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean @@ -833,7 +833,9 @@ theorem iSup_le_le {α : Type*} (f : ℕ → α → ℝ≥0∞) (n k : ℕ) (hk end SuprLemmas /-- `measurableLEEval μ ν` is the set of `∫⁻ x, f x ∂μ` for all `f ∈ measurableLE μ ν`. -/ -def measurableLEEval (μ ν : Measure α) : Set ℝ≥0∞ := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def measurableLEEval (μ ν : Measure α) : Set ℝ≥0∞ := (fun f : α → ℝ≥0∞ ↦ ∫⁻ x, f x ∂μ) '' measurableLE μ ν end LebesgueDecomposition diff --git a/Mathlib/MeasureTheory/Measure/MutuallySingular.lean b/Mathlib/MeasureTheory/Measure/MutuallySingular.lean index 30274996194..e5ce715eee3 100644 --- a/Mathlib/MeasureTheory/Measure/MutuallySingular.lean +++ b/Mathlib/MeasureTheory/Measure/MutuallySingular.lean @@ -53,7 +53,9 @@ theorem mk {s t : Set α} (hs : μ s = 0) (ht : ν t = 0) (hst : univ ⊆ s ∪ exact subset_toMeasurable _ _ hxs /-- A set such that `μ h.nullSet = 0` and `ν h.nullSetᶜ = 0`. -/ -def nullSet (h : μ ⟂ₘ ν) : Set α := h.choose +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def nullSet (h : μ ⟂ₘ ν) : Set α := h.choose lemma measurableSet_nullSet (h : μ ⟂ₘ ν) : MeasurableSet h.nullSet := h.choose_spec.1 diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean b/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean index ff9b25f67c9..86e8176e35b 100644 --- a/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean +++ b/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean @@ -563,7 +563,10 @@ theorem isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace [Topologic /-- Compact covering of a `σ`-compact topological space as `MeasureTheory.Measure.FiniteSpanningSetsIn`. -/ -def MeasureTheory.Measure.finiteSpanningSetsInCompact [TopologicalSpace α] [SigmaCompactSpace α] +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def MeasureTheory.Measure.finiteSpanningSetsInCompact + [TopologicalSpace α] [SigmaCompactSpace α] {_ : MeasurableSpace α} (μ : Measure α) [IsLocallyFiniteMeasure μ] : μ.FiniteSpanningSetsIn { K | IsCompact K } where set := compactCovering α @@ -573,7 +576,10 @@ def MeasureTheory.Measure.finiteSpanningSetsInCompact [TopologicalSpace α] [Sig /-- A locally finite measure on a `σ`-compact topological space admits a finite spanning sequence of open sets. -/ -def MeasureTheory.Measure.finiteSpanningSetsInOpen [TopologicalSpace α] [SigmaCompactSpace α] +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def MeasureTheory.Measure.finiteSpanningSetsInOpen + [TopologicalSpace α] [SigmaCompactSpace α] {_ : MeasurableSpace α} (μ : Measure α) [IsLocallyFiniteMeasure μ] : μ.FiniteSpanningSetsIn { K | IsOpen K } where set n := ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean b/Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean index 695dba97b89..e1cc8af8cd1 100644 --- a/Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean +++ b/Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean @@ -104,7 +104,9 @@ theorem SigmaFinite.out (h : SigmaFinite μ) : Nonempty (μ.FiniteSpanningSetsIn h.1 /-- If `μ` is σ-finite it has finite spanning sets in the collection of all measurable sets. -/ -def Measure.toFiniteSpanningSetsIn (μ : Measure α) [h : SigmaFinite μ] : +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def Measure.toFiniteSpanningSetsIn (μ : Measure α) [h : SigmaFinite μ] : μ.FiniteSpanningSetsIn { s | MeasurableSet s } where set n := toMeasurable μ (h.out.some.set n) set_mem _ := measurableSet_toMeasurable _ _ @@ -116,7 +118,9 @@ def Measure.toFiniteSpanningSetsIn (μ : Measure α) [h : SigmaFinite μ] : /-- A noncomputable way to get a monotone collection of sets that span `univ` and have finite measure using `Classical.choose`. This definition satisfies monotonicity in addition to all other properties in `SigmaFinite`. -/ -def spanningSets (μ : Measure α) [SigmaFinite μ] (i : ℕ) : Set α := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def spanningSets (μ : Measure α) [SigmaFinite μ] (i : ℕ) : Set α := accumulate μ.toFiniteSpanningSetsIn.set i theorem monotone_spanningSets (μ : Measure α) [SigmaFinite μ] : Monotone (spanningSets μ) := diff --git a/Mathlib/ModelTheory/Algebra/Field/CharP.lean b/Mathlib/ModelTheory/Algebra/Field/CharP.lean index aa00bd890bd..e022f7bf5ea 100644 --- a/Mathlib/ModelTheory/Algebra/Field/CharP.lean +++ b/Mathlib/ModelTheory/Algebra/Field/CharP.lean @@ -41,7 +41,9 @@ noncomputable def eqZero (n : ℕ) : Language.ring.Sentence := simp [eqZero] /-- The first-order theory of fields of characteristic `p` as a theory over the language of rings -/ -def _root_.FirstOrder.Language.Theory.fieldOfChar (p : ℕ) : Language.ring.Theory := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def _root_.FirstOrder.Language.Theory.fieldOfChar (p : ℕ) : Language.ring.Theory := Theory.field ∪ if p = 0 then (fun q => ∼(eqZero q)) '' {q : ℕ | q.Prime} diff --git a/Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean b/Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean index 338de145fc0..c8b764647d3 100644 --- a/Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean +++ b/Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean @@ -80,7 +80,9 @@ theorem realize_genericMonicPolyHasRoot [Field K] [CompatibleRing K] (n : ℕ) : /-- The theory of algebraically closed fields of characteristic `p` as a theory over the language of rings -/ -def _root_.FirstOrder.Language.Theory.ACF (p : ℕ) : Theory .ring := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def _root_.FirstOrder.Language.Theory.ACF (p : ℕ) : Theory .ring := Theory.fieldOfChar p ∪ genericMonicPolyHasRoot '' {n | 0 < n} instance [Language.ring.Structure K] (p : ℕ) [h : (Theory.ACF p).Model K] : diff --git a/Mathlib/NumberTheory/LSeries/Dirichlet.lean b/Mathlib/NumberTheory/LSeries/Dirichlet.lean index 07345140093..f718ca1edc3 100644 --- a/Mathlib/NumberTheory/LSeries/Dirichlet.lean +++ b/Mathlib/NumberTheory/LSeries/Dirichlet.lean @@ -429,7 +429,7 @@ of the L-series of the constant sequence `1` on its domain of convergence `re s lemma LSeries_vonMangoldt_eq {s : ℂ} (hs : 1 < s.re) : L ↗Λ s = - deriv (L 1) s / L 1 s := by refine (LSeries_congr (fun {n} _ ↦ ?_) s).trans <| LSeries_modOne_eq ▸ LSeries_twist_vonMangoldt_eq χ₁ hs - simp [Subsingleton.eq_one (n : ZMod 1)] + simp [Subsingleton.eq_one (α := ZMod 1)] /-- The L-series of the von Mangoldt function `Λ` equals the negative logarithmic derivative of the Riemann zeta function on its domain of convergence `re s > 1`. -/ diff --git a/Mathlib/NumberTheory/LSeries/ZetaZeros.lean b/Mathlib/NumberTheory/LSeries/ZetaZeros.lean index 3de3859e78e..0b8046e67ae 100644 --- a/Mathlib/NumberTheory/LSeries/ZetaZeros.lean +++ b/Mathlib/NumberTheory/LSeries/ZetaZeros.lean @@ -30,7 +30,9 @@ so that in particular any compact subset of `ℂ` contains only finitely many ze @[expose] public section /-- The zeros of Riemann's ζ-function. -/ -def riemannZetaZeros : Set ℂ := riemannZeta ⁻¹' {0} +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def riemannZetaZeros : Set ℂ := riemannZeta ⁻¹' {0} lemma mem_riemannZetaZeros {z : ℂ} : z ∈ riemannZetaZeros ↔ riemannZeta z = 0 := .rfl diff --git a/Mathlib/NumberTheory/LucasLehmer.lean b/Mathlib/NumberTheory/LucasLehmer.lean index 314677e515d..d3a82a41a70 100644 --- a/Mathlib/NumberTheory/LucasLehmer.lean +++ b/Mathlib/NumberTheory/LucasLehmer.lean @@ -514,13 +514,10 @@ theorem ω_pow_formula (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) : have : 1 ≤ 2 ^ (p' + 2) := Nat.one_le_pow _ _ (by decide) exact mod_cast h --- TODO: fix non-terminal simp (acting on two goals with different simp sets) -set_option linter.flexible false in set_option backward.isDefEq.respectTransparency false in /-- `q` is the minimum factor of `mersenne p`, so `M p = 0` in `X q`. -/ theorem mersenne_coe_X (p : ℕ) : (mersenne p : X (q p)) = 0 := by - ext <;> simp [mersenne, q, ZMod.natCast_eq_zero_iff, -pow_pos] - apply Nat.minFac_dvd + ext <;> simp [mersenne, q, ZMod.natCast_eq_zero_iff, Nat.minFac_dvd, -pow_pos] theorem ω_pow_eq_neg_one (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) : (ω : X (q (p' + 2))) ^ 2 ^ (p' + 1) = -1 := by diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean index 510b6f87e8f..e20fca7a52a 100644 --- a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean +++ b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean @@ -58,10 +58,10 @@ lemma gammaSet_one_const (a a' : Fin 2 → ZMod 1) : gammaSet 1 r a = gammaSet 1 /-- For level `N = 1`, the gamma sets simplify to only a `gcd` condition. -/ lemma gammaSet_one_eq (a : Fin 2 → ZMod 1) : gammaSet 1 r a = {v : Fin 2 → ℤ | (v 0).gcd (v 1) = r} := by - simp [gammaSet, Subsingleton.eq_zero] + simp [gammaSet, Subsingleton.eq_zero (α := Fin 2 → ZMod 1)] lemma gammaSet_one_mem_iff (v : Fin 2 → ℤ) : v ∈ gammaSet 1 r 0 ↔ (v 0).gcd (v 1) = r := by - simp [gammaSet, Subsingleton.eq_zero] + simp [gammaSet, Subsingleton.eq_zero (α := Fin 2 → ZMod 1)] /-- For level `N = 1`, the gamma sets are all equivalent; this is the equivalence. -/ def gammaSet_one_equiv (a a' : Fin 2 → ZMod 1) : gammaSet 1 r a ≃ gammaSet 1 r a' := diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean index 558dabc828b..9dfad8b98b3 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean @@ -55,7 +55,9 @@ variable (f : InfinitePlace K → ℝ≥0) /-- The convex body defined by `f`: the set of points `x : E` such that `‖x w‖ < f w` for all infinite places `w`. -/ -abbrev convexBodyLT : Set (mixedSpace K) := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable abbrev convexBodyLT : Set (mixedSpace K) := (Set.univ.pi (fun w : { w : InfinitePlace K // IsReal w } => ball 0 (f w))) ×ˢ (Set.univ.pi (fun w : { w : InfinitePlace K // IsComplex w } => ball 0 (f w))) @@ -145,7 +147,9 @@ open scoped Classical in needed to ensure the element constructed is not real, see for example `exists_primitive_element_lt_of_isComplex`. -/ -abbrev convexBodyLT' : Set (mixedSpace K) := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable abbrev convexBodyLT' : Set (mixedSpace K) := (Set.univ.pi (fun w : { w : InfinitePlace K // IsReal w } ↦ ball 0 (f w))) ×ˢ (Set.univ.pi (fun w : { w : InfinitePlace K // IsComplex w } ↦ if w = w₀ then {x | |x.re| < 1 ∧ |x.im| < (f w : ℝ) ^ 2} else ball 0 (f w))) diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean index 6527683f9be..3d71faf8b0a 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean @@ -161,7 +161,10 @@ variable [NumberField K] /-- The set of elements of the `fundamentalCone` of `norm ≤ 1`. -/ -abbrev normLeOne : Set (mixedSpace K) := fundamentalCone K ∩ {x | mixedEmbedding.norm x ≤ 1} +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable abbrev normLeOne : Set (mixedSpace K) := + fundamentalCone K ∩ {x | mixedEmbedding.norm x ≤ 1} variable {K} in theorem mem_normLeOne {x : mixedSpace K} : @@ -633,7 +636,9 @@ open scoped Classical in The set that parametrizes `normAtAllPlaces '' (normLeOne K)`, see `normAtAllPlaces_normLeOne_eq_image`. -/ -abbrev paramSet : Set (realSpace K) := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable abbrev paramSet : Set (realSpace K) := Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Ico 0 1 theorem measurableSet_paramSet : @@ -720,7 +725,9 @@ open scoped Classical in A compact set that contains `expMapBasis '' closure (paramSet K)` and furthermore is almost equal to it, see `compactSet_ae`. -/ -abbrev compactSet : Set (realSpace K) := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable abbrev compactSet : Set (realSpace K) := (Set.Icc (0 : ℝ) 1) • (expMapBasis '' Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1) theorem isCompact_compactSet : diff --git a/Mathlib/NumberTheory/PythagoreanTriples.lean b/Mathlib/NumberTheory/PythagoreanTriples.lean index 4a3ccc22d77..917922ab622 100644 --- a/Mathlib/NumberTheory/PythagoreanTriples.lean +++ b/Mathlib/NumberTheory/PythagoreanTriples.lean @@ -237,8 +237,6 @@ For the classification of Pythagorean triples, we will use a parametrization of variable {K : Type*} [Field K] --- Non-terminal simp, used to be field_simp -set_option linter.flexible false in -- see https://github.com/leanprover-community/mathlib4/issues/29041 set_option linter.unusedSimpArgs false in /-- A parameterization of the unit circle that is useful for classifying Pythagorean triples. @@ -269,9 +267,7 @@ def circleEquivGen (hk : ∀ x : K, 1 + x ^ 2 ≠ 0) : simp only [Prod.mk_inj, Subtype.mk_eq_mk] constructor · simp [field, h3] - · simp [field, h3] - rw [← add_neg_eq_iff_eq_add.mpr hxy.symm] - ring + · grind @[simp] theorem circleEquivGen_apply (hk : ∀ x : K, 1 + x ^ 2 ≠ 0) (x : K) : diff --git a/Mathlib/Order/BooleanGenerators.lean b/Mathlib/Order/BooleanGenerators.lean index e152409d611..ef9f5b27447 100644 --- a/Mathlib/Order/BooleanGenerators.lean +++ b/Mathlib/Order/BooleanGenerators.lean @@ -25,9 +25,9 @@ A set of *Boolean generators* in a compactly generated complete lattice is a sub the predicate described above. * `IsCompactlyGenerated.BooleanGenerators.complementedLattice_of_sSup_eq_top`: if `S` generates the entire lattice, then it is complemented. -* `IsCompactlyGenerated.BooleanGenerators.distribLattice_of_sSup_eq_top`: +* `IsCompactlyGenerated.BooleanGenerators.distribLatticeOfSSupEqTop`: if `S` generates the entire lattice, then it is distributive. -* `IsCompactlyGenerated.BooleanGenerators.booleanAlgebra_of_sSup_eq_top`: +* `IsCompactlyGenerated.BooleanGenerators.booleanAlgebraOfSSupEqTop`: if `S` generates the entire lattice, then it is a Boolean algebra. -/ @@ -52,7 +52,7 @@ A set of *Boolean generators* in a compactly generated complete lattice is a sub If the supremum of `S` is the whole lattice, then the lattice is a Boolean algebra -(see `IsCompactlyGenerated.BooleanGenerators.booleanAlgebra_of_sSup_eq_top`). +(see `IsCompactlyGenerated.BooleanGenerators.booleanAlgebraOfSSupEqTop`). -/ structure BooleanGenerators (S : Set α) : Prop where /-- The elements in a collection of Boolean generators are all atoms. -/ @@ -140,7 +140,7 @@ lemma sSup_inter (hS : BooleanGenerators S) {T₁ T₂ : Set α} (hT₁ : T₁ /-- A lattice generated by Boolean generators is a distributive lattice. -/ @[instance_reducible] -def distribLattice_of_sSup_eq_top (hS : BooleanGenerators S) (h : sSup S = ⊤) : +def distribLatticeOfSSupEqTop (hS : BooleanGenerators S) (h : sSup S = ⊤) : DistribLattice α where le_sup_inf a b c := by obtain ⟨Ta, hTa, rfl⟩ := hS.atomistic a (h ▸ le_top) @@ -153,20 +153,26 @@ def distribLattice_of_sSup_eq_top (hS : BooleanGenerators S) (h : sSup S = ⊤) simp only [Set.union_subset_iff, Set.mem_inter_iff, Set.mem_union] tauto +@[deprecated (since := "2026-07-18")] +alias distribLattice_of_sSup_eq_top := distribLatticeOfSSupEqTop + lemma complementedLattice_of_sSup_eq_top (hS : BooleanGenerators S) (h : sSup S = ⊤) : ComplementedLattice α := by - let _i := hS.distribLattice_of_sSup_eq_top h + let _i := hS.distribLatticeOfSSupEqTop h have _i₁ := isAtomistic_of_sSup_eq_top hS h apply complementedLattice_of_isAtomistic /-- A compactly generated complete lattice generated by Boolean generators is a Boolean algebra. -/ @[instance_reducible] noncomputable -def booleanAlgebra_of_sSup_eq_top (hS : BooleanGenerators S) (h : sSup S = ⊤) : BooleanAlgebra α := - let _i := hS.distribLattice_of_sSup_eq_top h +def booleanAlgebraOfSSupEqTop (hS : BooleanGenerators S) (h : sSup S = ⊤) : BooleanAlgebra α := + let _i := hS.distribLatticeOfSSupEqTop h have := hS.complementedLattice_of_sSup_eq_top h DistribLattice.booleanAlgebraOfComplemented α +@[deprecated (since := "2026-07-18")] +alias booleanAlgebra_of_sSup_eq_top := booleanAlgebraOfSSupEqTop + lemma sSup_le_sSup_iff_of_atoms (hS : BooleanGenerators S) (X Y : Set α) (hX : X ⊆ S) (hY : Y ⊆ S) : sSup X ≤ sSup Y ↔ X ⊆ Y := by refine ⟨?_, sSup_le_sSup⟩ diff --git a/Mathlib/Order/Category/NonemptyFinLinOrd.lean b/Mathlib/Order/Category/NonemptyFinLinOrd.lean index 06094177458..b17955e0d9b 100644 --- a/Mathlib/Order/Category/NonemptyFinLinOrd.lean +++ b/Mathlib/Order/Category/NonemptyFinLinOrd.lean @@ -228,4 +228,7 @@ def nonemptyFinLinOrdDualCompForgetToFinPartOrd : inv.app X := FinPartOrd.ofHom OrderHom.id /-- The generating arrow `i ⟶ i+1` in the category `Fin n` -/ -def Fin.hom_succ {n} (i : Fin n) : i.castSucc ⟶ i.succ := homOfLE (Fin.castSucc_le_succ i) +def Fin.homSucc {n} (i : Fin n) : i.castSucc ⟶ i.succ := homOfLE (Fin.castSucc_le_succ i) + +@[deprecated (since := "2026-07-18")] +alias Fin.hom_succ := Fin.homSucc diff --git a/Mathlib/Order/Filter/Ker.lean b/Mathlib/Order/Filter/Ker.lean index 9e397bb1f6d..eee196ab879 100644 --- a/Mathlib/Order/Filter/Ker.lean +++ b/Mathlib/Order/Filter/Ker.lean @@ -31,22 +31,25 @@ lemma ker_def (f : Filter α) : f.ker = ⋂ s ∈ f, s := sInter_eq_biInter @[simp] lemma subset_ker : s ⊆ f.ker ↔ ∀ t ∈ f, s ⊆ t := subset_sInter_iff /-- `Filter.principal` forms a Galois coinsertion with `Filter.ker`. -/ -def gi_principal_ker : GaloisCoinsertion (𝓟 : Set α → Filter α) ker := +def giPrincipalKer : GaloisCoinsertion (𝓟 : Set α → Filter α) ker := GaloisConnection.toGaloisCoinsertion (fun s f ↦ by simp [principal_le_iff]) <| by simp only [subset_def, mem_ker, mem_principal]; aesop -lemma ker_mono : Monotone (ker : Filter α → Set α) := gi_principal_ker.gc.monotone_u -lemma ker_surjective : Surjective (ker : Filter α → Set α) := gi_principal_ker.u_surjective +@[deprecated (since := "2026-07-18")] +alias gi_principal_ker := giPrincipalKer + +lemma ker_mono : Monotone (ker : Filter α → Set α) := giPrincipalKer.gc.monotone_u +lemma ker_surjective : Surjective (ker : Filter α → Set α) := giPrincipalKer.u_surjective @[simp] lemma ker_bot : ker (⊥ : Filter α) = ∅ := sInter_eq_empty_iff.2 fun _ ↦ ⟨∅, trivial, id⟩ -@[simp] lemma ker_top : ker (⊤ : Filter α) = univ := gi_principal_ker.gc.u_top -@[simp] lemma ker_eq_univ : ker f = univ ↔ f = ⊤ := gi_principal_ker.gc.u_eq_top.trans <| by simp -@[simp] lemma ker_inf (f g : Filter α) : ker (f ⊓ g) = ker f ∩ ker g := gi_principal_ker.gc.u_inf +@[simp] lemma ker_top : ker (⊤ : Filter α) = univ := giPrincipalKer.gc.u_top +@[simp] lemma ker_eq_univ : ker f = univ ↔ f = ⊤ := giPrincipalKer.gc.u_eq_top.trans <| by simp +@[simp] lemma ker_inf (f g : Filter α) : ker (f ⊓ g) = ker f ∩ ker g := giPrincipalKer.gc.u_inf @[simp] lemma ker_iInf (f : ι → Filter α) : ker (⨅ i, f i) = ⋂ i, ker (f i) := - gi_principal_ker.gc.u_iInf + giPrincipalKer.gc.u_iInf @[simp] lemma ker_sInf (S : Set (Filter α)) : ker (sInf S) = ⋂ f ∈ S, ker f := - gi_principal_ker.gc.u_sInf -@[simp] lemma ker_principal (s : Set α) : ker (𝓟 s) = s := gi_principal_ker.u_l_eq _ + giPrincipalKer.gc.u_sInf +@[simp] lemma ker_principal (s : Set α) : ker (𝓟 s) = s := giPrincipalKer.u_l_eq _ @[simp] lemma ker_pure (a : α) : ker (pure a) = {a} := by rw [← principal_singleton, ker_principal] diff --git a/Mathlib/Order/GaloisConnection/Basic.lean b/Mathlib/Order/GaloisConnection/Basic.lean index a626179797d..b9c0ea6b1e3 100644 --- a/Mathlib/Order/GaloisConnection/Basic.lean +++ b/Mathlib/Order/GaloisConnection/Basic.lean @@ -418,15 +418,21 @@ theorem gc_Ici_sInf [CompleteSemilatticeInf α] : fun _ _ ↦ le_sInf_iff.symm /-- `sSup` and `Iic` form a Galois insertion. -/ -def gi_sSup_Iic [CompleteSemilatticeSup α] : +def giSSupIic [CompleteSemilatticeSup α] : GaloisInsertion (sSup : Set α → α) (Iic : α → Set α) := gc_sSup_Iic.toGaloisInsertion fun _ ↦ le_sSup le_rfl +@[deprecated (since := "2026-07-18")] +alias gi_sSup_Iic := giSSupIic + /-- `toDual ∘ Ici` and `sInf ∘ ofDual` form a Galois coinsertion. -/ -def gci_Ici_sInf [CompleteSemilatticeInf α] : +def gciIciSInf [CompleteSemilatticeInf α] : GaloisCoinsertion (toDual ∘ Ici : α → (Set α)ᵒᵈ) (sInf ∘ ofDual : (Set α)ᵒᵈ → α) := gc_Ici_sInf.toGaloisCoinsertion fun _ ↦ sInf_le le_rfl +@[deprecated (since := "2026-07-18")] +alias gci_Ici_sInf := gciIciSInf + /-- If `α` is a partial order with bottom element (e.g., `ℕ`, `ℝ≥0`), then `WithBot.unbot' ⊥` and coercion form a Galois insertion. -/ @[to_dual giUntopDTop diff --git a/Mathlib/Order/Interval/Set/OrdConnectedComponent.lean b/Mathlib/Order/Interval/Set/OrdConnectedComponent.lean index 04840e3ddd3..cbb153278c6 100644 --- a/Mathlib/Order/Interval/Set/OrdConnectedComponent.lean +++ b/Mathlib/Order/Interval/Set/OrdConnectedComponent.lean @@ -116,7 +116,9 @@ theorem ordConnectedProj_eq {x y : s} : /-- A set that intersects each order connected component of a set by a single point. Defined as the range of `Set.ordConnectedProj s`. -/ -def ordConnectedSection (s : Set α) : Set α := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def ordConnectedSection (s : Set α) : Set α := range <| ordConnectedProj s theorem dual_ordConnectedSection (s : Set α) : @@ -165,7 +167,9 @@ theorem dual_ordSeparatingSet : /-- An auxiliary neighborhood that will be used in the proof of `OrderTopology.CompletelyNormalSpace`. -/ -def ordT5Nhd (s t : Set α) : Set α := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def ordT5Nhd (s t : Set α) : Set α := ⋃ x ∈ s, ordConnectedComponent (tᶜ ∩ (ordConnectedSection <| ordSeparatingSet s t)ᶜ) x theorem disjoint_ordT5Nhd : Disjoint (ordT5Nhd s t) (ordT5Nhd t s) := by diff --git a/Mathlib/Order/LiminfLimsup.lean b/Mathlib/Order/LiminfLimsup.lean index 4b9e2442ba5..0294720f9ca 100644 --- a/Mathlib/Order/LiminfLimsup.lean +++ b/Mathlib/Order/LiminfLimsup.lean @@ -974,12 +974,12 @@ section Classical open scoped Classical in /-- Given an indexed family of sets `s j` over `j : Subtype p` and a function `f`, then -`liminf_reparam j` is equal to `j` if `f` is bounded below on `s j`, and otherwise to some +`liminfReparam j` is equal to `j` if `f` is bounded below on `s j`, and otherwise to some index `k` such that `f` is bounded below on `s k` (if there exists one). To ensure good measurability behavior, this index `k` is chosen as the minimal suitable index. This function is used to write down a liminf in a measurable way, in `Filter.HasBasis.liminf_eq_ciSup_ciInf` and `Filter.HasBasis.liminf_eq_ite`. -/ -noncomputable def liminf_reparam +noncomputable def liminfReparam (f : ι → α) (s : ι' → Set ι) (p : ι' → Prop) [Countable (Subtype p)] [Nonempty (Subtype p)] (j : Subtype p) : Subtype p := let m : Set (Subtype p) := {j | BddBelow (range (fun (i : s j) ↦ f i))} @@ -992,6 +992,9 @@ noncomputable def liminf_reparam · exact ⟨0, Or.inr H⟩ if j ∈ m then j else g (Nat.find Z) +@[deprecated (since := "2026-07-18")] +alias liminf_reparam := liminfReparam + /-- Writing a liminf as a supremum of infimum, in a (possibly non-complete) conditionally complete linear order. A reparametrization trick is needed to avoid taking the infimum of sets which are not bounded below. -/ @@ -999,31 +1002,31 @@ theorem HasBasis.liminf_eq_ciSup_ciInf {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) {f : ι → α} (hs : ∀ (j : Subtype p), (s j).Nonempty) (H : ∃ (j : Subtype p), BddBelow (range (fun (i : s j) ↦ f i))) : - liminf f v = ⨆ (j : Subtype p), ⨅ (i : s (liminf_reparam f s p j)), f i := by + liminf f v = ⨆ (j : Subtype p), ⨅ (i : s (liminfReparam f s p j)), f i := by classical rcases H with ⟨j0, hj0⟩ let m : Set (Subtype p) := {j | BddBelow (range (fun (i : s j) ↦ f i))} have : ∀ (j : Subtype p), Nonempty (s j) := fun j ↦ Nonempty.coe_sort (hs j) have A : ⋃ (j : Subtype p), ⋂ (i : s j), Iic (f i) = - ⋃ (j : Subtype p), ⋂ (i : s (liminf_reparam f s p j)), Iic (f i) := by + ⋃ (j : Subtype p), ⋂ (i : s (liminfReparam f s p j)), Iic (f i) := by apply Subset.antisymm · apply iUnion_subset (fun j ↦ ?_) by_cases hj : j ∈ m - · have : j = liminf_reparam f s p j := by simp only [m, liminf_reparam, hj, ite_true] + · have : j = liminfReparam f s p j := by simp only [m, liminfReparam, hj, ite_true] conv_lhs => rw [this] apply subset_iUnion _ j · simp only [m, mem_ofPred_eq, ← nonempty_iInter_Iic_iff, not_nonempty_iff_eq_empty] at hj simp only [hj, empty_subset] · apply iUnion_subset (fun j ↦ ?_) - exact subset_iUnion (fun (k : Subtype p) ↦ (⋂ (i : s k), Iic (f i))) (liminf_reparam f s p j) - have B : ∀ (j : Subtype p), ⋂ (i : s (liminf_reparam f s p j)), Iic (f i) = - Iic (⨅ (i : s (liminf_reparam f s p j)), f i) := by + exact subset_iUnion (fun (k : Subtype p) ↦ (⋂ (i : s k), Iic (f i))) (liminfReparam f s p j) + have B : ∀ (j : Subtype p), ⋂ (i : s (liminfReparam f s p j)), Iic (f i) = + Iic (⨅ (i : s (liminfReparam f s p j)), f i) := by intro j apply (Iic_ciInf _).symm - change liminf_reparam f s p j ∈ m + change liminfReparam f s p j ∈ m by_cases Hj : j ∈ m - · simpa only [m, liminf_reparam, if_pos Hj] using Hj - · simp only [m, liminf_reparam, if_neg Hj] + · simpa only [m, liminfReparam, if_pos Hj] using Hj + · simp only [m, liminfReparam, if_neg Hj] have Z : ∃ n, (exists_surjective_nat (Subtype p)).choose n ∈ m ∨ ∀ j, j ∉ m := by rcases (exists_surjective_nat (Subtype p)).choose_spec j0 with ⟨n, rfl⟩ exact ⟨n, Or.inl hj0⟩ @@ -1040,7 +1043,7 @@ theorem HasBasis.liminf_eq_ite {v : Filter ι} {p : ι' → Prop} {s : ι' → S [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) (f : ι → α) : liminf f v = if ∃ (j : Subtype p), s j = ∅ then sSup univ else if ∀ (j : Subtype p), ¬BddBelow (range (fun (i : s j) ↦ f i)) then sSup ∅ - else ⨆ (j : Subtype p), ⨅ (i : s (liminf_reparam f s p j)), f i := by + else ⨆ (j : Subtype p), ⨅ (i : s (liminfReparam f s p j)), f i := by by_cases H : ∃ (j : Subtype p), s j = ∅ · rw [if_pos H] rcases H with ⟨j, hj⟩ @@ -1058,15 +1061,18 @@ theorem HasBasis.liminf_eq_ite {v : Filter ι} {p : ι' → Prop} {s : ι' → S · push Not at H' exact H' -/-- Given an indexed family of sets `s j` and a function `f`, then `limsup_reparam j` is equal +/-- Given an indexed family of sets `s j` and a function `f`, then `limsupReparam j` is equal to `j` if `f` is bounded above on `s j`, and otherwise to some index `k` such that `f` is bounded above on `s k` (if there exists one). To ensure good measurability behavior, this index `k` is chosen as the minimal suitable index. This function is used to write down a limsup in a measurable way, in `Filter.HasBasis.limsup_eq_ciInf_ciSup` and `Filter.HasBasis.limsup_eq_ite`. -/ -noncomputable def limsup_reparam +noncomputable def limsupReparam (f : ι → α) (s : ι' → Set ι) (p : ι' → Prop) [Countable (Subtype p)] [Nonempty (Subtype p)] (j : Subtype p) : Subtype p := - liminf_reparam (α := αᵒᵈ) f s p j + liminfReparam (α := αᵒᵈ) f s p j + +@[deprecated (since := "2026-07-18")] +alias limsup_reparam := limsupReparam /-- Writing a limsup as an infimum of supremum, in a (possibly non-complete) conditionally complete linear order. A reparametrization trick is needed to avoid taking the supremum of sets which are @@ -1075,7 +1081,7 @@ theorem HasBasis.limsup_eq_ciInf_ciSup {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) {f : ι → α} (hs : ∀ (j : Subtype p), (s j).Nonempty) (H : ∃ (j : Subtype p), BddAbove (range (fun (i : s j) ↦ f i))) : - limsup f v = ⨅ (j : Subtype p), ⨆ (i : s (limsup_reparam f s p j)), f i := + limsup f v = ⨅ (j : Subtype p), ⨆ (i : s (limsupReparam f s p j)), f i := HasBasis.liminf_eq_ciSup_ciInf (α := αᵒᵈ) hv hs H open scoped Classical in @@ -1086,7 +1092,7 @@ theorem HasBasis.limsup_eq_ite {v : Filter ι} {p : ι' → Prop} {s : ι' → S [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) (f : ι → α) : limsup f v = if ∃ (j : Subtype p), s j = ∅ then sInf univ else if ∀ (j : Subtype p), ¬BddAbove (range (fun (i : s j) ↦ f i)) then sInf ∅ - else ⨅ (j : Subtype p), ⨆ (i : s (limsup_reparam f s p j)), f i := + else ⨅ (j : Subtype p), ⨆ (i : s (limsupReparam f s p j)), f i := HasBasis.liminf_eq_ite (α := αᵒᵈ) hv f end Classical diff --git a/Mathlib/Order/Partition/Basic.lean b/Mathlib/Order/Partition/Basic.lean index 06607e2b075..d69a518d279 100644 --- a/Mathlib/Order/Partition/Basic.lean +++ b/Mathlib/Order/Partition/Basic.lean @@ -156,15 +156,15 @@ def partscopyEquiv (P : Partition s) (hst : s = t) : ↥(P.copy hst) ≃ ↥P := /-- A constructor for `Partition s` that removes `⊥` from the set of parts. -/ @[simps] -def removeBot (P : Set α) (indep : _root_.sSupIndep P) (sSup_eq : sSup P = s) : Partition s where +def removeBot (P : Set α) (indep : _root_.sSupIndep P) (hsSup : sSup P = s) : Partition s where parts := P \ {⊥} sSupIndep' := indep.mono sdiff_subset bot_notMem' := by simp - sSup_eq' := by simp [← sSup_eq] + sSup_eq' := by simp [← hsSup] @[simp] -lemma mem_removeBot (P : Set α) (indep : _root_.sSupIndep P) (sSup_eq : sSup P = s) : - x ∈ removeBot P indep sSup_eq ↔ x ∈ P ∧ x ≠ ⊥ := Iff.rfl +lemma mem_removeBot (P : Set α) (indep : _root_.sSupIndep P) (hsSup : sSup P = s) : + x ∈ removeBot P indep hsSup ↔ x ∈ P ∧ x ≠ ⊥ := Iff.rfl @[simp] lemma notMem_of_bot (P : Partition (⊥ : α)) (x : α) : x ∉ P := by diff --git a/Mathlib/Order/Preorder/Chain.lean b/Mathlib/Order/Preorder/Chain.lean index 8536a31860e..0e11d220192 100644 --- a/Mathlib/Order/Preorder/Chain.lean +++ b/Mathlib/Order/Preorder/Chain.lean @@ -292,7 +292,9 @@ theorem IsMaxChain.symm (h : IsMaxChain r s) : IsMaxChain (flip r) s := open scoped Classical in /-- Given a set `s`, if there exists a chain `t` strictly including `s`, then `SuccChain s` is one of these chains. Otherwise it is `s`. -/ -def SuccChain (r : α → α → Prop) (s : Set α) : Set α := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def SuccChain (r : α → α → Prop) (s : Set α) : Set α := if h : ∃ t, IsChain r s ∧ SuperChain r s t then h.choose else s theorem succChain_spec (h : ∃ t, IsChain r s ∧ SuperChain r s t) : diff --git a/Mathlib/Probability/Process/PartitionFiltration.lean b/Mathlib/Probability/Process/PartitionFiltration.lean index 1f100fc7eda..8f5a5751795 100644 --- a/Mathlib/Probability/Process/PartitionFiltration.lean +++ b/Mathlib/Probability/Process/PartitionFiltration.lean @@ -105,7 +105,9 @@ variable {α : Type*} [MeasurableSpace α] [CountablyGenerated α] /-- A filtration built from the measurable spaces generated by `countablePartition α n` for all `n : ℕ`. -/ -def countableFiltration (α : Type*) [m : MeasurableSpace α] [CountablyGenerated α] : +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def countableFiltration (α : Type*) [m : MeasurableSpace α] [CountablyGenerated α] : Filtration ℕ m where seq n := generateFrom (countablePartition α n) mono' := monotone_nat_of_le_succ (generateFrom_countablePartition_le_succ _) diff --git a/Mathlib/RepresentationTheory/Rep/Res.lean b/Mathlib/RepresentationTheory/Rep/Res.lean index def1ed7cfe3..8bb98274728 100644 --- a/Mathlib/RepresentationTheory/Rep/Res.lean +++ b/Mathlib/RepresentationTheory/Rep/Res.lean @@ -55,7 +55,7 @@ lemma res_obj_V : (res f M).V = M.V := rfl lemma resMap_hom_toLinearMap {M N : Rep k G} (p : M ⟶ N) : (resMap f p).hom.toLinearMap = p.hom.toLinearMap := rfl -@[deprecated (since := "26/06/2026")] +@[deprecated (since := "2026-06-26")] alias res_map_hom_toLinearMap := resMap_hom_toLinearMap @[simp] diff --git a/Mathlib/RingTheory/Binomial.lean b/Mathlib/RingTheory/Binomial.lean index ede4089fd67..fea1415c451 100644 --- a/Mathlib/RingTheory/Binomial.lean +++ b/Mathlib/RingTheory/Binomial.lean @@ -8,9 +8,9 @@ module public import Mathlib.Algebra.Algebra.Rat public import Mathlib.Algebra.Group.Torsion public import Mathlib.Algebra.Module.Rat +public import Mathlib.Algebra.Order.Ring.NNRat public import Mathlib.Algebra.Polynomial.Smeval public import Mathlib.Algebra.Ring.NegOnePow -public import Mathlib.Data.NNRat.Order public import Mathlib.GroupTheory.GroupAction.Ring public import Mathlib.RingTheory.Polynomial.Pochhammer public import Mathlib.Tactic.Field diff --git a/Mathlib/RingTheory/Extension/Presentation/Core.lean b/Mathlib/RingTheory/Extension/Presentation/Core.lean index caedd445088..3e486502c77 100644 --- a/Mathlib/RingTheory/Extension/Presentation/Core.lean +++ b/Mathlib/RingTheory/Extension/Presentation/Core.lean @@ -34,7 +34,9 @@ namespace Algebra.Presentation variable (P) in /-- The coefficients of a presentation are the coefficients of the relations. -/ -def coeffs : Set R := ⋃ (i : σ), (P.relation i).coeffs +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def coeffs : Set R := ⋃ (i : σ), (P.relation i).coeffs lemma coeffs_relation_subset_coeffs (x : σ) : ((P.relation x).coeffs : Set R) ⊆ P.coeffs := @@ -45,7 +47,9 @@ lemma finite_coeffs [Finite σ] : P.coeffs.Finite := variable (P) in /-- The core of a presentation is the subalgebra generated by the coefficients of the relations. -/ -def core : Subalgebra ℤ R := Algebra.adjoin _ P.coeffs +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def core : Subalgebra ℤ R := Algebra.adjoin _ P.coeffs variable (P) in lemma coeffs_subset_core : P.coeffs ⊆ P.core := Algebra.subset_adjoin @@ -56,12 +60,20 @@ lemma coeffs_relation_subset_core (x : σ) : variable (P) in /-- The core coerced to a type for performance reasons. -/ -def Core : Type _ := P.core - -instance : CommRing P.Core := fast_instance% (inferInstanceAs <| CommRing P.core) -instance : Algebra P.Core R := fast_instance% (inferInstanceAs <| Algebra P.core R) +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def Core : Type _ := P.core + +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable instance : CommRing P.Core := fast_instance% (inferInstanceAs <| CommRing P.core) +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable instance : Algebra P.Core R := fast_instance% (inferInstanceAs <| Algebra P.core R) instance : FaithfulSMul P.Core R := inferInstanceAs <| FaithfulSMul P.core R -instance : Algebra P.Core S := fast_instance% (inferInstanceAs <| Algebra P.core S) +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable instance : Algebra P.Core S := fast_instance% (inferInstanceAs <| Algebra P.core S) instance : IsScalarTower P.Core R S := inferInstanceAs <| IsScalarTower P.core R S instance [Finite σ] : FiniteType ℤ P.Core := .adjoin_of_finite P.finite_coeffs @@ -257,7 +269,9 @@ lemma jacobianRelations_spec [DecidableEq σ] [Fintype σ] : convert! P.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one.choose_spec /-- The set of coefficients that is enough to descend a submersive presentation `P`. -/ -def coeffs : Set R := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def coeffs : Set R := P.toPresentation.coeffs ∪ (P.σ (P.jacobian_isUnit.unit⁻¹ :)).coeffs ∪ ⋃ i, (P.jacobianRelations i).coeffs diff --git a/Mathlib/RingTheory/FractionalIdeal/Extended.lean b/Mathlib/RingTheory/FractionalIdeal/Extended.lean index d158d68aa6f..cfd6b347812 100644 --- a/Mathlib/RingTheory/FractionalIdeal/Extended.lean +++ b/Mathlib/RingTheory/FractionalIdeal/Extended.lean @@ -37,7 +37,10 @@ This file defines the extension of a fractional ideal along a ring homomorphism. fractional ideal, fractional ideals, extended, extension -/ -@[expose] public section +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- This is why this section is `noncomputable`. +-- See https://github.com/leanprover/lean4/issues/14084. +@[expose] public noncomputable section open IsLocalization FractionalIdeal Module Submodule diff --git a/Mathlib/RingTheory/HahnSeries/PowerSeries.lean b/Mathlib/RingTheory/HahnSeries/PowerSeries.lean index a5bb85af445..edae469e7ab 100644 --- a/Mathlib/RingTheory/HahnSeries/PowerSeries.lean +++ b/Mathlib/RingTheory/HahnSeries/PowerSeries.lean @@ -142,7 +142,7 @@ theorem ofPowerSeries_X_pow {R} [Semiring R] (n : ℕ) : simp set_option backward.isDefEq.respectTransparency false in --- Lemmas about converting hahn_series over fintype to and from mv_power_series +-- Lemmas converting Hahn series over a finite index type to and from `MvPowerSeries` /-- The ring `R⟦σ →₀ ℕ⟧` is isomorphic to `MvPowerSeries σ R` for a `Finite` `σ`. We take the index set of the hahn series to be `Finsupp` rather than `pi`, even though we assume `Finite σ` as this is more natural for alignment with `MvPowerSeries`. diff --git a/Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean b/Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean index 37d55774eba..4621f8f399a 100644 --- a/Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean +++ b/Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean @@ -7,7 +7,6 @@ module public import Mathlib.Analysis.Normed.Ring.Basic public import Mathlib.RingTheory.MvPowerSeries.Basic - public import Mathlib.Algebra.Order.Ring.IsNonarchimedean /-! diff --git a/Mathlib/RingTheory/Nilpotent/Exp.lean b/Mathlib/RingTheory/Nilpotent/Exp.lean index 46934cfa2a1..9a42547fcb9 100644 --- a/Mathlib/RingTheory/Nilpotent/Exp.lean +++ b/Mathlib/RingTheory/Nilpotent/Exp.lean @@ -199,11 +199,11 @@ theorem exp_smul {G : Type*} [Monoid G] [MulSemiringAction G A] exp (g • a) = g • exp a := (map_exp ha (MulSemiringAction.toRingHom G A g)).symm -set_option linter.flexible false in -- TODO: fix non-terminal simp theorem isNilpotent_exp_sub_one {a : A} (ha : IsNilpotent a) : IsNilpotent (exp a - 1) := by nontriviality A rw [exp, ← Nat.sub_add_cancel (pos_nilpotencyClass_iff.2 ha), Finset.sum_range_succ'] - simp + simp only [Nat.succ_eq_add_one, zero_add, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, + one_smul, add_sub_cancel_right] apply Commute.isNilpotent_sum fun _ _ ↦ smul (pow_of_pos ha <| by positivity) _ simp [Nat.factorial_ne_zero] diff --git a/Mathlib/RingTheory/Polynomial/ContentIdeal.lean b/Mathlib/RingTheory/Polynomial/ContentIdeal.lean index 9758b54a8d9..4bc689bd797 100644 --- a/Mathlib/RingTheory/Polynomial/ContentIdeal.lean +++ b/Mathlib/RingTheory/Polynomial/ContentIdeal.lean @@ -48,7 +48,9 @@ open Ideal variable {R S : Type*} [Semiring R] [Semiring S] (p : R[X]) /-- The content ideal of a polynomial `p` is the ideal generated by its coefficients. -/ -def contentIdeal := span (p.coeffs : Set R) +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def contentIdeal := span (p.coeffs : Set R) theorem contentIdeal_def : p.contentIdeal = span (p.coeffs : Set R) := rfl diff --git a/Mathlib/RingTheory/Polynomial/IntegralNormalization.lean b/Mathlib/RingTheory/Polynomial/IntegralNormalization.lean index 16fa71e9d8e..5229e7c85a8 100644 --- a/Mathlib/RingTheory/Polynomial/IntegralNormalization.lean +++ b/Mathlib/RingTheory/Polynomial/IntegralNormalization.lean @@ -185,7 +185,7 @@ variable [Semiring R] [IsCancelMulZero R] @[simp] theorem support_integralNormalization {f : R[X]} : (integralNormalization f).support = f.support := by - nontriviality R using Subsingleton.eq_zero + nontriviality R using Subsingleton.eq_zero (α := R[X]) have : IsDomain R := {} by_cases hf : f = 0; · simp [hf] ext i diff --git a/Mathlib/RingTheory/Polynomial/ScaleRoots.lean b/Mathlib/RingTheory/Polynomial/ScaleRoots.lean index baba79d9b53..eda00901954 100644 --- a/Mathlib/RingTheory/Polynomial/ScaleRoots.lean +++ b/Mathlib/RingTheory/Polynomial/ScaleRoots.lean @@ -168,7 +168,7 @@ theorem scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero {p : S[X]} {f : S →+ (hf : Function.Injective f) {r s : S} (hr : eval₂ f (f r / f s) p = 0) (hs : s ∈ nonZeroDivisors S) : eval₂ f (f r) (scaleRoots p s) = 0 := by -- if we don't specify the type with `(_ : S)`, the proof is much slower - nontriviality S using Subsingleton.eq_zero (_ : S) + nontriviality S using Subsingleton.eq_zero (α := S) convert! @scaleRoots_eval₂_eq_zero _ _ _ _ p f _ s hr rw [← mul_div_assoc, mul_comm, mul_div_cancel_right₀] exact map_ne_zero_of_mem_nonZeroDivisors _ hf hs diff --git a/Mathlib/RingTheory/PowerSeries/Derivative.lean b/Mathlib/RingTheory/PowerSeries/Derivative.lean index c926fb57153..8ba5d9e0460 100644 --- a/Mathlib/RingTheory/PowerSeries/Derivative.lean +++ b/Mathlib/RingTheory/PowerSeries/Derivative.lean @@ -61,6 +61,23 @@ theorem coeff_derivative (f : R⟦X⟧) (n : ℕ) : coeff n (d⁄dX R f) = coeff (n + 1) f * (n + 1) := by simp [coeff, derivative, MvPowerSeries.coeff_pderiv] +/-- The `k`-th coefficient of the `n`-th formal derivative: differentiating `n` times multiplies the +`(k + n)`-th coefficient by the ascending factorial `(k + 1)(k + 2) ⋯ (k + n)`. -/ +theorem coeff_iterate_derivative (f : R⟦X⟧) (n k : ℕ) : + coeff k ((d⁄dX R)^[n] f) = (k + 1).ascFactorial n * coeff (k + n) f := by + induction n generalizing k with + | zero => simp + | succ n ih => + rw [Function.iterate_succ_apply', coeff_derivative, ih, Nat.ascFactorial_succ, + ← Nat.succ_ascFactorial] + grind + +/-- Specialisation of `coeff_iterate_derivative` at `k = 0`: the constant term of the `n`-th formal +derivative recovers `n !` times the `n`-th coefficient, `constantCoeff (Dⁿ f) = n ! * coeff n f`. -/ +theorem constantCoeff_iterate_derivative (f : R⟦X⟧) (n : ℕ) : + constantCoeff ((d⁄dX R)^[n] f) = n ! * coeff n f := by + simpa using coeff_iterate_derivative f n 0 + theorem derivative_coe (f : R[X]) : d⁄dX R f = Polynomial.derivative f := by ext rw [coeff_derivative, coeff_coe, coeff_coe, Polynomial.coeff_derivative] diff --git a/Mathlib/RingTheory/PowerSeries/Restricted.lean b/Mathlib/RingTheory/PowerSeries/Restricted.lean index aa9376d8e99..cdf394d9c98 100644 --- a/Mathlib/RingTheory/PowerSeries/Restricted.lean +++ b/Mathlib/RingTheory/PowerSeries/Restricted.lean @@ -5,159 +5,87 @@ Authors: William Coram -/ module -public import Mathlib.Analysis.Normed.Group.Ultra -public import Mathlib.Analysis.RCLike.Basic +public import Mathlib.RingTheory.MvPowerSeries.Restricted public import Mathlib.RingTheory.PowerSeries.Basic -public import Mathlib.Tactic.Bound +public import Mathlib.Order.Filter.Cofinite /-! -# Restricted power series +# Univariate restricted power series -`IsRestricted` : We say a power series over a normed ring `R` is restricted for a parameter `c` if -`‖coeff R i f‖ * c ^ i → 0`. +`IsRestricted` : We say a univariate power series over a normed ring `R` is restricted for a +real number `c` if `‖coeff t f‖ * c i ^ t i → 0` under the cofinite filter. -/ @[expose] public section - namespace PowerSeries -variable {R : Type*} [NormedRing R] (c : ℝ) +open Filter +open scoped Topology Pointwise + +variable {R : Type*} [NormedRing R] (c : ℝ) (f : PowerSeries R) + +/-- Predicate for when `f` is a restricted power series. -/ +abbrev IsRestricted := + MvPowerSeries.IsRestricted (σ := Unit) (fun _ ↦ c) f + +private lemma isRestricted_comp_uniqueEquiv : + (fun (t : Unit →₀ ℕ) ↦ ‖MvPowerSeries.coeff t f‖ * t.prod (fun _ x ↦ c ^ x)) = + (fun (n : ℕ) ↦ ‖coeff n f‖ * c ^ n) ∘ Finsupp.uniqueEquiv () := by + funext t + simp only [Function.comp_apply, Finsupp.uniqueEquiv_apply, PUnit.default_eq_unit, + Finsupp.prod_pow, Finset.univ_unique, Finset.prod_singleton, coeff, + show (Finsupp.single () (t ())) = t by grind] + +lemma isRestricted_iff : IsRestricted c f ↔ + Tendsto (fun (t : ℕ) ↦ ‖coeff t f‖ * c ^ t) cofinite (𝓝 0) := by + rw [IsRestricted, MvPowerSeries.IsRestricted, isRestricted_comp_uniqueEquiv] + exact ⟨fun H ↦ (H.comp (Finsupp.uniqueEquiv ()).symm.injective.tendsto_cofinite).congr fun n ↦ + by simp, fun H ↦ H.comp (Finsupp.uniqueEquiv ()).injective.tendsto_cofinite⟩ + +lemma isRestricted_iff' : IsRestricted c f ↔ + Tendsto (fun (t : ℕ) ↦ ‖coeff t f‖ * c ^ t) atTop (𝓝 0) := by + simp_rw [isRestricted_iff, Nat.cofinite_eq_atTop] + +@[simp] +lemma isRestricted_abs_iff : IsRestricted |c| f ↔ IsRestricted c f := + MvPowerSeries.isRestricted_abs_iff (fun _ ↦ c) f -open PowerSeries Filter -open scoped Topology +lemma isRestricted_zero : IsRestricted c (0 : PowerSeries R) := + MvPowerSeries.isRestricted_zero (fun _ ↦ c) -/-- A power series over `R` is restricted of parameter `c` if we have -`‖coeff R i f‖ * c ^ i → 0`. -/ -def IsRestricted (f : PowerSeries R) := - Tendsto (fun (i : ℕ) ↦ (norm (coeff i f)) * c ^ i) atTop (𝓝 0) +lemma isRestricted_monomial (n : ℕ) (a : R) : IsRestricted c (monomial n a) := + MvPowerSeries.isRestricted_monomial (fun _ ↦ c) ((Finsupp.single () n)) a + +lemma isRestricted_one : IsRestricted c (1 : PowerSeries R) := + MvPowerSeries.isRestricted_monomial (fun _ ↦ c) 0 1 + +lemma isRestricted_C (a : R) : IsRestricted c (C a) := + MvPowerSeries.isRestricted_C (fun _ ↦ c) a + +variable {f} in +lemma isRestricted.add {g : PowerSeries R} (hf : IsRestricted c f) (hg : IsRestricted c g) : + IsRestricted c (f + g) := + MvPowerSeries.isRestricted.add (fun _ ↦ c) hf hg + +variable {f} in +lemma isRestricted.neg (hf : IsRestricted c f) : IsRestricted c (-f) := + MvPowerSeries.isRestricted.neg (fun _ ↦ c) hf + +lemma isRestricted.mul [IsUltrametricDist R] (c : ℝ) {f g : PowerSeries R} + (hf : IsRestricted c f) (hg : IsRestricted c g) : IsRestricted c (f * g) := + MvPowerSeries.isRestricted.mul (fun _ ↦ c) hf hg namespace IsRestricted -lemma isRestricted_iff {f : PowerSeries R} : IsRestricted c f ↔ - ∀ ε, 0 < ε → ∃ N, ∀ n, N ≤ n → ‖‖(coeff n) f‖ * c ^ n‖ < ε := by - simp [IsRestricted, NormedAddCommGroup.tendsto_atTop] - -lemma isRestricted_iff_abs (f : PowerSeries R) : IsRestricted c f ↔ IsRestricted |c| f := by - simp [isRestricted_iff] - -lemma zero : IsRestricted c (0 : PowerSeries R) := by - simp [IsRestricted] - -lemma one : IsRestricted c (1 : PowerSeries R) := by - simp only [isRestricted_iff, coeff_one, norm_mul, norm_pow, Real.norm_eq_abs] - refine fun _ _ ↦ ⟨1, fun n hn ↦ ?_ ⟩ - split - · lia - · simpa - -lemma monomial (n : ℕ) (a : R) : IsRestricted c (monomial n a) := by - simp only [monomial_eq_mk, isRestricted_iff, coeff_mk, norm_mul, norm_pow, - Real.norm_eq_abs, abs_norm] - refine fun _ _ ↦ ⟨n + 1, fun _ _ ↦ ?_⟩ - split - · lia - · simpa - -lemma C (a : R) : IsRestricted c (C a) := by - simpa [monomial_zero_eq_C_apply] using monomial c 0 a - -lemma add {f g : PowerSeries R} (hf : IsRestricted c f) (hg : IsRestricted c g) : - IsRestricted c (f + g) := by - simp only [isRestricted_iff, map_add, norm_mul, norm_pow, Real.norm_eq_abs] at ⊢ hf hg - intro ε hε - obtain ⟨fN, hfN⟩ := hf (ε / 2) (by positivity) - obtain ⟨gN, hgN⟩ := hg (ε / 2) (by positivity) - simp only [abs_norm] at hfN hgN ⊢ - refine ⟨max fN gN, fun n hn ↦ ?_ ⟩ - calc _ ≤ ‖(coeff n) f‖ * |c| ^ n + ‖(coeff n) g‖ * |c| ^ n := by grw [norm_add_le, add_mul] - _ < ε / 2 + ε / 2 := by gcongr <;> grind - _ = ε := by ring - -lemma neg {f : PowerSeries R} (hf : IsRestricted c f) : IsRestricted c (-f) := by - simpa [isRestricted_iff] using hf - -lemma smul {f : PowerSeries R} (hf : IsRestricted c f) (r : R) : IsRestricted c (r • f) := by - if h : r = 0 then simpa [h] using zero c else - simp_rw [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at ⊢ hf - intro ε _ - obtain ⟨n, hn⟩ := hf (ε / ‖r‖) (by positivity) - refine ⟨n, fun N hN ↦ ?_⟩ - calc _ ≤ ‖r‖ * ‖(coeff N) f‖ * |c| ^ N := - mul_le_mul_of_nonneg (norm_mul_le _ _) (by simp) (by simp) (by simp) - _ < ‖r‖ * (ε / ‖r‖) := by - rw [mul_assoc]; aesop - _ = ε := mul_div_cancel₀ _ (by aesop) - - -/-- The set of `‖coeff R i f‖ * c ^ i` for a given power series `f` and parameter `c`. -/ -def convergenceSet (f : PowerSeries R) : Set ℝ := {‖coeff i f‖ * c^i | i : ℕ} - -open Finset in -lemma convergenceSet_BddAbove {f : PowerSeries R} (hf : IsRestricted c f) : - BddAbove (convergenceSet c f) := by - simp_rw [isRestricted_iff] at hf - obtain ⟨N, hf⟩ := by simpa using (hf 1) - rw [bddAbove_def, convergenceSet] - use max 1 (max' (image (fun i ↦ ‖coeff i f‖ * c ^ i) (range (N + 1))) (by simp)) - simp only [Set.mem_ofPred_eq, le_sup_iff, forall_exists_index, forall_apply_eq_imp_iff] - intro i - rcases le_total i N with h | h - · right - apply le_max' - simp only [mem_image, mem_range] - exact ⟨i, by lia, rfl⟩ - · left - calc _ ≤ ‖(coeff i) f‖ * |c ^ i| := by bound - _ ≤ 1 := by simpa using (hf i h).le +/-- Restricted power series as an additive subgroup of `PowerSeries R`. -/ +def addSubgroup (c : ℝ) : AddSubgroup (PowerSeries R) := + MvPowerSeries.IsRestricted.addSubgroup (fun _ ↦ c) variable [IsUltrametricDist R] -open IsUltrametricDist - -lemma mul {f g : PowerSeries R} (hf : IsRestricted c f) (hg : IsRestricted c g) : - IsRestricted c (f * g) := by - obtain ⟨a, ha, fBound1⟩ := (bddAbove_iff_exists_ge 1).mp (convergenceSet_BddAbove _ - ((isRestricted_iff_abs c f).mp hf)) - obtain ⟨b, hb, gBound1⟩ := (bddAbove_iff_exists_ge 1).mp (convergenceSet_BddAbove _ - ((isRestricted_iff_abs c g).mp hg)) - simp only [convergenceSet, Set.mem_ofPred_eq, forall_exists_index, forall_apply_eq_imp_iff] - at fBound1 gBound1 - simp only [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm, - PowerSeries.coeff_mul] at ⊢ hf hg - intro ε hε - obtain ⟨Nf, fBound2⟩ := (hf (ε / (max a b))) (by positivity) - obtain ⟨Ng, gBound2⟩ := (hg (ε / (max a b))) (by positivity) - refine ⟨2 * max Nf Ng, fun n hn ↦ ?_⟩ - obtain ⟨⟨fst, snd⟩, hi, ultrametric⟩ := exists_norm_finsetSum_le (Finset.antidiagonal n) - (fun a ↦ (coeff a.1) f * (coeff a.2) g) - obtain ⟨rfl⟩ := by simpa using hi (⟨(0, n), by simp⟩) - calc _ ≤ ‖(coeff fst) f * (coeff snd) g‖ * |c| ^ (fst + snd) := by bound - _ ≤ ‖(coeff fst) f‖ * |c| ^ fst * (‖(coeff snd) g‖ * |c| ^ snd) := by - grw [norm_mul_le] - #adaptation_note - /-- - Broken in `nightly-2025-10-26`: this was by `grind`, but is now no longer supported. - See https://github.com/leanprover/lean4/pull/10970. - -/ - rw [pow_add] - grind - have : max Nf Ng ≤ fst ∨ max Nf Ng ≤ snd := by lia - rcases this with this | this - · calc _ < ε / max a b * b := by - grw [gBound1 snd] - gcongr - exact fBound2 fst (by omega) - _ ≤ ε := by - rw [div_mul_comm, mul_le_iff_le_one_left ‹_›] - bound - · calc _ < a * (ε / max a b) := by - grw [fBound1 fst] - gcongr - exact gBound2 snd (by omega) - _ ≤ ε := by - rw [mul_div_left_comm, mul_le_iff_le_one_right ‹_›] - bound - -end IsRestricted -end PowerSeries +/-- Restricted power series as an subring of `PowerSeries R`. -/ +def subring (c : ℝ) : Subring (PowerSeries R) := + MvPowerSeries.IsRestricted.subring (fun _ ↦ c) + +end PowerSeries.IsRestricted diff --git a/Mathlib/RingTheory/SimpleModule/Basic.lean b/Mathlib/RingTheory/SimpleModule/Basic.lean index d959b463994..9d011b5a840 100644 --- a/Mathlib/RingTheory/SimpleModule/Basic.lean +++ b/Mathlib/RingTheory/SimpleModule/Basic.lean @@ -16,7 +16,6 @@ public import Mathlib.Order.JordanHolder public import Mathlib.RingTheory.Ideal.Colon public import Mathlib.RingTheory.Noetherian.Defs public import Mathlib.SetTheory.Cardinal.NatCard - public import Mathlib.Algebra.NoZeroSMulDivisors.Basic /-! diff --git a/Mathlib/RingTheory/Smooth/NoetherianDescent.lean b/Mathlib/RingTheory/Smooth/NoetherianDescent.lean index 65ffbc4d7ba..9255cf2f38d 100644 --- a/Mathlib/RingTheory/Smooth/NoetherianDescent.lean +++ b/Mathlib/RingTheory/Smooth/NoetherianDescent.lean @@ -51,20 +51,34 @@ variable (D : DescentAux A B) variable (R) /-- (Implementation detail): The finite type `R`-algebra. -/ -def subalgebra (D : DescentAux A B) : Subalgebra R A := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def subalgebra (D : DescentAux A B) : Subalgebra R A := Algebra.adjoin R (D.P.coeffs ∪ ((⋃ i, (D.h i).coeffs) ∪ (⋃ i, ⋃ x ∈ (D.q i).coeffs, x.coeffs) ∪ (⋃ i, ⋃ x ∈ (D.p i).coeffs, x.coeffs)) : Set A) -instance : CommRing (D.subalgebra R) := inferInstanceAs <| CommRing (Algebra.adjoin _ _) - -instance algebra₀ : Algebra R (D.subalgebra R) := inferInstanceAs <| Algebra R (Algebra.adjoin _ _) - -instance algebra₁ : Algebra (D.subalgebra R) A := inferInstanceAs <| Algebra (Algebra.adjoin _ _) A - -instance algebra₂ : Algebra (D.subalgebra R) B := inferInstanceAs <| Algebra (Algebra.adjoin _ _) B +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable instance : CommRing (D.subalgebra R) := + inferInstanceAs <| CommRing (Algebra.adjoin _ _) + +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable instance algebra₀ : Algebra R (D.subalgebra R) := + inferInstanceAs <| Algebra R (Algebra.adjoin _ _) + +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable instance algebra₁ : Algebra (D.subalgebra R) A := + inferInstanceAs <| Algebra (Algebra.adjoin _ _) A + +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable instance algebra₂ : Algebra (D.subalgebra R) B := + inferInstanceAs <| Algebra (Algebra.adjoin _ _) B instance : IsScalarTower (D.subalgebra R) A B := inferInstanceAs <| IsScalarTower (Algebra.adjoin _ _) _ _ diff --git a/Mathlib/RingTheory/Valuation/Extension.lean b/Mathlib/RingTheory/Valuation/Extension.lean index 2cd3a3fc4c5..71f15d7604f 100644 --- a/Mathlib/RingTheory/Valuation/Extension.lean +++ b/Mathlib/RingTheory/Valuation/Extension.lean @@ -6,7 +6,6 @@ Authors: Jiedong Jiang, Bichang Lei, María Inés de Frutos-Fernández, Filippo module public import Mathlib.RingTheory.Valuation.ValuationSubring - public import Mathlib.Algebra.NoZeroSMulDivisors.Basic /-! diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index 6e239fb555c..8cdb1fb5033 100644 --- a/Mathlib/Tactic.lean +++ b/Mathlib/Tactic.lean @@ -99,7 +99,6 @@ public import Mathlib.Tactic.DeriveCountable public import Mathlib.Tactic.DeriveEncodable public import Mathlib.Tactic.DeriveFintype public import Mathlib.Tactic.DeriveTraversable -public import Mathlib.Tactic.Determinant.Bird public import Mathlib.Tactic.Determinant.Bird.Cert public import Mathlib.Tactic.Determinant.Bird.Meta public import Mathlib.Tactic.DuplicateDecls @@ -224,6 +223,7 @@ public import Mathlib.Tactic.MoveAdd public import Mathlib.Tactic.NoncommRing public import Mathlib.Tactic.Nontriviality public import Mathlib.Tactic.Nontriviality.Core +public import Mathlib.Tactic.NormDet public import Mathlib.Tactic.NormNum public import Mathlib.Tactic.NormNum.Abs public import Mathlib.Tactic.NormNum.Basic diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean index 01fa2cdc218..77101da34d5 100644 --- a/Mathlib/Tactic/Common.lean +++ b/Mathlib/Tactic/Common.lean @@ -122,7 +122,6 @@ public import Mathlib.Util.CountHeartbeats public import Mathlib.Util.PrintSorries public import Mathlib.Util.TransImports public import Mathlib.Util.WhatsNew - public import Lean.Elab.Tactic.Try /-! diff --git a/Mathlib/Tactic/Determinant/Bird.lean b/Mathlib/Tactic/Determinant/Bird.lean deleted file mode 100644 index 05fdc2ae979..00000000000 --- a/Mathlib/Tactic/Determinant/Bird.lean +++ /dev/null @@ -1,34 +0,0 @@ -/- -Copyright (c) 2026 Paul Cadman. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Paul Cadman --/ -module - -public import Mathlib.Tactic.Determinant.Bird.Cert - -/-! -# `norm_det` simproc and `eval_det` tactic - -A tactic for normalizing matrix determinants. --/ - -public meta section - -open Lean Meta Elab Tactic Simp -open Mathlib.Tactic.Determinant - -/-- reify a `BirdDet` call and normalize it using the certificate-chain evaluator -/ -def normalizeBirdDet (e : Expr) : MetaM Simp.Result := do - let ⟨rα, ctx⟩ ← reifyBirdDet e - let detNorm ← certBirdDet (rα := rα) |>.run' {} |>.run ctx |>.run .reducible - Mathlib.Tactic.RingNF.cleanup {} {expr := detNorm.norm, proof? := some detNorm.proof} - -/-- Normalize a literal `birdDet` call using the certificate-chain evaluator. -/ -simproc_decl norm_det (BirdDet.birdDet _ _) := fun e => do - return .done (← normalizeBirdDet e) - -/-- Normalize `birdDet` calls in the target using the certificate-chain simproc. -/ -macro (name := evalDet) "eval_det" : tactic => `(tactic| simp only [norm_det]) - -end diff --git a/Mathlib/Tactic/NormDet.lean b/Mathlib/Tactic/NormDet.lean new file mode 100644 index 00000000000..de5787fcd9e --- /dev/null +++ b/Mathlib/Tactic/NormDet.lean @@ -0,0 +1,89 @@ +/- +Copyright (c) 2026 Paul Cadman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Cadman +-/ +module + +public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic +meta import Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness +public meta import Mathlib.Tactic.Determinant.Bird.Cert + +/-! +# `norm_det` simproc and `eval_det` tactic + +This module defines the `norm_det` simproc and the `eval_det` tactic for +normalizing determinants of matrix literals over a commutative ring. +-/ + +public meta section + +open Lean Meta Qq +open Mathlib.Tactic.Determinant + +/-- reify a `BirdDet` call and normalize it using the certificate-chain evaluator -/ +private def normalizeBirdDet (e : Expr) : MetaM Simp.Result := do + let ⟨rα, ctx⟩ ← reifyBirdDet e + let detNorm ← certBirdDet (rα := rα) |>.run' {} |>.run ctx |>.run .reducible + Mathlib.Tactic.RingNF.cleanup {} {expr := detNorm.norm, proof? := some detNorm.proof} + +/-- Normalize the determinant of `A` from its `entries` in row-major order -/ +private def normalizeDetFromEntries {u : Level} {α : Q(Type u)} {n : Q(ℕ)} (rα : Q(CommRing $α)) + (A : Q(Matrix (Fin $n) (Fin $n) $α)) (entries : Array Q($α)) : + MetaM Simp.Result := do + let arrayExpr : Q(Array $α) ← mkArrayLit α entries.toList + let hA ← mkDecideProofQ q(Array.size $arrayExpr = $n * $n) + have : $arrayExpr =Q Array.ofFn fun k : Fin ($n * $n) ↦ $A k.divNat k.modNat := ⟨⟩ + let ofArrayEqA := q(Matrix.ofArray_ofFn $A) + let birdDet := q(BirdDet.birdDet $n $arrayExpr) + let detEqBirdDet := q($ofArrayEqA ▸ BirdDet.det_eq_birdDet $arrayExpr $hA) + let birdDetNorm ← normalizeBirdDet birdDet + let detEqBirdDetRes : Simp.Result := ⟨birdDet, some detEqBirdDet, true⟩ + detEqBirdDetRes.mkEqTrans birdDetNorm + +/-- Extract the entries of a square `!![...]` matrix literal in row-major order. +Returns `none` if `A` is not an `n × n` matrix literal. -/ +private def entriesOfMatrixLiteral? {u : Level} {α : Q(Type u)} {n : Q(ℕ)} + (A : Q(Matrix (Fin $n) (Fin $n) $α)) : + MetaM (Option (Array Q($α))) := do + let some dim ← getNatValue? n | return none + let ~q(Matrix.of $rows) := A | return none + let (matrixRows, _, _) ← Matrix.matchVecConsPrefix n rows + unless matrixRows.length == dim do return none + let entriesByRow ← matrixRows.mapM fun row => do + let (entries, _, _) ← Matrix.matchVecConsPrefix n row + return entries + unless entriesByRow.all (·.length == dim) do return none + let entries ← entriesByRow.flatten.mapM fun entry => do + let some entry ← checkTypeQ entry α | throwError "expected matrix entry to have type {α}" + return entry + return some entries.toArray + +/-- The `norm_det` simproc normalizes determinants of matrices written using `!![...]` +notation over a commutative ring. -/ +simproc_decl norm_det (Matrix.det _) := fun e => do + let e ← instantiateMVars e + let ⟨_, _, e⟩ ← inferTypeQ' e + let ~q(@Matrix.det (Fin $n) _ _ _ $rα $matrix) := e | return .continue + let some entries ← entriesOfMatrixLiteral? matrix | return .continue + return .done (← normalizeDetFromEntries rα matrix entries) + +/-- +`eval_det` normalizes determinants of matrices written using `!![...]` notation +over a commutative ring. + +Examples: + +```lean +example : Matrix.det (R := ℤ) !![1, 2; 3, 4] = -2 := by + eval_det + +example {R : Type*} [CommRing R] (a b c d : R) : + Matrix.det !![a, b; c, d] = a * d - b * c := by + eval_det + ring +``` +-/ +macro (name := evalDet) "eval_det" : tactic => `(tactic| simp only [norm_det]) + +end diff --git a/Mathlib/Topology/Algebra/ConstMulAction.lean b/Mathlib/Topology/Algebra/ConstMulAction.lean index 3185cf45929..4d70c0264fb 100644 --- a/Mathlib/Topology/Algebra/ConstMulAction.lean +++ b/Mathlib/Topology/Algebra/ConstMulAction.lean @@ -180,6 +180,17 @@ theorem isClosed_setOfPred_map_smul {N : Type*} (α β) [SMul M α] [SMul N β] end SMul +section SMulZeroClass + +variable [TopologicalSpace α] [Zero α] [SMulZeroClass M α] [ContinuousConstSMul M α] + +protected theorem Filter.Tendsto.const_smul_zero {g : β → α} {l : Filter β} + (c : M) (hg : Tendsto g l (𝓝 0)) : + Tendsto (fun x ↦ c • g x) l (𝓝 0) := + smul_zero c (A := α) ▸ hg.const_smul c + +end SMulZeroClass + section Monoid variable [TopologicalSpace α] diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean index 383e84088b4..da0922c9267 100644 --- a/Mathlib/Topology/Algebra/Module/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/Basic.lean @@ -66,9 +66,9 @@ theorem Submodule.eq_top_of_nonempty_interior' [NeBot (𝓝[{ x : R | IsUnit x } rcases hs with ⟨y, hy⟩ refine Submodule.eq_top_iff'.2 fun x => ?_ rw [mem_interior_iff_mem_nhds] at hy - have : Tendsto (fun c : R => y + c • x) (𝓝[{ x : R | IsUnit x }] 0) (𝓝 (y + (0 : R) • x)) := - tendsto_const_nhds.add ((tendsto_nhdsWithin_of_tendsto_nhds tendsto_id).smul tendsto_const_nhds) - rw [zero_smul, add_zero] at this + have : Tendsto (fun c : R ↦ y + c • x) (𝓝[{ x : R | IsUnit x }] 0) (𝓝 (y + 0)) := + tendsto_const_nhds.add ((tendsto_nhdsWithin_of_tendsto_nhds tendsto_id).zero_smul_const _) + rw [add_zero] at this obtain ⟨_, hu : y + _ • _ ∈ s, u, rfl⟩ := nonempty_of_mem (inter_mem (Filter.mem_map.1 (this hy)) self_mem_nhdsWithin) have hy' : y ∈ ↑s := mem_of_mem_nhds hy @@ -90,8 +90,8 @@ theorem Module.punctured_nhds_neBot [Nontrivial M] [NeBot (𝓝[≠] (0 : R))] [ rcases exists_ne (0 : M) with ⟨y, hy⟩ suffices Tendsto (fun c : R => x + c • y) (𝓝[≠] 0) (𝓝[≠] x) from this.neBot refine Tendsto.inf ?_ (tendsto_principal_principal.2 <| ?_) - · convert! tendsto_const_nhds.add ((@tendsto_id R _).smul_const y) - rw [zero_smul, add_zero] + · convert! tendsto_const_nhds.add ((@tendsto_id R _).zero_smul_const y) + rw [add_zero] · intro c hc simpa [hy] using hc diff --git a/Mathlib/Topology/Algebra/Module/EmbeddingOfLocal.lean b/Mathlib/Topology/Algebra/Module/EmbeddingOfLocal.lean index d65e2478292..29325bbb0d5 100644 --- a/Mathlib/Topology/Algebra/Module/EmbeddingOfLocal.lean +++ b/Mathlib/Topology/Algebra/Module/EmbeddingOfLocal.lean @@ -106,11 +106,10 @@ lemma ContinuousSMul.topology_eq_of_nhds_inf_principal_eq (t₁ t₂ : Topologic -- Let `w ∈ W` be arbitrary. intro w w_in_W -- Because `V` is a `t₁`-neighborhood of `0`, we have `c ^ n • w ∈ V` for some natural number `n`. - obtain ⟨n, hn⟩ : ∃ n : ℕ, c ^ n • w ∈ V := by + obtain ⟨n, hn⟩ : ∃ n : ℕ, c ^ n • w ∈ V := let := t₁ - have : Tendsto (fun k : ℕ ↦ c ^ k • w) atTop (𝓝 0) := - zero_smul 𝕜₁ w ▸ (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hc₁).smul_const w - exact this.eventually_mem V_mem |>.exists + tendsto_pow_atTop_nhds_zero_of_norm_lt_one hc₁ |>.zero_smul_const w + |>.eventually_mem V_mem |>.exists -- We will conclude by reducing `c ^ n • w ∈ V` to `w = c ^ 0 • w ∈ V` inductively. suffices c ^ 0 • w ∈ V by simpa apply Nat.decreasingInduction (motive := fun (k : ℕ) _ ↦ c^k • w ∈ V) ?_ hn n.zero_le diff --git a/Mathlib/Topology/Algebra/MulAction.lean b/Mathlib/Topology/Algebra/MulAction.lean index a2c24ba7ee7..ce466c4e934 100644 --- a/Mathlib/Topology/Algebra/MulAction.lean +++ b/Mathlib/Topology/Algebra/MulAction.lean @@ -201,10 +201,48 @@ instance SMulMemClass.continuousSMul {S : Type*} [SetLike S X] [SMulMemClass S M end SMul +section SMulZeroClass + +variable [Zero X] [SMulZeroClass M X] [ContinuousSMul M X] + +protected theorem Filter.Tendsto.smul_zero {f : α → M} {g : α → X} {l : Filter α} {c : M} + (hf : Tendsto f l (𝓝 c)) (hg : Tendsto g l (𝓝 0)) : + Tendsto (fun x ↦ f x • g x) l (𝓝 0) := + smul_zero c (A := X) ▸ hf.smul hg + +end SMulZeroClass + +section SMulWithZero + +variable [Zero M] [Zero X] [SMulWithZero M X] [ContinuousSMul M X] + +protected theorem Filter.Tendsto.zero_smul {f : α → M} {g : α → X} {l : Filter α} {a : X} + (hf : Tendsto f l (𝓝 0)) (hg : Tendsto g l (𝓝 a)) : + Tendsto (fun x ↦ f x • g x) l (𝓝 0) := + zero_smul M a ▸ hf.smul hg + +protected theorem Filter.Tendsto.zero_smul_const {f : α → M} {l : Filter α} + (hf : Tendsto f l (𝓝 0)) (a : X) : + Tendsto (fun x ↦ f x • a) l (𝓝 0) := + hf.zero_smul tendsto_const_nhds + +end SMulWithZero + section Monoid variable [Monoid M] [MulAction M X] [ContinuousSMul M X] +@[to_additive] +protected theorem Filter.Tendsto.one_smul {f : α → M} {g : α → X} {l : Filter α} {a : X} + (hf : Tendsto f l (𝓝 1)) (hg : Tendsto g l (𝓝 a)) : + Tendsto (fun x ↦ f x • g x) l (𝓝 a) := + one_smul M a ▸ hf.smul hg + +@[to_additive] +protected theorem Filter.Tendsto.one_smul_const {f : α → M} {l : Filter α} + (hf : Tendsto f l (𝓝 1)) (a : X) : Tendsto (fun x ↦ f x • a) l (𝓝 a) := + hf.one_smul tendsto_const_nhds + @[to_additive] instance Units.continuousSMul : ContinuousSMul Mˣ X := IsInducing.id.continuousSMul Units.continuous_val rfl diff --git a/Mathlib/Topology/Algebra/Valued/ValuationTopology.lean b/Mathlib/Topology/Algebra/Valued/ValuationTopology.lean index 2eeaf86c8b9..8cce79014c3 100644 --- a/Mathlib/Topology/Algebra/Valued/ValuationTopology.lean +++ b/Mathlib/Topology/Algebra/Valued/ValuationTopology.lean @@ -9,7 +9,6 @@ public import Mathlib.Algebra.Order.Group.Units public import Mathlib.Topology.Algebra.Nonarchimedean.Bases public import Mathlib.Topology.Algebra.UniformFilterBasis public import Mathlib.RingTheory.Valuation.ValuationSubring - public import Mathlib.Algebra.Order.GroupWithZero.Range /-! diff --git a/Mathlib/Topology/Category/Profinite/Nobeling/Successor.lean b/Mathlib/Topology/Category/Profinite/Nobeling/Successor.lean index f85f8dbf1c5..126fe2f46aa 100644 --- a/Mathlib/Topology/Category/Profinite/Nobeling/Successor.lean +++ b/Mathlib/Topology/Category/Profinite/Nobeling/Successor.lean @@ -121,7 +121,9 @@ theorem union_C0C1_eq : (C0 C ho) ∪ (C1 C ho) = C := by The intersection of `C0` and the projection of `C1`. We will apply the inductive hypothesis to this set. -/ -def C' := C0 C ho ∩ π (C1 C ho) (ord I · < o) +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def C' := C0 C ho ∩ π (C1 C ho) (ord I · < o) include hC in theorem isClosed_C' : IsClosed (C' C ho) := diff --git a/Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean b/Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean index 94cf0ce02c0..0c987502211 100644 --- a/Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean +++ b/Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean @@ -141,7 +141,9 @@ The image of the `GoodProducts` for `π C (ord I · < o)` in `LocallyConstant C refers to the setting in which we will use this, when we are mapping in `GoodProducts` from a smaller set, i.e. when `o` is a smaller ordinal than the one `C` is "contained" in. -/ -def smaller (o : Ordinal) : Set (LocallyConstant C ℤ) := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def smaller (o : Ordinal) : Set (LocallyConstant C ℤ) := (πs C o) '' (range (π C (ord I · < o))) /-- @@ -237,7 +239,9 @@ theorem GoodProducts.union : range C = ⋃ (e : {o' // o' < o}), (smaller C e.va The image of the `GoodProducts` in `C` is equivalent to the union of `smaller C o'` over all ordinals `o' < o`. -/ -def GoodProducts.range_equiv : range C ≃ ⋃ (e : {o' // o' < o}), (smaller C e.val) := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def GoodProducts.range_equiv : range C ≃ ⋃ (e : {o' // o' < o}), (smaller C e.val) := Equiv.setCongr (union C ho hsC) theorem GoodProducts.range_equiv_factorization : diff --git a/Mathlib/Topology/Compactness/SigmaCompact.lean b/Mathlib/Topology/Compactness/SigmaCompact.lean index 7adad95658a..d63b47913bc 100644 --- a/Mathlib/Topology/Compactness/SigmaCompact.lean +++ b/Mathlib/Topology/Compactness/SigmaCompact.lean @@ -199,7 +199,9 @@ variable [SigmaCompactSpace X] open SigmaCompactSpace /-- A choice of compact covering for a `σ`-compact space, chosen to be monotone. -/ -def compactCovering : ℕ → Set X := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def compactCovering : ℕ → Set X := accumulate exists_compact_covering.choose theorem isCompact_compactCovering (n : ℕ) : IsCompact (compactCovering X n) := diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index 5caac6abf7f..445fa61e0e1 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -500,7 +500,9 @@ open scoped Classical in component of `x` in `F` is the connected component of `x` in the subtype `F` seen as a set in `α`. This definition does not make sense if `x` is not in `F` so we return the empty set in this case. -/ -def connectedComponentIn (F : Set α) (x : α) : Set α := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def connectedComponentIn (F : Set α) (x : α) : Set α := if h : x ∈ F then (↑) '' connectedComponent (⟨x, h⟩ : F) else ∅ theorem connectedComponentIn_eq_image {F : Set α} {x : α} (h : x ∈ F) : @@ -649,7 +651,7 @@ class PreconnectedSpace (α : Type u) [TopologicalSpace α] : Prop where export PreconnectedSpace (isPreconnected_univ) /-- A connected space is a nonempty one where there is no non-trivial open partition. -/ -@[wikidata Q1491995] +@[wikidata Q1491995, mk_iff] class ConnectedSpace (α : Type u) [TopologicalSpace α] : Prop extends PreconnectedSpace α where /-- A connected space is nonempty. -/ toNonempty : Nonempty α diff --git a/Mathlib/Topology/Instances/CantorSet.lean b/Mathlib/Topology/Instances/CantorSet.lean index 2f13fc37604..559ef80a5c8 100644 --- a/Mathlib/Topology/Instances/CantorSet.lean +++ b/Mathlib/Topology/Instances/CantorSet.lean @@ -39,7 +39,9 @@ This file defines the Cantor ternary set and proves a few properties. middle third of each interval. Formally, the order `n + 1` pre-Cantor set is the union of the images under the functions `(· / 3)` and `((2 + ·) / 3)` of `preCantorSet n`. -/ -def preCantorSet : ℕ → Set ℝ +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def preCantorSet : ℕ → Set ℝ | 0 => Set.Icc 0 1 | n + 1 => (· / 3) '' preCantorSet n ∪ (fun x ↦ (2 + x) / 3) '' preCantorSet n @@ -52,7 +54,9 @@ def preCantorSet : ℕ → Set ℝ pre-Cantor sets. This means that the Cantor set is obtained by iteratively removing the open middle third of each subinterval, starting from the unit interval `[0, 1]`. -/ -def cantorSet : Set ℝ := ⋂ n, preCantorSet n +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def cantorSet : Set ℝ := ⋂ n, preCantorSet n /-! diff --git a/Mathlib/Topology/Instances/Rat.lean b/Mathlib/Topology/Instances/Rat.lean index 41efad1a53b..1e2408bbc0f 100644 --- a/Mathlib/Topology/Instances/Rat.lean +++ b/Mathlib/Topology/Instances/Rat.lean @@ -7,7 +7,7 @@ module public import Mathlib.Algebra.Algebra.Rat public import Mathlib.Algebra.Module.Rat -public import Mathlib.Data.NNRat.Order +public import Mathlib.Algebra.Order.Ring.NNRat public import Mathlib.Topology.Algebra.Order.Archimedean public import Mathlib.Topology.Algebra.Ring.Real public import Mathlib.Topology.Instances.Nat diff --git a/Mathlib/Topology/Irreducible.lean b/Mathlib/Topology/Irreducible.lean index 452d75ce3c4..1b9488ed10d 100644 --- a/Mathlib/Topology/Irreducible.lean +++ b/Mathlib/Topology/Irreducible.lean @@ -133,7 +133,9 @@ lemma exists_mem_irreducibleComponents_subset_of_isIrreducible (s : Set X) (hs : /-- A maximal irreducible set that contains a given point. -/ @[stacks 004W "(4)"] -def irreducibleComponent (x : X) : Set X := +-- Note: `Set` has no computational content, but Lean still attempts to compile it. +-- See https://github.com/leanprover/lean4/issues/14084. +noncomputable def irreducibleComponent (x : X) : Set X := Classical.choose (exists_preirreducible {x} isPreirreducible_singleton) theorem irreducibleComponent_property (x : X) : diff --git a/Mathlib/Topology/Sets/Compacts.lean b/Mathlib/Topology/Sets/Compacts.lean index eacdaf95b8a..bcac748c537 100644 --- a/Mathlib/Topology/Sets/Compacts.lean +++ b/Mathlib/Topology/Sets/Compacts.lean @@ -623,6 +623,14 @@ theorem singleton_prod_singleton (x : α) (y : β) : ({x} ×ˢ {y} : NonemptyCompacts (α × β)) = {(x, y)} := NonemptyCompacts.ext Set.singleton_prod_singleton +/-- `TopologicalSpace.NonemptyCompacts.toCompacts` as an order embedding. -/ +def toCompactsOrderEmbedding : NonemptyCompacts α ↪o Compacts α := + .ofMapLEIff toCompacts fun _ _ => .rfl + +@[simp] +theorem coe_toCompactsOrderEmbedding : ⇑(toCompactsOrderEmbedding (α := α)) = toCompacts := + rfl + end NonemptyCompacts /-! ### Positive compact sets -/ diff --git a/Mathlib/Topology/Sets/VietorisTopology.lean b/Mathlib/Topology/Sets/VietorisTopology.lean index 921dec54209..c7860354c96 100644 --- a/Mathlib/Topology/Sets/VietorisTopology.lean +++ b/Mathlib/Topology/Sets/VietorisTopology.lean @@ -330,6 +330,64 @@ instance [T1Space α] : T0Space (Set α) where t0 _ _ h := subset_antisymm (subset_of_specializes h.specializes) (subset_of_specializes h.specializes') +theorem isPreconnected_nonempty_finite_subsets {s : Set α} (hs : IsPreconnected s) : + IsPreconnected {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s} := by + rcases eq_empty_or_nonempty s with rfl | ⟨x, hx⟩ + · convert isPreconnected_empty + grind [Set.not_nonempty_empty] + suffices {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s} = + ⋃ n : ℕ+, range (ι := Fin n) '' Set.pi univ fun _ => s by + rw [this] + /- The family of nonempty subsets of `s` with at most `n` elements is connected, since it is the + image of `sⁿ` under the continuous map `(x₁, …, xₙ) ↦ {x₁, …, xₙ}`. It follows that their union + over `n ≥ 1` is also connected. -/ + exact isPreconnected_iUnion + ⟨{x}, mem_iInter_of_mem fun n => ⟨fun _ => x, by simpa⟩⟩ + (fun n => .image (isPreconnected_univ_pi fun _ => hs) _ (by fun_prop)) + refine subset_antisymm (fun t ht => ?_) + (iUnion_subset fun _ => image_subset_iff.mpr fun f hf => + ⟨range_nonempty _, finite_range _, by grind⟩) + obtain ⟨ht₁, ht₂, hts⟩ := ht + obtain ⟨n, f, -, rfl⟩ := ht₂.fin_param + rw [range_subset_iff] at hts + rw [range_nonempty_iff_nonempty] at ht₁ + lift n to ℕ+ using Fin.pos' + exact mem_iUnion_of_mem n <| mem_image_of_mem _ <| mem_univ_pi.mpr hts + +theorem isPreconnected_sUnion {s : Set (Set α)} (hs : IsPreconnected s) + (h : ∃ t ∈ s, IsPreconnected t) : IsPreconnected (⋃₀ s) := by + obtain ⟨t, hts, ht⟩ := h + have hts' := subset_sUnion_of_mem hts + /- Take open sets `U` and `V` covering `⋃₀ s`, and assume that they both intersect `⋃₀ s`. We have + to show that `U` and `V` intersect within `⋃₀ s` -/ + intro U V hU hV hUV + by_cases! ht' : t ⊆ U ∨ t ⊆ V + · -- Consider the case when one of them covers `t`, say `U`. + wlog htU : t ⊆ U generalizing U V + · grind + -- There is also some `u ∈ s` that intersects `V`. + rintro - hV' + rw [sUnion_eq_biUnion, iUnion₂_inter, nonempty_biUnion] at hV' + obtain ⟨u, hus, huV⟩ := hV' + -- Every set in `s` either is in `U` or intersects `V`. + have : s ⊆ U.powerset ∪ {v | (v ∩ V).Nonempty} := by + grind [=_ sdiff_subset_iff, =_ not_disjoint_iff_nonempty_inter] + -- Since `s` connects `t` and `u`, there is some `v ∈ s` that is in `U` and intersects `V`. + obtain ⟨v, hvs, hvU, hvV⟩ := + hs _ _ hU.powerset_vietoris (isOpen_inter_nonempty_of_isOpen hV) this + ⟨t, hts, htU⟩ ⟨u, hus, huV⟩ + -- `U` intersects `V` within `v`, and therefore also within `⋃₀ s`. + apply hvV.mono + grind + · -- If neither `U` nor `V` covers `t`, then they both intersect `t`, since `t ⊆ U ∪ V`. + rintro - - + have htU : ¬ Disjoint t U := by grind + have htV : ¬ Disjoint t V := by grind + rw [not_disjoint_iff_nonempty_inter] at htU htV + -- By the connectedness of `t`, `U` and `V` intersect within `t`, and therefore within `⋃₀ s`. + grw [← hts'] at hUV ⊢ + exact ht U V hU hV hUV htU htV + end vietoris namespace Compacts @@ -686,6 +744,35 @@ theorem separableSpace_iff : SeparableSpace (Compacts α) ↔ SeparableSpace α refine ⟨Classical.epsilon (· ∈ K), ?_, mem_image_of_mem _ hK₃⟩ exact hK₁ <| Classical.epsilon_spec (hK₂.mono inter_subset_left) +theorem isPreconnected_nonempty_finite_subsets {s : Set α} (hs : IsPreconnected s) : + IsPreconnected {K : Compacts α | (K : Set α).Nonempty ∧ (K : Set α).Finite ∧ ↑K ⊆ s} := by + rw [← isEmbedding_coe.isPreconnected_image] + convert vietoris.isPreconnected_nonempty_finite_subsets hs + exact subset_antisymm (image_subset_iff.mpr .rfl) (fun t ht => ⟨⟨t, ht.2.1.isCompact⟩, ht, rfl⟩) + +theorem isPreconnected_nonempty_subsets {s : Set α} (hs : IsPreconnected s) : + IsPreconnected {K : Compacts α | (K : Set α).Nonempty ∧ ↑K ⊆ s} := by + refine (isPreconnected_nonempty_finite_subsets hs).subset_closure (by grind) ?_ + rw [ofPred_and, ofPred_and] + simp_rw [Compacts.coe_nonempty, ← compl_singleton_eq] + grw [← isClopen_singleton_bot.compl.isOpen.inter_closure, closure_finite_subsets, + ← subset_closure] + +theorem isPreconnected_Icc {K L : Compacts α} (hK : K ≠ ⊥) (hL : IsPreconnected (L : Set α)) : + IsPreconnected (Icc K L) := by + wlog hKL : K ≤ L + · simpa [hKL] using isPreconnected_empty + convert (isPreconnected_nonempty_subsets hL).image (K ⊔ ·) (by fun_prop) + exact subset_antisymm + (fun M hM => ⟨M, ⟨Compacts.coe_nonempty.mpr (ne_bot_of_le_ne_bot hK hM.1), hM.2⟩, + sup_eq_right.mpr hM.1⟩) + (image_subset_iff.mpr fun M ⟨_, hM⟩ => ⟨le_sup_left, sup_le hKL hM⟩) + +theorem isPreconnected_Ioc {K L : Compacts α} (hL : IsPreconnected (L : Set α)) : + IsPreconnected (Ioc K L) := + isPreconnected_of_forall L fun M hM => ⟨Icc M L, Icc_subset_Ioc_left hM.1, right_mem_Icc.mpr hM.2, + left_mem_Icc.mpr hM.2, isPreconnected_Icc (ne_bot_of_gt hM.1) hL⟩ + end Compacts namespace NonemptyCompacts @@ -944,6 +1031,59 @@ theorem separableSpace_iff : SeparableSpace (NonemptyCompacts α) ↔ SeparableS ← range_toCompacts] exact (finite_singleton _).isSeparable.union (isSeparable_range continuous_toCompacts) +theorem isPreconnected_finite_subsets {s : Set α} (hs : IsPreconnected s) : + IsPreconnected {K : NonemptyCompacts α | (K : Set α).Finite ∧ ↑K ⊆ s} := by + rw [← isEmbedding_toCompacts.isPreconnected_image] + convert Compacts.isPreconnected_nonempty_finite_subsets hs + exact subset_antisymm + (image_subset_iff.mpr fun K hK => ⟨K.nonempty, hK⟩) + (fun K hK => ⟨⟨K, hK.1⟩, hK.2, rfl⟩) + +theorem isPreconnected_subsets {s : Set α} (hs : IsPreconnected s) : + IsPreconnected {K : NonemptyCompacts α | ↑K ⊆ s} := by + rw [← isEmbedding_toCompacts.isPreconnected_image] + convert Compacts.isPreconnected_nonempty_subsets hs + exact subset_antisymm + (image_subset_iff.mpr fun K hK => ⟨K.nonempty, hK⟩) + (fun K hK => ⟨⟨K, hK.1⟩, hK.2, rfl⟩) + +theorem isPreconnected_Icc {K L : NonemptyCompacts α} (hL : IsPreconnected (L : Set α)) : + IsPreconnected (Icc K L) := by + rw [← isEmbedding_toCompacts.isPreconnected_image, ← coe_toCompactsOrderEmbedding, + OrderEmbedding.image_Icc _ (by simpa [← Set.Ioi_bot] using ordConnected_Ioi)] + exact Compacts.isPreconnected_Icc (Compacts.coe_nonempty.mp K.nonempty) hL + +theorem isPreconnected_Ioc {K L : NonemptyCompacts α} (hL : IsPreconnected (L : Set α)) : + IsPreconnected (Ioc K L) := by + rw [← isEmbedding_toCompacts.isPreconnected_image, ← coe_toCompactsOrderEmbedding, + OrderEmbedding.image_Ioc _ (by simpa [← Set.Ioi_bot] using ordConnected_Ioi)] + exact Compacts.isPreconnected_Ioc hL + +theorem isPreconnected_Iic {K : NonemptyCompacts α} (hK : IsPreconnected (K : Set α)) : + IsPreconnected (Iic K) := + isPreconnected_subsets hK + +instance [PreconnectedSpace α] : PreconnectedSpace (NonemptyCompacts α) where + isPreconnected_univ := by simpa using isPreconnected_subsets isPreconnected_univ + +@[simp] +theorem preconnectedSpace_iff : PreconnectedSpace (NonemptyCompacts α) ↔ PreconnectedSpace α := by + refine ⟨fun h => ?_, fun h => inferInstance⟩ + rw [preconnectedSpace_iff_clopen] at h ⊢ + intro s hs + apply h _ ⟨isClosed_subsets_of_isClosed hs.isClosed, isOpen_subsets_of_isOpen hs.isOpen⟩ |>.imp + · simp only [Set.eq_empty_iff_forall_notMem] + exact fun h x hx => h {x} (Set.singleton_subset_iff.mpr hx) + · simp only [Set.eq_univ_iff_forall] + exact fun h x => Set.singleton_subset_iff.mp (h {x}) + +instance [ConnectedSpace α] : ConnectedSpace (NonemptyCompacts α) where + toNonempty := inferInstance + +@[simp] +protected theorem connectedSpace_iff : ConnectedSpace (NonemptyCompacts α) ↔ ConnectedSpace α := by + simp [connectedSpace_iff] + end NonemptyCompacts end TopologicalSpace diff --git a/Mathlib/Topology/UrysohnsLemma.lean b/Mathlib/Topology/UrysohnsLemma.lean index aa2e075d08d..3d6524584b7 100644 --- a/Mathlib/Topology/UrysohnsLemma.lean +++ b/Mathlib/Topology/UrysohnsLemma.lean @@ -82,7 +82,7 @@ lemmas about `midpoint`. Urysohn's lemma, normal topological space, locally compact topological space -/ -@[expose] public section +@[expose] public noncomputable section variable {X : Type*} [TopologicalSpace X] @@ -155,7 +155,7 @@ theorem subset_right_C (c : CU P) : c.C ⊆ c.right.C := /-- `n`-th approximation to a continuous function `f : X → ℝ` such that `f = 0` on `c.C` and `f = 1` outside of `c.U`. -/ -noncomputable def approx : ℕ → CU P → X → ℝ +def approx : ℕ → CU P → X → ℝ | 0, c, x => indicator c.Uᶜ 1 x | n + 1, c, x => midpoint ℝ (approx n c.left x) (approx n c.right x) @@ -237,7 +237,7 @@ theorem approx_mono (c : CU P) (x : X) : Monotone fun n => c.approx n x := * `0 ≤ f x ≤ 1` for all `x`; * `f` equals zero on `c.C` and equals one outside of `c.U`; -/ -protected noncomputable def lim (c : CU P) (x : X) : ℝ := +protected def lim (c : CU P) (x : X) : ℝ := ⨆ n, c.approx n x theorem tendsto_approx_atTop (c : CU P) (x : X) : diff --git a/MathlibTest/Algebra/MonoidAlgebra/Defs.lean b/MathlibTest/Algebra/MonoidAlgebra/Defs.lean index b0d1f964a90..cee2bc582a0 100644 --- a/MathlibTest/Algebra/MonoidAlgebra/Defs.lean +++ b/MathlibTest/Algebra/MonoidAlgebra/Defs.lean @@ -5,7 +5,6 @@ variable {R M A} [Semiring R] [Monoid M] [AddMonoid A] section Notation open scoped MonoidAlgebra AddMonoidAlgebra -set_option pp.mvars.anonymous false -- TODO: could resolve ambiguity based on Monoid / AddMonoid /-- error: Ambiguous term diff --git a/MathlibTest/Attribute/ToAdditive/Basic.lean b/MathlibTest/Attribute/ToAdditive/Basic.lean index 36768fc9e78..f9ee3c8b408 100644 --- a/MathlibTest/Attribute/ToAdditive/Basic.lean +++ b/MathlibTest/Attribute/ToAdditive/Basic.lean @@ -98,7 +98,6 @@ instance : my_has_scalar Nat Nat := ⟨fun a b => a * b⟩ set_option linter.translate.warnInvalid false in attribute [to_additive (reorder := α β) my_has_scalar] my_has_pow -set_option pp.mvars.anonymous false in /-- error: `to_additive` validation failed: expected {α : Type _} → {β : Type _} → [self : my_has_scalar β α] → α → β → α @@ -107,7 +106,6 @@ but 'Test.my_has_scalar.smul' has type -/ #guard_msgs in attribute [to_additive existing smul] my_has_pow.pow -set_option pp.mvars.anonymous false in /-- error: `to_additive` validation failed: expected {β : Type _} → {α : Type _} → [self : my_has_scalar β α] → α → β → α @@ -594,7 +592,7 @@ lemma one_eq_one'' {α : Type*} [One α] : (1 : α) = 1 := rfl /-- error: `to_additive` validation failed: expected - ∀ {α : Type ?u.1} [inst : Zero α], 0 = 0 + ∀ {α : Type _} [inst : Zero α], 0 = 0 but 'Eq.trans' has type ∀ {α : Sort u} {a b c : α}, a = b → b = c → a = c -/ diff --git a/MathlibTest/CategoryTheory/Bicategory/Basic.lean b/MathlibTest/CategoryTheory/Bicategory/Basic.lean index 65c11b88804..f8de368a9dd 100644 --- a/MathlibTest/CategoryTheory/Bicategory/Basic.lean +++ b/MathlibTest/CategoryTheory/Bicategory/Basic.lean @@ -33,7 +33,6 @@ set_option backward.defeqAttrib.useBackward true in /-- error: expression contains metavariables: (F.map f ≫ η.app b) ≫ ?_ -/ #guard_msgs in -set_option pp.mvars false in example (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) : η ≫ θ ⟶ η ≫ ι where as := { app a := η.app a ◁ Γ.as.app a diff --git a/MathlibTest/CategoryTheory/CategoryStar.lean b/MathlibTest/CategoryTheory/CategoryStar.lean index 5e0f143a13f..29bef43bbd9 100644 --- a/MathlibTest/CategoryTheory/CategoryStar.lean +++ b/MathlibTest/CategoryTheory/CategoryStar.lean @@ -4,8 +4,6 @@ import Mathlib.CategoryTheory.Functor.Category open CategoryTheory -set_option pp.mvars.anonymous false - section variable (C : Type*) [Category* C] diff --git a/MathlibTest/CategoryTheory/Monoidal/Basic.lean b/MathlibTest/CategoryTheory/Monoidal/Basic.lean index 4430c875873..d0a1a40e6a8 100644 --- a/MathlibTest/CategoryTheory/Monoidal/Basic.lean +++ b/MathlibTest/CategoryTheory/Monoidal/Basic.lean @@ -30,7 +30,6 @@ example {V₁ V₂ V₃ : C} (R : ∀ V₁ V₂ : C, V₁ ⊗ V₂ ⟶ V₂ ⊗ /-- error: expression contains metavariables: x ⊗ y ⊗ ?_ -/ #guard_msgs in -set_option pp.mvars false in example {x y z w : C} (f : x ⟶ y) (g : y ⟶ z) (h : x ⊗ y ⊗ w ⟶ y ⊗ z ⊗ w) (η : f ⊗ₘ (g ▷ w) = h) : (f ⊗ₘ g) ▷ w = 𝟙 _ ⊗≫ h ⊗≫ 𝟙 _ := by diff --git a/MathlibTest/DefEqAbuse.lean b/MathlibTest/DefEqAbuse.lean index 0db094fae6f..3d6e28170b8 100644 --- a/MathlibTest/DefEqAbuse.lean +++ b/MathlibTest/DefEqAbuse.lean @@ -187,7 +187,7 @@ theorem zoC_eq_iff {α} [GrC α] (a : α) : NumC.fromNat 0 = a ↔ a = GrC.add a /-- warning: #defeq_abuse: tactic fails with `backward.isDefEq.respectTransparency true` but succeeds with `false`. The following isDefEq checks are the root causes of the failure: - ❌️ @ZoC.zo Int instZoCInt =?= @ZoC.zo Int (@GrC.toZoC Int ?m.11) + ❌️ @ZoC.zo Int instZoCInt =?= @ZoC.zo Int (@GrC.toZoC Int ?_) -/ #guard_msgs in example (a : Int) : NumC.fromNat 0 = a ↔ a = GrC.add a a := by diff --git a/MathlibTest/DifferentialGeometry/Notation/Advanced.lean b/MathlibTest/DifferentialGeometry/Notation/Advanced.lean index 1f0384072fa..49ccd375e56 100644 --- a/MathlibTest/DifferentialGeometry/Notation/Advanced.lean +++ b/MathlibTest/DifferentialGeometry/Notation/Advanced.lean @@ -56,7 +56,6 @@ error: Could not find a model with corners for `TangentBundle (modelWithCornersS Hint: the expected type contains metavariables, maybe you need to provide an implicit argument -/ #guard_msgs in -set_option pp.mvars.anonymous false in lemma contMDiff_proj : CMDiff ∞ (proj) := by unfold proj exact contMDiff_snd_tangentBundle_modelSpace 𝕜 𝓘(𝕜) @@ -419,7 +418,6 @@ error: Could not find a model with corners for `ContinuousLinearMap σ E'' E'''' Hint: failures to find a model with corners can be debugged with the command `set_option trace.Elab.DiffGeo.MDiff true`. -/ #guard_msgs in -set_option pp.mvars.anonymous false in #check CMDiff 2 f variable {f : M → E'' →SL[σ] E''''} in @@ -491,7 +489,6 @@ trace: [Elab.DiffGeo.MDiff] Finding a model with corners for: `M` -/ #guard_msgs in set_option trace.Elab.DiffGeo.MDiff true in -set_option pp.mvars.anonymous false in #check CMDiff 2 f end diff --git a/MathlibTest/DifferentialGeometry/Notation/Basic.lean b/MathlibTest/DifferentialGeometry/Notation/Basic.lean index 34ebdba01e1..213d4267306 100644 --- a/MathlibTest/DifferentialGeometry/Notation/Basic.lean +++ b/MathlibTest/DifferentialGeometry/Notation/Basic.lean @@ -565,7 +565,6 @@ error: Could not find a model with corners for `?_`. Hint: the expected type contains metavariables, maybe you need to provide an implicit argument -/ #guard_msgs in -set_option pp.mvars.anonymous false in #check UniqueMDiffAt[Set.univ] m variable {s : TopologicalSpace.Opens M} @@ -589,7 +588,6 @@ in the application UniqueMDiffOn I s -/ #guard_msgs in -set_option pp.mvars.anonymous false in #check UniqueMDiffOn I s end UniqueMDiff diff --git a/MathlibTest/DifferentialGeometry/Notation/Delaborators.lean b/MathlibTest/DifferentialGeometry/Notation/Delaborators.lean index 6c43114e28e..52383e82785 100644 --- a/MathlibTest/DifferentialGeometry/Notation/Delaborators.lean +++ b/MathlibTest/DifferentialGeometry/Notation/Delaborators.lean @@ -230,7 +230,6 @@ variable {g : E × E → E × E} #check MDifferentiable 𝓘(ℝ, E × E) ((𝓘(ℝ, E)).prod (𝓘(ℝ, E))) g -- This can yield rather confusing errors -set_option pp.mvars.anonymous false in /-- error: Tactic `apply` failed: could not unify the conclusion of `@mdifferentiable_id` MDiff id diff --git a/MathlibTest/EuclideanSpace.lean b/MathlibTest/EuclideanSpace.lean index c0336ec46c2..781eb674053 100644 --- a/MathlibTest/EuclideanSpace.lean +++ b/MathlibTest/EuclideanSpace.lean @@ -10,7 +10,6 @@ section delaborator #guard_msgs in #check !₂[1, 2, 3] -set_option pp.mvars.anonymous false in /-- info: !₀[] : WithLp 0 (Fin 0 → ?_) -/ #guard_msgs in #check !₀[] diff --git a/MathlibTest/FinCoercions.lean b/MathlibTest/FinCoercions.lean index 69c81e743a5..2341fae3fce 100644 --- a/MathlibTest/FinCoercions.lean +++ b/MathlibTest/FinCoercions.lean @@ -6,8 +6,6 @@ module import Mathlib -set_option pp.mvars.anonymous false - -- We first verify that there is no global coercion from `Nat` to `Fin n`. -- Such a coercion would frequently introduce unexpected modular arithmetic. diff --git a/MathlibTest/Simproc/IPow.lean b/MathlibTest/Simproc/IPow.lean new file mode 100644 index 00000000000..dcd804e1fd4 --- /dev/null +++ b/MathlibTest/Simproc/IPow.lean @@ -0,0 +1,40 @@ +import Mathlib.Data.Complex.Basic + +/-! +# Tests for `simp`-reduction about `I ^ _`. +-/ + +open Complex + +-- simp can reduce I ^ n for literal nats n, as well as literal ints n, but not for variables n. +example : I ^ 4 = 1 := by simp +example : I ^ 5 = I := by simp +example : I ^ 100 = 1 := by simp + +example : I ^ 3 = -I := by simp + +example : I ^ (4 : ℤ) = 1 := by simp +example : I ^ (5 : ℤ) = I := by simp +example : I ^ (-4 : ℤ) = 1 := by simp +example : I ^ (-5 : ℤ) = -I := by simp +example : I ^ (-6 : ℤ) = -1 := by simp +example : I ^ (-7 : ℤ) = I := by simp +example : I ^ (-100 : ℤ) = 1 := by simp + +/-- error: `simp` made no progress -/ +#guard_msgs in +example {n : ℕ} : I ^ n = I ^ (n % 4) := by simp + +-- the appropriate simp only sequence can reduce I ^ n for literal nats n +example : I ^ 5 = I := by simp only [I_pow_eq_pow_mod', Nat.reduceMod, pow_one] +example : I ^ 6 = -1 := by simp only [I_pow_eq_pow_mod', Nat.reduceMod, I_sq] +example : I ^ 7 = -I := by simp only [I_pow_eq_pow_mod', Nat.reduceMod, I_pow_three] +example : I ^ 8 = 1 := by simp only [I_pow_eq_pow_mod', Nat.reduceMod, pow_zero] + +-- the appropriate simp only sequence can reduce I ^ n for literal ints n +example : I ^ (5 : ℤ) = I := by + simp only [zpow_ofNat, I_pow_eq_pow_mod', Nat.reduceMod, pow_one] + +-- the appropriate simp only sequence can reduce I ^ (-n) for literal nats n +example : I ^ (-5 : ℤ) = -I := by + simp only [Int.reduceNeg, zpow_neg, zpow_ofNat, I_pow_eq_pow_mod', Nat.reduceMod, pow_one, inv_I] diff --git a/MathlibTest/Tactic/Abel.lean b/MathlibTest/Tactic/Abel.lean index 643483f1a39..ce9b97245c9 100644 --- a/MathlibTest/Tactic/Abel.lean +++ b/MathlibTest/Tactic/Abel.lean @@ -176,7 +176,6 @@ h : R (2 • myId x) (2 • myId x) ⊢ True -/ #guard_msgs (trace) in -set_option pp.mvars.anonymous false in example (x : ℤ) (R : ℤ → ℤ → Prop) [Std.Refl R] : True := by have h : R (myId x + x) (x + myId x) := refl _ abel_nf at h diff --git a/MathlibTest/Tactic/Check.lean b/MathlibTest/Tactic/Check.lean index 49c0e03800c..7c83b034b54 100644 --- a/MathlibTest/Tactic/Check.lean +++ b/MathlibTest/Tactic/Check.lean @@ -1,6 +1,5 @@ import Mathlib.Tactic.Check -set_option pp.mvars.anonymous false set_option linter.unusedTactic false set_option linter.unusedVariables false diff --git a/MathlibTest/Tactic/GRewrite.lean b/MathlibTest/Tactic/GRewrite.lean index cb7404bd831..db429d3cbca 100644 --- a/MathlibTest/Tactic/GRewrite.lean +++ b/MathlibTest/Tactic/GRewrite.lean @@ -114,7 +114,7 @@ example (h₁ : W ⊂ Y) (h₂ : X ⊂ (W ∪ Z)) : X ⊂ (Y ∪ Z) := by -- Binder names are preserved: /-- -trace: α : Type ?u.3 +trace: α : Type _ X Y Z W : Set α a b : ℕ h : a < b @@ -130,7 +130,7 @@ example {a b : Nat} (h : a < b) (f : Nat → Nat) (hf : ∀ i, 0 ≤ f i) : rfl /-- -trace: α : Type ?u.3 +trace: α : Type _ X Y Z W : Set α ⊢ ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), max a b ≤ max a b -/ diff --git a/MathlibTest/Util/PrintSorries.lean b/MathlibTest/Util/PrintSorries.lean index a760b777a1b..8520023e1c8 100644 --- a/MathlibTest/Util/PrintSorries.lean +++ b/MathlibTest/Util/PrintSorries.lean @@ -1,7 +1,5 @@ import Mathlib.Util.PrintSorries -set_option pp.mvars.anonymous false - /-! Direct use of `sorry` -/ diff --git a/MathlibTest/Widget/Conv.lean b/MathlibTest/Widget/Conv.lean index 0a3c1f34fa3..1c065f5fc4a 100644 --- a/MathlibTest/Widget/Conv.lean +++ b/MathlibTest/Widget/Conv.lean @@ -152,7 +152,6 @@ example : 1 = Nat.log2 4 → False := by test "/0/1/1" exact test_sorry -set_option pp.mvars.anonymous false in /-- info: `conv?` would output: conv => diff --git a/MathlibTest/matrix.lean b/MathlibTest/matrix.lean index 75a20346778..59a4cd34833 100644 --- a/MathlibTest/matrix.lean +++ b/MathlibTest/matrix.lean @@ -7,7 +7,8 @@ import Mathlib.LinearAlgebra.Matrix.Determinant.Basic import Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs import Mathlib.LinearAlgebra.Matrix.Notation import Mathlib.RingTheory.Polynomial.Basic -import Mathlib.Tactic.Determinant.Bird +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.NormDet import Qq open Qq @@ -190,65 +191,63 @@ example (ι : Type*) [Inhabited ι] : Matrix.replicateCol ι (fun (_ : Fin 3) => simp_all rfl -section BirdDet - -open BirdDet +section NormDet variable {R : Type*} [CommRing R] -example : birdDet 0 #[] = (1 : ℤ) := by +example : Matrix.det !![] = (1 : ℤ) := by eval_det -example : birdDet 1 #[-1] = -1 := by +example : Matrix.det !![-1] = -1 := by eval_det -example : birdDet 2 #[1, 2, 3, 4] = -2 := by +example : Matrix.det !![1, 2; 3, 4] = -2 := by eval_det -example : birdDet 2 (let A := #[1, 2, 3, 4]; A) = -2 := by +example : Matrix.det (let A := !![1, 2; 3, 4]; A) = -2 := by eval_det -example (a b c d : R) : - birdDet 2 #[a, b, c, d] = a * d - b * c := by +example (a b c d : R) : Matrix.det !![a, b; c, d] = a * d - b * c := by eval_det ring -example (a b c d : R) : - birdDet 2 #[a, b, c, d] = a * d - b * c := by +example (a b c d : R) : Matrix.det !![a, b; c, d] = a * d - b * c := by simp only [norm_det] ring -example : birdDet 2 #[1, 2, 2, 4] + birdDet 2 #[2, 3, 4, 5] = -2 := by - simp only [norm_det] +example : Matrix.det !![1, 2; 2, 4] + Matrix.det !![2, 3; 4, 5] = -2 := by + eval_det norm_num -example : birdDet 2 #[birdDet 2 #[2, 3, 4, 5], 2, 2, 4] = -12 := by - simp only [norm_det] +example : Matrix.det !![Matrix.det !![2, 3; 4, 5], 2; 2, 4] = -12 := by + eval_det -example : - birdDet 8 - #[ 2, 0, -1, 0, 0, 0, 0, 0, - 0, 2, 0, -1, 0, 0, 0, 0, - -1, 0, 2, -1, 0, 0, 0, 0, - 0, -1, -1, 2, -1, 0, 0, 0, - 0, 0, 0, -1, 2, -1, 0, 0, - 0, 0, 0, 0, -1, 2, -1, 0, - 0, 0, 0, 0, 0, -1, 2, -1, - 0, 0, 0, 0, 0, 0, -1, 2] = 1 := by - simp only [norm_det] +example : Matrix.det + !![ 2, 0, -1, 0, 0, 0, 0, 0; + 0, 2, 0, -1, 0, 0, 0, 0; + -1, 0, 2, -1, 0, 0, 0, 0; + 0, -1, -1, 2, -1, 0, 0, 0; + 0, 0, 0, -1, 2, -1, 0, 0; + 0, 0, 0, 0, -1, 2, -1, 0; + 0, 0, 0, 0, 0, -1, 2, -1; + 0, 0, 0, 0, 0, 0, -1, 2] = 1 := by + eval_det open MvPolynomial in -lemma test_case_11 : - birdDet (R := MvPolynomial (Fin 3) R) - 3 - #[1 , X 0, (X 0) ^ 2, - 1 , X 1, (X 1) ^ 2, - 1 , X 2, (X 2) ^ 2] = (X 0 - X 1) * (X 1 - X 2) * (X 2 - X 0) := by - simp only [norm_det] +example : Matrix.det (R := MvPolynomial (Fin 3) R) + !![1 , X 0, (X 0) ^ 2; + 1 , X 1, (X 1) ^ 2; + 1 , X 2, (X 2) ^ 2] = (X 0 - X 1) * (X 1 - X 2) * (X 2 - X 0) := by + eval_det ring -end BirdDet +example {K : Type*} [Field K] (x i j k : K) (hx : x ≠ 0) : Matrix.det + !![x ^ 3, 0, 0; i, 1 / x, 0; j, k, 1 / x ^ 2] = 1 := by + eval_det + field_simp [hx] + +end NormDet end Matrix diff --git a/MathlibTest/superscript.lean b/MathlibTest/superscript.lean index 479a7602b86..9ccaae63acb 100644 --- a/MathlibTest/superscript.lean +++ b/MathlibTest/superscript.lean @@ -194,7 +194,6 @@ open Nat' (γ) in #guard_msgs in #check testsub(ᵧ ₙ) /- The delaborator should reject metavariables. -/ -set_option pp.mvars.anonymous false in /-- info: checkSubscript ?_ : Unit -/ #guard_msgs in #check checkSubscript ?_ @@ -229,7 +228,6 @@ open Nat' (γ) in #guard_msgs in #check testsup(ᵞ ⁿ) /- The delaborator should reject metavariables. -/ -set_option pp.mvars false in /-- info: checkSuperscript ?_ : Unit -/ #guard_msgs in #check checkSuperscript ?_ diff --git a/lakefile.lean b/lakefile.lean index bcdf13405f0..2afc2a7a303 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -39,7 +39,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[ ] /-- These options are passed as `leanOptions` to building mathlib, as well as the -`Archive` and `Counterexamples`. (`tests` omits the first two options.) -/ +`Archive` and `Counterexamples`. -/ abbrev mathlibLeanOptions := #[ ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` ⟨`autoImplicit, false⟩, @@ -47,6 +47,12 @@ abbrev mathlibLeanOptions := #[ ] ++ -- options that are used in `lake build` mathlibOnlyLinters.map fun s ↦ { s with name := `weak ++ s.name } +/-- These options are passed as `leanOptions` when building `MathlibTest`. We don't use the typical +mathlib options in order to simulate the default downstream environment. -/ +abbrev mathlibTestOptions : Array LeanOption := #[ + ⟨`pp.mvars.anonymous, false⟩ -- test stability: pretty-print `?m.37` as `?_` + ] + package mathlib where testDriver := "MathlibTest" lintDriver := "batteries/runLinter" @@ -79,6 +85,7 @@ lean_lib Cache where lean_lib MathlibTest where globs := #[`MathlibTest.+] + leanOptions := mathlibTestOptions lean_lib Archive where leanOptions := mathlibLeanOptions diff --git a/scripts/autolabel.lean b/scripts/autolabel.lean index 20ae2508666..e9b4031194f 100644 --- a/scripts/autolabel.lean +++ b/scripts/autolabel.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jon Eugster, Damiano Testa -/ import Lean.Elab.Command +import Cli.Basic /-! # Automatic labelling of PRs @@ -27,9 +28,7 @@ needs to be updated here if necessary: files have been modified and then finds all labels which should be added based on these changes. These are printed for testing purposes. -`lake exe autolabel [NUMBER]` will further try to add the applicable labels -to the PR specified. This requires the **GitHub CLI** `gh` to be installed! -Example: `lake exe autolabel 10402` for PR https://github.com/leanprover-community/mathlib4/pull/10402. +See `lake exe autolabel --help` for all arguments available. The script can add up to `MAX_LABELS` labels (defined below). If more than `MAX_LABELS` labels would be applicable, nothing happens. @@ -381,29 +380,24 @@ Note: `file` is duplicated below so that it is also visible in the plain text ou def githubAnnotation (type file title message : String) : String := s!"::{type} file={file},title={title}::{file}: {message}" -end AutoLabel - -open IO AutoLabel in - -/-- `args` is expected to have length 0 or 1, where the first argument is the PR number. - -If a PR number is provided, the script requires GitHub CLI `gh` to be installed in order -to add the label to the PR. - -## Exit codes: - -- `0`: success -- `1`: invalid arguments provided -- `2`: invalid labels defined -- `3`: ~labels do not cover all of `Mathlib/`~ (unused; only emitting warning) --/ -unsafe def main (args : List String): IO UInt32 := do - if args.length > 1 then - println s!"::error:: autolabel: invalid number of arguments ({args.length}), \ - expected at most 1. Please run without arguments or provide the target PR's \ - number as a single argument!" - return 1 - let prNumber? := args[0]? +/-- Available implementations about how to communicate with Github -/ +inductive GithubInteraction where +/-- no interaction with github -/ +| none +/-- use `gh` -/ +| gh (pr : Nat) +/-- use `curl` with an access token -/ +| curl (pr : Nat) (token : String) + +open IO in +def autoLabelCli (args : Cli.Parsed) : IO UInt32 := do + let force := args.hasFlag "force" + let tool: GithubInteraction := + match ((args.flag? "pr").map (·.as! Nat)), args.hasFlag "gh", args.flag? "curl" with + | none, _, _ => .none + | some _, false, none => .none + | some pr, true, _ => .gh pr + | some pr, false, some curlFlag => .curl pr (curlFlag.as! String) -- test: validate that all paths in `mathlibLabelData` actually exist let mut valid := true @@ -441,41 +435,81 @@ unsafe def main (args : List String): IO UInt32 := do -- return 3 -- get the modified files - println "Computing 'git diff --name-only origin/master...HEAD'" let gitDiff ← IO.Process.run { cmd := "git", args := #["diff", "--name-only", "origin/master...HEAD"] } - println s!"---\n{gitDiff}\n---" let modifiedFiles : Array FilePath := (gitDiff.splitOn "\n").toArray.map (⟨·⟩) -- find labels covering the modified files - let labels := dropDependentLabels <| getMatchingLabels modifiedFiles - println s!"::notice::Applicable labels: {labels}" + let newLabels := dropDependentLabels <| getMatchingLabels modifiedFiles + println s!"::notice::Applicable labels: {newLabels}" - match labels with + match newLabels with | #[] => - println s!"::warning::no label to add" + println s!"::warning::no labels to add" | newLabels => - match prNumber? with - | some n => - if newLabels.size > MAX_LABELS then - println s!"::notice::not adding more than {MAX_LABELS} labels: {newLabels}" - return 0 - let labelsPresent ← IO.Process.run { + if newLabels.size > MAX_LABELS then + println s!"::notice::not adding more than {MAX_LABELS} labels: {newLabels}" + return 0 + match tool with + | .gh prNr => + let labelsPresent ← if force then pure "" else IO.Process.run { cmd := "gh" - args := #["pr", "view", n, "--json", "labels", "--jq", ".labels .[] .name"]} - let labels := labelsPresent.splitToList (· == '\n') + args := #["pr", "view", s!"{prNr}", "--json", "labels", "--jq", ".labels .[] .name"]} + let existingLabels := labelsPresent.splitToList (· == '\n') let autoLabels := mathlibLabels.map (·.toString) - match labels.filter autoLabels.contains with - | [] => -- if the PR does not have a label that this script could add, then we add a label + match existingLabels.filter autoLabels.contains with + | [] => let _ ← IO.Process.run { cmd := "gh", - args := #["pr", "edit", n, "--add-label", s!"\"{",".intercalate <| newLabels.toList.map (·.toString)}\""] } - println s!"::notice::added labels: {newLabels}" - | t_labels_already_present => - println s!"::notice::Did not add labels '{newLabels}', \ - since {t_labels_already_present} were already present" - | none => - println s!"::warning::no PR-number provided, not adding labels. \ - (call `lake exe autolabel 150602` to add the labels to PR `150602`)" + args := #["pr", "edit", s!"{prNr}", "--add-label", ",".intercalate <| newLabels.toList.map (·.toString)] } + println s!"::notice::added label: {newLabels}" + | t_labels_already_present => + println s!"::notice::did not add labels '{newLabels}', since {t_labels_already_present} \ + were already present" + | .curl prNr token => + -- TODO: take existing labels on the PR into account + let _ ← IO.Process.run { + cmd := "curl", + args := #[ + "--request", "POST", + "--header", "Accept: application/vnd.github+json", + "--header", s!"authorization: Bearer {token}", + "--header", "X-GitHub-Api-Version: 2022-11-28", + "--url", s!"https://api.github.com/repos/leanprover-community/mathlib4/issues/{prNr}/labels", + "--data", "{\"labels\":[\"" ++ s!"{"\",\"".intercalate <| newLabels.toList.map (·.toString)}" ++ "\"]}" + ]} + println s!"::notice::added label: {newLabels}" + | .none => + println s!"::notice::github interaction disabled, not adding labels." return 0 + +end AutoLabel + +/-- Setting up command line options and help text for `lake exe autolabel` -/ +def autolabel : Cli.Cmd := `[Cli| + autolabel VIA AutoLabel.autoLabelCli; ["0.1.0"] + " + Determine a list of applicable mathlib labels comparing current changes to `origin/master`. + + This tool is mathlib-specific and has no application in downstream projects. + " + FLAGS: + "pr" : Nat; "the mathlib PR number. Must be combined with `--gh` or `--curl`." + "gh"; "apply label(s) using `gh`. Usage: `lake exe autolabel --pr 20156 --gh`" + "curl" : String; "apply label(s) using `curl`. \ + Usage: `lake exe autolabel --pr 20156 --curl `. \ + (currently, this implies `--force`)" + "force"; "apply labels even if there are already labels on the PR." +] + +/-- lake exe autolabel + +## Exit codes: + +- `0`: success +- `2`: invalid labels defined +- `3`: ~labels do not cover all of `Mathlib/`~ (unused; only emitting warning) +-/ +public def main (args : List String) : IO UInt32 := + autolabel.validate args diff --git a/upstream_sha b/upstream_sha index 7342ae1e3e1..1aee8ca2f4e 100644 --- a/upstream_sha +++ b/upstream_sha @@ -1 +1 @@ -6c5a9081e9b704f0d366214e1fd5e68e1538a4b2 +3bc2a1801c2416549ba5ba0b3f5728a28b87e7d9