mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAt.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos endPos : s.Pos}
  (le : startPos ≤ endPos),
  String.Slice.Pattern.Model.IsLongestMatch pat (startPos.sliceFrom endPos le) →
    String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos
-- Mathlib.Order.Hom.Bounded
TopHom.sup_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : SemilatticeSup β] [inst_2 : OrderTop β] (f g : TopHom α β)
  (a : α), (f ⊔ g) a = f a ⊔ g a
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_subset_Ici_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} [DenselyOrdered α], Set.Ioi b ⊆ Set.Ici a ↔ a ≤ b
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.instExpChar : ∀ {R : Type u} [inst : Semiring R] (p : ℕ) [h : ExpChar R p], ExpChar (Polynomial R) p
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.fixedPoints_of_subsingleton : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] [Subsingleton α],
  AddAction.fixedPoints G α = Set.univ
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.liftE.congr_simp : ∀ {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 l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) {A : C}
  (x x_1 : A ⟶ (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂₃)) (e_x : x = x_1)
  (h :
    CategoryTheory.CategoryStruct.comp x ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) = 0)
  (hn₂ : n₁ + 1 = n₂) (h' : CategoryTheory.CategoryStruct.comp x (X.δ f₁ f₂₃ n₁ n₂ hn₂) = 0) (hn₁ : n₀ + 1 = n₁),
  X.liftE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ x h hn₂ h' hn₁ = X.liftE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ x_1 ⋯ hn₂ ⋯ hn₁
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
Equiv.mulRight₀_symm_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) (ha : a ≠ 0),
  ⇑(Equiv.symm (Equiv.mulRight₀ a ha)) = fun x => x * a⁻¹
-- Init.Data.Vector.Range
Vector.le_snd_of_mem_zipIdx : ∀ {α : Type u_1} {n : ℕ} {x : α × ℕ} {k : ℕ} {xs : Vector α n}, x ∈ xs.zipIdx k → k ≤ x.2
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
/-- Given a point of a site, the skyscraper presheaf functor is right adjoint
to the fiber functor on presheaves.  -/
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [inst_2 : CategoryTheory.Limits.HasProducts A] →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                Φ.presheafFiber ⊣ Φ.skyscraperPresheafFunctor
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} {τ : Equiv.Perm ↥g.cycleFactorsFinset},
  τ ∈ (Equiv.Perm.OnCycleFactors.toPermHom g).range ↔
    ∀ (c : ↥g.cycleFactorsFinset), (↑(τ c)).support.card = (↑c).support.card
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHomClass.toAddMonoidHomClass : ∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} {inst : NonUnitalNonAssocSemiring α}
  {inst_1 : NonUnitalNonAssocSemiring β} {inst_2 : FunLike F α β} [self : NonUnitalRingHomClass F α β],
  AddMonoidHomClass F α β
-- Mathlib.Data.Fintype.EquivFin
/-- On a finite type, equivalence between the self-embeddings and the bijections.  -/
Equiv.embeddingEquivOfFinite : (α : Type u_4) → [Finite α] → (α ↪ α) ≃ (α ≃ α)
-- Mathlib.GroupTheory.Index
Subgroup.finite_quotient_of_finite_quotient_of_index_ne_zero : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {X : Type u_3} [inst_1 : MulAction G X]
  [Finite (MulAction.orbitRel.Quotient G X)], H.index ≠ 0 → Finite (MulAction.orbitRel.Quotient (↥H) X)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- The element in `Φ.Iteration i` that is deduced from an element
in `Φ.Iteration j` when `i ≤ j`.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.trunc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      {Φ : CategoryTheory.SmallObject.SuccStruct C} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] →
                [inst_5 : WellFoundedLT J] → {j : J} → Φ.Iteration j → {j' : J} → j' ≤ j → Φ.Iteration j'
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- **Alias** of `CategoryTheory.PreZeroHypercover.Hom.w₀`. -/
AlgebraicGeometry.Scheme.Cover.Hom.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} (self : E.Hom F) (i : E.I₀),
  CategoryTheory.CategoryStruct.comp (self.h₀ i) (F.f (self.s₀ i)) = E.f i
-- Batteries.Recycling.RBTree.WF
/-- The `balance2` function repairs the balance invariant when the second argument is red-red.  -/
RBTree.RBNode.RedRed.balance2 : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {p : Prop} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  l.Balanced c n → RBTree.RBNode.RedRed p r n → ∃ c, (l.balance2 v r).Balanced c (n + 1)
-- Mathlib.Topology.Algebra.Group.Basic
smul_connectedComponent : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] (g h : G),
  g • connectedComponent h = connectedComponent (g * h)
-- Mathlib.Order.Filter.Partial
Filter.rmap_rmap : ∀ {α : Type u} {β : Type v} {γ : Type w} (r : SetRel α β) (s : SetRel β γ) (l : Filter α),
  Filter.rmap s (Filter.rmap r l) = Filter.rmap (r.comp s) l
-- Mathlib.Topology.Order.LawsonTopology
Topology.scottHausdorff_le_lawson : ∀ {α : Type u_1} [inst : Preorder α], Topology.scottHausdorff α Set.univ ≤ Topology.lawson α
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_toAddSubmonoid : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G') (K : AddSubgroup G),
  (AddSubgroup.map f K).toAddSubmonoid = AddSubmonoid.map f K.toAddSubmonoid
-- Std.Http.Protocol.H1
/-- Returns `true` if the machine should flush buffered output.
 -/
Std.Http.Protocol.H1.Machine.shouldFlush : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Mathlib.FieldTheory.KummerExtension
autEquivRootsOfUnity_smul : ∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L},
  α ^ n = (algebraMap K L) a → ∀ [inst_4 : NeZero n] (σ : Gal(L/K)), (autEquivRootsOfUnity hζ H L) σ • α = σ α
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.mem_support_bind_iff : ∀ {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β) (b : β),
  b ∈ (p.bind f).support ↔ ∃ a ∈ p.support, b ∈ (f a).support
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
addEquivOfPrimeCardEq.eq_1 : ∀ {G : Type u_2} {G' : Type u_3} {p : ℕ} [inst : AddGroup G] [inst_1 : AddGroup G'] [inst_2 : Fact (Nat.Prime p)]
  (hG : Nat.card G = p) (hH : Nat.card G' = p), addEquivOfPrimeCardEq hG hH = addEquivOfAddCyclicCardEq ⋯
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
/-- The group of invertible linear maps from `M` to itself  -/
LinearMap.GeneralLinearGroup : (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type u_2
-- Mathlib.Algebra.Order.CauSeq.Completion
/-- The Cauchy completion forms a field.  -/
CauSeq.Completion.Cauchy.field : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Field β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → Field (CauSeq.Completion.Cauchy abv)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
intervalIntegral.integrable_deriv_smul_comp_iff_of_deriv_nonpos : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), f' x ≤ 0) →
        (IntervalIntegrable (fun x => f' x • (g ∘ f) x) MeasureTheory.volume a b ↔
          IntervalIntegrable g MeasureTheory.volume (f a) (f b))
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (f : ↑(X.presheaf.obj (Opposite.op U))),
  (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).basicOpen
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app hU.fromSpec U)) f) =
    PrimeSpectrum.basicOpen f
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.Ordered.eq_def : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : RBTree.RBNode α),
  RBTree.RBNode.Ordered cmp x =
    match x with
    | RBTree.RBNode.nil => True
    | RBTree.RBNode.node c a x b =>
      RBTree.RBNode.All (fun x_1 => RBTree.RBNode.cmpLT cmp x_1 x) a ∧
        RBTree.RBNode.All (fun x_1 => RBTree.RBNode.cmpLT cmp x x_1) b ∧
          RBTree.RBNode.Ordered cmp a ∧ RBTree.RBNode.Ordered cmp b
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α]
  {f : α → β → γ} {k : α} {fallback : γ}, (Std.HashMap.map f m).getD k fallback = (Option.map (f k) m[k]?).getD fallback
-- Mathlib.Order.Birkhoff
OrderEmbedding.birkhoffFinset.eq_1 : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : Fintype α] [inst_2 : DecidablePred SupIrred],
  OrderEmbedding.birkhoffFinset =
    RelEmbedding.trans OrderEmbedding.birkhoffSet Fintype.finsetOrderIsoSet.symm.toOrderEmbedding
-- Lean.Elab.Match
Lean.Elab.Term.GeneralizeResult.refined : Lean.Elab.Term.GeneralizeResult → Bool
-- Init.Data.Sum.Lemmas
Sum.not_isLeft : ∀ {α : Type u_1} {β : Type u_2} {x : α ⊕ β}, ¬x.isLeft = true ↔ x.isRight = true
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- A real function whose derivative tends to infinity from the right at a point is not
differentiable on the right at that point.  -/
not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi : ∀ (f : ℝ → ℝ) {a : ℝ},
  Filter.Tendsto (deriv f) (nhdsWithin a (Set.Ioi a)) Filter.atTop → ¬DifferentiableWithinAt ℝ f (Set.Ioi a) a
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.eq_bot_iff_card : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H = ⊥ ↔ Nat.card ↥H = 1
-- Lean.Expr
Lean.mkProjEx : Lean.Name → ℕ → Lean.Expr → Lean.Expr
-- Mathlib.Analysis.Analytic.Composition
/-- Given two formal multilinear series `q` and `p` and a composition `c` of `n`, one may
form a continuous multilinear map in `n` variables by applying the right coefficient of `p` to each
block of the composition, and then applying `q c.length` to the resulting vector. It is
called `q.compAlongComposition p c`.  -/
FormalMultilinearSeries.compAlongComposition : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        [inst : CommRing 𝕜] →
          [inst_1 : AddCommGroup E] →
            [inst_2 : AddCommGroup F] →
              [inst_3 : AddCommGroup G] →
                [inst_4 : Module 𝕜 E] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : Module 𝕜 G] →
                      [inst_7 : TopologicalSpace E] →
                        [inst_8 : TopologicalSpace F] →
                          [inst_9 : TopologicalSpace G] →
                            [inst_10 : IsTopologicalAddGroup E] →
                              [inst_11 : ContinuousConstSMul 𝕜 E] →
                                [inst_12 : IsTopologicalAddGroup F] →
                                  [inst_13 : ContinuousConstSMul 𝕜 F] →
                                    [inst_14 : IsTopologicalAddGroup G] →
                                      [inst_15 : ContinuousConstSMul 𝕜 G] →
                                        {n : ℕ} →
                                          FormalMultilinearSeries 𝕜 F G →
                                            FormalMultilinearSeries 𝕜 E F → Composition n → E [×n]→L[𝕜] G
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_coe : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑↑e = ⇑e
-- Mathlib.RingTheory.FinitePresentation
/-- A ring morphism `A →+* B` is of `RingHom.FinitePresentation` if `B` is finitely presented as
`A`-algebra.  -/
RingHom.FinitePresentation : {A : Type u_1} → {B : Type u_2} → [inst : CommRing A] → [inst_1 : CommRing B] → (A →+* B) → Prop
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.eq : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ t₃ t₄ : String}, p.Splits t₁ t₂ → p.Splits t₃ t₄ → t₁ = t₃ ∧ t₂ = t₄
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Context.mk.injEq : ∀ (config : Lean.Meta.Sym.Simp.Config) (initialLCtxSize dischargeDepth : ℕ) (config_1 : Lean.Meta.Sym.Simp.Config)
  (initialLCtxSize_1 dischargeDepth_1 : ℕ),
  ({ config := config, initialLCtxSize := initialLCtxSize, dischargeDepth := dischargeDepth } =
      { config := config_1, initialLCtxSize := initialLCtxSize_1, dischargeDepth := dischargeDepth_1 }) =
    (config = config_1 ∧ initialLCtxSize = initialLCtxSize_1 ∧ dischargeDepth = dischargeDepth_1)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Real.measurable_arccos : Measurable Real.arccos
-- Mathlib.Algebra.Group.Defs
pow_succ : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a ^ n * a
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.ι₂_desc_assoc : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃)
  {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.horn₃₁.ι₂
      (CategoryTheory.CategoryStruct.comp (SSet.horn₃₁.desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃) h) =
    CategoryTheory.CategoryStruct.comp f₂ h
-- Mathlib.GroupTheory.Perm.Option
Equiv.Perm.decomposeOption_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (σ : Equiv.Perm (Option α)),
  Equiv.Perm.decomposeOption σ = (σ none, Equiv.removeNone σ)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.denote_toPoly : ∀ (ctx : Nat.Internal.Linear.Context) (c : Nat.Internal.Linear.ExprCnstr),
  Nat.Internal.Linear.PolyCnstr.denote ctx c.toPoly = Nat.Internal.Linear.ExprCnstr.denote ctx c
-- Init.Tactics
/-- `get_elem_tactic_extensible` is an extensible tactic automatically called
by the notation `arr[i]` to prove any side conditions that arise when
constructing the term (e.g. the index is in bounds of the array).
The default behavior is to try `simp +arith` and `omega`
(for doing linear arithmetic in the index).

(Note that the core tactic `get_elem_tactic` has already tried
`done` and `assumption` before the extensible tactic is called.)
 -/
tacticGet_elem_tactic_extensible : Lean.ParserDescr
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.instInhabited : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → Inhabited (L.BoundedFormula α n)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.apply_eq_iff_eq : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ p₂ : P₁}, e p₁ = e p₂ ↔ p₁ = p₂
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.forIn_mapM : ∀ {α β β₂ γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w}
  [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad o Pred EPred] [inst_8 : MonadAttach n] [WeaklyLawfulMonadAttach n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_12 : MonadLiftT n o] [LawfulMonadLiftT n o]
  [inst_14 : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_16 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)}
  {P : Pred} {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out)
        g __do_lift acc ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.IterM.mapM f it) init g ⦃ Q; eQ ⦄
-- Mathlib.Analysis.Convex.Mul
ConcaveOn.smul'' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E]
  [inst_6 : AddCommGroup F] [inst_7 : LinearOrder F] [IsOrderedAddMonoid F] [inst_9 : AddCommGroup G]
  [inst_10 : Module 𝕜 G] [inst_11 : Module 𝕜 E] [inst_12 : Module 𝕜 F] [inst_13 : Module E F] [IsScalarTower 𝕜 E F]
  [SMulCommClass 𝕜 E F] [IsOrderedModule 𝕜 F] [IsStrictOrderedModule E F] {s : Set G} {f : G → E} {g : G → F},
  ConcaveOn 𝕜 s f →
    ConcaveOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → f x ≤ 0) → (∀ ⦃x : G⦄, x ∈ s → g x ≤ 0) → MonovaryOn f g s → ConvexOn 𝕜 s (f • g)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion.0.term𝕢 : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.mu_naturality_assoc : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) ⦃X Y : C⦄ (f : X ⟶ Y) {Z : C}
  (h : T.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (T.map (T.map f)) (CategoryTheory.CategoryStruct.comp (T.μ.app Y) h) =
    CategoryTheory.CategoryStruct.comp (T.μ.app X) (CategoryTheory.CategoryStruct.comp (T.map f) h)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- The equivalence between group homs `G → H` and bialgebra homs `R[G] → R[H]` of group algebras
over a domain.  -/
MonoidAlgebra.mapDomainBialgHomEquiv : {R : Type u_1} →
  {G : Type u_5} →
    {H : Type u_6} →
      [inst : CommRing R] →
        [IsDomain R] → [inst_2 : Group G] → [inst_3 : Group H] → (G →* H) ≃ (MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H)
-- Init.Data.Array.Monadic
Array.filterRevM_congr : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] {as bs : Array α},
  as = bs → ∀ {p q : α → m Bool}, (∀ (a : α), p a = q a) → Array.filterRevM p as = Array.filterRevM q bs
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {f : β → β},
  (t.modify k f).getKey? k' = if cmp k k' = Ordering.eq then if k ∈ t then some k else none else t.getKey? k'
-- Lean.Elab.App
/-- If the result type may be the `outParam` of some local instance.
See comment at `Context.resultIsOutParamSupport`
 -/
Lean.Elab.Term.ElabAppArgs.State.resultTypeOutParam? : Lean.Elab.Term.ElabAppArgs.State → Option Lean.MVarId
-- Init.Grind.ToInt
Lean.Grind.instReflBEqIntInterval : ReflBEq Lean.Grind.IntInterval
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.CommaMorphism.mk : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {X Y : CategoryTheory.Comma L R} →
                  (left : X.left ⟶ Y.left) →
                    (right : X.right ⟶ Y.right) →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp (L.map left) Y.hom =
                            CategoryTheory.CategoryStruct.comp X.hom (R.map right))
                          CategoryTheory.CommaMorphism.w._autoParam →
                        CategoryTheory.CommaMorphism X Y
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- The differential of a `P : PreSubmersivePresentation` is a `P.Ring`-linear map on
`σ → P.Ring`:

The `j`-th standard basis vector, corresponding to the `j`-th relation of `P`, is mapped
to the vector of partial derivatives of `P.relation j` with respect
to the coordinates `P.map i` for all `i : σ`.

The determinant of this map is the Jacobian of `P` used to define when a `PreSubmersivePresentation`
is submersive. See `PreSubmersivePresentation.jacobian`.
 -/
Algebra.PreSubmersivePresentation.differential : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              (P : Algebra.PreSubmersivePresentation R S ι σ) → [Finite σ] → (σ → P.Ring) →ₗ[P.Ring] σ → P.Ring
-- Mathlib.Combinatorics.Quiver.Prefunctor
/-- The action of a (pre)functor on edges/arrows/morphisms.  -/
Prefunctor.map : {V : Type u₁} →
  [inst : Quiver V] →
    {W : Type u₂} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
-- Mathlib.CategoryTheory.Products.Basic
/-- The "evaluation at `X`" functor, such that
`(evaluation.obj X).obj F = F.obj X`,
which is functorial in both `X` and `F`.
 -/
CategoryTheory.evaluation : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C (CategoryTheory.Functor (CategoryTheory.Functor C D) D)
-- Lean.Data.Options
Lean.Options.instInhabited : Inhabited Lean.Options
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.ofHom_apply : ∀ {X Y : Type u} [inst : Semigroup X] [inst_1 : Semigroup Y] (f : X →ₙ* Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (Semigrp.ofHom f)) x = f x
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_biUnion_le_tsum : ∀ {α : Type u_1} {ι : Type u_4} (f : α → ENNReal) (s : Set ι) (t : ι → Set α),
  ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x ≤ ∑' (i : ↑s) (x : ↑(t ↑i)), f ↑x
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- If a path `p` is Hamiltonian, then `p.support.get` defines an equivalence between
`Fin p.support.length` and `α`.  -/
SimpleGraph.Walk.IsHamiltonian.supportGetEquiv : {α : Type u_1} →
  [inst : DecidableEq α] →
    {G : SimpleGraph α} → {a b : α} → {p : G.Walk a b} → p.IsHamiltonian → Fin p.support.length ≃ α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.any_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {p : α → β → Bool},
  ((Std.DHashMap.Const.toList m).any fun x => p x.1 x.2) = m.any p
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, (m.alter k f).contains k = (f (m.get? k)).isSome
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.henstock_le_mcShane : BoxIntegral.IntegrationParams.Henstock ≤ BoxIntegral.IntegrationParams.McShane