mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.mapGenerators.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      F]
  (η η_1 : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)), η = η_1 → P.mapGenerators F η = P.mapGenerators F η_1
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `η ⊗ θ` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.evalHorizontalCompAux' : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
          Mathlib.Tactic.BicategoryLike.WhiskerLeft →
            Mathlib.Tactic.BicategoryLike.WhiskerLeft →
              Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result
-- Mathlib.RingTheory.IsAdjoinRoot
AdjoinRoot.isAdjoinRootMonic_toAdjoinRoot : ∀ {R : Type u} [inst : CommRing R] (f : Polynomial R) (hf : f.Monic),
  (AdjoinRoot.isAdjoinRootMonic f hf).toIsAdjoinRoot = AdjoinRoot.isAdjoinRoot f
-- Mathlib.Data.NNRat.BigOperators
NNRat.cast_prod : ∀ {α : Type u_1} {K : Type u_2} [inst : Semifield K] [CharZero K] (s : Finset α) (f : α → ℚ≥0),
  ↑(∏ a ∈ s, f a) = ∏ a ∈ s, ↑(f a)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_le_of_le_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup M) {T : Subsemigroup N} {f : M →ₙ* N},
  S ≤ Subsemigroup.comap f T → Subsemigroup.map f S ≤ T
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCommSq.domain : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (self : AlgebraicGeometry.ValuativeCommSq f), IsDomain self.R
-- Mathlib.Analysis.Meromorphic.Order
/-- If the order of a meromorphic function is negative, then this function converges to infinity
at this point. See also the iff version `tendsto_cobounded_iff_meromorphicOrderAt_neg`.  -/
tendsto_cobounded_of_meromorphicOrderAt_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  meromorphicOrderAt f x < 0 → Filter.Tendsto f (nhdsWithin x {x}ᶜ) (Bornology.cobounded E)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.aemeasurable_withDensity_ennreal_iff' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → NNReal},
  AEMeasurable f μ →
    ∀ {g : α → ENNReal}, AEMeasurable g (μ.withDensity fun x => ↑(f x)) ↔ AEMeasurable (fun x => ↑(f x) * g x) μ
-- Mathlib.ModelTheory.Order
FirstOrder.Language.model_preorder : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : Preorder M]
  [L.OrderedStructure M], M ⊨ L.preorderTheory
-- Std.Http.Protocol.H1.Message
/-- Direction of message flow from the server's perspective.
 -/
Std.Http.Protocol.H1.Direction : Type
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.edist_integral_le_lintegral_edist : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f g : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  μ.Integrable f →
    μ.Integrable g →
      edist ∫ᵛ (a : X), f a ∂[B; μ] ∫ᵛ (a : X), g a ∂[B; μ] ≤ ‖B‖ₑ * ∫⁻ (a : X), edist (f a) (g a) ∂μ.variation
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- The approximations of the least fixed point stabilize at a fixed point of `f`  -/
OrdinalApprox.lfpApprox_eq_of_mem_fixedPoints : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a b : Ordinal.{u}},
  a ≤ b →
    OrdinalApprox.lfpApprox f x a ∈ Function.fixedPoints ⇑f →
      OrdinalApprox.lfpApprox f x b = OrdinalApprox.lfpApprox f x a
-- Init.Data.Vector.Basic
/-- Set an element in a vector using a `Nat` index. Returns the vector unchanged if the index is out of
bounds.

This will perform the update destructively provided that the vector has a reference count of 1.
 -/
Vector.setIfInBounds : {α : Type u_1} → {n : ℕ} → Vector α n → ℕ → α → Vector α n
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
_private.Mathlib.MeasureTheory.Constructions.HaarToSphere.0.termDim : Lean.ParserDescr
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfterM.match_5.splitter : {α₂ γ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Option (Std.IterM m γ) → Sort u_3) →
      (it₂ : Option (Std.IterM m γ)) →
        (it₂ = none → motive none) → ((it₂_1 : Std.IterM m γ) → it₂ = some it₂_1 → motive (some it₂_1)) → motive it₂
-- Mathlib.Topology.MetricSpace.Holder
holderWith_one : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C : NNReal} {f : X → Y},
  HolderWith C 1 f ↔ LipschitzWith C f
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.intersection_covering_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S R : CategoryTheory.Sieve X}
  (J : CategoryTheory.GrothendieckTopology C), R ⊓ S ∈ J X ↔ R ∈ J X ∧ S ∈ J X
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.instLeAtTopConditional : ∀ (β : Type u_2) [inst : Preorder β] [inst_1 : LocallyFiniteOrder β], (SummationFilter.conditional β).LeAtTop
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableAt.sub_iff_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E}, DifferentiableAt 𝕜 g x → (DifferentiableAt 𝕜 (f - g) x ↔ DifferentiableAt 𝕜 f x)
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.counitAlgHom_comp_includeRight : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Bialgebra R B],
  (AlgHom.restrictScalars R (Bialgebra.counitAlgHom A (TensorProduct R A B))).comp Algebra.TensorProduct.includeRight =
    (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R B)
-- Mathlib.Analysis.Normed.Ring.Basic
norm_intCast_abs : ∀ {α : Type u_2} [inst : SeminormedRing α] (z : ℤ), ‖↑|z|‖ = ‖↑z‖
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.instZSMul.eq_1 : ∀ {M : Type u_5} {S : Type u_6} [inst : SubNegMonoid M] [inst_1 : SetLike S M] [inst_2 : AddSubgroupClass S M] {H : S},
  AddSubgroupClass.instZSMul = { smul := fun n a => ⟨n • ↑a, ⋯⟩ }
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.transIsEquivalentEventuallyEq : {α : Type u_1} →
  {β : Type u_2} →
    [inst : NormedAddCommGroup β] →
      {l : Filter α} → Trans (Asymptotics.IsEquivalent l) l.EventuallyEq (Asymptotics.IsEquivalent l)
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- **Stirling's Formula**  -/
Stirling.tendsto_stirlingSeq_sqrt_pi : Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds √Real.pi)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Multiset.aestronglyMeasurable_prod : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [inst : CommMonoid M]
  [inst_1 : TopologicalSpace M] [ContinuousMul M] (l : Multiset (α → M)),
  (∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) → MeasureTheory.AEStronglyMeasurable l.prod μ
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.homCategory.ext_iff : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} {m n : η ⟶ θ}, m = n ↔ ∀ (b : B), m.as.app b = n.as.app b
-- Mathlib.LinearAlgebra.Matrix.WithConv
instStarRingWithConvMatrix : {m : Type u_1} →
  {n : Type u_2} →
    {α : Type u_3} → [inst : NonUnitalNonAssocSemiring α] → [StarRing α] → StarRing (WithConv (Matrix m n α))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getD.eq_def : ∀ {α : Type u} {δ : Type w} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α fun x => δ) (k : α) (fallback : δ),
  Std.DTreeMap.Internal.Impl.Const.getD t k fallback =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => fallback
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r =>
      match compare k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getD l k fallback
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getD r k fallback
      | Ordering.eq => v'
-- Aesop.Util.UnorderedArraySet
/-- O(1)  -/
Aesop.UnorderedArraySet.isEmpty : {α : Type u_1} → [inst : BEq α] → Aesop.UnorderedArraySet α → Bool
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Icc_iff_integrableOn_Ioo' : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {a b : α},
  μ {a} ≠ ⊤ →
    autoParam (‖f a‖ₑ ≠ ⊤) integrableOn_Icc_iff_integrableOn_Ioo'._auto_1 →
      μ {b} ≠ ⊤ →
        autoParam (‖f b‖ₑ ≠ ⊤) integrableOn_Icc_iff_integrableOn_Ioo'._auto_3 →
          (MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.TypeDefinitionParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams),
  sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams } = 1 + sizeOf toTextDocumentPositionParams
-- Mathlib.Algebra.Polynomial.CoeffList
Polynomial.coeffList_neg : ∀ {R : Type u_1} [inst : Ring R] (P : Polynomial R), (-P).coeffList = List.map (fun x => -x) P.coeffList
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.Scheme.hom_unique_of_empty_source : (X : AlgebraicGeometry.Scheme) → Unique (∅ ⟶ X)
-- Init.Data.Array.QSort.Basic
Array.qpartition.congr_simp : ∀ {α : Type u_1} {n : ℕ} (as as_1 : Vector α n),
  as = as_1 →
    ∀ (lt lt_1 : α → α → Bool),
      lt = lt_1 →
        ∀ (lo hi : ℕ) (w : lo ≤ hi) (hlo : lo < n) (hhi : hi < n),
          Array.qpartition as lt lo hi w hlo hhi = Array.qpartition as_1 lt_1 lo hi w hlo hhi
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.forEachENode : (Lean.Meta.Grind.ENode → Lean.Meta.Grind.GoalM Unit) → Lean.Meta.Grind.GoalM Unit
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.SavedState.mk : Lean.Elab.Term.SavedState → Lean.Elab.Tactic.State → Lean.Elab.Tactic.SavedState
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_support_of_subsingletonAddUnits : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : DecidableEq β] [inst_1 : AddCommMonoid M] (f : α → β)
  [Subsingleton (AddUnits M)] (x : α →₀ M), (Finsupp.mapDomain f x).support = Finset.image f x.support
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.mem_span_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {N : Type u_3} [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : Module S N] [IsScalarTower R S N] {x : N} {a : Set N},
  x ∈ Submodule.span S a ↔ ∃ y ∈ Submodule.span R a, ∃ z, x = IsLocalization.mk' S 1 z • y
-- Mathlib.Data.TypeVec
TypeVec.fst_prod_mk : ∀ {n : ℕ} {α α' β β' : TypeVec.{u_1} n} (f : α.Arrow β) (g : α'.Arrow β'),
  TypeVec.comp TypeVec.prod.fst (TypeVec.prod.map f g) = TypeVec.comp f TypeVec.prod.fst
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.map_zero' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.AddMonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal], F.map 0 = 0
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toArray_eq_match_rco : ∀ {α : Type u} {r : Std.Roo α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α],
  r.toArray =
    match Std.PRange.succ? r.lower with
    | none => #[]
    | some next => (next...r.upper).toArray
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
/-- Bounding the norm of the iterated derivative of `B (f x) (g x)` in terms of the
iterated derivatives of `f` and `g` when `B` is bilinear of norm at most `1`:
`‖D^n (x ↦ B (f x) (g x))‖ ≤ ∑_{k ≤ n} n.choose k ‖D^k f‖ ‖D^{n-k} g‖`  -/
ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {D : Type uD} [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace 𝕜 D] {E : Type uE} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {F : Type uF}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {G : Type uG} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : D → E} {g : D → F} {N : WithTop ℕ∞},
  ContDiff 𝕜 N f →
    ContDiff 𝕜 N g →
      ∀ (x : D) {n : ℕ},
        ↑n ≤ N →
          ‖B‖ ≤ 1 →
            ‖iteratedFDeriv 𝕜 n (fun y => (B (f y)) (g y)) x‖ ≤
              ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.continuousWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [ContinuousAdd F] [ContinuousSMul 𝕜 F], HasFDerivWithinAt f f' s x → ContinuousWithinAt f s x
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.Rel₂ : (m : Type w → Type w') →
  {α₁ β₁ : Type w} →
    [inst : Std.Iterator α₁ m β₁] →
      {α₂ β₂ : Type w} →
        [inst_1 : Std.Iterator α₂ m β₂] →
          [Std.Iterators.Productive α₁ m] →
            [Std.Iterators.Finite α₂ m] → Std.IterM m (β₁ × β₂) → Std.IterM m (β₁ × β₂) → Prop
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.arrowι.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J]
  [inst_2 : CategoryTheory.Limits.HasIterationOfShape J C] {i : J} (F F_1 : CategoryTheory.Functor (↑(Set.Iio i)) C),
  F = F_1 →
    ∀ (hi : Order.IsSuccLimit i) (k k_1 : J) (e_k : k = k_1) (hk : k < i),
      CategoryTheory.SmallObject.SuccStruct.arrowι F hi k hk = CategoryTheory.SmallObject.SuccStruct.arrowι F_1 hi k_1 ⋯
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Surjective.comp_iff : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.Surjective f],
  AlgebraicGeometry.Surjective (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.Surjective g
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjointDomainMkCLM_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F)
  (y : ↥T.adjointDomain) (x : ↥T.domain), (T.adjointDomainMkCLM y) x = inner 𝕜 (↑y) (↑T x)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_sub_const_Ioc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x - a) '' Set.Ioc b c = Set.Ioc (b - a) (c - a)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The `AddHom` from the preimage of an additive subsemigroup to itself.  -/
AddHom.subsemigroupComap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Add M] → [inst_1 : Add N] → (f : M →ₙ+ N) → (N' : AddSubsemigroup N) → ↥(AddSubsemigroup.comap f N') →ₙ+ ↥N'
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.has_seq_basis : ∀ (α : Type ua) [inst : UniformSpace α] [(uniformity α).IsCountablyGenerated],
  ∃ V, (uniformity α).HasAntitoneBasis V ∧ ∀ (n : ℕ), (V n).IsSymm
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.unop_eq_top : ∀ {G : Type u_2} [inst : AddGroup G] {S : AddSubgroup Gᵃᵒᵖ}, S.unop = ⊤ ↔ S = ⊤
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.Hom.hom'.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  {R : CategoryTheory.InjectiveResolution X} {X' : C} {R' : CategoryTheory.InjectiveResolution X'} {f : X ⟶ X'}
  (φ : R.Hom R' f), φ.hom' = HomologicalComplex.extendMap φ.hom ComplexShape.embeddingUpNat
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.conjTranspose_nonsing_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [inst_3 : StarRing α], A⁻¹.conjTranspose = A.conjTranspose⁻¹
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.instNonemptyStructuredArrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] (d : D), Nonempty (CategoryTheory.StructuredArrow d F)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.xor_assoc : ∀ (x y z : ℕ), x ^^^ y ^^^ z = x ^^^ (y ^^^ z)
-- Mathlib.GroupTheory.ArchimedeanDensely
LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Nontrivial G] (g : G),
  ({x | x ≤ g}.WellFoundedOn fun x1 x2 => x1 > x2) ↔ Nonempty (G ≃+o ℤ)
-- Mathlib.ModelTheory.Syntax
/-- Maps a formula's symbols along a language map.  -/
FirstOrder.Language.LHom.onFormula : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → {α : Type u'} → (L →ᴸ L') → L.Formula α → L'.Formula α
-- Init.Data.SInt.Lemmas
ISize.ofInt_mul : ∀ (a b : ℤ), ISize.ofInt (a * b) = ISize.ofInt a * ISize.ofInt b
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.Gammaℝ_ne_zero_of_re_pos : ∀ {s : ℂ}, 0 < s.re → s.Gammaℝ ≠ 0
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.isReduced_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  P.IsReduced ↔ ∀ (i j : ι), ¬LinearIndependent R ![P.root i, P.root j] → P.root i = P.root j ∨ P.root i = -P.root j
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel.decidablePred : {α : Type u_1} →
  {r : α → α → Prop} → (sym : Std.Symm r) → [h : DecidableRel r] → DecidablePred fun x => x ∈ Sym2.fromRel sym
-- Mathlib.CategoryTheory.Abelian.Basic
/-- The canonical morphism `i : coimage f ⟶ Q` is a monomorphism  -/
CategoryTheory.Abelian.instMonoFactorThruCoimage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  CategoryTheory.Mono (CategoryTheory.Abelian.factorThruCoimage f)
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Normalization monoid: multiplying with `normUnit` gives a normal form for associated
elements.  -/
NormalizationMonoid : (α : Type u_2) → [MonoidWithZero α] → Type u_2
-- Mathlib.RingTheory.Valuation.Basic
Valuation.comap_apply : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] {S : Type u_7}
  [inst_2 : Ring S] (f : S →+* R) (v : Valuation R Γ₀) (s : S), (Valuation.comap f v) s = v (f s)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.toCone_proj : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J),
  CategoryTheory.Limits.Fan.proj B.toCone j = B.π j
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasStrictFDerivAt.isBigOTVS_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} [ContinuousAdd F] [ContinuousSMul 𝕜 F],
  HasStrictFDerivAt f f' x → (fun p => f p.1 - f p.2) =O[𝕜; nhds (x, x)] fun p => p.1 - p.2
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, returning `fallback` if no such key exists.
 -/
Std.ExtDTreeMap.getKeyLED : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → α → α
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.algEquiv_apply_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : Ring T] [inst_4 : Algebra R T] (h' : IsAdjoinRoot T f)
  (z : Polynomial R), (h.algEquiv h') (h.map z) = h'.map z
-- Lean.Elab.PreDefinition.MkInhabitant
_private.Lean.Elab.PreDefinition.MkInhabitant.0.Lean.Elab.mkInhabitant? : Lean.Expr → Bool → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Geometry.Manifold.SmoothEmbedding
Manifold.IsSmoothEmbedding.isImmersion : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} {E₃ : Type u_4} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : NormedAddCommGroup E₃] [inst_4 : NormedSpace 𝕜 E₃] {H : Type u_6} {G : Type u_8}
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E₁ H}
  {J : ModelWithCorners 𝕜 E₃ G} {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsSmoothEmbedding I J n f → Manifold.IsImmersion I J n f
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsFragment.inter : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A B S : Finset G},
  K ≤ 1 →
    S.Nonempty → Finset.IsFragment✝ K S A → Finset.IsFragment✝ K S B → (A ∩ B).Nonempty → Finset.IsFragment✝ K S (A ∩ B)
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.toReal_klDiv_smul_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
      ∀ {c : NNReal},
        c ≠ 0 →
          (InformationTheory.klDiv μ (c • ν)).toReal =
            (InformationTheory.klDiv μ ν).toReal + (↑c - 1) * ν.real Set.univ - Real.log ↑c * μ.real Set.univ
-- Mathlib.NumberTheory.RamificationInertia.Inertia
Ideal.inertiaDeg'_ne_zero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [p.IsMaximal] [Module.Finite R S] [P.LiesOver p], p.inertiaDeg' P ≠ 0
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.instGroup : {D : Type u_1} → {Q : Type u_2} → [Group D] → [Group Q] → Group (D ≀ᵣ Q)