mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.Images
CategoryTheory.Abelian.coimageImageComparisonFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  (f : CategoryTheory.Arrow C),
  CategoryTheory.Abelian.coimageImageComparisonFunctor.obj f =
    CategoryTheory.Arrow.mk (CategoryTheory.Abelian.coimageImageComparison f.hom)
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Functor.pi_map : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (F : (i : I) → CategoryTheory.Functor (C i) (D i))
  {X Y : (i : I) → C i} (α : X ⟶ Y) (i : I), (CategoryTheory.Functor.pi F).map α i = (F i).map (α i)
-- Mathlib.Topology.Algebra.Group.Basic
AddSubgroup.addCommGroupTopologicalClosure.eq_1 : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G] [inst_3 : T2Space G]
  (s : AddSubgroup G) (hs : ∀ (x y : ↥s), x + y = y + x),
  s.addCommGroupTopologicalClosure hs = { toAddGroup := s.topologicalClosure.toAddGroup, add_comm := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- The set of `PresheafOfModules.{v} R` consisting of objects of the
form `(free R).obj (yoneda.obj X)` for some `X`.  -/
PresheafOfModules.freeYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (R : CategoryTheory.Functor Cᵒᵖ RingCat) → CategoryTheory.ObjectProperty (PresheafOfModules R)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₁_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sc₁._auto_1),
  (X.sc₁ f g fg h n₀ n₁ hn₁).f = X.δ f g n₀ n₁ hn₁
-- Lean.Meta.Tactic.Grind.Types
/-- Runs `k` with the transparency setting specified by `Config.reducible`.
Uses reducible transparency if `reducible` is `true`, otherwise default transparency.
 -/
Lean.Meta.Grind.withGTransparency : {n : Type → Type u_1} →
  {α : Type} → [MonadControlT Lean.MetaM n] → [MonadLiftT Lean.Meta.Grind.GrindM n] → [Monad n] → n α → n α
-- Lean.Parser.Command
Lean.Parser.Command.declValEqns.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J], CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.Data.Finset.Max
Finset.le_min'_iff : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α}, x ≤ s.min' H ↔ ∀ y ∈ s, x ≤ y
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The angle at a point is at most π.  -/
EuclideanGeometry.angle_le_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ p₃ : P), EuclideanGeometry.angle p₁ p₂ p₃ ≤ Real.pi
-- Mathlib.Topology.Algebra.Group.Torsor
/-- The map `p' ↦ p /ₛ p'` as a homeomorphism: `Equiv.constSDiv` as a homeomorphism  -/
Homeomorph.constSDiv : {V : Type u_1} →
  {P : Type u_2} →
    [inst : Group V] →
      [inst_1 : TopologicalSpace V] →
        [inst_2 : Torsor V P] → [inst_3 : TopologicalSpace P] → [IsTopologicalTorsor P] → P → P ≃ₜ V
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.mk_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {h : ‖0‖ ≤ 1}, ⟨0, h⟩ = 0
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.reverse_balRight : ∀ {α : Type u_1} (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  (l.balRight v r).reverse = r.reverse.balLeft v l.reverse
-- Init.Core
instLawfulBEqString : LawfulBEq String
-- Init.Data.SInt.Lemmas
Int8.not_lt : ∀ {a b : Int8}, ¬a < b ↔ b ≤ a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.filter_equiv_self_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool},
  m.WF →
    ((Std.DHashMap.Raw.filter f m).Equiv m ↔
      ∀ (a : α) (h : a ∈ m), f (m.getKey a h) (Std.DHashMap.Raw.Const.get m a h) = true)
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.div : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {s t : 𝕜 → 𝕜'} {U : Set 𝕜},
  MeromorphicOn s U → MeromorphicOn t U → MeromorphicOn (s / t) U
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.b.eq_1 : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] (j : ι),
  f.b j = CategoryTheory.Limits.Sigma.desc fun c => c.mapToSucc
-- Mathlib.Analysis.Calculus.Conformal.InnerProduct
/-- The conformal factor of a conformal map at some point `x`. Some authors refer to this function
as the characteristic function of the conformal map.  -/
conformalFactorAt : {E : Type u_1} →
  {F : Type u_2} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : InnerProductSpace ℝ E] →
          [inst_3 : InnerProductSpace ℝ F] → {f : E → F} → {x : E} → ConformalAt f x → ℝ
-- Mathlib.Data.PFunctor.Multivariate.W
/-- **Alias** of `MvPFunctor.wInd`.

---

Induction principle for `W`  -/
MvPFunctor.w_ind : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u} n} →
      {C : P.W α → Sort v} →
        ((a : P.A) →
            (f' : (P.drop.B a).Arrow α) → (f : P.last.B a → P.W α) → ((i : P.last.B a) → C (f i)) → C (P.wMk a f' f)) →
          (x : P.W α) → C x
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.shiftClosure_eq_iSup : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms] (G : Type u_4) [inst_2 : AddGroup G] [inst_3 : CategoryTheory.HasShift C G],
  P.shiftClosure G = ⨆ x, P.shift x
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.Quotient.fintype : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [Fintype M] → (S : Submodule R M) → Fintype (M ⧸ S)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback fallback' : α}, t.getD (t.maxD fallback) fallback' = t.maxD fallback
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.End.invtSubmodule 0 = ⊤
-- Mathlib.Condensed.Light.Epi
LightCondMod.epi_iff_locallySurjective_on_lightProfinite : ∀ (R : Type u) [inst : Ring R] {X Y : LightCondMod R} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔
    ∀ (S : LightProfinite) (y : ↑(Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ)),
          ∃ x,
            (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x =
              (CategoryTheory.ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H0IsoOfIsTrivial.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.H0IsoOfIsTrivial A = groupHomology.H0IsoOfIsTrivial A
-- Lean.Server.Requests
Lean.Server.ServerRequestResponse.failure : {α : Type} → Lean.JsonRpc.ErrorCode → String → Lean.Server.ServerRequestResponse α
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Γ_obj : ∀ (X : AlgebraicGeometry.Schemeᵒᵖ), AlgebraicGeometry.Scheme.Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op ⊤)
-- Mathlib.Algebra.Module.Defs
add_smul : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r s : R) (x : M),
  (r + s) • x = r • x + s • x
-- Mathlib.Algebra.Free
Magma.AssocQuotient.map.eq_1 : ∀ {α : Type u} [inst : Mul α] {β : Type v} [inst_1 : Mul β] (f : α →ₙ* β),
  Magma.AssocQuotient.map f = Magma.AssocQuotient.lift (Magma.AssocQuotient.of.comp f)
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.cauchyPDF.eq_1 : ∀ (x₀ : ℝ) (γ : NNReal) (x : ℝ),
  ProbabilityTheory.cauchyPDF x₀ γ x = ENNReal.ofReal (ProbabilityTheory.cauchyPDFReal x₀ γ x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation Q → P 2 ≠ 0 → Q 2 = 0 → W'.add P Q = -(Q 1 ^ 2 * P 2) • P
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.π_eq_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I) (b : J.R),
  K.ι.app (CategoryTheory.Limits.WalkingMultispan.right b) = K.π b
-- Init.Data.List.SplitOn.Lemmas
/-- If no element satisfies `p` in the list `xs`, then `xs.splitOnP p = [xs]`  -/
List.splitOnP_eq_singleton : ∀ {α : Type u_1} {p : α → Bool} {xs : List α}, (∀ x ∈ xs, p x = false) → List.splitOnP p xs = [xs]
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- A functor `F : J ⥤ C` is eventually constant to `j : J` if
for any map `f : i ⟶ j`, the induced morphism `F.map f` is an isomorphism.
If `J` is cofiltered, this implies `F` has a limit.  -/
CategoryTheory.Functor.IsEventuallyConstantTo : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] → CategoryTheory.Functor J C → J → Prop
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.toCycles_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.toCycles i j) (K.iCycles j) = K.d i j
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.isLieAbelian_cartan : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H), IsLieAbelian ↥H
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.toWord_eq_nil_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {x : FreeAddGroup α}, x.toWord = [] ↔ x = 0
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj.congr_simp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {U : CategoryTheory.Functor B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B)
  (F' : CategoryTheory.Functor C A) (adj₁ adj₁_1 : F ⊣ U),
  adj₁ = adj₁_1 →
    ∀ (adj₂ adj₂_1 : F' ⊣ R.comp U),
      adj₂ = adj₂_1 →
        ∀ [inst_3 : CategoryTheory.Limits.HasReflexiveCoequalizers A] (Y Y_1 : B),
          Y = Y_1 →
            CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj R F' adj₁ adj₂ Y =
              CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj R F' adj₁_1 adj₂_1 Y_1
-- Mathlib.FieldTheory.PrimitiveElement
/-- **Primitive element theorem** assuming E is finite.  -/
Field.exists_primitive_element_of_finite_top : ∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] [Finite E], ∃ α, F⟮α⟯ = ⊤
-- Mathlib.Geometry.Manifold.BumpFunction
/-- Given `s ∈ 𝓝 c`, the supports of smooth bump functions `f : SmoothBumpFunction I c` such that
`tsupport f ⊆ s` form a basis of `𝓝 c`.  In other words, each of these supports is a
neighborhood of `c` and each neighborhood of `c` includes `support f` for some
`f : SmoothBumpFunction I c` such that `tsupport f ⊆ s`.  -/
SmoothBumpFunction.nhds_basis_support : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  [inst_5 : FiniteDimensional ℝ E] [T2Space M] {s : Set M},
  s ∈ nhds c → (nhds c).HasBasis (fun f => tsupport ↑f ⊆ s) fun f => Function.support ↑f
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- Commutative Hopf algebras over a commutative ring `R` are the same thing as cogroup
`R`-algebras.  -/
commHopfAlgCatEquivCogrpCommAlgCat : (R : Type u) → [inst : CommRing R] → CommHopfAlgCat R ≌ (CategoryTheory.Grp (CommAlgCat R)ᵒᵖ)ᵒᵖ
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.degree_spanningCoe : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (v : V) [inst : Fintype ↑(G'.neighborSet v)]
  [inst_1 : Fintype ↑(G'.spanningCoe.neighborSet v)], G'.spanningCoe.degree v = G'.degree v
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_eq_if : ∀ {m n : ℤ}, (m...n).toList = if m < n then m :: ((m + 1)...n).toList else []
-- Mathlib.Data.Finset.Lattice.Prod
Finset.sup'_product_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] {s : Finset β} {t : Finset γ}
  (h : (s ×ˢ t).Nonempty) (f : β × γ → α), (s ×ˢ t).sup' h f = t.sup' ⋯ fun i' => s.sup' ⋯ fun i => f (i, i')
-- Init.Data.List.Lemmas
List.filterMap_eq_filter : ∀ {α : Type u_1} {p : α → Bool}, List.filterMap (Option.guard fun x => p x) = List.filter p
-- Mathlib.Geometry.Manifold.StructureGroupoid
instMembershipOpenPartialHomeomorphStructureGroupoid : {H : Type u_1} → [inst : TopologicalSpace H] → Membership (OpenPartialHomeomorph H H) (StructureGroupoid H)
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- The global ref for looking up `apply at` lemmas.  -/
Mathlib.Tactic.ClickSuggestions.appAtRef : IO.Ref (Option (Lean.Meta.RefinedDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyAtLemma))
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.orthRadius.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p : P),
  s.orthRadius p = AffineSubspace.mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ
-- Init.WFComputable
/-- A computable version of `WellFounded.fixF`.  -/
WellFounded.fixFC : {α : Sort u} →
  {r : α → α → Prop} → {C : α → Sort v} → ((x : α) → ((y : α) → r y x → C y) → C x) → (x : α) → Acc r x → C x
-- Mathlib.Data.List.Chain
List.isChain_cons_iff_forall₂ : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α},
  List.IsChain R (a :: l) ↔ l = [] ∨ List.Forall₂ R (a :: l.dropLast) l
-- Init.Data.SInt.Lemmas
UInt64.toInt64_ofNatLT : ∀ {n : ℕ} (hn : n < UInt64.size), (UInt64.ofNatLT n hn).toInt64 = Int64.ofNat n
-- Mathlib.Data.List.Nodup
List.Nodup.cons : ∀ {α : Type u} {l : List α} {a : α}, a ∉ l → l.Nodup → (a :: l).Nodup
-- Mathlib.Analysis.Complex.Norm
Complex.abs_im_eq_norm : ∀ {z : ℂ}, |z.im| = ‖z‖ ↔ z.re = 0
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Coloring.mem_colorClasses : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) {v : V}, C.colorClass (C v) ∈ C.colorClasses
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.mul_left_cancel_iff' : ∀ {a b c m : ℕ}, c ≠ 0 → (c * a ≡ c * b [MOD c * m] ↔ a ≡ b [MOD m])
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.instLT.eq_1 : ∀ {M : Type u_1} [inst : Group M] [inst_1 : Lattice M],
  MulArchimedeanOrder.instLT =
    { lt := fun a b => ∀ (n : ℕ), |MulArchimedeanOrder.val b|ₘ ^ n < |MulArchimedeanOrder.val a|ₘ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} {fallback : β a}, t.contains a = false → t.getD a fallback = fallback
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.HasIntegral.add : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f g : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y y' : F},
  BoxIntegral.HasIntegral I l f vol y →
    BoxIntegral.HasIntegral I l g vol y' → BoxIntegral.HasIntegral I l (f + g) vol (y + y')
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableAt_ofNat : ∀ {𝕜 : 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] (n : ℕ) [inst_7 : OfNat F n] (x : E), DifferentiableAt 𝕜 (OfNat.ofNat n) x
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_35 : HSub Std.Time.Day.Offset Std.Time.Week.Offset Std.Time.Day.Offset
-- Lean.Meta.Instances
Lean.Meta.getDefaultInstancesPriorities : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → m Lean.Meta.PrioritySet
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.toTree.eq_def : ∀ (p : DyckWord),
  p.toTree = if p = 0 then BinaryTree.nil else BinaryTree.node () p.insidePart.toTree p.outsidePart.toTree
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.rangeFactorization : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β},
  Measurable f → Measurable (Set.rangeFactorization f)
-- Mathlib.CategoryTheory.Filtered.Small
/-- The factorization through a small filtered category is in fact a factorization, up to natural
isomorphism.  -/
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoringCompInclusion : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          (F : CategoryTheory.Functor D C) →
            (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoring F).comp
                (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion F) ≅
              F
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
`none` if no such element is found.

`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
iteration.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.findM?` always terminates after finitely many steps.

Example:
```lean example
#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false
```
```output
Almost! 6
Almost! 5
```
```output
some 1
```
 -/
Std.IterM.findM? : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → Std.IterM m β → (β → m (ULift.{w, 0} Bool)) → m (Option β)
-- Init.Data.SInt.Lemmas
Int64.ofNat_sub : ∀ (a b : ℕ), b ≤ a → Int64.ofNat (a - b) = Int64.ofNat a - Int64.ofNat b
-- Init.Prelude
instHMod : {α : Type u_1} → [Mod α] → HMod α α α
-- Init.Sym.Lemmas
Lean.Sym.Int8.lt_eq_false : ∀ (a b : Int8), decide (a < b) = false → (a < b) = False
-- Mathlib.Algebra.Homology.Homotopy
prevD_eq_toPrev_dTo : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (j : ι),
  (prevD j) f = CategoryTheory.CategoryStruct.comp ((toPrev j) f) (D.dTo j)
-- Mathlib.Topology.FiberBundle.Constructions
/-- Equip the total space of the fiberwise product of two fiber bundles `E₁`, `E₂` with
the induced topology from the diagonal embedding into `TotalSpace F₁ E₁ × TotalSpace F₂ E₂`.  -/
FiberBundle.Prod.topologicalSpace : {B : Type u_1} →
  (F₁ : Type u_2) →
    (E₁ : B → Type u_3) →
      (F₂ : Type u_4) →
        (E₂ : B → Type u_5) →
          [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
            [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
              TopologicalSpace (Bundle.TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x)
-- Init.Data.String.Subslice
String.Slice.Subslice.endExclusive_cast : ∀ {s t : String.Slice} {h : s.copy = t.copy} {sl : s.Subslice},
  (String.Slice.Subslice.cast h sl).endExclusive = sl.endExclusive.cast h
-- Mathlib.Order.CompleteLattice.Basic
iSup₂_le : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α},
  (∀ (i : ι) (j : κ i), f i j ≤ a) → ⨆ i, ⨆ j, f i j ≤ a
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X)
  [CategoryTheory.Limits.HasPullbacks C], R.HasPairwisePullbacks
-- Mathlib.Topology.Algebra.Monoid
/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `f : α → M` and `g : α → M` be functions. If `f` tends to zero on a filter `l`
and the image of `l` under `g` is disjoint from the cocompact filter on `M`, then
`fun x : α ↦ f x * g x` also tends to zero on `l`.  -/
Tendsto.tendsto_mul_zero_of_disjoint_cocompact_right : ∀ {M : Type u_3} {α : Type u_6} [inst : TopologicalSpace M] [inst_1 : MulZeroClass M] [ContinuousMul M] {f g : α → M}
  {l : Filter α},
  Filter.Tendsto f l (nhds 0) →
    Disjoint (Filter.map g l) (Filter.cocompact M) → Filter.Tendsto (fun x => f x * g x) l (nhds 0)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] [inst : Inhabited α] {f : (a : α) → β a → γ a} {k : α},
  t.WF → (Std.DTreeMap.Raw.map f t).getKey! k = t.getKey! k
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_eq_some_getD_of_contains : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {a : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.contains a t = true →
        Std.DTreeMap.Internal.Impl.Const.get? t a = some (Std.DTreeMap.Internal.Impl.Const.getD t a fallback)
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_fract : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  Int.fract (Int.fract a) = Int.fract a
-- Mathlib.Analysis.Normed.Module.Complemented
Submodule.coe_continuous_linearProjOfClosedCompl' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {p q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed ↑p)
  (hq : IsClosed ↑q), ⇑(Submodule.linearProjOfClosedCompl p q h hp hq) = ⇑(Submodule.projectionOnto p q h)
-- Mathlib.Combinatorics.HalesJewett
/-- Consider a subspace `l : Subspace η α ι` as a function `(η → α) → ι → α`.  -/
Combinatorics.Subspace.toFun : {η : Type u_5} → {α : Type u_6} → {ι : Type u_7} → Combinatorics.Subspace η α ι → (η → α) → ι → α
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformly.inv : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f : ι → β → α} {g : β → α}, TendstoUniformly f g l → TendstoUniformly f⁻¹ g⁻¹ l
-- Lean.Compiler.Options
Lean.Compiler.compiler.postponeCompile : Lean.Option Bool