mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
norm_cfc_le : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜}
  {a : A} {c : ℝ}, 0 ≤ c → (∀ x ∈ spectrum 𝕜 a, ‖f x‖ ≤ c) → ‖cfc f a‖ ≤ c
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : M` and a Localization map `F : M →* N` away from `x`, `invSelf` is `(F x)⁻¹`.  -/
Submonoid.LocalizationMap.AwayMap.invSelf : {M : Type u_1} →
  [inst : CommMonoid M] → {N : Type u_2} → [inst_1 : CommMonoid N] → (x : M) → Submonoid.LocalizationMap.AwayMap x N → N
-- Lean.Expr
Lean.instInhabitedMVarId : Inhabited Lean.MVarId
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.least?_eq_some : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLeast? α] [hn : Nonempty α],
  Std.PRange.least? = some Std.PRange.UpwardEnumerable.least
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Stream.readAll.loop : {m : Type → Type} →
  [Monad m] →
    [MonadExceptOf IO.Error m] →
      [Std.Http.Body.Stream.NextChunk m] → Std.Http.Body.Stream → Option UInt64 → ByteArray → m ByteArray
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piLeft.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (N : Type u_3) [inst_1 : AddCommMonoid N] [inst_2 : Module R N] {ι : Type u_4}
  (M : ι → Type u_5) [inst_3 : (i : ι) → AddCommMonoid (M i)] [inst_4 : (i : ι) → Module R (M i)] [inst_5 : Fintype ι]
  [inst_6 : DecidableEq ι],
  TensorProduct.piLeft R N M =
    ((TensorProduct.comm R ((i : ι) → M i) N).trans (TensorProduct.piRight R R N M)).trans
      (LinearEquiv.piCongrRight fun x => TensorProduct.comm R N (M x))
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
IsHomogeneous.subsemiringClosure_of_isHomogeneousElem : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜] {s : Set A},
  (∀ x ∈ s, SetLike.IsHomogeneousElem 𝒜 x) → DirectSum.SetLike.IsHomogeneous 𝒜 (Subsemiring.closure s)
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
/-- `abs : ℤ → ℤ` is an admissible absolute value.  -/
AbsoluteValue.absIsAdmissible : AbsoluteValue.abs.IsAdmissible
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.centerCongr.eq_1 : ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (e : M ≃+ N),
  AddSubmonoid.centerCongr e = AddSubsemigroup.centerCongr e
-- Mathlib.Analysis.Normed.Group.InfiniteSum
/-- Quantitative result associated to the direct comparison test for series: If `∑' i, g i` is
summable, and for all `i`, `‖f i‖₊ ≤ g i`, then `‖∑' i, f i‖₊ ≤ ∑' i, g i`. Note that we
do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
space.  -/
tsum_of_nnnorm_bounded : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E} {g : ι → NNReal} {a : NNReal},
  HasSum g a → (∀ (i : ι), ‖f i‖₊ ≤ g i) → ‖∑' (i : ι), f i‖₊ ≤ a
-- Mathlib.CategoryTheory.Sites.Sieves
/-- If a morphism `h` satisfies `Presieve.bind S R h`, this is a choice of a structure
in `BindStruct S R h`.  -/
CategoryTheory.Presieve.bind.bindStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {S : CategoryTheory.Presieve X} →
        {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} →
          {Z : C} → {h : Z ⟶ X} → S.bind R h → S.BindStruct R h
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.addUnits_ofAddUnits_eq : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)), S.ofAddUnits.addUnits = S
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.instBEqAssignment.beq : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Std.Tactic.BVDecide.LRAT.Internal.Assignment → Bool
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.epi_homologyMap_of_epi_cyclesMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [CategoryTheory.Epi (CategoryTheory.ShortComplex.cyclesMap φ)],
  CategoryTheory.Epi (CategoryTheory.ShortComplex.homologyMap φ)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.lift.tmul : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} (x : M) (y : N),
  (TensorProduct.lift f') (x ⊗ₜ[R] y) = (f' x) y
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.eqIgnoreAsciiCase.go : String.Slice → String.Pos.Raw → String.Slice → String.Pos.Raw → Bool
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.range_eq_univ : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), Set.range ⇑e = Set.univ
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.find?_char_eq_some_iff_splits : ∀ {c : Char} {s : String} {pos : s.Pos},
  s.find? c = some pos ↔ ∃ t u, pos.Splits t (String.singleton c ++ u) ∧ c ∉ t.toList
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.eq_factors_of_eq_counts : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {a b : Associates α},
  a ≠ 0 → b ≠ 0 → (∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors) → a.factors = b.factors
-- Mathlib.Tactic.Lift
instCanLiftIntNatCastLeOfNat : CanLift ℤ ℕ (fun n => ↑n) fun x => 0 ≤ x
-- Mathlib.Order.SuccPred.Basic
Order.Ioc_subset_Ioo_succ_right : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Ioc a b ⊆ Set.Ioo a (Order.succ b)
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
/-- If the comparison morphism `colimit (F ⋙ G) ⟶ G.obj (colimit F)` is an isomorphism, then `G`
preserves colimits of `F`.  -/
CategoryTheory.preservesColimit_of_isIso_post : ∀ {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} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.HasColimit F]
  [inst_4 : CategoryTheory.Limits.HasColimit (F.comp G)]
  [CategoryTheory.IsIso (CategoryTheory.Limits.colimit.post F G)], CategoryTheory.Limits.PreservesColimit F G
-- Mathlib.Topology.Algebra.InfiniteSum.Order
prod_le_hasProd : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} [L.NeBot] [L.LeAtTop] (s : Finset ι),
  (∀ i ∉ s, 1 ≤ f i) → HasProd f a L → ∏ i ∈ s, f i ≤ a
-- Std.Time.Date.Unit.Month
/-- The ordinal value representing the month of September.
 -/
Std.Time.Month.Ordinal.september : Std.Time.Month.Ordinal
-- Lean.Data.Options
_private.Lean.Data.Options.0.Lean.Option.updateBool : Lean.Options → Lean.Name → Bool → Lean.Options
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.out_top : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M], ⊤.out = 0
-- Lean.Parser.Basic
Lean.Parser.identEqFn : Lean.Name → Lean.Parser.ParserFn
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.div : ∀ {α : Type u} [inst : DivisionMonoid α] {a b : α}, IsUnit a → IsUnit b → IsUnit (a / b)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_obj_left : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).functor.obj X).left = X.left
-- Lean.Meta.Tactic.Cases
/-- Applies `cases` to any hypothesis of the form `h : r = s`.
 -/
Lean.MVarId.substEqs : Lean.MVarId → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The center is commutative.  -/
Subsemiring.center.commSemiring : {R : Type u_1} → [inst : Semiring R] → CommSemiring ↥(Subsemiring.center R)
-- Init.Data.ToString.Name
_private.Init.Data.ToString.Name.0.Lean.Name.needsNoEscapeAscii : (s : String) → s.utf8ByteSize > 0 → Bool
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLT?.go.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.gt) (h_2 : (x : Ordering) → motive x),
  (match Ordering.gt with
    | Ordering.gt => h_1 ()
    | x => h_2 x) =
    h_1 ()
-- Lean.Parser.Basic
Lean.Parser.TokenMap.insert : {α : Type} → Lean.Parser.TokenMap α → Lean.Name → α → Lean.Parser.TokenMap α
-- Std.Tactic.BVDecide.LRAT.Internal.Actions
Std.Tactic.BVDecide.LRAT.Internal.intToLiteral : {n : ℕ} → ℤ → Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given open range as an array in ascending order.
 -/
Std.Roo.toArray : {α : Type u} →
  [inst : LT α] →
    [DecidableLT α] →
      [inst_2 : Std.PRange.UpwardEnumerable α] →
        [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxo.IsAlwaysFinite α] → Std.Roo α → Array α
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereoInvFunAux_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (w : E),
  stereoInvFunAux v w = (‖w‖ ^ 2 + 4)⁻¹ • (4 • w + (‖w‖ ^ 2 - 4) • v)
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.X_add_C_scaleRoots : ∀ {R : Type u_1} [inst : Semiring R] (r s : R),
  (Polynomial.X + Polynomial.C r).scaleRoots s = Polynomial.X + Polynomial.C (r * s)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLTD_eq_getD_getKeyLT? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k fallback : α},
  Std.DTreeMap.Internal.Impl.getKeyLTD k t fallback = (Std.DTreeMap.Internal.Impl.getKeyLT? k t).getD fallback
-- Mathlib.Topology.MetricSpace.Equicontinuity
/-- For a family of functions to a (pseudo) metric spaces, a convenient way to prove
equicontinuity at a point is to show that all of the functions share a common *local* continuity
modulus.  -/
Metric.equicontinuousAt_of_continuity_modulus : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : TopologicalSpace β] {x₀ : β}
  (b : β → ℝ),
  Filter.Tendsto b (nhds x₀) (nhds 0) →
    ∀ (F : ι → β → α), (∀ᶠ (x : β) in nhds x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x) → EquicontinuousAt F x₀
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_subst : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} {n : ℕ}
  {φ : L.BoundedFormula α n} {tf : α → L.Term β} {v : β → M} {xs : Fin n → M},
  (φ.subst tf).Realize v xs ↔ φ.Realize (fun a => FirstOrder.Language.Term.realize v (tf a)) xs
-- Mathlib.Analysis.Calculus.FDeriv.Pow
HasFDerivAt.pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {f' : E →L[𝕜] 𝔸}
  {x : E},
  HasFDerivAt f f' x →
    ∀ (n : ℕ), HasFDerivAt (f ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') x
-- Mathlib.Algebra.Algebra.Prod
AlgHom.prodEquiv_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : (A →ₐ[R] B) × (A →ₐ[R] C)), AlgHom.prodEquiv f = f.1.prod f.2
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.neg : ∀ {A : Type u_1} [inst : Field A] {B : Type u_3} [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B),
  minpoly A (-x) = (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-Polynomial.X)
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
/-- The ideal corresponding to the class of `Q ∈ ℤ[X]` modulo `p` via
`NumberField.Ideal.primesOverSpanEquivMonicFactorsMod` is spanned by `p` and `Q(θ)`.
 -/
NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span : ∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [inst_1 : Fact (Nat.Prime p)]
  [inst_2 : NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial ℤ}
  (hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p),
  ↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) =
    Ideal.span {↑p, (Polynomial.aeval θ) Q}
-- Lean.Server.Rpc.Basic
Lean.Lsp.RpcWireFormat.v0.sizeOf_spec : sizeOf Lean.Lsp.RpcWireFormat.v0 = 1
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.monotone_u_comp_l : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → Monotone (u ∘ l)
-- Mathlib.Order.Interval.Set.Basic
Set.decidableMemIco : {α : Type u_1} →
  [inst : Preorder α] → {a b x : α} → [Decidable (a ≤ x)] → [Decidable (x < b)] → Decidable (x ∈ Set.Ico a b)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.add : ℤ → Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly
-- Mathlib.Computability.TuringMachine.Config
/-- The `stepNormal` function respects the `then k'` homomorphism. Note that this is an exact
equality, not a simulation; the original and embedded machines move in lock-step until the
embedded machine reaches the halt state.  -/
Turing.ToPartrec.stepNormal_then : ∀ (c : Turing.ToPartrec.Code) (k k' : Turing.ToPartrec.Cont) (v : List ℕ),
  Turing.ToPartrec.stepNormal c (k.then k') v = (Turing.ToPartrec.stepNormal c k v).then k'
-- Mathlib.MeasureTheory.SpecificCodomains.Pi
MeasureTheory.integrable_pi_iff : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {ι : Type u_2} [inst : Fintype ι]
  {E : ι → Type u_3} [inst_1 : (i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i},
  MeasureTheory.Integrable f μ ↔ ∀ (i : ι), MeasureTheory.Integrable (fun x => f x i) μ
-- Mathlib.Analysis.Fourier.ZMod
ZMod.invDFT_def' : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Ψ : ZMod N → E),
  ZMod.dft.symm Ψ = fun k => (↑N)⁻¹ • ZMod.dft Ψ (-k)
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of `Finset.Ico_sdiff_Ioo_self`. -/
Finset.Ico_diff_Ioo_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a < b → Finset.Ico a b \ Finset.Ioo a b = {a}
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.checkKind : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Parenthesizer
-- Lean.CoreM
Lean.Core.instMonadCoreM : Monad Lean.CoreM
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.functorToCore_map_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : Type u₂} [inst_1 : CategoryTheory.Groupoid G]
  (F : CategoryTheory.Functor G C) {X Y : G} (f : X ⟶ Y),
  ((CategoryTheory.Core.functorToCore F).map f).iso.inv = CategoryTheory.inv (F.map f)
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- Recursor for `OnePoint` using the preferred forms `∞` and `↑x`.  -/
OnePoint.rec : {X : Type u_1} → {C : OnePoint X → Sort u_3} → C OnePoint.infty → ((x : X) → C ↑x) → (z : OnePoint X) → C z
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.of_null : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  μ s = 0 → MeasureTheory.NullMeasurableSet s μ
-- Mathlib.Order.Disjoint
Disjoint.le_bot : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b → a ⊓ b ≤ ⊥
-- Init.Data.Nat.Lemmas
Nat.mod_two_not_eq_zero : ∀ {n : ℕ}, ¬n % 2 = 0 ↔ n % 2 = 1
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sSup_add : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M] (s t : Set M),
  sSup (s + t) = sSup s + sSup t
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.unop_eq_bot : ∀ {G : Type u_2} [inst : AddGroup G] {S : AddSubgroup Gᵃᵒᵖ}, S.unop = ⊥ ↔ S = ⊥
-- Mathlib.Topology.Separation.Basic
t1Space_iff_continuous_cofinite_of : ∀ {X : Type u_1} [inst : TopologicalSpace X], T1Space X ↔ Continuous ⇑CofiniteTopology.of
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.coe_compl : ∀ {V : Type u} {G : SimpleGraph V} [inst : Finite V] (G' : G.Finsubgraph), ↑G'ᶜ = (↑G')ᶜ
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.instWeakEquivalenceP₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A)
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty]
  [(HomotopicalAlgebra.weakEquivalences C).ContainsIdentities], HomotopicalAlgebra.WeakEquivalence P.p₀
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.instInhabitedDefaultBackwardSearcher : {a : Type} →
  {a_1 : a} → {a_2 : String.Slice} → Inhabited (String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher a_1 a_2)
-- Lean.Parser.Attr
Lean.Parser.attrParser.formatter : optParam ℕ 0 → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The canonical morphism `L₀.X₂ ⟶ P`.  -/
CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → (S : CategoryTheory.ShortComplex.SnakeInput C) → S.L₀.X₂ ⟶ S.P
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.enum.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.enum = 1
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given two points in an affine subspace, the angles between those two points at two other
points on opposite sides of that subspace have opposite signs.  -/
AffineSubspace.SOppSide.oangle_sign_eq_neg : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {s : AffineSubspace ℝ P} {p₁ p₂ p₃ p₄ : P},
  p₁ ∈ s →
    p₂ ∈ s → s.SOppSide p₃ p₄ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = -(EuclideanGeometry.oangle p₁ p₃ p₂).sign
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.not_isLoop : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsNonloop e → ¬M.IsLoop e
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.toList_rco : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.toList_rco._auto_1)
  [Std.TransCmp cmp] {t : Std.DTreeMap.Raw α β cmp},
  t.WF →
    ∀ {lowerBound upperBound : α},
      Std.Slice.toList (Std.Rco.Sliceable.mkSlice t lowerBound...upperBound) =
        List.filter (fun e => decide ((cmp e.fst lowerBound).isGE = true ∧ (cmp e.fst upperBound).isLT = true)) t.toList
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.single_zero : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (i : ι), (fun₀ | i => 0) = 0
-- Init.Data.Array.Attach
/-- Maps a partially defined function (defined on those terms of `α` that satisfy a predicate `P`) over
an array `xs : Array α`, given a proof that every element of `xs` in fact satisfies `P`.

`Array.pmap`, named for “partial map,” is the equivalent of `Array.map` for such partial functions.
 -/
Array.pmap : {α : Type u_1} → {β : Type u_2} → {P : α → Prop} → ((a : α) → P a → β) → (xs : Array α) → (∀ a ∈ xs, P a) → Array β
-- Mathlib.CategoryTheory.Comma.Final
CategoryTheory.Comma.isCofiltered_of_isCofiltered_costructuredArrow : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [CategoryTheory.IsCofiltered A] [CategoryTheory.IsCofiltered B]
  [∀ (b : B), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow L (R.obj b))],
  CategoryTheory.IsCofiltered (CategoryTheory.Comma L R)
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.uppcRec.match_1.splitter : {w : ℕ} →
  (motive : (s : ℕ) → s < w → Sort u_1) →
    (s : ℕ) →
      (hs : s < w) → ((hs : 0 < w) → motive 0 hs) → ((i : ℕ) → (hs : i + 1 < w) → motive i.succ hs) → motive s hs
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.cos_sq_arctan : ∀ (x : ℝ), Real.cos (Real.arctan x) ^ 2 = 1 / (1 + x ^ 2)
-- Mathlib.Algebra.Order.Floor.Ring
Int.abs_fract : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R} [IsOrderedRing R],
  |Int.fract a| = Int.fract a
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_0 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.vars 0 = ∅
-- Mathlib.Order.UpperLower.Closure
IsLowerSet.disjoint_upperClosure_right : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, IsLowerSet s → (Disjoint s ↑(upperClosure t) ↔ Disjoint s t)
-- Mathlib.GroupTheory.Torsion
CommGroup.freeRank_ge_of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : CommGroup G] [inst_1 : CommGroup H] [inst_2 : Group.FG G] [inst_3 : Group.FG H]
  (e : G →* H), Function.Surjective ⇑e → CommGroup.freeRank H ≤ CommGroup.freeRank G
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If the action of a countable group `G` admits an invariant measure `μ` with a fundamental domain
`s`, then every null-measurable set `t` such that the sets `g • t ∩ s` are pairwise a.e.-disjoint
has measure at most `μ s`.  -/
MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ →
    MeasureTheory.NullMeasurableSet t μ →
      Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) fun g => g • t ∩ s) → μ t ≤ μ s
-- Mathlib.Data.List.Lemmas
List.foldr_range_subset_of_range_subset : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → α → α} {g : γ → α → α},
  Set.range f ⊆ Set.range g → ∀ (a : α), Set.range (List.foldr f a) ⊆ Set.range (List.foldr g a)
-- Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : J.Subcanonical] {S T : C} (E : J.OneHypercover S) (f : (i : E.I₀) → E.X i ⟶ T)
  (h :
    ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
      CategoryTheory.CategoryStruct.comp (E.p₁ k) (f i) = CategoryTheory.CategoryStruct.comp (E.p₂ k) (f j))
  (i : E.I₀), CategoryTheory.CategoryStruct.comp (E.f i) (E.glueMorphisms f h) = f i