mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Widesubcategory
/-- The forgetful functor from an induced wide category to the original category.  -/
CategoryTheory.wideInducedFunctor : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₂} D] →
      (F : C → D) →
        (P : CategoryTheory.MorphismProperty D) →
          [inst_1 : P.IsMultiplicative] → CategoryTheory.Functor (CategoryTheory.InducedWideCategory D F P) D
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_const_on_unit_interval : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..a + 1, b = b
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- The composition of relative morphisms.  -/
SSet.RelativeMorphism.comp : {X Y Z : SSet} →
  {A : X.Subcomplex} →
    {B : Y.Subcomplex} →
      {φ : A.toSSet ⟶ B.toSSet} →
        SSet.RelativeMorphism A B φ →
          {C : Z.Subcomplex} →
            {ψ : B.toSSet ⟶ C.toSSet} →
              SSet.RelativeMorphism B C ψ →
                {φψ : A.toSSet ⟶ C.toSSet} → CategoryTheory.CategoryStruct.comp φ ψ = φψ → SSet.RelativeMorphism A C φψ
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_arrow_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h
-- Mathlib.Probability.Kernel.Category.Stoch
instIsDeterministicCarrierObjSFinKerStochHomHomHomWideSubcategoryOfDeterministicStoch : ∀ {X Y : Stoch} (κ : X ⟶ Y) [CategoryTheory.Deterministic κ], ProbabilityTheory.IsDeterministic κ.hom.hom
-- Mathlib.Logic.IsEmpty.Defs
/-- subtypes by false are false.  -/
Subtype.isEmpty_false : ∀ {α : Sort u}, IsEmpty { _a // False }
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.ofVar : Lean.Grind.CommRing.Var → Lean.Grind.CommRing.Poly
-- Mathlib.Order.Filter.CountablyGenerated
Filter.isCountablyGenerated_top : ∀ {α : Type u_1}, ⊤.IsCountablyGenerated
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept : ∀ (L : PeriodPair) (l₀ x : ℂ) (r : NNReal),
  0 < r →
    Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ →
      HasFPowerSeriesOnBall (L.weierstrassPExcept l₀) (L.weierstrassPExceptSeries l₀ x) x ↑r
-- Mathlib.RingTheory.Localization.Finiteness
Module.Finite.instFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors : ∀ {A : Type u_1} {C : Type u_2} [inst : CommRing A] [inst_1 : CommRing C] [inst_2 : Algebra A C] [Module.Finite A C],
  Module.Finite (FractionRing A) (Localization (Algebra.algebraMapSubmonoid C (nonZeroDivisors A)))
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRupAdd_insert : ∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (f : σ) (c : β),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c)
-- Lean.Server.CodeActions.Provider
/-- Main recursion for `findTactic?`. This takes a `stack` context and a root syntax `stx`,
and returns the best `FindTacticResult` it can find. It returns `none` (abort) if two or more
results are found, and `some none` (none yet) if no results are found.  -/
_private.Lean.Server.CodeActions.Provider.0.Lean.CodeAction.findTactic?.go : (String.Pos.Raw → Bool) →
  Lean.Syntax.Range →
    Lean.Syntax.Stack →
      Lean.Syntax → optParam (Option String.Pos.Raw) none → Option (Option Lean.CodeAction.FindTacticResult)
-- Mathlib.AlgebraicTopology.SimplicialCategory.Basic
/-- Abbreviation for the enriched hom of a simplicial category.  -/
CategoryTheory.SimplicialCategory.sHom : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.SimplicialCategory C] → C → C → SSet
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_Iio : ∀ {α : Type u_1} [inst : Preorder α] [LocallyFiniteOrderBot α] (a : α), (Set.Iio a).Finite
-- Mathlib.RingTheory.Coalgebra.Basic
DFinsupp.comul_single : ∀ (R : Type u) (ι : Type v) (A : ι → Type w) [inst : DecidableEq ι] [inst_1 : CommSemiring R]
  [inst_2 : (i : ι) → AddCommMonoid (A i)] [inst_3 : (i : ι) → Module R (A i)]
  [inst_4 : (i : ι) → CoalgebraStruct R (A i)] (i : ι) (a : A i),
  (CoalgebraStruct.comul fun₀ | i => a) =
    (TensorProduct.map (DFinsupp.lsingle i) (DFinsupp.lsingle i)) (CoalgebraStruct.comul a)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
CategoryTheory.Adjunction.hasRightCalculusOfFractions : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : F ⊣ G) (W : CategoryTheory.MorphismProperty C₁) [W.IsMultiplicative],
  W.IsInvertedBy G → W.functorCategory C₁ adj.counit → W.HasRightCalculusOfFractions
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.cofan_inj_epi_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  {Δ₁ Δ₂ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂)
  [inst_1 : CategoryTheory.Epi p.unop],
  CategoryTheory.CategoryStruct.comp ((s.cofan Δ₁).inj A) (X.map p) = (s.cofan Δ₂).inj (A.epiComp p)
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff_neg : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : NegZeroClass R] {x : HahnSeries Γ R} {a : Γ},
  (-x).coeff a = -x.coeff a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.slope_of_Y_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  x₁ = x₂ →
    y₁ ≠ W.negY x₂ y₂ → W.slope x₁ x₂ y₁ y₂ = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) {n : ℕ},
  AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ 0) = K.d (n + 1) n
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Submodule.reflection_mem_subspace_eq_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] {x : E}, x ∈ K → K.reflection x = x
-- Batteries.Data.Vector.Lemmas
Vector.get_replicate : ∀ {α : Type u_1} (n : ℕ) (a : α) (i : Fin n), (Vector.replicate n a).get i = a
-- Mathlib.Control.Traversable.Basic
/-- A transformation between applicative functors.  It is a natural
transformation such that `app` preserves the `Pure.pure` and
`Functor.map` (`<*>`) operations. See
`ApplicativeTransformation.preserves_map` for naturality.  -/
ApplicativeTransformation : (F : Type u → Type v) → [Applicative F] → (G : Type u → Type w) → [Applicative G] → Type (max (u + 1) v w)
-- Mathlib.Analysis.Normed.Ring.Lemmas
/-- Multiplication by a nonzero element `a` on the left, as a `Dilation` of a ring with a strictly
multiplicative norm.  -/
Dilation.mulLeft : {α : Type u_1} → [inst : NonUnitalNormedRing α] → [NormMulClass α] → (a : α) → a ≠ 0 → α →ᵈ α
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂).get! k = if k ∈ m₂ then m₁.get! k else default
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a : α}, t.contains a = (t.getKey? a).isSome
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertMany_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α},
  Std.DTreeMap.Internal.Impl.Const.get? (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k =
    (List.findSomeRev?
          (fun x =>
            match x with
            | (a, b) => if compare a k = Ordering.eq then some b else none)
          l).or
      (Std.DTreeMap.Internal.Impl.Const.get? t k)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Mathlib.Meta.Positivity.log_nz_of_isNNRat : ∀ {e : ℝ} {d n : ℕ},
  Mathlib.Meta.NormNum.IsNNRat e n d → decide (0 < ↑n / ↑d) = true → decide (↑n / ↑d < 1) = true → Real.log e ≠ 0
-- Mathlib.Algebra.CharZero.Quotient
QuotientAddGroup.zmultiples_zsmul_eq_zsmul_iff : ∀ {R : Type u_1} [inst : DivisionRing R] [CharZero R] {p : R} {ψ θ : R ⧸ AddSubgroup.zmultiples p} {z : ℤ},
  z ≠ 0 → (z • ψ = z • θ ↔ ∃ k, ψ = θ + ↑(↑k • (p / ↑z)))
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.coe_comp : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : AddMonoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (g : B →ₜ+ C) (f : A →ₜ+ B),
  ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.mem_uIoc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ∈ Set.uIoc b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₁.comp.injEq : ∀ (e : Lean.Expr) (a a_1 : Mathlib.Tactic.BicategoryLike.Mor₁) (e_1 : Lean.Expr)
  (a_2 a_3 : Mathlib.Tactic.BicategoryLike.Mor₁),
  (Mathlib.Tactic.BicategoryLike.Mor₁.comp e a a_1 = Mathlib.Tactic.BicategoryLike.Mor₁.comp e_1 a_2 a_3) =
    (e = e_1 ∧ a = a_2 ∧ a_1 = a_3)
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
OrderIso.cof_congr : ∀ {α γ : Type u} [inst : Preorder α] [inst_1 : Preorder γ] (f : α ≃o γ), Order.cof α = Order.cof γ
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
Lean.Meta.Grind.Arith.Linear.isSubInst : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr → Bool
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Create a reference for a `RefinedDiscrTree` for current module declarations.
 -/
Lean.Meta.RefinedDiscrTree.createModuleTreeRef : {α : Type} →
  (Lean.Name →
      Lean.ConstantInfo →
        Lean.MetaM (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))) →
    Lean.MetaM (Lean.Meta.RefinedDiscrTree.ModuleDiscrTreeRef α)
-- Mathlib.Topology.UnitInterval
unitInterval.coe_ne_one : ∀ {x : ↑unitInterval}, ↑x ≠ 1 ↔ x ≠ 1
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
ConcaveOn.condExp_map_le_trim : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} {mE : MeasurableSpace E}
  [BorelSpace E] (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)],
  ConcaveOn ℝ s φ →
    UpperSemicontinuousOn φ s →
      MeasureTheory.StronglyMeasurable φ →
        (∀ᵐ (a : α) ∂μ, f a ∈ s) →
          IsClosed s →
            MeasureTheory.Integrable f μ → MeasureTheory.Integrable (φ ∘ f) μ → μ[φ ∘ f | m] ≤ᵐ[μ.trim hm] φ ∘ μ[f | m]
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiff_of_contMDiff_inl : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {E' : Type u_17}
  [inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_18} [inst_8 : TopologicalSpace H']
  {J : ModelWithCorners 𝕜 E' H'} {N : Type u_20} {N' : Type u_21} [inst_9 : TopologicalSpace N]
  [inst_10 : TopologicalSpace N'] [inst_11 : ChartedSpace H' N] [inst_12 : ChartedSpace H' N'] {f : M → N},
  ContMDiff I J n (Sum.inl ∘ f) → ContMDiff I J n f
-- Init.Data.String.PosRaw
String.rawEndPos_empty : "".rawEndPos = 0
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.surjectiveOnStalks_iff_forall_maximal : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S},
  f.SurjectiveOnStalks ↔
    ∀ (I : Ideal S) (x : I.IsMaximal), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor_obj_X₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c),
  ((HomologicalComplex.shortComplexFunctor C c i).obj K).X₁ = K.X (c.prev i)
-- Mathlib.Order.Filter.Bases.Finite
Filter.HasBasis.iInf' : ∀ {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop}
  {s : (i : ι) → ι' i → Set α},
  (∀ (i : ι), (l i).HasBasis (p i) (s i)) →
    (⨅ i, l i).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i)) fun If => ⋂ i ∈ If.1, s i (If.2 i)
-- Init.Data.Array.Basic
/-- Applies a monadic function that returns an `Option` to each element of an array, collecting the
non-`none` values.

Only elements from `start` (inclusive) to `stop` (exclusive) are considered. Elements outside that
range are discarded. By default, the entire array is considered.

Example:
```lean example
#eval #[1, 2, 5, 2, 7, 7].filterMapM fun x => do
  IO.println s!"Examining {x}"
  if x > 2 then return some (2 * x)
  else return none
```
```output
Examining 1
Examining 2
Examining 5
Examining 2
Examining 7
Examining 7
```
```output
#[10, 14, 14]
```
 -/
Array.filterMapM : {α : Type u} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} → [Monad m] → (α → m (Option β)) → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → m (Array β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_modify_self : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ [Inhabited α] {k : α} {f : β → β} {hc : k ∈ Std.DTreeMap.Internal.Impl.Const.modify k f t},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).getKey k hc = k
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `extractTacticData tree` extracts tactic information from an `InfoTree`,
including the `ContextInfo` needed to run `MetaM` computations.
 -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.extractTacticData : Lean.Elab.InfoTree → Array Mathlib.Linter.Flexible.TacticData✝
-- Mathlib.RingTheory.Localization.BaseChange
/-- `S⁻¹M ⊗[R] N = S⁻¹(M ⊗[R] N)`.  -/
IsLocalizedModule.rTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_2) [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {M' : Type u_4} [inst_5 : AddCommMonoid M'] [inst_6 : Module R M']
  [inst_7 : Module A M'] [inst_8 : IsScalarTower R A M'] (S : Submonoid A) {N : Type u_7} [inst_9 : AddCommMonoid N]
  [inst_10 : Module R N] [inst_11 : Module A M] [inst_12 : IsScalarTower R A M] (g : M →ₗ[A] M')
  [h : IsLocalizedModule S g], IsLocalizedModule S ((TensorProduct.AlgebraTensorModule.rTensor R N) g)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.δ_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (i : Fin (n + 2))
  (x : CategoryTheory.ComposableArrows C (n + 1)) (j : Fin (n + 1)),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) i)) x).obj j =
    x.obj (i.succAbove j)
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.Embedding.mk.congr_simp : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (toEmbedding toEmbedding_1 : M ↪ N) (e_toEmbedding : toEmbedding = toEmbedding_1)
  (map_fun' :
    ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
      toEmbedding.toFun (FirstOrder.Language.Structure.funMap f x) =
        FirstOrder.Language.Structure.funMap f (toEmbedding.toFun ∘ x))
  (map_rel' :
    ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
      FirstOrder.Language.Structure.RelMap r (toEmbedding.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x),
  { toEmbedding := toEmbedding, map_fun' := map_fun', map_rel' := map_rel' } =
    { toEmbedding := toEmbedding_1, map_fun' := ⋯, map_rel' := ⋯ }
-- Init.PropLemmas
Decidable.not_not : ∀ {p : Prop} [Decidable p], ¬¬p ↔ p
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst_1 : Bornology β] (f : LocallyBoundedMap α β) (f' : α → β)
  (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S` is invertible, then
there is a linear map `lift g ∘ mkLinearMap = g`.
 -/
LocalizedModule.lift_comp : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M''] [inst_3 : Module R M] [inst_4 : Module R M''] (g : M →ₗ[R] M'')
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)),
  LocalizedModule.lift S g h ∘ₗ LocalizedModule.mkLinearMap S M = g
-- Mathlib.Algebra.Quaternion
Quaternion.coe_ratCast : ∀ {R : Type u_1} [inst : Field R] (q : ℚ), ↑↑q = ↑q
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} (h' : k ∈ Std.ExtDHashMap.filterMap f m),
  (f k (m.get k ⋯)).isSome = true
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.instHasOfPrecompPropertyLocalEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C}
  (W : CategoryTheory.MorphismProperty C), P.localEpi.HasOfPrecompProperty W
-- Mathlib.Algebra.Group.Hom.Defs
iterate_map_one : ∀ {M : Type u_10} {F : Type u_11} [inst : One M] [inst_1 : FunLike F M M] [OneHomClass F M M] (f : F) (n : ℕ),
  (⇑f)^[n] 1 = 1
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- The category of cones on `F` is just the comma category `(Δ ↓ F)`, where `Δ` is the constant
functor.  -/
CategoryTheory.Limits.Cone.equivCostructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) →
          CategoryTheory.Limits.Cone F ≌ CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F
-- Lean.Meta.Structure
Lean.Meta.StructProjDecl.mk.inj : ∀ {ref : Lean.Syntax} {projName : Lean.Name} {paramInfoOverrides : List (Option Lean.BinderInfo)} {ref_1 : Lean.Syntax}
  {projName_1 : Lean.Name} {paramInfoOverrides_1 : List (Option Lean.BinderInfo)},
  { ref := ref, projName := projName, paramInfoOverrides := paramInfoOverrides } =
      { ref := ref_1, projName := projName_1, paramInfoOverrides := paramInfoOverrides_1 } →
    ref = ref_1 ∧ projName = projName_1 ∧ paramInfoOverrides = paramInfoOverrides_1
-- Init.Data.SInt.Basic
/-- Constructs an `Int16` from an `Int`, clamping if the value is too small or too large.  -/
Int16.ofIntTruncate : ℤ → Int16
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- The pairing between a submodule `W` of a dual module `Dual R M` and the quotient of
`M` by the coannihilator of `W`, which is always nondegenerate.  -/
Submodule.quotDualCoannihilatorToDual : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (W : Submodule R (Module.Dual R M)) → M ⧸ W.dualCoannihilator →ₗ[R] Module.Dual R ↥W
-- Mathlib.Combinatorics.Quiver.Schreier
/-- Wraps a vertex of the acted-upon type into the Schreier graph.  -/
Quiver.SchreierGraph.ofVertex : {V : Type u_1} → {M : Type u_2} → [inst : SMul M V] → {S : Type u_3} → {_ι : S → M} → V → Quiver.SchreierGraph V _ι
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePushoutShapeOpEquiv_functor : ∀ (J : Type w), (CategoryTheory.Limits.widePushoutShapeOpEquiv J).functor = CategoryTheory.Limits.widePushoutShapeUnop J
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
summable_norm_sum_mul_antidiagonal_of_summable_norm : ∀ {R : Type u_1} [inst : NormedRing R] {f g : ℕ → R},
  (Summable fun x => ‖f x‖) →
    (Summable fun x => ‖g x‖) → Summable fun n => ‖∑ kl ∈ Finset.HasAntidiagonal.antidiagonal n, f kl.1 * g kl.2‖
-- Qq.SortLocalDecls
Qq.SortLocalDecls.State.visited : Qq.SortLocalDecls.State → Lean.NameSet
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticOnNhd.aeval_polynomial : ∀ {𝕜 : Type u_1} {E : Type u_2} {A : Type u_3} {B : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : CommSemiring A] {s : Set E}
  [inst_4 : NormedRing B] [inst_5 : NormedAlgebra 𝕜 B] [inst_6 : Algebra A B] {f : E → B},
  AnalyticOnNhd 𝕜 f s → ∀ (p : Polynomial A), AnalyticOnNhd 𝕜 (fun x => (Polynomial.aeval (f x)) p) s
-- Mathlib.Topology.Irreducible
/-- If `f : X → Y` is continuous, open, and has irreducible fibers, then it induces an
bijection between irreducible components  -/
irreducibleComponentsEquivOfIsPreirreducibleFiber : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (f : X → Y) →
          Continuous f →
            IsOpenMap f →
              (∀ (x : Y), IsPreirreducible (f ⁻¹' {x})) →
                Function.Surjective f → ↑(irreducibleComponents Y) ≃o ↑(irreducibleComponents X)
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
OrderMonoidWithZeroHom.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] (toMonoidWithZeroHom toMonoidWithZeroHom_1 : α →*₀ β)
  (e_toMonoidWithZeroHom : toMonoidWithZeroHom = toMonoidWithZeroHom_1)
  (monotone' : Monotone (↑toMonoidWithZeroHom).toFun),
  { toMonoidWithZeroHom := toMonoidWithZeroHom, monotone' := monotone' } =
    { toMonoidWithZeroHom := toMonoidWithZeroHom_1, monotone' := ⋯ }
-- Mathlib.CategoryTheory.Category.KleisliCat
CategoryTheory.KleisliCat.comp_def : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] (α β γ : CategoryTheory.KleisliCat m) (xs : α ⟶ β) (ys : β ⟶ γ) (a : α),
  CategoryTheory.CategoryStruct.comp xs ys a = xs a >>= ys
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictPeriods_SL2Z : (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods = AddSubgroup.zmultiples 1
-- Mathlib.Logic.Relation
Relation.flip_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {p : β → γ → Prop},
  flip (Relation.Comp r p) = Relation.Comp (flip p) (flip r)
-- Init.SizeOfLemmas
UInt64.sizeOf : ∀ (a : UInt64), sizeOf a = a.toNat + 3
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntryD_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α}
  {fallback : (a : α) × β a},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → Std.Internal.List.getEntryD a fallback l = Std.Internal.List.getEntryD a fallback l'
-- Mathlib.Data.Finmap
Finmap.empty_toFinmap : ∀ {α : Type u} {β : α → Type v}, ∅.toFinmap = ∅
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mapOrderEmbedding.congr_simp : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f f_1 : M →ₗ⁅R,L⁆ M'} (e_f : f = f_1)
  (hf : Function.Injective ⇑f), LieSubmodule.mapOrderEmbedding hf = LieSubmodule.mapOrderEmbedding ⋯
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabLink.name : Lean.Doc.ElabLink✝ → Lean.StrLit