mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- Implementation of the functor `PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X)`
when `X` is initial.

The functor is implemented as, on object level `M ↦ (c ↦ M(c))` where the `R(X)`-module structure
on `M(c)` is given by restriction of scalars along the unique morphism `R(c) ⟶ R(X)`; and on
morphism level `(f : M ⟶ N) ↦ (c ↦ f(c))`.
 -/
PresheafOfModules.forgetToPresheafModuleCatMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (X : Cᵒᵖ) →
        (hX : CategoryTheory.Limits.IsInitial X) →
          {M N : PresheafOfModules R} →
            (M ⟶ N) →
              (PresheafOfModules.forgetToPresheafModuleCatObj X hX M ⟶
                PresheafOfModules.forgetToPresheafModuleCatObj X hX N)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_const : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (y : F),
  MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.const α y) = μ.real Set.univ • y
-- Mathlib.Data.Set.Insert
Set.insert_subset_iff : ∀ {α : Type u_1} {s t : Set α} {a : α}, insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
-- Mathlib.Data.EReal.Basic
EReal.coe_toENNReal_eq_max : ∀ {x : EReal}, ↑x.toENNReal = max 0 x
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulToBackwardSearcherModel.isValidRevSearchFrom_toList : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.Model.PatternModel pat} {σ : String.Slice → Type}
  {inst_1 : String.Slice.Pattern.ToBackwardSearcher pat σ}
  {inst_2 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)}
  {inst_3 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id}
  [self : String.Slice.Pattern.Model.LawfulToBackwardSearcherModel pat] (s : String.Slice),
  String.Slice.Pattern.Model.IsValidRevSearchFrom pat s.endPos
    (String.Slice.Pattern.ToBackwardSearcher.toSearcher pat s).toList
-- Mathlib.Algebra.Module.Torsion.Basic
/-- A module over a domain is torsion-free iff its torsion submodule is trivial.  -/
Submodule.isTorsionFree_iff_torsion_eq_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M],
  Module.IsTorsionFree R M ↔ Submodule.torsion R M = ⊥
-- Mathlib.Order.Fin.Finset
Fin.orderIsoTriple_one : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableEq α] (a b c : α) (hab : a < b) (hbc : b < c),
  ↑((Fin.orderIsoTriple a b c hab hbc) 1) = b
-- Mathlib.NumberTheory.PellMatiyasevic
/-- The Pell `y` sequence.  -/
Pell.yn : {a : ℕ} → 1 < a → ℕ → ℕ
-- Mathlib.MeasureTheory.Measure.Regular
/-- **Alias** of `MeasurableSet.exists_isCompact_isClosed_sdiff_lt`.

---

If `μ` is inner regular for finite measure sets with respect to compact sets,
then any measurable set of finite measure can be approximated by a compact closed subset.
Compared to `MeasurableSet.exists_isCompact_sdiff_lt`,
this lemma additionally assumes that `α` is an R₁ space with Borel σ-algebra.  -/
MeasurableSet.exists_isCompact_isClosed_diff_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [BorelSpace α]
  [R1Space α] [μ.InnerRegularCompactLTTop] ⦃A : Set α⦄,
  MeasurableSet A → μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ (A \ K) < ε
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_ofClass : ∀ {S : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : SetLike S M] [inst_4 : AddSubmonoidClass S M] [inst_5 : SMulMemClass S R M] (s : S),
  ↑(Submodule.ofClass s) = ↑s
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting)
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C],
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.f)
      (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv =
    -CochainComplex.mappingCone.inr (CochainComplex.homOfDegreewiseSplit S σ)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.intervalIntegrable_enorm_iff : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε}
  [TopologicalSpace.PseudoMetrizableSpace ε] {μ : MeasureTheory.Measure ℝ} {a b : ℝ},
  MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b)) →
    (IntervalIntegrable (fun t => ‖f t‖ₑ) μ a b ↔ IntervalIntegrable f μ a b)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- the objects in the coverings of the fibre products  -/
CategoryTheory.PreOneHypercover.Y : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → (self : CategoryTheory.PreOneHypercover S) → ⦃i₁ i₂ : self.I₀⦄ → self.I₁ i₁ i₂ → C
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_mono_enorm_ae : ∀ {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : ENorm ε] [inst_1 : ENorm ε'] {f : α → ε} {g : α → ε'},
  0 ≤ q → (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) → MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNorm' g q μ
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.IsPrefix.of : ∀ {α : Type} {decls1 decls2 : Array (Std.Sat.AIG.Decl α)} (size_le : decls1.size ≤ decls2.size),
  (∀ (idx : ℕ) (h : idx < decls1.size), decls2[idx] = decls1[idx]) → Std.Sat.AIG.IsPrefix decls1 decls2
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.antitoneOn_rpow_Ioi_of_exponent_nonpos : ∀ {r : ℝ}, r ≤ 0 → AntitoneOn (fun x => x ^ r) (Set.Ioi 0)
-- Mathlib.Algebra.Order.Group.Abs
apply_abs_le_add_of_nonneg : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2}
  [inst_3 : AddZeroClass H] [inst_4 : LE H] [AddLeftMono H] [AddRightMono H] {f : G → H},
  (∀ (x : G), 0 ≤ f x) → ∀ (a : G), f |a| ≤ f a + f (-a)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.arrowCongr_refl : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] [inst_5 : Star A₁] [inst_6 : Star A₂],
  (StarAlgEquiv.refl R A₁).arrowCongr (StarAlgEquiv.refl R A₂) = Equiv.refl (A₁ →⋆ₐ[R] A₂)
-- Init.Data.UInt.Lemmas
UInt8.lt_asymm : ∀ {a b : UInt8}, a < b → ¬b < a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ} {k k' : α},
  t.WF → t.getKey? k = some k' → (Std.TreeMap.Raw.filterMap f t)[k]? = t[k]?.bind fun x => f k' x
-- Init.Data.Range.Polymorphic.Iterators
Std.Rii.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLeast?OfMonadOfFiniteIteratorId : {α : Type u} →
  {m : Type u → Type u_1} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : Std.PRange.Least? α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerableLeast? α] →
            [Monad m] → [Std.Iterators.Finite (Std.Rxi.Iterator α) Id] → ForIn' m (Std.Rii α) α inferInstance
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxcIterator.mk.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (iter : Std.DTreeMap.Internal.Zipper α β) (upper : α)
  (iter_1 : Std.DTreeMap.Internal.Zipper α β) (upper_1 : α),
  ({ iter := iter, upper := upper } = { iter := iter_1, upper := upper_1 }) = (iter = iter_1 ∧ upper = upper_1)
-- Mathlib.Topology.MetricSpace.Completion
UniformSpace.Completion.uniformity_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α],
  uniformity (UniformSpace.Completion α) = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε}
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- If-then-else as a `SimpleFunc`.  -/
MeasureTheory.SimpleFunc.piecewise : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      (s : Set α) →
        MeasurableSet s → MeasureTheory.SimpleFunc α β → MeasureTheory.SimpleFunc α β → MeasureTheory.SimpleFunc α β
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
CovariantDerivative.IsMetricCompatible.mvfderiv_inner_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] {V : M → Type u_5}
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → NormedAddCommGroup (V x)]
  [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] [inst_10 : FiberBundle F V] {cov : CovariantDerivative I F V}
  [inst_11 : VectorBundle ℝ F V] [inst_12 : IsContMDiffRiemannianBundle I 1 F V]
  [inst_13 : ContMDiffVectorBundle 1 F V I] [inst_14 : FiniteDimensional ℝ F],
  cov.IsMetricCompatible →
    ∀ {x : M} (X : (x : M) → TangentSpace I x) {σ τ : (x : M) → V x},
      MDiffAt (T% σ) x →
        MDiffAt (T% τ) x →
          ((d% fun x => inner ℝ (σ x) (τ x)) x) (X x) =
            (fun x => inner ℝ ((fun x => (↑cov σ x) (X x)) x) (τ x)) x +
              (fun x => inner ℝ (σ x) ((fun x => (↑cov τ x) (X x)) x)) x
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.homOfLE_comp_assoc : ∀ {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂) {S₃ : X.Subcomplex} (h' : S₂ ≤ S₃) {Z : SSet} (h_1 : S₃.toSSet ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.homOfLE h)
      (CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.homOfLE h') h_1) =
    CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.homOfLE ⋯) h_1
-- Mathlib.Topology.Compactness.Compact
Pi.exists_compact_superset_iff : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {s : Set ((i : ι) → X i)},
  (∃ K, IsCompact K ∧ s ⊆ K) ↔ ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ Function.eval i ⁻¹' Ki
-- Mathlib.Order.Partition.Basic
Partition.eq_of_mem_inter : ∀ {α : Type u_1} {x : α} {u s t : Set α} {P : Partition u}, t ∈ P → s ∈ P → x ∈ t ∩ s → t = s
-- Mathlib.Algebra.Group.Basic
eq_of_one_div_eq_one_div : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a b : α}, 1 / a = 1 / b → a = b
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.instQuasiCompactSndScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.pullback.snd f g)
-- Init.Data.Option.Lemmas
Option.min_filter_right : ∀ {α : Type u_1} [inst : Min α] [Std.IdempotentOp min] {p : α → Bool} {o : Option α},
  o ⊓ Option.filter p o = Option.filter p o
-- Mathlib.Data.Real.Embedding
Archimedean.ratLt_add : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M]
  [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x y : M),
  Archimedean.ratLt (x + y) = Archimedean.ratLt x + Archimedean.ratLt y
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.pow_mono : ∀ {f g : CircleDeg1Lift}, f ≤ g → ∀ (n : ℕ), f ^ n ≤ g ^ n
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
ClosedSubmodule.mem_orthogonal_toSubmodule_iff : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E) (v : E), v ∈ (↑K)ᗮ ↔ v ∈ Kᗮ
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.ruleSets.injEq : ∀ (rs rs_1 : Aesop.Frontend.RuleSets),
  (Aesop.Frontend.Feature.ruleSets rs = Aesop.Frontend.Feature.ruleSets rs_1) = (rs = rs_1)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {a : α}, ∅[a]? = none
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instOneAdicCauchySequence : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → One (AdicCompletion.AdicCauchySequence I R)
-- Init.Internal.Order.Basic
Lean.Order.bot_le : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] (x : α), Lean.Order.PartialOrder.rel Lean.Order.bot x
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Complex.measurable_arg : Measurable Complex.arg
-- Mathlib.Topology.Order.DenselyOrdered
/-- `Set.Ioc a b` is only closed if it is empty.  -/
isClosed_Ioc_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  IsClosed (Set.Ioc a b) ↔ b ≤ a
-- Mathlib.Topology.CompactOpen
ContinuousMap.isClosed_setOfPred_mapsTo : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {t : Set Y},
  IsClosed t → ∀ (s : Set X), IsClosed {f | Set.MapsTo (⇑f) s t}
-- Mathlib.Algebra.Lie.Classical
/-- An equivalence between two possible definitions of the classical Lie algebra of type B.  -/
LieAlgebra.Orthogonal.typeBEquivSo' : (l : Type u_4) →
  (R : Type u₂) →
    [inst : DecidableEq l] →
      [inst_1 : CommRing R] →
        [inst_2 : Fintype l] →
          [Invertible 2] → ↥(LieAlgebra.Orthogonal.typeB l R) ≃ₗ⁅R⁆ ↥(LieAlgebra.Orthogonal.so' (Unit ⊕ l) l R)
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.unitsSMul_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : Module.Basis ι R M} {w : ι → Rˣ} (i : ι), (v.unitsSMul w) i = w i • v i
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.IsPrefix_push : ∀ {α : Type} {decl : Std.Sat.AIG.Decl α} {decls : Array (Std.Sat.AIG.Decl α)},
  Std.Sat.AIG.IsPrefix decls (decls.push decl)
-- Mathlib.CategoryTheory.Limits.Creates
/-- The identity functor creates all colimits.  -/
CategoryTheory.idCreatesColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₁, u₁, u₁} (CategoryTheory.Functor.id C)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.sub_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → SubNegMonoid (R i)] [inst_2 : ∀ (i : ι), AddSubgroupClass (S i) (R i)]
  (x y : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (i : ι), (x - y) i = x i - y i
-- Mathlib.Algebra.Category.MonCat.Colimits
_private.Mathlib.Algebra.Category.MonCat.Colimits.0.MonCat.Colimits.descFunLift.match_1.eq_3 : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] (F : CategoryTheory.Functor J MonCat)
  (motive : MonCat.Colimits.Prequotient F → Sort u_3) (x y : MonCat.Colimits.Prequotient F)
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (MonCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive MonCat.Colimits.Prequotient.one)
  (h_3 : (x y : MonCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match x.mul y with
    | MonCat.Colimits.Prequotient.of j x => h_1 j x
    | MonCat.Colimits.Prequotient.one => h_2 ()
    | x.mul y => h_3 x y) =
    h_3 x y
-- Std.Http.Data.Headers.Name
Std.Http.Header.instDecidableEqName.decEq : (x x_1 : Std.Http.Header.Name) → Decidable (x = x_1)
-- Mathlib.Algebra.Group.Prod
Prod.instAddSemigroup.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddSemigroup M] [inst_1 : AddSemigroup N],
  Prod.instAddSemigroup = { toAdd := Prod.instAdd, add_assoc := ⋯ }
-- Init.Data.UInt.Lemmas
UInt16.le_ofNat_iff : ∀ {n : UInt16} {m : ℕ}, m < UInt16.size → (n ≤ UInt16.ofNat m ↔ n.toNat ≤ m)
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.extendRight.isIntegralClosure : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  {R : Type u_4} {S : Type u_5} [inst_7 : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra S ↥F]
  [inst_10 : Algebra S M] [inst_11 : IsScalarTower S (↥F) M] [inst_12 : Algebra R ↥F] [inst_13 : Algebra R M]
  [inst_14 : IsScalarTower R (↥F) M] [IsIntegralClosure S R ↥F], IsIntegralClosure S R ↥(F.extendRight M)
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.map_iSup : ∀ {α : Type u} {β : Type v} {ι : Sort x} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f : α → β},
  LeftOrdContinuous f → ∀ [Nonempty ι] (g : ι → α), f (⨆ i, g i) = ⨆ i, f (g i)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- In a Dedekind domain, for every ideals `0 < I ≤ J` there exists `a` such that `J = I + ⟨a⟩`.
TODO: Show that this property uniquely characterizes Dedekind domains.  -/
IsDedekindDomain.exists_sup_span_eq : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] {I J : Ideal R}, I ≤ J → I ≠ 0 → ∃ a, I ⊔ Ideal.span {a} = J
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.isEagerSplit : Lean.Name → Lean.Meta.Grind.GrindM Bool
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mapMahlerMeasure_mul : ∀ {A : Type u_1} [inst : Semiring A] (v : A →+* ℂ) (f g : Polynomial A),
  (f * g).mapMahlerMeasure v = f.mapMahlerMeasure v * g.mapMahlerMeasure v
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- The yoneda embedding of `FormalCoproduct.{w} C` into `w`-presheaves for a locally
`w`-small category.  -/
CategoryTheory.Limits.FormalCoproduct.shrinkYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] →
      CategoryTheory.Functor (CategoryTheory.Limits.FormalCoproduct C) (CategoryTheory.Functor Cᵒᵖ (Type w))
-- Init.Data.Float.Model.Unpacked.Operations.ToNat
/-- Converts an `UnpackedFloat` to a `UInt32`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.UnpackedFloat.toUInt32 : Float.Model.UnpackedFloat → UInt32
-- Mathlib.Topology.MetricSpace.Bounded
tendsto_cocompact_of_tendsto_dist_comp_atTop : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α} {l : Filter β} (x : α),
  Filter.Tendsto (fun y => dist (f y) x) l Filter.atTop → Filter.Tendsto f l (Filter.cocompact α)
-- Mathlib.Logic.Function.Defs
Function.fst_comp_diag : ∀ {α : Type u_1}, Prod.fst ∘ Function.diag = id
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_eq_zero_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε],
  0 < q → ∀ {f : α → ε}, MeasureTheory.AEStronglyMeasurable f μ → (MeasureTheory.eLpNorm' f q μ = 0 ↔ f =ᵐ[μ] 0)
-- Mathlib.Data.List.Rotate
List.rotate'_cons_succ : ∀ {α : Type u} (l : List α) (a : α) (n : ℕ), (a :: l).rotate' n.succ = (l ++ [a]).rotate' n
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.toEquiv_mkHomeomorph : ∀ {M : Type u_1} [inst : TopologicalSpace M], DomMulAct.mkHomeomorph.toEquiv = DomMulAct.mk
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k k' : α} {f : Option β → Option β} {hc : k' ∈ Std.DTreeMap.Raw.Const.alter t k f},
  Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.Const.alter t k f) k' hc =
    if heq : cmp k k' = Ordering.eq then (f (Std.DTreeMap.Raw.Const.get? t k)).get ⋯
    else Std.DTreeMap.Raw.Const.get t k' ⋯
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- If `a < b * c`, `b` is positive and `0 < c < 1`, then there is a power `c ^ n` with `n : ℤ`
strictly between `a` and `b`.  -/
exists_zpow_btwn_of_lt_mul : ∀ {K : Type u_4} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] [ExistsAddOfLE K]
  {a b c : K}, a < b * c → 0 < b → 0 < c → c < 1 → ∃ n, a < c ^ n ∧ c ^ n < b
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_normal : ∀ {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G) [S.Normal] (n : ℕ), (S.lowerCentralSeries n).Normal
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
/-- The Grothendieck topology on `TopCat` is subcanonical.  -/
TopCat.subcanonical_grothendieckTopology : TopCat.grothendieckTopology.Subcanonical
-- Mathlib.Order.Interval.Finset.Defs
Set.toFinset_Ioi : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α) [inst_2 : Fintype ↑(Set.Ioi a)],
  (Set.Ioi a).toFinset = Finset.Ioi a
-- Mathlib.Data.Finset.Density
Finset.dens_eq_card_div_card : ∀ {α : Type u_2} [inst : Fintype α] (s : Finset α), s.dens = ↑s.card / ↑(Fintype.card α)
-- Mathlib.LinearAlgebra.Goursat
/-- **Goursat's lemma** for an arbitrary submodule of a product.

If `L` is a submodule of `M × N`, then there exist submodules `M'' ≤ M' ≤ M` and `N'' ≤ N' ≤ N` such
that `L ≤ M' × N'`, and `L` is (the image in `M × N` of) the preimage of the graph of an `R`-linear
isomorphism `M' ⧸ M'' ≃ N' ⧸ N''`.  -/
Submodule.goursat : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {L : Submodule R (M × N)},
  ∃ M' N' M'' N'' e,
    L = Submodule.map (M'.subtype.prodMap N'.subtype) (Submodule.comap (M''.mkQ.prodMap N''.mkQ) (↑e).graph)
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_sum_le_of_le : ∀ {ι : Type u_3} {E : Type u_5} [inst : SeminormedAddCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → NNReal},
  (∀ b ∈ s, ‖f b‖₊ ≤ n b) → ‖∑ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b
-- Mathlib.LinearAlgebra.Prod
LinearMap.inl_map_mul : ∀ {R : Type u} [inst : Semiring R] {A : Type u_4} [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {B : Type u_5} [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] (a₁ a₂ : A),
  (LinearMap.inl R A B) (a₁ * a₂) = (LinearMap.inl R A B) a₁ * (LinearMap.inl R A B) a₂
-- Mathlib.Data.Matrix.Basic
/-- A version of `Set.matrix` for `AddSubmonoid`s.
Given an `AddSubmonoid` `S`, `S.matrix` is the `AddSubmonoid` of matrices `m`
all of whose entries `m i j` belong to `S`.  -/
AddSubmonoid.matrix : {m : Type u_2} → {n : Type u_3} → {A : Type u_14} → [inst : AddMonoid A] → AddSubmonoid A → AddSubmonoid (Matrix m n A)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_eq_none : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a : α}, a ∉ t → t.getKey? a = none
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.unopOpIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (X : Cᵒᵖ), F.unopOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- If `F` is an equivalence, it's a right adjoint.  -/
CategoryTheory.Functor.isRightAdjoint_of_isEquivalence : ∀ {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.IsEquivalence], F.IsRightAdjoint
-- Mathlib.Topology.Order.DenselyOrdered
closure_uIoo : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  a ≠ b → closure (Set.uIoo a b) = Set.uIcc a b