mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instPreservesFiniteColimitsIndYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Ind.yoneda
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.mem_mutuallySingularSetSlice : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) (a : α) (x : γ),
  x ∈ κ.mutuallySingularSetSlice η a ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Basic.0.Std.Legacy.Range.forIn'.loop.congr_simp : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (range : Std.Legacy.Range)
  (f f_1 : (i : ℕ) → i ∈ range → β → m (ForInStep β)),
  f = f_1 →
    ∀ (b b_1 : β),
      b = b_1 →
        ∀ (i i_1 : ℕ) (e_i : i = i_1) (hs : (i - range.start) % range.step = 0) (hl : range.start ≤ i),
          Std.Legacy.Range.forIn'.loop✝ range f b i hs hl = Std.Legacy.Range.forIn'.loop✝ range f_1 b_1 i_1 ⋯ ⋯
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- Goals created by the tactic  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.TacticData.goalsCreatedBy : Mathlib.Linter.Flexible.TacticData✝ → List Lean.MVarId
-- Mathlib.Algebra.Category.ModuleCat.Subobject
/-- An extensionality lemma showing that two elements of a cokernel by an image
are equal if they differ by an element of the image.

The application is for homology:
two elements in homology are equal if they differ by a boundary.
 -/
ModuleCat.cokernel_π_imageSubobject_ext : ∀ {R : Type u} [inst : Ring R] {L M N : ModuleCat R} (f : L ⟶ M) [inst_1 : CategoryTheory.Limits.HasImage f]
  (g : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶ N)
  [inst_2 : CategoryTheory.Limits.HasCokernel g] {x y : ↑N} (l : ↑L),
  x =
      y +
        (CategoryTheory.ConcreteCategory.hom g)
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.factorThruImageSubobject f)) l) →
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π g)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π g)) y
-- Mathlib.LinearAlgebra.BilinearMap
IsBilinearMap.mk : ∀ {R : Type u_1} [inst : CommSemiring R] {E : Type u_2} [inst_1 : AddCommMonoid E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommMonoid F] [inst_4 : Module R F] {G : Type u_4} [inst_5 : AddCommMonoid G] [inst_6 : Module R G]
  {f : E → F → G},
  (∀ (x₁ x₂ : E) (y : F), f (x₁ + x₂) y = f x₁ y + f x₂ y) →
    (∀ (c : R) (x : E) (y : F), f (c • x) y = c • f x y) →
      (∀ (x : E) (y₁ y₂ : F), f x (y₁ + y₂) = f x y₁ + f x y₂) →
        (∀ (c : R) (x : E) (y : F), f x (c • y) = c • f x y) → IsBilinearMap R f
-- Mathlib.Data.PFunctor.Univariate.M
/-- follow a path through a value of `M F` and return the subtree
found at the end of the path if it is a valid path for that value and
return a default tree  -/
PFunctor.M.isubtree : {F : PFunctor.{uA, uB}} → [DecidableEq F.A] → [Inhabited F.M] → PFunctor.Approx.Path F → F.M → F.M
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instLeast? : Std.PRange.Least? Int32
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_subset_iff : ∀ {α : Type u_1} [inst : Fintype α] {s : Finset α}, Finset.univ ⊆ s ↔ s = Finset.univ
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The power series expansion of `℘` at `x`.
See `PeriodPair.hasFPowerSeriesOnBall_weierstrassP`.  -/
PeriodPair.weierstrassPSeries : PeriodPair → ℂ → FormalMultilinearSeries ℂ ℂ ℂ
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- **Alias** of `Equicontinuous.isClosed_setOfPred_tendsto`.

---

If `F : ι → X → α` is an equicontinuous family of functions,
`f : X → α` is a continuous function, and `l` is a filter on `ι`,
then `{x | Filter.Tendsto (F · x) l (𝓝 (f x))}` is a closed set.  -/
Equicontinuous.isClosed_setOf_tendsto : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {l : Filter ι}
  {F : ι → X → α} {f : X → α},
  Equicontinuous F → Continuous f → IsClosed {x | Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))}
-- Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal
LinearMap.orthogonal_span_singleton_eq_to_lin_ker : ∀ {K : Type u_7} {V : Type u_9} {V₂ : Type u_11} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {J : K →+* K} {B : V →ₗ[K] V →ₛₗ[J] V₂} (x : V),
  Submodule.orthogonalBilin B (K ∙ x) = (B x).ker
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.comap_sup_of_injective : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  {f : M →ₛₗ[σ₁₂] M₂} [inst_6 : RingHomSurjective σ₁₂] {p q : Submodule R₂ M₂},
  Function.Injective ⇑f →
    p ≤ f.range → q ≤ f.range → Submodule.comap f (p ⊔ q) = Submodule.comap f p ⊔ Submodule.comap f q
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- A category `C` is a universally exact category if all equivalence relations in `C` are
universally effective equivalence relations.  -/
CategoryTheory.IsUniversallyEffectiveEquivalenceRelationCategory : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → {R A : C} → Prop
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- `Prod.snd` as an `AffineMap`.  -/
AffineMap.snd : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        {P2 : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V1] →
              [inst_2 : Module k V1] →
                [inst_3 : AddTorsor V1 P1] →
                  [inst_4 : AddCommGroup V2] → [inst_5 : Module k V2] → [inst_6 : AddTorsor V2 P2] → P1 × P2 →ᵃ[k] P2
-- Mathlib.Topology.Algebra.Support
range_eq_image_tsupport_or : ∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] (f : X → α),
  Set.range f = f '' tsupport f ∨ Set.range f = insert 0 (f '' tsupport f)
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousAt.sup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {x : α} {r' : α → β → Prop},
  SemicontinuousAt r x → SemicontinuousAt r' x → SemicontinuousAt (r ⊔ r') x
-- Mathlib.GroupTheory.Congruence.Basic
Con.ofSubmonoid.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] (N : Submonoid (M × M)) (H : Equivalence fun x y => (x, y) ∈ N),
  Con.ofSubmonoid N H = { r := fun x y => (x, y) ∈ N, iseqv := H, mul' := ⋯ }
-- Init.Data.Array.Basic
/-- Constructs an array of numbers of size `size`, starting at `start` and increasing by
`step` at each element.

In other words, `Array.range' start size step` is `#[start, start+step, ..., start+(len-1)*step]`.

Examples:
 * `Array.range' 0 3 (step := 1) = #[0, 1, 2]`
 * `Array.range' 0 3 (step := 2) = #[0, 2, 4]`
 * `Array.range' 0 4 (step := 2) = #[0, 2, 4, 6]`
 * `Array.range' 3 4 (step := 2) = #[3, 5, 7, 9]`
 -/
Array.range' : ℕ → ℕ → optParam ℕ 1 → Array ℕ
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber_zero : ∀ {E : Type u_3} [inst : EMetricSpace E] (A : Set E), Metric.coveringNumber 0 A = A.encard
-- Mathlib.RingTheory.Ideal.Operations
/-- Given `s`, a generating set of `R`, to check that an `x : M` falls in a
submodule `M'` of `x`, we only need to show that `r ^ n • x ∈ M'` for some `n` for each `r : s`.  -/
Submodule.mem_of_span_eq_top_of_smul_pow_mem : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (M' : Submodule R M) (s : Set R), Ideal.span s = ⊤ → ∀ (x : M), (∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ M') → x ∈ M'
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.comp_smul : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] (ρ : Representation A G V) (σ : Representation A G W)
  (τ : Representation A G U) (a : A) (f : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ), f.comp (a • g) = a • f.comp g
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.mul : (α : Type u_1) → [Ring α] → [inst : UniformSpace α] → Mul (UniformSpace.Completion α)
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.mk.sizeOf_spec : ∀ (levelParams : List Lean.Name) (largeElim : Bool) (params motives : Array Lean.Expr) (motiveToIdx : Lean.FVarIdMap ℕ)
  (minors : Array Lean.Expr) (recNames belowNames brecOnNames : Array Lean.Name),
  sizeOf
      { levelParams := levelParams, largeElim := largeElim, params := params, motives := motives,
        motiveToIdx := motiveToIdx, minors := minors, recNames := recNames, belowNames := belowNames,
        brecOnNames := brecOnNames } =
    1 + sizeOf levelParams + sizeOf largeElim + sizeOf params + sizeOf motives + sizeOf motiveToIdx + sizeOf minors +
          sizeOf recNames +
        sizeOf belowNames +
      sizeOf brecOnNames
-- Mathlib.Dynamics.Ergodic.Ergodic
PreErgodic.smul_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : MeasureTheory.Measure α} {R : Type u_2}
  [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal], PreErgodic f μ → ∀ (c : R), PreErgodic f (c • μ)
-- Mathlib.RingTheory.Trace.Quotient
/-- The trace map on `B → A` coincides with the trace map on `B⧸pB → A⧸p`.  -/
Algebra.trace_quotient_eq_of_isDedekindDomain : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [p.IsMaximal] (x : S) [inst_4 : IsDedekindDomain R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree R S]
  [inst_7 : Module.Finite R S] [inst_8 : IsIntegrallyClosed S],
  (Algebra.trace (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) =
    (Ideal.Quotient.mk p) ((Algebra.intTrace R S) x)
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
/-- The morphism `M.exteriorPower n ⟶ N.exteriorPower n` induced by a morphism `M ⟶ N`
in `ModuleCat R`.  -/
ModuleCat.exteriorPower.map : {R : Type u} → [inst : CommRing R] → {M N : ModuleCat R} → (M ⟶ N) → (n : ℕ) → M.exteriorPower n ⟶ N.exteriorPower n
-- Init.Data.SInt.Lemmas
ISize.toBitVec_mul : ∀ {a b : ISize}, (a * b).toBitVec = a.toBitVec * b.toBitVec
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_ceil_right : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto (fun x => ↑⌈x⌉) (nhdsWithin (↑n) (Set.Ioi ↑n)) (nhdsWithin (↑n + 1) (Set.Ici (↑n + 1)))
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.x_projective : ∀ (k : Type u) [inst : CommRing k] (G : Type u) [inst_1 : Group G] (n : ℕ),
  CategoryTheory.Projective ((Rep.standardComplex k G).X n)
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Problem.instToString : ToString Lean.Elab.Tactic.Omega.Problem
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- Turn a `K`-cover into a `Q`-cover by showing that the components satisfy `Q`.  -/
AlgebraicGeometry.Scheme.Cover.changeProp : {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
      [AlgebraicGeometry.Scheme.JointlySurjective K] →
        (𝒰 : AlgebraicGeometry.Scheme.Cover K X) →
          (∀ (j : 𝒰.I₀), Q (𝒰.f j)) → AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage Q) X
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.Sigma.dist.match_1.eq_1 : ∀ {ι : Type u_1} {E : ι → Type u_2} (motive : (i : ι) × E i → (i : ι) × E i → Sort u_3) (i : ι) (x : E i) (j : ι)
  (y : E j) (h_1 : (i : ι) → (x : E i) → (j : ι) → (y : E j) → motive ⟨i, x⟩ ⟨j, y⟩),
  (match ⟨i, x⟩, ⟨j, y⟩ with
    | ⟨i, x⟩, ⟨j, y⟩ => h_1 i x j y) =
    h_1 i x j y
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCommSq.mk.sizeOf_spec : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (R : Type u) [commRing : CommRing R] [domain : IsDomain R]
  [valuationRing : ValuationRing R] (K : Type u) [field : Field K] [algebra : Algebra R K]
  [isFractionRing : IsFractionRing R K] (i₁ : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X)
  (i₂ : AlgebraicGeometry.Spec (CommRingCat.of R) ⟶ Y)
  (commSq : CategoryTheory.CommSq i₁ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) f i₂),
  sizeOf
      { R := R, commRing := commRing, domain := domain, valuationRing := valuationRing, K := K, field := field,
        algebra := algebra, isFractionRing := isFractionRing, i₁ := i₁, i₂ := i₂, commSq := commSq } =
    1 + sizeOf R + sizeOf commRing + sizeOf domain + sizeOf valuationRing + sizeOf K + sizeOf field + sizeOf algebra +
            sizeOf isFractionRing +
          sizeOf i₁ +
        sizeOf i₂ +
      sizeOf commSq
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_prod_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (a : α × β),
  Set.Iic a = Set.Iic a.1 ×ˢ Set.Iic a.2
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Constructor for isomorphisms between multicoforks.  -/
CategoryTheory.Limits.Multicofork.ext : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      {I : CategoryTheory.Limits.MultispanIndex J C} →
        {K K' : CategoryTheory.Limits.Multicofork I} →
          (e : K.pt ≅ K'.pt) →
            autoParam (∀ (i : J.R), CategoryTheory.CategoryStruct.comp (K.π i) e.hom = K'.π i)
                CategoryTheory.Limits.Multicofork.ext._auto_1 →
              (K ≅ K')
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- **Alias** of `Topology.RelCWComplex.finite_iff_finite_cells`.

---

A CW complex is finite iff the total number of its cells is finite.  -/
Topology.CWComplex.finite_iff_finite_cells : ∀ {X : Type u_2} [inst : TopologicalSpace X] {C D : Set X} [inst_1 : Topology.RelCWComplex C D],
  Topology.RelCWComplex.Finite C ↔ Finite ((n : ℕ) × Topology.RelCWComplex.cell C n)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.eq_snd_of_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v}, p.IsPath → s(u, w) ∈ p.edges → w = p.snd
-- Mathlib.Dynamics.Flow
/-- Transitivity of factors of flows.  -/
Flow.IsFactorOf.trans : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) {β : Type u_3} {γ : Type u_4} [inst_3 : TopologicalSpace β] [inst_4 : TopologicalSpace γ]
  (ψ : Flow τ β) (χ : Flow τ γ), ϕ.IsFactorOf ψ → ψ.IsFactorOf χ → ϕ.IsFactorOf χ
-- Mathlib.Topology.Order.DenselyOrdered
interior_Ico : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] {a b : α}, interior (Set.Ico a b) = Set.Ioo a b
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.exp_llr_of_ac : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν → (fun x => Real.exp (MeasureTheory.llr μ ν x)) =ᵐ[μ] fun x => (μ.rnDeriv ν x).toReal
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.toFun_add : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Add β] (f g : UniformOnFun α β 𝔖),
  (UniformOnFun.toFun 𝔖) (f + g) = (UniformOnFun.toFun 𝔖) f + (UniformOnFun.toFun 𝔖) g
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
AddAction.instIsMultiplyPretransitiveOfIsMultiplyPreprimitive : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] (n : ℕ)
  [AddAction.IsMultiplyPreprimitive M α n], AddAction.IsMultiplyPretransitive M α n
-- Init.Data.UInt.Bitwise
UInt32.toBitVec_and : ∀ (a b : UInt32), (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Finite product of seminormed groups, using the sup norm.  -/
Pi.seminormedCommGroup : {ι : Type u_1} →
  {G : ι → Type u_4} → [Fintype ι] → [(i : ι) → SeminormedCommGroup (G i)] → SeminormedCommGroup ((i : ι) → G i)
-- Mathlib.Geometry.Euclidean.Projection
/-- Reflection in an affine subspace, which is expected to be nonempty
and complete. The word "reflection" is sometimes understood to mean
specifically reflection in a codimension-one subspace, and sometimes
more generally to cover operations such as reflection in a point. The
definition here, of reflection in an affine subspace, is a more
general sense of the word that includes both those common cases.  -/
EuclideanGeometry.reflection : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            [inst_3 : MetricSpace P] →
              [inst_4 : NormedAddTorsor V P] →
                (s : AffineSubspace 𝕜 P) → [Nonempty ↥s] → [s.direction.HasOrthogonalProjection] → P ≃ᵃⁱ[𝕜] P
-- Lean.LibrarySuggestions.SineQuaNon
Lean.LibrarySuggestions.sineQuaNonSelector : optParam Float 1.5 → Lean.LibrarySuggestions.Selector
-- Lean.Parser.Term
Lean.Parser.Term.pipeProj.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_preimage : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] (s : Set α) (f : α → M) (B : Set M),
  s.indicator f ⁻¹' B = s.ite (f ⁻¹' B) (0 ⁻¹' B)
-- Lean.DocString.Markdown
/-- Splits off the trailing run of whitespace from an inline tree, returning the remainder as a new
inline and the whitespace as a plain string. This allows emphasis to be applied to strings that
start or end with whitespace, taking the flanking rules of Markdown into account.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.trimRight : {i : Type u_1} → Lean.Doc.Inline i → Lean.Doc.Inline i × String
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_sub_pi_mul_I : ∀ (z : ℂ), Complex.exp (z - ↑Real.pi * Complex.I) = -Complex.exp z
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1 : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyIrreducible g]
  [AlgebraicGeometry.UniversallyOpen g] [IrreducibleSpace ↥X], IrreducibleSpace ↥(CategoryTheory.Limits.pullback f g)
-- Mathlib.RingTheory.Localization.Rat
Rat.isFractionRingNum : ∀ (q : ℚ), Associated (IsFractionRing.num ℤ q) q.num
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.coe_id_orderHom : ∀ (α : Type u_2) [inst : Preorder α], ↑(PseudoEpimorphism.id α) = OrderHom.id
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.replaceTR.go.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (l : List α) (b c : α) (a : Array α), List.replaceTR.go✝ l b c [] a = l
-- Mathlib.Topology.MetricSpace.Dilation
/-- The identity is a dilation  -/
Dilation.id : (α : Type u_5) → [inst : PseudoEMetricSpace α] → α →ᵈ α
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.mem_of_insert_indep : ∀ {α : Type u_1} {M : Matroid α} {B : Set α} {e : α}, M.IsBase B → M.Indep (insert e B) → e ∈ B
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.transEventuallyEqIsBigO : {α : Type u_1} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : Norm E] →
        [inst_1 : Norm F] →
          {l : Filter α} → Trans (fun x1 x2 => x1 =ᶠ[l] x2) (fun x1 x2 => x1 =O[l] x2) fun x1 x2 => x1 =O[l] x2
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_X_pow : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] (n : ℕ), (Polynomial.X ^ n).degree = ↑n
-- Aesop.Check
Aesop.Check.isEnabled : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → Aesop.Check → m Bool
-- Mathlib.Combinatorics.Quiver.Subquiver
Quiver.Total.ext : ∀ {V : Type u} {inst : Quiver V} {x y : Quiver.Total V}, x.left = y.left → x.right = y.right → x.hom ≍ y.hom → x = y
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.id_apply : ∀ (X : Semigrp) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.fst_comp_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.fst.comp (AddMonoid.Coprod.swap M N) = AddMonoid.Coprod.snd
-- Init.Core
false_of_true_iff_false : (True ↔ False) → False
-- Mathlib.Order.Interval.Set.Image
directedOn_le_Icc : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), DirectedOn (fun x1 x2 => x1 ≤ x2) (Set.Icc a b)
-- Batteries.Tactic.GeneralizeProofs
/-- State for the `MAbs` monad.  -/
Batteries.Tactic.GeneralizeProofs.AState : Type
-- Mathlib.Order.InitialSeg
PrincipalSeg.mem_range_of_rel : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans β s] (f : PrincipalSeg r s) {a : α}
  {b : β}, s b (f.toRelEmbedding a) → b ∈ Set.range ⇑f.toRelEmbedding
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.three_dvd_b_of_dvd_a_of_gcd_eq_one_of_case2 : ∀ {a b c : ℤ},
  a ≠ 0 →
    {a, b, c}.gcd id = 1 →
      3 ∣ a →
        a ^ 3 + b ^ 3 + c ^ 3 = 0 →
          (∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3) → 3 ∣ b
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.ext : ∀ {M : Type u_1} [inst : AddZeroClass M] {s₁ s₂ : SaturatedAddSubmonoid M},
  s₁.toAddSubmonoid = s₂.toAddSubmonoid → s₁ = s₂
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.degree_U_neg_one : ∀ (R : Type u_1) [inst : CommRing R], (Polynomial.Chebyshev.U R (-1)).degree = ⊥
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.hoFunctor₂_naturality : ∀ {X Y : SSet.Truncated 2} (f : X ⟶ Y),
  ((SSet.oneTruncation₂.comp CategoryTheory.Cat.freeRefl).map f).toFunctor.comp
      (SSet.Truncated.HomotopyCategory.quotientFunctor Y) =
    (SSet.Truncated.HomotopyCategory.quotientFunctor X).comp (SSet.Truncated.mapHomotopyCategory f)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extendIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cocone F) {X : C} (f : s.pt ≅ X),
  s.extendIso f = { hom := { hom := f.hom, w := ⋯ }, inv := { hom := f.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.ext : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {t₁ t₂ : AlgebraicGeometry.Scheme.Pullback.Triplet f g},
  t₁.x = t₂.x → t₁.y = t₂.y → t₁ = t₂
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- If a polynomial starts with two positive coefficients, then the sign changes in the product
`(X - η) * P` is the same as `(X - η) * P.eraseLead`. This lemma lets us do induction on the
degree of P when P starts with matching coefficient signs. Of course this is also true when the
first two coefficients of P are *negative*, but we just prove the case where they're positive
since it's cleaner and sufficient for the later use.  -/
Polynomial.signVariations_X_sub_C_mul_eraseLead_le : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {P : Polynomial R} {η : R},
  0 < P.leadingCoeff →
    0 < P.nextCoeff →
      ((Polynomial.X - Polynomial.C η) * P.eraseLead).signVariations ≤
        ((Polynomial.X - Polynomial.C η) * P).signVariations
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.frontier_setOfPred_im_le`. -/
Complex.frontier_setOf_im_le : ∀ (a : ℝ), frontier {z | z.im ≤ a} = {z | z.im = a}
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.neg_left_iff : ∀ {R : Type u_1} [inst : CommRing R] (x y : R), IsRelPrime (-x) y ↔ IsRelPrime x y
-- Mathlib.Topology.UniformSpace.Cauchy
completeSpace_iff_ultrafilter : ∀ {α : Type u} [uniformSpace : UniformSpace α], CompleteSpace α ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ∃ x, ↑l ≤ nhds x