mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- `toIocDiv` is continuous on the left at every point.

In fact, a stronger statement is true:
it's eventually constant on the left, see `eventuallyEq_toIocDiv_nhdsLE`.  -/
continuousWithinAt_toIocDiv_Iic : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜),
  ContinuousWithinAt (toIocDiv hp a) (Set.Iic x) x
-- Lean.Elab.BuiltinNotation
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.elabParserMacroAux : Lean.Term → Lean.Term → Bool → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ),
  F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X).unop =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso F.op n).inv.app
          (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor Dᵒᵖ n).map
            ((CategoryTheory.Functor.commShiftIso F n).hom.app (Opposite.unop X)).op).unop
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).counitIso.inv.app
            (Opposite.op (F.obj (Opposite.unop X)))).unop)
-- Std.Data.DHashMap.Raw
/-- Returns an array of all keys present in the hash map in some order.  -/
Std.DHashMap.Raw.keysArray : {α : Type u} → {β : α → Type v} → Std.DHashMap.Raw α β → Array α
-- Mathlib.CategoryTheory.Limits.Fubini
/-- Extract the functor `J ⥤ C` consisting of the cone points and the maps between them,
from a `DiagramOfCones`.
 -/
CategoryTheory.Limits.DiagramOfCones.conePoints : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              CategoryTheory.Limits.DiagramOfCones F → CategoryTheory.Functor J C
-- Mathlib.Analysis.Convolution
MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      ∀ (x : G), MeasureTheory.AEStronglyMeasurable (fun t => (L (f t)) (g (x - t))) μ
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x x' : ↥X) (h : x ⤳ x') {Z : CommRingCat}
  (h_1 : X.presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x) h_1) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x')
      (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes h) h_1)
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  (CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux M).hom = CategoryTheory.CategoryStruct.id M.X.X
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.saturation_bot : ∀ {M : Type u_1} [inst : AddZeroClass M], ⊥.saturation = ⊥
-- Mathlib.Order.Interval.Finset.Defs
/-- Left-infinite right-open interval  -/
LocallyFiniteOrderBot.finsetIio : {α : Type u_1} → {inst : Preorder α} → [self : LocallyFiniteOrderBot α] → α → Finset α
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_eq_one_iff_inv_eq₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, a ≠ 0 → (a * b = 1 ↔ a⁻¹ = b)
-- Std.Data.ExtDHashMap.Basic
/-- Computes the intersection of the given hash maps. The result will only contain entries from the first map.

This function always iterates through the smaller map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.ExtDHashMap.inter : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → Std.ExtDHashMap α β → Std.ExtDHashMap α β
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimits_of_hasColimits_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ],
  CategoryTheory.Limits.HasLimitsOfSize.{v₂, u₂, v₁, u₁} C
-- Mathlib.LinearAlgebra.Orientation
Orientation.reindex_refl : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] (M : Type u_2)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {ι : Type u_4},
  Orientation.reindex R M (Equiv.refl ι) = Equiv.refl (Orientation R M ι)
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_right_addition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} (f g : X ⟶ Y),
  f + g =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
      (CategoryTheory.Limits.biprod.desc f g)
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
CategoryTheory.Functor.hasPointwiseLeftDerivedFunctor_of_inverts : ∀ {C : Type u₁} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₃, u₃} H]
  (F : CategoryTheory.Functor C H) {W : CategoryTheory.MorphismProperty C},
  W.IsInvertedBy F → F.HasPointwiseLeftDerivedFunctor W
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
/-- `ContinuousMultilinearMap.compContinuousLinearMap` as a bundled continuous linear equiv.
Given a family of continuous linear equivalences `f : Π i, E i ≃L[𝕜] E₁ i`,
this function returns a continuous linear equivalence
between the space of continuous multilinear maps with domain `Π i, E i` and codomain `F`
and the space of multilinear maps with domain `Π i, E₁ i` and the same codomain,
by composing the multilinear maps with `f`.  -/
ContinuousLinearEquiv.continuousMultilinearMapCongrLeft : {𝕜 : Type u_1} →
  {ι : Type u_2} →
    {E : ι → Type u_3} →
      {E₁ : ι → Type u_4} →
        (F : Type u_5) →
          [inst : NormedField 𝕜] →
            [inst_1 : (i : ι) → TopologicalSpace (E i)] →
              [inst_2 : (i : ι) → AddCommGroup (E i)] →
                [inst_3 : (i : ι) → Module 𝕜 (E i)] →
                  [inst_4 : (i : ι) → TopologicalSpace (E₁ i)] →
                    [inst_5 : (i : ι) → AddCommGroup (E₁ i)] →
                      [inst_6 : (i : ι) → Module 𝕜 (E₁ i)] →
                        [inst_7 : AddCommGroup F] →
                          [inst_8 : Module 𝕜 F] →
                            [inst_9 : TopologicalSpace F] →
                              [inst_10 : IsTopologicalAddGroup F] →
                                [inst_11 : ContinuousConstSMul 𝕜 F] →
                                  ((i : ι) → E i ≃L[𝕜] E₁ i) →
                                    ContinuousMultilinearMap 𝕜 E₁ F ≃L[𝕜] ContinuousMultilinearMap 𝕜 E F
-- Lean.Elab.Match
Lean.Elab.Term.GeneralizeResult.mk.inj : ∀ {discrs : Array Lean.Elab.Term.Discr} {toClear : Array Lean.FVarId} {matchType : Lean.Expr}
  {altViews : Array Lean.Elab.Term.TermMatchAltView} {refined : Bool} {discrs_1 : Array Lean.Elab.Term.Discr}
  {toClear_1 : Array Lean.FVarId} {matchType_1 : Lean.Expr} {altViews_1 : Array Lean.Elab.Term.TermMatchAltView}
  {refined_1 : Bool},
  { discrs := discrs, toClear := toClear, matchType := matchType, altViews := altViews, refined := refined } =
      { discrs := discrs_1, toClear := toClear_1, matchType := matchType_1, altViews := altViews_1,
        refined := refined_1 } →
    discrs = discrs_1 ∧ toClear = toClear_1 ∧ matchType = matchType_1 ∧ altViews = altViews_1 ∧ refined = refined_1
-- Mathlib.GroupTheory.OrderOfElement
/-- A nonempty idempotent subset of a finite additive group is a subgroup  -/
addSubgroupOfIdempotent : {G : Type u_6} → [inst : AddGroup G] → [Finite G] → (S : Set G) → S.Nonempty → S + S = S → AddSubgroup G
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- For a concrete category `(A, s)` where the forgetful functor `s : A ⥤ Type v` preserves limits and
reflects isomorphisms, and `A` has limits, an `A`-valued presheaf `P : Cᵒᵖ ⥤ A` is a sheaf iff its
underlying `Type`-valued presheaf `P ⋙ s : Cᵒᵖ ⥤ Type` is a sheaf.

Note this lemma applies for "algebraic" categories, e.g. groups, abelian groups and rings, but not
for the category of topological spaces, topological rings, etc. since reflecting isomorphisms does
not hold.
 -/
CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A' : Type u₂}
  [inst_1 : CategoryTheory.Category.{max v₁ u₁, u₂} A'] (J : CategoryTheory.GrothendieckTopology C)
  (P' : CategoryTheory.Functor Cᵒᵖ A') (s : CategoryTheory.Functor A' (Type (max v₁ u₁)))
  [CategoryTheory.Limits.HasLimits A'] [CategoryTheory.Limits.PreservesLimits s] [s.ReflectsIsomorphisms],
  CategoryTheory.Presheaf.IsSheaf J P' ↔ CategoryTheory.Presheaf.IsSheaf J (P'.comp s)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J],
  (∀ (X₁ X₂ : CategoryTheory.Functor J C) (c₁ : CategoryTheory.Limits.Cocone X₁) (c₂ : CategoryTheory.Limits.Cocone X₂)
      (h₁ : CategoryTheory.Limits.IsColimit c₁) (h₁ : CategoryTheory.Limits.IsColimit c₂) (f : X₁ ⟶ X₂),
      W.functorCategory J f →
        ∀ (φ : c₁.pt ⟶ c₂.pt),
          (∀ (j : J),
              CategoryTheory.CategoryStruct.comp (c₁.ι.app j) φ =
                CategoryTheory.CategoryStruct.comp (f.app j) (c₂.ι.app j)) →
            W φ) →
    W.IsStableUnderColimitsOfShape J
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- A functorial version of `Cosimplicial_object.Augmented.leftOp`.  -/
CategoryTheory.cosimplicialToSimplicialAugmented : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ)
      (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ
-- Lean.Meta.MkIffOfInductiveProp
/-- Has the effect of `refine ⟨e₁,e₂,⋯, ?_⟩`.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.MVarId.existsi : Lean.MVarId → List Lean.Expr → Lean.MetaM Lean.MVarId
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- If `f` has derivative `f'` within `s` at `x`, then for any `r > ‖f'‖` the ratio
`‖f z - f x‖ / ‖z - x‖` is less than `r` in some neighborhood of `x` within `s`.
In other words, the limit superior of this ratio as `z` tends to `x` along `s`
is less than or equal to `‖f'‖`.  -/
HasDerivWithinAt.limsup_norm_slope_le : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {f' : E} {s : Set ℝ} {x r : ℝ},
  HasDerivWithinAt f f' s x → ‖f'‖ < r → ∀ᶠ (z : ℝ) in nhdsWithin x s, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
-- Mathlib.Algebra.Ring.Int.Parity
Int.odd_sub : ∀ {m n : ℤ}, Odd (m - n) ↔ (Odd m ↔ Even n)
-- Mathlib.GroupTheory.OrderOfElement
AddRightCancelMonoid.infinite_multiples : ∀ {G : Type u_1} [inst : AddRightCancelMonoid G] {a : G}, (↑(AddSubmonoid.multiples a)).Infinite ↔ ¬IsOfFinAddOrder a
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm_top : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {K : TopologicalSpace.Compacts E} {i : ℕ} {f : ContDiffMapSupportedIn E F ⊤ K} {x : E},
  ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F ⊤ K i) f
-- Mathlib.Topology.ContinuousMap.T0Sierpinski
TopologicalSpace.productOfMemOpens_isEmbedding : ∀ (X : Type u_1) [inst : TopologicalSpace X] [T0Space X], Topology.IsEmbedding ⇑(TopologicalSpace.productOfMemOpens X)
-- Mathlib.RingTheory.Flat.Basic
IsTensorProduct.map_id_injective_of_flat_right : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {M₁ : Type u_5} {M₂ : Type u_6} {N₁ : Type u_7}
  [inst_5 : AddCommMonoid M₁] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₁] [inst_8 : Module R M₂]
  [inst_9 : AddCommMonoid N₁] [inst_10 : Module R N₁] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f)
  {g : N₁ →ₗ[R] M₂ →ₗ[R] N} (hg : IsTensorProduct g) (i : M₁ →ₗ[R] N₁),
  Function.Injective ⇑i → ∀ [Module.Flat R M₂], Function.Injective ⇑(hf.map hg i LinearMap.id)
-- Init.Data.SInt.Lemmas
Int32.right_eq_add : ∀ {a b : Int32}, b = a + b ↔ a = 0
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (producers : Std.Queue (IO.Promise Bool))
  (consumers : Std.Queue (Std.CloseableChannel.Bounded.Consumer✝ α)) (capacity : ℕ)
  (buf : Vector (IO.Ref (Option α)) capacity) (bufCount sendIdx : ℕ) (hsend : sendIdx < capacity) (recvIdx : ℕ)
  (hrecv : recvIdx < capacity) (closed : Bool),
  sizeOf
      { producers := producers, consumers := consumers, capacity := capacity, buf := buf, bufCount := bufCount,
        sendIdx := sendIdx, hsend := hsend, recvIdx := recvIdx, hrecv := hrecv, closed := closed } =
    1 + sizeOf producers + sizeOf consumers + sizeOf capacity + sizeOf buf + sizeOf bufCount + sizeOf sendIdx +
            sizeOf hsend +
          sizeOf recvIdx +
        sizeOf hrecv +
      sizeOf closed
-- Init.Grind.AC
Lean.Grind.AC.Seq.union : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  X.zeroLocus ↑(I.ideal U) ∩ ↑↑U ⊆ I.supportSet
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_X_pow : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [Nontrivial R] (s : σ) (n : ℕ),
  (MvPolynomial.X s ^ n).support = {fun₀ | s => n}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.fold_eq_foldl_toList : ∀ {α : Type u} {δ : Type w} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {f : δ → α → β → δ} {init : δ},
  Std.DHashMap.Raw.fold f init ↑m = List.foldl (fun a b => f a b.1 b.2) init (Std.DHashMap.Raw.Const.toList ↑m)
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.range_projectionOnto`. -/
Submodule.linearProjOfIsCompl_range : ∀ {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), (p.projectionOnto q h).range = ⊤
-- Std.Time.Format.Modifier
Std.Time.Fraction.truncated.injEq : ∀ (digits digits_1 : ℕ),
  (Std.Time.Fraction.truncated digits = Std.Time.Fraction.truncated digits_1) = (digits = digits_1)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Reinterpret a continuous `A`-alternating map as a continuous `R`-alternating map, if `A` is an
algebra over `R` and their actions on all involved modules agree with the action of `R` on `A`.  -/
ContinuousAlternatingMap.restrictScalars : (R : Type u_1) →
  {M : Type u_2} →
    {N : Type u_4} →
      {ι : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] →
                      {A : Type u_7} →
                        [inst_7 : Semiring A] →
                          [inst_8 : SMul R A] →
                            [inst_9 : Module A M] →
                              [inst_10 : Module A N] →
                                [IsScalarTower R A M] → [IsScalarTower R A N] → M [⋀^ι]→L[A] N → M [⋀^ι]→L[R] N
-- Mathlib.NumberTheory.Divisors
Int.divisorsAntidiag_ofNat : ∀ (n : ℕ),
  (OfNat.ofNat n).divisorsAntidiag =
    (Finset.map (Nat.castEmbedding.prodMap Nat.castEmbedding) n.divisorsAntidiagonal).disjUnion
      (Finset.map
        ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap
          (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))))
        n.divisorsAntidiagonal)
      ⋯
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Even if a function has equation theorems,
we also store it in the `toUnfold` set in the following two cases:
1- It was defined by structural recursion and has a smart-unfolding associated declaration.
2- It is non-recursive.

Reason: `unfoldPartialApp := true` or conditional equations may not apply.

Remark: In the future, we are planning to disable this
behavior unless `unfoldPartialApp := true`.
Moreover, users will have to use `f.eq_def` if they want to force the definition to be
unfolded.
 -/
Lean.Meta.Simp.unfoldEvenWithEqns : Lean.Name → Lean.CoreM Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.DHashMap.Const.getD (Std.DHashMap.Const.ofList l) k' fallback = v
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_const : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {x : M} {c : M'},
  (mfderiv% fun x => c) x = 0
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.comp_of_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} {y : β},
  ContinuousWithinAt g t y → ContinuousWithinAt f s x → Set.MapsTo f s t → f x = y → ContinuousWithinAt (g ∘ f) s x
-- Init.Data.Dyadic.Basic
/-- Convert a rational number `x` to the greatest dyadic number with precision at most `prec`
which is less than or equal to `x`.
 -/
Rat.toDyadic : ℚ → ℤ → Dyadic
-- Mathlib.Data.Set.Sups
Set.infs_right_comm : ∀ {α : Type u_2} [inst : SemilatticeInf α] (s t u : Set α), s ⊼ t ⊼ u = s ⊼ u ⊼ t
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.δ.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.δ = ⋯.desc (CategoryTheory.CategoryStruct.comp S.φ₁ S.v₂₃.τ₁) ⋯
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instSMul : {R : Type u_1} → {S : Type u_2} → {a b : R} → [SMul S R] → SMul S (QuadraticAlgebra R a b)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.numNodes_toTree : ∀ (p : DyckWord), p.toTree.numNodes = p.semilength
-- Mathlib.Topology.Algebra.Group.Pointwise
/-- If a function defined on a topological additive group has a support contained in a compact
set, then either the function is trivial or the group is locally compact.  -/
eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : TopologicalSpace α] [inst_4 : Zero α] [T1Space α] {f : G → α} {k : Set G},
  IsCompact k → Function.support f ⊆ k → Continuous f → f = 0 ∨ LocallyCompactSpace G
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
/-- The canonical approximate unit in a C⋆-algebra generated by the basis of sets
`{x | a ≤ x} ∩ closedBall 0 1` for `0 ≤ a`. See also `CStarAlgebra.hasBasis_approximateUnit`.  -/
CStarAlgebra.approximateUnit : (A : Type u_1) → [inst : NonUnitalCStarAlgebra A] → [inst_1 : PartialOrder A] → [StarOrderedRing A] → Filter A
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toComon_forget : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.Bimon.toComon C).comp (CategoryTheory.Comon.forget C) = CategoryTheory.Bimon.forget C
-- Mathlib.Analysis.Complex.Exponential
/-- Extension for the `positivity` tactic: `Real.exp` is always positive.  -/
Mathlib.Meta.Positivity.evalExp : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Algebra.Algebra.Bilinear
/-- A `LinearMap` preserves multiplication if pre- and post- composition with `LinearMap.mul` are
equivalent. By converting the statement into an equality of `LinearMap`s, this lemma allows various
specialized `ext` lemmas about `→ₗ[R]` to then be applied.

This is the `LinearMap` version of `AddMonoidHom.map_mul_iff`.  -/
LinearMap.map_mul_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A]
  [inst_2 : NonUnitalSemiring B] [inst_3 : Module R B] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : SMulCommClass R B B] [inst_8 : IsScalarTower R B B] (f : A →ₗ[R] B),
  (∀ (x y : A), f (x * y) = f x * f y) ↔ (LinearMap.mul R A).compr₂ f = (LinearMap.mul R B ∘ₗ f).compl₂ f
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_sub : ∀ (R : Type u_1) [inst : Ring R] {S : Type u_2} [inst_1 : AddCommGroup S] [inst_2 : Pow S ℕ] [inst_3 : Module R S]
  (p q : Polynomial R) (x : S), (p - q).smeval x = p.smeval x - q.smeval x
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.edist_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
  {f : X → Y}, HolderWith C r f → ∀ (x y : X), edist (f x) (f y) ≤ ↑C * edist x y ^ ↑r
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionObj : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) [inst_3 : F.Monoidal] (d : D) (c : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c = (F.obj c).obj d
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetAux_eq_map_coe : ∀ {α : Type u_1} {l : List α}, Multiset.powersetAux l = List.map Multiset.ofList l.sublists
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, ∅.minKey? = none
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.willDelete.sizeOf_spec : sizeOf Lean.Widget.DiffTag.willDelete = 1
-- Mathlib.Data.Sum.Order
Sum.Lex.toLex_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], StrictMono ⇑toLex