mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Calculus
HasFDerivAt.norm_sq : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {G : Type u_4}
  [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {x : G} {f : G → F} {f' : G →L[ℝ] F},
  HasFDerivAt f f' x → HasFDerivAt (fun x => ‖f x‖ ^ 2) (2 • (innerSL ℝ) (f x) ∘SL f') x
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- A monad equipped with the ability to construct `HorizontalComp` terms.  -/
Mathlib.Tactic.BicategoryLike.MonadHorizontalComp : (Type → Type) → Type
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.edist_le_infEDist_add_ediam : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {s : Set α},
  y ∈ s → edist x y ≤ Metric.infEDist x s + Metric.ediam s
-- Init.Data.Option.Lemmas
Option.pfilter.eq_1 : ∀ {α : Type u_1} (p_2 : (a : α) → none = some a → Bool), none.pfilter p_2 = none
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.isOrdered.eq_3 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (l r : Option α) (c : RBTree.RBColor) (l_1 : RBTree.RBNode α) (v : α)
  (r_1 : RBTree.RBNode α),
  RBTree.RBNode.isOrdered cmp (RBTree.RBNode.node c l_1 v r_1) l r =
    (RBTree.RBNode.isOrdered cmp l_1 l (some v) && RBTree.RBNode.isOrdered cmp r_1 (some v) r)
-- Mathlib.CategoryTheory.Limits.Types.Images
/-- Auxiliary lemma. Use `limit_of_surjections_surjective` instead.  -/
CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux : ∀ {F : CategoryTheory.Functor ℕᵒᵖ (Type u)},
  (∀ (n : ℕ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op))) →
    Function.Surjective
      ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.Types.limitCone F).π.app (Opposite.op 0)))
-- Mathlib.Combinatorics.Quiver.Schreier
/-- The quiver structure on a Schreier graph. An arrow from `x` to `y` exists when
there is an `s : S` such that `(ι s) • x = y`.  -/
Quiver.SchreierGraph.schreierGraphQuiver : (V : Type u_1) → {M : Type u_2} → [inst : SMul M V] → {S : Type u_3} → (ι : S → M) → Quiver (Quiver.SchreierGraph V ι)
-- Mathlib.Data.PNat.Find
PNat.find_eq_one : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n), PNat.find h = 1 ↔ p 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = (t.getKey? a).isSome
-- Mathlib.SetTheory.ZFC.Class
/-- Convert a conglomerate (a collection of classes) into a class  -/
Class.congToClass : Set Class.{u} → Class.{u}
-- Init.Data.Int.Gcd
Int.dvd_gcd_iff : ∀ {a b : ℤ} {c : ℕ}, c ∣ a.gcd b ↔ ↑c ∣ a ∧ ↑c ∣ b
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.brecOn.go : {motive_1 : Lean.Meta.Match.Example → Sort u} →
  {motive_2 : List Lean.Meta.Match.Example → Sort u} →
    (t : Lean.Meta.Match.Example) →
      ((t : Lean.Meta.Match.Example) → t.below → motive_1 t) →
        ((t : List Lean.Meta.Match.Example) → Lean.Meta.Match.Example.below_1 t → motive_2 t) → motive_1 t ×' t.below
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.iCycles.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ),
  X.iCycles f g n = CategoryTheory.Limits.kernel.ι (X.δ f g n (n + 1) ⋯)
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.subterminalInclusion_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C]
  {X Y : CategoryTheory.InducedCategory C CategoryTheory.ObjectProperty.FullSubcategory.obj} (f : X ⟶ Y),
  (CategoryTheory.subterminalInclusion C).map f = f.hom
-- Mathlib.Probability.Distributions.Beta
/-- The beta pdf is positive for all positive reals with positive parameters.  -/
ProbabilityTheory.betaPDFReal_pos : ∀ {α β x : ℝ}, 0 < x → x < 1 → 0 < α → 0 < β → 0 < ProbabilityTheory.betaPDFReal α β x
-- Init.Data.Vector.Lemmas
Vector.contains_flatten : ∀ {α : Type u_1} {n m : ℕ} [inst : BEq α] {xs : Vector (Vector α n) m} {x : α},
  xs.flatten.contains x = xs.any fun xs => xs.contains x
-- Mathlib.Algebra.Group.Action.Defs
/-- Pushforward an additive action along a surjective map respecting `+ᵥ`.  -/
Function.Surjective.addAction : {M : Type u_1} →
  {α : Type u_5} →
    {β : Type u_6} →
      [inst : AddMonoid M] →
        [inst_1 : AddAction M α] →
          [inst_2 : VAdd M β] →
            (f : α → β) → Function.Surjective f → (∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) → AddAction M β
-- Init.Data.String.Search
/-- Finds the position of the first match of the pattern `pattern` in after the position
`pos`. If there is no match `s.endPos` is returned.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".toSlice.startPos.find Char.isWhitespace).get! == ' '`

* `("tea".toSlice.pos ⟨1⟩ (by decide)).find (fun (c : Char) => c == 't') == "tea".toSlice.endPos`
 -/
String.Slice.Pos.find : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        {s : String.Slice} → s.Pos → (pattern : ρ) → [String.Slice.Pattern.ToForwardSearcher pattern σ] → s.Pos
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.comp_apply : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥X),
  (CategoryTheory.CategoryStruct.comp f g) x = g (f x)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.semigroup : {I : Type u} → {f : I → Type v₁} → [(i : I) → Semigroup (f i)] → Semigroup ((i : I) → f i)
-- Mathlib.Algebra.Group.Semiconj.Units
AddSemiconjBy.addUnits_neg_symm_left_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {a : AddUnits M} {x y : M}, AddSemiconjBy (↑(-a)) y x ↔ AddSemiconjBy (↑a) x y
-- Mathlib.ModelTheory.DirectLimit
_private.Mathlib.ModelTheory.DirectLimit.0.FirstOrder.Language.«termΣˣ» : Lean.ParserDescr
-- Mathlib.Order.CompleteLattice.Chain
ChainClosure.succ : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, ChainClosure r s → ChainClosure r (SuccChain r s)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β},
  (m.alter k f).getD k' fallback = if (k == k') = true then (f m[k]?).getD fallback else m.getD k' fallback
-- Mathlib.Data.Finset.Sigma
Finset.mem_sigma : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} {a : (i : ι) × α i},
  a ∈ s.sigma t ↔ a.fst ∈ s ∧ a.snd ∈ t a.fst
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.brecOn_3.eq : ∀ {motive_1 : Lean.Lsp.DocumentSymbol → Sort u} {motive_2 : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol → Sort u}
  {motive_3 : Option (Array Lean.Lsp.DocumentSymbol) → Sort u} {motive_4 : Array Lean.Lsp.DocumentSymbol → Sort u}
  {motive_5 : List Lean.Lsp.DocumentSymbol → Sort u} (t : Array Lean.Lsp.DocumentSymbol)
  (F_1 : (t : Lean.Lsp.DocumentSymbol) → t.below → motive_1 t)
  (F_2 : (t : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_1 t → motive_2 t)
  (F_3 : (t : Option (Array Lean.Lsp.DocumentSymbol)) → Lean.Lsp.DocumentSymbol.below_2 t → motive_3 t)
  (F_4 : (t : Array Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_3 t → motive_4 t)
  (F_5 : (t : List Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_4 t → motive_5 t),
  Lean.Lsp.DocumentSymbol.brecOn_3 t F_1 F_2 F_3 F_4 F_5 =
    F_4 t (Lean.Lsp.DocumentSymbol.brecOn_3.go t F_1 F_2 F_3 F_4 F_5).2
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.matchAt?_cast : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} (hst : s.copy = t.copy)
  {startPos : s.Pos},
  String.Slice.Pattern.Model.matchAt? pat (startPos.cast hst) =
    Option.map (fun x => x.cast hst) (String.Slice.Pattern.Model.matchAt? pat startPos)
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.instBot : (R : Type u_1) → [inst : NonUnitalNonAssocRing R] → Bot (TwoSidedIdeal R)
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.Section.equivComp_apply : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G} (σ : S.Section)
  (equiv : S.Equiv S') (a : G), (σ.equivComp equiv) a = equiv (σ a)
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.instCountableSymbolsWithConstants : ∀ {L : FirstOrder.Language} {α : Type u'} [Countable α] [Countable L.Symbols], Countable (L.withConstants α).Symbols
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m] {Z : C}
  (h_1 : CategoryTheory.Subobject.underlying.obj h.Ω₀ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (h.iso m).inv.hom)
      (CategoryTheory.CategoryStruct.comp (h.π m) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.pullbackπ (h.χ m) h.Ω₀) h_1
-- Mathlib.RingTheory.Ideal.Operations
Submodule.comap_smul'' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type w}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {f : M →ₗ[R] M'},
  Function.Injective ⇑f →
    ∀ {p : Submodule R M'}, p ≤ f.range → ∀ {I : Ideal R}, Submodule.comap f (I • p) = I • Submodule.comap f p
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.diff_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → (t₁ \ t₃).Equiv (t₂ \ t₃)
-- Mathlib.GroupTheory.PushoutI
/-- The underlying set, containing exactly one element of each coset of the base group  -/
Monoid.PushoutI.NormalWord.Transversal.set : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] → {φ : (i : ι) → H →* G i} → Monoid.PushoutI.NormalWord.Transversal φ → (i : ι) → Set (G i)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- A choice of limit cone for a functor `F : J ⥤ TopCat`.
Generally you should just use `limit.cone F`, unless you need the actual definition
(which is in terms of `Types.limitCone`).
 -/
TopCat.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → (F : CategoryTheory.Functor J TopCat) → CategoryTheory.Limits.Cone F
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.mk.inj : ∀ {G : Type u_1} {inst : CommGroup G} {toSubmonoid : Submonoid G}
  {eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a ∈ toSubmonoid.carrier → a⁻¹ ∈ toSubmonoid.carrier → a = 1}
  {toSubmonoid_1 : Submonoid G}
  {eq_one_of_mem_of_inv_mem'_1 : ∀ {a : G}, a ∈ toSubmonoid_1.carrier → a⁻¹ ∈ toSubmonoid_1.carrier → a = 1},
  { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem' } =
      { toSubmonoid := toSubmonoid_1, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'_1 } →
    toSubmonoid = toSubmonoid_1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.existsProp.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Lean.Meta.Grind.SplitSource.existsProp e) = 1 + sizeOf e
-- Aesop.Forward.State
Aesop.ForwardState.instToMessageData : Lean.ToMessageData Aesop.ForwardState
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If three points lie in the affine span of two points, the first four points are collinear.  -/
collinear_insert_insert_insert_left_of_mem_affineSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ p₄ p₅ : P},
  p₁ ∈ line[k, p₄, p₅] → p₂ ∈ line[k, p₄, p₅] → p₃ ∈ line[k, p₄, p₅] → Collinear k {p₁, p₂, p₃, p₄}
-- Mathlib.Tactic.NormNum.Irrational
Mathlib.Meta.NormNum.NotPowerCertificate.mk : {m n : Q(ℕ)} →
  (k : Q(ℕ)) → Q(«$k» ^ «$n» < «$m») → Q(«$m» < («$k» + 1) ^ «$n») → Mathlib.Meta.NormNum.NotPowerCertificate m n
-- Mathlib.Lean.MessageData.Trace
/-- Determine the status of a trace node from its rendered header string.

`withTraceNode` prepends `checkEmoji`/`crossEmoji`/`bombEmoji`
(defined in `Lean.Util.Trace`) to trace headers to indicate outcomes.

The `TraceResult` will be recorded in trace messages directly in [lean4#12698](https://github.com/leanprover/lean4/pull/12698).
Once that PR is available, callers should prefer `td.result?` over calling this function.  -/
Lean.MessageData.traceResultOf : String → Option Lean.TraceResult
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_eq_det_toMatrix_of_finset : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M]
  [inst_3 : DecidableEq M] {s : Finset M} (b : Module.Basis (↥s) A M) (f : M →ₗ[A] M),
  LinearMap.det f = ((LinearMap.toMatrix b b) f).det
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.localization_comap_injective : ∀ {R : Type u} (S : Type v) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Submonoid R)
  [IsLocalization M S], Function.Injective (PrimeSpectrum.comap (algebraMap R S))
-- Mathlib.Topology.Order.OrderClosed
Icc_mem_nhdsLE_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b c : α},
  b ∈ Set.Ioc a c → Set.Icc a c ∈ nhdsWithin b (Set.Iic b)
-- Init.Core
not_not_not : ∀ {a : Prop}, ¬¬¬a ↔ ¬a
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.lowerBoundP?_mem_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x : α} {t : RBTree.RBSet α cmp},
  t.lowerBoundP? cut = some x → x ∈ t.toList
-- Lean.Widget.InteractiveGoal
/-- If true, the hypothesis was not present on the previous tactic state.
Only present in tactic-mode goals.  -/
Lean.Widget.InteractiveHypothesisBundle.isInserted? : Lean.Widget.InteractiveHypothesisBundle → Option Bool
-- Mathlib.Algebra.FreeAlgebra.Cardinality
FreeAlgebra.cardinalMk_eq_one : ∀ (R : Type u) [inst : CommSemiring R] (X : Type v) [Subsingleton R], Cardinal.mk (FreeAlgebra R X) = 1
-- Mathlib.Algebra.Lie.OfAssociative
LieSubalgebra.ad_comp_incl_eq : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (K : LieSubalgebra R L)
  (x : ↥K), (LieAlgebra.ad R L) ↑x ∘ₗ ↑K.incl = ↑K.incl ∘ₗ (LieAlgebra.ad R ↥K) x
-- Batteries.Linter.UnnecessarySeqFocus
/-- Search for tactic executions in the info tree and remove executed tactic syntaxes.  -/
Batteries.Linter.UnnecessarySeqFocus.markUsedTacticsList : Lean.Environment → {ω : Type} → Lean.PersistentArray Lean.Elab.InfoTree → Batteries.Linter.UnnecessarySeqFocus.M ω Unit
-- Init.RCases
/-- A multi argument binder `(pat1 pat2 : ty)` binds a list of patterns and gives them all type `ty`.
 -/
Lean.Parser.Tactic.rintroPat.binder : Lean.ParserDescr
-- Aesop.Script.SpecificTactics
Aesop.tryCasesS : Lean.MVarId → Lean.FVarId → Array Aesop.CtorNames → Aesop.ScriptM (Option (Array Lean.Meta.CasesSubgoal))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β}, k ∉ m₁ → (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback
-- Mathlib.Analysis.Normed.Operator.Banach
instInhabitedNonlinearRightInverseToContinuousLinearMap : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NontriviallyNormedField 𝕜'] →
        {σ : 𝕜 →+* 𝕜'} →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {F : Type u_4} →
                  [inst_4 : NormedAddCommGroup F] →
                    [inst_5 : NormedSpace 𝕜' F] →
                      {σ' : 𝕜' →+* 𝕜} →
                        [inst_6 : RingHomInvPair σ σ'] →
                          [RingHomIsometric σ'] →
                            [inst_8 : RingHomInvPair σ' σ] → (f : E ≃SL[σ] F) → Inhabited (↑f).NonlinearRightInverse
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.foldM_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w}
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [inst_4 : Monad o]
  [LawfulMonad m] [LawfulMonad n] [inst_7 : Std.Internal.Do.Assertion Pred] [inst_8 : Std.Internal.Do.Assertion EPred]
  [inst_9 : Std.Internal.Do.WPMonad o Pred EPred] [inst_10 : Std.IteratorLoop α m n] [inst_11 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o] [inst_14 : MonadLiftT m n] [inst_15 : MonadLiftT n o]
  [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : δ → γ → o δ}
  {init : δ} {it : Std.IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b => do
          let __x ← liftM (f b).run
          match __x with
            | some c => g d c
            | x => pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.IterM.filterMapWithPostcondition f it) ⦃ Q; eQ ⦄
-- Batteries.Data.String.Lemmas
String.toList_dropWhile : ∀ (p : Char → Bool) (s : String), (String.Legacy.dropWhile s p).toList = List.dropWhile p s.toList
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Iio_cast : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n),
  ∑ i < Fin.cast h a, f i = ∑ i < a, f (Fin.cast h i)
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.mulAction_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {X : C}
  (σ : CategoryTheory.Aut F) (x : (F.obj X).obj), σ • x = (CategoryTheory.ConcreteCategory.hom (σ.hom.app X)) x
-- Mathlib.Data.Finset.Density
Finset.dens_ne_one : ∀ {α : Type u_2} [inst : Fintype α] {s : Finset α} [Nonempty α], s.dens ≠ 1 ↔ s ≠ Finset.univ
-- Mathlib.NumberTheory.ModularForms.Basic
ModularFormClass.bdd_at_infty_slash : ∀ {k : ℤ} {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : FunLike F UpperHalfPlane ℂ] (f : F) [Γ.IsArithmetic]
  (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) [ModularFormClass F Γ k],
  UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k g ⇑f)
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  (F : CategoryTheory.Functor C (Type w)) [inst_2 : CategoryTheory.Limits.HasColimitsOfShape F.Elementsᵒᵖ (Type w)]
  (u : F.Elements),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst))
      u.snd =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.colimit.ι
          ((CategoryTheory.CategoryOfElements.π F).op.comp (CategoryTheory.shrinkYoneda.{w, v₁, u₁}.obj u.fst))
          (Opposite.op u)))
      (CategoryTheory.shrinkYonedaObjObjEquiv.symm
        (CategoryTheory.CategoryStruct.id
          (Opposite.unop ((CategoryTheory.CategoryOfElements.π F).op.obj (Opposite.op u)))))
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- A non-unital subsemiring of a `NonUnitalNonAssocCommSemiring` inherits a
`NonUnitalNonAssocCommSemiring` structure  -/
NonUnitalSubsemiringClass.toNonUnitalNonAssocCommSemiring : {S : Type v} →
  (s : S) →
    {R : Type u_1} →
      [inst : NonUnitalNonAssocCommSemiring R] →
        [inst_1 : SetLike S R] → [NonUnitalSubsemiringClass S R] → NonUnitalNonAssocCommSemiring ↥s
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_assoc : ∀ {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) (i : EInt) (X : C) {Z : C} (h : (t.eTruncLT.obj i).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj i).map ((t.eTruncLTι i).app X)) h =
    CategoryTheory.CategoryStruct.comp ((t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X)) h
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₂_comp_bind₂ : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] (f : R →+* MvPolynomial σ S) (g : S →+* MvPolynomial σ T),
  (MvPolynomial.bind₂ g).comp (MvPolynomial.bind₂ f) = MvPolynomial.bind₂ ((MvPolynomial.bind₂ g).comp f)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_le_ceil_sub : ∀ (f : CircleDeg1Lift) (x : ℝ), f.translationNumber ≤ ↑⌈f x - x⌉
-- Init.Data.UInt.Bitwise
UInt16.shiftRight_and : ∀ {a b c : UInt16}, (a &&& b) >>> c = a >>> c &&& b >>> c
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Expr.updateAppS! : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.RingTheory.Ideal.Prime
Ideal.IsPrime.mul_mem_iff_mem_or_mem : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α} [I.IsTwoSided], I.IsPrime → ∀ {x y : α}, x * y ∈ I ↔ x ∈ I ∨ y ∈ I
-- Mathlib.ModelTheory.Substructures
/-- The natural embedding of an `L.Substructure` of `M` into `M`.  -/
FirstOrder.Language.Substructure.subtype : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → (S : L.Substructure M) → L.Embedding (↥S) M
-- Mathlib.Topology.FiberBundle.Trivialization
/-- If the fiber is nonempty, then the projection also is.  -/
Bundle.Pretrivialization.toPartialEquiv_injective : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [Nonempty F], Function.Injective Bundle.Pretrivialization.toPartialEquiv
-- Lean.Meta.HaveTelescope
/-- Constructs the final result. If `keepUnused` is `false`, it eliminates unused let-declarations from
`exprResult` using `zetaUnused` above. This flag is used when we set `ZetaUnusedMode.twoPasses`.
 -/
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.SimpHaveResult.toResult : Lean.Level → Lean.Expr → Lean.Meta.SimpHaveResult✝ → Bool → Lean.MetaM Lean.Meta.MonadSimp.Result
-- Init.Prelude
/-- Mutates the current state, replacing its value with the result of applying `f` to it.

Use `modifyThe` to explicitly select a state type to modify.

It is equivalent to `do set (f (← get))`. However, using `modify` may lead to higher performance
because it doesn't add a new reference to the state value. Additional references can inhibit
in-place updates of data.
 -/
modify : {σ : Type u} → {m : Type u → Type v} → [MonadState σ m] → (σ → σ) → m PUnit.{u + 1}
-- Mathlib.Topology.Baire.BaireMeasurable
/-- We say a set is a `BaireMeasurableSet` if it differs from some Borel set by
a meager set. This forms a σ-algebra.

It is equivalent, and a more standard definition, to say that the set differs from
some *open* set by a meager set. See `BaireMeasurableSet.iff_residualEq_isOpen`  -/
BaireMeasurableSet : {α : Type u_1} → [TopologicalSpace α] → Set α → Prop
-- Mathlib.Data.Set.Basic
Set.ssubset_univ_iff_nonempty_compl : ∀ {α : Type u} {s : Set α}, s ⊂ Set.univ ↔ sᶜ.Nonempty
-- Mathlib.Analysis.InnerProductSpace.Symmetric
InnerProductSpace.isSymmetricProjection_rankOne_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x : E}, ‖x‖ = 1 → (↑(((InnerProductSpace.rankOne 𝕜) x) x)).IsSymmetricProjection
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveTermGoal.pretty : Lean.Widget.InteractiveTermGoal → Std.Format