mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesLimit_iff_of_iso_diagram : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K₁ K₂ : CategoryTheory.Functor J C}
  (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂),
  CategoryTheory.Limits.PreservesLimit K₁ F ↔ CategoryTheory.Limits.PreservesLimit K₂ F
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X] (f : ↑(X.presheaf.obj (Opposite.op ⊤))),
  (TopologicalSpace.Opens.map X.isoSpec.hom.base).obj (PrimeSpectrum.basicOpen f) = X.basicOpen f
-- Mathlib.Topology.Order.LiminfLimsup
/-- If a filter is converging, its liminf coincides with its limit.  -/
limsSup_eq_of_le_nhds : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {f : Filter α} {a : α} [f.NeBot], f ≤ nhds a → f.limsSup = a
-- Init.Prelude
/-- Translates an action from monad `m` into monad `n`.  -/
liftM : {m : Type u_1 → Type u_2} → {n : Type u_1 → Type u_3} → [self : MonadLiftT m n] → {α : Type u_1} → m α → n α
-- Mathlib.Algebra.Group.Defs
npowRec'_two_mul : ∀ {M : Type u_2} [inst : Semigroup M] [inst_1 : One M] (k : ℕ) (m : M), npowRec' (2 * k) m = npowRec' k (m * m)
-- Mathlib.MeasureTheory.Measure.Restrict
/-- **Alias** of the reverse direction of `MeasureTheory.Measure.ext_iff_of_iUnion_eq_univ`.

---

Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using `Union`).  -/
MeasureTheory.Measure.ext_of_iUnion_eq_univ : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  ⋃ i, s i = Set.univ → (∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)) → μ = ν
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.Suggestion.pretty : Lean.Meta.Tactic.TryThis.Suggestion → optParam (Option ℕ) none → optParam ℕ 0 → optParam ℕ 0 → Lean.CoreM String
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_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) (A : Type u) [inst_2 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K]
  (X : CategoryTheory.Sheaf K A) (X_1 : Cᵒᵖ),
  ((F.sheafPushforwardContinuousCompSheafToPresheafIso A J K).inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj.obj (Opposite.op (F.obj (Opposite.unop X_1))))
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that `f(S) ⊆ AddUnits N`, for all
`w, z : N` and `y ∈ S`, we have `z = w - f y ↔ z + f y = w`.  -/
AddSubmonoid.LocalizationMap.add_neg_right : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {f : M →+ N}
  (h : ∀ (y : ↥S), IsAddUnit (f ↑y)) (y : ↥S) (w z : N),
  z = w + ↑(-(IsAddUnit.liftRight (f.domRestrict S) h) y) ↔ z + f ↑y = w
-- Init.Meta.Defs
Lean.Syntax.toNat : Lean.Syntax → ℕ
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.instIsComonHomId : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.ComonObj M], CategoryTheory.IsComonHom (CategoryTheory.CategoryStruct.id M)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [Inhabited α] {k fallback : α} {f : β k → β k},
  (t.modify k f).getKeyD k fallback = if k ∈ t then k else fallback
-- Mathlib.RingTheory.Localization.Module
IsLocalizedModule.map_bijective_iff_localizedModuleMap_bijective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_4} {N' : Type u_5} [inst : CommSemiring R] {S : Submonoid R}
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid M'] [inst_6 : Module R M'] [inst_7 : AddCommMonoid N'] [inst_8 : Module R N']
  (g₁ : M →ₗ[R] M') (g₂ : N →ₗ[R] N') [inst_9 : IsLocalizedModule S g₁] [inst_10 : IsLocalizedModule S g₂]
  {l : M →ₗ[R] N},
  Function.Bijective ⇑((IsLocalizedModule.map S g₁ g₂) l) ↔ Function.Bijective ⇑((LocalizedModule.map S) l)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.isNormal_veblenWith_zero : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → 0 < f 0 → Order.IsNormal fun x => Ordinal.veblenWith f x 0
-- Mathlib.Topology.MetricSpace.Similarity
Similar.comp_left : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {F : Type u_6}
  [inst_3 : FunLike F P₁ P₃] [DilationClass F P₁ P₃] (f : F), Similar v₁ v₂ → Similar (⇑f ∘ v₁) v₂
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_eq_of_tendsto₀ : ∀ (f : CircleDeg1Lift) {τ' : ℝ},
  Filter.Tendsto (fun n => (⇑f)^[n] 0 / ↑n) Filter.atTop (nhds τ') → f.translationNumber = τ'
-- Mathlib.Topology.Bornology.Basic
Bornology.IsBounded.all : ∀ {α : Type u_2} [inst : Bornology α] [BoundedSpace α] (s : Set α), Bornology.IsBounded s
-- Mathlib.RingTheory.Morita.Matrix
MatrixModCat.unitIso.eq_1 : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι),
  MatrixModCat.unitIso R i =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        ((fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑X) i).trans
            (fromModuleCatToModuleCatLinearEquiv R (↑X) i)).toModuleIso)
      ⋯
-- Mathlib.Computability.Primrec.Basic
Primrec.dom_finite : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] [Finite α] (f : α → σ), Primrec f
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.ker_eq_bot_of_mono : ∀ {A B : GrpCat} (f : A ⟶ B) [CategoryTheory.Mono f], (GrpCat.Hom.hom f).ker = ⊥
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.normConfig_zeta : Lean.Meta.Grind.normConfig✝.zeta = true
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
toMul_sum : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (f : ι → Additive M),
  Additive.toMul (∑ i ∈ s, f i) = ∏ i ∈ s, Additive.toMul (f i)
-- Mathlib.Data.NNReal.Defs
/-- `Real.toNNReal` and `NNReal.toReal : ℝ≥0 → ℝ` form a Galois insertion.  -/
NNReal.gi : GaloisInsertion Real.toNNReal NNReal.toReal
-- Std.Http.Data.URI.Basic
/-- Creates an empty URI builder.
 -/
Std.Http.URI.Builder.empty : Std.Http.URI.Builder
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.one_apply : ∀ {ι : Type u_1} {M : ι → Type u_5} [inst : (i : ι) → One (M i)] (i : ι), 1 i = 1
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.comap_bot' : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F), AddSubmonoid.comap f ⊥ = AddMonoidHom.mker f
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the forward direction of `hasMFDerivWithinAt_iff_hasFDerivWithinAt`. -/
HasMFDerivWithinAt.hasFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {s : Set E} {x : E}
  {f' : TangentSpace (modelWithCornersSelf 𝕜 E) x →L[𝕜] TangentSpace (modelWithCornersSelf 𝕜 E') (f x)},
  HasMFDerivAt[s] f x f' → HasFDerivWithinAt f f' s x
-- Mathlib.Topology.Constructions.SumProd
Continuous.prodMap : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : Z → X} {g : W → Y},
  Continuous f → Continuous g → Continuous (Prod.map f g)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.addActionHom_singleton_bijective : ∀ (G : Type u_1) [inst : AddGroup G] (α : Type u_2) [inst_1 : AddAction G α] [inst_2 : DecidableEq α],
  Function.Bijective ⇑(Set.powersetCard.addActionHom_singleton G α)
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularFormClass.analyticAt_cuspFunction_zero : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F)
  [ModularFormClass F Γ k], 0 < h → h ∈ Γ.strictPeriods → AnalyticAt ℂ (UpperHalfPlane.cuspFunction h ⇑f) 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_filter_key : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α] {f : α → Bool} {k : α},
  m.WF → (Std.DHashMap.Raw.filter (fun k x => f k) m).getKey! k = (Option.filter f (m.getKey? k)).get!
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.beq_congr : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α]
  [inst_1 : (k : α) → BEq (β k)] {m₃ m₄ : Std.DHashMap α β}, m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ == m₂) = (m₃ == m₄)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonClientCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.ClientCapabilities
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceToInt : Lean.Meta.Simp.DSimproc
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.eq_7 : ∀ (motive : Lean.Expr → Sort u_1) (f a : Lean.Expr) (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a))
  (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (f a : Lean.Expr) → motive (f.app a))
  (h_8 : (data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a))
  (h_9 : (typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a))
  (h_10 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo))
  (h_11 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo))
  (h_12 :
    (declName : Lean.Name) → (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)),
  (match f.app a with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | f.app a => h_7 f a
    | Lean.Expr.mdata data a => h_8 data a
    | Lean.Expr.proj typeName idx a => h_9 typeName idx a
    | Lean.Expr.forallE binderName d b binderInfo => h_10 binderName d b binderInfo
    | Lean.Expr.lam binderName d b binderInfo => h_11 binderName d b binderInfo
    | Lean.Expr.letE declName t v b nondep => h_12 declName t v b nondep) =
    h_7 f a
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with scalar multiplication.  -/
InnerProductSpace.laplacianWithin_smul_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra ℝ 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : InnerProductSpace ℝ E] [inst_4 : FiniteDimensional ℝ E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] [IsScalarTower ℝ 𝕜 F]
  {f : E → F} {x : E} {s : Set E} (v : 𝕜),
  ContDiffWithinAt ℝ 2 f s x →
    UniqueDiffOn ℝ s →
      InnerProductSpace.laplacianWithin (v • f) s =ᶠ[nhdsWithin x s] v • InnerProductSpace.laplacianWithin f s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insert.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α)
  (b : β a), t.insert a b = Std.ExtDTreeMap.lift (fun m => Std.ExtDTreeMap.mk (m.insert a b)) ⋯ t
-- Mathlib.CategoryTheory.Subfunctor.Basic
/-- The subfunctor as a functor.  -/
CategoryTheory.Subfunctor.toFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type w)} → CategoryTheory.Subfunctor F → CategoryTheory.Functor C (Type w)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_minKey?_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → (Std.Internal.List.minKey? (Std.Internal.List.insertEntry k v l)).isSome = true
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.mem_compPartialSumTarget_iff : ∀ {m M N : ℕ} {a : (n : ℕ) × Composition n},
  a ∈ FormalMultilinearSeries.compPartialSumTarget m M N ↔
    m ≤ a.snd.length ∧ a.snd.length < M ∧ ∀ (j : Fin a.snd.length), a.snd.blocksFun j < N
-- Mathlib.RingTheory.Etale.StandardEtale
/-- Mapping a standard etale pair under a ring homomorphism.  -/
StandardEtalePair.map : {R : Type u_1} →
  {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → StandardEtalePair R → (R →+* S) → StandardEtalePair S
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropy_nonneg : ∀ {X : Type u_1} {F : Set X} [inst : UniformSpace X] (T : X → X), F.Nonempty → 0 ≤ Dynamics.coverEntropy T F
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- The resolution maps intertwine the descent of a morphism and that morphism.  -/
CategoryTheory.InjectiveResolution.desc_commutes_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Z ⟶ Y)
  (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z) {Z_1 : CochainComplex C ℕ}
  (h : I.cocomplex ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp J.ι
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.desc f I J) h) =
    CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) (CategoryTheory.CategoryStruct.comp I.ι h)
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.instFunLike : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        (φ : M →* N) →
          (A : Type u_4) →
            [inst_2 : AddMonoid A] →
              [inst_3 : DistribMulAction M A] →
                (B : Type u_5) → [inst_4 : AddMonoid B] → [inst_5 : DistribMulAction N B] → FunLike (A →ₑ+[φ] B) A B
-- Mathlib.Order.Filter.Basic
Filter.NeBot.not_disjoint : ∀ {α : Type u} {f : Filter α} {s t : Set α}, f.NeBot → s ∈ f → t ∈ f → ¬Disjoint s t
-- Mathlib.Combinatorics.SimpleGraph.Trails
SimpleGraph.Walk.IsEulerian.isTrail : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Walk u v}, p.IsEulerian → p.IsTrail
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a fallback : α}, (t.erase k).getKeyD a fallback = if cmp k a = Ordering.eq then fallback else t.getKeyD a fallback
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)}
  {hl₁ : Std.Internal.List.DistinctKeys l₁} {k : α},
  Std.Internal.List.containsKey k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) =
    (Std.Internal.List.containsKey k l₁ && Std.Internal.List.containsKey k l₂)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
/-- **Alias** of `MeasureTheory.measure_sdiff_symm`.

---

If `s` and `t` are null measurable sets of equal measure
and their intersection has finite measure,
then `s \ t` and `t \ s` have equal measures too.  -/
MeasureTheory.measure_diff_symm : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    MeasureTheory.NullMeasurableSet t μ → μ s = μ t → μ (s ∩ t) ≠ ⊤ → μ (s \ t) = μ (t \ s)
-- Mathlib.Analysis.Calculus.FDeriv.Linear
IsBoundedLinearMap.hasFDerivAt : ∀ {𝕜 : 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}
  {x : E} (h : IsBoundedLinearMap 𝕜 f), HasFDerivAt f (IsBoundedLinearMap.toContinuousLinearMap f h) x
-- Mathlib.Analysis.Calculus.FDeriv.Mul
ContinuousLinearMap.mulLeftRight.congr_simp : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R],
  ContinuousLinearMap.mulLeftRight 𝕜 R = ContinuousLinearMap.mulLeftRight 𝕜 R
-- Mathlib.Analysis.Calculus.Rademacher
/-- A function on a finite-dimensional space which is Lipschitz on a set and taking values in a
product space is differentiable almost everywhere in this set. Superseded by
`LipschitzOnWith.ae_differentiableWithinAt_of_mem` which works for functions taking value in any
finite-dimensional space.  -/
LipschitzOnWith.ae_differentiableWithinAt_of_mem_pi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {C : NNReal} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {ι : Type u_3}
  [inst_6 : Fintype ι] {f : E → ι → ℝ} {s : Set E},
  LipschitzOnWith C f s → ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceToNat : Lean.Meta.Simp.DSimproc
-- Init.Data.Nat.Lemmas
Nat.sub_lt_iff_lt_add' : ∀ {a b c : ℕ}, b ≤ a → (a - b < c ↔ a < b + c)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_lt_pi_iff : ∀ {z : ℂ}, z.arg < Real.pi ↔ 0 ≤ z.re ∨ z.im ≠ 0
-- Init.Data.Nat.Coprime
Nat.coprime_mul_iff_right : ∀ {k m n : ℕ}, k.Coprime (m * n) ↔ k.Coprime m ∧ k.Coprime n
-- Lean.Elab.DocString
Lean.Doc.DocArg.ident.sizeOf_spec : ∀ (val : Lean.Ident), sizeOf (Lean.Doc.DocArg.ident val) = 1 + sizeOf val
-- Mathlib.LinearAlgebra.Prod
/-- The left injection into a product is a linear map.  -/
LinearMap.inl : (R : Type u) →
  (M : Type v) →
    (M₂ : Type w) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → M →ₗ[R] M × M₂
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.collect.go : Lean.Meta.Grind.EMatch.InstanceMap → Lean.Expr → StateM Lean.Meta.Grind.Action.CollectState✝ Unit
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.continuous_symm_of_mem_pretrivializationAtlas : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E)
  {e : Bundle.Pretrivialization F Bundle.TotalSpace.proj},
  e ∈ a.pretrivializationAtlas → ContinuousOn (↑e.symm) e.target
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.addCancelCommMonoid : {α : Type u_1} →
  [inst : AddCancelCommMonoid α] → [inst_1 : Preorder α] → [AddLeftMono α] → AddCancelCommMonoid { x // 0 ≤ x }
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.trivialFunctor_obj_V : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] (V : ModuleCat k),
  ↑((Rep.trivialFunctor k G).obj V) = ↑V
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Probability.CondVar
/-- Conditional variance of a real-valued random variable. It is defined as `0` if any one of the
following conditions is true:
- `m` is not a sub-σ-algebra of `m₀`,
- `μ` is not σ-finite with respect to `m`,
- `X - μ[X | m]` is not square-integrable.  -/
ProbabilityTheory.condVar : {Ω : Type u_1} → {m₀ : MeasurableSpace Ω} → MeasurableSpace Ω → (Ω → ℝ) → MeasureTheory.Measure Ω → Ω → ℝ
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.measure_inter_eq_of_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  (∀ᵐ (a : α) ∂μ, a ∈ t) → μ (t ∩ s) = μ s
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.enorm_eq_iSup_enorm : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)), ‖f‖ₑ = ⨆ x, ‖f x‖ₑ
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.ReflectsMonomorphisms.iso_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G), F.ReflectsMonomorphisms ↔ G.ReflectsMonomorphisms
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- If a bifunctor preserves separately limits of `K₁` in the first variable and limits
of `K₂` in the second variable, then it preserves colimit of the pair of cones `K₁, K₂`.  -/
CategoryTheory.Limits.PreservesLimit₂.of_preservesLimits_in_each_variable : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [∀ (x : C₂), CategoryTheory.Limits.PreservesLimit K₁ (G.flip.obj x)]
  [∀ (x : C₁), CategoryTheory.Limits.PreservesLimit K₂ (G.obj x)], CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_zero : ∀ {α : Type u_1} {M₀ : Type u_7} [inst : CommMonoidWithZero M₀] (f : α → M₀) (x : α),
  f x = 0 → Function.HasFiniteMulSupport f → ∏ᶠ (x : α), f x = 0
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- Finitely generated modules, as a property of objects of `ModuleCat R`.  -/
ModuleCat.isFG : (R : Type u) → [inst : Ring R] → CategoryTheory.ObjectProperty (ModuleCat R)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.to_red : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Red L₁ L₂
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.keys_eq_keys : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.keys = Std.Internal.List.keys t.toListModel
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.pos_add_of_left`. -/
add_pos_of_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [IsBotZeroClass α] [AddLeftMono α] {a : α},
  0 < a → ∀ (b : α), 0 < a + b
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.cofork_π : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g],
  (CategoryTheory.Limits.coequalizer.cofork f g).π = CategoryTheory.Limits.coequalizer.π f g
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- `pelimVar p1 p2` calls `elimVar` on the `Comp` components of `p1` and `p2`.
If this returns `v1` and `v2`, it creates a new `PComp` equal to `v1*p1 + v2*p2`,
and tracks this in the `CompSource`.
 -/
Mathlib.Tactic.Linarith.pelimVar : Mathlib.Tactic.Linarith.PComp → Mathlib.Tactic.Linarith.PComp → ℕ → Option Mathlib.Tactic.Linarith.PComp
-- Init.Data.List.Nat.Range
List.mk_mem_zipIdx_iff_le_and_getElem?_sub : ∀ {α : Type u_1} {k i : ℕ} {x : α} {l : List α}, (x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = some x