mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
HasStrictFDerivAt.restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F} {f' : E →L[𝕜'] F}
  {x : E}, HasStrictFDerivAt f f' x → HasStrictFDerivAt f (ContinuousLinearMap.restrictScalars 𝕜 f') x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
/-- An idempotent operator `f` commutes with `T` if and only if
both `range f` and `ker f` are invariant under `T`.  -/
ContinuousLinearMap.IsIdempotentElem.commute_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {f T : M →L[R] M},
  IsIdempotentElem f → (Commute f T ↔ (↑f).range ∈ Module.End.invtSubmodule ↑T ∧ (↑f).ker ∈ Module.End.invtSubmodule ↑T)
-- Mathlib.Analysis.Real.Sqrt
ContinuousWithinAt.sqrt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {s : Set α} {x : α},
  ContinuousWithinAt f s x → ContinuousWithinAt (fun x => √(f x)) s x
-- Mathlib.Data.Tree.Basic
/-- A binary tree with values stored in non-leaf nodes.  -/
BinaryTree : Type u → Type u
-- Mathlib.NumberTheory.Dioph
Poly.coe_mul : ∀ {α : Type u_1} (f g : Poly α), ⇑(f * g) = ⇑f * ⇑g
-- Init.Data.Nat.Basic
Nat.pred_le_of_le_succ : ∀ {n m : ℕ}, n ≤ m.succ → n.pred ≤ m
-- Mathlib.RingTheory.Kaehler.Basic
instModuleKaehlerDifferentialOfSMulCommClass : (R : Type u_3) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {R' : Type u_1} → [inst_3 : CommRing R'] → [inst_4 : Algebra R' S] → [SMulCommClass R R' S] → Module R' Ω[S⁄R]
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.ofFractionRing.sizeOf_spec : ∀ {K : Type u} [inst : CommRing K] [inst_1 : SizeOf K] (toFractionRing : FractionRing (Polynomial K)),
  sizeOf { toFractionRing := toFractionRing } = 1 + sizeOf toFractionRing
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.orelseMergeErrorsImp : {α : Type} →
  Lean.MetaM α →
    Lean.MetaM α →
      (optParam (Lean.Syntax → Lean.Syntax → Lean.Syntax) fun r₁ x => r₁) →
        (optParam (Lean.MessageData → Lean.MessageData → Lean.MessageData) fun m₁ m₂ =>
            m₁ ++ Lean.MessageData.ofFormat Std.Format.line ++ m₂) →
          Lean.MetaM α
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.dist_iterate_next_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K)
  (hx : x ∈ Metric.closedBall x₀ ↑r) (α : ODE.FunSpace t₀ x₀ r L) (n : ℕ),
  dist α ((ODE.FunSpace.next hf hx)^[n] α) ≤
    (∑ i ∈ Finset.range n, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i.factorial) * dist α (ODE.FunSpace.next hf hx α)
-- Mathlib.GroupTheory.DivisibleHull
/-- Use `Equiv.injective archimedeanClassOrderIso` for public API.  -/
_private.Mathlib.GroupTheory.DivisibleHull.0.DivisibleHull.aux_archimedeanClassOrderHom_injective : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  Function.Injective ⇑(DivisibleHull.archimedeanClassOrderHom✝ M)
-- Mathlib.Algebra.Category.Ring.EqualizerPushout
/-- Any map `f : S ⟶ R` in `CommRingCatᵒᵖ` with faithfully flat `f.unop.hom : R.unop ⟶ S.unop` is
an effective epimorphism.  -/
CommRingCat.Opposite.effectiveEpi_of_faithfullyFlat : ∀ {R S : CommRingCatᵒᵖ} (f : S ⟶ R), (CommRingCat.Hom.hom f.unop).FaithfullyFlat → CategoryTheory.EffectiveEpi f
-- Mathlib.Topology.Separation.Regular
T4Space.toNormalSpace : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T4Space X], NormalSpace X
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.dualBasis_repr : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) [inst_4 : Finite ι] (l : Module.Dual R M) (i : ι),
  (b.dualBasis.repr l) i = l (b i)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) (F : (c : C) × (d : C) × (c ⟶ d)),
  F ∈ S ↔ F.snd.snd ∈ S.arrows F.fst F.snd.fst
-- Mathlib.AlgebraicGeometry.GluingOneHypercover
AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₁ : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i₁ i₂ : D.J) (x : PUnit.{u + 1}), D.oneHypercover.p₁ x = D.f i₁ i₂
-- Mathlib.Topology.Category.LightProfinite.Sequence
/-- The one point compactification of the natural numbers as a light profinite set.  -/
LightProfinite.NatUnionInfty : LightProfinite
-- Mathlib.Tactic.FunProp.Types
/-- Increase transition depth. Return `none` if maximum transition depth has been reached.  -/
Mathlib.Meta.FunProp.withIncreasedTransitionDepth : {α : Type} → Mathlib.Meta.FunProp.FunPropM (Option α) → Mathlib.Meta.FunProp.FunPropM (Option α)
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addDysonETransform.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommGroup α] (e : α) (x : Finset α × Finset α),
  Finset.addDysonETransform e x = (x.1 ∪ (e +ᵥ x.2), x.2 ∩ (-e +ᵥ x.1))
-- Init.Data.Int.Cooper
Int.dvd_of_mul_dvd : ∀ {a b c : ℤ}, a * b ∣ a * c → 0 < a → b ∣ c
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.Extension.Hom.mapKer.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] (f f_1 : P.Hom P') (e_f : f = f_1)
  [alg : Algebra P.Ring P'.Ring] (halg : algebraMap P.Ring P'.Ring = f.toRingHom), f.mapKer halg = f_1.mapKer ⋯
-- Init.Data.Nat.Lemmas
Nat.add_right_inj : ∀ {m k n : ℕ}, n + m = n + k ↔ m = k
-- Mathlib.Data.List.Permutation
List.mem_permutationsAux2 : ∀ {α : Type u_1} {t : α} {ts ys l l' : List α},
  l' ∈ (List.permutationsAux2 t ts [] ys fun x => l ++ x).2 ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
-- Mathlib.Order.Filter.Map
Filter.eventually_bind : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → Filter β} {p : β → Prop},
  (∀ᶠ (y : β) in f.bind m, p y) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in m x, p y
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.instQuasiCompactFstScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.QuasiCompact g],
  AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Data.Nat.BinaryRec
Nat.bitCasesOn_bit : ∀ {motive : ℕ → Sort u} (h : (b : Bool) → (n : ℕ) → motive (Nat.bit b n)) (b : Bool) (n : ℕ),
  Nat.bitCasesOn (Nat.bit b n) h = h b n
-- Mathlib.Data.Stream.Init
Stream'.map_cons : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α) (s : Stream' α),
  Stream'.map f (Stream'.cons a s) = Stream'.cons (f a) (Stream'.map f s)
-- Init.Data.List.TakeDrop
List.takeWhile_append : ∀ {α : Type u_1} {p : α → Bool} {xs ys : List α},
  List.takeWhile p (xs ++ ys) =
    if (List.takeWhile p xs).length = xs.length then xs ++ List.takeWhile p ys else List.takeWhile p xs
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.isUniformInducing_toUniformOnFun : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : UniformSpace F]
  [inst_7 : IsUniformAddGroup F], IsUniformInducing ContinuousMultilinearMap.toUniformOnFun
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instSmallStrictColimitsOfShapeOfSmallOfLocallySmall : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [CategoryTheory.ObjectProperty.Small.{w, v_1, u_1} P]
  [CategoryTheory.LocallySmall.{w, v_1, u_1} C] [Small.{w, u'} J] [CategoryTheory.LocallySmall.{w, v', u'} J],
  CategoryTheory.ObjectProperty.Small.{w, v_1, u_1} (P.strictColimitsOfShape J)
-- Mathlib.Algebra.LinearRecurrence
LinearRecurrence.mk.inj : ∀ {R : Type u_1} {inst : CommSemiring R} {order : ℕ} {coeffs : Fin order → R} {order_1 : ℕ}
  {coeffs_1 : Fin order_1 → R},
  { order := order, coeffs := coeffs } = { order := order_1, coeffs := coeffs_1 } → order = order_1 ∧ coeffs ≍ coeffs_1
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.State.mk.inj : ∀ {modified : Bool} {mvarId : Lean.MVarId} {entries : Array Lean.Meta.SimpAll.Entry} {ctx : Lean.Meta.Simp.Context}
  {simprocs : Lean.Meta.Simp.SimprocsArray} {usedTheorems : Lean.Meta.Simp.UsedSimps}
  {diag : Lean.Meta.Simp.Diagnostics} {modified_1 : Bool} {mvarId_1 : Lean.MVarId}
  {entries_1 : Array Lean.Meta.SimpAll.Entry} {ctx_1 : Lean.Meta.Simp.Context}
  {simprocs_1 : Lean.Meta.Simp.SimprocsArray} {usedTheorems_1 : Lean.Meta.Simp.UsedSimps}
  {diag_1 : Lean.Meta.Simp.Diagnostics},
  { modified := modified, mvarId := mvarId, entries := entries, ctx := ctx, simprocs := simprocs,
        usedTheorems := usedTheorems, diag := diag } =
      { modified := modified_1, mvarId := mvarId_1, entries := entries_1, ctx := ctx_1, simprocs := simprocs_1,
        usedTheorems := usedTheorems_1, diag := diag_1 } →
    modified = modified_1 ∧
      mvarId = mvarId_1 ∧
        entries = entries_1 ∧ ctx = ctx_1 ∧ simprocs = simprocs_1 ∧ usedTheorems = usedTheorems_1 ∧ diag = diag_1
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.instFunLike : {R : Type u_2} →
  {L : Type u_3} →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] → [inst_7 : LieRing.IsNilpotent L] → FunLike (LieModule.Weight R L M) L R
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.boolKernel_true : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  (ProbabilityTheory.Kernel.boolKernel μ ν) true = ν
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {fallback : β} {f : Option β → Option β}, (t.alter k f).getD k fallback = (f t[k]?).getD fallback
-- Init.Data.Nat.MinMax
Nat.mul_max_mul_left : ∀ (a b c : ℕ), max (a * b) (a * c) = a * max b c
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem.mk.inj : ∀ {label : String} {detail? : Option String} {documentation? : Option Lean.Lsp.MarkupContent}
  {kind? : Option Lean.Lsp.CompletionItemKind} {textEdit? : Option Lean.Lsp.InsertReplaceEdit}
  {sortText? : Option String} {data? : Option Lean.Lsp.ResolvableCompletionItemData}
  {tags? : Option (Array Lean.Lsp.CompletionItemTag)} {label_1 : String} {detail?_1 : Option String}
  {documentation?_1 : Option Lean.Lsp.MarkupContent} {kind?_1 : Option Lean.Lsp.CompletionItemKind}
  {textEdit?_1 : Option Lean.Lsp.InsertReplaceEdit} {sortText?_1 : Option String}
  {data?_1 : Option Lean.Lsp.ResolvableCompletionItemData} {tags?_1 : Option (Array Lean.Lsp.CompletionItemTag)},
  { label := label, detail? := detail?, documentation? := documentation?, kind? := kind?, textEdit? := textEdit?,
        sortText? := sortText?, data? := data?, tags? := tags? } =
      { label := label_1, detail? := detail?_1, documentation? := documentation?_1, kind? := kind?_1,
        textEdit? := textEdit?_1, sortText? := sortText?_1, data? := data?_1, tags? := tags?_1 } →
    label = label_1 ∧
      detail? = detail?_1 ∧
        documentation? = documentation?_1 ∧
          kind? = kind?_1 ∧ textEdit? = textEdit?_1 ∧ sortText? = sortText?_1 ∧ data? = data?_1 ∧ tags? = tags?_1
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_double_succ : Primrec fun n => 2 * n + 1
-- Mathlib.Algebra.Group.Irreducible.Defs
/-- If an irreducible element can be written as a sum, then one term is an additive unit.  -/
AddIrreducible.isAddUnit_or_isAddUnit : ∀ {M : Type u_1} [inst : AddMonoid M] {p : M}, AddIrreducible p → ∀ ⦃a b : M⦄, p = a + b → IsAddUnit a ∨ IsAddUnit b
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.comp_asNatTrans_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e f g : C ≌ D} (α : e ⟶ f) (β : f ⟶ g) {Z : CategoryTheory.Functor C D} (h : g.functor ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.asNatTrans (CategoryTheory.CategoryStruct.comp α β))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.asNatTrans α)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.asNatTrans β) h)
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.range_fiberι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y),
  Set.range ⇑(AlgebraicGeometry.Scheme.Hom.fiberι f y) = ⇑f ⁻¹' {y}
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.uniformContinuous_lift : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β}
  (h : ∀ (a b : α), Inseparable a b → f a = f b), UniformContinuous (SeparationQuotient.lift f h) ↔ UniformContinuous f
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instOne : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [One Y] → One (LocallyConstant X Y)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Modification.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (app : (a : B) → η.app a ⟶ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)) (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
      CategoryTheory.Lax.OplaxTrans.Modification.naturality._autoParam),
  sizeOf { app := app, naturality := naturality } = 1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km fallback : α}, t.max? = some km → t.getD km fallback = km
-- Mathlib.Data.Finset.Pairwise
Set.PairwiseDisjoint.image_finset_of_le : ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι] {s : Finset ι}
  {f : ι → α},
  (↑s).PairwiseDisjoint f → ∀ {g : ι → ι}, (∀ (a : ι), f (g a) ≤ f a) → (↑(Finset.image g s)).PairwiseDisjoint f
-- Mathlib.Analysis.Normed.Field.TransferInstance
/-- Transfer a `NormedField` across an `Equiv`  -/
Equiv.normedField : {α : Type u_1} → {β : Type u_2} → [NormedField β] → α ≃ β → NormedField α
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getOrderedAddInst : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Mathlib.Probability.Moments.SubGaussian
/-- A corollary of Hoeffding's lemma for bounded random variables.  -/
ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ] {a b : ℝ},
  AEMeasurable X μ →
    (∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) →
      ProbabilityTheory.HasSubgaussianMGF (fun ω => X ω - ∫ (x : Ω), X x ∂μ) ((‖b - a‖₊ / 2) ^ 2) μ
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.escapeAux : String → Char → String
-- Mathlib.Analysis.Normed.Group.Uniform
nnnorm_map' : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) (x : E), ‖f x‖₊ = ‖x‖₊
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.of_zeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y)
  [inst_2 : K.HasPullbacks], (∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) → P f
-- Init.Data.List.Lemmas
List.foldl_map_hom : ∀ {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {l : List α},
  (∀ (x y : α), f' (g x) (g y) = g (f x y)) → List.foldl f' (g a) (List.map g l) = g (List.foldl f a l)
-- Mathlib.Topology.Gluing
TopCat.GlueData.isOpen_iff : ∀ (D : TopCat.GlueData) (U : Set ↑D.glued),
  IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) ⁻¹' U)
-- Mathlib.Data.List.Dedup
List.dedup_eq_cons : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (a : α) (l' : List α),
  l.dedup = a :: l' ↔ a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'
-- Init.Data.Vector.Lemmas
Vector.foldlM_append : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n k : ℕ} [inst : Monad m] [LawfulMonad m] {f : β → α → m β}
  {b : β} {xs : Vector α n} {ys : Vector α k},
  Vector.foldlM f b (xs ++ ys) = do
    let b ← Vector.foldlM f b xs
    Vector.foldlM f b ys
-- Mathlib.Logic.Hydra
Relation.cutExpand_zero : ∀ {α : Type u_1} {r : α → α → Prop} {x : α}, Relation.CutExpand r 0 {x}
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.injective_toLp : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [inst_5 : OpensMeasurableSpace E]
  [inst_6 : SecondCountableTopologyEither E F] (p : ENNReal)
  (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.injective_toLp._auto_1) [hμ : μ.HasTemperateGrowth]
  [μ.IsOpenPosMeasure], Function.Injective fun f => f.toLp p μ
-- Init.Core
Sum.nonemptyLeft : ∀ {α : Type u} {β : Type v} [h : Nonempty α], Nonempty (α ⊕ β)
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
/-- If a set in a manifold has the unique derivative property, then its pullback by any extended
chart, in the vector space, also has the unique derivative property.  -/
UniqueMDiffOn.uniqueMDiffOn_target_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} [IsManifold I 1 M],
  UniqueMDiff[s] → ∀ (x : M), UniqueMDiff[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s]
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.α_inv_hom : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y Z : CategoryTheory.FreeMonoidalCategory C}, CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.noSibling_combine : ∀ {α : Type u_1} (le : α → α → Bool) (s : Batteries.PairingHeapImp.Heap α),
  (Batteries.PairingHeapImp.Heap.combine le s).NoSibling
-- Mathlib.Tactic.ProdAssoc
Lean.Expr.ProdTree.prod.sizeOf_spec : ∀ (fst snd : Lean.Expr.ProdTree) (lfst lsnd : Lean.Level),
  sizeOf (fst.prod snd lfst lsnd) = 1 + sizeOf fst + sizeOf snd + sizeOf lfst + sizeOf lsnd
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.Core.comp_mem_uniformity_sets : ∀ {α : Type ua} {c : UniformSpace.Core α} {s : SetRel α α}, s ∈ c.uniformity → ∃ t ∈ c.uniformity, SetRel.comp t t ⊆ s
-- Init.Data.BitVec.BasicAux
/-- Return the bound in terms of toNat.  -/
BitVec.isLt : ∀ {w : ℕ} (x : BitVec w), x.toNat < 2 ^ w
-- Mathlib.Tactic.DepRewrite
/-- The pattern to generalize over.  -/
Mathlib.Tactic.DepRewrite.Context.p : Mathlib.Tactic.DepRewrite.Context → Lean.Expr
-- Mathlib.Tactic.FunProp.FunctionData
/-- Is head function of `f` a constant?

If the head of `f` is a projection return the name of corresponding projection function.  -/
Mathlib.Meta.FunProp.FunctionData.getFnConstName? : Mathlib.Meta.FunProp.FunctionData → Lean.MetaM (Option Lean.Name)
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.GrothendieckTopology.preserveFiniteLimits_plusFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1}
  {CD : D → Type t} [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] [CategoryTheory.Limits.HasFiniteLimits D]
  [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget D)]
  [(CategoryTheory.forget D).ReflectsIsomorphisms], CategoryTheory.Limits.PreservesFiniteLimits (J.plusFunctor D)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.postCongr_hom_app_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F G : CategoryTheory.Functor T D} (e : F ≅ G) (X_1 : CategoryTheory.Under X),
  ((CategoryTheory.Under.postCongr e).hom.app X_1).right = e.hom.app X_1.right
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_omega0 : Ordinal.omega0.cof = Cardinal.aleph0
-- Qq.Delab
Qq.Impl.delabQuotedLevelDefEq : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.tensorUnit_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C},
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X)).hom = CategoryTheory.CategoryStruct.id X
-- Mathlib.Probability.Density
ProbabilityTheory.IndepFun.add_hasPDF : ∀ {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [inst : AddGroup G]
  {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant]
  {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ]
  [MeasureTheory.IsFiniteMeasure ℙ], ProbabilityTheory.IndepFun X Y ℙ → MeasureTheory.HasPDF (X + Y) ℙ μ
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNorm_indicator_const' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {c : ε} {s : Set α},
  MeasurableSet s → μ s ≠ 0 → p ≠ 0 → MeasureTheory.eLpNorm (s.indicator fun x => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)
-- Mathlib.RepresentationTheory.Continuous.Basic
instFunLikeContRepresentationContinuousLinearMapId : (R : Type u_1) →
  (G : Type u_2) →
    (V : Type u_3) →
      [inst : Monoid G] →
        [inst_1 : Ring R] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : TopologicalSpace V] →
              [inst_4 : IsTopologicalAddGroup V] →
                [inst_5 : Module R V] → FunLike (ContRepresentation R G V) G (V →L[R] V)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_prod' : ∀ {α : Type u_1} {β : Type u_2} {f : α × β → ENNReal}, ∑' (p : α × β), f p = ∑' (a : α) (b : β), f (a, b)