diff --git a/Mathlib.lean b/Mathlib.lean index 60a6904ec63fee..4d002f3a687f93 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2268,7 +2268,6 @@ import Mathlib.CategoryTheory.SmallObject.Iteration.Basic import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty -import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom import Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting import Mathlib.CategoryTheory.SmallObject.WellOrderInductionData import Mathlib.CategoryTheory.Square diff --git a/Mathlib/Algebra/Free.lean b/Mathlib/Algebra/Free.lean index 0fbfaa9678903a..50106b3d672c7d 100644 --- a/Mathlib/Algebra/Free.lean +++ b/Mathlib/Algebra/Free.lean @@ -61,9 +61,6 @@ instance [Inhabited α] : Inhabited (FreeMagma α) := ⟨of default⟩ @[to_additive] instance : Mul (FreeMagma α) := ⟨FreeMagma.mul⟩ --- Porting note: invalid attribute 'match_pattern', declaration is in an imported module --- attribute [match_pattern] Mul.mul - @[to_additive (attr := simp)] theorem mul_eq (x y : FreeMagma α) : mul x y = x * y := rfl @@ -80,12 +77,10 @@ theorem hom_ext {β : Type v} [Mul β] {f g : FreeMagma α →ₙ* β} (h : f end FreeMagma -#adaptation_note /-- nightly-2024-02-25 -we need to write `mul x y` in the second pattern, instead of `x * y`. --/ /-- Lifts a function `α → β` to a magma homomorphism `FreeMagma α → β` given a magma `β`. -/ def FreeMagma.liftAux {α : Type u} {β : Type v} [Mul β] (f : α → β) : FreeMagma α → β | FreeMagma.of x => f x - | mul x y => liftAux f x * liftAux f y + | x * y => liftAux f x * liftAux f y /-- Lifts a function `α → β` to an additive magma homomorphism `FreeAddMagma α → β` given an additive magma `β`. -/ @@ -185,13 +180,11 @@ end Category end FreeMagma -#adaptation_note /-- nightly-2024-02-25 -we need to write `mul x y` in the second pattern, instead of `x * y`. -/ /-- `FreeMagma` is traversable. -/ protected def FreeMagma.traverse {m : Type u → Type u} [Applicative m] {α β : Type u} (F : α → m β) : FreeMagma α → m (FreeMagma β) | FreeMagma.of x => FreeMagma.of <$> F x - | mul x y => (· * ·) <$> x.traverse F <*> y.traverse F + | x * y => (· * ·) <$> x.traverse F <*> y.traverse F /-- `FreeAddMagma` is traversable. -/ protected def FreeAddMagma.traverse {m : Type u → Type u} [Applicative m] {α β : Type u} @@ -262,12 +255,10 @@ end Category end FreeMagma -#adaptation_note /-- nightly-2024-02-25 -we need to write `mul x y` in the second pattern, instead of `x * y`. -/ /-- Representation of an element of a free magma. -/ protected def FreeMagma.repr {α : Type u} [Repr α] : FreeMagma α → Lean.Format | FreeMagma.of x => repr x - | mul x y => "( " ++ x.repr ++ " * " ++ y.repr ++ " )" + | x * y => "( " ++ x.repr ++ " * " ++ y.repr ++ " )" /-- Representation of an element of a free additive magma. -/ protected def FreeAddMagma.repr {α : Type u} [Repr α] : FreeAddMagma α → Lean.Format @@ -279,12 +270,10 @@ attribute [to_additive existing] FreeMagma.repr @[to_additive] instance {α : Type u} [Repr α] : Repr (FreeMagma α) := ⟨fun o _ => FreeMagma.repr o⟩ -#adaptation_note /-- nightly-2024-02-25 -we need to write `mul x y` in the second pattern, instead of `x * y`. -/ /-- Length of an element of a free magma. -/ def FreeMagma.length {α : Type u} : FreeMagma α → ℕ | FreeMagma.of _x => 1 - | mul x y => x.length + y.length + | x * y => x.length + y.length /-- Length of an element of a free additive magma. -/ def FreeAddMagma.length {α : Type u} : FreeAddMagma α → ℕ diff --git a/Mathlib/Algebra/LinearRecurrence.lean b/Mathlib/Algebra/LinearRecurrence.lean index b9fe57a324105f..cec0da0476a215 100644 --- a/Mathlib/Algebra/LinearRecurrence.lean +++ b/Mathlib/Algebra/LinearRecurrence.lean @@ -92,7 +92,8 @@ theorem eq_mk_of_is_sol_of_eq_init {u : ℕ → α} {init : Fin E.order → α} rw [mkSol] split_ifs with h' · exact mod_cast heq ⟨n, h'⟩ - · rw [← tsub_add_cancel_of_le (le_of_not_lt h'), h (n - E.order)] + · dsimp only + rw [← tsub_add_cancel_of_le (le_of_not_lt h'), h (n - E.order)] congr with k have : n - E.order + k < n := by omega rw [eq_mk_of_is_sol_of_eq_init h heq (n - E.order + k)] diff --git a/Mathlib/Algebra/TrivSqZeroExt.lean b/Mathlib/Algebra/TrivSqZeroExt.lean index 310e8819885872..cf3a609ed57306 100644 --- a/Mathlib/Algebra/TrivSqZeroExt.lean +++ b/Mathlib/Algebra/TrivSqZeroExt.lean @@ -640,12 +640,12 @@ $r_0\cdots r_{i-1}m_ir_{i+1}\cdots r_n$. -/ theorem snd_list_prod [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (l : List (tsze R M)) : l.prod.snd = - (l.enum.map fun x : ℕ × tsze R M => - ((l.map fst).take x.1).prod •> x.snd.snd <• ((l.map fst).drop x.1.succ).prod).sum := by + (l.zipIdx.map fun x : tsze R M × ℕ => + ((l.map fst).take x.2).prod •> x.fst.snd <• ((l.map fst).drop x.2.succ).prod).sum := by induction l with | nil => simp | cons x xs ih => - rw [List.enum_cons, ← List.map_fst_add_enum_eq_enumFrom] + rw [List.zipIdx_cons'] simp_rw [List.map_cons, List.map_map, Function.comp_def, Prod.map_snd, Prod.map_fst, id, List.take_zero, List.take_succ_cons, List.prod_nil, List.prod_cons, snd_mul, one_smul, List.drop, mul_smul, List.sum_cons, fst_list_prod, ih, List.smul_sum, List.map_map, diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean index dea028ad9f7471..ba83a3ede5f6d0 100644 --- a/Mathlib/Analysis/Analytic/Composition.lean +++ b/Mathlib/Analysis/Analytic/Composition.lean @@ -550,7 +550,7 @@ def compChangeOfVariables (m M N : ℕ) (i : Σ n, Fin n → ℕ) (hi : i ∈ co rw [mem_compPartialSumSource_iff] at hi refine ⟨∑ j, f j, ofFn fun a => f a, fun hi' => ?_, by simp [sum_ofFn]⟩ rename_i i - obtain ⟨j, rfl⟩ : ∃ j : Fin n, f j = i := by rwa [mem_ofFn, Set.mem_range] at hi' + obtain ⟨j, rfl⟩ : ∃ j : Fin n, f j = i := by rwa [mem_ofFn', Set.mem_range] at hi' exact (hi.2 j).1 @[simp] diff --git a/Mathlib/CategoryTheory/SmallObject/Construction.lean b/Mathlib/CategoryTheory/SmallObject/Construction.lean index 4a30175a01a6cd..333e74170d002c 100644 --- a/Mathlib/CategoryTheory/SmallObject/Construction.lean +++ b/Mathlib/CategoryTheory/SmallObject/Construction.lean @@ -9,10 +9,10 @@ import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback /-! # Construction for the small object argument -Given a family of morphisms `f i : A i ⟶ B i` in a category `C` -and an object `S : C`, we define a functor -`SmallObject.functor f S : Over S ⥤ Over S` which sends -an object given by `πX : X ⟶ S` to the pushout `functorObj f πX`: +Given a family of morphisms `f i : A i ⟶ B i` in a category `C`, +we define a functor +`SmallObject.functor f : Arrow S ⥤ Arrow S` which sends +an object given by arrow `πX : X ⟶ S` to the pushout `functorObj f πX`: ``` ∐ functorObjSrcFamily f πX ⟶ X @@ -20,7 +20,7 @@ an object given by `πX : X ⟶ S` to the pushout `functorObj f πX`: | | v v -∐ functorObjTgtFamily f πX ⟶ functorObj f S πX +∐ functorObjTgtFamily f πX ⟶ functorObj f πX ``` where the morphism on the left is a coproduct (of copies of maps `f i`) indexed by a type `FunctorObjIndex f πX` which parametrizes the @@ -33,8 +33,8 @@ A i ⟶ X B i ⟶ S ``` -The morphism `ιFunctorObj f S πX : X ⟶ functorObj f πX` is part of -a natural transformation `SmallObject.ε f S : 𝟭 (Over S) ⟶ functor f S`. +The morphism `ιFunctorObj f πX : X ⟶ functorObj f πX` is part of +a natural transformation `SmallObject.ε f : 𝟭 (Arrow C) ⟶ functor f S`. The main idea in this construction is that for any commutative square as above, there may not exist a lifting `B i ⟶ X`, but the construction provides a tautological morphism `B i ⟶ functorObj f πX` @@ -62,7 +62,7 @@ variable {C : Type u} [Category.{v} C] {I : Type w} {A B : I → C} (f : ∀ i, section -variable {S : C} {X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) +variable {S X : C} (πX : X ⟶ S) /-- Given a family of morphisms `f i : A i ⟶ B i` and a morphism `πX : X ⟶ S`, this type parametrizes the commutative squares with a morphism `f i` on the left @@ -79,7 +79,6 @@ structure FunctorObjIndex where attribute [reassoc (attr := simp)] FunctorObjIndex.w variable [HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] - [HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] /-- The family of objects `A x.i` parametrized by `x : FunctorObjIndex f πX`. -/ abbrev functorObjSrcFamily (x : FunctorObjIndex f πX) : C := A x.i @@ -101,10 +100,9 @@ noncomputable abbrev functorObjLeft : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX := Limits.Sigma.map (functorObjLeftFamily f πX) -section variable [HasPushout (functorObjTop f πX) (functorObjLeft f πX)] -/-- The functor `SmallObject.functor f S : Over S ⥤ Over S` that is part of +/-- The functor `SmallObject.functor f : Arrow C ⥤ Arrow C` that is part of the small object argument for a family of morphisms `f`, on an object given as a morphism `πX : X ⟶ S`. -/ noncomputable abbrev functorObj : C := @@ -141,79 +139,92 @@ lemma ρFunctorObj_π : ρFunctorObj f πX ≫ πFunctorObj f πX = π'FunctorOb lemma ιFunctorObj_πFunctorObj : ιFunctorObj f πX ≫ πFunctorObj f πX = πX := by simp [ιFunctorObj, πFunctorObj] -/-- The canonical morphism `∐ (functorObjSrcFamily f πX) ⟶ ∐ (functorObjSrcFamily f πY)` -induced by a morphism in `φ : X ⟶ Y` such that `φ ≫ πX = πY`. -/ -noncomputable def functorMapSrc (hφ : φ ≫ πY = πX) : - ∐ (functorObjSrcFamily f πX) ⟶ ∐ functorObjSrcFamily f πY := - Sigma.map' (fun x => FunctorObjIndex.mk x.i (x.t ≫ φ) x.b (by simp [hφ])) (fun _ => 𝟙 _) +section -end +variable {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) + [HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] + [HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] -variable (hφ : φ ≫ πY = πX) +/-- The canonical morphism `∐ (functorObjSrcFamily f πX) ⟶ ∐ (functorObjSrcFamily f πY)` +induced by a morphism `Arrow.mk πX ⟶ Arrow.mk πY`. -/ +noncomputable def functorMapSrc : + ∐ (functorObjSrcFamily f πX) ⟶ ∐ functorObjSrcFamily f πY := + Sigma.map' (fun x => FunctorObjIndex.mk x.i (x.t ≫ τ.left) (x.b ≫ τ.right) (by simp)) + (fun _ => 𝟙 _) @[reassoc] lemma ι_functorMapSrc (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : t ≫ πX = f i ≫ b) - (t' : A i ⟶ Y) (fac : t ≫ φ = t') : - Sigma.ι _ (FunctorObjIndex.mk i t b w) ≫ functorMapSrc f πX πY φ hφ = + (b' : B i ⟶ T) (hb' : b ≫ τ.right = b') + (t' : A i ⟶ Y) (ht' : t ≫ τ.left = t') : + Sigma.ι _ (FunctorObjIndex.mk i t b w) ≫ functorMapSrc f τ = Sigma.ι (functorObjSrcFamily f πY) - (FunctorObjIndex.mk i t' b (by rw [← w, ← fac, assoc, hφ])) := by - subst fac + (FunctorObjIndex.mk i t' b' (by + have := τ.w + dsimp at this + rw [← hb', ← reassoc_of% w, ← ht', assoc, this])) := by + subst hb' ht' simp [functorMapSrc] @[reassoc (attr := simp)] lemma functorMapSrc_functorObjTop : - functorMapSrc f πX πY φ hφ ≫ functorObjTop f πY = functorObjTop f πX ≫ φ := by + functorMapSrc f τ ≫ functorObjTop f πY = functorObjTop f πX ≫ τ.left := by ext ⟨i, t, b, w⟩ - simp [ι_functorMapSrc_assoc f πX πY φ hφ i t b w _ rfl] + simp [ι_functorMapSrc_assoc f τ i t b w _ rfl] /-- The canonical morphism `∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY` -induced by a morphism in `φ : X ⟶ Y` such that `φ ≫ πX = πY`. -/ -noncomputable def functorMapTgt (hφ : φ ≫ πY = πX) : +induced by a morphism `Arrow.mk πX ⟶ Arrow.mk πY`. -/ +noncomputable def functorMapTgt : ∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY := - Sigma.map' (fun x => FunctorObjIndex.mk x.i (x.t ≫ φ) x.b (by simp [hφ])) (fun _ => 𝟙 _) + Sigma.map' (fun x => FunctorObjIndex.mk x.i (x.t ≫ τ.left) (x.b ≫ τ.right) (by simp)) + (fun _ => 𝟙 _) @[reassoc] lemma ι_functorMapTgt (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : t ≫ πX = f i ≫ b) - (t' : A i ⟶ Y) (fac : t ≫ φ = t') : - Sigma.ι _ (FunctorObjIndex.mk i t b w) ≫ functorMapTgt f πX πY φ hφ = + (b' : B i ⟶ T) (hb' : b ≫ τ.right = b') + (t' : A i ⟶ Y) (ht' : t ≫ τ.left = t') : + Sigma.ι _ (FunctorObjIndex.mk i t b w) ≫ functorMapTgt f τ = Sigma.ι (functorObjTgtFamily f πY) - (FunctorObjIndex.mk i t' b (by rw [← w, ← fac, assoc, hφ])) := by - subst fac + (FunctorObjIndex.mk i t' b' (by + have := τ.w + dsimp at this + rw [← hb', ← reassoc_of% w, ← ht', assoc, this])) := by + subst hb' ht' simp [functorMapTgt] lemma functorMap_comm : - functorObjLeft f πX ≫ functorMapTgt f πX πY φ hφ = - functorMapSrc f πX πY φ hφ ≫ functorObjLeft f πY := by + functorObjLeft f πX ≫ functorMapTgt f τ = + functorMapSrc f τ ≫ functorObjLeft f πY := by ext ⟨i, t, b, w⟩ simp only [ι_colimMap_assoc, Discrete.natTrans_app, ι_colimMap, - ι_functorMapTgt f πX πY φ hφ i t b w _ rfl, - ι_functorMapSrc_assoc f πX πY φ hφ i t b w _ rfl] + ι_functorMapTgt f τ i t b w _ rfl, + ι_functorMapSrc_assoc f τ i t b w _ rfl] variable [HasPushout (functorObjTop f πX) (functorObjLeft f πX)] [HasPushout (functorObjTop f πY) (functorObjLeft f πY)] -/-- The functor `SmallObject.functor f S : Over S ⥤ Over S` that is part of +/-- The functor `SmallObject.functor f S : Arrow S ⥤ Arrow S` that is part of the small object argument for a family of morphisms `f`, on morphisms. -/ noncomputable def functorMap : functorObj f πX ⟶ functorObj f πY := - pushout.map _ _ _ _ φ (functorMapTgt f πX πY φ hφ) (functorMapSrc f πX πY φ hφ) (by simp) - (functorMap_comm f πX πY φ hφ) + pushout.map _ _ _ _ τ.left (functorMapTgt f τ) (functorMapSrc f τ) (by simp) + (functorMap_comm f τ) @[reassoc (attr := simp)] -lemma functorMap_π : functorMap f πX πY φ hφ ≫ πFunctorObj f πY = πFunctorObj f πX := by +lemma functorMap_π : functorMap f τ ≫ πFunctorObj f πY = πFunctorObj f πX ≫ τ.right := by ext ⟨i, t, b, w⟩ - · simp [functorMap, hφ] - · simp [functorMap, ι_functorMapTgt_assoc f πX πY φ hφ i t b w _ rfl] + · simp [functorMap] + · simp [functorMap, ι_functorMapTgt_assoc f τ i t b w _ rfl] variable (X) in @[simp] -lemma functorMap_id : functorMap f πX πX (𝟙 X) (by simp) = 𝟙 _ := by +lemma functorMap_id : functorMap f (𝟙 (Arrow.mk πX)) = 𝟙 _ := by ext ⟨i, t, b, w⟩ · simp [functorMap] - · simp [functorMap, ι_functorMapTgt_assoc f πX πX (𝟙 X) (by simp) i t b w t (by simp)] + · simp [functorMap, + ι_functorMapTgt_assoc f (𝟙 (Arrow.mk πX)) i t b w b (by simp) t (by simp)] @[reassoc (attr := simp)] lemma ιFunctorObj_naturality : - ιFunctorObj f πX ≫ functorMap f πX πY φ hφ = φ ≫ ιFunctorObj f πY := by + ιFunctorObj f πX ≫ functorMap f τ = τ.left ≫ ιFunctorObj f πY := by simp [ιFunctorObj, functorMap] lemma ιFunctorObj_extension {i : I} (t : A i ⟶ X) (b : B i ⟶ S) @@ -225,31 +236,39 @@ lemma ιFunctorObj_extension {i : I} (t : A i ⟶ X) (b : B i ⟶ S) end -variable (S : C) [HasPushouts C] - [∀ {X : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] +variable [HasPushouts C] + [∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] -/-- The functor `Over S ⥤ Over S` that is constructed in order to apply the small +/-- The functor `Arrow C ⥤ Arrow C` that is constructed in order to apply the small object argument to a family of morphisms `f i : A i ⟶ B i`, see the introduction of the file `Mathlib.CategoryTheory.SmallObject.Construction` -/ @[simps! obj map] -noncomputable def functor : Over S ⥤ Over S where - obj π := Over.mk (πFunctorObj f π.hom) - map {π₁ π₂} φ := Over.homMk (functorMap f π₁.hom π₂.hom φ.left (Over.w φ)) - map_id _ := by ext; dsimp; simp - map_comp {π₁ π₂ π₃} φ φ' := by - ext1 - dsimp - ext ⟨i, t, b, w⟩ - · simp - · simp [functorMap, ι_functorMapTgt_assoc f π₁.hom π₂.hom φ.left (Over.w φ) i t b w _ rfl, - ι_functorMapTgt_assoc f π₁.hom π₃.hom (φ.left ≫ φ'.left) (Over.w (φ ≫ φ')) i t b w _ rfl, - ι_functorMapTgt_assoc f π₂.hom π₃.hom (φ'.left) (Over.w φ') i (t ≫ φ.left) b - (by simp [w]) (t ≫ φ.left ≫ φ'.left) (by simp)] - -/-- The canonical natural transformation `𝟭 (Over S) ⟶ functor f S`. -/ -@[simps! app] -noncomputable def ε : 𝟭 (Over S) ⟶ functor f S where - app w := Over.homMk (ιFunctorObj f w.hom) +noncomputable def functor : Arrow C ⥤ Arrow C where + obj π := Arrow.mk (πFunctorObj f π.hom) + map {π₁ π₂} τ := Arrow.homMk (functorMap f τ) τ.right + map_id g := by + ext + · apply functorMap_id + · dsimp + map_comp {π₁ π₂ π₃} τ τ' := by + ext + · dsimp + simp [functorMap] + ext ⟨i, t, b, w⟩ + · simp + · simp [ι_functorMapTgt_assoc f τ i t b w _ rfl _ rfl, + ι_functorMapTgt_assoc f (τ ≫ τ') i t b w _ rfl _ rfl, + ι_functorMapTgt_assoc f τ' i (t ≫ τ.left) (b ≫ τ.right) + (by simp [reassoc_of% w]) (b ≫ τ.right ≫ τ'.right) (by simp) + (t ≫ (τ ≫ τ').left) (by simp)] + · dsimp + +/-- The canonical natural transformation `𝟭 (Arrow C) ⟶ functor f`. -/ +@[simps app] +noncomputable def ε : 𝟭 (Arrow C) ⟶ functor f where + app π := Arrow.homMk (ιFunctorObj f π.hom) (𝟙 _) + +end end SmallObject diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean index d739917e114af0..af7544acc81f57 100644 --- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean +++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean @@ -4,59 +4,84 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ import Mathlib.CategoryTheory.Category.Preorder -import Mathlib.CategoryTheory.Limits.IsLimit +import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic +import Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape +import Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg +import Mathlib.CategoryTheory.Limits.Comma import Mathlib.Order.ConditionallyCompleteLattice.Basic import Mathlib.Order.SuccPred.Limit - -/-! # Transfinite iterations of a functor - -In this file, given a functor `Φ : C ⥤ C` and a natural transformation -`ε : 𝟭 C ⟶ Φ`, we shall define the transfinite iterations of `Φ` (TODO). - -Given `j : J` where `J` is a well ordered set, we first introduce -a category `Iteration ε j`. An object in this category consists of -a functor `F : Set.Iic j ⥤ C ⥤ C` equipped with the data -which makes it the `i`th-iteration of `Φ` for all `i` such that `i ≤ j`. -Under suitable assumptions on `C`, we shall show that this category -`Iteration ε j` is equivalent to the punctual category (TODO). -In this file, we show that the there is at most one morphism between -two objects. In `SmallObject.Iteration.UniqueHom`, we shall show -that there does always exist a unique morphism between -two objects (TODO). Then, we shall show the existence of -an object (TODO). In these proofs, which are all done using -transfinite induction, we have to treat three cases separately: -* the case `j = ⊥`; -* the case `j` is a successor; -* the case `j` is a limit element. +import Mathlib.Order.Interval.Set.InitialSeg + +/-! # Transfinite iterations of a successor structure + +In this file, we introduce the structure `SuccStruct` on a category `C`. +It consists of the data of an object `X₀ : C`, a successor map `succ : C → C` +and a morphism `toSucc : X ⟶ succ X` for any `X : C`. The map `toSucc` +does not have to be natural in `X`. For any element `j : J` in a +well-ordered type `J`, we would like to define +the iteration of `Φ : SuccStruct C`, as a functor `F : J ⥤ C` +such that `F.obj ⊥ = X₀`, `F.obj j ⟶ F.obj (Order.succ j)` is `toSucc (F.obj j)` +when `j` is not maximal, and when `j` is limit, `F.obj j` should be the +colimit of the `F.obj k` for `k < j`. + +In the small object argument, we shall apply this to the iteration of +a functor `F : C ⥤ C` equipped with a natural transformation `ε : 𝟭 C ⟶ F`: +this will correspond to the case of +`SuccStruct.ofNatTrans ε : SuccStruct (C ⥤ C)`, for which `X₀ := 𝟭 C`, +`succ G := G ⋙ F` and `toSucc G : G ⟶ G ⋙ F` is given by `whiskerLeft G ε`. + +The construction of the iteration of `Φ : SuccStruct C` is done +by transfinite induction, under an assumption `HasIterationOfShape C J`. +However, for a limit element `j : J`, the definition of `F.obj j` +does not involve only the objects `F.obj i` for `i < j`, but it also +involves the maps `F.obj i₁ ⟶ F.obj i₂` for `i₁ ≤ i₂ < j`. +Then, this is not a straightforward application of definitions by +transfinite induction. In order to solve this technical difficulty, +we introduce a structure `Φ.Iteration j` for any `j : J`. This +structure contains all the expected data and properties for +all the indices that are `≤ j`. In this file, we show that +`Φ.Iteration j` is a subsingleton. The existence shall be +obtained in the file `SmallObject.Iteration.Nonempty`, and +the construction of the functor `Φ.iterationFunctor J : J ⥤ C` +and of its colimit `Φ.iteration J : C` will done in the +file `SmallObject.TransfiniteIteration`. + +The map `Φ.toSucc X : X ⟶ Φ.succ X` does not have to be natural +(and it is not in certain applications). Then, two isomorphic +objects `X` and `Y` may have non isomorphic successors. This is +the reason why we make an extensive use of equalities in +`C` and in `Arrow C` in the definitions. + +## Note + +The iteration was first introduced in mathlib by Joël Riou, using +a different approach as the one described above. After refactoring +his code, he found that the approach described above had already +been used in the pioneering formalization work in Lean 3 by +Reid Barton in 2018 towards the model category structure on +topological spaces. -/ -universe u +universe w v v' u u' namespace CategoryTheory open Category Limits -variable {C : Type*} [Category C] {Φ : C ⥤ C} (ε : 𝟭 C ⟶ Φ) {J : Type u} - -namespace Functor - -namespace Iteration +namespace SmallObject -variable [Preorder J] {j : J} (F : Set.Iic j ⥤ C) +variable {C : Type u} [Category.{v} C] {J : Type w} -/-- The map `F.obj ⟨i, _⟩ ⟶ F.obj ⟨Order.succ i, _⟩` when `F : Set.Iic j ⥤ C` -and `i : J` is such that `i < j`. -/ -noncomputable abbrev mapSucc' [SuccOrder J] (i : J) (hi : i < j) : - F.obj ⟨i, hi.le⟩ ⟶ F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ := - F.map <| homOfLE <| Subtype.mk_le_mk.2 <| Order.le_succ i +section -variable {i : J} (hi : i ≤ j) +variable [PartialOrder J] {j : J} (F : Set.Iic j ⥤ C) {i : J} (hi : i ≤ j) /-- The functor `Set.Iio i ⥤ C` obtained by "restriction" of `F : Set.Iic j ⥤ C` when `i ≤ j`. -/ def restrictionLT : Set.Iio i ⥤ C := - (monotone_inclusion_lt_le_of_le hi).functor ⋙ F + (Set.principalSegIioIicOfLE hi).monotone.functor ⋙ F + @[simp] lemma restrictionLT_obj (k : J) (hk : k < i) : @@ -68,18 +93,14 @@ lemma restrictionLT_map {k₁ k₂ : Set.Iio i} (φ : k₁ ⟶ k₂) : /-- Given `F : Set.Iic j ⥤ C`, `i : J` such that `hi : i ≤ j`, this is the cocone consisting of all maps `F.obj ⟨k, hk⟩ ⟶ F.obj ⟨i, hi⟩` for `k : J` such that `k < i`. -/ -@[simps] -def coconeOfLE : Cocone (restrictionLT F hi) where - pt := F.obj ⟨i, hi⟩ - ι := - { app := fun ⟨k, hk⟩ => F.map (homOfLE (by simpa using hk.le)) - naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ _ => by - simp [comp_id, ← Functor.map_comp, homOfLE_comp] } +@[simps!] +def coconeOfLE : Cocone (restrictionLT F hi) := + (Set.principalSegIioIicOfLE hi).cocone F /-- The functor `Set.Iic i ⥤ C` obtained by "restriction" of `F : Set.Iic j ⥤ C` when `i ≤ j`. -/ def restrictionLE : Set.Iic i ⥤ C := - (monotone_inclusion_le_le_of_le hi).functor ⋙ F + (Set.initialSegIicIicOfLE hi).monotone.functor ⋙ F @[simp] lemma restrictionLE_obj (k : J) (hk : k ≤ i) : @@ -89,187 +110,334 @@ lemma restrictionLE_obj (k : J) (hk : k ≤ i) : lemma restrictionLE_map {k₁ k₂ : Set.Iic i} (φ : k₁ ⟶ k₂) : (restrictionLE F hi).map φ = F.map (homOfLE (by simpa using leOfHom φ)) := rfl -end Iteration +end -/-- The category of `j`th iterations of a functor `Φ` equipped with a natural -transformation `ε : 𝟭 C ⟶ Φ`. An object consists of the data of all iterations -of `Φ` for `i : J` such that `i ≤ j` (this is the field `F`). Such objects are -equipped with data and properties which characterizes the iterations up to a unique -isomorphism for the three types of elements: `⊥`, successors, limit elements. -/ -structure Iteration [Preorder J] [OrderBot J] [SuccOrder J] (j : J) where - /-- The data of all `i`th iterations for `i : J` such that `i ≤ j`. -/ - F : Set.Iic j ⥤ C ⥤ C - /-- The zeroth iteration is the identity functor. -/ - isoZero : F.obj ⟨⊥, bot_le⟩ ≅ 𝟭 C - /-- The iteration on a successor element is obtained by composition of - the previous iteration with `Φ`. -/ - isoSucc (i : J) (hi : i < j) : F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ ≅ F.obj ⟨i, hi.le⟩ ⋙ Φ - /-- The natural map from an iteration to its successor is induced by `ε`. -/ - mapSucc'_eq (i : J) (hi : i < j) : - Iteration.mapSucc' F i hi = whiskerLeft _ ε ≫ (isoSucc i hi).inv - /-- If `i` is a limit element, the `i`th iteration is the colimit - of `k`th iterations for `k < i`. -/ - isColimit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) : - IsColimit (Iteration.coconeOfLE F hij) +variable (C) in +/-- A successor structure on a category consists of the +data of an object `succ X` for any `X : C`, a map `toSucc X : X ⟶ toSucc X` +(which does not need to be natural), and a zeroth object `X₀`. +-/ +structure SuccStruct where + /-- the zeroth object -/ + X₀ : C + /-- the successor of an object -/ + succ (X : C) : C + /-- the map to the successor -/ + toSucc (X : C) : X ⟶ succ X + +namespace SuccStruct + +/-- Given a functor `Φ : C ⥤ C`, a natural transformation of the form `𝟭 C ⟶ Φ` +induces a successor structure on `C ⥤ C`. -/ +@[simps] +def ofNatTrans {F : C ⥤ C} (ε : 𝟭 C ⟶ F) : SuccStruct (C ⥤ C) where + succ G := G ⋙ F + toSucc G := whiskerLeft G ε + X₀ := 𝟭 C -namespace Iteration +variable (Φ : SuccStruct C) -variable {ε} -variable {j : J} +/-- The class of morphisms that are of the form `toSucc X : X ⟶ succ X`. -/ +def prop : MorphismProperty C := .ofHoms (fun (X : C) ↦ Φ.toSucc X) + +lemma prop_toSucc (X : C) : Φ.prop (Φ.toSucc X) := ⟨_⟩ + +/-- The map `Φ.toSucc X : X ⟶ Φ.Succ X`, as an element in `Arrow C`. -/ +def toSuccArrow (X : C) : Arrow C := Arrow.mk (Φ.toSucc X) + +lemma prop_iff {X Y : C} (f : X ⟶ Y) : + Φ.prop f ↔ Arrow.mk f = Φ.toSuccArrow X := by + constructor + · rintro ⟨_⟩ + rfl + · intro h + rw [← Φ.prop.arrow_mk_mem_toSet_iff, h] + apply prop_toSucc + +variable [LinearOrder J] + +/-- Given a functor `F : Set.Iic ⥤ C`, this is the morphism in `C`, as an element +in `Arrow C`, that is obtained by applying `F.map` to an inequality. -/ +def arrowMap {j : J} (F : Set.Iic j ⥤ C) (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j) : + Arrow C := + Arrow.mk (F.map (homOfLE h₁₂ : ⟨i₁, h₁₂.trans h₂⟩ ⟶ ⟨i₂, h₂⟩)) + +@[simp] +lemma arrowMap_refl {j : J} (F : Set.Iic j ⥤ C) (i : J) (hi : i ≤ j) : + arrowMap F i i (by simp) hi = Arrow.mk (𝟙 (F.obj ⟨i, hi⟩)) := by + simp [arrowMap] + +lemma arrowMap_restrictionLE {j : J} (F : Set.Iic j ⥤ C) {j' : J} (hj' : j' ≤ j) + (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j') : + arrowMap (restrictionLE F hj') i₁ i₂ h₁₂ h₂ = + arrowMap F i₁ i₂ h₁₂ (h₂.trans hj') := rfl section -variable [Preorder J] [OrderBot J] [SuccOrder J] (iter : Φ.Iteration ε j) +variable [SuccOrder J] {j : J} (F : Set.Iic j ⥤ C) (i : J) (hi : i < j) -/-- For `iter : Φ.Iteration.ε j`, this is the map -`iter.F.obj ⟨i, _⟩ ⟶ iter.F.obj ⟨Order.succ i, _⟩` if `i : J` is such that `i < j`. -/ -noncomputable abbrev mapSucc (i : J) (hi : i < j) : - iter.F.obj ⟨i, hi.le⟩ ⟶ iter.F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ := - mapSucc' iter.F i hi +/-- Given a functor `F : Set.Iic j ⥤ C` and `i : J` such that `i < j`, +this is the arrow `F.obj ⟨i, _⟩ ⟶ F.obj ⟨Order.succ i, _⟩`. -/ +def arrowSucc : Arrow C := + arrowMap F i (Order.succ i) (Order.le_succ i) (Order.succ_le_of_lt hi) -lemma mapSucc_eq (i : J) (hi : i < j) : - iter.mapSucc i hi = whiskerLeft _ ε ≫ (iter.isoSucc i hi).inv := - iter.mapSucc'_eq _ hi +lemma arrowSucc_def : + arrowSucc F i hi = arrowMap F i (Order.succ i) (Order.le_succ i) (Order.succ_le_of_lt hi) := + rfl end section -variable [Preorder J] [OrderBot J] [SuccOrder J] (iter₁ iter₂ : Φ.Iteration ε j) +variable [HasIterationOfShape J C] + {i : J} (F : Set.Iio i ⥤ C) (hi : Order.IsSuccLimit i) (k : J) (hk : k < i) -/-- A morphism between two objects `iter₁` and `iter₂` in the -category `Φ.Iteration ε j` of `j`th iterations of a functor `Φ` -equipped with a natural transformation `ε : 𝟭 C ⟶ Φ` consists of a natural -transformation `natTrans : iter₁.F ⟶ iter₂.F` which is compatible with the -isomorphisms `isoZero` and `isoSucc`. -/ -structure Hom where - /-- A natural transformation `iter₁.F ⟶ iter₂.F` -/ - natTrans : iter₁.F ⟶ iter₂.F - natTrans_app_zero : - natTrans.app ⟨⊥, bot_le⟩ = iter₁.isoZero.hom ≫ iter₂.isoZero.inv := by aesop_cat - natTrans_app_succ (i : J) (hi : i < j) : - natTrans.app ⟨Order.succ i, Order.succ_le_of_lt hi⟩ = (iter₁.isoSucc i hi).hom ≫ - whiskerRight (natTrans.app ⟨i, hi.le⟩) _ ≫ (iter₂.isoSucc i hi).inv := by aesop_cat +/-- Given `F : Set.Iio i ⥤ C`, with `i` a limit element, and `k` such that `hk : k < i`, +this is the map `colimit.ι F ⟨k, hk⟩`, as an element in `Arrow C`. -/ +noncomputable def arrowι : Arrow C := + letI := hasColimitsOfShape_of_isSuccLimit C i hi + Arrow.mk (colimit.ι F ⟨k, hk⟩) -namespace Hom +lemma arrowι_def : + letI := hasColimitsOfShape_of_isSuccLimit C i hi + arrowι F hi k hk = Arrow.mk (colimit.ι F ⟨k, hk⟩) := rfl -attribute [simp, reassoc] natTrans_app_zero +end -/-- The identity morphism in the category `Φ.Iteration ε j`. -/ -@[simps] -def id : Hom iter₁ iter₁ where - natTrans := 𝟙 _ +variable [SuccOrder J] [OrderBot J] [HasIterationOfShape J C] -variable {iter₁ iter₂} +/-- The category of `j`th iterations of a succesor structure `Φ : SuccStruct C`. +An object consists of the data of all iterations of `Φ` for `i : J` such +that `i ≤ j` (this is the field `F`). Such objects are +equipped with data and properties which characterizes uniquely the iterations +on three types of elements: `⊥`, successors, limit elements. -/ +@[ext] +structure Iteration [WellFoundedLT J] (j : J) where + /-- The data of all `i`th iterations for `i : J` such that `i ≤ j`. -/ + F : Set.Iic j ⥤ C + /-- The zeroth iteration is the zeroth object . -/ + obj_bot : F.obj ⟨⊥, bot_le⟩ = Φ.X₀ + /-- The iteration on a successor element is the successor. -/ + arrowSucc_eq (i : J) (hi : i < j) : arrowSucc F i hi = Φ.toSuccArrow (F.obj ⟨i, hi.le⟩) + /-- The iteration on a limit element identifies to the colimit of the + value on smaller elements, see `Iteration.isColimit`. -/ + arrowMap_limit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i) : + arrowMap F k i hk.le hij = arrowι (restrictionLT F hij) hi k hk + +variable [WellFoundedLT J] --- Note: this is not made a global ext lemma because it is shown below --- that the type of morphisms is a subsingleton. -lemma ext' {f g : Hom iter₁ iter₂} (h : f.natTrans = g.natTrans) : f = g := by - cases f - cases g - subst h - rfl +namespace Iteration -attribute [local ext] ext' +variable {Φ} +variable {j : J} -/-- The composition of morphisms in the category `Iteration ε j`. -/ -@[simps] -def comp {iter₃ : Iteration ε j} (f : Hom iter₁ iter₂) (g : Hom iter₂ iter₃) : - Hom iter₁ iter₃ where - natTrans := f.natTrans ≫ g.natTrans - natTrans_app_succ i hi := by simp [natTrans_app_succ _ _ hi] - -instance : Category (Iteration ε j) where - Hom := Hom - id := id - comp := comp - -instance {J} {j : J} [PartialOrder J] [OrderBot J] [WellFoundedLT J] [SuccOrder J] - {iter₁ iter₂ : Iteration ε j} : - Subsingleton (iter₁ ⟶ iter₂) where - allEq f g := by - apply ext' - suffices ∀ i hi, f.natTrans.app ⟨i, hi⟩ = g.natTrans.app ⟨i, hi⟩ by - ext ⟨i, hi⟩ : 2 - apply this - intro i - induction i using SuccOrder.limitRecOn with - | hm j H => - obtain rfl := H.eq_bot - simp [natTrans_app_zero] - | hs j H IH => - intro hj - simp [Hom.natTrans_app_succ, IH, (Order.lt_succ_of_not_isMax H).trans_le hj] - | hl j H IH => - refine fun hj ↦ (iter₁.isColimit j H hj).hom_ext ?_ - rintro ⟨k, hk⟩ - simp [IH k hk] - -end Hom +section -@[simp] -lemma natTrans_id : Hom.natTrans (𝟙 iter₁) = 𝟙 _ := rfl +variable (iter : Φ.Iteration j) + +lemma obj_succ (i : J) (hi : i < j) : + iter.F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ = Φ.succ (iter.F.obj ⟨i, hi.le⟩) := + congr_arg Comma.right (iter.arrowSucc_eq i hi) + +lemma prop_map_succ (i : J) (hi : i < j) : + Φ.prop (iter.F.map (homOfLE (Order.le_succ i) : + ⟨i, hi.le⟩ ⟶ ⟨Order.succ i, Order.succ_le_of_lt hi⟩)) := by + rw [prop_iff, ← arrowMap, ← arrowSucc_def _ _ hi, iter.arrowSucc_eq] + +lemma obj_limit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) : + letI := hasColimitsOfShape_of_isSuccLimit C i hi + iter.F.obj ⟨i, hij⟩ = colimit (restrictionLT iter.F hij) := + congr_arg Comma.right (iter.arrowMap_limit i hi hij ⊥ (Order.IsSuccLimit.bot_lt hi)) + +/-- The iteration on a limit element identifies to the colimit of the +value on smaller elements. -/ +noncomputable def isColimit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) : + IsColimit (coconeOfLE iter.F hij) := by + letI := hasColimitsOfShape_of_isSuccLimit C i hi + refine IsColimit.ofIsoColimit (colimit.isColimit (restrictionLT iter.F hij)) + (Cocones.ext (eqToIso (iter.obj_limit i hi hij).symm) ?_) + rintro ⟨k, hk⟩ + apply Arrow.mk_injective + dsimp + rw [← arrowMap] + simp [iter.arrowMap_limit i hi hij k hk, arrowι_def] + +/-- The element in `Φ.Iteration i` that is deduced from an element +in `Φ.Iteration j` when `i ≤ j`. -/ +@[simps F] +def trunc (iter : Φ.Iteration j) {j' : J} (hj' : j' ≤ j) : Φ.Iteration j' where + F := restrictionLE iter.F hj' + obj_bot := iter.obj_bot + arrowSucc_eq i hi := iter.arrowSucc_eq i (lt_of_lt_of_le hi hj') + arrowMap_limit i hi hij k hk := iter.arrowMap_limit i hi (hij.trans hj') k hk -variable {iter₁ iter₂} +end -@[simp, reassoc] -lemma natTrans_comp {iter₃ : Iteration ε j} (φ : iter₁ ⟶ iter₂) (ψ : iter₂ ⟶ iter₃) : - (φ ≫ ψ).natTrans = φ.natTrans ≫ ψ.natTrans := rfl +namespace subsingleton -@[reassoc] -lemma natTrans_naturality (φ : iter₁ ⟶ iter₂) (i₁ i₂ : J) (h : i₁ ≤ i₂) (h' : i₂ ≤ j) : - iter₁.F.map (by exact homOfLE h) ≫ φ.natTrans.app ⟨i₂, h'⟩ = - φ.natTrans.app ⟨i₁, h.trans h'⟩ ≫ iter₂.F.map (by exact homOfLE h) := by - apply φ.natTrans.naturality +variable {K : Type w} [LinearOrder K] {x : K} (F G : Set.Iic x ⥤ C) -variable (ε) in -/-- The evaluation functor `Iteration ε j ⥤ C ⥤ C` at `i : J` when `i ≤ j`. -/ -@[simps] -def eval {i : J} (hi : i ≤ j) : Iteration ε j ⥤ C ⥤ C where - obj iter := iter.F.obj ⟨i, hi⟩ - map φ := φ.natTrans.app _ - -/-- Given `iter : Iteration ε j` and `i : J` such that `i ≤ j`, this is the -induced element in `Iteration ε i`. -/ -@[simps F isoZero isoSucc] -def trunc (iter : Iteration ε j) {i : J} (hi : i ≤ j) : Iteration ε i where - F := restrictionLE iter.F hi - isoZero := iter.isoZero - isoSucc k hk := iter.isoSucc k (lt_of_lt_of_le hk hi) - mapSucc'_eq k hk := iter.mapSucc'_eq k (lt_of_lt_of_le hk hi) - isColimit k hk' hk := iter.isColimit k hk' (hk.trans hi) - -variable (ε) in -/-- The truncation functor `Iteration ε j ⥤ Iteration ε i` when `i ≤ j`. -/ -@[simps obj] -def truncFunctor {i : J} (hi : i ≤ j) : Iteration ε j ⥤ Iteration ε i where - obj iter := iter.trunc hi - map {iter₁ iter₂} φ := - { natTrans := whiskerLeft _ φ.natTrans - natTrans_app_succ := fun k hk => φ.natTrans_app_succ k (lt_of_lt_of_le hk hi) } +section -@[simp] -lemma truncFunctor_map_natTrans_app - (φ : iter₁ ⟶ iter₂) {i : J} (hi : i ≤ j) (k : J) (hk : k ≤ i) : - ((truncFunctor ε hi).map φ).natTrans.app ⟨k, hk⟩ = - φ.natTrans.app ⟨k, hk.trans hi⟩ := rfl +variable (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x) -end +/-- Auxiliary definition for the proof of `Subsingleton (Φ.Iteration j)`. -/ +def MapEq : Prop := arrowMap F k₁ k₂ h₁₂ h₂ = arrowMap G k₁ k₂ h₁₂ h₂ + +namespace MapEq + +variable {k₁ k₂ h₁₂ h₂} (h : MapEq F G k₁ k₂ h₁₂ h₂) + +include h + +lemma src : F.obj ⟨k₁, h₁₂.trans h₂⟩ = G.obj ⟨k₁, h₁₂.trans h₂⟩ := + congr_arg Comma.left h + +lemma tgt : F.obj ⟨k₂, h₂⟩ = G.obj ⟨k₂, h₂⟩ := + congr_arg Comma.right h -namespace Hom +lemma w : + F.map (homOfLE h₁₂ : ⟨k₁, h₁₂.trans h₂⟩ ⟶ ⟨k₂, h₂⟩) = + eqToHom (by rw [h.src]) ≫ G.map (homOfLE h₁₂ : ⟨k₁, h₁₂.trans h₂⟩ ⟶ ⟨k₂, h₂⟩) ≫ + eqToHom (by rw [h.tgt]) := by + have := (Arrow.mk_eq_mk_iff _ _).1 h + tauto -variable [PartialOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] - {iter₁ iter₂ : Φ.Iteration ε j} +end MapEq -lemma congr_app (φ φ' : iter₁ ⟶ iter₂) (i : J) (hi : i ≤ j) : - φ.natTrans.app ⟨i, hi⟩ = φ'.natTrans.app ⟨i, hi⟩ := by - obtain rfl := Subsingleton.elim φ φ' +end + +variable {F G} + +lemma mapEq_refl (k : K) (hk : k ≤ x) (h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩) : + MapEq F G k k (by simp) hk := by + rw [MapEq, arrowMap_refl, arrowMap_refl, h] + +lemma mapEq_trans {i₁ i₂ i₃ : K} (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ ≤ i₃) {h₃ : i₃ ≤ x} + (m₁₂ : MapEq F G i₁ i₂ h₁₂ (h₂₃.trans h₃)) (m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃) : + MapEq F G i₁ i₃ (h₁₂.trans h₂₃) h₃ := by + simp only [MapEq, arrowMap, Arrow.mk_eq_mk_iff] + refine ⟨m₁₂.src, m₂₃.tgt, ?_⟩ + rw [← homOfLE_comp (y := ⟨i₂, h₂₃.trans h₃⟩) h₁₂ h₂₃] + simp [-homOfLE_comp, m₁₂.w, m₂₃.w] + +lemma ext (h : ∀ (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x), + MapEq F G k₁ k₂ h₁₂ h₂) : + F = G := by + apply Arrow.functor_ext + rintro ⟨k₁, _⟩ ⟨k₂, h₂⟩ f + apply h + +end subsingleton + +open subsingleton in +instance subsingleton : Subsingleton (Φ.Iteration j) where + allEq iter₁ iter₂ := by + suffices iter₁.F = iter₂.F by aesop + revert iter₁ iter₂ + induction j using SuccOrder.limitRecOn with + | hm j h => + obtain rfl := h.eq_bot + intro iter₁ iter₂ + refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_) + obtain rfl : k₂ = ⊥ := by simpa using h₂ + obtain rfl : k₁ = ⊥ := by simpa using h₁₂ + apply mapEq_refl _ _ (by simp only [obj_bot]) + | hs j hj₁ hj₂ => + intro iter₁ iter₂ + refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_) + have h₀ := Order.le_succ j + replace hj₂ := hj₂ (iter₁.trunc h₀) (iter₂.trunc h₀) + have hsucc := Functor.congr_obj hj₂ ⟨j, by simp⟩ + dsimp at hj₂ hsucc + wlog h : k₂ ≤ j generalizing k₁ k₂ + · obtain h₂ | rfl := h₂.lt_or_eq + · exact this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂) + · by_cases h' : k₁ ≤ j + · apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp)) + simp only [MapEq, ← arrowSucc_def _ _ (Order.lt_succ_of_not_isMax hj₁), + arrowSucc_eq, hsucc] + · simp only [not_le] at h' + obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂ + ((Order.succ_le_iff_of_not_isMax hj₁).2 h') + rw [MapEq, arrowMap_refl, arrowMap_refl, + obj_succ _ _ h', obj_succ _ _ h', hsucc] + simp only [MapEq, ← arrowMap_restrictionLE _ (Order.le_succ j) _ _ _ h, hj₂] + | hl j h₁ h₂ => + intro iter₁ iter₂ + refine ext (fun k₁ k₂ h₁₂ h₃ ↦ ?_) + wlog h₄ : k₂ < j generalizing k₁ k₂; swap + · have := h₂ k₂ h₄ (iter₁.trunc h₄.le) (iter₂.trunc h₄.le) + simp at this + simp only [MapEq, ← arrowMap_restrictionLE _ h₄.le _ _ _ (by rfl), this] + · obtain rfl : j = k₂ := le_antisymm (by simpa using h₄) h₃ + have : restrictionLT iter₁.F le_rfl = restrictionLT iter₂.F le_rfl := + Arrow.functor_ext (fun _ l _ ↦ this _ _ _ _ l.2) + by_cases h₅ : k₁ < j + · dsimp [MapEq] + simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this] + · obtain rfl : k₁ = j := le_antisymm h₁₂ (by simpa using h₅) + apply mapEq_refl + simp only [obj_limit _ _ h₁, this] + +lemma congr_obj {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) + (k : J) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂) : + iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩ := by + wlog h : j₁ ≤ j₂ generalizing j₁ j₂ + · exact (this iter₂ iter₁ h₂ h₁ (le_of_lt (by simpa using h))).symm + rw [Subsingleton.elim iter₁ (iter₂.trunc h)] + dsimp + +lemma congr_arrowMap {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) + {k₁ k₂ : J} (h : k₁ ≤ k₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) : + arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂ := by + wlog hj : j₁ ≤ j₂ generalizing j₁ j₂ + · simp [this iter₂ iter₁ h₂ h₁ ((not_le.1 hj).le)] + rw [Subsingleton.elim iter₁ (iter₂.trunc hj)] rfl -end Hom +lemma congr_map {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) + {k₁ k₂ : J} (h : k₁ ≤ k₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) : + iter₁.F.map (homOfLE h : ⟨k₁, h.trans h₁⟩ ⟶ ⟨k₂, h₁⟩) = + eqToHom (congr_obj iter₁ iter₂ k₁ (h.trans h₁) (h.trans h₂)) ≫ + iter₂.F.map (homOfLE h) ≫ + eqToHom (congr_obj iter₁ iter₂ k₂ h₁ h₂).symm := by + have := (Arrow.mk_eq_mk_iff _ _).1 (congr_arrowMap iter₁ iter₂ h h₁ h₂) + tauto + +/-- Given `iter₁ : Φ.Iteration j₁` and `iter₂ : Φ.Iteration j₂`, with `j₁ ≤ j₂`, +if `k₁ ≤ k₂` are elements such that `k₁ ≤ j₁` and `k₂ ≤ k₂`, then this +is the canonical map `iter₁.F.obj ⟨k₁, h₁⟩ ⟶ iter₂.F.obj ⟨k₂, h₂⟩`. -/ +def mapObj {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) + {k₁ k₂ : J} (h₁₂ : k₁ ≤ k₂) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂) : + iter₁.F.obj ⟨k₁, h₁⟩ ⟶ iter₂.F.obj ⟨k₂, h₂⟩ := + eqToHom (congr_obj iter₁ iter₂ k₁ h₁ (h₁.trans hj)) ≫ + iter₂.F.map (homOfLE h₁₂) + +lemma arrow_mk_mapObj {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) + {k₁ k₂ : J} (h₁₂ : k₁ ≤ k₂) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂) : + Arrow.mk (mapObj iter₁ iter₂ h₁₂ h₁ h₂ hj) = + arrowMap iter₂.F k₁ k₂ h₁₂ h₂ := by + simp [mapObj, arrowMap] + +@[simp] +lemma mapObj_refl {j : J} (iter : Φ.Iteration j) + {k l : J} (h : k ≤ l) (h' : l ≤ j) : + mapObj iter iter h (h.trans h') h' (by rfl) = iter.F.map (homOfLE h) := by + simp [mapObj] + +@[reassoc (attr := simp)] +lemma mapObj_trans {j₁ j₂ j₃ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) + (iter₃ : Φ.Iteration j₃) {k₁ k₂ k₃ : J} (h₁₂ : k₁ ≤ k₂) (h₂₃ : k₂ ≤ k₃) + (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (h₃ : k₃ ≤ j₃) (h₁₂' : j₁ ≤ j₂) (h₂₃' : j₂ ≤ j₃) : + mapObj iter₁ iter₂ h₁₂ h₁ h₂ h₁₂' ≫ mapObj iter₂ iter₃ h₂₃ h₂ h₃ h₂₃' = + mapObj iter₁ iter₃ (h₁₂.trans h₂₃) h₁ h₃ (h₁₂'.trans h₂₃') := by + simp [mapObj, congr_map iter₂ iter₃ h₁₂ h₂ (h₂.trans h₂₃'), ← Functor.map_comp] end Iteration -end Functor +end SuccStruct + +end SmallObject end CategoryTheory diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean index 166469022df524..730a42b41c6792 100644 --- a/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean +++ b/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean @@ -22,12 +22,14 @@ namespace CategoryTheory open Category -namespace Functor +namespace SmallObject variable {C : Type*} [Category C] {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j) (F : Set.Iic j ⥤ C) {X : C} (τ : F.obj ⟨j, by simp⟩ ⟶ X) +namespace SuccStruct + namespace extendToSucc variable (X) @@ -37,14 +39,22 @@ it sends `Order.succ j` to the given object `X`. -/ def obj (i : Set.Iic (Order.succ j)) : C := if hij : i.1 ≤ j then F.obj ⟨i.1, hij⟩ else X +lemma obj_eq (i : Set.Iic j) : + obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ = F.obj i := dif_pos i.2 + /-- The isomorphism `obj F X ⟨i, _⟩ ≅ F.obj i` when `i : Set.Iic j`. -/ def objIso (i : Set.Iic j) : - obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i := eqToIso (dif_pos i.2) + obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i := + eqToIso (obj_eq _ _ _) + +include hj in +lemma obj_succ_eq : obj F X ⟨Order.succ j, by simp⟩ = X := + dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj) /-- The isomorphism `obj F X ⟨Order.succ j, _⟩ ≅ X`. -/ def objSuccIso : obj F X ⟨Order.succ j, by simp⟩ ≅ X := - eqToIso (dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj)) + eqToIso (obj_succ_eq hj _ _) variable {X} @@ -76,7 +86,7 @@ lemma map_self_succ : (objIso F X ⟨j, by simp⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv := by dsimp [map] rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj), - dif_pos (by rfl), map_id, comp_id, id_comp] + dif_pos (by rfl), Functor.map_id, comp_id, id_comp] @[simp] lemma map_id (i : J) (hi : i ≤ Order.succ j) : @@ -93,15 +103,15 @@ lemma map_comp (i₁ i₂ i₃ : J) (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ map hj F τ i₁ i₂ h₁₂ (h₂₃.trans h) ≫ map hj F τ i₂ i₃ h₂₃ h := by by_cases h₁ : i₃ ≤ j · rw [map_eq hj F τ i₁ i₂ _ (h₂₃.trans h₁), map_eq hj F τ i₂ i₃ _ h₁, - map_eq hj F τ i₁ i₃ _ h₁, assoc, assoc, Iso.inv_hom_id_assoc, ← map_comp_assoc, + map_eq hj F τ i₁ i₃ _ h₁, assoc, assoc, Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc, homOfLE_comp] · obtain rfl : i₃ = Order.succ j := le_antisymm h (Order.succ_le_of_lt (not_le.1 h₁)) obtain h₂ | rfl := h₂₃.lt_or_eq · rw [Order.lt_succ_iff_of_not_isMax hj] at h₂ rw [map_eq hj F τ i₁ i₂ _ h₂] dsimp [map] - rw [dif_neg h₁, dif_pos (h₁₂.trans h₂), dif_neg h₁, dif_pos h₂, - assoc, assoc, Iso.inv_hom_id_assoc,comp_id, ← map_comp_assoc, homOfLE_comp] + rw [dif_neg h₁, dif_pos (h₁₂.trans h₂), dif_neg h₁, dif_pos h₂, assoc, assoc, + Iso.inv_hom_id_assoc,comp_id, ← Functor.map_comp_assoc, homOfLE_comp] · rw [map_id, comp_id] end extendToSucc @@ -116,10 +126,18 @@ def extendToSucc : Set.Iic (Order.succ j) ⥤ C where map_id _ := extendToSucc.map_id _ F τ _ _ map_comp {i₁ i₂ i₃} f g := extendToSucc.map_comp hj F τ i₁ i₂ i₃ (leOfHom f) (leOfHom g) i₃.2 -/-- The isomorphism `(extendToSucc hj F τ).obj ⟨i, _⟩ ≅ F.obj i` when `i : Set.Iic j` -/ -def extendToSuccObjIso (i : Set.Iic j) : - (extendToSucc hj F τ).obj ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i := - extendToSucc.objIso F X i +lemma extendToSucc_obj_eq (i : J) (hi : i ≤ j) : + (extendToSucc hj F τ).obj ⟨i, hi.trans (Order.le_succ j)⟩ = F.obj ⟨i, hi⟩ := + extendToSucc.obj_eq F X ⟨i, hi⟩ + +/-- The isomorphism `(extendToSucc hj F τ).obj ⟨i, _⟩ ≅ F.obj i` when `i ≤ j` -/ +def extendToSuccObjIso (i : J) (hi : i ≤ j) : + (extendToSucc hj F τ).obj ⟨i, hi.trans (Order.le_succ j)⟩ ≅ F.obj ⟨i, hi⟩ := + extendToSucc.objIso F X ⟨i, hi⟩ + +lemma extendToSucc_obj_succ_eq : + (extendToSucc hj F τ).obj ⟨Order.succ j, by simp⟩ = X := + extendToSucc.obj_succ_eq hj F X /-- The isomorphism `(extendToSucc hj F τ).obj ⟨Order.succ j, _⟩ ≅ X`. -/ def extendToSuccObjSuccIso : @@ -130,32 +148,46 @@ def extendToSuccObjSuccIso : lemma extendToSuccObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) : (extendToSucc hj F τ).map (homOfLE hi : ⟨i₁, hi.trans (hi₂.trans (Order.le_succ j))⟩ ⟶ ⟨i₂, hi₂.trans (Order.le_succ j)⟩) ≫ - (extendToSuccObjIso hj F τ ⟨i₂, hi₂⟩).hom = - (extendToSuccObjIso hj F τ ⟨i₁, hi.trans hi₂⟩).hom ≫ F.map (homOfLE hi) := by + (extendToSuccObjIso hj F τ i₂ hi₂).hom = + (extendToSuccObjIso hj F τ i₁ (hi.trans hi₂)).hom ≫ F.map (homOfLE hi) := by dsimp [extendToSucc, extendToSuccObjIso] rw [extendToSucc.map_eq _ _ _ _ _ _ hi₂, assoc, assoc, Iso.inv_hom_id, comp_id] /-- The isomorphism expressing that `extendToSucc hj F τ` extends `F`. -/ @[simps!] def extendToSuccRestrictionLEIso : - Iteration.restrictionLE (extendToSucc hj F τ) (Order.le_succ j) ≅ F := - NatIso.ofComponents (extendToSuccObjIso hj F τ) (by + SmallObject.restrictionLE (extendToSucc hj F τ) (Order.le_succ j) ≅ F := + NatIso.ofComponents (fun i ↦ extendToSuccObjIso hj F τ i.1 i.2) (by rintro ⟨i₁, h₁⟩ ⟨i₂, h₂⟩ f apply extendToSuccObjIso_hom_naturality) -lemma extentToSucc_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) : +lemma extendToSucc_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) : (extendToSucc hj F τ).map (homOfLE hi : ⟨i₁, hi.trans (hi₂.trans (Order.le_succ j))⟩ ⟶ ⟨i₂, hi₂.trans (Order.le_succ j)⟩) = - (extendToSuccObjIso hj F τ ⟨i₁, hi.trans hi₂⟩).hom ≫ F.map (homOfLE hi) ≫ - (extendToSuccObjIso hj F τ ⟨i₂, hi₂⟩).inv := by + (extendToSuccObjIso hj F τ i₁ (hi.trans hi₂)).hom ≫ F.map (homOfLE hi) ≫ + (extendToSuccObjIso hj F τ i₂ hi₂).inv := by rw [← extendToSuccObjIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id] lemma extendToSucc_map_le_succ : (extendToSucc hj F τ).map (homOfLE (Order.le_succ j)) = - (extendToSuccObjIso hj F τ ⟨j, by simp⟩).hom ≫ τ ≫ + (extendToSuccObjIso hj F τ j (by simp)).hom ≫ τ ≫ (extendToSuccObjSuccIso hj F τ).inv := extendToSucc.map_self_succ _ _ _ -end Functor +lemma arrowMap_extendToSucc (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) : + arrowMap (extendToSucc hj F τ) i₁ i₂ hi (hi₂.trans (Order.le_succ j)) = + arrowMap F i₁ i₂ hi hi₂ := by + simp [arrowMap, extendToSucc_map hj F τ i₁ i₂ hi hi₂, + extendToSuccObjIso, extendToSucc.objIso] + +lemma arrowSucc_extendToSucc : + arrowSucc (extendToSucc hj F τ) j (Order.lt_succ_of_not_isMax hj) = + Arrow.mk τ := by + simp [arrowSucc, arrowMap, extendToSucc_map_le_succ, extendToSuccObjIso, + extendToSucc.objIso, extendToSuccObjSuccIso, extendToSucc.objSuccIso] + +end SuccStruct + +end SmallObject end CategoryTheory diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean index 35b3bf90ea04c9..c75826a22944fb 100644 --- a/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean +++ b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean @@ -21,7 +21,9 @@ namespace CategoryTheory open Category Limits -namespace Functor +namespace SmallObject + +namespace SuccStruct variable {C : Type*} [Category C] {J : Type u} [LinearOrder J] @@ -29,23 +31,23 @@ variable {C : Type*} [Category C] namespace ofCocone -/-- Auxiliary definition for `Functor.ofCocone`. -/ +/-- Auxiliary definition for `ofCocone`. -/ def obj (i : J) : C := if hi : i < j then F.obj ⟨i, hi⟩ else c.pt -/-- Auxiliary definition for `Functor.ofCocone`. -/ +/-- Auxiliary definition for `ofCocone`. -/ def objIso (i : J) (hi : i < j) : obj c i ≅ F.obj ⟨i, hi⟩ := eqToIso (dif_pos hi) -/-- Auxiliary definition for `Functor.ofCocone`. -/ +/-- Auxiliary definition for `ofCocone`. -/ def objIsoPt : obj c j ≅ c.pt := eqToIso (dif_neg (by simp)) -/-- Auxiliary definition for `Functor.ofCocone`. -/ +/-- Auxiliary definition for `ofCocone`. -/ def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) : obj c i₁ ⟶ obj c i₂ := if h₂ : i₂ < j then @@ -92,11 +94,19 @@ def ofCocone : Set.Iic j ⥤ C where map_id i := ofCocone.map_id _ _ i.2 map_comp {_ _ i₃} _ _ := ofCocone.map_comp _ _ _ _ _ _ i₃.2 +lemma ofCocone_obj_eq (i : J) (hi : i < j) : + (ofCocone c).obj ⟨i, hi.le⟩ = F.obj ⟨i, hi⟩ := + dif_pos hi + /-- The isomorphism `(ofCocone c).obj ⟨i, _⟩ ≅ F.obj ⟨i, _⟩` when `i < j`. -/ def ofCoconeObjIso (i : J) (hi : i < j) : (ofCocone c).obj ⟨i, hi.le⟩ ≅ F.obj ⟨i, hi⟩ := ofCocone.objIso c _ _ +lemma ofCocone_obj_eq_pt : + (ofCocone c).obj ⟨j, by simp⟩ = c.pt := + dif_neg (by simp) + /-- The isomorphism `(ofCocone c).obj ⟨j, _⟩ ≅ c.pt`. -/ def ofCoconeObjIsoPt : (ofCocone c).obj ⟨j, by simp⟩ ≅ c.pt := @@ -127,20 +137,32 @@ lemma ofCoconeObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ when `c : Cocone F`. -/ @[simps!] def restrictionLTOfCoconeIso : - Iteration.restrictionLT (ofCocone c) (Preorder.le_refl j) ≅ F := + SmallObject.restrictionLT (ofCocone c) (Preorder.le_refl j) ≅ F := NatIso.ofComponents (fun ⟨i, hi⟩ ↦ ofCoconeObjIso c i hi) (by intros; apply ofCoconeObjIso_hom_naturality) variable {c} in /-- If `c` is a colimit cocone, then so is `coconeOfLE (ofCocone c) (Preorder.le_refl j)`. -/ def isColimitCoconeOfLEOfCocone (hc : IsColimit c) : - IsColimit (Iteration.coconeOfLE (ofCocone c) (Preorder.le_refl j)) := + IsColimit (coconeOfLE (ofCocone c) (Preorder.le_refl j)) := (IsColimit.precomposeInvEquiv (restrictionLTOfCoconeIso c) _).1 (IsColimit.ofIsoColimit hc (Cocones.ext (ofCoconeObjIsoPt c).symm (fun ⟨i, hi⟩ ↦ by dsimp rw [ofCocone_map_to_top _ _ hi, Iso.inv_hom_id_assoc]))) -end Functor +lemma arrowMap_ofCocone (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ < j) : + arrowMap (ofCocone c) i₁ i₂ h₁₂ h₂.le = + Arrow.mk (F.map (homOfLE h₁₂ : ⟨i₁, lt_of_le_of_lt h₁₂ h₂⟩ ⟶ ⟨i₂, h₂⟩)) := + Arrow.ext (ofCocone_obj_eq _ _ _) (ofCocone_obj_eq _ _ _) (ofCocone_map _ _ _ _ _) + +lemma arrowMap_ofCocone_to_top (i : J) (hi : i < j) : + arrowMap (ofCocone c) i j hi.le (by simp) = Arrow.mk (c.ι.app ⟨i, hi⟩) := by + rw [arrowMap, ofCocone_map_to_top _ _ hi] + exact Arrow.ext (ofCocone_obj_eq _ _ _) (ofCocone_obj_eq_pt _) rfl + +end SuccStruct + +end SmallObject end CategoryTheory diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean index 80bdbaec34cea1..69f13db5160b72 100644 --- a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean +++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean @@ -3,18 +3,16 @@ Copyright (c) 2024 Joël Riou. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ +import Mathlib.CategoryTheory.SmallObject.Iteration.Basic import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc +import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone /-! -# Existence of objects in the category of iterations of functors +# Existence of the iteration of a successor structure -Given a functor `Φ : C ⥤ C` and a natural transformation `ε : 𝟭 C ⟶ Φ`, -we shall show in this file that for any well ordered set `J`, -and `j : J`, the category `Functor.Iteration ε j` is nonempty. -As we already know from the main result in `SmallObject.Iteration.UniqueHom` -that such objects, if they exist, are unique up to a unique isomorphism, -we shall show the existence of a term in `Functor.Iteration ε j` by -transfinite induction. +Given `Φ : SuccStruct C`, we show by transfinite induction +that for any element `j` in a well ordered set `J`, +the type `Φ.Iteration j` is nonempty. -/ @@ -22,76 +20,138 @@ universe u namespace CategoryTheory -open Category Limits +namespace SmallObject + +namespace SuccStruct -variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ} - {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] +open Category Limits -namespace Functor +variable {C : Type*} [Category C] (Φ : SuccStruct C) + {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] + [HasIterationOfShape J C] namespace Iteration -variable (ε J) in -/-- The obvious term in `Iteration ε ⊥`: it is given by the identity functor. -/ -def mkOfBot : Iteration ε (⊥ : J) where - F := (Functor.const _).obj (𝟭 C) - isoZero := Iso.refl _ - isoSucc _ h := by simp at h - mapSucc'_eq _ h := by simp at h - isColimit x hx h := by - exfalso - refine hx.not_isMin (by simpa using h) - -/-- When `j : J` is not maximal, this is the extension as `Iteration ε (Order.succ j)` -of any `iter : Iteration ε j`. -/ -noncomputable def mkOfSucc {j : J} (hj : ¬IsMax j) (iter : Iteration ε j) : - Iteration ε (Order.succ j) where - F := extendToSucc hj iter.F (whiskerLeft _ ε) - isoZero := (extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨⊥, by simp⟩).trans iter.isoZero - isoSucc i hi := - if hij : i < j then - extendToSuccObjIso _ _ _ ⟨Order.succ i, Order.succ_le_of_lt hij⟩ ≪≫ - iter.isoSucc i hij ≪≫ (isoWhiskerRight (extendToSuccObjIso _ _ _ ⟨i, hij.le⟩).symm _) - else - have hij' : i = j := le_antisymm - (by simpa only [Order.lt_succ_iff_of_not_isMax hj] using hi) (by simpa using hij) - eqToIso (by subst hij'; rfl) ≪≫ extendToSuccObjSuccIso hj iter.F (whiskerLeft _ ε) ≪≫ - isoWhiskerRight ((extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨j, by simp⟩).symm.trans - (eqToIso (by subst hij'; rfl))) _ - mapSucc'_eq i hi := by - obtain hi' | rfl := ((Order.lt_succ_iff_of_not_isMax hj).mp hi).lt_or_eq - · ext X - have := iter.mapSucc_eq i hi' - dsimp [mapSucc, mapSucc'] at this ⊢ - rw [extentToSucc_map _ _ _ _ _ _ (Order.succ_le_of_lt hi'), this, dif_pos hi'] +variable (J) in +/-- The obvious term in `Φ.Iteration ε ⊥` that is given by `Φ.X₀`. -/ +def mkOfBot : Φ.Iteration (⊥ : J) where + F := (Functor.const _).obj Φ.X₀ + obj_bot := rfl + arrowSucc_eq _ h := by simp at h + arrowMap_limit _ h₁ h₂ := (h₁.not_isMin (by simpa using h₂)).elim + +variable {Φ} + +open Functor in +/-- When `j : J` is not maximal, this is the extension in `Φ.Iteration (Order.succ j)` +of any `iter : Φ.Iteration j`. -/ +noncomputable def mkOfSucc {j : J} (hj : ¬IsMax j) (iter : Φ.Iteration j) : + Φ.Iteration (Order.succ j) where + F := extendToSucc hj iter.F (Φ.toSucc _) + obj_bot := by rw [extendToSucc_obj_eq _ _ _ _ bot_le, obj_bot] + arrowSucc_eq i hi₁ := by + rw [Order.lt_succ_iff_of_not_isMax hj] at hi₁ + obtain hi₁ | rfl := hi₁.lt_or_eq + · rw [arrowSucc_def, arrowMap_extendToSucc _ _ _ _ _ _ (Order.succ_le_of_lt hi₁), + ← arrowSucc_def _ _ hi₁, iter.arrowSucc_eq i hi₁, + extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i hi₁.le] + · rw [arrowSucc_extendToSucc, toSuccArrow, + extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i] + arrowMap_limit i hi hij k hk := by + have hij' := (Order.IsSuccLimit.le_succ_iff hi).1 hij + rw [arrowMap_extendToSucc _ _ _ _ _ _ hij', arrowMap_limit _ _ hi _ _ hk] + congr 1 + apply Arrow.functor_ext + rintro ⟨k₁, h₁⟩ ⟨k₂, h₂⟩ f + dsimp + rw [← arrowMap, ← arrowMap, arrowMap_extendToSucc] + +namespace mkOfLimit + +open Functor + +variable {j : J} (hj : Order.IsSuccLimit j) (iter : ∀ (i : J), i < j → Φ.Iteration i) + +/-- Assuming `j : J` is a limit element and that we have `∀ (i : J), i < j → Φ.Iteration i`, +this is the inductive system `Set.Iio j ⥤ C` which sends `⟨i, _⟩` to +`(iter i _).F.obj ⟨i, _⟩`. -/ +@[simps] +noncomputable def inductiveSystem : Set.Iio j ⥤ C where + obj i := (iter i.1 i.2).F.obj ⟨i.1, by simp⟩ + map {i₁ i₂} f := mapObj (iter i₁.1 i₁.2) (iter i₂.1 i₂.2) (leOfHom f) + (by simp) (by simp) (leOfHom f) + +/-- The extension of `inductiveSystem iter` to a functor `Set.Iic j ⥤ C` which +sends the top element to the colimit of `inductiveSystem iter`. -/ +noncomputable def functor : Set.Iic j ⥤ C := + letI := hasColimitsOfShape_of_isSuccLimit C j hj + ofCocone (colimit.cocone (inductiveSystem iter)) + +lemma functor_obj (i : J) (hi : i < j) {k : J} (iter' : Φ.Iteration k) (hk : i ≤ k) : + (functor hj iter).obj ⟨i, hi.le⟩ = iter'.F.obj ⟨i, hk⟩ := by + dsimp only [functor] + rw [ofCocone_obj_eq _ _ hi] + apply congr_obj + +lemma arrowMap_functor (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ < j) : + arrowMap (functor hj iter) i₁ i₂ h₁₂ h₂.le = + Arrow.mk (mapObj (iter i₁ (lt_of_le_of_lt h₁₂ h₂)) (iter i₂ h₂) h₁₂ + (by simp) (by simp) h₁₂) := + arrowMap_ofCocone _ _ _ _ h₂ + +lemma arrowMap_functor_to_top (i : J) (hi : i < j) : + letI := hasColimitsOfShape_of_isSuccLimit C j hj + arrowMap (functor hj iter) i j hi.le (by simp) = + Arrow.mk (colimit.ι (inductiveSystem iter) ⟨i, hi⟩) := + arrowMap_ofCocone_to_top _ _ _ + +end mkOfLimit + +open mkOfLimit in +/-- When `j` is a limit element, this is the element in `Φ.Iteration j` +that is constructed from elements in `Φ.Iteration i` for all `i < j`. -/ +noncomputable def mkOfLimit {j : J} (hj : Order.IsSuccLimit j) + (iter : ∀ (i : J), i < j → Φ.Iteration i) : + Φ.Iteration j where + F := functor hj iter + obj_bot := functor_obj hj iter ⊥ (Order.IsSuccLimit.bot_lt hj) (mkOfBot Φ J) (by rfl) + arrowSucc_eq i hi := by + rw [arrowSucc_def, arrowMap_functor _ _ _ _ (Order.le_succ i) + ((Order.IsSuccLimit.succ_lt_iff hj).2 hi), arrow_mk_mapObj, + ← arrowSucc_def _ _ ((Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi))), + arrowSucc_eq, functor_obj _ _ _ hi] + arrowMap_limit i hi hij k hk := by + obtain hij | rfl := hij.lt_or_eq + · rw [arrowMap_functor _ _ _ _ _ hij, arrow_mk_mapObj, + arrowMap_limit _ _ hi _ _ hk] + congr 1 + apply Arrow.functor_ext + rintro ⟨l₁, hl₁⟩ ⟨l₂, hl₂⟩ f dsimp - rw [assoc, assoc] - erw [ε.naturality_assoc] - · ext X - dsimp [mapSucc'] - rw [dif_neg (gt_irrefl i), extendToSucc_map_le_succ] + rw [← arrowMap, ← arrowMap, arrowMap_functor hj iter l₁ l₂ _ (hl₂.trans hij), + arrow_mk_mapObj] + apply congr_arrowMap + · rw [arrowMap_functor_to_top _ _ _ hk, ← arrowι_def _ hi] + congr 1 + apply Arrow.functor_ext + rintro ⟨l₁, hl₁⟩ ⟨l₂, hl₂⟩ f dsimp - rw [id_comp, comp_id] - erw [ε.naturality_assoc] - isColimit i hi hij := by - have hij' : i ≤ j := by - obtain hij | rfl := hij.lt_or_eq - · exact (Order.lt_succ_iff_of_not_isMax hj).1 hij - · exfalso - exact Order.not_isSuccLimit_succ_of_not_isMax hj hi - refine (IsColimit.precomposeHomEquiv - (isoWhiskerLeft (monotone_inclusion_lt_le_of_le hij').functor - (extendToSuccRestrictionLEIso hj iter.F (whiskerLeft _ ε))).symm _).1 - (IsColimit.ofIsoColimit (iter.isColimit i hi hij') - (Iso.symm (Cocones.ext (extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨i, hij'⟩) - (fun ⟨k, hk⟩ ↦ ?_)))) - dsimp - rw [assoc, extendToSuccObjIso_hom_naturality hj iter.F (whiskerLeft _ ε)] - dsimp - rw [Iso.inv_hom_id_assoc] + rw [← arrowMap, arrow_mk_mapObj, arrowMap_functor _ _ _ _ _ hl₂, arrow_mk_mapObj] + +variable (Φ) + +instance nonempty (j : J) : Nonempty (Φ.Iteration j) := by + induction j using SuccOrder.limitRecOn with + | hm i hi => + obtain rfl : i = ⊥ := by simpa using hi + exact ⟨mkOfBot Φ J⟩ + | hs i hi hi' => exact ⟨mkOfSucc hi hi'.some⟩ + | hl i hi hi' => exact ⟨mkOfLimit hi (fun a ha ↦ (hi' a ha).some)⟩ end Iteration -end Functor +end SuccStruct + +end SmallObject end CategoryTheory diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean deleted file mode 100644 index 5e804f4b551037..00000000000000 --- a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean +++ /dev/null @@ -1,249 +0,0 @@ -/- -Copyright (c) 2024 Joël Riou. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joël Riou --/ -import Mathlib.CategoryTheory.SmallObject.Iteration.Basic - -/-! -# Uniqueness of morphisms in the category of iterations of functors - -Given a functor `Φ : C ⥤ C` and a natural transformation `ε : 𝟭 C ⟶ Φ`, -we show in this file that there exists a unique morphism -between two arbitrary objects in the category `Functor.Iteration ε j` -when `j : J` and `J` is a well orderered set. - --/ - -universe u - -namespace CategoryTheory - -open Category Limits - -variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ} - {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] - -namespace Functor - -namespace Iteration - -namespace Hom - -/-- The (unique) morphism between two objects in `Iteration ε ⊥` -/ -def mkOfBot (iter₁ iter₂ : Iteration ε (⊥ : J)) : iter₁ ⟶ iter₂ where - natTrans := - { app := fun ⟨i, hi⟩ => eqToHom (by congr; simpa using hi) ≫ iter₁.isoZero.hom ≫ - iter₂.isoZero.inv ≫ eqToHom (by congr; symm; simpa using hi) - naturality := fun ⟨i, hi⟩ ⟨k, hk⟩ φ => by - obtain rfl : i = ⊥ := by simpa using hi - obtain rfl : k = ⊥ := by simpa using hk - obtain rfl : φ = 𝟙 _ := rfl - simp } - natTrans_app_succ i hi := by simp at hi - -section - -variable {i : J} {iter₁ iter₂ : Iteration ε (Order.succ i)} - (hi : ¬IsMax i) (φ : iter₁.trunc (SuccOrder.le_succ i) ⟶ iter₂.trunc (SuccOrder.le_succ i)) - -/-- Auxiliary definition for `mkOfSucc`. -/ -noncomputable def mkOfSuccNatTransApp (k : J) (hk : k ≤ Order.succ i) : - iter₁.F.obj ⟨k, hk⟩ ⟶ iter₂.F.obj ⟨k, hk⟩ := - if hk' : k = Order.succ i then - eqToHom (by subst hk'; rfl) ≫ (iter₁.isoSucc i (Order.lt_succ_of_not_isMax hi)).hom ≫ - whiskerRight (φ.natTrans.app ⟨i, by simp⟩) _ ≫ - (iter₂.isoSucc i (Order.lt_succ_of_not_isMax hi)).inv ≫ - eqToHom (by subst hk'; rfl) - else - φ.natTrans.app ⟨k, Order.le_of_lt_succ (by - obtain hk | rfl := hk.lt_or_eq - · exact hk - · tauto)⟩ - -lemma mkOfSuccNatTransApp_eq_of_le (k : J) (hk : k ≤ i) : - mkOfSuccNatTransApp hi φ k (hk.trans (Order.le_succ i)) = - φ.natTrans.app ⟨k, hk⟩ := - dif_neg (by rintro rfl; simpa using lt_of_le_of_lt hk (Order.lt_succ_of_not_isMax hi)) - -@[simp] -lemma mkOfSuccNatTransApp_succ_eq : - mkOfSuccNatTransApp hi φ (Order.succ i) (by rfl) = - (iter₁.isoSucc i (Order.lt_succ_of_not_isMax hi)).hom ≫ - whiskerRight (φ.natTrans.app ⟨i, by simp⟩) _ ≫ - (iter₂.isoSucc i (Order.lt_succ_of_not_isMax hi)).inv := by - dsimp [mkOfSuccNatTransApp] - rw [dif_pos rfl, comp_id, id_comp] - -/-- Auxiliary definition for `mkOfSucc`. -/ -@[simps] -noncomputable def mkOfSuccNatTrans : - iter₁.F ⟶ iter₂.F where - app := fun ⟨k, hk⟩ => mkOfSuccNatTransApp hi φ k hk - naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f => by - dsimp - have hk : k₁ ≤ k₂ := leOfHom f - obtain h₂ | rfl := hk₂.lt_or_eq - · replace h₂ : k₂ ≤ i := Order.le_of_lt_succ h₂ - rw [mkOfSuccNatTransApp_eq_of_le hi φ k₂ h₂, - mkOfSuccNatTransApp_eq_of_le hi φ k₁ (hk.trans h₂)] - exact natTrans_naturality φ k₁ k₂ hk h₂ - · obtain h₁ | rfl := hk.lt_or_eq - · have h₂ : k₁ ≤ i := Order.le_of_lt_succ h₁ - let f₁ : (⟨k₁, hk⟩ : { l | l ≤ Order.succ i}) ⟶ - ⟨i, Order.le_succ i⟩ := homOfLE h₂ - let f₂ : (⟨i, Order.le_succ i⟩ : Set.Iic (Order.succ i)) ⟶ - ⟨Order.succ i, by simp⟩ := homOfLE (Order.le_succ i) - obtain rfl : f = f₁ ≫ f₂ := rfl - rw [Functor.map_comp, Functor.map_comp, assoc, - mkOfSuccNatTransApp_eq_of_le hi φ k₁ h₂] - erw [← natTrans_naturality_assoc φ k₁ i h₂ (by rfl)] - rw [mkOfSuccNatTransApp_succ_eq] - dsimp - have ha : iter₁.F.map f₂ = iter₁.mapSucc i (Order.lt_succ_of_not_isMax hi) := rfl - have hb : iter₂.F.map f₂ = iter₂.mapSucc i (Order.lt_succ_of_not_isMax hi) := rfl - rw [ha, hb] - rw [iter₁.mapSucc_eq i, iter₂.mapSucc_eq i, assoc, - Iso.inv_hom_id_assoc] - ext X - dsimp - rw [← ε.naturality_assoc] - rfl - · obtain rfl : f = 𝟙 _ := rfl - rw [Functor.map_id, Functor.map_id, id_comp, comp_id] - -end - -/-- The (unique) morphism between two objects in `Iteration ε (Order.succ i)`, -assuming we have a morphism between the truncations to `Iteration ε i`. -/ -noncomputable def mkOfSucc - {i : J} (iter₁ iter₂ : Iteration ε (Order.succ i)) (hi : ¬IsMax i) - (φ : iter₁.trunc (SuccOrder.le_succ i) ⟶ iter₂.trunc (SuccOrder.le_succ i)) : - iter₁ ⟶ iter₂ where - natTrans := mkOfSuccNatTrans hi φ - natTrans_app_zero := by - dsimp - rw [mkOfSuccNatTransApp_eq_of_le _ _ _ bot_le, φ.natTrans_app_zero] - rfl - natTrans_app_succ k hk := by - obtain hk' | rfl := (Order.le_of_lt_succ hk).lt_or_eq - · dsimp - rw [mkOfSuccNatTransApp_eq_of_le hi φ k hk'.le, - mkOfSuccNatTransApp_eq_of_le hi φ (Order.succ k) (Order.succ_le_of_lt hk'), - φ.natTrans_app_succ _ hk'] - rfl - · simp [mkOfSuccNatTransApp_eq_of_le hi φ k (by rfl)] - -variable {j : J} {iter₁ iter₂ : Iteration ε j} - -section - -variable (φ : ∀ (i : J) (hi : i < j), iter₁.trunc hi.le ⟶ iter₂.trunc hi.le) - [WellFoundedLT J] (hj : Order.IsSuccLimit j) - -/-- Auxiliary definition for `mkOfLimit`. -/ -def mkOfLimitNatTransApp (i : J) (hi : i ≤ j) : - iter₁.F.obj ⟨i, hi⟩ ⟶ iter₂.F.obj ⟨i, hi⟩ := - if h : i < j - then - (φ i h).natTrans.app ⟨i, by simp⟩ - else by - obtain rfl : i = j := by - obtain h' | rfl := hi.lt_or_eq - · exfalso - exact h h' - · rfl - exact (iter₁.isColimit i hj (by simp)).desc (Cocone.mk _ - { app := fun ⟨k, hk⟩ => (φ k hk).natTrans.app ⟨k, by simp⟩ ≫ - iter₂.F.map (homOfLE (by exact hk.le)) - naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f => by - have hf : k₁ ≤ k₂ := by simpa using leOfHom f - dsimp - rw [comp_id, congr_app (φ k₁ hk₁) ((truncFunctor ε hf).map (φ k₂ hk₂))] - erw [natTrans_naturality_assoc (φ k₂ hk₂) k₁ k₂ hf (by rfl)] - dsimp - rw [← Functor.map_comp, homOfLE_comp] }) - -lemma mkOfLimitNatTransApp_eq_of_lt (i : J) (hi : i < j) : - mkOfLimitNatTransApp φ hj i hi.le = (φ i hi).natTrans.app ⟨i, by simp⟩ := - dif_pos hi - -lemma mkOfLimitNatTransApp_naturality_top (i : J) (hi : i < j) : - iter₁.F.map (homOfLE (by simpa using hi.le) : ⟨i, hi.le⟩ ⟶ ⟨j, by simp⟩) ≫ - mkOfLimitNatTransApp φ hj j (by rfl) = - mkOfLimitNatTransApp φ hj i hi.le ≫ iter₂.F.map (homOfLE (by simpa using hi.le)) := by - rw [mkOfLimitNatTransApp_eq_of_lt φ hj i hi, mkOfLimitNatTransApp, dif_neg (by simp)] - exact (iter₁.isColimit j hj (by rfl)).fac _ ⟨i, hi⟩ - -/-- Auxiliary definition for `mkOfLimit`. -/ -@[simps] -def mkOfLimitNatTrans : iter₁.F ⟶ iter₂.F where - app := fun ⟨k, hk⟩ => mkOfLimitNatTransApp φ hj k hk - naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f => by - have hk : k₁ ≤ k₂ := leOfHom f - obtain h₂ | rfl := hk₂.lt_or_eq - · dsimp - rw [mkOfLimitNatTransApp_eq_of_lt _ hj k₂ h₂, - mkOfLimitNatTransApp_eq_of_lt _ hj k₁ (lt_of_le_of_lt hk h₂), - congr_app (φ k₁ (lt_of_le_of_lt hk h₂)) ((truncFunctor ε hk).map (φ k₂ h₂))] - exact natTrans_naturality (φ k₂ h₂) k₁ k₂ hk (by rfl) - · obtain h₁ | rfl := hk₁.lt_or_eq - · exact mkOfLimitNatTransApp_naturality_top _ hj _ h₁ - · obtain rfl : f = 𝟙 _ := rfl - simp only [map_id, id_comp, comp_id] - -/-- The (unique) morphism between two objects in `Iteration ε j` when `j` is a limit element, -assuming we have a morphism between the truncations to `Iteration ε i` for all `i < j`. -/ -def mkOfLimit : iter₁ ⟶ iter₂ where - natTrans := mkOfLimitNatTrans φ hj - natTrans_app_zero := by - simp [mkOfLimitNatTransApp_eq_of_lt φ _ ⊥ (by simpa only [bot_lt_iff_ne_bot] using hj.ne_bot)] - natTrans_app_succ i h := by - dsimp - have h' := hj.succ_lt h - rw [mkOfLimitNatTransApp_eq_of_lt φ hj _ h', - (φ _ h').natTrans_app_succ i (Order.lt_succ_of_not_isMax (not_isMax_of_lt h)), - mkOfLimitNatTransApp_eq_of_lt φ _ _ h, - congr_app (φ i h) ((truncFunctor ε (Order.le_succ i)).map (φ (Order.succ i) h'))] - dsimp - -end - -variable [WellFoundedLT J] - -instance : Nonempty (iter₁ ⟶ iter₂) := by - let P := fun (i : J) => ∀ (hi : i ≤ j), - Nonempty ((truncFunctor ε hi).obj iter₁ ⟶ (truncFunctor ε hi).obj iter₂) - suffices ∀ i, P i from this j (by rfl) - intro i - induction i using SuccOrder.limitRecOn with - | hm i hi => - obtain rfl : i = ⊥ := by simpa using hi - exact fun hi' ↦ ⟨Hom.mkOfBot _ _⟩ - | hs i hi hi' => - exact fun hi'' ↦ ⟨Hom.mkOfSucc _ _ hi (hi' ((Order.le_succ i).trans hi'')).some⟩ - | hl i hi hi' => - exact fun hi'' ↦ ⟨Hom.mkOfLimit (fun k hk ↦ (hi' k hk (hk.le.trans hi'')).some) hi⟩ - -noncomputable instance : Unique (iter₁ ⟶ iter₂) := - uniqueOfSubsingleton (Nonempty.some inferInstance) - -end Hom - -variable [WellFoundedLT J] {j : J} (iter₁ iter₂ iter₃ : Iteration ε j) - -/-- The canonical isomorphism between two objects in the category `Iteration ε j`. -/ -noncomputable def iso : iter₁ ≅ iter₂ where - hom := default - inv := default - -@[simp] -lemma iso_refl : iso iter₁ iter₁ = Iso.refl _ := by aesop_cat - -lemma iso_trans : iso iter₁ iter₂ ≪≫ iso iter₂ iter₃ = iso iter₁ iter₃ := by aesop_cat - -end Iteration - -end Functor - -end CategoryTheory diff --git a/Mathlib/Combinatorics/Enumerative/Composition.lean b/Mathlib/Combinatorics/Enumerative/Composition.lean index fcf38ce5355100..1583aa24ea0554 100644 --- a/Mathlib/Combinatorics/Enumerative/Composition.lean +++ b/Mathlib/Combinatorics/Enumerative/Composition.lean @@ -478,7 +478,7 @@ theorem eq_ones_iff_length {c : Composition n} : c = ones n ↔ c.length = n := _ < ∑ i : Fin c.length, c.blocksFun i := by { obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H - rw [← ofFn_blocksFun, mem_ofFn c.blocksFun, Set.mem_range] at hi + rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi rw [← hj] at i_blocks exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩ diff --git a/Mathlib/Computability/Primrec.lean b/Mathlib/Computability/Primrec.lean index a4c9369593bb28..5c47e48f3f4da5 100644 --- a/Mathlib/Computability/Primrec.lean +++ b/Mathlib/Computability/Primrec.lean @@ -619,15 +619,17 @@ theorem list_findIdx₁ {p : α → β → Bool} (hp : Primrec₂ p) : | a :: l => (cond (hp.comp .id (const a)) (const 0) (succ.comp (list_findIdx₁ hp l))).of_eq fun n => by simp [List.findIdx_cons] -theorem list_indexOf₁ [DecidableEq α] (l : List α) : Primrec fun a => l.indexOf a := +theorem list_idxOf₁ [DecidableEq α] (l : List α) : Primrec fun a => l.idxOf a := list_findIdx₁ (.swap .beq) l +@[deprecated (since := "2025-01-30")] alias list_indexOf₁ := list_idxOf₁ + theorem dom_fintype [Finite α] (f : α → σ) : Primrec f := let ⟨l, _, m⟩ := Finite.exists_univ_list α option_some_iff.1 <| by haveI := decidableEqOfEncodable α - refine ((list_get?₁ (l.map f)).comp (list_indexOf₁ l)).of_eq fun a => ?_ - rw [List.get?_eq_getElem?, List.getElem?_map, List.getElem?_indexOf (m a), Option.map_some'] + refine ((list_get?₁ (l.map f)).comp (list_idxOf₁ l)).of_eq fun a => ?_ + rw [List.get?_eq_getElem?, List.getElem?_map, List.getElem?_idxOf (m a), Option.map_some'] -- Porting note: These are new lemmas -- I added it because it actually simplified the proofs @@ -952,9 +954,11 @@ theorem list_findIdx {f : α → List β} {p : α → β → Bool} to₂ <| cond (hp.comp fst <| fst.comp snd) (const 0) (succ.comp <| snd.comp snd)).of_eq fun a => by dsimp; induction f a <;> simp [List.findIdx_cons, *] -theorem list_indexOf [DecidableEq α] : Primrec₂ (@List.indexOf α _) := +theorem list_idxOf [DecidableEq α] : Primrec₂ (@List.idxOf α _) := to₂ <| list_findIdx snd <| Primrec.beq.comp₂ snd.to₂ (fst.comp fst).to₂ +@[deprecated (since := "2025-01-30")] alias list_indexOf := list_idxOf + theorem nat_strong_rec (f : α → ℕ → σ) {g : α → List σ → Option σ} (hg : Primrec₂ g) (H : ∀ a n, g a ((List.range n).map (f a)) = some (f a n)) : Primrec₂ f := suffices Primrec₂ fun a n => (List.range n).map (f a) from diff --git a/Mathlib/Computability/RegularExpressions.lean b/Mathlib/Computability/RegularExpressions.lean index a1922965cec30b..ebc30c43127244 100644 --- a/Mathlib/Computability/RegularExpressions.lean +++ b/Mathlib/Computability/RegularExpressions.lean @@ -17,11 +17,6 @@ computer science such as the POSIX standard. * Show that this regular expressions and DFA/NFA's are equivalent. -/ --- Porting note: this has been commented out --- * `attribute [pattern] has_mul.mul` has been added into this file, it could be moved. - - - open List Set open Computability @@ -72,9 +67,6 @@ instance : Zero (RegularExpression α) := instance : Pow (RegularExpression α) ℕ := ⟨fun n r => npowRec r n⟩ --- Porting note: declaration in an imported module --- attribute [match_pattern] Mul.mul - @[simp] theorem zero_def : (zero : RegularExpression α) = 0 := rfl @@ -92,8 +84,6 @@ theorem comp_def (P Q : RegularExpression α) : comp P Q = P * Q := rfl -- This was renamed to `matches'` during the port of Lean 4 as `matches` is a reserved word. -#adaptation_note /-- nightly-2024-02-25 - we need to write `comp x y` in the pattern `comp P Q`, instead of `x * y`. -/ /-- `matches' P` provides a language which contains all strings that `P` matches -/ -- Porting note: was '@[simp] but removed based on -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simpNF.20issues.20in.20Computability.2ERegularExpressions.20!4.232306/near/328355362 @@ -102,7 +92,7 @@ def matches' : RegularExpression α → Language α | 1 => 1 | char a => {[a]} | P + Q => P.matches' + Q.matches' - | comp P Q => P.matches' * Q.matches' + | P * Q => P.matches' * Q.matches' | star P => P.matches'∗ @[simp] @@ -136,22 +126,18 @@ theorem matches'_pow (P : RegularExpression α) : ∀ n : ℕ, (P ^ n).matches' theorem matches'_star (P : RegularExpression α) : P.star.matches' = P.matches'∗ := rfl -#adaptation_note /-- nightly-2024-02-25 - we need to write `comp x y` in the pattern `comp P Q`, instead of `x * y`. -/ /-- `matchEpsilon P` is true if and only if `P` matches the empty string -/ def matchEpsilon : RegularExpression α → Bool | 0 => false | 1 => true | char _ => false | P + Q => P.matchEpsilon || Q.matchEpsilon - | comp P Q => P.matchEpsilon && Q.matchEpsilon + | P * Q => P.matchEpsilon && Q.matchEpsilon | star _P => true section DecidableEq variable [DecidableEq α] -#adaptation_note /-- nightly-2024-02-25 - we need to write `comp x y` in the pattern `comp P Q`, instead of `x * y`. -/ /-- `P.deriv a` matches `x` if `P` matches `a :: x`, the Brzozowski derivative of `P` with respect to `a` -/ def deriv : RegularExpression α → α → RegularExpression α @@ -159,7 +145,7 @@ def deriv : RegularExpression α → α → RegularExpression α | 1, _ => 0 | char a₁, a₂ => if a₁ = a₂ then 1 else 0 | P + Q, a => deriv P a + deriv Q a - | comp P Q, a => if P.matchEpsilon then deriv P a * Q + deriv Q a else deriv P a * Q + | P * Q, a => if P.matchEpsilon then deriv P a * Q + deriv Q a else deriv P a * Q | star P, a => deriv P a * star P @[simp] @@ -343,8 +329,6 @@ instance (P : RegularExpression α) : DecidablePred (· ∈ P.matches') := fun _ end DecidableEq -#adaptation_note /-- nightly-2024-02-25 - we need to write `comp x y` in the pattern `comp P Q`, instead of `x * y`. -/ /-- Map the alphabet of a regular expression. -/ @[simp] def map (f : α → β) : RegularExpression α → RegularExpression β @@ -352,7 +336,7 @@ def map (f : α → β) : RegularExpression α → RegularExpression β | 1 => 1 | char a => char (f a) | R + S => map f R + map f S - | comp R S => map f R * map f S + | R * S => map f R * map f S | star R => star (map f R) @[simp] @@ -361,31 +345,24 @@ protected theorem map_pow (f : α → β) (P : RegularExpression α) : | 0 => by unfold map; rfl | n + 1 => (congr_arg (· * map f P) (RegularExpression.map_pow f P n) :) -#adaptation_note /-- nightly-2024-02-25 - we need to write `comp x y` in the pattern `comp P Q`, instead of `x * y`. -/ @[simp] theorem map_id : ∀ P : RegularExpression α, P.map id = P | 0 => rfl | 1 => rfl | char _ => rfl | R + S => by simp_rw [map, map_id] - | comp R S => by simp_rw [map, map_id]; rfl + | R * S => by simp_rw [map, map_id] | star R => by simp_rw [map, map_id] -#adaptation_note /-- nightly-2024-02-25 - we need to write `comp x y` in the pattern `comp P Q`, instead of `x * y`. -/ @[simp] theorem map_map (g : β → γ) (f : α → β) : ∀ P : RegularExpression α, (P.map f).map g = P.map (g ∘ f) | 0 => rfl | 1 => rfl | char _ => rfl | R + S => by simp only [map, Function.comp_apply, map_map] - | comp R S => by simp only [map, Function.comp_apply, map_map] + | R * S => by simp only [map, Function.comp_apply, map_map] | star R => by simp only [map, Function.comp_apply, map_map] -#adaptation_note /-- nightly-2024-02-25 - we need to write `comp x y` in the pattern `comp R S`, - instead of `x * y` (and the `erw` was just `rw`). -/ /-- The language of the map is the map of the language. -/ @[simp] theorem matches'_map (f : α → β) : @@ -396,7 +373,7 @@ theorem matches'_map (f : α → β) : rw [eq_comm] exact image_singleton | R + S => by simp only [matches'_map, map, matches'_add, map_add] - | comp R S => by simp [matches'_map] + | R * S => by simp [matches'_map] | star R => by simp [matches'_map] end RegularExpression diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index 41d00bd2897614..016b08669bf2b3 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -596,10 +596,6 @@ lemma _root_.finCongr_symm_apply_coe (h : m = n) (k : Fin n) : ((finCongr h).sym a generic theorem about `cast`. -/ lemma _root_.finCongr_eq_equivCast (h : n = m) : finCongr h = .cast (h ▸ rfl) := by subst h; simp -@[simp] -theorem cast_zero {n' : ℕ} [NeZero n] {h : n = n'} : (0 : Fin n).cast h = - by { haveI : NeZero n' := by {rw [← h]; infer_instance}; exact 0} := rfl - /-- While in many cases `Fin.cast` is better than `Equiv.cast`/`cast`, sometimes we want to apply a generic theorem about `cast`. -/ theorem cast_eq_cast (h : n = m) : (Fin.cast h : Fin n → Fin m) = _root_.cast (h ▸ rfl) := by diff --git a/Mathlib/Data/FinEnum.lean b/Mathlib/Data/FinEnum.lean index d928b5d459a79a..3743426362fb7e 100644 --- a/Mathlib/Data/FinEnum.lean +++ b/Mathlib/Data/FinEnum.lean @@ -46,8 +46,8 @@ def ofNodupList [DecidableEq α] (xs : List α) (h : ∀ x : α, x ∈ xs) (h' : FinEnum α where card := xs.length equiv := - ⟨fun x => ⟨xs.indexOf x, by rw [List.indexOf_lt_length_iff]; apply h⟩, xs.get, fun x => by simp, - fun i => by ext; simp [List.indexOf_getElem h']⟩ + ⟨fun x => ⟨xs.idxOf x, by rw [List.idxOf_lt_length_iff]; apply h⟩, xs.get, fun x => by simp, + fun i => by ext; simp [List.idxOf_getElem h']⟩ /-- create a `FinEnum` instance from an exhaustive list; duplicates are removed -/ def ofList [DecidableEq α] (xs : List α) (h : ∀ x : α, x ∈ xs) : FinEnum α := diff --git a/Mathlib/Data/Finset/Sort.lean b/Mathlib/Data/Finset/Sort.lean index d4354b5039a5bf..4b49c0b4443dd2 100644 --- a/Mathlib/Data/Finset/Sort.lean +++ b/Mathlib/Data/Finset/Sort.lean @@ -170,7 +170,7 @@ theorem coe_orderIsoOfFin_apply (s : Finset α) {k : ℕ} (h : s.card = k) (i : rfl theorem orderIsoOfFin_symm_apply (s : Finset α) {k : ℕ} (h : s.card = k) (x : s) : - ↑((s.orderIsoOfFin h).symm x) = (s.sort (· ≤ ·)).indexOf ↑x := + ↑((s.orderIsoOfFin h).symm x) = (s.sort (· ≤ ·)).idxOf ↑x := rfl theorem orderEmbOfFin_apply (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k) : diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 569361c5a5b429..55bb99dc01ffa2 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -29,10 +29,6 @@ open Nat hiding one_pos namespace List --- Renamed in lean core; to be removed with the version bump. -alias replicate_append_replicate := append_replicate_replicate -alias append_eq_nil_iff := append_eq_nil - universe u v w variable {ι : Type*} {α : Type u} {β : Type v} {γ : Type w} {l₁ l₂ : List α} @@ -662,24 +658,24 @@ variable [DecidableEq α] The ported versions of the earlier proofs are given in comments. -/ --- indexOf_cons_eq _ rfl -@[simp] -theorem indexOf_cons_self {a : α} {l : List α} : indexOf a (a :: l) = 0 := by - rw [indexOf, findIdx_cons, beq_self_eq_true, cond] -- fun e => if_pos e -theorem indexOf_cons_eq {a b : α} (l : List α) : b = a → indexOf a (b :: l) = 0 - | e => by rw [← e]; exact indexOf_cons_self +theorem idxOf_cons_eq {a b : α} (l : List α) : b = a → idxOf a (b :: l) = 0 + | e => by rw [← e]; exact idxOf_cons_self + +@[deprecated (since := "2025-01-30")] alias indexOf_cons_eq := idxOf_cons_eq -- fun n => if_neg n @[simp] -theorem indexOf_cons_ne {a b : α} (l : List α) : b ≠ a → indexOf a (b :: l) = succ (indexOf a l) - | h => by simp only [indexOf, findIdx_cons, Bool.cond_eq_ite, beq_iff_eq, h, ite_false] +theorem idxOf_cons_ne {a b : α} (l : List α) : b ≠ a → idxOf a (b :: l) = succ (idxOf a l) + | h => by simp only [idxOf, findIdx_cons, Bool.cond_eq_ite, beq_iff_eq, h, ite_false] + +@[deprecated (since := "2025-01-30")] alias indexOf_cons_ne := idxOf_cons_ne -theorem indexOf_eq_length_iff {a : α} {l : List α} : indexOf a l = length l ↔ a ∉ l := by +theorem idxOf_eq_length_iff {a : α} {l : List α} : idxOf a l = length l ↔ a ∉ l := by induction' l with b l ih · exact iff_of_true rfl (not_mem_nil _) - simp only [length, mem_cons, indexOf_cons, eq_comm] + simp only [length, mem_cons, idxOf_cons, eq_comm] rw [cond_eq_if] split_ifs with h <;> simp at h · exact iff_of_false (by rintro ⟨⟩) fun H => H <| Or.inl h.symm @@ -687,42 +683,47 @@ theorem indexOf_eq_length_iff {a : α} {l : List α} : indexOf a l = length l rw [← ih] exact succ_inj' -@[deprecated (since := "2025-01-28")] -alias indexOf_eq_length := indexOf_eq_length_iff - @[simp] -theorem indexOf_of_not_mem {l : List α} {a : α} : a ∉ l → indexOf a l = length l := - indexOf_eq_length_iff.2 +theorem idxOf_of_not_mem {l : List α} {a : α} : a ∉ l → idxOf a l = length l := + idxOf_eq_length_iff.2 + +@[deprecated (since := "2025-01-30")] alias indexOf_of_not_mem := idxOf_of_not_mem -theorem indexOf_le_length {a : α} {l : List α} : indexOf a l ≤ length l := by +theorem idxOf_le_length {a : α} {l : List α} : idxOf a l ≤ length l := by induction' l with b l ih; · rfl - simp only [length, indexOf_cons, cond_eq_if, beq_iff_eq] + simp only [length, idxOf_cons, cond_eq_if, beq_iff_eq] by_cases h : b = a · rw [if_pos h]; exact Nat.zero_le _ · rw [if_neg h]; exact succ_le_succ ih -theorem indexOf_lt_length_iff {a} {l : List α} : indexOf a l < length l ↔ a ∈ l := - ⟨fun h => Decidable.byContradiction fun al => Nat.ne_of_lt h <| indexOf_eq_length_iff.2 al, - fun al => (lt_of_le_of_ne indexOf_le_length) fun h => indexOf_eq_length_iff.1 h al⟩ +@[deprecated (since := "2025-01-30")] alias indexOf_le_length := idxOf_le_length + +theorem idxOf_lt_length_iff {a} {l : List α} : idxOf a l < length l ↔ a ∈ l := + ⟨fun h => Decidable.byContradiction fun al => Nat.ne_of_lt h <| idxOf_eq_length_iff.2 al, + fun al => (lt_of_le_of_ne idxOf_le_length) fun h => idxOf_eq_length_iff.1 h al⟩ -@[deprecated (since := "2025-01-22")] alias indexOf_lt_length := indexOf_lt_length_iff +@[deprecated (since := "2025-01-30")] alias indexOf_lt_length_iff := idxOf_lt_length_iff -theorem indexOf_append_of_mem {a : α} (h : a ∈ l₁) : indexOf a (l₁ ++ l₂) = indexOf a l₁ := by +theorem idxOf_append_of_mem {a : α} (h : a ∈ l₁) : idxOf a (l₁ ++ l₂) = idxOf a l₁ := by induction' l₁ with d₁ t₁ ih · exfalso exact not_mem_nil a h rw [List.cons_append] by_cases hh : d₁ = a - · iterate 2 rw [indexOf_cons_eq _ hh] - rw [indexOf_cons_ne _ hh, indexOf_cons_ne _ hh, ih (mem_of_ne_of_mem (Ne.symm hh) h)] + · iterate 2 rw [idxOf_cons_eq _ hh] + rw [idxOf_cons_ne _ hh, idxOf_cons_ne _ hh, ih (mem_of_ne_of_mem (Ne.symm hh) h)] -theorem indexOf_append_of_not_mem {a : α} (h : a ∉ l₁) : - indexOf a (l₁ ++ l₂) = l₁.length + indexOf a l₂ := by +@[deprecated (since := "2025-01-30")] alias indexOf_append_of_mem := idxOf_append_of_mem + +theorem idxOf_append_of_not_mem {a : α} (h : a ∉ l₁) : + idxOf a (l₁ ++ l₂) = l₁.length + idxOf a l₂ := by induction' l₁ with d₁ t₁ ih · rw [List.nil_append, List.length, Nat.zero_add] - rw [List.cons_append, indexOf_cons_ne _ (ne_of_not_mem_cons h).symm, List.length, + rw [List.cons_append, idxOf_cons_ne _ (ne_of_not_mem_cons h).symm, List.length, ih (not_mem_of_not_mem_cons h), Nat.succ_add] +@[deprecated (since := "2025-01-30")] alias indexOf_append_of_not_mem := idxOf_append_of_not_mem + end IndexOf /-! ### nth element -/ @@ -775,35 +776,45 @@ theorem ext_getElem! [Inhabited α] (hl : length l₁ = length l₂) (h : ∀ n ext_getElem hl fun n h₁ h₂ ↦ by simpa only [← getElem!_pos] using h n @[simp] -theorem getElem_indexOf [DecidableEq α] {a : α} : ∀ {l : List α} (h : indexOf a l < l.length), - l[indexOf a l] = a +theorem getElem_idxOf [DecidableEq α] {a : α} : ∀ {l : List α} (h : idxOf a l < l.length), + l[idxOf a l] = a | b :: l, h => by by_cases h' : b = a <;> - simp [h', if_pos, if_false, getElem_indexOf] + simp [h', if_pos, if_false, getElem_idxOf] --- This is incorrectly named and should be `get_indexOf`; +@[deprecated (since := "2025-01-30")] alias getElem_indexOf := getElem_idxOf + +-- This is incorrectly named and should be `get_idxOf`; -- this already exists, so will require a deprecation dance. -theorem indexOf_get [DecidableEq α] {a : α} {l : List α} (h) : get l ⟨indexOf a l, h⟩ = a := by +theorem idxOf_get [DecidableEq α] {a : α} {l : List α} (h) : get l ⟨idxOf a l, h⟩ = a := by simp +@[deprecated (since := "2025-01-30")] alias indexOf_get := idxOf_get + @[simp] -theorem getElem?_indexOf [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : - l[indexOf a l]? = some a := by - rw [getElem?_eq_getElem, getElem_indexOf (indexOf_lt_length_iff.2 h)] +theorem getElem?_idxOf [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : + l[idxOf a l]? = some a := by + rw [getElem?_eq_getElem, getElem_idxOf (idxOf_lt_length_iff.2 h)] --- This is incorrectly named and should be `get?_indexOf`; +@[deprecated (since := "2025-01-30")] alias getElem?_indexOf := getElem?_idxOf + +-- This is incorrectly named and should be `get?_idxOf`; -- this already exists, so will require a deprecation dance. -theorem indexOf_get? [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : - get? l (indexOf a l) = some a := by simp [h] +theorem idxOf_get? [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : + get? l (idxOf a l) = some a := by simp [h] + +@[deprecated (since := "2025-01-30")] alias indexOf_get? := idxOf_get? -theorem indexOf_inj [DecidableEq α] {l : List α} {x y : α} (hx : x ∈ l) (hy : y ∈ l) : - indexOf x l = indexOf y l ↔ x = y := +theorem idxOf_inj [DecidableEq α] {l : List α} {x y : α} (hx : x ∈ l) (hy : y ∈ l) : + idxOf x l = idxOf y l ↔ x = y := ⟨fun h => by have x_eq_y : - get l ⟨indexOf x l, indexOf_lt_length_iff.2 hx⟩ = - get l ⟨indexOf y l, indexOf_lt_length_iff.2 hy⟩ := by + get l ⟨idxOf x l, idxOf_lt_length_iff.2 hx⟩ = + get l ⟨idxOf y l, idxOf_lt_length_iff.2 hy⟩ := by simp only [h] - simp only [indexOf_get] at x_eq_y; exact x_eq_y, fun h => by subst h; rfl⟩ + simp only [idxOf_get] at x_eq_y; exact x_eq_y, fun h => by subst h; rfl⟩ + +@[deprecated (since := "2025-01-30")] alias indexOf_inj := idxOf_inj theorem get_reverse' (l : List α) (n) (hn') : l.reverse.get n = l.get ⟨l.length - 1 - n, hn'⟩ := by diff --git a/Mathlib/Data/List/Count.lean b/Mathlib/Data/List/Count.lean index ff77b8257b8d55..e8305bd7e081b2 100644 --- a/Mathlib/Data/List/Count.lean +++ b/Mathlib/Data/List/Count.lean @@ -3,6 +3,7 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro -/ +import Batteries.Data.List.Perm import Mathlib.Logic.Function.Basic import Mathlib.Tactic.Common diff --git a/Mathlib/Data/List/Enum.lean b/Mathlib/Data/List/Enum.lean index 38f58ee6b82232..1bc5b003288bee 100644 --- a/Mathlib/Data/List/Enum.lean +++ b/Mathlib/Data/List/Enum.lean @@ -21,58 +21,31 @@ namespace List variable {α : Type*} -@[deprecated getElem?_enumFrom (since := "2024-08-15")] -theorem get?_enumFrom (n) (l : List α) (m) : - get? (enumFrom n l) m = (get? l m).map fun a => (n + m, a) := by - simp - -@[deprecated getElem?_enum (since := "2024-08-15")] -theorem get?_enum (l : List α) (n) : get? (enum l) n = (get? l n).map fun a => (n, a) := by - simp - -@[deprecated getElem_enumFrom (since := "2024-08-15")] -theorem get_enumFrom (l : List α) (n) (i : Fin (l.enumFrom n).length) : - (l.enumFrom n).get i = (n + i, l.get (i.cast enumFrom_length)) := by - simp - -@[deprecated getElem_enum (since := "2024-08-15")] -theorem get_enum (l : List α) (i : Fin l.enum.length) : - l.enum.get i = (i.1, l.get (i.cast enum_length)) := by - simp - -@[deprecated mk_add_mem_enumFrom_iff_getElem? (since := "2024-08-12")] -theorem mk_add_mem_enumFrom_iff_get? {n i : ℕ} {x : α} {l : List α} : - (n + i, x) ∈ enumFrom n l ↔ l.get? i = x := by - simp [mem_iff_get?] - -@[deprecated mk_mem_enumFrom_iff_le_and_getElem?_sub (since := "2024-08-12")] -theorem mk_mem_enumFrom_iff_le_and_get?_sub {n i : ℕ} {x : α} {l : List α} : - (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l.get? (i - n) = x := by - simp [mk_mem_enumFrom_iff_le_and_getElem?_sub] - -@[deprecated mk_mem_enum_iff_getElem? (since := "2024-08-15")] -theorem mk_mem_enum_iff_get? {i : ℕ} {x : α} {l : List α} : (i, x) ∈ enum l ↔ l.get? i = x := by - simp [enum, mk_mem_enumFrom_iff_le_and_getElem?_sub] - -set_option linter.deprecated false in -@[deprecated mem_enum_iff_getElem? (since := "2024-08-15")] -theorem mem_enum_iff_get? {x : ℕ × α} {l : List α} : x ∈ enum l ↔ l.get? x.1 = x.2 := - mk_mem_enum_iff_get? - -theorem forall_mem_enumFrom {l : List α} {n : ℕ} {p : ℕ × α → Prop} : - (∀ x ∈ l.enumFrom n, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (n + i, l[i]) := by - simp only [forall_mem_iff_getElem, getElem_enumFrom, enumFrom_length] - -theorem forall_mem_enum {l : List α} {p : ℕ × α → Prop} : - (∀ x ∈ l.enum, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (i, l[i]) := - forall_mem_enumFrom.trans <| by simp - -theorem exists_mem_enumFrom {l : List α} {n : ℕ} {p : ℕ × α → Prop} : - (∃ x ∈ l.enumFrom n, p x) ↔ ∃ (i : ℕ) (_ : i < length l), p (n + i, l[i]) := by - simp only [exists_mem_iff_getElem, getElem_enumFrom, enumFrom_length] - -theorem exists_mem_enum {l : List α} {p : ℕ × α → Prop} : - (∃ x ∈ l.enum, p x) ↔ ∃ (i : ℕ) (_ : i < length l), p (i, l[i]) := - exists_mem_enumFrom.trans <| by simp +theorem forall_mem_zipIdx {l : List α} {n : ℕ} {p : α × ℕ → Prop} : + (∀ x ∈ l.zipIdx n, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (l[i], n + i) := by + simp only [forall_mem_iff_getElem, getElem_zipIdx, length_zipIdx] + +/-- Variant of `forall_mem_zipIdx` with the `zipIdx` argument specialized to `0`. -/ +theorem forall_mem_zipIdx' {l : List α} {p : α × ℕ → Prop} : + (∀ x ∈ l.zipIdx, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (l[i], i) := + forall_mem_zipIdx.trans <| by simp + +theorem exists_mem_zipIdx {l : List α} {n : ℕ} {p : α × ℕ → Prop} : + (∃ x ∈ l.zipIdx n, p x) ↔ ∃ (i : ℕ) (_ : i < length l), p (l[i], n + i) := by + simp only [exists_mem_iff_getElem, getElem_zipIdx, length_zipIdx] + +/-- Variant of `exists_mem_zipIdx` with the `zipIdx` argument specialized to `0`. -/ +theorem exists_mem_zipIdx' {l : List α} {p : α × ℕ → Prop} : + (∃ x ∈ l.zipIdx, p x) ↔ ∃ (i : ℕ) (_ : i < length l), p (l[i], i) := + exists_mem_zipIdx.trans <| by simp + +@[deprecated (since := "2025-01-28")] +alias forall_mem_enumFrom := forall_mem_zipIdx +@[deprecated (since := "2025-01-28")] +alias forall_mem_enum := forall_mem_zipIdx' +@[deprecated (since := "2025-01-28")] +alias exists_mem_enumFrom := exists_mem_zipIdx +@[deprecated (since := "2025-01-28")] +alias exists_mem_enum := exists_mem_zipIdx' end List diff --git a/Mathlib/Data/List/FinRange.lean b/Mathlib/Data/List/FinRange.lean index de540552321459..4931507ccde7ae 100644 --- a/Mathlib/Data/List/FinRange.lean +++ b/Mathlib/Data/List/FinRange.lean @@ -60,12 +60,14 @@ theorem get_finRange {n : ℕ} {i : ℕ} (h) : theorem finRange_map_get (l : List α) : (finRange l.length).map l.get = l := List.ext_get (by simp) (by simp) -@[simp] theorem indexOf_finRange {k : ℕ} (i : Fin k) : (finRange k).indexOf i = i := by - have : (finRange k).indexOf i < (finRange k).length := indexOf_lt_length_iff.mpr (by simp) - have h₁ : (finRange k).get ⟨(finRange k).indexOf i, this⟩ = i := indexOf_get this +@[simp] theorem idxOf_finRange {k : ℕ} (i : Fin k) : (finRange k).idxOf i = i := by + have : (finRange k).idxOf i < (finRange k).length := idxOf_lt_length_iff.mpr (by simp) + have h₁ : (finRange k).get ⟨(finRange k).idxOf i, this⟩ = i := idxOf_get this have h₂ : (finRange k).get ⟨i, by simp⟩ = i := get_finRange _ simpa using (Nodup.get_inj_iff (nodup_finRange k)).mp (Eq.trans h₁ h₂.symm) +@[deprecated (since := "2025-01-30")] alias indexOf_finRange := idxOf_get + @[simp] theorem map_coe_finRange (n : ℕ) : ((finRange n) : List (Fin n)).map (Fin.val) = List.range n := by apply List.ext_getElem <;> simp diff --git a/Mathlib/Data/List/Forall2.lean b/Mathlib/Data/List/Forall2.lean index 0cb3064f00ac4d..cb0a1e713998c9 100644 --- a/Mathlib/Data/List/Forall2.lean +++ b/Mathlib/Data/List/Forall2.lean @@ -226,7 +226,8 @@ theorem rel_flatten : (Forall₂ (Forall₂ R) ⇒ Forall₂ R) flatten flatten @[deprecated (since := "2025-10-15")] alias rel_join := rel_flatten -theorem rel_flatMap : (Forall₂ R ⇒ (R ⇒ Forall₂ P) ⇒ Forall₂ P) List.flatMap List.flatMap := +theorem rel_flatMap : (Forall₂ R ⇒ (R ⇒ Forall₂ P) ⇒ Forall₂ P) + (Function.swap List.flatMap) (Function.swap List.flatMap) := fun _ _ h₁ _ _ h₂ => rel_flatten (rel_map (@h₂) h₁) @[deprecated (since := "2025-10-16")] alias rel_bind := rel_flatMap diff --git a/Mathlib/Data/List/Indexes.lean b/Mathlib/Data/List/Indexes.lean index e307495cd9f2cd..21c03a33508e0f 100644 --- a/Mathlib/Data/List/Indexes.lean +++ b/Mathlib/Data/List/Indexes.lean @@ -42,6 +42,7 @@ theorem mapIdx_append_one : ∀ {f : ℕ → α → β} {l : List α} {e : α}, mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e] := mapIdx_concat +set_option linter.deprecated false in @[deprecated "Deprecated without replacement." (since := "2025-01-29"), local simp] theorem map_enumFrom_eq_zipWith : ∀ (l : List α) (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i ↦ f (i + n)) (range (length l)) l := by @@ -68,11 +69,12 @@ theorem map_enumFrom_eq_zipWith : ∀ (l : List α) (n : ℕ) (f : ℕ → α @[deprecated (since := "2024-10-15")] alias mapIdx_eq_nil := mapIdx_eq_nil_iff +set_option linter.deprecated false in @[deprecated "Deprecated without replacement." (since := "2025-01-29")] theorem get_mapIdx (l : List α) (f : ℕ → α → β) (i : ℕ) (h : i < l.length) (h' : i < (l.mapIdx f).length := h.trans_le length_mapIdx.ge) : (l.mapIdx f).get ⟨i, h'⟩ = f i (l.get ⟨i, h⟩) := by - simp [mapIdx_eq_enum_map, enum_eq_zip_range] + simp [mapIdx_eq_zipIdx_map, enum_eq_zip_range] @[deprecated (since := "2024-08-19")] alias nthLe_mapIdx := get_mapIdx @@ -160,6 +162,7 @@ end MapIdx section FoldrIdx -- Porting note: Changed argument order of `foldrIdxSpec` to align better with `foldrIdx`. +set_option linter.deprecated false in /-- Specification of `foldrIdx`. -/ @[deprecated "Deprecated without replacement." (since := "2025-01-29")] def foldrIdxSpec (f : ℕ → α → β → β) (b : β) (as : List α) (start : ℕ) : β := @@ -205,6 +208,7 @@ theorem findIdxs_eq_map_indexesValues (p : α → Prop) [DecidablePred p] (as : section FoldlIdx -- Porting note: Changed argument order of `foldlIdxSpec` to align better with `foldlIdx`. +set_option linter.deprecated false in /-- Specification of `foldlIdx`. -/ @[deprecated "Deprecated without replacement." (since := "2025-01-29")] def foldlIdxSpec (f : ℕ → α → β → α) (a : α) (bs : List β) (start : ℕ) : α := @@ -257,6 +261,7 @@ section MapIdxM -- Porting note: `[Applicative m]` replaced by `[Monad m] [LawfulMonad m]` variable {m : Type u → Type v} [Monad m] +set_option linter.deprecated false in /-- Specification of `mapIdxMAux`. -/ @[deprecated "Deprecated without replacement." (since := "2025-01-29")] def mapIdxMAuxSpec {β} (f : ℕ → α → m β) (start : ℕ) (as : List α) : m (List β) := @@ -322,7 +327,7 @@ theorem mapIdxMAux'_eq_mapIdxMGo {α} (f : ℕ → α → m PUnit) (as : List α simp only [seqRight_eq, map_eq_pure_bind, seq_pure, LawfulMonad.bind_assoc, pure_bind] theorem mapIdxM'_eq_mapIdxM {α} (f : ℕ → α → m PUnit) (as : List α) : - mapIdxM' f as = mapIdxM as f *> pure PUnit.unit := + mapIdxM' f as = mapIdxM f as *> pure PUnit.unit := mapIdxMAux'_eq_mapIdxMGo f as #[] end MapIdxM' diff --git a/Mathlib/Data/List/Intervals.lean b/Mathlib/Data/List/Intervals.lean index 0ea92237b08225..bc6af1bfc374a3 100644 --- a/Mathlib/Data/List/Intervals.lean +++ b/Mathlib/Data/List/Intervals.lean @@ -81,7 +81,7 @@ theorem append_consecutive {n m l : ℕ} (hnm : n ≤ m) (hml : m ≤ l) : dsimp only [Ico] convert range'_append n (m-n) (l-m) 1 using 2 · rw [Nat.one_mul, Nat.add_sub_cancel' hnm] - · rw [Nat.sub_add_sub_cancel hml hnm] + · omega @[simp] theorem inter_consecutive (n m l : ℕ) : Ico n m ∩ Ico m l = [] := by diff --git a/Mathlib/Data/List/MinMax.lean b/Mathlib/Data/List/MinMax.lean index 1adc6b35b85fce..e069728cff22fc 100644 --- a/Mathlib/Data/List/MinMax.lean +++ b/Mathlib/Data/List/MinMax.lean @@ -185,10 +185,10 @@ theorem argmin_cons (f : α → β) (a : α) (l : List α) : variable [DecidableEq α] theorem index_of_argmax : - ∀ {l : List α} {m : α}, m ∈ argmax f l → ∀ {a}, a ∈ l → f m ≤ f a → l.indexOf m ≤ l.indexOf a + ∀ {l : List α} {m : α}, m ∈ argmax f l → ∀ {a}, a ∈ l → f m ≤ f a → l.idxOf m ≤ l.idxOf a | [], m, _, _, _, _ => by simp | hd :: tl, m, hm, a, ha, ham => by - simp only [indexOf_cons, argmax_cons, Option.mem_def] at hm ⊢ + simp only [idxOf_cons, argmax_cons, Option.mem_def] at hm ⊢ cases h : argmax f tl · rw [h] at hm simp_all @@ -206,12 +206,12 @@ theorem index_of_argmax : exact Nat.zero_le _ theorem index_of_argmin : - ∀ {l : List α} {m : α}, m ∈ argmin f l → ∀ {a}, a ∈ l → f a ≤ f m → l.indexOf m ≤ l.indexOf a := + ∀ {l : List α} {m : α}, m ∈ argmin f l → ∀ {a}, a ∈ l → f a ≤ f m → l.idxOf m ≤ l.idxOf a := @index_of_argmax _ βᵒᵈ _ _ _ theorem mem_argmax_iff : m ∈ argmax f l ↔ - m ∈ l ∧ (∀ a ∈ l, f a ≤ f m) ∧ ∀ a ∈ l, f m ≤ f a → l.indexOf m ≤ l.indexOf a := + m ∈ l ∧ (∀ a ∈ l, f a ≤ f m) ∧ ∀ a ∈ l, f m ≤ f a → l.idxOf m ≤ l.idxOf a := ⟨fun hm => ⟨argmax_mem hm, fun _ ha => le_of_mem_argmax ha hm, fun _ => index_of_argmax hm⟩, by rintro ⟨hml, ham, hma⟩ @@ -220,21 +220,21 @@ theorem mem_argmax_iff : · have := _root_.le_antisymm (hma n (argmax_mem harg) (le_of_mem_argmax hml harg)) (index_of_argmax harg hml (ham _ (argmax_mem harg))) - rw [(indexOf_inj hml (argmax_mem harg)).1 this, Option.mem_def]⟩ + rw [(idxOf_inj hml (argmax_mem harg)).1 this, Option.mem_def]⟩ theorem argmax_eq_some_iff : argmax f l = some m ↔ - m ∈ l ∧ (∀ a ∈ l, f a ≤ f m) ∧ ∀ a ∈ l, f m ≤ f a → l.indexOf m ≤ l.indexOf a := + m ∈ l ∧ (∀ a ∈ l, f a ≤ f m) ∧ ∀ a ∈ l, f m ≤ f a → l.idxOf m ≤ l.idxOf a := mem_argmax_iff theorem mem_argmin_iff : m ∈ argmin f l ↔ - m ∈ l ∧ (∀ a ∈ l, f m ≤ f a) ∧ ∀ a ∈ l, f a ≤ f m → l.indexOf m ≤ l.indexOf a := + m ∈ l ∧ (∀ a ∈ l, f m ≤ f a) ∧ ∀ a ∈ l, f a ≤ f m → l.idxOf m ≤ l.idxOf a := @mem_argmax_iff _ βᵒᵈ _ _ _ _ _ theorem argmin_eq_some_iff : argmin f l = some m ↔ - m ∈ l ∧ (∀ a ∈ l, f m ≤ f a) ∧ ∀ a ∈ l, f a ≤ f m → l.indexOf m ≤ l.indexOf a := + m ∈ l ∧ (∀ a ∈ l, f m ≤ f a) ∧ ∀ a ∈ l, f a ≤ f m → l.idxOf m ≤ l.idxOf a := mem_argmin_iff end LinearOrder diff --git a/Mathlib/Data/List/Nodup.lean b/Mathlib/Data/List/Nodup.lean index 084e0e51bba633..858af6ecd2ebd1 100644 --- a/Mathlib/Data/List/Nodup.lean +++ b/Mathlib/Data/List/Nodup.lean @@ -120,17 +120,21 @@ 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) -theorem indexOf_getElem [DecidableEq α] {l : List α} (H : Nodup l) (i : Nat) (h : i < l.length) : - indexOf l[i] l = i := - suffices (⟨indexOf l[i] l, indexOf_lt_length_iff.2 (getElem_mem _)⟩ : Fin l.length) = ⟨i, h⟩ +theorem idxOf_getElem [DecidableEq α] {l : List α} (H : Nodup l) (i : Nat) (h : i < l.length) : + idxOf l[i] l = i := + suffices (⟨idxOf l[i] l, idxOf_lt_length_iff.2 (getElem_mem _)⟩ : Fin l.length) = ⟨i, h⟩ from Fin.val_eq_of_eq this nodup_iff_injective_get.1 H (by simp) --- This is incorrectly named and should be `indexOf_get`; +@[deprecated (since := "2025-01-30")] alias indexOf_getElem := idxOf_getElem + +-- This is incorrectly named and should be `idxOf_get`; -- this already exists, so will require a deprecation dance. -theorem get_indexOf [DecidableEq α] {l : List α} (H : Nodup l) (i : Fin l.length) : - indexOf (get l i) l = i := by - simp [indexOf_getElem, H] +theorem get_idxOf [DecidableEq α] {l : List α} (H : Nodup l) (i : Fin l.length) : + idxOf (get l i) l = i := by + simp [idxOf_getElem, H] + +@[deprecated (since := "2025-01-30")] alias get_indexOf := get_idxOf theorem nodup_iff_count_le_one [DecidableEq α] {l : List α} : Nodup l ↔ ∀ a, count a l ≤ 1 := nodup_iff_sublist.trans <| @@ -343,7 +347,7 @@ protected theorem Nodup.set : theorem Nodup.map_update [DecidableEq α] {l : List α} (hl : l.Nodup) (f : α → β) (x : α) (y : β) : l.map (Function.update f x y) = - if x ∈ l then (l.map f).set (l.indexOf x) y else l.map f := by + if x ∈ l then (l.map f).set (l.idxOf x) y else l.map f := by induction' l with hd tl ihl; · simp rw [nodup_cons] at hl simp only [mem_cons, map, ihl hl.2] diff --git a/Mathlib/Data/List/NodupEquivFin.lean b/Mathlib/Data/List/NodupEquivFin.lean index 0edcc7b2aba6c0..5673bb3adebe14 100644 --- a/Mathlib/Data/List/NodupEquivFin.lean +++ b/Mathlib/Data/List/NodupEquivFin.lean @@ -50,8 +50,8 @@ the set of elements of `l`. -/ @[simps] def getEquiv (l : List α) (H : Nodup l) : Fin (length l) ≃ { x // x ∈ l } where toFun i := ⟨get l i, get_mem _ _⟩ - invFun x := ⟨indexOf (↑x) l, indexOf_lt_length_iff.2 x.2⟩ - left_inv i := by simp only [List.get_indexOf, eq_self_iff_true, Fin.eta, Subtype.coe_mk, H] + invFun x := ⟨idxOf (↑x) l, idxOf_lt_length_iff.2 x.2⟩ + left_inv i := by simp only [List.get_idxOf, eq_self_iff_true, Fin.eta, Subtype.coe_mk, H] right_inv x := by simp /-- If `l` lists all the elements of `α` without duplicates, then `List.get` defines @@ -63,8 +63,8 @@ decidable equality. -/ def getEquivOfForallMemList (l : List α) (nd : l.Nodup) (h : ∀ x : α, x ∈ l) : Fin l.length ≃ α where toFun i := l.get i - invFun a := ⟨_, indexOf_lt_length_iff.2 (h a)⟩ - left_inv i := by simp [List.indexOf_getElem, nd] + invFun a := ⟨_, idxOf_lt_length_iff.2 (h a)⟩ + left_inv i := by simp [List.idxOf_getElem, nd] right_inv a := by simp end Nodup @@ -92,7 +92,7 @@ theorem coe_getIso_apply : (H.getIso l i : α) = get l i := rfl @[simp] -theorem coe_getIso_symm_apply : ((H.getIso l).symm x : ℕ) = indexOf (↑x) l := +theorem coe_getIso_symm_apply : ((H.getIso l).symm x : ℕ) = idxOf (↑x) l := rfl end Sorted diff --git a/Mathlib/Data/List/OfFn.lean b/Mathlib/Data/List/OfFn.lean index 0e77e65fdc740f..b51e2171232bb3 100644 --- a/Mathlib/Data/List/OfFn.lean +++ b/Mathlib/Data/List/OfFn.lean @@ -123,15 +123,14 @@ theorem ofFn_getElem_eq_map {β : Type*} (l : List α) (f : α → β) : ofFn (fun i : Fin l.length => f <| l[(i : Nat)]) = l.map f := by rw [← Function.comp_def, ← map_ofFn, ofFn_getElem] --- not registered as a simp lemma, as otherwise it fires before `forall_mem_ofFn_iff` which --- is much more useful -theorem mem_ofFn {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ a ∈ Set.range f := by +-- Note there is a now another `mem_ofFn` defined in Lean, with an existential on the RHS, +-- which is marked as a simp lemma. +theorem mem_ofFn' {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ a ∈ Set.range f := by simp only [mem_iff_get, Set.mem_range, get_ofFn] exact ⟨fun ⟨i, hi⟩ => ⟨Fin.cast (by simp) i, hi⟩, fun ⟨i, hi⟩ => ⟨Fin.cast (by simp) i, hi⟩⟩ -@[simp] theorem forall_mem_ofFn_iff {n : ℕ} {f : Fin n → α} {P : α → Prop} : - (∀ i ∈ ofFn f, P i) ↔ ∀ j : Fin n, P (f j) := by simp only [mem_ofFn, Set.forall_mem_range] + (∀ i ∈ ofFn f, P i) ↔ ∀ j : Fin n, P (f j) := by simp @[simp] theorem ofFn_const : ∀ (n : ℕ) (c : α), (ofFn fun _ : Fin n => c) = replicate n c diff --git a/Mathlib/Data/List/ProdSigma.lean b/Mathlib/Data/List/ProdSigma.lean index 6e1aec6c08dede..e18598bb29ea0c 100644 --- a/Mathlib/Data/List/ProdSigma.lean +++ b/Mathlib/Data/List/ProdSigma.lean @@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Mario Carneiro -/ import Mathlib.Data.List.Basic import Mathlib.Data.Prod.Basic -import Mathlib.Data.Sigma.Basic /-! # Lists in product and sigma types diff --git a/Mathlib/Data/List/Sigma.lean b/Mathlib/Data/List/Sigma.lean index 5b5e7fba9dd66c..f449bb66953150 100644 --- a/Mathlib/Data/List/Sigma.lean +++ b/Mathlib/Data/List/Sigma.lean @@ -128,7 +128,10 @@ theorem nodupKeys_flatten {L : List (List (Sigma β))} : @[deprecated (since := "2024-10-15")] alias nodupKeys_join := nodupKeys_flatten -theorem nodup_enum_map_fst (l : List α) : (l.enum.map Prod.fst).Nodup := by simp [List.nodup_range] +theorem nodup_zipIdx_map_snd (l : List α) : (l.zipIdx.map Prod.snd).Nodup := by + simp [List.nodup_range'] + +@[deprecated (since := "2025-01-28")] alias nodup_enum_map_fst := nodup_zipIdx_map_snd theorem mem_ext {l₀ l₁ : List (Sigma β)} (nd₀ : l₀.Nodup) (nd₁ : l₁.Nodup) (h : ∀ x, x ∈ l₀ ↔ x ∈ l₁) : l₀ ~ l₁ := diff --git a/Mathlib/Data/List/Sublists.lean b/Mathlib/Data/List/Sublists.lean index cf9436cf681189..c403e3538cf540 100644 --- a/Mathlib/Data/List/Sublists.lean +++ b/Mathlib/Data/List/Sublists.lean @@ -367,9 +367,9 @@ theorem revzip_sublists (l : List α) : ∀ l₁ l₂, (l₁, l₂) ∈ revzip l rw [revzip] induction' l using List.reverseRecOn with l' a ih · intro l₁ l₂ h - simp? at h says + simp? at h says simp only [sublists_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons, zip_nil_right, - mem_singleton, Prod.mk.injEq] at h + mem_cons, Prod.mk.injEq, not_mem_nil, or_false] at h simp [h] · intro l₁ l₂ h rw [sublists_concat, reverse_append, zip_append (by simp), ← map_reverse, zip_map_right, diff --git a/Mathlib/Data/List/ToFinsupp.lean b/Mathlib/Data/List/ToFinsupp.lean index 3af2f3ea04c131..48590950ee13be 100644 --- a/Mathlib/Data/List/ToFinsupp.lean +++ b/Mathlib/Data/List/ToFinsupp.lean @@ -114,15 +114,18 @@ theorem toFinsupp_concat_eq_toFinsupp_add_single {R : Type*} [AddZeroClass R] (x addLeftEmbedding_apply, add_zero] -theorem toFinsupp_eq_sum_map_enum_single {R : Type*} [AddMonoid R] (l : List R) +theorem toFinsupp_eq_sum_mapIdx_single {R : Type*} [AddMonoid R] (l : List R) [DecidablePred (getD l · 0 ≠ 0)] : - toFinsupp l = (l.enum.map fun nr : ℕ × R => Finsupp.single nr.1 nr.2).sum := by + toFinsupp l = (l.mapIdx fun n r => Finsupp.single n r).sum := by /- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: `induction` fails to substitute `l = []` in `[DecidablePred (getD l · 0 ≠ 0)]`, so we manually do some `revert`/`intro` as a workaround -/ revert l; intro l induction l using List.reverseRecOn with | nil => exact toFinsupp_nil | append_singleton x xs ih => - classical simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih] + classical simp [toFinsupp_concat_eq_toFinsupp_add_single, ih] + +@[deprecated (since := "2025-01-28")] +alias toFinsupp_eq_sum_map_enum_single := toFinsupp_eq_sum_mapIdx_single end List diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean index 1ba10228980431..6954d22b815386 100644 --- a/Mathlib/Data/Nat/Defs.lean +++ b/Mathlib/Data/Nat/Defs.lean @@ -436,8 +436,6 @@ protected lemma div_ne_zero_iff : a / b ≠ 0 ↔ b ≠ 0 ∧ b ≤ a := by simp @[simp] protected lemma div_pos_iff : 0 < a / b ↔ 0 < b ∧ b ≤ a := by simp [Nat.pos_iff_ne_zero] -protected lemma div_pos (hba : b ≤ a) (hb : 0 < b) : 0 < a / b := Nat.div_pos_iff.2 ⟨hb, hba⟩ - lemma lt_mul_of_div_lt (h : a / c < b) (hc : 0 < c) : a < b * c := Nat.lt_of_not_ge <| Nat.not_le_of_gt h ∘ (Nat.le_div_iff_mul_le hc).2 @@ -518,9 +516,7 @@ protected lemma div_le_self' (m n : ℕ) : m / n ≤ m := by lemma two_mul_odd_div_two (hn : n % 2 = 1) : 2 * (n / 2) = n - 1 := by conv => rhs; rw [← Nat.mod_add_div n 2, hn, Nat.add_sub_cancel_left] -@[gcongr] -lemma div_le_div_left (hcb : c ≤ b) (hc : 0 < c) : a / b ≤ a / c := - (Nat.le_div_iff_mul_le hc).2 <| Nat.le_trans (Nat.mul_le_mul_left _ hcb) (div_mul_le_self _ _) +attribute [gcongr] div_le_div_left lemma div_eq_self : m / n = m ↔ m = 0 ∨ n = 1 := by constructor diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean index bde0bf0b51b409..7b3dfcc978157b 100644 --- a/Mathlib/Data/Nat/Digits.lean +++ b/Mathlib/Data/Nat/Digits.lean @@ -150,22 +150,22 @@ theorem ofDigits_eq_foldr {α : Type*} [Semiring α] (b : α) (L : List ℕ) : · dsimp [ofDigits] rw [ih] -theorem ofDigits_eq_sum_map_with_index_aux (b : ℕ) (l : List ℕ) : - ((List.range l.length).zipWith ((fun i a : ℕ => a * b ^ (i + 1))) l).sum = - b * ((List.range l.length).zipWith (fun i a => a * b ^ i) l).sum := by +theorem ofDigits_eq_sum_mapIdx_aux (b : ℕ) (l : List ℕ) : + (l.zipWith ((fun a i : ℕ => a * b ^ (i + 1))) (List.range l.length)).sum = + b * (l.zipWith (fun a i => a * b ^ i) (List.range l.length)).sum := by suffices - (List.range l.length).zipWith (fun i a : ℕ => a * b ^ (i + 1)) l = - (List.range l.length).zipWith (fun i a => b * (a * b ^ i)) l + l.zipWith (fun a i : ℕ => a * b ^ (i + 1)) (List.range l.length) = + l.zipWith (fun a i=> b * (a * b ^ i)) (List.range l.length) by simp [this] congr; ext; simp [pow_succ]; ring theorem ofDigits_eq_sum_mapIdx (b : ℕ) (L : List ℕ) : ofDigits b L = (L.mapIdx fun i a => a * b ^ i).sum := by - rw [List.mapIdx_eq_enum_map, List.enum_eq_zip_range, List.map_uncurry_zip_eq_zipWith, - ofDigits_eq_foldr] + rw [List.mapIdx_eq_zipIdx_map, List.zipIdx_eq_zip_range', List.map_zip_eq_zipWith, + ofDigits_eq_foldr, ← List.range_eq_range'] induction' L with hd tl hl · simp - · simpa [List.range_succ_eq_map, List.zipWith_map_left, ofDigits_eq_sum_map_with_index_aux] using + · simpa [List.range_succ_eq_map, List.zipWith_map_right, ofDigits_eq_sum_mapIdx_aux] using Or.inl hl @[simp] diff --git a/Mathlib/Data/Option/Basic.lean b/Mathlib/Data/Option/Basic.lean index d6f5815d92c9eb..a12db6bd272f94 100644 --- a/Mathlib/Data/Option/Basic.lean +++ b/Mathlib/Data/Option/Basic.lean @@ -152,16 +152,6 @@ theorem pmap_map (g : γ → α) (x : Option γ) (H) : pmap f (x.map g) H = pmap (fun a h ↦ f (g a) h) x fun _ h ↦ H _ (mem_map_of_mem _ h) := by cases x <;> simp only [map_none', map_some', pmap] -theorem map_pmap (g : β → γ) (f : ∀ a, p a → β) (x H) : - Option.map g (pmap f x H) = pmap (fun a h ↦ g (f a h)) x H := by - cases x <;> simp only [map_none', map_some', pmap] - --- Porting note: Can't simp tag this anymore because `pmap` simplifies --- @[simp] -theorem pmap_eq_map (p : α → Prop) (f : α → β) (x H) : - @pmap _ _ p (fun a _ ↦ f a) x H = Option.map f x := by - cases x <;> simp only [map_none', map_some', pmap] - theorem pmap_bind {α β γ} {x : Option α} {g : α → Option β} {p : β → Prop} {f : ∀ b, p b → γ} (H) (H' : ∀ (a : α), ∀ b ∈ g a, b ∈ x >>= g) : pmap f (x >>= g) H = x >>= fun a ↦ pmap f (g a) fun _ h ↦ H _ (H' a _ h) := by diff --git a/Mathlib/Data/Sigma/Basic.lean b/Mathlib/Data/Sigma/Basic.lean index 85bb264783fc71..50310134cc9742 100644 --- a/Mathlib/Data/Sigma/Basic.lean +++ b/Mathlib/Data/Sigma/Basic.lean @@ -50,12 +50,8 @@ instance instDecidableEqSigma [h₁ : DecidableEq α] [h₂ : ∀ a, DecidableEq | _, _, isFalse n => isFalse fun h ↦ Sigma.noConfusion h fun _ e₂ ↦ n <| eq_of_heq e₂ | _, _, _, _, isFalse n => isFalse fun h ↦ Sigma.noConfusion h fun e₁ _ ↦ n e₁ --- sometimes the built-in injectivity support does not work -@[simp] theorem mk.inj_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} : - Sigma.mk a₁ b₁ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ HEq b₁ b₂ := - ⟨fun h ↦ by cases h; simp, - fun ⟨h₁, h₂⟩ ↦ by subst h₁; rw [eq_of_heq h₂]⟩ + Sigma.mk a₁ b₁ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ HEq b₁ b₂ := by simp @[simp] theorem eta : ∀ x : Σa, β a, Sigma.mk x.1 x.2 = x @@ -225,11 +221,6 @@ instance decidableEq [h₁ : DecidableEq α] [h₂ : ∀ a, DecidableEq (β a)] | _, _, isFalse n => isFalse fun h ↦ PSigma.noConfusion h fun _ e₂ ↦ n <| eq_of_heq e₂ | _, _, _, _, isFalse n => isFalse fun h ↦ PSigma.noConfusion h fun e₁ _ ↦ n e₁ --- See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/porting.20data.2Esigma.2Ebasic/near/304855864 --- for an explanation of why this is currently needed. It generates `PSigma.mk.inj`. --- This could be done elsewhere. -gen_injective_theorems% PSigma - theorem mk.inj_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} : @PSigma.mk α β a₁ b₁ = @PSigma.mk α β a₂ b₂ ↔ a₁ = a₂ ∧ HEq b₁ b₂ := (Iff.intro PSigma.mk.inj) fun ⟨h₁, h₂⟩ ↦ diff --git a/Mathlib/Data/ULift.lean b/Mathlib/Data/ULift.lean index 29aed3723b5e7b..4fb68daa44d183 100644 --- a/Mathlib/Data/ULift.lean +++ b/Mathlib/Data/ULift.lean @@ -46,9 +46,7 @@ theorem up_surjective : Surjective (@up α) := theorem up_bijective : Bijective (@up α) := Equiv.plift.symm.bijective -@[simp] -theorem up_inj {x y : α} : up x = up y ↔ x = y := - up_injective.eq_iff +theorem up_inj {x y : α} : up x = up y ↔ x = y := by simp theorem down_surjective : Surjective (@down α) := Equiv.plift.surjective @@ -103,9 +101,7 @@ theorem up_surjective : Surjective (@up α) := theorem up_bijective : Bijective (@up α) := Equiv.ulift.symm.bijective -@[simp] -theorem up_inj {x y : α} : up x = up y ↔ x = y := - up_injective.eq_iff +theorem up_inj {x y : α} : up x = up y ↔ x = y := by simp theorem down_surjective : Surjective (@down α) := Equiv.ulift.surjective diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean index 05e5a64c67a953..32bc8a0b172856 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean @@ -858,9 +858,9 @@ variable [DecidableEq α] {l : List α} theorem Nodup.isCycleOn_formPerm (h : l.Nodup) : l.formPerm.IsCycleOn { a | a ∈ l } := by refine ⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => ?_⟩ - rw [Set.mem_setOf, ← List.indexOf_lt_length_iff] at ha hb - rw [← List.getElem_indexOf ha, ← List.getElem_indexOf hb] - refine ⟨l.indexOf b - l.indexOf a, ?_⟩ + rw [Set.mem_setOf, ← List.idxOf_lt_length_iff] at ha hb + rw [← List.getElem_idxOf ha, ← List.getElem_idxOf hb] + refine ⟨l.idxOf b - l.idxOf a, ?_⟩ simp only [sub_eq_neg_add, zpow_add, zpow_neg, Equiv.Perm.inv_eq_iff_eq, zpow_natCast, Equiv.Perm.coe_mul, List.formPerm_pow_apply_getElem _ h, Function.comp] rw [add_comm] diff --git a/Mathlib/Lean/Meta/KAbstractPositions.lean b/Mathlib/Lean/Meta/KAbstractPositions.lean index ffb5899f965683..d8b18350513d2e 100644 --- a/Mathlib/Lean/Meta/KAbstractPositions.lean +++ b/Mathlib/Lean/Meta/KAbstractPositions.lean @@ -71,7 +71,7 @@ def viewKAbstractSubExpr (e : Expr) (pos : SubExpr.Pos) : MetaM (Option (Expr × if subExpr.hasLooseBVars then return none let positions ← kabstractPositions subExpr e - let some n := positions.indexOf? pos | unreachable! + let some n := positions.idxOf? pos | unreachable! return some (subExpr, if positions.size == 1 then none else some (n + 1)) /-- Determine whether the result of abstracting `subExpr` from `e` at position `pos` results diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 91124505b00ab9..a593265e814c46 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -1154,14 +1154,14 @@ protected def mkPiAlgebraFin : MultilinearMap R (fun _ : Fin n => A) A where toFun m := (List.ofFn m).prod map_update_add' {dec} m i x y := by rw [Subsingleton.elim dec (by infer_instance)] - have : (List.finRange n).indexOf i < n := by - simpa using List.indexOf_lt_length_iff.2 (List.mem_finRange i) + have : (List.finRange n).idxOf i < n := by + simpa using List.idxOf_lt_length_iff.2 (List.mem_finRange i) simp [List.ofFn_eq_map, (List.nodup_finRange n).map_update, List.prod_set, add_mul, this, mul_add, add_mul] map_update_smul' {dec} m i c x := by rw [Subsingleton.elim dec (by infer_instance)] - have : (List.finRange n).indexOf i < n := by - simpa using List.indexOf_lt_length_iff.2 (List.mem_finRange i) + have : (List.finRange n).idxOf i < n := by + simpa using List.idxOf_lt_length_iff.2 (List.mem_finRange i) simp [List.ofFn_eq_map, (List.nodup_finRange n).map_update, List.prod_set, this] variable {R A n} diff --git a/Mathlib/Logic/Equiv/List.lean b/Mathlib/Logic/Equiv/List.lean index 7c84c312dfc461..37b796a38066bc 100644 --- a/Mathlib/Logic/Equiv/List.lean +++ b/Mathlib/Logic/Equiv/List.lean @@ -112,7 +112,7 @@ end Finset /-- A listable type with decidable equality is encodable. -/ def encodableOfList [DecidableEq α] (l : List α) (H : ∀ x, x ∈ l) : Encodable α := - ⟨fun a => indexOf a l, l.get?, fun _ => indexOf_get? (H _)⟩ + ⟨fun a => idxOf a l, l.get?, fun _ => idxOf_get? (H _)⟩ /-- A finite type is encodable. Because the encoding is not unique, we wrap it in `Trunc` to preserve computability. -/ diff --git a/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean b/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean index d609a2dcc3395b..50d947b4ff8164 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean @@ -575,7 +575,8 @@ private def fastJacobiSym (a : ℤ) (b : ℕ) : ℤ := refine Nat.le_of_dvd (Int.gcd_pos_iff.mpr (mod_cast .inr hb0)) ?_ refine Nat.dvd_gcd (Int.ofNat_dvd_left.mp (Int.dvd_of_emod_eq_zero ha2)) ?_ exact Int.ofNat_dvd_left.mp (Int.dvd_of_emod_eq_zero (mod_cast hb2)) - · rw [← IH (b / 2) (b.div_lt_self (Nat.pos_of_ne_zero hb0) one_lt_two)] + · dsimp only + rw [← IH (b / 2) (b.div_lt_self (Nat.pos_of_ne_zero hb0) one_lt_two)] obtain ⟨b, rfl⟩ := Nat.dvd_of_mod_eq_zero hb2 rw [mul_right' a (by decide) fun h ↦ hb0 (mul_eq_zero_of_right 2 h), b.mul_div_cancel_left (by decide), mod_left a 2, Nat.cast_ofNat, diff --git a/Mathlib/NumberTheory/Ostrowski.lean b/Mathlib/NumberTheory/Ostrowski.lean index 292717210cee34..024a8093ad42f0 100644 --- a/Mathlib/NumberTheory/Ostrowski.lean +++ b/Mathlib/NumberTheory/Ostrowski.lean @@ -55,17 +55,17 @@ private lemma tendsto_nat_rpow_inv : -- Multiplication by a constant moves in a List.sum private lemma list_mul_sum {R : Type*} [CommSemiring R] {T : Type*} (l : List T) (y : R) (x : R) : (l.mapIdx fun i _ => x * y ^ i).sum = x * (l.mapIdx fun i _ => y ^ i).sum := by - simp_rw [← smul_eq_mul, List.smul_sum, List.mapIdx_eq_enum_map] + simp_rw [← smul_eq_mul, List.smul_sum, List.mapIdx_eq_zipIdx_map] congr 1 simp -- Geometric sum for lists private lemma list_geom {T : Type*} {F : Type*} [Field F] (l : List T) {y : F} (hy : y ≠ 1) : (l.mapIdx fun i _ => y ^ i).sum = (y ^ l.length - 1) / (y - 1) := by - rw [← geom_sum_eq hy l.length, List.mapIdx_eq_enum_map, Finset.sum_range, ← Fin.sum_univ_get'] - simp only [List.getElem_enum, Function.uncurry_apply_pair] - let e : Fin l.enum.length ≃ Fin l.length := finCongr List.enum_length - exact Fintype.sum_bijective e e.bijective _ _ fun _ ↦ rfl + rw [← geom_sum_eq hy l.length, List.mapIdx_eq_zipIdx_map, Finset.sum_range, ← Fin.sum_univ_get'] + simp only [List.getElem_zipIdx, Function.uncurry_apply_pair] + let e : Fin l.zipIdx.length ≃ Fin l.length := finCongr List.length_zipIdx + exact Fintype.sum_bijective e e.bijective _ _ fun _ ↦ by simp [e] open AbsoluteValue -- does not work as intended after `namespace Rat.AbsoluteValue` @@ -294,10 +294,10 @@ lemma apply_le_sum_digits (n : ℕ) {m : ℕ} (hm : 1 < m) : _ = f L'.sum := by rw [Nat.ofDigits_eq_sum_mapIdx]; norm_cast _ ≤ (L'.map f).sum := listSum_le f L' _ ≤ (L.mapIdx fun i _ ↦ m * (f m) ^ i).sum := ?_ - simp only [hL', List.mapIdx_eq_enum_map, List.map_map] - refine List.sum_le_sum fun ⟨i, a⟩ hia ↦ ?_ + simp only [hL', List.mapIdx_eq_zipIdx_map, List.map_map] + refine List.sum_le_sum fun ⟨a, i⟩ hia ↦ ?_ dsimp only [Function.comp_apply, Function.uncurry_apply_pair] - replace hia := List.mem_enumFrom hia + replace hia := List.mem_zipIdx hia push_cast rw [map_mul, map_pow] refine mul_le_mul_of_nonneg_right ?_ <| pow_nonneg (f.nonneg _) i @@ -316,15 +316,14 @@ lemma one_lt_of_not_bounded (notbdd : ¬ ∀ n : ℕ, f n ≤ 1) {n₀ : ℕ} (h calc f m ≤ (L.mapIdx fun i _ ↦ n₀ * f n₀ ^ i).sum := apply_le_sum_digits m hn₀ _ ≤ (L.mapIdx fun _ _ ↦ (n₀ : ℝ)).sum := by - simp only [List.mapIdx_eq_enum_map, List.map_map] + simp only [List.mapIdx_eq_zipIdx_map, List.map_map] refine List.sum_le_sum fun ⟨i, a⟩ _ ↦ ?_ simp only [Function.comp_apply, Function.uncurry_apply_pair] exact mul_le_of_le_of_le_one' (mod_cast le_refl n₀) (pow_le_one₀ (by positivity) h) (by positivity) (by positivity) _ = n₀ * (Nat.log n₀ m + 1) := by - rw [List.mapIdx_eq_enum_map, List.eq_replicate_of_mem (a := (n₀ : ℝ)) - (l := List.map (Function.uncurry fun _ _ ↦ n₀) (List.enum L)), - List.sum_replicate, List.length_map, List.enum_length, nsmul_eq_mul, mul_comm, + rw [List.mapIdx_eq_zipIdx_map, List.eq_replicate_of_mem (a := (n₀ : ℝ)) (l := L.zipIdx.map _), + List.sum_replicate, List.length_map, List.length_zipIdx, nsmul_eq_mul, mul_comm, Nat.digits_len n₀ m hn₀ (not_eq_zero_of_lt hm), Nat.cast_add_one] simp +contextual _ ≤ n₀ * (logb n₀ m + 1) := by gcongr; exact natLog_le_logb .. diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean index 0adce71cb1c935..0e42cdb9f044f9 100644 --- a/Mathlib/Order/Monotone/Basic.lean +++ b/Mathlib/Order/Monotone/Basic.lean @@ -133,18 +133,6 @@ instance [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a < b → f b < f a)] : end Decidable -lemma monotone_inclusion_le_le_of_le [Preorder α] {k j : α} (hkj : k ≤ j) : - Monotone (fun ⟨i, hi⟩ => ⟨i, hi.trans hkj⟩ : { i // i ≤ k } → { i // i ≤ j}) := - fun _ _ h => h - -lemma monotone_inclusion_lt_le_of_le [Preorder α] {k j : α} (hkj : k ≤ j) : - Monotone (fun ⟨i, hi⟩ => ⟨i, hi.le.trans hkj⟩ : { i // i < k } → { i // i ≤ j}) := - fun _ _ h => h - -lemma monotone_inclusion_lt_lt_of_le [Preorder α] {k j : α} (hkj : k ≤ j) : - Monotone (fun ⟨i, hi⟩ => ⟨i, lt_of_lt_of_le hi hkj⟩ : { i // i < k } → { i // i < j}) := - fun _ _ h => h - /-! ### Monotonicity on the dual order Strictly, many of the `*On.dual` lemmas in this section should use `ofDual ⁻¹' s` instead of `s`, diff --git a/Mathlib/Order/RelSeries.lean b/Mathlib/Order/RelSeries.lean index 81867c483651ca..d8d45c2b14c06c 100644 --- a/Mathlib/Order/RelSeries.lean +++ b/Mathlib/Order/RelSeries.lean @@ -177,7 +177,7 @@ instance membership : Membership α (RelSeries r) := theorem mem_def : x ∈ s ↔ x ∈ Set.range s := Iff.rfl @[simp] theorem mem_toList : x ∈ s.toList ↔ x ∈ s := by - rw [RelSeries.toList, List.mem_ofFn, RelSeries.mem_def] + rw [RelSeries.toList, List.mem_ofFn', RelSeries.mem_def] theorem subsingleton_of_length_eq_zero (hs : s.length = 0) : {x | x ∈ s}.Subsingleton := by rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩ diff --git a/Mathlib/Tactic/DeriveTraversable.lean b/Mathlib/Tactic/DeriveTraversable.lean index 54a52f0b432bf8..1844b160ba5ef1 100644 --- a/Mathlib/Tactic/DeriveTraversable.lean +++ b/Mathlib/Tactic/DeriveTraversable.lean @@ -217,7 +217,7 @@ def mkOneInstance (n cls : Name) (tac : MVarId → TermElabM Unit) let params := params.pop let tgt := mkAppN tgt params let tgt ← mkInst cls tgt - params.zipWithIndex.foldrM (fun (param, i) tgt => do + params.zipIdx.foldrM (fun (param, i) tgt => do -- add typeclass hypothesis for each inductive parameter let tgt ← (do guard (i < decl.numParams) diff --git a/Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean b/Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean index 160faf10c28542..188e872f4dc197 100644 --- a/Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean +++ b/Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean @@ -327,7 +327,7 @@ def elimAllVarsM : LinarithM Unit := do those hypotheses. It produces an initial state for the elimination monad. -/ def mkLinarithData (hyps : List Comp) (maxVar : ℕ) : LinarithData := - ⟨maxVar, .ofList (hyps.enum.map fun ⟨n, cmp⟩ => PComp.assump cmp n) _⟩ + ⟨maxVar, .ofList (hyps.mapIdx fun n cmp => PComp.assump cmp n) _⟩ /-- An oracle that uses Fourier-Motzkin elimination. -/ def CertificateOracle.fourierMotzkin : CertificateOracle where diff --git a/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean b/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean index a96634597705a0..87d71a0c573f5a 100644 --- a/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean +++ b/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean @@ -32,7 +32,8 @@ Extract the certificate from the `vec` found by `Linarith.SimplexAlgorithm.findP def postprocess (vec : Array ℚ) : Std.HashMap ℕ ℕ := let common_den : ℕ := vec.foldl (fun acc item => acc.lcm item.den) 1 let vecNat : Array ℕ := vec.map (fun x : ℚ => (x * common_den).floor.toNat) - Std.HashMap.empty.insertMany <| vecNat.toList.enum.filter (fun ⟨_, item⟩ => item != 0) + Std.HashMap.empty.insertMany <| vecNat.zipIdx.filterMap + fun ⟨item, idx⟩ => if item != 0 then some (idx, item) else none end SimplexAlgorithm diff --git a/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Datatypes.lean b/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Datatypes.lean index 2f6eb09ce7de1a..177ec7e8b2a329 100644 --- a/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Datatypes.lean +++ b/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Datatypes.lean @@ -57,8 +57,8 @@ instance : UsableInSimplexAlgorithm DenseMatrix where getElem mat i j := mat.data[i]![j]! setElem mat i j v := ⟨mat.data.modify i fun row => row.set! j v⟩ getValues mat := - mat.data.zipWithIndex.foldl (init := []) fun acc (row, i) => - let rowVals := Array.toList <| row.zipWithIndex.filterMap fun (v, j) => + mat.data.zipIdx.foldl (init := []) fun acc (row, i) => + let rowVals := Array.toList <| row.zipIdx.filterMap fun (v, j) => if v != 0 then .some (i, j, v) else @@ -72,7 +72,7 @@ instance : UsableInSimplexAlgorithm DenseMatrix where swapRows mat i j := ⟨mat.data.swapIfInBounds i j⟩ subtractRow mat i j coef := let newData : Array (Array Rat) := mat.data.modify j fun row => - row.zipWith mat.data[i]! fun x y => x - coef * y + Array.zipWith (fun x y => x - coef * y) row mat.data[i]! ⟨newData⟩ divideRow mat i coef := ⟨mat.data.modify i (·.map (· / coef))⟩ @@ -92,7 +92,7 @@ instance : UsableInSimplexAlgorithm SparseMatrix where else ⟨mat.data.modify i fun row => row.insert j v⟩ getValues mat := - mat.data.zipWithIndex.foldl (init := []) fun acc (row, i) => + mat.data.zipIdx.foldl (init := []) fun acc (row, i) => let rowVals := row.toList.map fun (j, v) => (i, j, v) rowVals ++ acc ofValues {n _ : Nat} vals := Id.run do diff --git a/Mathlib/Tactic/Linarith/Verification.lean b/Mathlib/Tactic/Linarith/Verification.lean index 2a5e07a579937c..9fe7e89217e921 100644 --- a/Mathlib/Tactic/Linarith/Verification.lean +++ b/Mathlib/Tactic/Linarith/Verification.lean @@ -214,10 +214,10 @@ def proveFalseByLinarith (transparency : TransparencyMode) (oracle : Certificate return certificate let (sm, zip) ← withTraceNode `linarith (return m!"{exceptEmoji ·} Building final expression") do - let enum_inputs := inputs.enum + let enum_inputs := inputs.zipIdx -- construct a list pairing nonzero coeffs with the proof of their corresponding -- comparison - let zip := enum_inputs.filterMap fun ⟨n, e⟩ => (certificate[n]?).map (e, ·) + let zip := enum_inputs.filterMap fun ⟨e, n⟩ => (certificate[n]?).map (e, ·) let mls ← zip.mapM fun ⟨e, n⟩ => do mulExpr n (← leftOfIneqProof e) -- `sm` is the sum of input terms, scaled to cancel out all variables. let sm ← addExprs mls diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean index 5786f3360de338..babc21254285c8 100644 --- a/Mathlib/Tactic/Linter/TextBased.lean +++ b/Mathlib/Tactic/Linter/TextBased.lean @@ -201,9 +201,9 @@ section /-- Lint on any occurrences of the string "Adaptation note:" or variants thereof. -/ def adaptationNoteLinter : TextbasedLinter := fun lines ↦ Id.run do let mut errors := Array.mkEmpty 0 - for (line, idx) in lines.zipWithIndex do + for h : idx in [:lines.size] do -- We make this shorter to catch "Adaptation note", "adaptation note" and a missing colon. - if line.containsSubstr "daptation note" then + if lines[idx].containsSubstr "daptation note" then errors := errors.push (StyleError.adaptationNote, idx + 1) return (errors, none) @@ -212,7 +212,8 @@ def adaptationNoteLinter : TextbasedLinter := fun lines ↦ Id.run do def trailingWhitespaceLinter : TextbasedLinter := fun lines ↦ Id.run do let mut errors := Array.mkEmpty 0 let mut fixedLines := lines - for (line, idx) in lines.zipWithIndex do + for h : idx in [:lines.size] do + let line := lines[idx] if line.back == ' ' then errors := errors.push (StyleError.trailingWhitespace, idx + 1) fixedLines := fixedLines.set! idx line.trimRight diff --git a/Mathlib/Tactic/Linter/UnusedTactic.lean b/Mathlib/Tactic/Linter/UnusedTactic.lean index 807699e1024c36..379ef18d2ff6a1 100644 --- a/Mathlib/Tactic/Linter/UnusedTactic.lean +++ b/Mathlib/Tactic/Linter/UnusedTactic.lean @@ -5,6 +5,7 @@ Authors: Damiano Testa -/ import Lean.Elab.Command +import Lean.Parser.Syntax import Batteries.Tactic.Unreachable -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. diff --git a/Mathlib/Tactic/MinImports.lean b/Mathlib/Tactic/MinImports.lean index b841e9bad99426..57ad4068615bf9 100644 --- a/Mathlib/Tactic/MinImports.lean +++ b/Mathlib/Tactic/MinImports.lean @@ -3,10 +3,10 @@ Copyright (c) 2024 Damiano Testa. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Damiano Testa -/ -import Mathlib.Init -import ImportGraph.Imports import Lean.Elab.DefView import Lean.Util.CollectAxioms +import Mathlib.Init +import ImportGraph.Imports /-! # `#min_imports in` a command to find minimal imports diff --git a/Mathlib/Tactic/MkIffOfInductiveProp.lean b/Mathlib/Tactic/MkIffOfInductiveProp.lean index 2c97c99dd86ae0..bc24422910a3c1 100644 --- a/Mathlib/Tactic/MkIffOfInductiveProp.lean +++ b/Mathlib/Tactic/MkIffOfInductiveProp.lean @@ -191,7 +191,7 @@ def toCases (mvar : MVarId) (shape : List Shape) : MetaM Unit := do let ⟨h, mvar'⟩ ← mvar.intro1 let subgoals ← mvar'.cases h - let _ ← (shape.zip subgoals.toList).enum.mapM fun ⟨p, ⟨⟨shape, t⟩, subgoal⟩⟩ ↦ do + let _ ← (shape.zip subgoals.toList).zipIdx.mapM fun ⟨⟨⟨shape, t⟩, subgoal⟩, p⟩ ↦ do let vars := subgoal.fields let si := (shape.zip vars.toList).filterMap (fun ⟨c,v⟩ ↦ if c then some v else none) let mvar'' ← select p (subgoals.size - 1) subgoal.mvarId diff --git a/Mathlib/Tactic/MoveAdd.lean b/Mathlib/Tactic/MoveAdd.lean index 5c0f00d0efe32d..8ed7a04de0339c 100644 --- a/Mathlib/Tactic/MoveAdd.lean +++ b/Mathlib/Tactic/MoveAdd.lean @@ -169,7 +169,7 @@ similarly for the pairs with second coordinate equal to `false`. def weight (L : List (α × Bool)) (a : α) : ℤ := let l := L.length match L.find? (Prod.fst · == a) with - | some (_, b) => if b then - l + (L.indexOf (a, b) : ℤ) else (L.indexOf (a, b) + 1 : ℤ) + | some (_, b) => if b then - l + (L.idxOf (a, b) : ℤ) else (L.idxOf (a, b) + 1 : ℤ) | none => 0 /-- `reorderUsing toReorder instructions` produces a reordering of `toReorder : List α`, @@ -196,7 +196,7 @@ def reorderUsing (toReorder : List α) (instructions : List (α × Bool)) : List let reorder := uToReorder.qsort fun x y => match uInstructions.find? (Prod.fst · == x), uInstructions.find? (Prod.fst · == y) with | none, none => - ((uToReorder.indexOf? x).map Fin.val).get! ≤ ((uToReorder.indexOf? y).map Fin.val).get! + (uToReorder.idxOf? x).get! ≤ (uToReorder.idxOf? y).get! | _, _ => weight uInstructions x ≤ weight uInstructions y (reorder.map Prod.fst).toList diff --git a/Mathlib/Tactic/Widget/StringDiagram.lean b/Mathlib/Tactic/Widget/StringDiagram.lean index 0a6871ad89cdcf..f72bf44ff6397c 100644 --- a/Mathlib/Tactic/Widget/StringDiagram.lean +++ b/Mathlib/Tactic/Widget/StringDiagram.lean @@ -186,12 +186,12 @@ variable {ρ : Type} [MonadMor₁ (CoherenceM ρ)] /-- The list of nodes at the top of a string diagram. -/ def topNodes (η : WhiskerLeft) : CoherenceM ρ (List Node) := do - return (← η.srcM).toList.enum.map (fun (i, f) => .id ⟨0, i, i, f⟩) + return (← η.srcM).toList.mapIdx fun i f => .id ⟨0, i, i, f⟩ /-- The list of nodes at the top of a string diagram. The position is counted from the specified natural number. -/ def NormalExpr.nodesAux (v : ℕ) : NormalExpr → CoherenceM ρ (List (List Node)) - | NormalExpr.nil _ α => return [(← α.srcM).toList.enum.map (fun (i, f) => .id ⟨v, i, i, f⟩)] + | NormalExpr.nil _ α => return [(← α.srcM).toList.mapIdx fun i f => .id ⟨v, i, i, f⟩] | NormalExpr.cons _ _ η ηs => do let s₁ := η.nodes v 0 0 let s₂ ← ηs.nodesAux (v + 1) @@ -216,7 +216,7 @@ def NormalExpr.strands (e : NormalExpr) : CoherenceM ρ (List (List Strand)) := -- sanity check if xs.length ≠ ys.length then throwError "The number of the start and end points of a string does not match." - (xs.zip ys).enum.mapM fun (k, (n₁, f₁), (n₂, _)) => do + (xs.zip ys).mapIdxM fun k ((n₁, f₁), (n₂, _)) => do return ⟨n₁.hPosTar + k, n₁, n₂, f₁⟩ end BicategoryLike diff --git a/MathlibTest/fun_prop_dev.lean b/MathlibTest/fun_prop_dev.lean index 866e3b6aebefa0..8128212a89b5fe 100644 --- a/MathlibTest/fun_prop_dev.lean +++ b/MathlibTest/fun_prop_dev.lean @@ -393,7 +393,7 @@ example (f : β → γ) (g : α → β) (h : B) : Con (fun x => f (g x)) := by f end MultipleLambdaTheorems -/-- warning: `?m` is not a `fun_prop` goal! -/ +/-- info: `?m` is not a `fun_prop` goal! -/ #guard_msgs in #check_failure ((by fun_prop) : ?m) diff --git a/lake-manifest.json b/lake-manifest.json index f263b2cfc76dc0..79acbce8d52da4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e104724db91693a3a088c5fdd76cff4fac331739", + "rev": "59a8514bb0ee5bae2689d8be717b5272c9b3dc1c", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1a6613663c3eb08c401ce0fd1a408412f2c2321e", + "rev": "5013810061a18ca1f5510106172b94c6fbd0a2fc", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dafff53912eac07a1a983080df61df10f622fe25", + "rev": "8fff3f074da9237cd4e179fd6dd89be6c4022d41", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "44dab9f36aa73d5f789629b55528c5a1501877a6", + "rev": "ba9a63be53f16b3b6e4043641c6bad4883e650b4", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f53b5c1f9151dce5971165b4302b5b38a35be58d", + "rev": "a3abab9293f13409f8a0236838a001056d270476", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "fin-find", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "rev": "a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 8b4f470c73e011..3ca992cf968f8f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.16.0 \ No newline at end of file +leanprover/lean4:v4.17.0-rc1 diff --git a/scripts/noshake.json b/scripts/noshake.json index c41910752e88bc..c8aeb867d26d7f 100644 --- a/scripts/noshake.json +++ b/scripts/noshake.json @@ -247,7 +247,8 @@ ["Mathlib.Algebra.Group.Basic", "Mathlib.Init.Order.LinearOrder"], "Mathlib.Tactic.Measurability": ["Mathlib.Algebra.Group.Defs", "Mathlib.Tactic.Measurability.Init"], - "Mathlib.Tactic.Linter.UnusedTactic": ["Batteries.Tactic.Unreachable"], + "Mathlib.Tactic.Linter.UnusedTactic": + ["Batteries.Tactic.Unreachable", "Lean.Parser.Syntax"], "Mathlib.Tactic.LinearCombination": ["Mathlib.Tactic.LinearCombination.Lemmas"], "Mathlib.Tactic.Lemma": ["Lean.Parser.Command"],