mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.Maps
Ideal.le_comap_of_map_le : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] {f : F}
  {I : Ideal R} {K : Ideal S} [inst_3 : RingHomClass F R S], Ideal.map f I ≤ K → I ≤ Ideal.comap f K
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
/-- The isomorphism between the sheafification of `P` composed with `F` and
the sheafification of `P ⋙ F`, functorially in `P`.  -/
CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          {E : Type u_2} →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} E] →
              (F : CategoryTheory.Functor D E) →
                [inst_3 :
                    ∀ (J : CategoryTheory.Limits.MulticospanShape),
                      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] →
                  [inst_4 :
                      ∀ (J : CategoryTheory.Limits.MulticospanShape),
                        CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] →
                    [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
                      [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] →
                        [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] →
                          [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
                                CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] →
                            (J.sheafification D).comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ D E).obj F) ≅
                              ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ D E).obj F).comp (J.sheafification E)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_injective : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M],
  Function.Injective DFunLike.coe
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {v : β k}, (t.getThenInsertIfNew? k v).1 = t.get? k
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.freeObj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (F : CategoryTheory.Functor Cᵒᵖ (Type u)) (X : Cᵒᵖ),
  (PresheafOfModules.freeObj F).obj X = (ModuleCat.free ↑(R.obj X)).obj (F.obj X)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.tag_index_eq_self_of_mem_smul_span : ∀ {ι : Type u_1} (n : ℕ) [NeZero n] [inst : Finite ι] {x : ι → ℝ},
  x ∈ (↑n)⁻¹ • Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)) →
    BoxIntegral.unitPartition.tag n (BoxIntegral.unitPartition.index n x) = x
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- **Noether's first isomorphism theorem** (a definition): the canonical isomorphism between
`G/(ker φ)` to `range φ`.  -/
QuotientGroup.quotientKerEquivRange : {G : Type u} → [inst : Group G] → {H : Type v} → [inst_1 : Group H] → (φ : G →* H) → G ⧸ φ.ker ≃* ↥φ.range
-- Mathlib.Tactic.Linter.ValidatePRTitle
/-- Check if `title` matches the mathlib conventions for PR titles
(documented at <https://leanprover-community.github.io/contribute/commit.html>).

Not all checks are implemented: for instance, no effort is made to verify if the title or body
are written in present imperative tense.
Return all error messages for violations found.
 -/
validateTitle : String → Array String
-- Mathlib.Analysis.Convex.Function
/-- A concave function on a segment is lower-bounded by the min of its endpoints.  -/
ConcaveOn.ge_on_segment' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f →
    ∀ {x y : E}, x ∈ s → y ∈ s → ∀ {a b : 𝕜}, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.uniformIntegrable_congr_ae : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {f g : ι → α → β},
  (∀ (n : ι), f n =ᵐ[μ] g n) → (MeasureTheory.UniformIntegrable f p μ ↔ MeasureTheory.UniformIntegrable g p μ)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_Ioi : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a : α} [ClosedIicTopology α], MeasurableSet (Set.Ioi a)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.length_reverse : ∀ {α : Type u_1} {a : FreeAddMonoid α}, a.reverse.length = a.length
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.supportAddSubgroup_ne_top : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R), P.supportAddSubgroup ≠ ⊤
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instHashablePurity.hash : Lean.Compiler.LCNF.Purity → UInt64
-- Mathlib.AlgebraicTopology.SingularSet
SSet.stdSimplexToTop_app_app_hom_apply_down_hom_apply : ∀ (X : SimplexCategory) (X_1 : SimplexCategoryᵒᵖ) (a : (SSet.stdSimplex.obj X).obj X_1)
  (a_1 : ↑(Opposite.unop (SimplexCategory.toTop.{u}.op.obj X_1))),
  (TopCat.Hom.hom ((CategoryTheory.ConcreteCategory.hom ((SSet.stdSimplexToTop.app X).app X_1)) a).down) a_1 =
    (SSet.toTopSimplex.hom.app X).hom' ((((sSetTopAdj.unit.app (SSet.stdSimplex.obj X)).app X_1).hom' a).down.hom' a_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.X_ne_zero_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P : Fin 3 → R},
  W'.Nonsingular P → P 2 = 0 → P 0 ≠ 0
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_mono`.

---

The extended diameter is monotonous with respect to inclusion  -/
EMetric.diam_mono : ∀ {X : Type u_2} {s t : Set X} [inst : PseudoEMetricSpace X], s ⊆ t → Metric.ediam s ≤ Metric.ediam t
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- Given a functor `F : J ⥤ TopCat` and a cocone `c : Cocone (F ⋙ forget)`
of the underlying cocone of types, this is the type `c.pt`
with the supremum of the topologies that are coinduced by the maps `c.ι.app j`.  -/
TopCat.coconePtOfCoconeForget : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    {F : CategoryTheory.Functor J TopCat} →
      CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget TopCat)) → Type u
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.instIsContinuousCompId : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [F.IsContinuous J K],
  (F.comp (CategoryTheory.Functor.id D)).IsContinuous J K
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instInterOfBEqOfHashable : {α : Type u} → [BEq α] → [Hashable α] → Inter (Std.HashSet.Raw α)
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SupSet α] [inst_1 : SupSet β] [inst_2 : SupSet γ]
  {g : sSupHom β γ} {f₁ f₂ : sSupHom α β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inlHom_apply : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module Rᵐᵒᵖ M] (r : R), (TrivSqZeroExt.inlHom R M) r = TrivSqZeroExt.inl r
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjHomologySelfIso_inv_homologyι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).inv
      (((HomologicalComplex.single C c j).obj A).homologyι j) =
    (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom
-- Mathlib.Order.Filter.Defs
Filter.mk.injEq : ∀ {α : Type u_1} (sets : Set (Set α)) (univ_sets : Set.univ ∈ sets)
  (sets_of_superset : ∀ {x y : Set α}, x ∈ sets → x ⊆ y → y ∈ sets)
  (inter_sets : ∀ {x y : Set α}, x ∈ sets → y ∈ sets → x ∩ y ∈ sets) (sets_1 : Set (Set α))
  (univ_sets_1 : Set.univ ∈ sets_1) (sets_of_superset_1 : ∀ {x y : Set α}, x ∈ sets_1 → x ⊆ y → y ∈ sets_1)
  (inter_sets_1 : ∀ {x y : Set α}, x ∈ sets_1 → y ∈ sets_1 → x ∩ y ∈ sets_1),
  ({ sets := sets, univ_sets := univ_sets, sets_of_superset := sets_of_superset, inter_sets := inter_sets } =
      { sets := sets_1, univ_sets := univ_sets_1, sets_of_superset := sets_of_superset_1,
        inter_sets := inter_sets_1 }) =
    (sets = sets_1)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert.eq_def : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (x : G.Walk u v) (x_1 : ℕ),
  x.getVert x_1 =
    match v, x, x_1 with
    | .(u), SimpleGraph.Walk.nil, x => u
    | v, SimpleGraph.Walk.cons h p, 0 => u
    | v, SimpleGraph.Walk.cons h q, n.succ => q.getVert n
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.eq_of_le : ∀ {α : Type u_1} {ι : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α},
  s.PairwiseDisjoint f → ∀ {i j : ι}, i ∈ s → j ∈ s → f i ≠ ⊥ → f i ≤ f j → i = j
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_of_contains_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.ExtDHashMap.filterMap f m).contains k = true → m.contains k = true
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.IterM.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Algebra.Ring.Subsemiring.Order
/-- A subsemiring of an ordered semiring is an ordered semiring.  -/
Subsemiring.toIsOrderedRing : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] (s : Subsemiring R), IsOrderedRing ↥s
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.map_compDer : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_2)
  (B : Type u_3) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra A B]
  [inst_7 : Algebra S B] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : SMulCommClass S A B],
  (KaehlerDifferential.map R S A B).compDer (KaehlerDifferential.D R A) =
    Derivation.compAlgebraMap A (Derivation.restrictScalars R (KaehlerDifferential.D S B))
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- A cohomological spectral sequence lying on finitely many rows
has differentials given by the vector `(r, 1 - r)` on the `r`th page.  -/
CategoryTheory.CohomologicalSpectralSequenceFin : (C : Type u_1) → [inst : CategoryTheory.Category.{u_3, u_1} C] → [CategoryTheory.Abelian C] → ℕ → ℤ → Type (max u_1 u_3)
-- Init.Notation
/-- A case tag argument has the form `tag x₁ ... xₙ`; it refers to tag `tag` and renames
the last `n` hypotheses to `x₁ ... xₙ`.
 -/
Lean.Parser.Tactic.caseArg : Lean.ParserDescr
-- Mathlib.Order.Defs.Unbundled
symm_def : ∀ {α : Sort u_1} {r : α → α → Prop}, Std.Symm r ↔ ∀ ⦃a b : α⦄, r a b → r b a
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
/-- `MultilinearMap.dfinsuppFamily` as a linear map.  -/
MultilinearMap.dfinsuppFamilyₗ : {ι : Type uι} →
  {κ : ι → Type uκ} →
    {R : Type uR} →
      {M : (i : ι) → κ i → Type uM} →
        {N : ((i : ι) → κ i) → Type uN} →
          [DecidableEq ι] →
            [Fintype ι] →
              [inst : CommSemiring R] →
                [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] →
                  [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] →
                    [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)] →
                      [inst_4 : (p : (i : ι) → κ i) → Module R (N p)] →
                        ((p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)) →ₗ[R]
                          MultilinearMap R (fun i => Π₀ (j : κ i), M i j) (Π₀ (t : (i : ι) → κ i), N t)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The `h` in the Weierstrass preparation theorem.  -/
PowerSeries.weierstrassUnit : {A : Type u_1} →
  [inst : CommRing A] →
    [inst_1 : IsLocalRing A] →
      [IsAdicComplete (IsLocalRing.maximalIdeal A) A] →
        (g : PowerSeries A) → (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 → PowerSeries A
-- Std.Time.Internal.Bounded
/-- Casts the boundaries of the `Bounded` using equivalences.
 -/
Std.Time.Internal.Bounded.cast : {rel : ℤ → ℤ → Prop} →
  {lo₁ lo₂ hi₁ hi₂ : ℤ} →
    lo₁ = lo₂ → hi₁ = hi₂ → Std.Time.Internal.Bounded rel lo₁ hi₁ → Std.Time.Internal.Bounded rel lo₂ hi₂
-- Init.Data.Array.Bootstrap
Array.toList_pop : ∀ {α : Type u_1} {xs : Array α}, xs.pop.toList = xs.toList.dropLast
-- Lean.Environment
/-- Compute extension entries for all levels at once by calling `exportEntriesFn` once per extension.
Returns an `OLeanEntries` of arrays mapping extension names to their exported data.
 -/
_private.Lean.Environment.0.Lean.computeExtEntries : Lean.Environment → IO (Lean.OLeanEntries (Array (Lean.Name × Array Lean.EnvExtensionEntry)))
-- Mathlib.Data.Finset.Max
Finset.exists_next_right : ∀ {α : Type u_2} [inst : LinearOrder α] {x : α} {s : Finset α},
  (∃ y ∈ s, x < y) → ∃ y ∈ s, x < y ∧ ∀ z ∈ s, x < z → y ≤ z
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.comp_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {l : Filter α} {α₂ : Type u_4} {f g : α₂ → β}
  {l' : Filter α₂},
  Asymptotics.IsEquivalent l' f g → ∀ {k : α → α₂}, Filter.Tendsto k l l' → Asymptotics.IsEquivalent l (f ∘ k) (g ∘ k)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The cardinality of a block divides the cardinality of the ambient type  -/
MulAction.IsBlock.ncard_dvd_card : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] [MulAction.IsPretransitive G X] {B : Set X},
  MulAction.IsBlock G B → B.Nonempty → B.ncard ∣ Nat.card X
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.forall : ∀ {G : Type u_3} [inst : DivInvMonoid G] (p : ConjAct G → Prop),
  (∀ (x : ConjAct G), p x) ↔ ∀ (x : G), p (ConjAct.toConjAct x)
-- Mathlib.Data.Finset.Prod
Finset.mem_diag : ∀ {α : Type u_1} {s : Finset α} {x : α × α}, x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.mk : {α : Type u_4} →
  [inst : TopologicalSpace α] →
    (carrier : Set α) → IsIrreducible carrier → IsClosed carrier → TopologicalSpace.IrreducibleCloseds α
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Twice a base angle of an isosceles triangle with apex at the center of a circle, plus twice
the angle at the apex of a triangle with the same base but apex on the circle, equals `π`.  -/
EuclideanGeometry.Sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
  p₁ ∈ s →
    p₂ ∈ s →
      p₃ ∈ s →
        p₂ ≠ p₁ →
          p₂ ≠ p₃ →
            p₁ ≠ p₃ → 2 • EuclideanGeometry.oangle p₃ p₁ s.center + 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv.eq_1 : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G],
  Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv k G =
    (HomotopyEquiv.ofIso (Rep.standardComplex.compForgetAugmentedIso k G).symm).trans
      ((classifyingSpaceUniversalCover.extraDegeneracyCompForgetAugmentedToModule k G).homotopyEquiv.trans
        (HomotopyEquiv.ofIso
          ((ChainComplex.single₀ (ModuleCat k)).mapIso
            ((MonoidAlgebra.coeffLinearEquiv k).trans (Finsupp.uniqueLinearEquiv k k default)).toModuleIso)))
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {D₁ : Type u₁'} [inst_2 : CategoryTheory.Category.{v₁', u₁'} D₁]
  {D₂ : Type u₂'} [inst_3 : CategoryTheory.Category.{v₂', u₂'} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [inst_4 : L₁.IsLocalization W₁]
  [inst_5 : L₂.IsLocalization W₂] {M : Type w'} [inst_6 : AddMonoid M] [inst_7 : CategoryTheory.HasShift C₁ M]
  [inst_8 : CategoryTheory.HasShift C₂ M] [inst_9 : CategoryTheory.HasShift D₁ M]
  [inst_10 : CategoryTheory.HasShift D₂ M] [inst_11 : L₁.CommShift M] [inst_12 : L₂.CommShift M]
  [inst_13 : Φ.functor.CommShift M] {X₁ Y₁ : C₁} {X₂ Y₂ : C₂}
  [inst_14 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁]
  [inst_15 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂]
  [inst_16 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂]
  [inst_17 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] (eX : Φ.functor.obj X₁ ≅ X₂)
  (eY : Φ.functor.obj Y₁ ≅ Y₂) (G : CategoryTheory.Functor D₁ D₂) [inst_18 : G.CommShift M]
  (e : Φ.functor.comp L₂ ≅ L₁.comp G) [CategoryTheory.NatTrans.CommShift e.hom M] {m : M}
  (f : CategoryTheory.Localization.SmallShiftedHom W₁ X₁ Y₁ m),
  (CategoryTheory.Localization.SmallShiftedHom.equiv W₂ L₂) (Φ.smallShiftedHomMap eX eY f) =
    (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ (CategoryTheory.CategoryStruct.comp (L₂.map eX.inv) (e.hom.app X₁))).comp
      ((((CategoryTheory.Localization.SmallShiftedHom.equiv W₁ L₁) f).map G).comp
        (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ (CategoryTheory.CategoryStruct.comp (e.inv.app Y₁) (L₂.map eY.hom))) ⋯)
      ⋯
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.toGrothendieck.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (K : CategoryTheory.Coverage C),
  K.toGrothendieck = K.toGrothendieck.copy (fun X => Set.ofPred (K.Saturate X)) ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tsum_eq_zero_add' : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [T2Space M] [ContinuousAdd M] {f : ℕ → M},
  (Summable fun n => f (n + 1)) → ∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry preserves edistances.  -/
Isometry.edist_eq : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → ∀ (x y : α), edist (f x) (f y) = edist x y
-- Mathlib.Order.Interval.Multiset
/-- The multiset of elements `x` such that `x ≤ b`. Basically `Set.Iic b` as a multiset.  -/
Multiset.Iic : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderBot α] → α → Multiset α
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiff_subtype_val : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {U : TopologicalSpace.Opens M},
  ContMDiff I I n Subtype.val
-- Init.Data.SInt.Lemmas
Int16.toInt_neg : ∀ (n : Int16), (-n).toInt = (-n.toInt).bmod (2 ^ 16)
-- Mathlib.Algebra.Algebra.Epi
LinearMap.restrictScalars₁₂.congr_simp : ∀ {R : Type u_1} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] {M : Type u_5} {N : Type u_7} {Pₗ : Type u_11}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid Pₗ] [inst_5 : Module R M]
  [inst_6 : Module S N] [inst_7 : Module R Pₗ] [inst_8 : Module S Pₗ] [inst_9 : SMulCommClass S R Pₗ] (R' : Type u_14)
  (S' : Type u_15) [inst_10 : Semiring R'] [inst_11 : Semiring S'] [inst_12 : Module R' M] [inst_13 : Module S' N]
  [inst_14 : Module R' Pₗ] [inst_15 : Module S' Pₗ] [inst_16 : SMulCommClass S' R' Pₗ] [inst_17 : SMul S' S]
  [inst_18 : IsScalarTower S' S N] [inst_19 : IsScalarTower S' S Pₗ] [inst_20 : SMul R' R]
  [inst_21 : IsScalarTower R' R M] [inst_22 : IsScalarTower R' R Pₗ] (B B_1 : M →ₗ[R] N →ₗ[S] Pₗ),
  B = B_1 → LinearMap.restrictScalars₁₂ R' S' B = LinearMap.restrictScalars₁₂ R' S' B_1
-- Mathlib.Data.Prod.TProd
List.TProd.instInhabited : {ι : Type u} → {α : ι → Type v} → {l : List ι} → [(i : ι) → Inhabited (α i)] → Inhabited (List.TProd α l)
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorInt32 : LawfulXor Int32
-- Mathlib.Data.Set.Pairwise.Basic
Set.Pairwise.insert : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
  s.Pairwise r → (∀ b ∈ s, a ≠ b → r a b ∧ r b a) → (insert a s).Pairwise r
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineMap.mk.congr_simp : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (toFun toFun_1 : P1 → P2) (e_toFun : toFun = toFun_1)
  (linear linear_1 : V1 →ₗ[k] V2) (e_linear : linear = linear_1)
  (map_vadd' : ∀ (p : P1) (v : V1), toFun (v +ᵥ p) = linear v +ᵥ toFun p),
  { toFun := toFun, linear := linear, map_vadd' := map_vadd' } =
    { toFun := toFun_1, linear := linear_1, map_vadd' := ⋯ }
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrLeftEquiv_refl : ∀ {M : Type u_4} {N : Type u_8} [inst : AddZeroClass M] [inst_1 : AddMonoid N],
  (AddEquiv.refl M).addMonoidHomCongrLeftEquiv = Equiv.refl (M →+ N)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.option.sizeOf_spec : ∀ (stx : Lean.Syntax), sizeOf (Lean.Elab.CompletionInfo.option stx) = 1 + sizeOf stx
-- Mathlib.RingTheory.Flat.EquationalCriterion
_private.Mathlib.RingTheory.Flat.EquationalCriterion.0.Module.Flat.exists_factorization_of_comp_eq_zero_of_free_aux : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  {K : Type u_3} {n : ℕ} [inst_4 : AddCommGroup K] [inst_5 : Module R K] [Module.Finite R K] {f : K →ₗ[R] Fin n →₀ R}
  {x : (Fin n →₀ R) →ₗ[R] M}, x ∘ₗ f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a ∘ₗ f = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_le_size_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, t.size ≤ (t.insert k v).size
-- Aesop.Options.Public
/-- (aesop) Warn when `aesop` does not close the goal, i.e. is used as a non-terminal tactic.
 -/
Aesop.aesop.warn.nonterminal : Lean.Option Bool