mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Given a pair of additive homomorphisms `f`, `g` such that `g.comp f = id` and
`f.comp g = id`, returns an additive equivalence with `toFun = f` and `invFun = g`. This
constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive
homomorphisms.  -/
AddHom.toAddEquiv : {M : Type u_4} →
  {N : Type u_5} →
    [inst : Add M] →
      [inst_1 : Add N] → (f : M →ₙ+ N) → (g : N →ₙ+ M) → g.comp f = AddHom.id M → f.comp g = AddHom.id N → M ≃+ N
-- Mathlib.RingTheory.Derivation.MapCoeffs
Derivation.apply_eval_eq : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (d : Derivation R A M) (x : A)
  (p : Polynomial A),
  d (Polynomial.eval x p) =
    (PolynomialModule.eval x) (d.mapCoeffs p) + Polynomial.eval x (Polynomial.derivative p) • d x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.monObj_mul : ∀ {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]
  {F : CategoryTheory.Functor C D} [inst_4 : F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.MonObj (F.obj X)],
  CategoryTheory.MonObj.mul =
    hF.preimage
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X) CategoryTheory.MonObj.mul)
-- Mathlib.Data.Fintype.EquivFin
/-- There is (computably) a bijection between `Fin (card α)` and `α`.

Since it is not unique and depends on which permutation
of the universe list is used, the bijection is wrapped in `Trunc` to
preserve computability.

See `Fintype.truncEquivFin` for a version that gives an equivalence
given `[DecidableEq α]`.
 -/
Fintype.truncFinBijection : (α : Type u_4) → [inst : Fintype α] → Trunc { f // Function.Bijective f }
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.apply_posSubmonoid_ne_zero : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_2} [inst_2 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible] (x : ↥(ValuativeRel.posSubmonoid R)), v ↑x ≠ 0
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.map_Y : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S T : J.Cover X} (I : S.Arrow) (f : S ⟶ T), (I.map f).Y = I.Y
-- Mathlib.Algebra.Group.Action.Pi
Pi.vaddAssocClass'' : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} [inst : (i : ι) → VAdd (α i) (β i)]
  [inst_1 : (i : ι) → VAdd (β i) (γ i)] [inst_2 : (i : ι) → VAdd (α i) (γ i)]
  [∀ (i : ι), VAddAssocClass (α i) (β i) (γ i)], VAddAssocClass ((i : ι) → α i) ((i : ι) → β i) ((i : ι) → γ i)
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_roi_eq_toList_mkSlice_rco : ∀ {α : Type u_1} {xs : List α} {lo : ℕ},
  Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) =
    Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs (lo + 1)...xs.length)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_erase_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {k : α}, (m.erase k).getKey! k = default
-- Mathlib.Data.Nat.Find
Nat.find_pos : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (h : ∃ n, p n), 0 < Nat.find h ↔ ¬p 0
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `NonUnitalNonAssocSemiring` instance along an injective function.  -/
Function.Injective.nonUnitalNonAssocSemiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : S → R) →
      Function.Injective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : SMul ℕ S] →
                [inst_4 : NonUnitalNonAssocSemiring R] →
                  f 0 = 0 →
                    (∀ (x y : S), f (x + y) = f x + f y) →
                      (∀ (x y : S), f (x * y) = f x * f y) →
                        (∀ (n : ℕ) (x : S), f (n • x) = n • f x) → NonUnitalNonAssocSemiring S
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a b : α}, cmp a b = Ordering.eq → Std.DTreeMap.Raw.Const.get? t a = Std.DTreeMap.Raw.Const.get? t b
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_fun_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {γ : Path a b},
  ∫ᶜ (x : E) in γ, 0 = 0
-- Lean.Data.Position
Lean.Position.lt : Lean.Position → Lean.Position → Bool
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.toHomeomorph_apply : ∀ {𝕜 : 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)
  [inst_4 : I.Boundaryless] (a : H), I.toHomeomorph a = ↑I a
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.add_iff_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₂ =O[l] g → ((fun x => f₁ x + f₂ x) =O[l] g ↔ f₁ =O[l] g)
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndInfo.funIndName : Lean.Meta.FunIndInfo → Lean.Name
-- Mathlib.Topology.Maps.Strict.Basic
/-- Strict maps are preserved when precomposing with a homeomorphism.  -/
Homeomorph.isStrictMap_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : X ≃ₜ Y) {f : Y → Z}, Topology.IsStrictMap (f ∘ ⇑e) ↔ Topology.IsStrictMap f
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- Finite sums of interval integrable functions are interval integrable.  -/
IntervalIntegrable.finsum : ∀ {ι : Type u_1} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {ε : Type u_8} [inst : TopologicalSpace ε]
  [inst_1 : ENormedAddCommMonoid ε] [ContinuousAdd ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : ι → ℝ → ε},
  (∀ (i : ι), IntervalIntegrable (f i) μ a b) → IntervalIntegrable (∑ᶠ (i : ι), f i) μ a b
-- Mathlib.Topology.Constructions.SumProd
IsOpenMap.sumElim : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z}, IsOpenMap f → IsOpenMap g → IsOpenMap (Sum.elim f g)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Flattening nested binary convex combination into a single convex combination.  -/
Convexity.convexCombPair_convexCombPair_right_eq_sConvexComb : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s')
  (ht' : 0 ≤ t') (h' : s' + t' = 1) (m₁ m₂ m₃ : M),
  Convexity.convexCombPair s t hs ht h m₁ (Convexity.convexCombPair s' t' hs' ht' h' m₂ m₃) =
    Convexity.sConvexComb
      (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.single m₁)
        (Convexity.StdSimplex.duple m₂ m₃ hs' ht' h'))
-- Mathlib.Algebra.Polynomial.Degree.Monomial
Polynomial.C_mul_X_pow_eq_self : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.support.card ≤ 1 → Polynomial.C p.leadingCoeff * Polynomial.X ^ p.natDegree = p
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.eLpNorm'_add_le : ∀ {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε]
  {q : ℝ} {μ : MeasureTheory.Measure α} {f g : α → ε},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      1 ≤ q → MeasureTheory.eLpNorm' (f + g) q μ ≤ MeasureTheory.eLpNorm' f q μ + MeasureTheory.eLpNorm' g q μ
-- Init.System.IO
/-- Writes the provided bytes to the handle.

Writing to a handle is typically buffered, and may not immediately modify the file on disk. Use
`IO.FS.Handle.flush` to write changes to buffers to the associated device.
 -/
IO.FS.Handle.write : IO.FS.Handle → ByteArray → IO Unit
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.arrowCongrRight_apply : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ↪ β) (f : γ → α), e.arrowCongrRight f = ⇑e ∘ f
-- Mathlib.NumberTheory.Padics.PadicVal.Defs
padicValNat.one : ∀ {p : ℕ}, padicValNat p 1 = 0
-- Init.GrindInstances.Ring.UInt
UInt64.intCast : IntCast UInt64
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_of_contains_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β}, (t.insert k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Mathlib.Order.Disjoint
Disjoint.inf_right : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α} (c : α), Disjoint a b → Disjoint a (b ⊓ c)
-- Mathlib.MeasureTheory.MeasurableSpace.Invariants
MeasurableSpace.le_invariants_iterate : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → α) (n : ℕ),
  MeasurableSpace.invariants f ≤ MeasurableSpace.invariants f^[n]
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstModNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.ShortComplex.Exact.fIsKernel.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Balanced C] (hS : S.Exact)
  [inst_3 : CategoryTheory.Mono S.f], hS.fIsKernel = hS.fIsKernel
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_mul_of_apply_of_le : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddCommMonoid ι] [inst_5 : PartialOrder ι]
  [CanonicallyOrderedAdd ι] [inst_7 : SetLike.GradedMonoid A] [inst_8 : Sub ι] [OrderedSub ι] [AddLeftReflectLE ι]
  (r : DirectSum ι fun i => ↥(A i)) {i : ι} (r' : ↥(A i)) (n : ι),
  i ≤ n → ↑((r * (DirectSum.of (fun i => ↥(A i)) i) r') n) = ↑(r (n - i)) * ↑r'
-- Mathlib.Computability.AkraBazzi.AkraBazzi
AkraBazziRecurrence.rpow_p_mul_one_add_smoothingFn_ge : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r),
  ∀ᶠ (n : ℕ) in Filter.atTop,
    ∀ (i : α),
      b i ^ AkraBazziRecurrence.p a b * ↑n ^ AkraBazziRecurrence.p a b * (1 + AkraBazziRecurrence.smoothingFn ↑n) ≤
        ↑(r i n) ^ AkraBazziRecurrence.p a b * (1 + AkraBazziRecurrence.smoothingFn ↑(r i n))
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.coe_ringHom_injective : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ}, Function.Injective fun f => ↑f
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_eq_of_eq_mul_right : ∀ {a b c : ℤ}, b ≠ 0 → a = b * c → a.fdiv b = c
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject.Split C) (n : ℕ),
  (CategoryTheory.SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁.hom.app X).f.f n =
    CategoryTheory.CategoryStruct.comp
      ((X.s.cofan (Opposite.op { len := n })).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n })))
      (AlgebraicTopology.DoldKan.PInfty.f n)
-- Batteries.Data.List.Lemmas
List.dropPrefix?.eq_2 : ∀ {α : Type u_1} [inst : BEq α] (head : α) (tail : List α), [].dropPrefix? (head :: tail) = none
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.FunInfoEnvCacheKey.mk.inj : ∀ {c : Lean.Name} {ls : List Lean.Level} {maxArgs? : Option ℕ} {c_1 : Lean.Name} {ls_1 : List Lean.Level}
  {maxArgs?_1 : Option ℕ},
  { c := c, ls := ls, maxArgs? := maxArgs? } = { c := c_1, ls := ls_1, maxArgs? := maxArgs?_1 } →
    c = c_1 ∧ ls = ls_1 ∧ maxArgs? = maxArgs?_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : β → β} {hc : k' ∈ t.modify k f}, (t.modify k f)[k'] = if heq : cmp k k' = Ordering.eq then f t[k] else t[k']
-- Mathlib.GroupTheory.Perm.Subgroup
Equiv.Perm.subtypeCongrHom.decidableMemRange : {α : Type u_1} →
  (p : α → Prop) →
    [inst : DecidablePred p] →
      [Fintype (Equiv.Perm { a // p a } × Equiv.Perm { a // ¬p a })] →
        [DecidableEq (Equiv.Perm α)] → DecidablePred fun x => x ∈ (Equiv.Perm.subtypeCongrHom p).range
-- Mathlib.Order.Monotone.Defs
monotone_lam : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder γ] {f : α → β → γ},
  (∀ (b : β), Monotone fun a => f a b) → Monotone f
-- Mathlib.Logic.Equiv.Prod
Equiv.boolArrowEquivProd_symm_apply : ∀ (α : Type u_9) (p : α × α) (b : Bool), (Equiv.boolArrowEquivProd α).symm p b = if b = true then p.2 else p.1
-- Init.GrindInstances.Ring.Int
Lean.Grind.instNoNatZeroDivisorsInt : Lean.Grind.NoNatZeroDivisors ℤ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- The short complex `H₁(S, A) ⟶ H₁(G, A) ⟶ H₁(G ⧸ S, A_S)`. The first map is the
"corestriction" map induced by the inclusion `ι : S →* G` and the identity on `Res(ι)(A)`, and the
second map is the "coinflation" map induced by the quotient maps `G →* G ⧸ S` and `A →ₗ A_S`.  -/
groupHomology.H1CoresCoinf : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → Rep.{u, u, u} k G → (S : Subgroup G) → [S.Normal] → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.Data.List.Lattice
/-- **Alias** of the reverse direction of `List.inter_eq_nil_iff_disjoint`. -/
List.Disjoint.inter_eq_nil : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : DecidableEq α], l₁.Disjoint l₂ → l₁ ∩ l₂ = []
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_pos_iff_notMem_closure`.

---

The infimum edistance of a point to a set is positive if and only if the point is not in the
closure of the set.  -/
EMetric.infEdist_pos_iff_notMem_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {E : Set α}, 0 < Metric.infEDist x E ↔ x ∉ closure E
-- Mathlib.Tactic.Order.Graph.Tarjan
/-- `onStack.contains v` iff `v` is in `stack`. The structure is used to check it efficiently.  -/
Mathlib.Tactic.Order.Graph.TarjanState.onStack : Mathlib.Tactic.Order.Graph.TarjanState → Std.HashSet ℕ
-- Init.Meta.Defs
/-- Syntax that represents a priority (e.g. for an instance declaration).
 -/
Lean.Syntax.Prio : Type
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.augment_hom_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) (X₀ : C)
  (f : X₀ ⟶ X.obj { len := 0 })
  (w :
    ∀ (i : SimplexCategory) (g₁ g₂ : { len := 0 } ⟶ i),
      CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.map g₂)),
  (X.augment X₀ f w).hom.app { len := 0 } = f
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.martingalePart_add_predictablePart : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (ℱ : MeasureTheory.Filtration ℕ m0) (μ : MeasureTheory.Measure Ω) (f : ℕ → Ω → E),
  MeasureTheory.martingalePart f ℱ μ + MeasureTheory.predictablePart f ℱ μ = f
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.den_intCast : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : DecidableEq m] (a : ℤ), (↑a).den = 1
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F) (x : E),
  ‖A x‖ = √(RCLike.re (inner 𝕜 ((ContinuousLinearMap.adjoint A ∘SL A) x) x))
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.EStateM.run_bind.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (x : α) (s : σ)
  (h_1 : (x : α) → (s : σ) → motive (EStateM.Result.ok x s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.ok x s with
    | EStateM.Result.ok x s => h_1 x s
    | EStateM.Result.error e s => h_2 e s) =
    h_1 x s
-- Mathlib.Analysis.Calculus.FDeriv.Linear
IsBoundedLinearMap.hasFDerivAtFilter : ∀ {𝕜 : 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] {f : E → F}
  {L : Filter (E × E)} (h : IsBoundedLinearMap 𝕜 f),
  HasFDerivAtFilter f (IsBoundedLinearMap.toContinuousLinearMap f h) L
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.mul_inv : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]}, ‖z‖ = 1 → z * z.inv = 1
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_countable' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable α] [MeasurableSingletonClass α]
  (f : α → ENNReal), ∫⁻ (a : α), f a ∂μ = ∑' (a : α), f a * μ {a}
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- **Alias** of `Ordinal.CNF.snd_pos`.

---

Every coefficient in a Cantor normal form is positive.  -/
Ordinal.CNF.lt_snd : ∀ {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}}, x ∈ Ordinal.CNF b o → 0 < x.2
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.associated_content_C_mul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (r : R) (p : Polynomial R),
  Associated (Polynomial.C r * p).content (r * p.content)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_natCast_lt_mul_natCast : ∀ {n : ℕ} {a b : Cardinal.{u_1}}, n ≠ 0 → (a * ↑n < b * ↑n ↔ a < b)
-- Mathlib.RingTheory.DualNumber
TrivSqZeroExt.isNilpotent_iff_isNilpotent_fst : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] {x : TrivSqZeroExt R M}, IsNilpotent x ↔ IsNilpotent x.fst
-- Mathlib.Algebra.Notation.Support
/-- `mulSupport` of a function is the set of points `x` such that `f x ≠ 1`.  -/
Function.mulSupport : {ι : Type u_1} → {M : Type u_3} → [One M] → (ι → M) → Set ι
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The direction of the affine span of coplanar points is finite-dimensional.  -/
Coplanar.finiteDimensional_direction_affineSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P}, Coplanar k s → FiniteDimensional k ↥(affineSpan k s).direction
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.MapTarget.lawful : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ}
  (self : Std.Sat.AIG.RefVec.MapTarget aig len), Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref self.func
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroBitVecUint : ∀ {v : ℕ}, Lean.Grind.ToInt.Zero (BitVec v) (Lean.Grind.IntInterval.uint v)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_of_one_le : ∀ {x : ℝ}, 1 ≤ x → Real.arcsin x = Real.pi / 2
-- Mathlib.Geometry.Manifold.Notation
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.guessBaseFieldForNormedSpace.findFromLocalInstance : Lean.Expr → Lean.Elab.TermElabM (Option Lean.Expr)
-- Mathlib.Topology.Order.IsLUB
IsLUB.nhdsWithin_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  IsLUB s a → s.Nonempty → (nhdsWithin a s).NeBot
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_right_injective : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} (x : α p), Function.Injective (p.insertNth x)
-- Mathlib.Computability.PartrecCode
/-- **Kleene's second recursion theorem**  -/
Nat.Partrec.Code.fixed_point₂ : ∀ {f : Nat.Partrec.Code → ℕ →. ℕ}, Partrec₂ f → ∃ c, c.eval = f c
-- Mathlib.Order.LiminfLimsup
/-- **Alias** of `Filter.liminfReparam`.

---

Given an indexed family of sets `s j` over `j : Subtype p` and a function `f`, then
`liminfReparam j` is equal to `j` if `f` is bounded below on `s j`, and otherwise to some
index `k` such that `f` is bounded below on `s k` (if there exists one).
To ensure good measurability behavior, this index `k` is chosen as the minimal suitable index.
This function is used to write down a liminf in a measurable way,
in `Filter.HasBasis.liminf_eq_ciSup_ciInf` and `Filter.HasBasis.liminf_eq_ite`.  -/
Filter.liminf_reparam : {α : Type u_1} →
  {ι : Type u_4} →
    {ι' : Type u_5} →
      [ConditionallyCompleteLinearOrder α] →
        (ι → α) →
          (ι' → Set ι) → (p : ι' → Prop) → [Countable (Subtype p)] → [Nonempty (Subtype p)] → Subtype p → Subtype p
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr : Type
-- Mathlib.Data.Rat.Defs
Rat.zero_iff_num_zero : ∀ {q : ℚ}, q = 0 ↔ q.num = 0
-- Mathlib.FieldTheory.Separable
IsSeparable.map : ∀ {F : Type u_1} {L : Type u_2} {K : Type u_3} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K]
  [inst_3 : Ring L] [inst_4 : Algebra F L] {x : K} (f : K →ₐ[F] L),
  Function.Injective ⇑f → IsSeparable F x → IsSeparable F (f x)
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.isOpen_preimage_ofLower : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsOpen (⇑Topology.WithLower.ofLower ⁻¹' s) ↔ IsOpen s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_inter_le_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ ∩ t₂).size ≤ t₁.size
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.leftAdjointObjIsDefined_of_isColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor D C} {J : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} J]
  {R : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone R} (hc : CategoryTheory.Limits.IsColimit c)
  [CategoryTheory.Limits.HasColimitsOfShape J D],
  (∀ (j : J), F.leftAdjointObjIsDefined (R.obj j)) → F.leftAdjointObjIsDefined c.pt
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.singleDistribMulActionHom.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] [inst_1 : Monoid R] [inst_2 : DistribMulAction R S]
  (a : M),
  MonoidAlgebra.singleDistribMulActionHom a =
    { toFun := (↑(MonoidAlgebra.singleAddHom a)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- The 'unopposite' of an additive semigroup hom `αᵐᵒᵖ →+ βᵐᵒᵖ`. Inverse to
`AddHom.mul_op`.  -/
AddHom.mulUnop : {α : Type u_3} → {β : Type u_4} → [inst : Add α] → [inst_1 : Add β] → (αᵐᵒᵖ →ₙ+ βᵐᵒᵖ) ≃ (α →ₙ+ β)
-- Mathlib.NumberTheory.PrimeCounting
Nat.one_lt_of_mem_primesLE : ∀ {p n : ℕ}, p ∈ n.primesLE → 1 < p
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- Given `A : IndexSet Δ₁`, if `p.unop : unop Δ₂ ⟶ unop Δ₁` is an epi, this
is the obvious element in `A : IndexSet Δ₂` associated to the composition
of epimorphisms `p.unop ≫ A.e`.  -/
CategoryTheory.SimplicialObject.Splitting.IndexSet.epiComp : {Δ₁ Δ₂ : SimplexCategoryᵒᵖ} →
  CategoryTheory.SimplicialObject.Splitting.IndexSet Δ₁ →
    (p : Δ₁ ⟶ Δ₂) → [CategoryTheory.Epi p.unop] → CategoryTheory.SimplicialObject.Splitting.IndexSet Δ₂
-- Lean.Util.PPExt
Lean.PPFns.ppExprWithInfos : Lean.PPFns → Lean.PPContext → Lean.Expr → IO Lean.FormatWithInfos
-- Mathlib.Data.Nat.Factorization.Basic
Nat.factorization_eq_zero_iff_remainder : ∀ {p r : ℕ} (i : ℕ), Nat.Prime p → r ≠ 0 → (¬p ∣ r ↔ (p * i + r).factorization p = 0)