mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Constants.term.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (c : L.Constants), c.term = FirstOrder.Language.func c default
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.growsPolynomially_id : AkraBazziRecurrence.GrowsPolynomially fun x => x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.baseChange_add : ∀ {R : Type r} {S : Type s} {F : Type u} {K : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field F]
  [inst_3 : Field K] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R F]
  [inst_6 : Algebra S F] [IsScalarTower R S F] [inst_8 : Algebra R K] [inst_9 : Algebra S K] [IsScalarTower R S K]
  (f : F →ₐ[S] K) {P Q : Fin 3 → F},
  (W'.baseChange F).Nonsingular P →
    (W'.baseChange F).Nonsingular Q → (W'.baseChange K).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (W'.baseChange F).add P Q
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Submodule.finrank_strictMono : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V], StrictMono fun s => Module.finrank K ↥s
-- Mathlib.Tactic.MoveAdd
/-- `unifyMovements` takes as input
* an array of `Expr × Bool × Syntax`, as in the output of `parseArrows`,
* the `Name` `op` of a binary operation,
* an `Expr`ession `tgt`.

It unifies each `Expr`ession appearing as a first factor of the array with the atoms
for the operation `op` in the expression `tgt`, returning
* the lists of pairs of a matched subexpression with the corresponding `Bool`ean;
* a pair of a list of error messages and the corresponding list of Syntax terms where the error
  should be thrown;
* an array of debugging messages.
 -/
Mathlib.MoveAdd.unifyMovements : Lean.Name →
  Array (Lean.Expr × Bool × Lean.Syntax) →
    Lean.Expr →
      Lean.MetaM (List (Lean.Expr × Bool) × (List Lean.MessageData × List Lean.Syntax) × Array Lean.MessageData)
-- Lean.Declaration
Lean.instInhabitedQuotVal.default : Lean.QuotVal
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertManyIfNew!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ ((a : α) × β a)]
  (t : Std.DTreeMap.Internal.Impl α β) (l : ρ),
  t.insertManyIfNew! l =
    (have r := ⟨t, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, b⟩ =>
              have r := ⟨Std.DTreeMap.Internal.Impl.insertIfNew! a b ↑r, ⋯⟩;
              pure (ForInStep.yield r)
      have r : t.IteratedSlowNewInsertionInto := __s
      pure r).run
-- Mathlib.RingTheory.Algebraic.Basic
isAlgebraic_iff_not_injective : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x : A},
  IsAlgebraic R x ↔ ¬Function.Injective ⇑(Polynomial.aeval x)
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.aeval_sumElim_pderiv_inl : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {S : Type u_1} {τ : Type u_2} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (j : σ),
  (MvPolynomial.aeval (Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ f))) ((MvPolynomial.pderiv (Sum.inl j)) p) =
    (MvPolynomial.pderiv j) ((MvPolynomial.aeval (Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ f))) p)
-- Init.System.IOError
IO.Error.resourceVanished.injEq : ∀ (osCode : UInt32) (details : String) (osCode_1 : UInt32) (details_1 : String),
  (IO.Error.resourceVanished osCode details = IO.Error.resourceVanished osCode_1 details_1) =
    (osCode = osCode_1 ∧ details = details_1)
-- Std.Time.Format
Std.Time.PlainDateTime.instToString : ToString Std.Time.PlainDateTime
-- Init.Data.List.Impl
/-- Tail recursive implementation of `findRev?`. This is only used at runtime.  -/
List.findRev?TR : {α : Type u_1} → (α → Bool) → List α → Option α
-- Mathlib.Order.Filter.ENNReal
NNReal.limsup_of_not_isBoundedUnder : ∀ {ι : Type u_1} {f : Filter ι} {u : ι → NNReal},
  ¬Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u → Filter.limsup u f = 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
/-- This is an intermediate result; use the more general `CFC.concaveOn_nnrpow` instead.  -/
_private.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order.0.CFC.concaveOn_nnrpow_Ioo : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {p : NNReal},
  p ∈ Set.Ioo 0 1 → ConcaveOn ℝ (Set.Ici 0) fun a => a ^ p
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.starPullbackIsoStar_hom_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (X_1 : C),
  ((CategoryTheory.Over.starPullbackIsoStar f).hom.app X_1).left =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.map
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (Y ⨯ X_1)))
          CategoryTheory.Limits.prod.fst)
        f CategoryTheory.Limits.prod.fst f (CategoryTheory.CategoryStruct.id (Y ⨯ X_1))
        (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) ⋯ ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.prod.fst f).hom
        (CategoryTheory.Limits.pullbackProdFstIsoProd f X_1).hom)
-- Mathlib.Data.Sym.Basic
SymOptionSuccEquiv.encode_of_none_notMem : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (s : Sym (Option α) n.succ) (h : none ∉ s),
  SymOptionSuccEquiv.encode s = Sum.inr (Sym.map (fun o => (↑o).get ⋯) s.attach)
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : DenselyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F) {r : NNReal}, r < ‖f‖₊ → ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
-- Mathlib.Topology.Compactness.Lindelof
mem_coclosedLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  s ∈ Filter.coclosedLindelof X ↔ ∃ t, IsClosed t ∧ IsLindelof t ∧ tᶜ ⊆ s
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m₁ ∩ m₂)[k]? = if k ∈ m₂ then m₁[k]? else none
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_smul : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {R : Type u_4} [inst_3 : SMul R K] [inst_4 : SMul R L] [inst_5 : IsScalarTower R K L] (r : R) (x : ↥S),
  ↑(r • x) = r • ↑x
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.univ_ne_zero : Cardinal.univ.{u, v} ≠ 0
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- The additive bijection `Ext X Y 0 ≃+ (X ⟶ Y)`.  -/
CategoryTheory.Abelian.Ext.addEquiv₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] → {X Y : C} → CategoryTheory.Abelian.Ext X Y 0 ≃+ (X ⟶ Y)
-- Mathlib.Order.CompleteLattice.Basic
/-- A version of `iInf_option` useful for rewriting right-to-left.  -/
iInf_option_elim : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (a : α) (f : β → α), ⨅ o, o.elim a f = a ⊓ ⨅ b, f b
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- The image of a connected component in a totally disconnected space is a singleton.  -/
Continuous.image_connectedComponent_eq_singleton : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] [TotallyDisconnectedSpace β]
  {f : α → β}, Continuous f → ∀ (a : α), f '' connectedComponent a = {f a}
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.self_mem_ordConnectedComponent : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α}, x ∈ s.ordConnectedComponent x ↔ x ∈ s
-- Mathlib.Combinatorics.SimpleGraph.Diam
/-- The eccentricity of a vertex is the greatest distance between it and any other vertex.  -/
SimpleGraph.eccent : {α : Type u_1} → SimpleGraph α → α → ℕ∞
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsClosedUnderBinaryProductsOfIsTriangulatedOfIsClosedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] [P.IsClosedUnderIsomorphisms], P.IsClosedUnderBinaryProducts
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.coe_neg : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [inst_7 : IsTopologicalAddGroup N], ⇑(-f) = -⇑f
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instLaxMonoidalActionTypeLinearization : (k : Type u) → (G : Type v) → [inst : CommRing k] → [inst_1 : Monoid G] → (Rep.linearization k G).LaxMonoidal
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.instFinitePrimeSpectrum : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R], Finite (PrimeSpectrum R)
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- The category under any object `X` factors through the category under the initial object `I`.  -/
CategoryTheory.Under.forgetMapInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      {I : C} →
        (hI : CategoryTheory.Limits.IsInitial I) →
          CategoryTheory.Under.forget X ≅
            (CategoryTheory.Under.map (hI.to X)).comp (CategoryTheory.Under.equivalenceOfIsInitial hI).functor
-- Mathlib.Data.Bool.Count
List.IsChain.count_not_cons : ∀ {b : Bool} {l : List Bool},
  List.IsChain (fun x1 x2 => x1 ≠ x2) (b :: l) → List.count (!b) l = List.count b l + l.length % 2
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_le' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α}, a ∈ s → sInf s ≤ a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h₁ : t₁.WF)
  (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₂.get k ⋯
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.mk : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] → (toSubgroup : Subgroup G) → IsOpen toSubgroup.carrier → OpenSubgroup G
-- Std.Http.Transport
/-- Sends a single ByteArray through a channel.
 -/
Std.Http.Internal.Mock.send : Std.CloseableChannel ByteArray → ByteArray → Std.Async.Async Unit
-- Mathlib.Topology.ContinuousMap.Basic
/-- Descend a continuous map, which is constant on the fibres, along a quotient map.  -/
Topology.IsQuotientMap.lift : {X : Type u_1} →
  {Y : Type u_2} →
    {Z : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] →
            {f : C(X, Y)} → Topology.IsQuotientMap ⇑f → (g : C(X, Z)) → Function.FactorsThrough ⇑g ⇑f → C(Y, Z)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActivateNextGuardResult.ready : Lean.Meta.Grind.ActivateNextGuardResult
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.IsMaximal.mem_of_models : ∀ {L : FirstOrder.Language} {T : L.Theory}, T.IsMaximal → ∀ {φ : L.Sentence}, T ⊨ᵇ φ → φ ∈ T
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piEquivLim.congr_simp : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [inst : LinearOrder ι]
  {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} {equiv equiv_1 : (j : ↑(Set.Iio i)) → F ↑j ≃ InverseSystem.piLT X ↑j}
  (e_equiv : equiv = equiv_1) (nat : InverseSystem.IsNatEquiv f equiv)
  (equivLim equivLim_1 : F i ≃ ↑(InverseSystem.limit f i)),
  equivLim = equivLim_1 →
    ∀ (hi : Order.IsSuccPrelimit i) (j : ↑(Set.Iic i)),
      InverseSystem.piEquivLim nat equivLim hi j = InverseSystem.piEquivLim ⋯ equivLim_1 hi j
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.setRed.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2)
  (h_1 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) → (v : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node c a v b))
  (h_2 : Unit → motive RBTree.RBNode.nil),
  (match RBTree.RBNode.nil with
    | RBTree.RBNode.node c a v b => h_1 c a v b
    | RBTree.RBNode.nil => h_2 ()) =
    h_2 ()
-- Init.Data.Fin.Lemmas
Fin.addNat_one : ∀ {n : ℕ} {i : Fin n}, i.addNat 1 = i.succ
-- Mathlib.CategoryTheory.Galois.Basic
/-- A morphism from an object `X` with non-empty fiber to a connected object `A` is an
epimorphism.  -/
CategoryTheory.PreGaloisCategory.epi_of_nonempty_of_isConnected : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A : C}
  [CategoryTheory.PreGaloisCategory.IsConnected A] [h : Nonempty (F.obj X).obj] (f : X ⟶ A), CategoryTheory.Epi f
-- Mathlib.Analysis.Analytic.Linear
analyticWithinAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {z : E}, AnalyticWithinAt 𝕜 id s z
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective : ∀ (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) (x : ↑D.glued.toTopCat),
  ∃ i y, (CategoryTheory.ConcreteCategory.hom (D.ι i).base) y = x
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_iSizeToInt : ∀ (x : ISize) {h₁ : Int8.minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ Int8.maxValue.toInt},
  Int8.ofIntLE x.toInt h₁ h₂ = x.toInt8
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.inclusion.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M} (h : S ≤ T),
  Submonoid.inclusion h = S.subtype.codRestrict T ⋯
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.piUnique_apply : ∀ {α : Type u_9} [inst : Unique α] (R : Type u_10) [inst_1 : Semiring R] (f : α → Type u_11)
  [inst_2 : (x : α) → AddCommMonoid (f x)] [inst_3 : (x : α) → Module R (f x)],
  ⇑(LinearEquiv.piUnique R f) = (Equiv.piUnique f).toFun
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ringEq.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) (lhs : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ringEq c lhs) = 1 + sizeOf c + sizeOf lhs
-- Mathlib.Topology.Order.OrderClosed
Ioc_mem_nhdsLE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a < b → Set.Ioc a b ∈ nhdsWithin b (Set.Iic b)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_inter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β k},
        (m₁.inter! m₂).getD k fallback =
          if Std.DTreeMap.Internal.Impl.contains k m₂ = true then m₁.getD k fallback else fallback
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_right_le_size_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₂.size ≤ (m₁ ∪ m₂).size
-- Std.Do.Triple.Basic
/-- Modus ponens for two Hoare triple specifications of a program `x`.
This theorem is useful for separating proofs. If `h₁ : Triple x P₁ Q₁` proves a basic property about
`x` and `h₂ : Triple x P₂ (Q₁ →ₚ Q₂)` is an advanced proof for `Q₂` that builds on the basic proof
for `Q₁`, then `mp x h₁ h₂` is a proof for `Q₂` about `x`.
 -/
Std.Do.Triple.mp : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {P₁ : Std.Do.Assertion ps} {Q₁ : Std.Do.PostCond α ps}
  {P₂ : Std.Do.Assertion ps} {Q₂ : Std.Do.PostCond α ps} [inst : Std.Do.WP m ps] (x : m α),
  ⦃P₁⦄ x ⦃Q₁⦄ → ⦃P₂⦄ x ⦃Q₁.imp Q₂⦄ → ⦃P₁ ∧ P₂⦄ x ⦃Q₁.and Q₂⦄
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp_compQuasiMeasurePreserving : ∀ {α : Type u_1} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace γ] {β : Type u_5} [inst_3 : MeasurableSpace β]
  {ν : MeasureTheory.Measure β} (g : γ → δ) (hg : Continuous g) (f : β →ₘ[ν] γ) {φ : α → β}
  (hφ : MeasureTheory.Measure.QuasiMeasurePreserving φ μ ν),
  (MeasureTheory.AEEqFun.comp g hg f).compQuasiMeasurePreserving φ hφ =
    MeasureTheory.AEEqFun.comp g hg (f.compQuasiMeasurePreserving φ hφ)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If `s` is a colimit cofork over `f` and `g`, then a morphism `k : Y ⟶ W` satisfying
`f ≫ k = g ≫ k` induces a morphism `l : s.pt ⟶ W` such that `cofork.π s ≫ l = k`.  -/
CategoryTheory.Limits.Cofork.IsColimit.desc : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {s : CategoryTheory.Limits.Cofork f g} →
          CategoryTheory.Limits.IsColimit s →
            {W : C} →
              (k : Y ⟶ W) → CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k → (s.pt ⟶ W)
-- Mathlib.Data.Set.Functor
Set.seqRight_def : ∀ {α β : Type u} (s : Set α) (t : Set β), s *> t = {a | s.Nonempty ∧ a ∈ t}
-- Mathlib.Topology.Algebra.OpenSubgroup
Subgroup.subgroupOf_isOpen : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (U K : Subgroup G), IsOpen ↑K → IsOpen ↑(K.subgroupOf U)
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.liftEquiv_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : PerfectRing M p]
  [inst_6 : IsPRadical i p] [inst_7 : ExpChar L p], (PerfectRing.liftEquiv M i p) j = PerfectRing.lift i j p
-- Mathlib.Algebra.Field.Opposite
MulOpposite.instRatCast : {α : Type u_1} → [RatCast α] → RatCast αᵐᵒᵖ
-- Mathlib.RingTheory.PowerSeries.Basic
/-- Formal power series over a coefficient type `R`  -/
PowerSeries : Type u_1 → Type (max u_1 0)
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `UInt32.ofNat 5 = 5`
* `UInt32.ofNat 65539 = 65539`
* `UInt32.ofNat 4_294_967_299 = 3`
 -/
UInt32.ofNat : ℕ → UInt32
-- Init.Data.Array.Lemmas
/-- Variant of `any_filterMap` with a side condition for the `stop` argument.  -/
Array.any_filterMap' : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {xs : Array α} {f : α → Option β} {p : β → Bool},
  stop = (Array.filterMap f xs).size →
    (Array.filterMap f xs).any p 0 stop =
      xs.any fun a =>
        match f a with
        | some b => p b
        | none => false
-- Mathlib.RingTheory.Valuation.Discrete.RankOne
/-- A discrete valuation has rank one.  -/
Valuation.IsRankOneDiscrete.rankOne : {Γ : Type u_1} →
  [inst : LinearOrderedCommGroupWithZero Γ] →
    {R : Type u_2} →
      [inst_1 : Ring R] → (v : Valuation R Γ) → [hv : v.IsRankOneDiscrete] → {e : NNReal} → 1 < e → v.RankOne
-- Mathlib.Order.InitialSeg
InitialSeg.le_apply_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a : α} {b : β} [inst_1 : PartialOrder α] (f : α ≤i β),
  b ≤ f a ↔ ∃ c ≤ a, f c = b
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.denest.eq_1 : ∀ (p : DyckWord) (hn : p.IsNested),
  p.denest hn = { toList := (↑p).dropLast.tail, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }
-- Mathlib.CategoryTheory.IsoCat
/-- The bijection on objects induced by a functor that is an isomorphism of categories.  -/
CategoryTheory.Functor.objEquiv : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → (F : CategoryTheory.Functor C D) → [F.IsIso] → C ≃ D
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.takeWhile_eq_filter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {bound : α} {l : List ((a : α) × β a)}
  {l_ordered : List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l},
  List.takeWhile (fun e => (compare e.fst bound).isLT) l = List.filter (fun e => (compare e.fst bound).isLT) l
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- The terminal object of `Top` is `PUnit`.  -/
TopCat.isTerminalPUnit : CategoryTheory.Limits.IsTerminal (TopCat.of PUnit.{u + 1})
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.comap_sectR : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : α) {f : δ → β}
  (hf : Measurable f), (κ.sectR a).comap f hf = κ.comap (fun d => (a, f d)) ⋯
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_nsmul : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → AddMonoid (G i)] [inst_3 : ∀ (i : ι), AddSubmonoidClass (S i) (G i)]
  (i : ι) (r : G i) (n : ℕ), RestrictedProduct.single A i (n • r) = n • RestrictedProduct.single A i r
-- Lean.LibrarySuggestions.Basic
/-- A premise whose name has one of the following components is not retrieved.

Use `run_cmd modifyEnv fun env => nameDenyListExt.addEntry env name` to add a name to the deny list.
 -/
Lean.LibrarySuggestions.nameDenyListExt : Lean.SimplePersistentEnvExtension String (List String)
-- Mathlib.Order.OrdContinuous
OrderIso.leftOrdContinuous : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β), LeftOrdContinuous ⇑e
-- Mathlib.Algebra.Free
FreeSemigroup.instDecidableEq : {α : Type u} → [DecidableEq α] → DecidableEq (FreeSemigroup α)
-- Mathlib.Topology.Separation.LinearUpperLowerSetTopology
instCompletelyNormalSpaceOfIsLowerSet : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [Topology.IsLowerSet α], CompletelyNormalSpace α
-- Mathlib.FieldTheory.Galois.Basic
/-- See `InfiniteGalois.mem_range_algebraMap_iff_fixed` for the infinite case,
i.e. without the `[FiniteDimensional F E]` assumption.  -/
IsGalois.mem_range_algebraMap_iff_fixed : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [IsGalois F E]
  [FiniteDimensional F E] (x : E), x ∈ Set.range ⇑(algebraMap F E) ↔ ∀ (f : Gal(E/F)), f x = x
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- Some repackaging:
the presheaf of functions satisfying `continuousPrelocal` is just the same thing as
the presheaf of continuous functions.
 -/
TopCat.subpresheafContinuousPrelocalIsoPresheafToTop : {X : TopCat} → (T : TopCat) → TopCat.subpresheafToTypes (X.continuousPrelocal ↑T) ≅ X.presheafToTop T
-- Mathlib.Combinatorics.Colex
/-- For finsets of naturals, the colexicographic order is equivalent to the order induced by the
`n`-ary expansion.  -/
Finset.geomSum_lt_geomSum_iff_toColex_lt_toColex : ∀ {s t : Finset ℕ} {n : ℕ}, 2 ≤ n → (∑ i ∈ s, n ^ i < ∑ i ∈ t, n ^ i ↔ toColex s < toColex t)
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.growsPolynomially_rpow : ∀ (p : ℝ), AkraBazziRecurrence.GrowsPolynomially fun x => x ^ p
-- Mathlib.Order.Heyting.Basic
fst_sdiff : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiff α] [inst_1 : SDiff β] (a b : α × β), (b \ a).1 = b.1 \ a.1
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.State.mctx : Lean.MetavarContext.LevelMVarToParam.State → Lean.MetavarContext