mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Germ.Basic
/-- A germ `P` of functions `α → β` is constant w.r.t. `l`.  -/
Filter.Germ.IsConstant : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → l.Germ β → Prop
-- Lean.Elab.Tactic.Try
/-- `evalSuggest` for `first_par` tactic - returns first successful result, cancels others.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestFirstPar : Array (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.instHasRightCalculusOfFractionsOppositeOpOfHasLeftCalculusOfFractions : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [h : W.HasLeftCalculusOfFractions], W.op.HasRightCalculusOfFractions
-- Mathlib.RingTheory.PowerBasis
PowerBasis.minpolyGen_map : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] {S' : Type u_7} [inst_2 : CommRing S']
  [inst_3 : Algebra A S] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S'),
  (pb.map e).minpolyGen = pb.minpolyGen
-- Mathlib.Topology.Compactness.Compact
isCompact_iff_finite : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [DiscreteTopology X], IsCompact s ↔ s.Finite
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore numerator of a fraction.  -/
OreLocalization.oreNum : {R : Type u_1} → [inst : Monoid R] → {S : Submonoid R} → [OreLocalization.OreSet S] → R → ↥S → R
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {A B : CategoryTheory.Mon C} →
        (X : C) →
          (actLeft : CategoryTheory.MonoidalCategoryStruct.tensorObj A.X X ⟶ X) →
            autoParam
                (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) actLeft =
                  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)
                Bimod.one_actLeft._autoParam →
              autoParam
                  (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X) actLeft =
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X X).hom
                      (CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X actLeft) actLeft))
                  Bimod.left_assoc._autoParam →
                (actRight : CategoryTheory.MonoidalCategoryStruct.tensorObj X B.X ⟶ X) →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.one) actRight =
                        (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)
                      Bimod.actRight_one._autoParam →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.mul) actRight =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.associator X B.X B.X).inv
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.whiskerRight actRight B.X) actRight))
                        Bimod.right_assoc._autoParam →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.whiskerRight actLeft B.X) actRight =
                            CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.associator A.X X B.X).hom
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X actRight) actLeft))
                          Bimod.middle_assoc._autoParam →
                        Bimod A B
-- Mathlib.Order.RelIso.Basic
RelIso.coe_toEmbedding : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s), ⇑f.toEmbedding = ⇑f
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- The Euler product for Dirichlet L-series, valid for `s.re > 1`.
This version is stated in terms of `HasProd`.  -/
DirichletCharacter.LSeries_eulerProduct_hasProd : ∀ {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N),
  1 < s.re → HasProd (fun p => (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (LSeries (fun n => χ ↑n) s)
-- Mathlib.Analysis.Fourier.Notation
FourierInvPair.mk : ∀ {E : Type u_5} {F : Type u_6} [inst : FourierTransform F E] [inst_1 : FourierTransformInv E F],
  (∀ (f : E), FourierTransform.fourier (FourierTransformInv.fourierInv f) = f) → FourierInvPair E F
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.idealFactorsFunOfQuotHom_id : ∀ {A : Type u_2} [inst : CommRing A] [inst_1 : IsDedekindDomain A] {J : Ideal A},
  IsDedekindDomain.idealFactorsFunOfQuotHom ⋯ = OrderHom.id
-- Mathlib.Algebra.Category.Grp.Yoneda
/-- The `CommGrpCat`-valued coyoneda embedding.  -/
CommGrpCat.coyoneda : CategoryTheory.Functor CommGrpCatᵒᵖ (CategoryTheory.Functor CommGrpCat CommGrpCat)
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.comp_preservesCofilteredLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
  [CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G],
  CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.minDegree_of_subsingleton : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [Subsingleton V], G.minDegree = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_ext : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l l' : List ((_ : α) × Unit)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys l' →
      (∀ (a : α), Std.Internal.List.containsKey a l = Std.Internal.List.containsKey a l') → l.Perm l'
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.convMul_def : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R C] [inst_5 : Coalgebra.IsCocomm R C] (f g : WithConv (C →ₐc[R] A)),
  f * g =
    WithConv.toConv
      ((Bialgebra.mulBialgHom R A).comp
        ((Bialgebra.TensorProduct.map f.ofConv g.ofConv).comp (Bialgebra.comulBialgHom R C)))
-- Mathlib.RingTheory.Flat.Basic
/-- `M` is flat if and only if `f ⊗ 𝟙 M` is injective whenever `f` is an injective linear map
in a universe that `R` fits in.  -/
Module.Flat.iff_rTensor_preserves_injective_linearMapₛ : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Small.{v', u} R],
  Module.Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
      [inst_7 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)
-- Mathlib.NumberTheory.FLT.Four
Fermat42.mul : ∀ {a b c k : ℤ}, k ≠ 0 → (Fermat42 a b c ↔ Fermat42 (k * a) (k * b) (k ^ 2 * c))
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.of_not_lt : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : LT α] [Lean.Grind.ToInt.LT α i]
  {a b : α} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ¬a < b → b' ≤ a'
-- Std.Data.DTreeMap.Internal.WF.Defs
_private.Std.Data.DTreeMap.Internal.WF.Defs.0.Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.Data.Multiset.Basic
Multiset.strongInductionOn.eq_def : ∀ {α : Type u_1} {p : Multiset α → Sort u_3} (s : Multiset α)
  (ih : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s),
  s.strongInductionOn ih = ih s fun t _h => t.strongInductionOn ih
-- Mathlib.Order.FixedPoints
OrderHom.isGreatest_gfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), IsGreatest (Function.fixedPoints ⇑f) (OrderHom.gfp f)
-- Mathlib.Tactic.ClickSuggestions.TryPremises
/-- An array of candidate lemmas, corresponding to a single section.  -/
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates : Type
-- Mathlib.CategoryTheory.Functor.Basic
/-- A functor preserves identity morphisms.  -/
CategoryTheory.Functor.map_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (self : CategoryTheory.Functor C D) (X : C),
  self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) (r : ℝ),
  μ (Metric.closedBall x r) = μ (Metric.ball x r)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.pullbackObjIso_hom_comp_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D)
  {Z : C} (h : G.obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackObjIso f g d).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (f.app d) (g.app d)) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pullback.snd f g).app d) h
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cycles₁IsoOfIsTrivial.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  groupHomology.cycles₁IsoOfIsTrivial A = groupHomology.cycles₁IsoOfIsTrivial A
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.bot_orthogonal_eq_top : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ⊥ᗮ = ⊤
-- Mathlib.Analysis.Normed.Group.Defs
/-- An enormed commutative monoid is a commutative monoid endowed with a continuous enorm
which is positive definite.  -/
ENormedCommMonoid : (E : Type u_8) → [TopologicalSpace E] → Type u_8
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.projectiveSeminorm_tprod_le : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (m : (i : ι) → E i),
  ‖⨂ₜ[𝕜] (i : ι), m i‖ ≤ ∏ i, ‖m i‖
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃)
  [CategoryTheory.Presheaf.IsLocallySurjective J f₁] [CategoryTheory.Presheaf.IsLocallySurjective J f₂],
  CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.CategoryStruct.comp f₁ f₂)
-- Mathlib.Data.PFun
PFun.mem_prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α →. γ} {g : β →. δ} {x : α × β} {y : γ × δ},
  y ∈ f.prodMap g x ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The inclusion maps into the abstract finite coproduct are open embeddings.  -/
CompHausLike.Sigma.isOpenEmbedding_ι : ∀ {P : TopCat → Prop} {α : Type w} [inst : Finite α] (X : α → CompHausLike P)
  [inst_1 : CompHausLike.HasExplicitFiniteCoproduct X] (a : α),
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι X a))
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.whiskerRight_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] {X₁ X₂ : P.FullSubcategory} (f : X₁ ⟶ X₂)
  (Y : P.FullSubcategory),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y =
    CategoryTheory.ObjectProperty.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.obj)
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
RealRMK.instIsFiniteMeasureRieszMeasure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  [inst_4 : CompactSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ),
  MeasureTheory.IsFiniteMeasure (RealRMK.rieszMeasure Λ)
-- Init.Data.Vector.Count
Vector.count_set : ∀ {α : Type u_1} [inst : BEq α] {n i : ℕ} {a b : α} {xs : Vector α n} (h : i < n),
  Vector.count b (xs.set i a h) =
    (Vector.count b xs - if (xs[i] == b) = true then 1 else 0) + if (a == b) = true then 1 else 0
-- Mathlib.Algebra.Group.Action.End
/-- `MulAut.applyDistribMulAction` is faithful.  -/
MulAut.apply_faithfulSMul : ∀ {M : Type u_2} [inst : Monoid M], FaithfulSMul (MulAut M) M
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
LinearMap.finrank_le_finrank_of_surjective : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {M' : Type u_2} [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.Finite R M] {f : M →ₗ[R] M'},
  Function.Surjective ⇑f → Module.finrank R M' ≤ Module.finrank R M
-- Lean.Message
Lean.MessageData.ofExpr : Lean.Expr → Lean.MessageData
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
/-- The morphism of simplicial chain complexes induces by a morphism
of simplicial sets.  -/
SSet.chainComplexMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] → {X Y : SSet} → (X ⟶ Y) → (R : C) → X.chainComplex R ⟶ Y.chainComplex R
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C},
  J₁ = J₂ ↔ ⇑J₁ = ⇑J₂
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.support_smul_subset_vadd_support : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ']
  [inst_2 : VAdd Γ Γ'] [inst_3 : IsOrderedCancelVAdd Γ Γ'] [inst_4 : AddCommMonoid V] [inst_5 : MulZeroClass R]
  [inst_6 : SMulWithZero R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V},
  ((HahnModule.of R).symm (x • y)).support ⊆ x.support +ᵥ ((HahnModule.of R).symm y).support
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.truncate.congr_simp : ∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {m : ℕ} (hm : n ≤ m),
  TruncatedWittVector.truncate hm = TruncatedWittVector.truncate hm
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.top_ne_one : ∀ {α : Type u} [inst : One α], ⊤ ≠ 1
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lof_eq_of : ∀ (R : Type u) [inst : Semiring R] (ι : Type v) (M : ι → Type w) [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i : ι) (b : M i),
  (DirectSum.lof R ι M i) b = (DirectSum.of M i) b
-- Mathlib.Topology.Algebra.Group.Basic
map_mul_right_nhds_one : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (x : G),
  Filter.map (fun x_1 => x_1 * x) (nhds 1) = nhds x
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_mono : Monotone CircleDeg1Lift.translationNumber
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.groupoidPi : {I : Type u} → {J : I → Type u₂} → [(i : I) → CategoryTheory.Groupoid (J i)] → CategoryTheory.Groupoid ((i : I) → J i)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.addAction' : {S : Type u'} →
  {R : Type u} →
    {M : Type v} →
      [inst : AddMonoid R] →
        [inst_1 : AddAction R M] →
          [inst_2 : AddMonoid S] →
            [inst_3 : VAdd S R] →
              [inst_4 : AddAction S M] → [VAddAssocClass S R M] → (p : SubAddAction R M) → AddAction S ↥p
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_self_nonneg : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] {x : F}, 0 ≤ RCLike.re (inner 𝕜 x x)
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instSub.eq_1 : ∀ {α : Type u} [inst : AddMonoid α],
  AddUnits.instSub = { sub := fun a b => { val := ↑a + ↑(-b), neg := ↑b + ↑(-a), val_neg := ⋯, neg_val := ⋯ } }
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_anyM : ∀ {γ : Type w} [inst : Lean.Order.PartialOrder γ] {m : Type → Type v} [inst_1 : Monad m]
  [inst_2 : (α : Type) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {α : Type} (f : γ → α → m Bool)
  (xs : List α), Lean.Order.monotone f → Lean.Order.monotone fun x => List.anyM (f x) xs
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.subtype : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : CommGroup α] [IsUniformGroup α] {f : β → α}
  [CompleteSpace α], Multipliable f → ∀ (p : β → Prop), Multipliable (f ∘ Subtype.val)
-- Mathlib.Data.Nat.Factorization.Defs
/-- If `a = ∏ pᵢ ^ nᵢ` and `b = ∏ pᵢ ^ mᵢ`, then `factorizationLCMRight = ∏ pᵢ ^ kᵢ`, where
`kᵢ = mᵢ` if `nᵢ < mᵢ` and `0` otherwise. Note that the product is over the divisors of `lcm a b`,
so if one of `a` or `b` is `0` then the result is `1`.

Note that `factorizationLCMRight a b` is *not* `factorizationLCMLeft b a`: the difference is
that in `factorizationLCMLeft a b` there are the primes whose exponent in `a` is bigger or equal
than the exponent in `b`, while in `factorizationLCMRight a b` there are the primes whose
exponent in `b` is strictly bigger than in `a`. For example `factorizationLCMLeft 2 2 = 2`, but
`factorizationLCMRight 2 2 = 1`.  -/
Nat.factorizationLCMRight : ℕ → ℕ → ℕ
-- Init.Data.UInt.Bitwise
USize.or_assoc : ∀ (a b c : USize), a ||| b ||| c = a ||| (b ||| c)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_eq_toIocMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b c : α}, toIocMod hp a b = toIocMod hp a c ↔ ∃ n, c - b = n • p
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.mem_Icc_algebraMap_iff_norm_le : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {x : A} {r : ℝ},
  0 ≤ r → (x ∈ Set.Icc 0 ((algebraMap ℝ A) r) ↔ 0 ≤ x ∧ ‖x‖ ≤ r)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.singleton.sizeOf_spec : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : SizeOf ι]
  [inst_2 : (a : ι) → SizeOf (M a)] {i : ι} (x : M i) (a : x ≠ 1),
  sizeOf (Monoid.CoprodI.NeWord.singleton x a) = 1 + sizeOf i + sizeOf x
-- Init.Data.String.Defs
/-- The number of bytes of the UTF-8 encoding of the string slice.  -/
String.Slice.utf8ByteSize : String.Slice → ℕ
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of the coordinate-wise `n`th power of a tuple
is `n` times its logarithmic height.  -/
Height.logHeight_pow : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) (n : ℕ),
  Height.logHeight (x ^ n) = ↑n * Height.logHeight x
-- Init.Prelude
/-- Check if a given name refers to a declaration.  -/
Lean.Macro.Methods.hasDecl : Lean.Macro.Methods → Lean.Name → Lean.MacroM Bool
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.pos_of_notMem_negAt_plusPart : ∀ {K : Type u_1} [inst : Field K] {s : Set { w // w.IsReal }} (A : Set (NumberField.mixedEmbedding.mixedSpace K))
  {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ ⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A →
    ∀ {w : { w // w.IsReal }}, w ∉ s → 0 < x.1 w
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
mem_integralClosure_iff : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {a : A},
  a ∈ integralClosure R A ↔ IsIntegral R a
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
deriv.log : ∀ {f : ℝ → ℝ} {x : ℝ}, DifferentiableAt ℝ f x → f x ≠ 0 → deriv (fun x => Real.log (f x)) x = deriv f x / f x
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.uncurrySum_apply : ∀ {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {G : Type wG} {G' : Type wG'} [inst : Fintype ι] [inst_1 : Fintype ι']
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
  [inst_5 : NormedAddCommGroup G'] [inst_6 : NormedSpace 𝕜 G']
  (f : ContinuousMultilinearMap 𝕜 (fun x => G) (ContinuousMultilinearMap 𝕜 (fun x => G) G')) (m : ι ⊕ ι' → G),
  f.uncurrySum m = (f (m ∘ Sum.inl)) (m ∘ Sum.inr)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- Auxiliary definition for `extend.leftHomologyData`.  -/
HomologicalComplex.extend.leftHomologyData.isColimitCokernelCofork : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {i j k : ι} →
                      {i' j' k' : ι'} →
                        (hj' : e.f j = j') →
                          (hi : c.prev j = i) →
                            (hi' : c'.prev j' = i') →
                              (hk : c.next j = k) →
                                (hk' : c'.next j' = k') →
                                  (cone : CategoryTheory.Limits.KernelFork (K.d j k)) →
                                    (hcone : CategoryTheory.Limits.IsLimit cone) →
                                      (cocone :
                                          CategoryTheory.Limits.CokernelCofork
                                            (hcone.lift (CategoryTheory.Limits.KernelFork.ofι (K.d i j) ⋯))) →
                                        CategoryTheory.Limits.IsColimit cocone →
                                          CategoryTheory.Limits.IsColimit
                                            (HomologicalComplex.extend.leftHomologyData.cokernelCofork K e hj' hi hi' hk
                                              hk' cone hcone cocone)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.hom_ext_of_forall : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X ⟶ Y),
  (∀ (x : ↥X), ∃ U, x ∈ U ∧ CategoryTheory.CategoryStruct.comp U.ι f = CategoryTheory.CategoryStruct.comp U.ι g) → f = g
-- Mathlib.Data.Nat.BinaryRec
/-- `bit b` appends the digit `b` to the little end of the binary representation of
its natural number input.  -/
Nat.bit : Bool → ℕ → ℕ