mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Homotopy.HSpaces
unitInterval.qRight_zero_right : ∀ (t : ↑unitInterval), ↑(unitInterval.qRight (t, 0)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1
-- Mathlib.LinearAlgebra.Orientation
Orientation.map_positiveOrientation_of_isEmpty : ∀ {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] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  (ι : Type u_4) [inst_7 : IsEmpty ι] (f : M ≃ₗ[R] N), (Orientation.map ι f) positiveOrientation = positiveOrientation
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.image_add_right_Ioo : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] [inst_5 : DecidableEq α] (a b c : α),
  Finset.image (fun x => x + c) (Finset.Ioo a b) = Finset.Ioo (a + c) (b + c)
-- Mathlib.Topology.Constructions
instDiscreteTopologyMultiplicative : ∀ {X : Type u} [inst : TopologicalSpace X] [DiscreteTopology X], DiscreteTopology (Multiplicative X)
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkAtomCached.match_3.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (motive : Std.Sat.AIG α → Sort u_1) →
        (aig : Std.Sat.AIG α) →
          ((decls : Array (Std.Sat.AIG.Decl α)) →
              (cache : Std.Sat.AIG.Cache α decls) →
                (hdag : Std.Sat.AIG.IsDAG α decls) →
                  (hzero : 0 < decls.size) →
                    (hconst : decls[0] = Std.Sat.AIG.Decl.false) →
                      motive { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }) →
            motive aig
-- Init.Data.Sum.Basic
Sum.getLeft_inl : ∀ {α : Type u_1} {β : Type u_2} {x : α} (h : (Sum.inl x).isLeft = true), (Sum.inl x).getLeft h = x
-- Mathlib.FieldTheory.SeparableClosure
Field.sepDegree_le_rank : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Field.sepDegree F E ≤ Module.rank F E
-- Init.Data.List.Lemmas
List.dropLast_append_of_ne_nil : ∀ {α : Type u} {l l' : List α}, l ≠ [] → (l' ++ l).dropLast = l' ++ l.dropLast
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.unitIso_inv_hom_id_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X : C),
  CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (e.unit.app X) =
    CategoryTheory.CategoryStruct.id (e.inverse.obj (e.functor.obj X))
-- Mathlib.MeasureTheory.Integral.CircleIntegral
cauchyPowerSeries_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ) (w : ℂ),
  ((cauchyPowerSeries f c R n) fun x => w) =
    (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- If two chain maps become equal in the homotopy category, then they are homotopic.  -/
HomotopyCategory.homotopyOfEq : {ι : Type u_2} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            (f g : C ⟶ D) → (HomotopyCategory.quotient V c).map f = (HomotopyCategory.quotient V c).map g → Homotopy f g
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.add_prod_add : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  [inst_10 : ContinuousAdd M₂] [inst_11 : ContinuousAdd M₃] (f₁ f₂ : ContinuousMultilinearMap R M₁ M₂)
  (g₁ g₂ : ContinuousMultilinearMap R M₁ M₃), (f₁ + f₂).prod (g₁ + g₂) = f₁.prod g₁ + f₂.prod g₂
-- Mathlib.Analysis.Asymptotics.TVS
/-- Eta-expanded form of `Asymptotics.IsLittleOTVS.symm` -/
Asymptotics.IsLittleOTVS.fun_symm : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {g : α → F} [ContinuousNeg E] {f₁ f₂ : α → E},
  (fun i => f₁ i - f₂ i) =o[𝕜; l] g → (fun i => f₂ i - f₁ i) =o[𝕜; l] g
-- Init.Data.Rat.Lemmas
Rat.abs_eq_zero_iff : ∀ {x : ℚ}, x.abs = 0 ↔ x = 0
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.ctor.sizeOf_spec : ∀ (ctorName : Lean.Name) (us : List Lean.Level) (params : List Lean.Expr) (fields : List Lean.Meta.Match.Pattern),
  sizeOf (Lean.Meta.Match.Pattern.ctor ctorName us params fields) =
    1 + sizeOf ctorName + sizeOf us + sizeOf params + sizeOf fields
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.monoLift_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  [inst_2 : CategoryTheory.Mono f] {T : C} (g : T ⟶ Y)
  (hg : CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π f) = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.monoLift f g hg) f = g
-- Init.Data.SInt.Bitwise
Int16.toInt64_xor : ∀ (a b : Int16), (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.toSubspace_apply : ∀ {η : Type u_1} {α : Type u_2} {ι : Type u_3} (l : Combinatorics.Line (η → α) ι) (a : η → α) (ie : ι × η),
  ↑l.toSubspace a ie = ↑l a ie.1 ie.2
-- Mathlib.GroupTheory.Congruence.Defs
Con.coe_iInf : ∀ {M : Type u_1} [inst : Mul M] {ι : Sort u_4} (f : ι → Con M), ⇑(iInf f) = ⨅ i, ⇑(f i)
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Scheme.Etale.forget_mk : ∀ {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) [inst : AlgebraicGeometry.Etale f],
  (AlgebraicGeometry.Scheme.Etale.forget X).obj (AlgebraicGeometry.Scheme.Etale.mk f) = CategoryTheory.Over.mk f
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.TaggedPrepartition.distortion_unionComplToSubordinate : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I)
  (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → ↑(Set.Ioi 0)),
  (π₁.unionComplToSubordinate π₂ hU r).distortion = max π₁.distortion π₂.distortion
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.FunPropDecl.mk.injEq : ∀ (funPropName : Lean.Name) (path : Array Lean.Meta.DiscrTree.Key) (funArgId : ℕ) (funPropName_1 : Lean.Name)
  (path_1 : Array Lean.Meta.DiscrTree.Key) (funArgId_1 : ℕ),
  ({ funPropName := funPropName, path := path, funArgId := funArgId } =
      { funPropName := funPropName_1, path := path_1, funArgId := funArgId_1 }) =
    (funPropName = funPropName_1 ∧ path = path_1 ∧ funArgId = funArgId_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equation_of_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  P ≈ Q → (W'.Equation P ↔ W'.Equation Q)
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- **Alias** of `isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_le`.

---

**Prokhorov theorem**: Given a sequence of compact sets `Kₙ` and a sequence `uₙ` tending
to zero, the finite measures of mass at most `C` giving mass at most `uₙ` to the complement of `Kₙ`
form a compact set.  -/
isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le : ∀ {E : Type u_1} [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  {u : ℕ → NNReal} {K : ℕ → Set E} (C : NNReal),
  Filter.Tendsto u Filter.atTop (nhds 0) →
    (∀ (n : ℕ), IsCompact (K n)) → NormalSpace E ∨ Monotone K → IsCompact {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoLocallyUniformly.neg` -/
TendstoLocallyUniformly.fun_neg : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F : ι → X → α} {f : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l → TendstoLocallyUniformly (fun i i_1 => -F i i_1) (fun i => -f i) l
-- Mathlib.Algebra.Order.Ring.Abs
pow_eq_neg_one_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ},
  a ^ n = -1 ↔ a = -1 ∧ Odd n
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.ofEquivFun_equivFun : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι] (v : Module.Basis ι R M), Module.Basis.ofEquivFun v.equivFun = v
-- Mathlib.Analysis.Analytic.Order
/-- The order of an analytic function `f` at `z₀` is zero iff `f` does not vanish at `z₀`.  -/
AnalyticAt.analyticOrderAt_ne_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜}, AnalyticAt 𝕜 f z₀ → (analyticOrderAt f z₀ ≠ 0 ↔ f z₀ = 0)
-- Mathlib.Order.Sublattice
/-- The image of a sublattice along a monoid homomorphism is a sublattice.  -/
Sublattice.map : {α : Type u_2} →
  {β : Type u_3} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom α β → Sublattice α → Sublattice β
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.Γ_map_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y),
  AlgebraicGeometry.PresheafedSpace.Γ.map f.op = f.c.app (Opposite.op ⊤)
-- Lean.Elab.Command.Scope
/-- The current list of names for universe level variables to use for new declarations. This is managed by the `universe` command.  -/
Lean.Elab.Command.Scope.levelNames : Lean.Elab.Command.Scope → List Lean.Name
-- Mathlib.Topology.Category.Born
Born.instLargeCategory : CategoryTheory.LargeCategory Born
-- Mathlib.Analysis.Convex.BetweenList
List.sbtw_nil : ∀ (R : Type u_1) {V : Type u_2} (P : Type u_4) [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P], List.Sbtw R []
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.mul_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Mul β] [ContinuousMul β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : β), MeasureTheory.AEStronglyMeasurable (fun x => f x * c) μ
-- Mathlib.CategoryTheory.DifferentialObject
/-- The underlying object of a differential object.  -/
CategoryTheory.DifferentialObject.obj : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.DifferentialObject S C → C
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.bayesRisk_zero_left : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} [Nonempty 𝓨] (ℓ : Θ → 𝓨 → ENNReal) (π : MeasureTheory.Measure Θ),
  ProbabilityTheory.bayesRisk ℓ 0 π = 0
-- Mathlib.Data.ZMod.Basic
/-- **Alias** of the reverse direction of `ZMod.natCast_eq_one_iff_odd`. -/
Odd.natCast_zmod_two : ∀ {n : ℕ}, Odd n → ↑n = 1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftUnshift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ γ_1 : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'),
  γ = γ_1 →
    ∀ (n : ℤ) (hn : n + a = n') (T : CochainComplex.HomComplex.Triplet n), γ.leftUnshift n hn T = γ_1.leftUnshift n hn T
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.map_hom_inv_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D),
  CategoryTheory.CategoryStruct.comp (F.map e.hom) (F.map e.inv) = CategoryTheory.CategoryStruct.id (F.obj X)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDocumentSymbolAux : {Self : Type} → [Lean.FromJson Self] → Lean.FromJson (Lean.Lsp.DocumentSymbolAux Self)
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNorm_mulVec : ∀ {l : Type u_2} {m : Type u_3} {α : Type u_5} [inst : Fintype l] [inst_1 : Fintype m]
  [inst_2 : NonUnitalSeminormedRing α] (A : Matrix l m α) (v : m → α), ‖A.mulVec v‖ ≤ ‖A‖ * ‖v‖
-- Init.Data.Int.Linear
Int.Internal.Linear.of_var_eq : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (k : ℤ) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.of_var_eq_cert x k p = true →
    Int.Internal.Linear.Var.denote ctx x = k → Int.Internal.Linear.Poly.denote' ctx p = 0
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousWithinAt.lowerSemicontinuousWithinAt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {f : α → γ},
  ContinuousWithinAt f s x → LowerSemicontinuousWithinAt f s x
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
CategoryTheory.Adjunction.isLocalization_rightAdjoint : ∀ {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₁}
  [F.Full] [F.Faithful] (adj : F ⊣ G) (W : CategoryTheory.MorphismProperty C₁),
  W.IsInvertedBy G → W.functorCategory C₁ adj.counit → G.IsLocalization W
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
MeasurableEquiv.coe_toLp_symm : ∀ (p : ENNReal) (X : Type u_1) [inst : MeasurableSpace X], ⇑(MeasurableEquiv.toLp p X).symm = WithLp.ofLp
-- Lean.Elab.DocString
Lean.Doc.CodeSuggestion.mk : Lean.Name → Option String → Option String → Lean.Doc.CodeSuggestion
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.toSubring_one : ∀ {R : Type u_1} [inst : Ring R] (T : Subring R), Polynomial.toSubring 1 T ⋯ = 1
-- Init.Grind.Ordered.Module
/-- `a + c ≤ b + c` iff `a ≤ b`.  -/
Lean.Grind.OrderedAdd.add_le_left_iff : ∀ {M : Type u} {inst : HAdd M M M} {inst_1 : LE M} {inst_2 : Std.IsPreorder M} [self : Lean.Grind.OrderedAdd M]
  {a b : M} (c : M), a ≤ b ↔ a + c ≤ b + c
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
/-- A module has dimension 1 iff there is some `v : V` so `{v}` is a basis.

See also `Module.Basis.nonempty_unique_index_of_finrank_eq_one`  -/
finrank_eq_one_iff : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V] (ι : Type u_1) [Unique ι], Module.finrank K V = 1 ↔ Nonempty (Module.Basis ι K V)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.eq_C_iff : ∀ {K : Type u} [inst : Field K] (f : RatFunc K), (∃ c, f = RatFunc.C c) ↔ f.num.natDegree = 0 ∧ f.denom.natDegree = 0
-- Batteries.Data.List.Basic
List.dropSlice.eq_3 : ∀ {α : Type u_1} (x n : ℕ) (x_3 : α) (xs : List α), List.dropSlice n.succ x (x_3 :: xs) = x_3 :: List.dropSlice n x xs
-- Mathlib.Order.SymmDiff
hnot_symmDiff_self : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), symmDiff (￢a) a = ⊤
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
/-- The pullback given by the instance `HasPullbacks (Type u)` is isomorphic to the
explicit pullback object given by `PullbackObj`.
 -/
CategoryTheory.Limits.Types.pullbackIsoPullback : {X Y Z : Type u} →
  (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.pullback f g ≅ CategoryTheory.Limits.Types.PullbackObj f g
-- Mathlib.MeasureTheory.Measure.NullMeasurable
/-- Given a measure we can complete it to a (complete) measure on all null measurable sets.  -/
MeasureTheory.Measure.completion : {α : Type u_2} →
  {x : MeasurableSpace α} →
    (μ : MeasureTheory.Measure α) → MeasureTheory.Measure (MeasureTheory.NullMeasurableSpace α μ)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RocSliceData.mk : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.DTreeMap.Internal.Impl α β → Std.Roc α → Std.DTreeMap.Internal.RocSliceData α β
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.sat_true : ∀ {α : Type} {a : α → Bool}, Std.Tactic.BVDecide.BoolExpr.Sat a (Std.Tactic.BVDecide.BoolExpr.const true)
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- Balls are monotone in the radius.  -/
SimpleGraph.ball_mono : ∀ {V : Type u_1} {G : SimpleGraph V} {c : V} {r₁ r₂ : ℕ∞}, r₁ ≤ r₂ → G.ball c r₁ ⊆ G.ball c r₂
-- Init.Data.List.Impl
/-- Extracts the first `n` elements of `xs`, or the whole list if `n` is greater than `xs.length`.

`O(min n |xs|)`. This is a tail-recursive version of `List.take`, used at runtime.

Examples:
* `[a, b, c, d, e].takeTR 0 = []`
* `[a, b, c, d, e].takeTR 3 = [a, b, c]`
* `[a, b, c, d, e].takeTR 6 = [a, b, c, d, e]`
 -/
List.takeTR : {α : Type u_1} → ℕ → List α → List α
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestAttemptAllTac : Lean.Elab.Tactic.Try.TryTactic
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₁ → (t₁ ∩ t₂).getKeyD k fallback = fallback
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The composition of the inverse of the isomorphism `pullbackSpecIso R S T` (from the pullback of
`Spec S ⟶ Spec R` and `Spec T ⟶ Spec R` to `Spec (S ⊗[R] T)`) with the second projection is
the morphism `Spec (S ⊗[R] T) ⟶ Spec T` obtained by applying `Spec.map` to the ring morphism
`t ↦ 1 ⊗ₜ[R] t`.
 -/
AlgebraicGeometry.pullbackSpecIso_inv_snd : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).inv
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))) =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)
-- Mathlib.Data.Finset.Pi
Finset.pi_nonempty : ∀ {α : Type u_1} {β : α → Type u} {s : Finset α} {t : (a : α) → Finset (β a)} [inst : DecidableEq α],
  (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty
-- Mathlib.Data.PNat.Prime
PNat.gcd_comm : ∀ {m n : ℕ+}, m.gcd n = n.gcd m
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.constInsertMany : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {ρ : Type u_1} [inst : ForIn Id ρ (α × β)]
  {l : ρ} {t : Std.DTreeMap.Raw α (fun x => β) cmp}, t.WF → (Std.DTreeMap.Raw.Const.insertMany t l).WF
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
le_self_pow : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] {a : M} {n : ℕ}, 1 ≤ a → n ≠ 0 → a ≤ a ^ n
-- Lean.Class
/-- If `declName` is a class, return the positions of universe level parameters that only appear in output parameter types.  -/
Lean.getOutLevelParamPositions? : Lean.Environment → Lean.Name → Option (Array ℕ)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_eq_nil : ∀ {m n : ℤ}, n ≤ m → (m<...=n).toList = []
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haarMeasure_apply : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G} {s : Set G},
  MeasurableSet s →
    (MeasureTheory.Measure.haarMeasure K₀) s =
      (MeasureTheory.Measure.haar.haarContent K₀).outerMeasure s /
        (MeasureTheory.Measure.haar.haarContent K₀).measure ↑K₀
-- Init.Data.String.Slice
String.Slice.instHashable : Hashable String.Slice
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.coe_coe : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} (f : ↑(GenLoop N X x)), ⇑↑f = ⇑f
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.instCommRingUniversalFactorizationRing : {R : Type u_1} →
  [inst : CommRing R] →
    {n : ℕ} →
      (m k : ℕ) →
        (hn : n = m + k) →
          (p : Polynomial.MonicDegreeEq R n) → CommRing (Polynomial.UniversalFactorizationRing m k hn p)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instIsCancelMulOfMulOpposite : ∀ {M : Type u_1} [inst : Mul Mᵐᵒᵖ] [IsCancelMul Mᵐᵒᵖ], IsCancelMul Mᵈᵐᵃ
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsIntegralClosure : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  IsIntegralClosure (NumberField.RingOfIntegers L) (NumberField.RingOfIntegers K) L
-- Std.Time.DateTime.WallTime
/-- Subtracts a `Second.Offset` from the given `WallTime`.
 -/
Std.Time.WallTime.subSeconds : Std.Time.WallTime → Std.Time.Second.Offset → Std.Time.WallTime
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.setIntegral_condExpL2_indicator : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} {hm : m ≤ m0},
  MeasurableSet s →
    ∀ (ht : MeasurableSet t),
      μ s ≠ ⊤ →
        ∀ (hμt : μ t ≠ ⊤),
          ∫ (x : α) in s, ↑↑↑((MeasureTheory.condExpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 ht hμt 1)) x ∂μ =
            μ.real (t ∩ s)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.mul_apply : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Mul R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R] (f g : BoundedContinuousFunction α R) (x : α),
  (f * g) x = f x * g x
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instNonUnitalSubringClass : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A]
  [inst_3 : Star A], NonUnitalSubringClass (NonUnitalStarSubalgebra R A) A
-- Init.Data.List.Range
List.getElem?_range : ∀ {i n : ℕ}, i < n → (List.range n)[i]? = some i
-- Mathlib.CategoryTheory.Bicategory.Strict.Basic
/-- A bicategory is called `Strict` if the left unitors, the right unitors, and the associators are
isomorphisms given by equalities.
 -/
CategoryTheory.Bicategory.Strict : (B : Type u) → [CategoryTheory.Bicategory B] → Prop
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm : ∀ {ι : Type uι} [inst : Fintype ι] {𝕜 : Type u𝕜} [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type uE}
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_1}
  [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] (x : PiTensorProduct 𝕜 fun i => E i),
  ‖(PiTensorProduct.toDualContinuousMultilinearMap F) x‖ ≤ ‖x‖
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- `x` is semiconjugate to `y` by `a`, if `a * x = y * a`.  -/
SemiconjBy : {M : Type u_2} → [Mul M] → M → M → M → Prop
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.tensorEquiv_single_tmul_single : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] (m : M) (r₁ : R) (n : N) (r₂ : R),
  (AddMonoidAlgebra.tensorEquiv R) (AddMonoidAlgebra.single m r₁ ⊗ₜ[R] AddMonoidAlgebra.single n r₂) =
    AddMonoidAlgebra.single (m, n) (r₁ * r₂)
-- Mathlib.Topology.NhdsWithin
mem_nhdsWithin_iff_exists_mem_nhds_inter : ∀ {α : Type u_1} [inst : TopologicalSpace α] {t : Set α} {a : α} {s : Set α},
  t ∈ nhdsWithin a s ↔ ∃ u ∈ nhds a, u ∩ s ⊆ t
-- Mathlib.Algebra.Category.Grp.Limits
/-- The categorical kernel inclusion for `f : G ⟶ H`, as an object over `G`,
agrees with the `AddSubgroup.subtype` map.
 -/
AddCommGrpCat.kernelIsoKerOver : {G H : AddCommGrpCat} →
  (f : G ⟶ H) →
    CategoryTheory.Over.mk (CategoryTheory.Limits.kernel.ι f) ≅
      CategoryTheory.Over.mk (AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f).ker.subtype)