mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
/-- A natural transformation `G₂₀ ⟶ G₂₁ ⋙ G₁₀` involving right adjoint functors
induces a natural transformation `F₀₁ ⋙ F₁₂ ⟶ F₀₂` between the corresponding
left adjoint functors.  -/
CategoryTheory.Adjunction.leftAdjointCompNatTrans : {C₀ : Type u_1} →
  {C₁ : Type u_2} →
    {C₂ : Type u_3} →
      [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₂] →
            {F₀₁ : CategoryTheory.Functor C₀ C₁} →
              {F₁₂ : CategoryTheory.Functor C₁ C₂} →
                {F₀₂ : CategoryTheory.Functor C₀ C₂} →
                  {G₁₀ : CategoryTheory.Functor C₁ C₀} →
                    {G₂₁ : CategoryTheory.Functor C₂ C₁} →
                      {G₂₀ : CategoryTheory.Functor C₂ C₀} →
                        (F₀₁ ⊣ G₁₀) → (F₁₂ ⊣ G₂₁) → (F₀₂ ⊣ G₂₀) → (G₂₀ ⟶ G₂₁.comp G₁₀) → (F₀₁.comp F₁₂ ⟶ F₀₂)
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.logRatio_pos : ∀ {c : ENNReal}, 2⁻¹ < c → c < 1 → 0 < ProbabilityTheory.Fernique.logRatio c
-- Mathlib.Data.Finset.Sups
Finset.compls_eq_empty : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Finset α}, s.compls = ∅ ↔ s = ∅
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instHasOfPostcompPropertySchemeTopMorphismProperty : CategoryTheory.MorphismProperty.HasOfPostcompProperty @AlgebraicGeometry.IsImmersion ⊤
-- Std.Async.Process
/-- Returns the amount of free system memory in bytes.
 -/
Std.IO.Process.freeMemory : IO UInt64
-- Mathlib.Algebra.Homology.Augment
CochainComplex.augment_X_succ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) (i : ℕ),
  (C.augment f w).X (i + 1) = C.X i
-- Mathlib.Algebra.Category.MonCat.Basic
CategoryTheory.Iso.commMonCatIsoToAddEquiv.eq_1 : ∀ {X Y : AddCommMonCat} (i : X ≅ Y),
  i.commMonCatIsoToAddEquiv = (AddCommMonCat.Hom.hom i.hom).toAddEquiv (AddCommMonCat.Hom.hom i.inv) ⋯ ⋯
-- Mathlib.Tactic.NormNum.Ineq
/-- Helper function to synthesize typed `Ring α` `PartialOrder α` `IsOrderedRing α`
expressions.  -/
Mathlib.Meta.NormNum.inferOrderedRing : {u : Lean.Level} →
  (α : Q(Type u)) → Lean.MetaM ((x : Q(Ring «$α»)) × (x_1 : Q(PartialOrder «$α»)) × Q(IsOrderedRing «$α»))
-- Lean.Elab.Command
Lean.Elab.Command.Context.quotContext? : Lean.Elab.Command.Context → Option Lean.Name
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_edist_eq_card : ∀ {α : Type u_2} {β : Type u_3} [inst : EDist α] [inst_1 : EDist β] (f g : WithLp 0 (α × β)),
  edist f g = (if edist f.fst g.fst = 0 then 0 else 1) + if edist f.snd g.snd = 0 then 0 else 1
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.brecOn.go : {motive :
    (a : Lean.Omega.Constraint) → (a_1 : Lean.Omega.Coeffs) → Lean.Elab.Tactic.Omega.Justification a a_1 → Sort u} →
  {a : Lean.Omega.Constraint} →
    {a_1 : Lean.Omega.Coeffs} →
      (t : Lean.Elab.Tactic.Omega.Justification a a_1) →
        ((a : Lean.Omega.Constraint) →
            (a_2 : Lean.Omega.Coeffs) →
              (t : Lean.Elab.Tactic.Omega.Justification a a_2) →
                Lean.Elab.Tactic.Omega.Justification.below t → motive a a_2 t) →
          motive a a_1 t ×' Lean.Elab.Tactic.Omega.Justification.below t
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.representableByUliftFunctorEquiv_symm_apply_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {X : C}
  (R : F.RepresentableBy X) {Y : C},
  (CategoryTheory.Functor.representableByUliftFunctorEquiv.symm R).homEquiv = R.homEquiv.trans Equiv.ulift.symm
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.plusFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {X Y : CategoryTheory.Functor Cᵒᵖ D}
  (η : X ⟶ Y), (J.plusFunctor D).map η = J.plusMap η
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.allM_eq_match_step : ∀ {α β : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {p : β → m Bool},
  Std.Iter.allM p it =
    match ↑it.step with
    | Std.IterStep.yield it' x => do
      let __do_lift ← p x
      if __do_lift = true then Std.Iter.allM p it' else pure false
    | Std.IterStep.skip it' => Std.Iter.allM p it'
    | Std.IterStep.done => pure true
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_monotone : ∀ {α : Type u}, Monotone (Cardinal.mk ∘ Set.Elem)
-- Mathlib.Algebra.Order.Group.PosPart
one_lt_leOnePart_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Group α] {a : α} [MulLeftMono α], 1 < a⁻ᵐ ↔ a < 1
-- Mathlib.RingTheory.Artinian.Module
instIsArtinianRingProd : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] [IsArtinianRing R] [IsArtinianRing S],
  IsArtinianRing (R × S)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instSimpAndPureTrue_1 : ∀ (σs : List (Type u_1)) (P : Std.Do.SPred σs), Std.Do.SPred.Tactic.SimpAnd ⌜True⌝ P P
-- Mathlib.NumberTheory.Padics.Complex
/-- The norm on `PadicAlgCl p` extends the `p`-adic norm on `ℚ_[p]`.  -/
PadicAlgCl.norm_extends : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ℚ_[p]), ‖(algebraMap ℚ_[p] (PadicAlgCl p)) x‖ = ‖x‖
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.Iterators.Types.Take.instIterator.match_1.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM m β)
  (h' : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h' : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h'⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h' : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h'⟩)
  (h_3 : (h' : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h'⟩),
  (match ⟨Std.IterStep.skip it', h'⟩ with
    | ⟨Std.IterStep.yield it' out, h'⟩ => h_1 it' out h'
    | ⟨Std.IterStep.skip it', h'⟩ => h_2 it' h'
    | ⟨Std.IterStep.done, h'⟩ => h_3 h') =
    h_2 it' h'
-- Mathlib.LinearAlgebra.Determinant
/-- Builds a linear equivalence from a linear map on a finite-dimensional vector space whose
determinant is nonzero.  -/
LinearMap.equivOfDetNeZero : {𝕜 : Type u_5} →
  [inst : Field 𝕜] →
    {M : Type u_6} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module 𝕜 M] → [FiniteDimensional 𝕜 M] → (f : M →ₗ[𝕜] M) → LinearMap.det f ≠ 0 → M ≃ₗ[𝕜] M
-- Init.Data.Nat.Mod
Nat.mod_mul_right_mod : ∀ (a b c : ℕ), a % (b * c) % b = a % b
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_span_insert : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  (r : S) (s : Set S),
  Ideal.absNorm (Ideal.span (insert r s)) ∣ gcd (Ideal.absNorm (Ideal.span s)) ((Algebra.norm ℤ) r).natAbs
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginSeries_summable_aux₁ : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r r' : NNReal},
  ↑r + ↑r' < p.radius → Summable fun s => ‖p (s.fst + s.snd.fst)‖₊ * r ^ s.snd.fst * r' ^ s.fst
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
/-- The binary fan provided by `fst'` and `snd'`.  -/
CategoryTheory.ChosenPullbacksAlong.binaryFan : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (Y Z : CategoryTheory.Over X) → [CategoryTheory.ChosenPullbacksAlong Z.hom] → CategoryTheory.Limits.BinaryFan Y Z
-- Mathlib.Topology.MetricSpace.Cover
Metric.IsCover.refl : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (s : Set X), Metric.IsCover ε s s
-- Mathlib.Topology.MetricSpace.Congruence
/-- Congruence holds if and only if all extended distances between points with different
indices are the same.  -/
congruent_iff_pairwise_edist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂],
  Congruent v₁ v₂ ↔ Pairwise fun i₁ i₂ => edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.AEStronglyMeasurable.comp_ae_measurable' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] {mα : MeasurableSpace α}
  {x : MeasurableSpace γ} {f : α → β} {μ : MeasureTheory.Measure γ} {g : γ → α},
  MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map g μ) →
    AEMeasurable g μ → MeasureTheory.AEStronglyMeasurable (f ∘ g) μ
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.coe_sum : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {α : Type u_1} (s : Finset α) (f : α → ℤ_[p]), ↑(∑ z ∈ s, f z) = ∑ z ∈ s, ↑(f z)
-- Std.Data.DTreeMap.Basic
/-- Compares two tree maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.DTreeMap.Const.beq : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [BEq β] → Std.DTreeMap α (fun x => β) cmp → Std.DTreeMap α (fun x => β) cmp → Bool
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.inner_eq_zero : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) {i j : ι},
  i ≠ j → inner 𝕜 (b i) (b j) = 0
-- Init.Data.UInt.Basic
instLEUInt64 : LE UInt64
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_mod : ∀ (a b : UInt8), (a % b).toUInt32 = a.toUInt32 % b.toUInt32
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.mk_le_of_surjective : ∀ {α β : Type u} {f : α → β}, Function.Surjective f → Cardinal.mk β ≤ Cardinal.mk α
-- Mathlib.Data.DFinsupp.Defs
/-- **Alias** of `DFinsupp.filter_add_filter_not`. -/
DFinsupp.filter_pos_add_filter_neg : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (p : ι → Prop)
  [inst_1 : DecidablePred p], DFinsupp.filter p f + DFinsupp.filter (fun i => ¬p i) f = f
-- Mathlib.Logic.Small.Basic
small_prod : ∀ {α : Type u_1} {β : Type u_2} [Small.{w, u_1} α] [Small.{w, u_2} β], Small.{w, max u_2 u_1} (α × β)
-- Init.Prelude
/-- Boolean “and”, also known as conjunction. `and x y` can be written `x && y`.

The corresponding propositional connective is `And : Prop → Prop → Prop`, written with the `∧`
operator.

The Boolean `and` is a `@[macro_inline]` function in order to give it short-circuiting evaluation:
if `x` is `false` then `y` is not evaluated at runtime.


Conventions for notations in identifiers:

 * The recommended spelling of `&&` in identifiers is `and`.

 * The recommended spelling of `||` in identifiers is `or`. -/
Bool.and : Bool → Bool → Bool
-- Init.Data.Array.Lemmas
/-- Variant of `foldlM_append` with a side condition for the `stop` argument.  -/
Array.foldlM_append' : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] [LawfulMonad m] {f : β → α → m β} {b : β}
  {xs xs' : Array α} {stop : ℕ},
  stop = xs.size + xs'.size →
    Array.foldlM f b (xs ++ xs') 0 stop = do
      let init ← Array.foldlM f b xs
      Array.foldlM f init xs'
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.toOrderRingHom_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β], Function.Injective OrderRingIso.toOrderRingHom
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.orthogonalProjection_map : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {V₂ : Type u_4} {P₂ : Type u_5} [inst_3 : NormedAddCommGroup V₂]
  [inst_4 : InnerProductSpace 𝕜 V₂] [inst_5 : MetricSpace P] [inst_6 : NormedAddTorsor V P] [inst_7 : MetricSpace P₂]
  [inst_8 : NormedAddTorsor V₂ P₂] (s : AffineSubspace 𝕜 P) [inst_9 : Nonempty ↥s]
  [inst_10 : s.direction.HasOrthogonalProjection] (f : P →ᵃⁱ[𝕜] P₂)
  [inst_11 : (AffineSubspace.map f.toAffineMap s).direction.HasOrthogonalProjection] (p : P),
  ↑((EuclideanGeometry.orthogonalProjection (AffineSubspace.map f.toAffineMap s)) (f p)) =
    f ↑((EuclideanGeometry.orthogonalProjection s) p)
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit'.match_3.eq_4 : ∀ (motive : Lean.Expr → Sort u_1) (h_1 : (name : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const name us))
  (h_2 : (f x : Lean.Expr) → motive (f.app x))
  (h_3 :
    (binderName : Lean.Name) →
      (ty body : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName ty body binderInfo))
  (h_4 : Unit → motive (Lean.Expr.sort Lean.Level.zero)) (h_5 : (a : Lean.Level) → motive (Lean.Expr.sort a.succ))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (x : Lean.Expr) → motive x),
  (match Lean.Expr.sort Lean.Level.zero with
    | Lean.Expr.const name us => h_1 name us
    | f.app x => h_2 f x
    | Lean.Expr.forallE binderName ty body binderInfo => h_3 binderName ty body binderInfo
    | Lean.Expr.sort Lean.Level.zero => h_4 ()
    | Lean.Expr.sort a.succ => h_5 a
    | Lean.Expr.sort u => h_6 u
    | x => h_7 x) =
    h_4 ()
-- Mathlib.Data.Nat.Factorial.Cast
/-- Convenience lemma. The `a - 1` is not using truncated subtraction, as opposed to the definition
of `Nat.descFactorial` as a natural.  -/
Nat.cast_descFactorial_two : ∀ (S : Type u_1) [inst : Ring S] (a : ℕ), ↑(a.descFactorial 2) = ↑a * (↑a - 1)
-- Init.PropLemmas
dite_then_true : ∀ {p : Prop} [inst : Decidable p] {x : ¬p → Prop}, (if h : p then True else x h) ↔ ∀ (h : ¬p), x h
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_def : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin n → M), ∏ i, f i = (List.map f (List.finRange n)).prod
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.vadd.eq_1 : ∀ {M' : Type u_1} {α : Type u_2} [inst : AddZeroClass M'] [inst_1 : VAdd M' α] (S : AddSubmonoid M'),
  S.vadd = inferInstance
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_ofVal : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x : WithVal v), WithVal.toVal v x.ofVal = x
-- Mathlib.MeasureTheory.OuterMeasure.OfAddContent
MeasureTheory.AddContent.isCaratheodory_ofFunction_of_mem : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α},
  MeasureTheory.IsSetSemiring C →
    ∀ (m : MeasureTheory.AddContent ENNReal C),
      (∀ s ∉ C, m s = ⊤) → s ∈ C → (MeasureTheory.OuterMeasure.ofFunction ⇑m ⋯).IsCaratheodory s
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SymM : Type → Type
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.decidableMemCenter : {R : Type u} →
  [inst : NonUnitalRing R] → [DecidableEq R] → [Fintype R] → DecidablePred fun x => x ∈ NonUnitalSubring.center R
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    ∀ {fallback : γ k},
      Std.Internal.List.getValueCastD k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l)
          fallback =
        ((Std.Internal.List.getValueCast? k l).bind (f k)).getD fallback
-- Mathlib.Analysis.Convex.Body
ConvexBody.isCompact : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] (K : ConvexBody V),
  IsCompact ↑K
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.instOneHom : (X Y : MonCat) → One (X ⟶ Y)
-- Mathlib.Data.ENat.Pow
ENat.epow_left_mono : ∀ {y : ℕ∞}, Monotone fun x => x ^ y
-- Mathlib.Data.Nat.Choose.Basic
Nat.factorial_dvd_descFactorial : ∀ (n k : ℕ), k.factorial ∣ n.descFactorial k
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_eq_one : ∀ {α : Type u} [inst : One α] {a : α}, ↑a = 1 ↔ a = 1
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.revPositions.eq_1 : ∀ (s : String), s.revPositions = s.revPositionsFrom s.endPos
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
MeasureTheory.condExp_restrict_ae_eq_restrict : ∀ {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} {s : Set α} (hm : m ≤ m0)
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasurableSet s → MeasureTheory.Integrable f μ → (μ.restrict s)[f | m] =ᵐ[μ.restrict s] μ[f | m]
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- Composition as a linear map.  -/
ZeroAtInftyContinuousMap.compLinearMap : {β : Type v} →
  {γ : Type w} →
    {δ : Type u_2} →
      [inst : TopologicalSpace β] →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : TopologicalSpace δ] →
            [inst_3 : AddCommMonoid δ] →
              [inst_4 : ContinuousAdd δ] →
                {R : Type u_3} →
                  [inst_5 : Semiring R] →
                    [inst_6 : Module R δ] →
                      [inst_7 : ContinuousConstSMul R δ] →
                        CocompactMap β γ → ZeroAtInftyContinuousMap γ δ →ₗ[R] ZeroAtInftyContinuousMap β δ
-- Init.Data.List.Basic
List.elem_eq_true_of_mem : ∀ {α : Type u} [inst : BEq α] [ReflBEq α] {a : α} {as : List α}, a ∈ as → List.elem a as = true
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt),
  t.eTruncLTGEIsoGELT a b =
    (CategoryTheory.asIso (t.eTruncLTGELTSelfToLTGE a b)).symm ≪≫ CategoryTheory.asIso (t.eTruncLTGELTSelfToGELT a b)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.lift_cof_iSup : ∀ {β : Type v} [inst : LinearOrder β] [Small.{u, v} β] [NoMaxOrder β] {f : β → Ordinal.{u}},
  StrictMono f → Cardinal.lift.{v, u} (⨆ i, f i).cof = Cardinal.lift.{u, v} (Order.cof β)
-- Mathlib.GroupTheory.Frattini
/-- The Frattini subgroup of a group is the intersection of the maximal subgroups.  -/
frattini : (G : Type u_1) → [inst : Group G] → Subgroup G
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal
InnerProductGeometry.IsConformalMap.preserves_angle : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {f' : E →L[ℝ] F},
  IsConformalMap f' → ∀ (u v : E), InnerProductGeometry.angle (f' u) (f' v) = InnerProductGeometry.angle u v
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.fill.eq_1 : ∀ {α : Type u_1} (x : RBTree.RBNode α), RBTree.RBNode.Path.root.fill x = x
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiSeparated_isStableUnderComposition : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.QuasiSeparated
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_insert_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).size ≤ t.size + 1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A binary fan gives a binary cofan in the opposite category.  -/
CategoryTheory.Limits.BinaryFan.op : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → CategoryTheory.Limits.BinaryFan X Y → CategoryTheory.Limits.BinaryCofan (Opposite.op X) (Opposite.op Y)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instHashableLetValue.hash : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu → UInt64
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roc.size.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (lower : α) → motive (some lower)),
  (match none with
    | none => h_1 ()
    | some lower => h_2 lower) =
    h_1 ()
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_fun_neg : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.variance (fun ω => -X ω) μ = ProbabilityTheory.variance X μ
-- Mathlib.SetTheory.Ordinal.Commute
Ordinal.addCommute_iff_eq_mul_natCast : ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ ↔ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
-- Mathlib.Data.Finset.Empty
Finset.eq_empty_or_nonempty : ∀ {α : Type u_1} (s : Finset α), s = ∅ ∨ s.Nonempty
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- [Stacks Tag 00Z7](https://stacks.math.columbia.edu/tag/00Z7) -/
CategoryTheory.GrothendieckTopology.instInfSet : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → InfSet (CategoryTheory.GrothendieckTopology C)
-- Lean.Meta.Basic
Lean.Meta.instInhabitedDiagnostics.default : Lean.Meta.Diagnostics
-- Batteries.Data.Array.Scan
Array.scanlM.loop_toList : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} {as : Array α} {start : ℕ} {acc : Array β}
  [inst : Monad m] [LawfulMonad m] {f : β → α → m β} {stop : ℕ} (h : stop ≤ as.size),
  Array.toList <$> Array.scanlM.loop f init as start stop h acc = do
    let __do_lift ← List.scanlM f init (List.take (stop - start) (List.drop start as.toList))
    pure (acc.toList ++ __do_lift)
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.instIsRightAdjointSheafSubtypeCarrierMemGrothendieckTopologySheafRestrictOfOverOverOverPullback : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {X : TopCat} (U : TopologicalSpace.Opens ↑X)
  [((Opens.grothendieckTopology ↑X).overPullback A U).IsRightAdjoint], U.sheafRestrict.IsRightAdjoint
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- In a compact space, the space of probability measures is also compact.  -/
instCompactSpaceProbabilityMeasure : ∀ {E : Type u_1} [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  [CompactSpace E], CompactSpace (MeasureTheory.ProbabilityMeasure E)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Algebra.smulTower_leftMulMatrix : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring T]
  [inst_3 : Algebra R S] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [inst_6 : IsScalarTower R S T] {m : Type u_4}
  {n : Type u_5} [inst_7 : Fintype m] [inst_8 : Fintype n] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n]
  (b : Module.Basis m R S) (c : Module.Basis n S T) (x : T) (ik jk : m × n),
  (Algebra.leftMulMatrix (b.smulTower c)) x ik jk =
    (Algebra.leftMulMatrix b) ((Algebra.leftMulMatrix c) x ik.2 jk.2) ik.1 jk.1
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNClique.mk : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α}, G.IsClique ↑s → s.card = n → G.IsNClique n s
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeffAddEquiv_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (self : MonoidAlgebra R M),
  MonoidAlgebra.coeffAddEquiv self = self.coeff
-- Init.Data.Array.Lex.Lemmas
Array.singleton_lex_singleton : ∀ {α : Type u_1} {a b : α} [inst : BEq α] {lt : α → α → Bool}, #[a].lex #[b] lt = lt a b