mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.repeatTR.loop : {α : Type u} → (α → α) → ℕ → α → α
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiff.finsum_section_of_locallyFinite : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {ι : Type u_7} {t : ι → (x : M) → V x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) →
    (∀ (i : ι), ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, t i x⟩) →
      ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, ∑ᶠ (i : ι), t i x⟩
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLE_arrow_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} {X Y : CategoryTheory.Subobject B} (h : X ≤ Y)
  {Z : C} (h_1 : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ofLE Y h) (CategoryTheory.CategoryStruct.comp Y.arrow h_1) =
    CategoryTheory.CategoryStruct.comp X.arrow h_1
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.instIteratorLoop.loop_eq_wf : ∀ {α : Type u} {n : Type u → Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_5 : Monad n]
  [LawfulMonad n] {γ : Type u} {LargeEnough : α → Prop}
  {hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b} {upperBound next : α}
  {hn : LargeEnough next} {acc : γ} (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxo.Iterator α) Id Pl)
  (f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n (Subtype (Pl out c))),
  Std.Rxo.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl upperBound acc next hn f =
    Std.Rxo.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc next hn f
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.jacobiSymNat.mod_left : ∀ (a b ab : ℕ) (r : ℤ),
  a % b = ab → Mathlib.Meta.NormNum.jacobiSymNat ab b = r → Mathlib.Meta.NormNum.jacobiSymNat a b = r
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwiseDisjoint_singleton' : ∀ {ι : Type u_4} (s : Set ι), s.PairwiseDisjoint singleton
-- Std.Sat.AIG.Lemmas
/-- If an index contains a `Decl.false` we know how to denote it.
 -/
Std.Sat.AIG.denote_idx_false : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {start : ℕ} {assign : α → Bool} {invert : Bool}
  {aig : Std.Sat.AIG α} {hstart : start < aig.decls.size},
  aig.decls[start] = Std.Sat.AIG.Decl.false →
    ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ = invert
-- Mathlib.LinearAlgebra.Projection
Submodule.quotientEquivOfIsCompl_symm_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (h : IsCompl p q) (a : ↥q), (p.quotientEquivOfIsCompl q h).symm a = Submodule.Quotient.mk ↑a
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.unop_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
  {f : X ⟶ Y} (φ : W₁.MapFactorizationData W₂ f), φ.unop.i = φ.p.unop
-- Mathlib.GroupTheory.OrderOfElement
/-- The equivalence between `Subgroup.zmultiples` of two elements `a, b` of the same additive
order, mapping `i • a` to `i • b`.  -/
zmultiplesEquivZMultiples : {G : Type u_1} →
  [inst : AddGroup G] →
    {x y : G} → [Finite G] → addOrderOf x = addOrderOf y → ↥(AddSubgroup.zmultiples x) ≃ ↥(AddSubgroup.zmultiples y)
-- Mathlib.Analysis.Normed.Group.Constructions
Function.Surjective.pi_norm_comp : ∀ {ι : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Fintype ι] [inst_1 : SeminormedAddGroup E] [inst_2 : Fintype F]
  {f : ι → F}, Function.Surjective f → ∀ (g : F → E), ‖g ∘ f‖ = ‖g‖
-- Init.Data.SInt.Lemmas
Int64.toUInt64_ofNat' : ∀ {n : ℕ}, (Int64.ofNat n).toUInt64 = UInt64.ofNat n
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
/-- If `G` has a minimal degree of at least `(1 - 1 / r + o(1)) * n`, then `G` contains a
copy of a `completeEquipartiteGraph` in `r + 1` parts each of size `t`.

This is the minimal-degree version of the **Erdős-Stone theorem**.  -/
SimpleGraph.eventually_completeEquipartiteGraph_isContained_of_minDegree : ∀ {ε : ℝ},
  0 < ε →
    ∀ (r t : ℕ),
      ∀ᶠ (n : ℕ) in Filter.atTop,
        ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
          ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n → (SimpleGraph.completeEquipartiteGraph (r + 1) t).IsContained G
-- Mathlib.Order.KrullDimension
/-- The coheight of an element is infinite iff there exist series of arbitrary length ending in that
element.
 -/
Order.coheight_eq_top_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, Order.coheight x = ⊤ ↔ ∀ (n : ℕ), ∃ p, RelSeries.head p = x ∧ p.length = n
-- Mathlib.GroupTheory.Focal
AddSubgroup.instIsAddCommutativeQuotientSubtypeMemFocalAddSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), IsAddCommutative (↥H ⧸ H.focalAddSubgroupOf)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.take : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsPath → ∀ (n : ℕ), (p.take n).IsPath
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformlyOn.piProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β]
  {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [inst_2 : UniformSpace γ] {G : ι → α → γ} {g : α → γ},
  TendstoLocallyUniformlyOn F f p s →
    TendstoLocallyUniformlyOn G g p s →
      TendstoLocallyUniformlyOn (fun n => Function.prod (F n) (G n)) (Function.prod f g) p s
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The sine of an angle in a right-angled triangle as a ratio of sides.  -/
Orientation.sin_oangle_add_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x + y) y).sin = ‖x‖ / ‖x + y‖
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfLax_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) (F' : F.PseudoCore) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.Pseudofunctor.mkOfLax F F').mapComp f g = F'.mapCompIso f g
-- Init.Data.Float.Float32
/-- Computes the arc tangent (inverse tangent) of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`atanf`.
 -/
Float32.atan : Float32 → Float32
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.category_id_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (a : X.I),
  (CategoryTheory.CategoryStruct.id X).f a = a
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.rank_insert : ∀ (x y : ZFSet.{u_1}), (insert x y).rank = max (Order.succ x.rank) y.rank
-- Mathlib.Order.Directed
Directed.mono : ∀ {α : Type u_1} {r s : α → α → Prop} {ι : Sort u_5} {f : ι → α},
  (∀ (a b : α), r a b → s a b) → Directed r f → Directed s f
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.congrRightRingEquiv_symm_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} [inst_1 : Semiring Y] [inst_2 : Semiring Z]
  (e : Y ≃+* Z) (g : LocallyConstant X Z) (a : X), ((LocallyConstant.congrRightRingEquiv e).symm g) a = e.symm (g a)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A diffeomorphism is a partial diffeomorphism.  -/
Diffeomorph.toPartialDiffeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        {I : ModelWithCorners 𝕜 E H₁} →
                          {J : ModelWithCorners 𝕜 F H₂} →
                            {M : Type u_8} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H₂ N] →
                                        {n : WithTop ℕ∞} → Diffeomorph I J M N n → PartialDiffeomorph I J M N n
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Icc_castLE : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n),
  ∏ i ∈ Finset.Icc (Fin.castLE h a) (Fin.castLE h b), f i = ∏ i ∈ Finset.Icc a b, f (Fin.castLE h i)
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Methods.mk.injEq : ∀ (pre post pre_1 post_1 : Lean.Meta.Sym.Simp.Simproc),
  ({ pre := pre, post := post } = { pre := pre_1, post := post_1 }) = (pre = pre_1 ∧ post = post_1)
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- Two nonempty compact spaces have the same image in `GHSpace` if and only if they are
isometric.  -/
GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquiv : ∀ {X : Type u} [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X] {Y : Type v}
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
  GromovHausdorff.toGHSpace X = GromovHausdorff.toGHSpace Y ↔ Nonempty (X ≃ᵢ Y)
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.eval_intCast_map : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (p : Polynomial R) (i : ℤ),
  Polynomial.eval (↑i) (Polynomial.map f p) = f (Polynomial.eval (↑i) p)
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.mk : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [toIsHomLift : p.IsHomLift f φ],
  (∀ {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'],
      ∃! χ, p.IsHomLift (CategoryTheory.CategoryStruct.id R) χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ') →
    p.IsCartesian f φ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
/-- Helper function for `mkSimpleOpThm?` and `mkPowThm?`  -/
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.mkSimpleOpThmCore? : Lean.Expr → Lean.Name → Lean.Name → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Mathlib.Analysis.Convex.Exposed
/-- A point is exposed with respect to `A` iff there exists a hyperplane whose intersection with
`A` is exactly that point.  -/
Set.exposedPoints : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [TopologicalSpace 𝕜] →
      [inst : Ring 𝕜] →
        [PartialOrder 𝕜] → [inst_2 : AddCommMonoid E] → [TopologicalSpace E] → [Module 𝕜 E] → Set E → Set E
-- Mathlib.Topology.Separation.Hausdorff
/-- If a function `f` is

- injective on a compact set `s`;
- continuous at every point of this set;
- injective on a neighborhood of each point of this set,

then it is injective on an open neighborhood of this set.  -/
Set.InjOn.exists_isOpen_superset : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {f : X → Y}
  {s : Set X},
  Set.InjOn f s →
    IsCompact s →
      (∀ x ∈ s, ContinuousAt f x) → (∀ x ∈ s, ∃ u ∈ nhds x, Set.InjOn f u) → ∃ t, IsOpen t ∧ s ⊆ t ∧ Set.InjOn f t
-- Mathlib.Topology.Order.LiminfLimsup
limsSup_nhds : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] (a : α),
  (nhds a).limsSup = a
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.ιOfLE_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P')
  (X : P.FullSubcategory), ((CategoryTheory.ObjectProperty.ιOfLE h).obj X).obj = X.obj
-- Mathlib.Algebra.GroupWithZero.Basic
/-- **Alias** of `pow_eq_zero_iff'`.

---

A variant of `pow_eq_zero_iff` assuming `M₀` is not trivial.  -/
IsReduced.pow_eq_zero_iff' : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀] [Nontrivial M₀], a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_eq_cfc_real : ∀ {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} {y : ℝ},
  autoParam (0 ≤ a) CFC.rpow_eq_cfc_real._auto_1 → a ^ y = cfc (fun x => x ^ y) a
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepNormal_eval : ∀ (c : Turing.ToPartrec.Code) (v : List ℕ),
  StateTransition.eval Turing.ToPartrec.step (Turing.ToPartrec.stepNormal c Turing.ToPartrec.Cont.halt v) =
    Turing.ToPartrec.Cfg.halt <$> c.eval v
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomAddAct.instVAddAEEqFun.eq_1 : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : VAdd M α] [inst_3 : MeasurableConstVAdd M α]
  [inst_4 : MeasureTheory.VAddInvariantMeasure M α μ],
  DomAddAct.instVAddAEEqFun = { vadd := fun c f => f.compMeasurePreserving (fun x => DomAddAct.mk.symm c +ᵥ x) ⋯ }
-- Batteries.Recycling.RBTree.Basic
/-- `path.del t c` does the second part of `RBNode.del`, which unwinds the stack
and rebuilds the tree. The `c` argument is the color of the node before the deletion
(we used `t₀.isBlack` for this in `RBNode.del` but the original tree is no longer
available in this formulation).
 -/
RBTree.RBNode.Path.del : {α : Type u_1} → RBTree.RBNode.Path α → RBTree.RBNode α → RBTree.RBColor → RBTree.RBNode α
-- Std.Http.Data.URI.Config
/-- Maximum length of a single path segment, in bytes.
 -/
Std.Http.URI.Config.maxSegmentLength : Std.Http.URI.Config → ℕ
-- Init.Data.String.PosRaw
String.Pos.Raw.lt_inc : ∀ {p : String.Pos.Raw}, p < p.inc
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddCommGroup.ofAddDist'.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : AddCommGroup E] [inst_2 : MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 0 x)
  (h₂ : ∀ (x y z : E), dist (z + x) (z + y) ≤ dist x y),
  NormedAddCommGroup.ofAddDist' h₁ h₂ =
    { toNorm := (NormedAddGroup.ofAddDist' h₁ h₂).toNorm, toAddGroup := (NormedAddGroup.ofAddDist' h₁ h₂).toAddGroup,
      add_comm := ⋯, toMetricSpace := (NormedAddGroup.ofAddDist' h₁ h₂).toMetricSpace, dist_eq := ⋯ }
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.rescale_one : ∀ {R : Type u_1} [inst : CommSemiring R], PowerSeries.rescale 1 = RingHom.id (PowerSeries R)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.op_unop_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Cofork f g), c.op.unop.π = c.π
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- A `FredholmDecomposition` of the codomain.  -/
ContinuousLinearMap.FredholmPackage.decCodom : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : Module 𝕜 F] →
                [inst_5 : TopologicalSpace E] →
                  [inst_6 : TopologicalSpace F] → {u : E →L[𝕜] F} → u.FredholmPackage → FredholmDecomposition 𝕜 F
-- Init.Data.Nat.Bitwise.Basic
/-- Bitwise exclusive or. Usually accessed via the `^^^` operator.

Each bit of the resulting value is set if the corresponding bit is set in exactly one of the inputs.
 -/
Nat.xor : ℕ → ℕ → ℕ
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_span_singleton_eq_map_flip : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) (s : Submodule R M) (n : N),
  Submodule.map₂ f s (R ∙ n) = Submodule.map (f.flip n) s
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mk : {α : Type u} →
  [inst : MeasurableSpace α] →
    {β : Type v} →
      (toFun : α → β) →
        (∀ (x : β), MeasurableSet (toFun ⁻¹' {x})) → (Set.range toFun).Finite → MeasureTheory.SimpleFunc α β
-- Mathlib.Topology.UnitInterval
unitInterval.coe_ne_zero : ∀ {x : ↑unitInterval}, ↑x ≠ 0 ↔ x ≠ 0
-- Mathlib.Tactic.Linter.Style
/-- The "longFile" linter emits a warning on files which are longer than a certain number of lines
(`linter.style.longFileDefValue` by default on mathlib, no limit for downstream projects).
If this option is set to `N` lines, the linter warns once a file has more than `N` lines.
A value of `0` silences the linter entirely.
 -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.Style.longFile.longFileLinter : Lean.Linter
-- Mathlib.Data.Nat.Size
Nat.size_le : ∀ {m n : ℕ}, m.size ≤ n ↔ m < 2 ^ n
-- Init.Data.Array.Attach
Array.pmap_map : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {p : β → Prop} {g : (b : β) → p b → γ} {f : α → β} {xs : Array α}
  (H : ∀ a ∈ Array.map f xs, p a), Array.pmap g (Array.map f xs) H = Array.pmap (fun a h => g (f a) h) xs ⋯
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange.addMonoidHom_id : ∀ {ι : Type u} {β₂ : ι → Type v₂} [inst : (i : ι) → AddZeroClass (β₂ i)],
  (DFinsupp.mapRange.addMonoidHom fun i => AddMonoidHom.id (β₂ i)) = AddMonoidHom.id (Π₀ (i : ι), β₂ i)
-- Mathlib.Computability.DFA
DFA.mem_acceptsFrom : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) {s : σ} {x : List α}, x ∈ M.acceptsFrom s ↔ M.evalFrom s x ∈ M.accept
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a normed group from a norm, i.e., registering the distance and the metric
space structure from the norm properties. Note that in most cases this instance creates bad
definitional equalities (e.g., it does not take into account a possibly existing `UniformSpace`
instance on `E`).  -/
AddGroupNorm.toNormedAddGroup : {E : Type u_5} → [inst : AddGroup E] → AddGroupNorm E → NormedAddGroup E
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Integrable.integral_condKernel : ∀ {α : Type u_1} {Ω : Type u_2} {E : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace Ω]
  [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E]
  {ρ : MeasureTheory.Measure (α × Ω)} [inst_5 : MeasureTheory.IsFiniteMeasure ρ] {f : α × Ω → E},
  MeasureTheory.Integrable f ρ → MeasureTheory.Integrable (fun x => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
hasSum_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β},
  ¬L.NeBot → ∀ (f : β → α) (a : α), HasSum f a L
-- Mathlib.CategoryTheory.Quotient.Preadditive
/-- The addition on the morphisms in the category `Quotient r` when `r` is compatible
with the addition.  -/
CategoryTheory.Quotient.Preadditive.add : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (r : HomRel C) →
        [CategoryTheory.Congruence r] →
          (∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)) →
            {X Y : CategoryTheory.Quotient r} → (X ⟶ Y) → (X ⟶ Y) → (X ⟶ Y)
-- Aesop.Stats.Basic
Aesop.ForwardInstantiationStats.mk.sizeOf_spec : ∀ («matches» hyps : ℕ), sizeOf { «matches» := «matches», hyps := hyps } = 1 + sizeOf «matches» + sizeOf hyps
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.mk : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            (toPartialEquiv : PartialEquiv Z (B × F)) →
              IsOpen toPartialEquiv.target →
                (baseSet : Set B) →
                  IsOpen baseSet →
                    toPartialEquiv.source = proj ⁻¹' baseSet →
                      toPartialEquiv.target = baseSet ×ˢ Set.univ →
                        (∀ p ∈ toPartialEquiv.source, (↑toPartialEquiv p).1 = proj p) → Bundle.Pretrivialization F proj
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
writtenInExtChartAt_sumInl_eventuallyEq_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {q : M},
  writtenInExtChartAt I I q Sum.inl =ᶠ[nhdsWithin (↑(extChartAt I q) q) (Set.range ↑I)] id
-- Mathlib.Algebra.Order.Ring.Basic
sq_pos_iff : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {a : R},
  0 < a ^ 2 ↔ a ≠ 0
-- Mathlib.Order.Nucleus
Nucleus.instMin : {X : Type u_1} → [inst : SemilatticeInf X] → Min (Nucleus X)
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.Hom.ext_iff : ∀ {X : UniformSpaceCat} {Y : UniformSpaceCat} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Data.ENat.Basic
ENat.lift.congr_simp : ∀ (x x_1 : ℕ∞) (e_x : x = x_1) (h : x < ⊤), x.lift h = x_1.lift ⋯
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.inv₀_mem_inv_iff : ∀ {R : Type u} {A : Type v} [inst : Semifield R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : Aˣ},
  r⁻¹ ∈ spectrum R ↑a⁻¹ ↔ r ∈ spectrum R ↑a
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.ExchangeProperty.encard_sdiff_le_aux : ∀ {α : Type u_1} {IsBase : Set α → Prop} {B₁ B₂ : Set α},
  Matroid.ExchangeProperty IsBase → IsBase B₁ → IsBase B₂ → (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
-- Mathlib.RingTheory.Congruence.Defs
RingCon.hasNSMul : {R : Type u_1} → [inst : AddMonoid R] → [inst_1 : Mul R] → (c : RingCon R) → SMul ℕ c.Quotient
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If `C` has all limits of diagrams `parallelPair f g`, then it has all equalizers  -/
CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [∀ {X Y : C} {f g : X ⟶ Y}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)],
  CategoryTheory.Limits.HasEqualizers C
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
/-- The canonical map from the tensor algebra to a direct sum of tensor powers.  -/
TensorAlgebra.toDirectSum : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → TensorAlgebra R M →ₐ[R] DirectSum ℕ fun n => TensorPower R n M
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Colex.addRightStrictMono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddMonoid (α i)]
  [inst_2 : (i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)],
  AddRightStrictMono (Colex (Π₀ (i : ι), α i))