mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous on a
subset `S : Set X` iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is
equicontinuous on `S`.  -/
IsUniformInducing.equicontinuousOn_iff : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} {β : Type u_8} [tX : TopologicalSpace X] [uα : UniformSpace α]
  [uβ : UniformSpace β] {F : ι → X → α} {S : Set X} {u : α → β},
  IsUniformInducing u → (EquicontinuousOn F S ↔ EquicontinuousOn ((fun x => u ∘ x) ∘ F) S)
-- Lean.Expr
/-- Checks if an expression is an "integer numeral in normal form",
i.e. of type `Nat` or `Int`, and either a natural number numeral in normal form (as specified by `nat?`),
or the negation of a positive natural number numeral in normal form,
and if so returns the integer.
 -/
Lean.Expr.int? : Lean.Expr → Option ℤ
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.Bicategory.instStrictOfIsLocallyDiscrete : ∀ (B : Type u_1) [inst : CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B],
  CategoryTheory.Bicategory.Strict B
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
/-- The functor `toOver X` is the right adjoint to the functor `Over.forget X`.  -/
CategoryTheory.forgetAdjToOver : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X : C) → CategoryTheory.Over.forget X ⊣ CategoryTheory.toOver X
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.mul_sum_of_notMem : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R},
  OrthogonalIdempotents e → ∀ {i : I} {s : Finset I}, i ∉ s → e i * ∑ j ∈ s, e j = 0
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.mem_asSubmodule_iff : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} {σ : Subrepresentation ρ} {v : W}, v ∈ σ.asSubmodule ↔ v ∈ σ
-- Mathlib.Algebra.Ring.Pi
Pi.constNonUnitalRingHom_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : NonUnitalNonAssocSemiring β] (a : β) (a_1 : α),
  (Pi.constNonUnitalRingHom α β) a a_1 = Function.const α a a_1
-- Lean.Elab.Level
Lean.Elab.Level.instMonadNameGeneratorLevelElabM : Lean.MonadNameGenerator Lean.Elab.Level.LevelElabM
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_singleton : ∀ {α : Type u_1} {β : Type u_2} {a : α} {f : (i : ℕ) → α → i < 1 → β},
  #v[a].mapFinIdx f = #v[f 0 a Vector.mapFinIdx_singleton._proof_1]
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionSpec.julian.inj : ∀ {day day_1 : Std.Time.Internal.Bounded.LE 1 365},
  Std.Time.TimeZone.TransitionSpec.julian day = Std.Time.TimeZone.TransitionSpec.julian day_1 → day = day_1
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.val_toUnits_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(pinGroup Q)), ↑(pinGroup.toUnits x) = ↑x
-- Mathlib.RingTheory.PrincipalIdealDomain
IsBezout.mk : ∀ {R : Type u} [inst : Semiring R], (∀ (I : Ideal R), I.FG → Submodule.IsPrincipal I) → IsBezout R
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a b : α}
  {fallback : β}, cmp a b = Ordering.eq → t.getD a fallback = t.getD b fallback
-- Std.Internal.UV.Loop
/-- Checks if the event loop is still active and processing events.
 -/
Std.Internal.UV.Loop.alive : BaseIO Bool
-- Init.Data.Fin.Lemmas
Fin.eq_mk_iff_val_eq : ∀ {n : ℕ} {a : Fin n} {k : ℕ} {hk : k < n}, a = ⟨k, hk⟩ ↔ ↑a = k
-- Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
SimpleGraph.binomialRandom_zero : ∀ (V : Type u_1) [Countable V], SimpleGraph.binomialRandom V 0 = MeasureTheory.Measure.dirac ⊥
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_erase : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF →
    ∀ {k a : α},
      Std.DHashMap.Internal.Raw₀.Const.get! (m.erase k) a =
        if (k == a) = true then default else Std.DHashMap.Internal.Raw₀.Const.get! m a
-- Mathlib.Topology.Instances.RatLemmas
Rat.cocompact_inf_nhds_neBot : ∀ {p : ℚ}, (Filter.cocompact ℚ ⊓ nhds p).NeBot
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
/-- This lemma establishes a condition under which a subgraph is the same as a connected component.
Note the asymmetry in the hypothesis `h`: `v` is in `H.verts`, but `w` is not required to be.
 -/
SimpleGraph.Subgraph.Connected.exists_verts_eq_connectedComponentSupp : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph},
  H.Connected → (∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w) → ∃ c, H.verts = c.supp
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- "Functoriality" of `MakesOverArrow η s` in `η`.  -/
CategoryTheory.OverPresheafAux.MakesOverArrow.map₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A}
  {μ : G ⟶ A} {ε : F ⟶ G},
  CategoryTheory.CategoryStruct.comp ε μ = η →
    ∀ {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {u : F.obj (Opposite.op X)},
      CategoryTheory.OverPresheafAux.MakesOverArrow η s u →
        CategoryTheory.OverPresheafAux.MakesOverArrow μ s
          ((CategoryTheory.ConcreteCategory.hom (ε.app (Opposite.op X))) u)
-- Mathlib.Data.Matrix.Composition
Matrix.compLinearEquiv_apply : ∀ (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) (R₀ : Type u_7) [inst : Semiring R₀]
  [inst_1 : AddCommMonoid R] [inst_2 : Module R₀ R] (a : Matrix I J (Matrix K L R)),
  (Matrix.compLinearEquiv I J K L R R₀) a = (Matrix.comp I J K L R) a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The finite-quotient diagram viewed in `ProfiniteAddGrp`.  -/
ProfiniteAddGrp.ProfiniteCompletion.diagram : (G : AddGrpCat) → CategoryTheory.Functor (FiniteIndexNormalAddSubgroup ↑G) ProfiniteAddGrp.{u}
-- Init.Control.Lawful.Instances
OptionT.lift.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type u} (x : m α),
  OptionT.lift x =
    OptionT.mk do
      let __do_lift ← x
      pure (some __do_lift)
-- Mathlib.Combinatorics.Matroid.Minor.Order
/-- `≤m` denotes the minor relation on matroids.  -/
Matroid.«term_≤m_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Gluing
TopCat.GlueData.instIsIsoT : ∀ (h : TopCat.GlueData.MkCore) (i j : h.J), CategoryTheory.IsIso (h.t i j)
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.minEntryD.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3) (size : ℕ)
  (k : α) (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β) (x : α × β)
  (h_1 : (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (fallback : α × β) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) =
    h_2 size k v r x
-- Mathlib.Algebra.Group.AddChar
/-- Composing a `MonoidHom` with an `AddChar` yields another `AddChar`.  -/
MonoidHom.compAddChar : {A : Type u_1} →
  {M : Type u_3} →
    [inst : AddMonoid A] →
      [inst_1 : Monoid M] → {N : Type u_5} → [inst_2 : Monoid N] → (M →* N) → AddChar A M → AddChar A N
-- Mathlib.Data.Int.Cast.Lemmas
zmultiplesHom_apply : ∀ (β : Type u_4) [inst : AddGroup β] (x : β) (n : ℤ), ((zmultiplesHom β) x) n = n • x
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_sqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A) (x : ℝ),
  IsUnit a → autoParam (0 ≤ a) CFC.rpow_sqrt._auto_1 → CFC.sqrt a ^ x = a ^ (x / 2)
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Comonad.coalgebraPreadditive_homGroup_sub_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (U : CategoryTheory.Comonad C) [inst_2 : U.Additive] (F G : U.Coalgebra) (α β : F ⟶ G), (α - β).f = α.f - β.f
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_erase_eq_iff_not_compare_eq_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, (t.erase k).min he = t.min ⋯ ↔ ¬cmp k (t.min ⋯) = Ordering.eq
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.mem_range_left : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d) (i : Fin (m + 2)), i ≠ k.castSucc → i ∈ Set.range ⇑(x.cast hd).simplex.1
-- Mathlib.Condensed.Discrete.Characterization
CondensedMod.isDiscrete_tfae : ∀ (R : Type (u + 1)) [inst : Ring R] (M : CondensedMod R),
  [Condensed.IsDiscrete M, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (Condensed.discrete (ModuleCat R)).essImage M, (CondensedMod.LocallyConstant.functor R).essImage M,
      CategoryTheory.IsIso ((CondensedMod.LocallyConstant.adjunction R).counit.app M),
      CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite)
        ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M),
      ∀ (S : Profinite),
        Nonempty
          (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp M.obj).mapCocone S.asLimitCone.op))].TFAE
-- Mathlib.Logic.Equiv.Pairwise
EmbeddingLike.pairwise_comp : ∀ {X : Type u_1} {Y : Type u_2} {F : Sort u_3} [inst : FunLike F Y X] [EmbeddingLike F Y X] (f : F) {p : X → X → Prop},
  Pairwise p → Pairwise (Function.onFun p ⇑f)
-- Init.Data.List.Sublist
List.IsPrefix.isInfix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁ <:+: l₂
-- Mathlib.Algebra.Ring.GeomSum
Nat.pow_sub_pow_dvd_pow_sub_pow : ∀ {m k : ℕ} (x y : ℕ), m ∣ k → x ^ m - y ^ m ∣ x ^ k - y ^ k
-- Lean.MetavarContext
Lean.DependsOn.State.mctx : Lean.DependsOn.State → Lean.MetavarContext
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.card_supp_le_succ_natDegree : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.support.card ≤ p.natDegree + 1
-- Mathlib.Analysis.Calculus.FDeriv.Pow
_private.Mathlib.Analysis.Calculus.FDeriv.Pow.0.aux : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] (f : E → 𝔸) (f' : E →L[𝕜] 𝔸)
  (x : E) (n : ℕ),
  f x • ∑ i ∈ Finset.range (n + 1), MulOpposite.op (f x ^ i) • f x ^ ((n + 1).pred - i) • f' +
      MulOpposite.op (f x ^ (n + 1)) • f' =
    ∑ i ∈ Finset.range (n + 1 + 1), MulOpposite.op (f x ^ i) • f x ^ ((n + 1 + 1).pred - i) • f'
-- Lean.Meta.Sym.SymM
/-- Returns the internalized `True` constant.   -/
Lean.Meta.Sym.getTrueExpr : Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Two closed sets are at zero Hausdorff distance if and only if they coincide.  -/
IsClosed.hausdorffDist_zero_iff_eq : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
  IsClosed s → IsClosed t → Metric.hausdorffEDist s t ≠ ⊤ → (Metric.hausdorffDist s t = 0 ↔ s = t)
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid_indep_iff : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : NoZeroDivisors A] {s : Set A},
  (AlgebraicIndependent.matroid R A).Indep s ↔ AlgebraicIndepOn R id s
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegrable_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} (R : ℝ),
  CircleIntegrable f c R ↔
    IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) MeasureTheory.volume 0 (2 * Real.pi)
-- Mathlib.Topology.Category.Profinite.EffectiveEpi
Profinite.effectiveEpiFamily_tfae : ∀ {α : Type} [inst : Finite α] {B : Profinite} (X : α → Profinite) (π : (a : α) → X a ⟶ B),
  [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π),
      ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b].TFAE
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The functor `C ⥤ D × E` obtained from two monoidal functors is monoidal.  -/
CategoryTheory.Functor.Monoidal.prod' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (F : CategoryTheory.Functor C D) →
                    (G : CategoryTheory.Functor C E) → [F.Monoidal] → [G.Monoidal] → (F.prod' G).Monoidal
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `LE.le.sdiff_ssubset_of_nonempty`. -/
HasSubset.Subset.sdiff_ssubset_of_nonempty : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → s.Nonempty → t \ s ⊂ t
-- Mathlib.RingTheory.Trace.Basic
Algebra.trace_eq_zero_of_not_isSeparable : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  ¬Algebra.IsSeparable K L → Algebra.trace K L = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
/-- A natural transformation is co-equifibered if every commutative square of the following form is
a pushout.
```
F(X) → F(Y)
 ↓      ↓
G(X) → G(Y)
```
 -/
CategoryTheory.NatTrans.Coequifibered : {J : Type u_1} →
  {C : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_3} C] → CategoryTheory.MorphismProperty (CategoryTheory.Functor J C)
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.jacobianRelationsOfHasCoeffs.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P P_1 : Algebra.SubmersivePresentation R S ι σ) (e_P : P = P_1)
  (R₀ : Type u_5) [inst_4 : CommRing R₀] [inst_5 : Algebra R₀ R] [inst_6 : Algebra R₀ S] [inst_7 : IsScalarTower R₀ R S]
  [inst_8 : P.HasCoeffs R₀] (i i_1 : σ),
  i = i_1 → P.jacobianRelationsOfHasCoeffs R₀ i = P_1.jacobianRelationsOfHasCoeffs R₀ i_1
-- Mathlib.CategoryTheory.Bicategory.Opposites
/-- A 2-isomorphism in `B` gives a 2-isomorphism in `Bᵒᵖ`  -/
CategoryTheory.Iso.op2_unop : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b : Bᵒᵖ} → {f g : a ⟶ b} → (f.unop ≅ g.unop) → (f ≅ g)
-- Mathlib.Analysis.Calculus.FDeriv.Star
/-- If `f` has derivative `f'` at `z`, then `star ∘ f ∘ star` has derivative `starL ∘ f' ∘ starL`
at `star z`.  -/
HasFDerivAt.star_star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : StarModule 𝕜 F] [inst_8 : ContinuousStar F] [inst_9 : StarAddMonoid E]
  [inst_10 : StarModule 𝕜 E] [inst_11 : ContinuousStar E] [NormedStarGroup 𝕜] {f : E → F} {z : E} {f' : E →L[𝕜] F},
  HasFDerivAt f f' z → HasFDerivAt (star ∘ f ∘ star) (↑(starL 𝕜) ∘SL f' ∘SL ↑(starL 𝕜)) (star z)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_succ : ∀ (a b : Ordinal.{u_1}), a ^ Order.succ b = a ^ b * a
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.le_of_lt_add : ∀ {m a b : ℕ}, a ≡ b [MOD m] → a < b + m → a ≤ b
-- Mathlib.Algebra.Group.Pi.Basic
Pi.leftCancelMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → LeftCancelMonoid (f i)],
  Pi.leftCancelMonoid =
    { toSemigroup := Pi.leftCancelSemigroup.toSemigroup, toOne := Pi.monoid.toOne, one_mul := ⋯, mul_one := ⋯,
      toNPow := Pi.monoid.toNPow, npow_zero := ⋯, npow_succ := ⋯, toIsLeftCancelMul := ⋯ }
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δAux_C : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  (Q : Algebra.Generators S T ι) (r : S),
  (Algebra.Generators.H1Cotangent.δAux R Q) (MvPolynomial.C r) = 1 ⊗ₜ[S] (KaehlerDifferential.D R S) r
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a surjective `CommMonoid` homomorphism `g : M →* P`, and a submonoid `S ⊆ M`,
the induced monoid homomorphism from the localization of `M` at `S` to the
localization of `P` at `g S`, is surjective.
 -/
Submonoid.LocalizationMap.map_surjective_of_surjective : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {Q : Type u_4} [inst_3 : CommMonoid Q],
  Function.Surjective ⇑g → ∀ (k : (Submonoid.map g S).LocalizationMap Q), Function.Surjective ⇑(f.map ⋯ k)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {k : α}, ∅.contains k = false
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.setIntegral_densityProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (n : ℕ) (a : α) {s : Set β},
      MeasurableSet s →
        ∀ {A : Set γ}, MeasurableSet A → ∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a = (κ a).real (A ×ˢ s)
-- Init.Data.Bool
Bool.lt_of_le_of_lt : ∀ {x y z : Bool}, x ≤ y → y < z → x < z
-- Init.System.IO
IO.FS.Metadata.mk.sizeOf_spec : ∀ (accessed modified : IO.FS.SystemTime) (byteSize : UInt64) (type : IO.FS.FileType) (numLinks : UInt64),
  sizeOf { accessed := accessed, modified := modified, byteSize := byteSize, type := type, numLinks := numLinks } =
    1 + sizeOf accessed + sizeOf modified + sizeOf byteSize + sizeOf type + sizeOf numLinks
-- Init.Data.SInt.Lemmas
Int32.toUInt32_ofNat' : ∀ {n : ℕ}, (Int32.ofNat n).toUInt32 = UInt32.ofNat n
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.unitOfList_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α},
  Std.ExtHashMap.unitOfList l = ∅ ↔ l = []
-- Init.Data.Int.Order
Int.toNat_natCast_add_one : ∀ {n : ℕ}, (↑n + 1).toNat = n + 1
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.isOpenEmbedding : ∀ {X : TopCat} {x : ↑X} (U : TopologicalSpace.OpenNhds x),
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (↑U).inclusion')
-- Mathlib.Tactic.NormNum.RealSqrt
Mathlib.Meta.NormNum.isNat_nnrealSqrt : ∀ {x : NNReal} {nx ny : ℕ},
  Mathlib.Meta.NormNum.IsNat x nx → ny * ny = nx → Mathlib.Meta.NormNum.IsNat (NNReal.sqrt x) ny
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection is the unique point in `K` with the
orthogonality property.  -/
Submodule.eq_starProjection_of_mem_of_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] {u v : E},
  v ∈ K → (∀ w ∈ K, inner 𝕜 (u - v) w = 0) → K.starProjection u = v
-- Lean.Meta.ArgsPacker
/-- Given type `(x : A ⊗' B ⊗' … ⊗' D) → R[x]`
return expression of type `(x : A) → (y : B) → … → (z : D) → R[(x,y,z)]`
 -/
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Unary.curryType : Array Lean.Name → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fdiv_cancel_of_fmod_eq_zero : ∀ {a b : ℤ}, a.fmod b = 0 → b * a.fdiv b = a
-- Init.Data.SInt.Bitwise
Int32.shiftRight_xor : ∀ {a b c : Int32}, (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
-- Mathlib.Algebra.AlgebraicCard
Algebraic.infinite_of_charZero : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [CharZero A],
  {x | IsAlgebraic R x}.Infinite
-- Mathlib.Analysis.Convex.Integral
/-- **Jensen's inequality**: if a function `g : E → ℝ` is convex and continuous on a convex closed
set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending
`μ`-a.e. points of a set `t` to `s`, then the value of `g` at the average value of `f` over `t` is
less than or equal to the average value of `g ∘ f` over `t` provided that both `f` and `g ∘ f` are
integrable.  -/
ConvexOn.map_set_average_le : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ},
  ConvexOn ℝ s g →
    ContinuousOn g s →
      IsClosed s →
        μ t ≠ 0 →
          μ t ≠ ⊤ →
            (∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) →
              MeasureTheory.IntegrableOn f t μ →
                MeasureTheory.IntegrableOn (g ∘ f) t μ → g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
-- Lean.LibrarySuggestions.SineQuaNon
/-- The "sine qua non" triggers for imported constants. This is initialized on first use.  -/
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.sineQuaNonTriggerMap : Lean.CoreM (Lean.NameMap (List (Lean.Name × Float)))
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.IsValuedIn.mk : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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} {S : Type u_6}
  [inst_5 : CommRing S] [inst_6 : Algebra S R], (∀ (i j : ι), ∃ s, (algebraMap S R) s = P.pairing i j) → P.IsValuedIn S
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
NonUnitalStarSubsemiring.mem_carrier : ∀ {R : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarRing R] {s : NonUnitalStarSubsemiring R} {x : R},
  x ∈ s.carrier ↔ x ∈ s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_lt_nsmul_left : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftStrictMono M] {a : M} {n m : ℕ},
  0 < a → n < m → n • a < m • a