mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.colimitNegAux.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat) (x : (j : J) × ↑(F.obj j)),
  AddGrpCat.FilteredColimits.colimitNegAux F x = AddGrpCat.FilteredColimits.G.mk F ⟨x.fst, -x.snd⟩
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.disjoint_iff_right : ∀ {α : Type u_1} {ι : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → (Disjoint l' l ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l')
-- Mathlib.Data.Vector3
/-- Construct a vector from a function on `Fin2`.  -/
Vector3.ofFn : {α : Type u_1} → {n : ℕ} → (Fin2 n → α) → Vector3 α n
-- Mathlib.RingTheory.WittVector.Teichmuller
/-- The Teichmüller lift of an element of `R` to `𝕎 R`.
The `0`-th coefficient of `teichmuller p r` is `r`, and all others are `0`.
This is a monoid homomorphism.  -/
WittVector.teichmuller : (p : ℕ) → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [inst : CommRing R] → R →* WittVector p R
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.equivPresentedGroup_symm_apply_of : ∀ {α : Type u_1} {β : Type u_2} (x : β) (rels : Set (FreeGroup α)) (e : α ≃ β),
  (PresentedGroup.equivPresentedGroup rels e).symm (PresentedGroup.of x) = PresentedGroup.of (e.symm x)
-- Mathlib.RingTheory.MvPowerSeries.Rename
_private.Mathlib.RingTheory.MvPowerSeries.Rename.0.MvPowerSeries.killComplFun_monomial_eq_zero : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {e : σ ↪ τ} {x : τ →₀ ℕ} (r : R),
  x ∉ Set.range (Finsupp.embDomain e) → MvPowerSeries.killComplFun e ((MvPowerSeries.monomial x) r) = 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.addConst.go : ℤ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Analysis.Convex.Function
/-- If `f` is convex on `s`, so is `(f ∘ g)` on `g ⁻¹' s` for a linear `g`.  -/
ConvexOn.comp_linearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid F] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β]
  [inst_6 : Module 𝕜 E] [inst_7 : Module 𝕜 F] [inst_8 : SMul 𝕜 β] {f : F → β} {s : Set F},
  ConvexOn 𝕜 s f → ∀ (g : E →ₗ[𝕜] F), ConvexOn 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_le : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [inst : StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasCondSubgaussianMGF m hm X c μ →
    ∀ (t : ℝ), ∀ᵐ (ω' : Ω) ∂μ.trim hm, μ[fun ω => Real.exp (t * X ω) | m] ω' ≤ Real.exp (↑c * t ^ 2 / 2)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Cell.getEntry?.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (p : (a : α) × β a) → motive (some p)),
  (match none with
    | none => h_1 ()
    | some p => h_2 p) =
    h_1 ()
-- Mathlib.Data.List.Lemmas
List.mapAccumr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ → γ × β) (x : γ), List.mapAccumr f [] x = (x, [])
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
/-- Let `it` be an iterator and `f` a monadic function mapping `it`'s outputs to iterators.
Then `it.flatMapM f` is an iterator that goes over `it` and for each output, it applies `f` and
iterates over the resulting iterator. `it.flatMapM f` emits all values obtained from the inner
iterators -- first, all of the first inner iterator, then all of the second one, and so on.

**Marble diagram (without monadic effects):**

```text
it                 ---a      --b      c    --d -⊥
f a                    a1-a2⊥
f b                             b1-b2⊥
f c                                    c1-c2⊥
f d                                           ⊥
it.flatMapM        ----a1-a2----b1-b2--c1-c2----⊥
```

**Termination properties:**

* `Finite` instance: only if `it` and the inner iterators are finite
* `Productive` instance: only if `it` is finite and the inner iterators are productive

For certain functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer
iterator is productive and the inner
iterators are productive *and provably never empty*, then the resulting iterator is also productive.

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it` or an internal iterator.

For each value emitted by the outer iterator `it`, this combinator calls `f`.
 -/
Std.IterM.flatMapM : {α β α₂ γ : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      [inst_1 : MonadAttach m] →
        [Std.Iterator α m β] → [Std.Iterator α₂ m γ] → (f : β → m (Std.IterM m γ)) → Std.IterM m β → Std.IterM m γ
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
CompleteLattice.MulticoequalizerDiagram.multispanIndex_right : ∀ {T : Type u} [inst : CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T}
  (d : CompleteLattice.MulticoequalizerDiagram x u v) (a : ι), d.multispanIndex.right a = u a
-- Mathlib.Topology.Spectral.Hom
SpectralMap.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : SpectralMap α β},
  f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.hasLeftHomology_iff_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex Cᵒᵖ), S.HasLeftHomology ↔ S.unop.HasRightHomology
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃)
  (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X_1 : C₁) (X_2 : C₂)
  (X_3 : C₃),
  (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).obj X_1).obj X_2).obj X_3 =
    ((X.obj (F₁.obj X_1)).obj (F₂.obj X_2)).obj (F₃.obj X_3)
-- Lean.MetavarContext
Lean.MetavarContext.getLevelDepth : Lean.MetavarContext → Lean.LMVarId → ℕ
-- Lean.Compiler.Old
Lean.Compiler.checkIsDefinition : Lean.Environment → Lean.Name → Except String Unit
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_eq_none : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, a ∉ m → m.getKey? a = none
-- Aesop.Forward.Match.Types
/-- The substitution induced by the hyps or pattern substitutions added to
the slots.  -/
Aesop.Match.subst : Aesop.Match → Aesop.Substitution
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.ext_iff : ∀ {α : ℚ} {x y : Std.Time.Internal.UnitVal α}, x = y ↔ x.val = y.val
-- Mathlib.Topology.Homeomorph.Lemmas
IsHomeomorph.prodMap : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {W : Type u_5} [inst_3 : TopologicalSpace W] {f : X → Y} {g : Z → W},
  IsHomeomorph f → IsHomeomorph g → IsHomeomorph (Prod.map f g)
-- Mathlib.MeasureTheory.Group.Measure
/-- In a noncompact locally compact additive group, a left-invariant measure which is positive on
open sets has infinite mass.  -/
MeasureTheory.measure_univ_of_isAddLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] [inst_3 : AddGroup G]
  [IsTopologicalAddGroup G] [WeaklyLocallyCompactSpace G] [NoncompactSpace G] (μ : MeasureTheory.Measure G)
  [μ.IsOpenPosMeasure] [μ.IsAddLeftInvariant], μ Set.univ = ⊤
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.commonNeighbors_symm : ∀ {V : Type u} (G : SimpleGraph V) (v w : V), G.commonNeighbors v w = G.commonNeighbors w v
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
mem_fixingAddSubgroup_iff : ∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s : Set α} {m : M},
  m ∈ fixingAddSubgroup M s ↔ ∀ y ∈ s, m +ᵥ y = y
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- An isomorphism `X ⟶ Y` is a `P`-cover of `Y`.  -/
AlgebraicGeometry.Scheme.coverOfIsIso : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [P.ContainsIdentities] →
    [P.RespectsIso] →
      {X Y : AlgebraicGeometry.Scheme} →
        (f : X ⟶ Y) →
          [CategoryTheory.IsIso f] → AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) Y
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.vadd_orbit_subset : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] (m : M) (a : α),
  m +ᵥ AddAction.orbit M a ⊆ AddAction.orbit M a
-- Init.Data.Nat.Basic
Nat.not_add_one_le_zero : ∀ (n : ℕ), ¬n + 1 ≤ 0
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSet_zero_left : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure α}
  {s t : Set Ω}, ProbabilityTheory.Kernel.IndepSet s t 0 μ
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.forget₂AddCommMon_preservesLimitsAux.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections],
  AddCommGrpCat.forget₂AddCommMon_preservesLimitsAux F =
    AddCommMonCat.limitConeIsLimit (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddCommMonCat))
-- Init.Data.Int.Linear
Int.Internal.Linear.hugeFuel : ℕ
-- Init.Data.BitVec.Lemmas
BitVec.toInt_ofNat' : ∀ {n : ℕ} (x : ℕ), (BitVec.ofNat n x).toInt = (↑x).bmod (2 ^ n)
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.charP : ∀ {R : Type u} [inst : Semiring R] {p : ℕ} [CharP R p], CharP (Polynomial R) p
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.neg_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x x' : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F x x' → CommRingCat.Colimits.Relation F x.neg x'.neg
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.smul_vec2 : ∀ {α : Type u} {R : Type u_1} [inst : SMul R α] (x : R) (a₀ a₁ : α), x • ![a₀, a₁] = ![x • a₀, x • a₁]
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.comp_id : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (f : α →ᵈ β),
  f.comp (Dilation.id α) = f
-- Mathlib.LinearAlgebra.PerfectPairing.Restrict
/-- Restricting a perfect pairing to a subring of the scalars results in a perfect pairing.  -/
LinearMap.IsPerfPair.restrictScalars : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [inst_5 : p.IsPerfPair] {S : Type u_4}
  {M' : Type u_5} {N' : Type u_6} [inst_6 : CommRing S] [inst_7 : IsDomain S] [inst_8 : Algebra S R]
  [inst_9 : Module S M] [inst_10 : Module S N] [inst_11 : IsScalarTower S R M] [inst_12 : IsScalarTower S R N]
  [inst_13 : Module.IsTorsionFree S R] [inst_14 : Nontrivial R] [inst_15 : AddCommGroup M'] [inst_16 : Module S M']
  [inst_17 : AddCommGroup N'] [inst_18 : Module S N'] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N),
  Function.Injective ⇑i →
    Function.Injective ⇑j →
      Submodule.span R ↑i.range = ⊤ →
        Submodule.span R ↑j.range = ⊤ →
          (∀ (g : Module.Dual S N'), ∃ m, ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g) →
            (∀ (g : Module.Dual S M'), ∃ n, ↑S (p.flip.toPerfPair (j n)) ∘ₗ i = Algebra.linearMap S R ∘ₗ g) →
              ∀ (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range),
                (i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp).IsPerfPair
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
AlgebraicGeometry.pointOfClosedPoint_comp : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [inst_1 : IsAlgClosed K]
  (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [inst_2 : AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X)
  (hx : IsClosed {x}),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pointOfClosedPoint f x hx) f =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K))
-- Mathlib.Order.Monotone.Basic
/-- If an antitone function is equal at two points, it is equal between all of them  -/
Antitone.eq_of_ge_of_le : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β} {a₁ a₂ : α},
  Antitone f → f a₁ = f a₂ → ∀ {i : α}, a₁ ≤ i → i ≤ a₂ → f i = f a₁
-- Mathlib.Order.Minimal
minimal_subset_iff' : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α}, Minimal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → t ⊆ s → s ⊆ t
-- Mathlib.Data.Nat.Factorization.Basic
/-- The multiplicity of prime `p` in `p` is `1`  -/
Nat.Prime.factorization_self : ∀ {p : ℕ}, Nat.Prime p → p.factorization p = 1
-- Mathlib.Analysis.LocallyConvex.HahnBanach
/-- **Hahn-Banach theorem** for linear functionals dominated by a continuous seminorm on
polynormable spaces over `ℝ`.  -/
Module.Dual.exists_continuous_extension_of_le_seminorm_real : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : Module ℝ E] [PolynormableSpace ℝ E]
  (S : Subspace ℝ E) (f : Module.Dual ℝ ↥S) {p : Seminorm ℝ E},
  Continuous ⇑p → (∀ (x : ↥S), f x ≤ p ↑x) → ∃ g, (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), |g x| ≤ p x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_eq_getValue! : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Inhabited β] {l : List ((_ : α) × β)} {a : α}
  (h : Std.Internal.List.containsKey a l = true), Std.Internal.List.getValue a l h = Std.Internal.List.getValue! a l
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.instTotalLe : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : LinearOrder M], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Data.Setoid.Basic
Setoid.quotientKerEquivOfRightInverse_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (hf : Function.RightInverse g f) (b : β),
  (Setoid.quotientKerEquivOfRightInverse f g hf).symm b = Quotient.mk'' (g b)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.gcd_dvd_left : ∀ (a b : ℤ), Int.Internal.Linear.gcd✝ a b ∣ a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toList_ric' : ∀ {n k : ℕ}, List.map (fun x => k + x) (*...=n).toList = (k...=k + n).toList
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableOn.add_iff_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {s : Set E}, DifferentiableOn 𝕜 f s → (DifferentiableOn 𝕜 (f + g) s ↔ DifferentiableOn 𝕜 g s)
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ioc_pred_pred_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] [NoMinOrder α] (a b : α),
  Finset.Ioc (Order.pred a) (Order.pred b) = Finset.Ico a b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α}, m.contains a = false → Std.DHashMap.Const.get? m a = none
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  (X : P.FullSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.obj).inv
-- Mathlib.Data.Int.CardIntervalMod
/-- There are `⌊(b - v) / r⌋ - ⌊(a - v) / r⌋` numbers congruent to `v` mod `r` in `(a, b]`,
if `a ≤ b`.  -/
Int.Ioc_filter_modEq_card : ∀ (a b : ℤ) {r : ℤ},
  0 < r → ∀ (v : ℤ), ↑{x ∈ Finset.Ioc a b | x ≡ v [ZMOD r]}.card = max (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) 0
-- Aesop.Index.Basic
Aesop.instInhabitedIndexMatchLocation : Inhabited Aesop.IndexMatchLocation
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.horn.spineId_map_hornInclusion : ∀ {n : ℕ} (i : Fin (n + 3)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 2)),
  (SSet.horn.spineId i h₀ hₙ).map (SSet.horn (n + 2) i).ι = SSet.stdSimplex.spineId (n + 2)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.cyclotomic_pos : ∀ {n : ℕ},
  2 < n →
    ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] (x : R),
      0 < Polynomial.eval x (Polynomial.cyclotomic n R)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_hyperplane : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (i : ι)
  [MeasureTheory.NullSingletonClass (μ i)] (x : α i), (MeasureTheory.Measure.pi μ) {f | f i = x} = 0
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- the index type of the coverings of the fibre products  -/
CategoryTheory.PreOneHypercover.I₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → (self : CategoryTheory.PreOneHypercover S) → self.I₀ → self.I₀ → Type w
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_of_finite : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [Finite α]
  [MeasurableSingletonClass α] (f : α → β), Measurable f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.toString : {w : ℕ} → Std.Tactic.BVDecide.BVExpr w → String
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosure.isAlgebraic : ∀ {R : Type u} {K : Type v} {inst : CommRing R} {inst_1 : Field K} {inst_2 : Algebra R K}
  {inst_3 : Module.IsTorsionFree R K} [self : IsAlgClosure R K], Algebra.IsAlgebraic R K
-- Mathlib.Probability.Process.Filtration
/-- The exterior σ-algebras of finite sets of `α` form a cofiltration indexed by `Finset α`.  -/
MeasureTheory.Filtration.cylinderEventsCompl : {Ω : Type u_1} → {m : MeasurableSpace Ω} → {α : Type u_4} → MeasureTheory.Filtration (Finset α)ᵒᵈ MeasurableSpace.pi
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- the cokernel condition for `p`  -/
CategoryTheory.ShortComplex.RightHomologyData.wp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (self : S.RightHomologyData), CategoryTheory.CategoryStruct.comp S.f self.p = 0
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor_map_τ₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) {X Y : HomologicalComplex C c} (f : X ⟶ Y),
  ((HomologicalComplex.shortComplexFunctor C c i).map f).τ₁ = f.f (c.prev i)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- Given a rank function `f : P.RankFunction ι` for a proper pairing `P`
of a subcomplex of a simplicial set, this is the induced morphism
`f.sigmaStdSimplex j ⟶ f.filtration (Order.succ j)` for any `j : ι`.  -/
SSet.Subcomplex.Pairing.RankFunction.b : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          (f : P.RankFunction ι) →
            [P.IsProper] →
              [inst_2 : SuccOrder ι] →
                [NoMaxOrder ι] → (j : ι) → f.sigmaStdSimplex j ⟶ (f.filtration (Order.succ j)).toSSet
-- Lean.Elab.InfoTree.Types
Lean.Elab.ContextInfo.mk.inj : ∀ {toCommandContextInfo : Lean.Elab.CommandContextInfo} {parentDecl? : Option Lean.Name}
  {autoImplicits : Array Lean.Expr} {toCommandContextInfo_1 : Lean.Elab.CommandContextInfo}
  {parentDecl?_1 : Option Lean.Name} {autoImplicits_1 : Array Lean.Expr},
  { toCommandContextInfo := toCommandContextInfo, parentDecl? := parentDecl?, autoImplicits := autoImplicits } =
      { toCommandContextInfo := toCommandContextInfo_1, parentDecl? := parentDecl?_1,
        autoImplicits := autoImplicits_1 } →
    toCommandContextInfo = toCommandContextInfo_1 ∧ parentDecl? = parentDecl?_1 ∧ autoImplicits = autoImplicits_1
-- Mathlib.Computability.DFA
/-- `M.acceptsFrom s` is the language of `x` such that `M.evalFrom s x` is an accept state.
 -/
DFA.acceptsFrom : {α : Type u} → {σ : Type v} → DFA α σ → σ → Language α
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_sigma : ∀ {ι : Type u_2} (f : ι → Type u_1), Cardinal.mk ((i : ι) × f i) = Cardinal.sum fun i => Cardinal.mk (f i)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The forgetful functor from additive monoid objects to the ambient category.  -/
CategoryTheory.AddMon.forget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor (CategoryTheory.AddMon C) C
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- A subset of a cospherical set is cospherical.  -/
EuclideanGeometry.Cospherical.subset : ∀ {P : Type u_2} [inst : MetricSpace P] {ps₁ ps₂ : Set P},
  ps₁ ⊆ ps₂ → EuclideanGeometry.Cospherical ps₂ → EuclideanGeometry.Cospherical ps₁
-- Init.Internal.Order.Basic
/-- The least upper bound of an arbitrary subset exists.
 -/
Lean.Order.CompleteLattice.has_sup : ∀ {α : Sort u} [self : Lean.Order.CompleteLattice α] (c : α → Prop), Exists (Lean.Order.is_sup c)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.applyPartition.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] (k : α → Ordering) (l : Std.DTreeMap.Internal.Impl α β)
  (f :
    List ((a : α) × β a) →
      (c : Std.DTreeMap.Internal.Cell α β k) →
        (Std.DTreeMap.Internal.Impl.contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ),
  Std.DTreeMap.Internal.Impl.applyPartition k l f = Std.DTreeMap.Internal.Impl.applyPartition.go k l f [] l ⋯ []
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.ae_map_le : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb →
    MeasureTheory.ae (MeasureTheory.Measure.map f μa) ≤ MeasureTheory.ae μb
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.LawfulEqOrd α] [Std.TransOrd α] [inst_3 : BEq α]
  [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.maxKey? l = some k ↔
      Std.Internal.List.containsKey k l = true ∧
        ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true)