mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkFunctorRight_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E)
  (G : CategoryTheory.Functor D E) (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G)
  (X : D), (CategoryTheory.Join.mkFunctorRight F G α).inv.app X = CategoryTheory.CategoryStruct.id (G.obj X)
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instLEPosition : LE Lean.Lsp.Position
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.norm_setToFun_le_toReal : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C),
  ‖MeasureTheory.setToFun μ T hT f‖ ≤ ↑(NNReal.mk C hC) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- Any object at the top left of a pullback square is isomorphic to the object at the top left
of any other pullback square with the same cospan.  -/
CategoryTheory.IsPullback.isoIsPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : C} →
      (X Y : C) →
        {Z : C} →
          {fst : P ⟶ X} →
            {snd : P ⟶ Y} →
              {f : X ⟶ Z} →
                {g : Y ⟶ Z} →
                  {P' : C} →
                    {fst' : P' ⟶ X} →
                      {snd' : P' ⟶ Y} →
                        CategoryTheory.IsPullback fst snd f g → CategoryTheory.IsPullback fst' snd' f g → (P ≅ P')
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.toContinuousLinearMap_apply : ∀ {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] (f : M [⋀^ι]→L[R] N) [inst_7 : DecidableEq ι] (m : ι → M) (i : ι) (x : M),
  (f.toContinuousLinearMap m i) x = f (Function.update m i x)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
/-- The preadditive structure on `D`, when `L : C ⥤ D` is a localization
functor, `C` is preadditive and there is a left calculus of fractions.  -/
CategoryTheory.Localization.preadditive : {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] →
        [CategoryTheory.Preadditive C] →
          (L : CategoryTheory.Functor C D) →
            (W : CategoryTheory.MorphismProperty C) →
              [L.IsLocalization W] → [W.HasLeftCalculusOfFractions] → CategoryTheory.Preadditive D
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_swap : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), (o.kahler x) y = (starRingEnd ℂ) ((o.kahler y) x)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimit.ι_desc_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (H : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimit H]
  (c : CategoryTheory.Limits.Cocone H) (j : J) (k : K),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι H j).app k)
      ((CategoryTheory.Limits.colimit.desc H c).app k) =
    (c.ι.app j).app k
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- The atlas of charts in the `ChartedSpace`.  -/
ChartedSpace.atlas : {H : Type u_5} →
  {inst : TopologicalSpace H} →
    {M : Type u_6} → {inst_1 : TopologicalSpace M} → [self : ChartedSpace H M] → Set (OpenPartialHomeomorph M H)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.mul_vlt_mul_iff_right`. -/
ValuativeRel.vlt_mul_left_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, 0 <ᵥ x → (x * y <ᵥ x * z ↔ y <ᵥ z)
-- Mathlib.Geometry.RingedSpace.Stalks
/-- A morphism of presheafed spaces induces a morphism of stalks.
 -/
AlgebraicGeometry.PresheafedSpace.Hom.stalkMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : AlgebraicGeometry.PresheafedSpace C} →
        (α : X.Hom Y) →
          (x : ↑↑X) → Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom α.base) x) ⟶ X.presheaf.stalk x
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith_def : ∀ {α : Type u_18} {E : Type u_19} {F : Type u_20} [inst : Norm E] [inst_1 : Norm F] (c : ℝ) (l : Filter α) (f : α → E)
  (g : α → F), Asymptotics.IsBigOWith c l f g = ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.ext : ∀ {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} {x y : F.LaxMonoidal},
  CategoryTheory.Functor.LaxMonoidal.ε F = CategoryTheory.Functor.LaxMonoidal.ε F →
    CategoryTheory.Functor.LaxMonoidal.μ F = CategoryTheory.Functor.LaxMonoidal.μ F → x = y
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.univ_pi_Ioc_ae_eq_Icc : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)] {f g : (i : ι) → α i},
  (Set.univ.pi fun i => Set.Ioc (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] Set.Icc f g
-- Mathlib.Topology.Category.TopCat.Opens
/-- The inclusion `U ⟶ ⊤` as a morphism in the category of open sets.
 -/
TopologicalSpace.Opens.leTop : {X : TopCat} → (U : TopologicalSpace.Opens ↑X) → U ⟶ ⊤
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} (h : t.WF),
  (Std.DTreeMap.Raw.filterMap f t).getKey? k =
    (t.getKey? k).pfilter fun x h' => (f x (Std.DTreeMap.Raw.Const.get t x ⋯)).isSome
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_eq_get_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : a ∈ t}, t[a] = t[a]?.get ⋯
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.BlockTriangular.charpoly : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  {α : Type u_5} {b : n → α} [inst_3 : LinearOrder α],
  M.BlockTriangular b → M.charpoly = ∏ a ∈ Finset.image b Finset.univ, (M.toSquareBlock b a).charpoly
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.ctor.injEq : ∀ (a : Lean.Name) (a_1 : List Lean.Meta.Match.Example) (a_2 : Lean.Name) (a_3 : List Lean.Meta.Match.Example),
  (Lean.Meta.Match.Example.ctor a a_1 = Lean.Meta.Match.Example.ctor a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.toTopologicalSpace_bot : ∀ {α : Type ua}, ⊥.toTopologicalSpace = ⊥
-- Mathlib.Order.WithBot
WithBot.some_eq_coe : ∀ {α : Type u_1} (a : α), some a = ↑a
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.instTop : {α : Type u_2} → {β : Type u_3} → [inst : InfSet α] → {x : CompleteLattice β} → Top (sInfHom α β)
-- Mathlib.Algebra.Field.Basic
Commute.one_div_add_one_div : ∀ {K : Type u_1} [inst : DivisionSemiring K] {a b : K}, Commute a b → a ≠ 0 → b ≠ 0 → 1 / a + 1 / b = (a + b) / (a * b)
-- Mathlib.RingTheory.FiniteLength
IsFiniteLength.below : {R : Type u_1} →
  [inst : Ring R] →
    {motive : (M : Type u_2) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → IsFiniteLength R M → Prop} →
      {M : Type u_2} → {inst_1 : AddCommGroup M} → {inst_2 : Module R M} → IsFiniteLength R M → Prop
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjIso_hom_restrict : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjIso✝ I U).hom
      (I.gluedTo ∣_ ↑U) =
    I.glueDataObjι U
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
List.one_le_prod : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {s : List R},
  (∀ a ∈ s, 1 ≤ a) → 1 ≤ s.prod
-- Mathlib.CategoryTheory.Action.Limits
Action.instReflectsColimitForget : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} J] (F : CategoryTheory.Functor J (Action V G)),
  CategoryTheory.Limits.ReflectsColimit F (Action.forget V G)
-- Mathlib.GroupTheory.Torsion
CommMonoid.Torsion.ofTorsion.eq_1 : ∀ (G : Type u_1) [inst : CommMonoid G], CommMonoid.Torsion.ofTorsion G = ⋯.torsionMulEquiv
-- Mathlib.Data.Nat.Cast.Basic
map_natCast : ∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : FunLike F R S] [RingHomClass F R S] (f : F) (n : ℕ), f ↑n = ↑n
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.edist_eq_iSup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  {f g : C(α, β)}, edist f g = ⨆ x, edist (f x) (g x)
-- Init.Core
/-- `HEq.ndrec` specialized to homogeneous heterogeneous equality, symmetric variant  -/
HEq.homo_ndrec_symm : {α : Sort u2} → {a : α} → {motive : α → Sort u1} → motive a → {b : α} → b ≍ a → motive b
-- Mathlib.Analysis.Meromorphic.IsolatedZeros
/-- Formulation of `MeromorphicAt.eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin` as an
identity principle: Let `U` be a subset of `𝕜` and assume that `x ∈ U` is not an isolated point of
`U`. If function `f` and `g` are meromorphic at `x` and agree along a subset that is codiscrete
within `U`, then `f` and `g` agree in a punctured neighbourhood of `f`.
 -/
MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {x : 𝕜} {f g : 𝕜 → E},
  MeromorphicAt f x →
    MeromorphicAt g x →
      x ∈ U → AccPt x (Filter.principal U) → f =ᶠ[Filter.codiscreteWithin U] g → f =ᶠ[nhdsWithin x {x}ᶜ] g
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- Use `IndObjectPresentation.cocone` instead.  -/
CategoryTheory.Limits.IndObjectPresentation.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (self : CategoryTheory.Limits.IndObjectPresentation A) →
        self.F.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const self.I).obj A
-- Mathlib.Data.Finsupp.Single
Finsupp.apply_single' : ∀ {α : Type u_1} {N : Type u_7} {P : Type u_8} [inst : Zero N] [inst_1 : Zero P] (e : N → P),
  e 0 = 0 → ∀ (a : α) (n : N) (b : α), e ((fun₀ | a => n) b) = (fun₀ | a => e n) b
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.coe_prodCongr : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6}
  [inst_2 : TopologicalSpace X'] [inst_3 : TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y'),
  ⇑(h₁.prodCongr h₂) = Prod.map ⇑h₁ ⇑h₂
-- Mathlib.Algebra.Group.Units.Hom
IsUnit.liftRight_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (hf : ∀ (x : M), IsUnit (f x))
  (x : M), (IsUnit.liftRight f hf) x = ⋯.unit
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.indepFun_mul_left : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β} [inst_2 : Mul β]
  [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.CondIndepFun m' hm' (f i * f j) (f k) μ
-- Init.Data.Array.Lemmas
Array.push_eq_append_singleton : ∀ {α : Type u_1} {as : Array α} {x : α}, as.push x = as ++ #[x]
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Multiset.disjoint_sum_right : ∀ {α : Type u_6} {a : Multiset α} {i : Multiset (Multiset α)}, Disjoint a i.sum ↔ ∀ b ∈ i, Disjoint a b
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If there is a primitive `n`th root of unity in `R`, then `X ^ n - Y ^ n = ∏ (X - μ Y)`,
where `μ` varies over the `n`-th roots of unity.  -/
IsPrimitiveRoot.pow_sub_pow_eq_prod_sub_mul : ∀ {R : Type u_1} [inst : CommRing R] {ζ : R} {n : ℕ} (x y : R) [inst_1 : IsDomain R],
  0 < n → IsPrimitiveRoot ζ n → x ^ n - y ^ n = ∏ ζ ∈ Polynomial.nthRootsFinset n 1, (x - ζ * y)
-- Mathlib.Algebra.Order.Group.Synonym
toDual_smul : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α), OrderDual.toDual (b • a) = b • OrderDual.toDual a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblXYZ_X : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.dblXYZ P 0 = W'.dblX P
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceLErase.match_7.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l : Std.DTreeMap.Internal.Impl α β) →
      (motive :
          (r : Std.DTreeMap.Internal.Impl α β) →
            r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size → Sort u_3) →
        (r : Std.DTreeMap.Internal.Impl α β) →
          (hrb : r.Balanced) →
            (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size) →
              ((hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                  (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size Std.DTreeMap.Internal.Impl.leaf.size) →
                    motive Std.DTreeMap.Internal.Impl.leaf hrb hlr) →
                ((rs : ℕ) →
                    (k : α) →
                      (v : β k) →
                        (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                          (hrb : (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).Balanced) →
                            (hlr :
                                Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size
                                  (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).size) →
                              motive (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r) hrb hlr) →
                  motive r hrb hlr
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_add_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α},
  (s + t).card = s.card * t.card ↔ Set.InjOn (fun p => p.1 + p.2) (↑s ×ˢ ↑t)
-- Mathlib.Combinatorics.Additive.SmallTripling
/-- If `A` is symmetric (`A⁻¹ = A`) and has small tripling, then `A` has small powers,
in the sense that `|A ^ m|` is at most `|A|` times a constant exponential in `m`.

See also `Finset.small_alternating_pow_of_small_tripling` for a version with a weaker constant but
which encompasses non-symmetric sets.  -/
Finset.small_pow_of_small_tripling : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] {A : Finset G} {K : ℝ} {m : ℕ},
  3 ≤ m → ↑(A ^ 3).card ≤ K * ↑A.card → A⁻¹ = A → ↑(A ^ m).card ≤ K ^ (m - 2) * ↑A.card
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.ideal_eq_iInf_under_map_away : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Finset R},
  Ideal.span ↑S = ⊤ → ∀ (I : Ideal R), I = ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_keysArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k : α},
  k ∈ m.keysArray ↔ k ∈ m
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_abs : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (p : ENNReal), MeasureTheory.lpNorm |f| p μ = MeasureTheory.lpNorm f p μ
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.congr_of_eventuallyEq_of_mem : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → f₁ =ᶠ[nhdsWithin x s] f → x ∈ s → ContDiffWithinAt 𝕜 n f₁ s x
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The step function for the TM2 model.  -/
Turing.TM2.stepAux : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} → [DecidableEq K] → Turing.TM2.Stmt Γ Λ σ → σ → ((k : K) → List (Γ k)) → Turing.TM2.Cfg Γ Λ σ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Break.runK.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
alternatingGroup.normalClosure_finRotate_five : Subgroup.normalClosure {⟨finRotate 5, ⋯⟩} = ⊤
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase_dup_rhs.injEq : ∀ (c c_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.erase_dup_rhs c = Lean.Meta.Grind.AC.EqCnstrProof.erase_dup_rhs c_1) = (c = c_1)
-- Lean.Util.MonadBacktrack
Lean.MonadBacktrack.restoreState : {s : outParam Type} → {m : Type → Type} → [self : Lean.MonadBacktrack s m] → s → m Unit
-- Mathlib.Tactic.DefEqAbuse
/-- Convenience wrapper which accumulates the results of `visitM` across `arr`, attempting to
produce `empty` and `combine` from `{}` and `(· ++ ·)` or `(· ∪ ·)`, then `.ascend`s with the result
(if any). This effectively replaces a return value of `.descend`.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.visitWithAndAscendM : {m : Type → Type} →
  [Monad m] →
    {α : Type} →
      {β : Type u_1} →
        Array β →
          (β → m α) →
            autoParam α Lean.MessageData.visitWithAndAscendM._auto_1✝ →
              autoParam (α → α → α) Lean.MessageData.visitWithAndAscendM._auto_3✝ → m (Lean.MessageData.VisitStep✝ α)
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : MeasureTheory.Measure α}
  {f : α → MeasureTheory.Measure β} {s : Set β},
  MeasurableSet s → AEMeasurable f m → (m.bind f) s = ∫⁻ (a : α), (f a) s ∂m
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_neg : ∀ (a : BitVec 16), Int16.ofBitVec (-a) = -Int16.ofBitVec a
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.Std.Iter.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Lean.HeadIndex
Lean.instInhabitedHeadIndex.default : Lean.HeadIndex
-- Mathlib.Data.Countable.Basic
instCountableSigma : ∀ {α : Type u} {π : α → Type w} [Countable α] [∀ (a : α), Countable (π a)], Countable (Sigma π)
-- Mathlib.Algebra.Star.MonoidHom
/-- Reinterpret a `StarMulEquiv` as a `StarMonoidHom`.  -/
StarMulEquiv.toStarMonoidHom : {A : Type u_2} →
  {B : Type u_3} → [inst : Monoid A] → [inst_1 : Monoid B] → [inst_2 : Star A] → [inst_3 : Star B] → (A ≃⋆* B) → A →⋆* B
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.exists_neg_mem_iff_exists_mem : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {P : G → Prop}, (∃ x ∈ K, P (-x)) ↔ ∃ x ∈ K, P x
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.out_mk : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] (a : α), (Associates.mk a).out = normalize a
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F) {s : Set (G × ((i : ι) → Em i))},
  AnalyticOnNhd 𝕜 (fun p => (f p.1) p.2) s
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- A nonzero element of an eigenspace is an eigenvector. (Def 5.8 of [axler2024])  -/
Module.End.HasEigenvector : {R : Type v} →
  {M : Type w} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → M → Prop
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.ringEquiv_symm_mk : ∀ {ι : Type u_1} [inst : Preorder ι] (G : ι → Type u_2) [inst_1 : (i : ι) → CommRing (G i)]
  (f' : (i j : ι) → i ≤ j → G i →+* G j) [inst_2 : DirectedSystem G fun i j h => ⇑(f' i j h)]
  [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι] {g : (i : ι) × G i},
  (Ring.DirectLimit.ringEquiv G f').symm ⟦g⟧ = (Ring.DirectLimit.of G (fun x1 x2 x3 => ⇑(f' x1 x2 x3)) g.fst) g.snd
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- A function `f : G × G → M` satisfies the multiplicative 2-cocycle condition if
`f(gh, j) * f(g, h) = g • f(h, j) * f(g, hj)` for all `g, h : G`.  -/
groupCohomology.IsMulCocycle₂ : {G : Type u_1} → {M : Type u_2} → [Mul G] → [CommGroup M] → [SMul G M] → (G × G → M) → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.diag_map_fst_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y]
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct (X ⨯ Y) (X ⨯ Y)] {Z : C} (h : X ⨯ Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag (X ⨯ Y))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) h) =
    h
-- Mathlib.Topology.Sets.BaseChangeNhds
/-- For `K` a compact subset included in a compact subset `L`, there
is a map sending open neighbourhoods of `L` to the ones of `K`  -/
TopologicalSpace.Compacts.baseChangeOpenNhds : {α : Type u_1} → [inst : TopologicalSpace α] → {K L : TopologicalSpace.Compacts α} → (K ⟶ L) → ↑L.openNhds → ↑K.openNhds
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_sup : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [H.Characteristic] [K.Characteristic], (H ⊔ K).Characteristic
-- Mathlib.Data.Finset.Sups
Finset.powerset_union : ∀ {α : Type u_2} [inst : DecidableEq α] (s t : Finset α), (s ∪ t).powerset = s.powerset ⊻ t.powerset
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.GoalContext.mk : Lean.LocalContext →
  Lean.LocalInstances →
    Lean.LocalContext → Lean.LocalInstances → Std.HashMap Lean.FVarId Lean.FVarId → Aesop.EqualUpToIds.GoalContext
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.zpowers_eq_closure : ∀ {G : Type u_1} [inst : Group G] (g : G), Subgroup.zpowers g = Subgroup.closure {g}
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.smul_const_lt_weak : ∀ {α : Type u_1} {b c : α} {K : Type u_2} [inst : Semiring K] [inst_1 : PartialOrder K] [inst_2 : AddCommMonoid α]
  [inst_3 : PartialOrder α] [inst_4 : Module K α] [PosSMulMono K α], b < c → ∀ {s : K}, 0 ≤ s → s • b ≤ s • c
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.instToJsonMethod : Lean.ToJson Aesop.ScriptGenerated.Method