mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Jensen
StrictConcaveOn.lt_map_sum_iff_of_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 < w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) → (∑ i ∈ t, w i • f (p i) < f (∑ i ∈ t, w i • p i) ↔ ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.hasSum_setIntegral_iUnion : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {ι : Type u_7} [Countable ι] {s : ι → Set X},
  (∀ (i : ι), MeasurableSet (s i)) →
    Pairwise (Function.onFun Disjoint s) →
      μ.IntegrableOn f (⋃ i, s i) → HasSum (fun n => ∫ᵛ (x : X) in s n, f x ∂[B; μ]) ∫ᵛ (x : X) in ⋃ n, s n, f x ∂[B; μ]
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The fan given by `productTriangle T`.  -/
CategoryTheory.Pretriangulated.productTriangle.fan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {J : Type u_1} →
        (T : J → CategoryTheory.Pretriangulated.Triangle C) →
          [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] →
            [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] →
              [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] →
                [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] →
                  CategoryTheory.Limits.Fan T
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_pow_boole : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → M) (a : ι),
  (∏ x ∈ s, f x ^ if a = x then 1 else 0) = if a ∈ s then f a else 1
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- If `c` is a limit cone, `G.mapCocone c.op` is a colimit cone and the projection maps in `c`
are epimorphic, then `cocone G c.pt` is a colimit cone.
 -/
LightProfinite.Extend.isColimitCocone : {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} →
  (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) →
    {C : Type u_1} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        (G : CategoryTheory.Functor LightProfiniteᵒᵖ C) →
          CategoryTheory.Limits.IsLimit c →
            [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] →
              CategoryTheory.Limits.IsColimit (G.mapCocone c.op) →
                CategoryTheory.Limits.IsColimit (LightProfinite.Extend.cocone G c.pt)
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- The functor taking a representation of `G` to its `n`-th Tate cohomology group.  -/
tateCohomologyFunctor : {R G : Type u} →
  [inst : CommRing R] → [inst_1 : Group G] → [Fintype G] → ℤ → CategoryTheory.Functor (Rep.{u, u, u} R G) (ModuleCat R)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.cosPartialEquiv_target : Real.cosPartialEquiv.target = Set.Icc (-1) 1
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.le_initialBound : ∀ (ε : ℝ) (l : ℕ), l ≤ SzemerediRegularity.initialBound ε l
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.le_mul_of_no_prime_factors : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] {I J K : Ideal R},
  (∀ (P : Ideal R), J ≤ P → K ≤ P → ¬P.IsPrime) → I ≤ J → I ≤ K → I ≤ J * K
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.δ_castSucc_map_assoc : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)}
  (self : f.RelStruct g i) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc) (CategoryTheory.CategoryStruct.comp self.map h) =
    CategoryTheory.CategoryStruct.comp f.map h
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_congr : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f g : α → M} {s t : Set α},
  s = t → (∀ x ∈ t, f x = g x) → ∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ᶠ (i : α) (_ : i ∈ t), g i
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.inhabited_self_FGEquiv : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → Inhabited (L.FGEquiv M M)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.struct : Lean.Lsp.SymbolKind
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.SameKeys.wf : ∀ {α : Type u} {β : α → Type v} {β' : α → Type u_1} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β}
  {t' : Std.DTreeMap.Internal.Impl α β'}, t.SameKeys t' → t.WF → t'.WF
-- Mathlib.Topology.Inseparable
SeparationQuotient.preimage_mk_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {t : Set (SeparationQuotient X)},
  SeparationQuotient.mk ⁻¹' closure t = closure (SeparationQuotient.mk ⁻¹' t)
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.add_neg_eq_zero : ∀ {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α}, a + ↑(-u) = 0 ↔ a = ↑u
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.find?.eq_def : ∀ {α : Type u_1} (cut : α → Ordering) (x : RBTree.RBNode α),
  RBTree.RBNode.find? cut x =
    match x with
    | RBTree.RBNode.nil => none
    | RBTree.RBNode.node c a y b =>
      match cut y with
      | Ordering.lt => RBTree.RBNode.find? cut a
      | Ordering.gt => RBTree.RBNode.find? cut b
      | Ordering.eq => some y
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.trivializationOfVAddDisjoint.eq_1 : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hf : Topology.IsQuotientMap f) [inst_4 : ContinuousConstVAdd G E]
  (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) [inst_5 : TopologicalSpace G]
  [inst_6 : DiscreteTopology G] (U : Set E) (open_U : IsOpen U)
  (disjoint : ∀ (g : G), ((fun x => g +ᵥ x) '' U ∩ U).Nonempty → g = 0),
  hf.trivializationOfVAddDisjoint hfG U open_U disjoint =
    IsOpen.trivializationDiscrete (fun g => (fun x => g +ᵥ x) ⁻¹' U) (f '' U) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Init.Data.Nat.ToString
Nat.four_eq_digitChar : ∀ {n : ℕ}, '4' = n.digitChar ↔ n = 4
-- Init.Data.Vector.Extract
Vector.extract_append_left : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m}, (xs ++ ys).extract 0 n = Vector.cast ⋯ xs.extract
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.rlp_of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.IsIso f], T.rlp f
-- Init.Data.List.Lemmas
List.length_filter_eq_length_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, (List.filter p l).length = l.length ↔ ∀ a ∈ l, p a = true
-- Mathlib.Data.UInt
USize.toBitVec_natCast : ∀ (n : ℕ), (↑n).toBitVec = ↑n
-- Mathlib.Data.ZMod.Basic
/-- The unique ring isomorphism between `ZMod n` and a ring `R`
of characteristic `n` and cardinality `n`.  -/
ZMod.ringEquiv : {n : ℕ} → (R : Type u_1) → [inst : Ring R] → [CharP R n] → [inst_2 : Fintype R] → Fintype.card R = n → ZMod n ≃+* R
-- Batteries.Data.List.Basic
/-- A list of length 0 is a chain.  -/
List.IsChain.nil : ∀ {α : Type u_1} {R : α → α → Prop}, List.IsChain R []
-- Lean.Expr
/-- Returns `have x : t := v; b`, a non-dependent `let` expression.  -/
Lean.mkHave : Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β ky)
  (l r : Std.DTreeMap.Internal.Impl α β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.getEntryGT k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    if hkky : compare k ky = Ordering.lt then Std.DTreeMap.Internal.Impl.getEntryGTD k l ⟨ky, y⟩
    else Std.DTreeMap.Internal.Impl.getEntryGT k r ⋯ ⋯
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.smul_def : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (T : Type u_1) [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : IsLocalization S T] (x : T) (m : M)
  (s : ↥S),
  x • LocalizedModule.mk m s = LocalizedModule.mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s)
-- Init.Data.List.Basic
/-- Applies a function to each element of the list, returning the resulting list of values.

`O(|l|)`. This is the tail-recursive variant of `List.map`, used in runtime code.

Examples:
* `[a, b, c].mapTR f = [f a, f b, f c]`
* `[].mapTR Nat.succ = []`
* `["one", "two", "three"].mapTR (·.length) = [3, 3, 5]`
* `["one", "two", "three"].mapTR (·.reverse) = ["eno", "owt", "eerht"]`
 -/
List.mapTR : {α : Type u} → {β : Type v} → (α → β) → List α → List β
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.sigmaFiniteTrim_mono : ∀ {α : Type u_1} {m m₂ m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (hm₂ : m₂ ≤ m)
  [MeasureTheory.SigmaFinite (μ.trim ⋯)], MeasureTheory.SigmaFinite (μ.trim hm)
-- Mathlib.CategoryTheory.Monoidal.Linear
CategoryTheory.MonoidalLinear.congr_simp : ∀ (R : Type u_1) [inst : Semiring R] (C : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.MonoidalCategory C] [inst_5 : CategoryTheory.MonoidalPreadditive C],
  CategoryTheory.MonoidalLinear R C = CategoryTheory.MonoidalLinear R C
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Submodule.toLinearMap_subtypeL : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (p : Submodule R M), ↑p.subtypeL = p.subtype
-- Mathlib.Dynamics.Flow
Flow.map_zero_apply : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  (ϕ : Flow τ α) (x : α), ϕ.toFun 0 x = x
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.Ctx.root : Lean.Elab.Tactic.Try.Ctx → Lean.TSyntax `tactic
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.instLaxBraidedDiscretePUnitCommMonToLaxBraidedObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (A : CategoryTheory.CommMon C) →
          (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj A).LaxBraided
-- Batteries.Data.Float.Basic
/-- Converts `f` to a string, including all decimal digits.  -/
Float.toStringFull : Float → String
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.toAdd_symm_eq : ∀ {α : Type u}, Multiplicative.toAdd.symm = Multiplicative.ofAdd
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.Slice.Pattern.Model.posFind?_eq_some_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {σ : String.Slice → Type}
  [inst_2 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_3 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id]
  [inst_4 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id]
  [∀ (s : String.Slice), Std.LawfulIteratorLoop (σ s) Id Id] [inst_6 : String.Slice.Pattern.ToForwardSearcher pat σ]
  [String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat] {s : String.Slice} {pos pos' : s.Pos},
  pos.find? pat = some pos' ↔
    pos ≤ pos' ∧
      String.Slice.Pattern.Model.MatchesAt pat pos' ∧
        ∀ (pos'' : s.Pos), pos ≤ pos'' → pos'' < pos' → ¬String.Slice.Pattern.Model.MatchesAt pat pos''
-- Init.Data.List.TakeDrop
List.take_add_one : ∀ {α : Type u_1} {l : List α} {i : ℕ}, List.take (i + 1) l = List.take i l ++ l[i]?.toList
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasStrictFDerivAt_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_6} {F' : ι → Type u_7} [inst_3 : (i : ι) → NormedAddCommGroup (F' i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} {φ' : (i : ι) → E →L[𝕜] F' i},
  HasStrictFDerivAt (fun x i => φ i x) (ContinuousLinearMap.pi φ') x ↔ ∀ (i : ι), HasStrictFDerivAt (φ i) (φ' i) x
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₀_ne_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, E ≠ ⊥ → RatFunc.Luroth.Q₀✝ E ≠ 0
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp'.eq_def : ∀ (x : Turing.ToPartrec.Code) (x_1 : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp' x x_1 =
    match x, x_1 with
    | c@h:Turing.ToPartrec.Code.zero', k => Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k)
    | c@h:Turing.ToPartrec.Code.succ, k => Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k)
    | c@h:Turing.ToPartrec.Code.tail, k => Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k)
    | c@h:(f.cons fs), k =>
      Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k) ∪
        (Turing.PartrecToTM2.codeSupp' f (Turing.PartrecToTM2.Cont'.cons₁ fs k) ∪
          (Turing.PartrecToTM2.trStmts₁
              (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.aux
                (Turing.PartrecToTM2.move₂ (fun s => decide (s = Turing.PartrecToTM2.Γ'.consₗ))
                  Turing.PartrecToTM2.K'.stack Turing.PartrecToTM2.K'.main
                  (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.aux Turing.PartrecToTM2.K'.stack
                    (Turing.PartrecToTM2.trNormal fs k.cons₂)))) ∪
            (Turing.PartrecToTM2.codeSupp' fs k.cons₂ ∪
              Turing.PartrecToTM2.trStmts₁
                (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)))))
    | c@h:(f.comp g), k =>
      Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k) ∪
        (Turing.PartrecToTM2.codeSupp' g (Turing.PartrecToTM2.Cont'.comp f k) ∪
          (Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal f k) ∪ Turing.PartrecToTM2.codeSupp' f k))
    | c@h:(f.case g), k =>
      Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k) ∪
        (Turing.PartrecToTM2.codeSupp' f k ∪ Turing.PartrecToTM2.codeSupp' g k)
    | c@h:f.fix, k =>
      Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k) ∪
        (Turing.PartrecToTM2.codeSupp' f (Turing.PartrecToTM2.Cont'.fix f k) ∪
          (Turing.PartrecToTM2.trStmts₁
              (Turing.PartrecToTM2.Λ'.clear Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.K'.main
                (Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.fix f k))) ∪
            {Turing.PartrecToTM2.Λ'.ret k}))
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_top : ↑⊤ = Cardinal.aleph0
-- Mathlib.Topology.Constructible
IsRetrocompact.biUnion : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Type u_4} {f : ι → Set X} {t : Set ι},
  t.Finite → (∀ i ∈ t, IsRetrocompact (f i)) → IsRetrocompact (⋃ i ∈ t, f i)
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.containsThenInsert!.size : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → ℕ
-- Mathlib.Algebra.MvPolynomial.Monad
/-- `join₁` is the monadic join operation corresponding to `MvPolynomial.bind₁`. Given a polynomial `p`
with coefficients in `R` whose variables are polynomials in `σ` with coefficients in `R`,
`join₁ p` collapses `p` to a polynomial with variables in `σ` and coefficients in `R`.
This operation is an algebra hom.
 -/
MvPolynomial.join₁ : {σ : Type u_1} → {R : Type u_3} → [inst : CommSemiring R] → MvPolynomial (MvPolynomial σ R) R →ₐ[R] MvPolynomial σ R
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.coe_comp_rangeRestrict : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), Subtype.val ∘ ⇑f.rangeRestrict = ⇑f
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.skipWhile_eq_self_iff_or : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos},
  pos.skipWhile pat = pos ↔
    ¬String.Slice.Pattern.Model.MatchesAt pat pos ∨ String.Slice.Pattern.Model.IsLongestMatchAt pat pos pos
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
/-- **Continuous mapping theorem**: if `X n` tends to `Z` in distribution and `g` is continuous,
then `g ∘ X n` tends to `g ∘ Z` in distribution.  -/
MeasureTheory.TendstoInDistribution.continuous_comp : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)}
  {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [inst : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
  {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} [inst_1 : MeasureTheory.IsProbabilityMeasure μ']
  {mE : MeasurableSpace E} {X : (i : ι) → Ω i → E} {Z : Ω' → E} {l : Filter ι} [inst_2 : TopologicalSpace E]
  {F : Type u_6} [inst_3 : OpensMeasurableSpace E] [inst_4 : TopologicalSpace F] [inst_5 : MeasurableSpace F]
  [inst_6 : BorelSpace F] {g : E → F},
  Continuous g →
    MeasureTheory.TendstoInDistribution X l Z μ μ' →
      MeasureTheory.TendstoInDistribution (fun n => g ∘ X n) l (g ∘ Z) μ μ'
-- Mathlib.Topology.Separation.Basic
Set.Subsingleton.closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s : Set X}, s.Subsingleton → (closure s).Subsingleton
-- Lean.SubExpr
/-- Returns true if `pred` is true for each coordinate in `p`. -/
Lean.SubExpr.Pos.all : (ℕ → Bool) → Lean.SubExpr.Pos → Bool
-- Mathlib.Analysis.Calculus.Deriv.Basic
Filter.EventuallyEq.derivWithin_eq_of_mem : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  f₁ =ᶠ[nhdsWithin x s] f → x ∈ s → derivWithin f₁ s x = derivWithin f s x
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularEpi.fac_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.IsRegularEpi f] (k : X ⟶ Z)
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.left f) k =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.right f) k)
  {Z_1 : C} (h_1 : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.desc f k h) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Lean.Compiler.IR.Basic
Lean.IR.Param.mk.injEq : ∀ (x : Lean.IR.VarId) (borrow : Bool) (ty : Lean.IR.IRType) (x_1 : Lean.IR.VarId) (borrow_1 : Bool)
  (ty_1 : Lean.IR.IRType),
  ({ x := x, borrow := borrow, ty := ty } = { x := x_1, borrow := borrow_1, ty := ty_1 }) =
    (x = x_1 ∧ borrow = borrow_1 ∧ ty = ty_1)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.balanceL_eq_balance : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α},
  l.Sized →
    r.Sized →
      (l.size = 0 → r.size ≤ 1) →
        (1 ≤ l.size → 1 ≤ r.size → r.size ≤ Ordnode.delta * l.size) → l.balanceL x r = l.balance x r
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.waitExpectedType : Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The meromorphic function of `s` which agrees with
`1 / 2 * Gamma (s / 2) * π ^ (-s / 2) * ∑' (n : ℤ), 1 / |n + a| ^ s` for `1 < re s`.
 -/
HurwitzZeta.completedHurwitzZetaEven : UnitAddCircle → ℂ → ℂ
-- Std.Data.DTreeMap.Basic
/-- If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
returns the map unaltered.
 -/
Std.DTreeMap.insertIfNew : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → (a : α) → β a → Std.DTreeMap α β cmp
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.reindex_g₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι),
  (c.reindex e).g₂ = c.g₂
-- Mathlib.Data.Finset.Lattice.Pi
Finset.sup_inf : ∀ {α : Type u_1} {ι : Type u_2} [inst : DistribLattice α] [inst_1 : BoundedOrder α] [inst_2 : DecidableEq ι]
  {κ : ι → Type u_3} (s : Finset ι) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → α),
  (s.sup fun i => (t i).inf (f i)) = (s.pi t).inf fun g => s.attach.sup fun i => f (↑i) (g ↑i ⋯)
-- Mathlib.Topology.Algebra.Algebra
/-- If a subalgebra of a topological algebra is commutative, then so is its topological closure.
See note [reducible non-instances].  -/
Subalgebra.commRingTopologicalClosure : {R : Type u_1} →
  [inst : CommRing R] →
    {A : Type u} →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : Ring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : IsSemitopologicalRing A] →
              [T2Space A] → (s : Subalgebra R A) → (∀ (x y : ↥s), x * y = y * x) → CommRing ↥s.topologicalClosure
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLE.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (f f_1 : A ⟶ B) (e_f : f = f_1)
  [inst_1 : CategoryTheory.Mono f] (X : CategoryTheory.Subobject B) (h : CategoryTheory.Subobject.mk f ≤ X),
  CategoryTheory.Subobject.ofMkLE f X h = CategoryTheory.Subobject.ofMkLE f_1 X ⋯
-- Init.Data.List.Lemmas
List.sum_singleton : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] [Std.LawfulRightIdentity (fun x1 x2 => x1 + x2) 0] {x : α},
  [x].sum = x
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric.0.CovariantDerivative.derivMetricTensor.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] {V : M → Type u_5}
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → NormedAddCommGroup (V x)]
  [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] [inst_10 : FiberBundle F V] (cov : CovariantDerivative I F V)
  [inst_11 : VectorBundle ℝ F V] [inst_12 : IsContMDiffRiemannianBundle I 1 F V]
  [inst_13 : ContMDiffVectorBundle 1 F V I] [inst_14 : FiniteDimensional ℝ F] (x : M),
  cov.derivMetricTensor x =
    TensorialAt.mkHom₂ (fun x1 x2 => CovariantDerivative.derivMetricTensorAux✝ I cov x1 x2 x) x ⋯ ⋯
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `i : K →+* L` and `j : K →+* M` are ring homomorphisms of characteristic `p` rings, such that
`i` is `p`-radical, and `M` is a perfect ring, then `PerfectRing.liftAux` is well-defined.  -/
PerfectRing.liftAux_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] [ExpChar K p] [inst_5 : PerfectRing M p]
  [inst_6 : IsPRadical i p] (x : L) (n : ℕ) (y : K),
  i y = x ^ p ^ n → PerfectRing.liftAux i j p x = (iterateFrobeniusEquiv M p n).symm (j y)