mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₁)}
  (h : (F.map f).toFunctor.obj ((F.map (CategoryTheory.CategoryStruct.id b₀)).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).hom.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId b₀).inv.toNatTrans.app X)) h
-- Mathlib.Order.Basic
lt_of_strongLT : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Preorder (π i)] {a b : (i : ι) → π i} [Nonempty ι],
  StrongLT a b → a < b
-- Init.Data.BitVec.Lemmas
BitVec.smod_zero : ∀ {w : ℕ} {x : BitVec w}, x.smod 0#w = x
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSliceTo_le_ofSliceTo_iff : ∀ {s : String.Slice} {p : s.Pos} {q r : (s.sliceTo p).Pos},
  String.Slice.Pos.ofSliceTo q ≤ String.Slice.Pos.ofSliceTo r ↔ q ≤ r
-- Mathlib.CategoryTheory.Shift.Induced
CategoryTheory.HasShift.Induced.add_inv_app_obj : ∀ {C : Type u_2} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) {A : Type u_3} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D)
  (i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F)
  [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full]
  [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (a b : A) (X : C),
  (CategoryTheory.HasShift.Induced.add F s i a b).inv.app (F.obj X) =
    CategoryTheory.CategoryStruct.comp ((s b).map ((i a).hom.app X))
      (CategoryTheory.CategoryStruct.comp ((i b).hom.app ((CategoryTheory.shiftFunctor C a).obj X))
        (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X))
          ((i (a + b)).inv.app X)))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {aig : Std.Sat.AIG α} (input input_1 : aig.RefVec w),
  input = input_1 →
    ∀ (distance distance_1 : ℕ),
      distance = distance_1 →
        ∀ (curr : ℕ) (hcurr : curr ≤ w) (s s_1 : aig.RefVec curr),
          s = s_1 →
            Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go input distance curr hcurr s =
              Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go input_1 distance_1 curr hcurr s_1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (m.insertMany l).getKey? k = m.getKey? k
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.specializingMap_respectsIso : (AlgebraicGeometry.topologically @SpecializingMap).RespectsIso
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
/-- Left-invariant global derivations.

A global derivation is left-invariant if it is equal to its pullback along left multiplication by
an arbitrary element of `G`.
 -/
LeftInvariantDerivation : {𝕜 : 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) →
                (G : Type u_4) →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] → [inst_6 : Monoid G] → [ContMDiffMul I (↑⊤) G] → Type (max u_1 u_4)
-- Mathlib.Order.Interval.Set.Basic
Set.right_notMem_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ∉ Set.Ico b a
-- Mathlib.Algebra.Group.Defs
RightCancelMonoid.toIsRightCancelMul : ∀ {M : Type u} [self : RightCancelMonoid M], IsRightCancelMul M
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalWhiskerLeft_id : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} {η : f ⟶ g}
  {η₁ : f ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g}
  {η₂ :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ⟶
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g},
  CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.leftUnitor g).inv = η₁ →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom η₁ = η₂ →
      CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η = η₂
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_whiskerRight_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.LaxFunctor B C} (x_3 x_4 : x ⟶ x_1) (Γ : x_3 ⟶ x_4) (ι : x_1 ⟶ x_2) (a : B),
  (CategoryTheory.Bicategory.whiskerRight Γ ι).as.app a = CategoryTheory.Bicategory.whiskerRight (Γ.as.app a) (ι.app a)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.Cells.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} →
                      {f : X ⟶ Y} →
                        {c : HomotopicalAlgebra.RelativeCellComplex basicCell f} →
                          (j : J) → (hj : ¬IsMax j) → (c.attachCells j hj).ι → c.Cells
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a b : α}, cmp a b = Ordering.eq → t[a]! = t[b]!
-- Init.Prelude
/-- Expands macros in the given syntax. A return value of `none` means there
was nothing to expand.  -/
Lean.Macro.Methods.expandMacro? : Lean.Macro.Methods → Lean.Syntax → Lean.MacroM (Option Lean.Syntax)
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- An open immersion induces an isomorphism from the domain onto the image  -/
AlgebraicGeometry.IsOpenImmersion.isoRestrict : {X Z : AlgebraicGeometry.Scheme} → (f : X ⟶ Z) → [H : AlgebraicGeometry.IsOpenImmersion f] → X ≅ Z.restrict ⋯
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.div.congr_simp : ∀ {A : Type u_1} [inst : CommRing A] {g g_1 : PowerSeries A} (e_g : g = g_1) {I I_1 : Ideal A} (e_I : I = I_1)
  (H : g.IsWeierstrassDivisorAt I) (f f_1 : PowerSeries A),
  f = f_1 → ∀ [inst_1 : IsPrecomplete I A] (a a_1 : Unit →₀ ℕ), a = a_1 → H.div f a = ⋯.div f_1 a_1
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.existsUnique : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (t : CategoryTheory.Limits.Cone F),
  ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.limit.π F j) = t.π.app j
-- Aesop.Index.RulePattern
Aesop.instBEqEntry : BEq Aesop.RulePatternIndex.Entry
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int.0.Int.reduceUnary : Lean.Name → ℕ → (ℤ → ℤ) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Data.Multiset.Powerset
Multiset.bind_powerset_len : ∀ {α : Type u_2} (S : Multiset α), ((Multiset.range (S.card + 1)).bind fun k => Multiset.powersetCard k S) = S.powerset
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.headD.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool) (a : α),
  Batteries.BinomialHeap.Imp.Heap.headD le a Batteries.BinomialHeap.Imp.Heap.nil = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mkNatIso_hom_app_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J K : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)}
  (e₁ :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G))
  (e₂ :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G))
  (coh :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e₁.hom F)
          (CategoryTheory.CategoryStruct.comp (K.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
            (CategoryTheory.CategoryStruct.comp
              (K.whiskerLeft
                (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                    (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
              (K.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv)) =
        CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
          (CategoryTheory.CategoryStruct.comp
            (J.whiskerLeft
              (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                  (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
            (CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv
              (CategoryTheory.Functor.whiskerRight e₂.hom G))))
      CategoryTheory.Limits.CategoricalPullback.mkNatIso._auto_1)
  (X_1 : X), ((CategoryTheory.Limits.CategoricalPullback.mkNatIso e₁ e₂ coh).hom.app X_1).fst = e₁.hom.app X_1
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited α]
  {l : List α} {k : α}, l.contains k = false → (Std.ExtHashSet.ofList l).get! k = default
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.map_coe : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (hinj : Function.Injective ⇑f)
  {u v : V} (p : G.Path u v), ↑(SimpleGraph.Path.map f hinj p) = SimpleGraph.Walk.map f ↑p
-- Init.Data.Range.Polymorphic.UInt
USize.rxcHasSize_eq_toBitVec : ∀ {lo : BitVec System.Platform.numBits} {hi : USize},
  Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
CategoryTheory.Limits.map_ι_comp_inv_sigmaComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [inst_2 : CategoryTheory.Limits.HasCoproduct f]
  [inst_3 : CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)]
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.Limits.sigmaComparison G f)] (j : J),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Sigma.ι f j))
      (CategoryTheory.inv (CategoryTheory.Limits.sigmaComparison G f)) =
    CategoryTheory.Limits.Sigma.ι (fun x => G.obj (f x)) j
-- Mathlib.Order.Filter.Basic
Filter.Eventually.mono : ∀ {α : Type u} {p q : α → Prop} {f : Filter α}, (∀ᶠ (x : α) in f, p x) → (∀ (x : α), p x → q x) → ∀ᶠ (x : α) in f, q x
-- Std.Time.Zoned.RecurringRule
/-- Standard time abbreviation.
 -/
Std.Time.TimeZone.RecurringRule.stdName : Std.Time.TimeZone.RecurringRule → String
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_gt' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) (i : ι), MeasurableSet {ω | ↑i < τ ω}
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.dpow_one : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (self : DividedPowers I) {x : A}, x ∈ I → self.dpow 1 x = x
-- Mathlib.Analysis.Complex.Isometry
rotation_trans : ∀ (a b : Circle), (rotation a).trans (rotation b) = rotation (b * a)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_i_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_i._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_i._auto_3) {Z : C}
  (h : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv
      (CategoryTheory.CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).iCycles h) =
    CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂ n₁) h
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.threeAPFree_sphere : ∀ {n d k : ℕ}, ThreeAPFree ↑(Behrend.sphere n d k)
-- Mathlib.Data.ENat.Basic
ENat.toNat_top : ⊤.toNat = 0
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Characterizing the inverse direction of the associator
with respect to the unit transformations  -/
CategoryTheory.MonoidalCategory.DayConvolution.associator_inv_unit_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  (H : CategoryTheory.Functor C V) [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_6 :
    CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)]
  [inst_7 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H]
  [inst_8 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_9 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  (x y z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x)
        ((CategoryTheory.MonoidalCategory.DayConvolution.unit G H).app (y, z)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.unit F
              (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)).app
          (x, CategoryTheory.MonoidalCategoryStruct.tensorObj y z))
        ((CategoryTheory.MonoidalCategory.DayConvolution.associator F G H).inv.app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj x (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj x) (G.obj y) (H.obj z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y)) (H.obj z))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.DayConvolution.unit
                (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H).app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj x y, z))
          ((CategoryTheory.MonoidalCategory.DayConvolution.convolution
                (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H).map
            (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom)))
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- The function tends to zero along the `cocompact` filter.  -/
ZeroAtInftyContinuousMap.zero_at_infty' : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  (self : ZeroAtInftyContinuousMap α β), Filter.Tendsto self.toFun (Filter.cocompact α) (nhds 0)
-- Mathlib.Algebra.GroupWithZero.Equiv
MulEquiv.toMonoidWithZeroHom_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : MulZeroOneClass G] [inst_1 : MulZeroOneClass H] (f : G ≃* H),
  Function.Surjective ⇑f.toMonoidWithZeroHom
-- Mathlib.CategoryTheory.Bicategory.Product
/-- The pseudofunctor swapping the factors of a cartesian product of bicategories,
`B × C ⥤ C × B`.  -/
CategoryTheory.Bicategory.Prod.swap : (B : Type u₁) →
  [inst : CategoryTheory.Bicategory B] →
    (C : Type u₂) → [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.StrictPseudofunctor (B × C) (C × B)
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.ofNatModule : {α : Type u} → [inst : Lean.Grind.NatModule α] → Lean.Grind.IntModule (Lean.Grind.IntModule.OfNatModule.Q α)
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformly.congr_inseparable_right : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι} {g : α → β},
  TendstoLocallyUniformly F f p → (∀ (x : α), Inseparable (f x) (g x)) → TendstoLocallyUniformly F g p
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Coequifibered.op : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor J C} {α : F ⟶ G},
  CategoryTheory.NatTrans.Coequifibered α → CategoryTheory.NatTrans.Equifibered (CategoryTheory.NatTrans.op α)
-- Mathlib.Algebra.Ring.Prod
RingHom.coe_snd : ∀ {R : Type u_1} {S : Type u_3} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S], ⇑(RingHom.snd R S) = Prod.snd
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_small : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.RespectsIso] [K.Small],
  (∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X),
      P f → ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) →
    (∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X),
        (∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) → P f) →
      P.IsLocalAtSource K
-- Mathlib.MeasureTheory.Function.Holder
MeasureTheory.Lp.add_smul : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q r : ENNReal}
  [hpqr : p.HolderTriple q r] [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : IsBoundedSMul 𝕜 E] (f : ↥(MeasureTheory.Lp 𝕜 p μ)) (g₁ g₂ : ↥(MeasureTheory.Lp E q μ)),
  f • (g₁ + g₂) = f • g₁ + f • g₂
-- Std.Sat.AIG.Basic
Std.Sat.AIG.CacheHit.hbound : ∀ {α : Type} {decls : Array (Std.Sat.AIG.Decl α)} {decl : Std.Sat.AIG.Decl α} (self : Std.Sat.AIG.CacheHit decls decl),
  self.idx < decls.size
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_sshiftRight' : ∀ {w : ℕ} {x y : BitVec w} {i : ℕ},
  (x.sshiftRight' y).getLsbD i = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb)
-- Mathlib.Data.ENNReal.Inv
ENNReal.zpow_lt_top : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → ∀ (n : ℤ), a ^ n < ⊤
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.symm_map_nhdsWithin_image : ∀ {𝕜 : 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) {x : H}
  {s : Set H}, Filter.map (↑I.symm) (nhdsWithin (↑I x) (↑I '' s)) = nhdsWithin x s
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
MeasureTheory.Measure.instIsMarkovKernelCondKernel : ∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (ρ : MeasureTheory.Measure (α × Ω)) [inst_2 : MeasureTheory.IsFiniteMeasure ρ],
  ProbabilityTheory.IsMarkovKernel ρ.condKernel
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_mul : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) (x y : R), ↑(x * y) = ↑x * ↑y
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.ofStabilizer.snoc_last : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {a : α} {n : ℕ}
  (x : Fin n ↪ ↥(SubMulAction.ofStabilizer G a)), (SubMulAction.ofStabilizer.snoc x) (Fin.last n) = a
-- Mathlib.RingTheory.Algebraic.Basic
/-- Bijection between algebra equivalences and algebra homomorphisms  -/
Algebra.IsAlgebraic.algEquivEquivAlgHom : (K : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing K] →
      [IsDomain K] →
        [inst_2 : Field L] →
          [inst_3 : Algebra K L] → [Module.IsTorsionFree K L] → [Algebra.IsAlgebraic K L] → (L ≃ₐ[K] L) ≃* (L →ₐ[K] L)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.mk.inj : ∀ {α : Type u} {β : Type v} {inst : TopologicalSpace α} {inst_1 : Zero β} {inst_2 : TopologicalSpace β}
  {toContinuousMap : C(α, β)} {zero_at_infty' : Filter.Tendsto toContinuousMap.toFun (Filter.cocompact α) (nhds 0)}
  {toContinuousMap_1 : C(α, β)}
  {zero_at_infty'_1 : Filter.Tendsto toContinuousMap_1.toFun (Filter.cocompact α) (nhds 0)},
  { toContinuousMap := toContinuousMap, zero_at_infty' := zero_at_infty' } =
      { toContinuousMap := toContinuousMap_1, zero_at_infty' := zero_at_infty'_1 } →
    toContinuousMap = toContinuousMap_1
-- Mathlib.Order.Disjoint
IsCompl.left_le_iff : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y z : α}, IsCompl x y → (x ≤ z ↔ Codisjoint z y)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`.
```
Vᵢⱼ ⟶ Uᵢ
 |      |
 ↓      ↓
 Uⱼ ⟶ X
```
 -/
AlgebraicGeometry.LocallyRingedSpace.GlueData.vPullbackConeIsLimit : (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) → (i j : D.J) → CategoryTheory.Limits.IsLimit (D.vPullbackCone i j)
-- Std.Data.HashMap.Basic
/-- Internal implementation detail of the hash map  -/
Std.HashMap.inner : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashMap α β → Std.DHashMap α fun x => β
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.fold_eq_foldl_toArray : ∀ {α : Type u} {δ : Type w} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {f : δ → α → β → δ} {init : δ},
  Std.DHashMap.Raw.fold f init ↑m = Array.foldl (fun a b => f a b.1 b.2) init (Std.DHashMap.Raw.Const.toArray ↑m)
-- Init.Data.SInt.Float
/-- Obtains a `Float` whose value is near the given `ISize`.

It will be exactly the value of the given `ISize` if such a `Float` exists. If no such `Float`
exists, the returned value will either be the smallest `Float` that is larger than the given value,
or the largest `Float` that is smaller than the given value.

This function does not reduce in the kernel.
 -/
ISize.toFloat : ISize → Float