mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.surjective_eq_epimorphisms_iff : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC],
  CategoryTheory.MorphismProperty.surjective C = CategoryTheory.MorphismProperty.epimorphisms C ↔
    (CategoryTheory.forget C).PreservesEpimorphisms
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.cast_refl : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {i : ℕ}
  (h : i = i), TensorPower.cast R M h = LinearEquiv.refl R (TensorPower R i M)
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.eq_pow_of_pell : ∀ {m n k : ℕ},
  n ^ k = m ↔
    k = 0 ∧ m = 1 ∨
      0 < k ∧
        (n = 0 ∧ m = 0 ∨
          0 < n ∧
            ∃ w a t z,
              ∃ (a1 : 1 < a),
                Pell.xn a1 k ≡ Pell.yn a1 k * (a - n) + m [MOD t] ∧
                  2 * a * n = t + (n * n + 1) ∧
                    m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)
-- Mathlib.Order.Partition.Finpartition
Finpartition.combine.eq_1 : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α]
  {ι : Type u_2} {I : Finset ι} {a : ι → α} (P : (i : ι) → Finpartition (a i)) (ha : I.SupIndep a),
  Finpartition.combine P ha =
    { parts := I.biUnion fun i => (P i).parts, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
-- Std.Internal.UV.System
/-- Gets the scheduling priority of a process.
 -/
Std.Internal.UV.System.osGetPriority : UInt64 → IO Int64
-- Mathlib.RingTheory.MatrixAlgebra
Matrix.kroneckerAlgEquiv_symm_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (x : Matrix (m × n) (m × n) R),
  (Matrix.kroneckerAlgEquiv m n R).symm x = (kroneckerLinearEquiv m m n n R).symm x
-- Mathlib.Order.Bounds.Basic
union_lowerBounds_subset_lowerBounds_inter : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, lowerBounds s ∪ lowerBounds t ⊆ lowerBounds (s ∩ t)
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.kernelIsoKer_hom_comp_subtype : ∀ {G H : AddCommGrpCat} (f : G ⟶ H),
  CategoryTheory.CategoryStruct.comp (AddCommGrpCat.kernelIsoKer f).hom
      (AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f).ker.subtype) =
    CategoryTheory.Limits.kernel.ι f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.instIsMultiplicativeFunctorEquifibered : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C], CategoryTheory.NatTrans.Equifibered.IsMultiplicative
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_add : ∀ {A : Type u_3} {E : Type u_4} (x y : WithCStarModule A E) [inst : AddCommGroup E],
  (WithCStarModule.equiv A E) (x + y) = (WithCStarModule.equiv A E) x + (WithCStarModule.equiv A E) y
-- Mathlib.Logic.Equiv.Finset
Denumerable.raise_lower' : ∀ {l : List ℕ} {n : ℕ}, (∀ m ∈ l, n ≤ m) → l.SortedLT → Denumerable.raise' (Denumerable.lower' l n) n = l
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).Q = h.Q
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (l : Filter α) (f g : α → β), (f =ᶠ[l] g) = ∀ᶠ (x : α) in l, f x = g x
-- Mathlib.Order.CompleteLattice.Defs
/-- Note that we rarely use `CompleteSemilatticeInf`
(in fact, any such object is always a `CompleteLattice`, so it's usually best to start there).

Nevertheless it is sometimes a useful intermediate step in constructions.
 -/
CompleteSemilatticeInf : Type u_8 → Type u_8
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_mul : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (I J : Ideal ↑(X.presheaf.obj (Opposite.op U))),
  X.zeroLocus ↑(I * J) = X.zeroLocus ↑I ∪ X.zeroLocus ↑J
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.cosh_lt_cosh : ∀ {x y : ℝ}, Real.cosh x < Real.cosh y ↔ |x| < |y|
-- Mathlib.ModelTheory.Algebra.Field.Basic
_private.Mathlib.ModelTheory.Algebra.Field.Basic.0.FirstOrder.Field.FieldAxiom.toSentence.match_1.eq_5 : ∀ (motive : FirstOrder.Field.FieldAxiom → Sort u_1) (h_1 : Unit → motive FirstOrder.Field.FieldAxiom.addAssoc)
  (h_2 : Unit → motive FirstOrder.Field.FieldAxiom.zeroAdd)
  (h_3 : Unit → motive FirstOrder.Field.FieldAxiom.negAddCancel)
  (h_4 : Unit → motive FirstOrder.Field.FieldAxiom.mulAssoc) (h_5 : Unit → motive FirstOrder.Field.FieldAxiom.mulComm)
  (h_6 : Unit → motive FirstOrder.Field.FieldAxiom.oneMul) (h_7 : Unit → motive FirstOrder.Field.FieldAxiom.existsInv)
  (h_8 : Unit → motive FirstOrder.Field.FieldAxiom.leftDistrib)
  (h_9 : Unit → motive FirstOrder.Field.FieldAxiom.existsPairNE),
  (match FirstOrder.Field.FieldAxiom.mulComm with
    | FirstOrder.Field.FieldAxiom.addAssoc => h_1 ()
    | FirstOrder.Field.FieldAxiom.zeroAdd => h_2 ()
    | FirstOrder.Field.FieldAxiom.negAddCancel => h_3 ()
    | FirstOrder.Field.FieldAxiom.mulAssoc => h_4 ()
    | FirstOrder.Field.FieldAxiom.mulComm => h_5 ()
    | FirstOrder.Field.FieldAxiom.oneMul => h_6 ()
    | FirstOrder.Field.FieldAxiom.existsInv => h_7 ()
    | FirstOrder.Field.FieldAxiom.leftDistrib => h_8 ()
    | FirstOrder.Field.FieldAxiom.existsPairNE => h_9 ()) =
    h_5 ()
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.instOne : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → One (N ⋊[φ] G)
-- Mathlib.Analysis.Calculus.ContDiff.Convolution
/-- Compute the total derivative of `f ⋆ g` if `g` is `C^1` with compact support and `f` is locally
integrable. To write down the total derivative as a convolution, we use
`ContinuousLinearMap.precompR`.  -/
HasCompactSupport.hasFDerivAt_convolution_right : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'} [inst_3 : RCLike 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F]
  [inst_8 : MeasurableSpace G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [inst_9 : NormedAddCommGroup G]
  [BorelSpace G] [inst_11 : NormedSpace 𝕜 G] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant],
  HasCompactSupport g →
    MeasureTheory.LocallyIntegrable f μ →
      ContDiff 𝕜 1 g →
        ∀ (x₀ : G),
          HasFDerivAt (MeasureTheory.convolution f g L μ)
            (MeasureTheory.convolution f (fderiv 𝕜 g) (ContinuousLinearMap.precompR G L) μ x₀) x₀
-- Mathlib.NumberTheory.Real.Irrational
irrational_sqrt_intCast_iff : ∀ {z : ℤ}, Irrational √↑z ↔ ¬IsSquare z ∧ 0 ≤ z
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.rightUnitor_hom_left_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : A),
  φ.rightUnitor.hom.left.app X = CategoryTheory.CategoryStruct.id (φ.left.obj X)
-- Mathlib.Data.DFinsupp.Module
/-- Dependent functions with finite support inherit a semiring action from an action on each
coordinate.  -/
DFinsupp.instSMulZeroClass : {ι : Type u} →
  {γ : Type w} →
    {β : ι → Type v} →
      [inst : (i : ι) → Zero (β i)] → [(i : ι) → SMulZeroClass γ (β i)] → SMulZeroClass γ (Π₀ (i : ι), β i)
-- Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {I : Ideal R} {x : S},
  IsIntegral (↥(Algebra.adjoin R {x | ∃ r ∈ I, Polynomial.C r * Polynomial.X = x})) (Polynomial.C x * Polynomial.X) →
    ∃ p, p.Monic ∧ (Polynomial.aeval x) p = 0 ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
-- Init.Coe
/-- `CoeSort α β` is a coercion to a sort. `β` must be a universe, and this is
triggered when `a : α` appears in a place where a type is expected, like
`(x : a)` or `a → a`.
`CoeSort` instances apply to `CoeOut` as well.
 -/
CoeSort : Sort u → outParam (Sort v) → Sort (max (max 1 u) v)
-- Mathlib.Logic.Equiv.Basic
/-- The set of natural numbers is equivalent to `ℕ ⊕ PUnit`.  -/
Equiv.natEquivNatSumPUnit : ℕ ≃ ℕ ⊕ PUnit.{u_9 + 1}
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.neg_iInf : ∀ {G : Type u_2} [inst : AddGroup G] {ι : Sort u_7} (S : ι → AddSubmonoid G), -⨅ i, S i = ⨅ i, -S i
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H1_induction_on : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {C : ↑(groupHomology.H1 A) → Prop}
  (x : ↑(groupHomology.H1 A)),
  (∀ (x : ↥(groupHomology.cycles₁ A)), C ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A)) x)) → C x
-- Mathlib.Data.Finset.Image
/-- Associate to an embedding `f` from `α` to `β` the order embedding that maps a finset to its
image under `f`.  -/
Finset.mapEmbedding : {α : Type u_1} → {β : Type u_2} → (α ↪ β) → Finset α ↪o Finset β
-- Mathlib.Algebra.Order.Sub.Defs
tsub_le_iff_tsub_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a - c ≤ b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
/-- **Alias** of `CategoryTheory.NatTrans.Equifibered.of_discrete`. -/
CategoryTheory.NatTrans.equifibered_of_discrete : ∀ {C : Type u_3} {ι : Type u_5} [inst : CategoryTheory.Category.{v_2, u_3} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} (α : F ⟶ G), CategoryTheory.NatTrans.Equifibered α
-- Mathlib.Data.Matrix.Diagonal
Matrix.submatrix_one_embedding : ∀ {l : Type u_1} {m : Type u_2} {α : Type v} [inst : Zero α] [inst_1 : One α] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq l] (e : l ↪ m), Matrix.submatrix 1 ⇑e ⇑e = 1
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max!_erase_eq_of_not_compare_max!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, t.erase k ≠ ∅ → ¬cmp k t.max! = Ordering.eq → (t.erase k).max! = t.max!
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.isoMk_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F G : CategoryTheory.LaxBraidedFunctor C D} (e : F.toFunctor ≅ G.toFunctor)
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal e.hom],
  (CategoryTheory.LaxBraidedFunctor.isoMk e).hom = CategoryTheory.LaxBraidedFunctor.homMk e.hom
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_diff_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₁.isEmpty = true → (m₁ \ m₂).isEmpty = true
-- Mathlib.Order.Nucleus
/-- The smallest nucleus is the identity.  -/
Nucleus.instBot : {X : Type u_1} → [inst : SemilatticeInf X] → OrderBot (Nucleus X)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_split_ineq_cert.eq_1 : ∀ (p₁ p₂ : Int.Internal.Linear.Poly) (k b : ℤ) (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_dvd_left_split_ineq_cert p₁ p₂ k b p' =
    (p₂.leadCoeff.beq' b).and'
      (p'.beq' ((Int.Internal.Linear.Poly.combine_mul_k b (-p₁.leadCoeff) p₁.tail p₂.tail).addConst_k (b * k)))
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.parsePosixTzP : optParam Bool false → Std.Internal.Parsec.String.Parser Std.Time.TimeZone.RecurringRule
-- Init.Data.SInt.Lemmas
Int32.toInt_minValue : Int32.minValue.toInt = -2 ^ 31
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.M.map_mk : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) {j k : J} (f : j ⟶ k)
  (x : ↑(F.obj j)),
  MonCat.FilteredColimits.M.mk F ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x⟩ =
    MonCat.FilteredColimits.M.mk F ⟨j, x⟩
-- Mathlib.Tactic.Linter.HashCommandLinter
/-- The linter emits a warning on any command beginning with `#` that itself emits no message.
For example, `#guard true` and `#check_tactic True ~> True by skip` trigger a message.
There is a list of silent `#`-command that are allowed.
 -/
Mathlib.Linter.linter.hashCommand : Lean.Option Bool
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
NormedAddGroupHom.ker.lift.congr_simp : ∀ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] (f f_1 : NormedAddGroupHom V₁ V₂)
  (e_f : f = f_1) (g : NormedAddGroupHom V₂ V₃) (h : g.comp f = 0),
  NormedAddGroupHom.ker.lift f g h = NormedAddGroupHom.ker.lift f_1 g ⋯
-- Mathlib.RepresentationTheory.Basic
/-- A `G`-action on `H` induces a representation `G →* End(k[H])` in the natural way.  -/
Representation.ofMulAction : (k : Type u_1) →
  [inst : Semiring k] →
    (G : Type u_2) → [inst_1 : Monoid G] → (H : Type u_3) → [MulAction G H] → Representation k G (MonoidAlgebra k H)
-- Std.Http.Protocol.H1
/-- Closes the writer side, preventing any further message output.
 -/
Std.Http.Protocol.H1.Machine.closeWriter : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.MeasureTheory.Measure.Prod
/-- The symmetric version of Tonelli's Theorem for set integrals: For `ℝ≥0∞`-valued almost
everywhere measurable functions on `s ×ˢ t`, the integral of `f` on `s ×ˢ t` is equal to the
iterated integral on `t` and `s` respectively.  -/
MeasureTheory.setLIntegral_prod_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set α} {t : Set β}
  (f : α × β → ENNReal),
  AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t)) →
    ∫⁻ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν
-- Mathlib.GroupTheory.OrderOfElement
/-- If `S` is a nonempty subset of a finite group `G`, then `S ^ |G|` is a subgroup  -/
powCardSubgroup : {G : Type u_6} → [inst : Group G] → [Fintype G] → (S : Set G) → S.Nonempty → Subgroup G
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_neg : ∀ {A : Type u_3} {E : Type u_4} (x : WithCStarModule A E) [inst : AddCommGroup E],
  (WithCStarModule.equiv A E) (-x) = -(WithCStarModule.equiv A E) x
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.instIsEquivalenceRightExtensionPostcomp₁OfIsIso : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') [G.IsEquivalence] (f : L.comp G ⟶ L') [CategoryTheory.IsIso f]
  (F : CategoryTheory.Functor C H), (CategoryTheory.Functor.RightExtension.postcomp₁ G f F).IsEquivalence
-- Mathlib.Data.Countable.Defs
Prop.countable' : Countable Prop
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.mono_lift_of_mono_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Mono g],
  CategoryTheory.Mono (CategoryTheory.Limits.prod.lift f g)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.foldr_eq_foldr_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {δ : Type w} {f : α → δ → δ} {init : δ},
  Std.TreeSet.Raw.foldr f init t = List.foldr f init t.toList
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.integral_linearMap_gaussianReal : ∀ {μ : ℝ} {v : NNReal} (L : ℝ →ₗ[ℝ] ℝ), ∫ (x : ℝ), L x ∂ProbabilityTheory.gaussianReal μ v = L μ
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
Cardinal.ord_cardinalMk : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [IsRegularCardinalOrder α],
  (Cardinal.mk α).ord = Ordinal.type fun x1 x2 => x1 < x2
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instEssentiallySmallOppositeOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P.op
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Construct a homeomorphism from an invertible continuous linear map.  -/
ContinuousLinearMap.homeomorphOfUnit : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] → [inst_3 : Module R₁ M₁] → (M₁ →L[R₁] M₁)ˣ → M₁ ≃ₜ M₁
-- Mathlib.Algebra.Group.Hom.Defs
/-- Turn an element of a type `F` satisfying `AddMonoidHomClass F M N` into an
actual `MonoidHom`. This is declared as the default coercion from `F` to `M →+ N`.  -/
AddMonoidHomClass.toAddMonoidHom : {M : Type u_4} →
  {N : Type u_5} →
    {F : Type u_9} →
      [inst : AddZero M] → [inst_1 : AddZero N] → [inst_2 : FunLike F M N] → [AddMonoidHomClass F M N] → F → M →+ N
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.cond.match_1.splitter : (motive : Bool → Sort u_1) → (c : Bool) → (Unit → motive true) → (Unit → motive false) → motive c
-- Lean.Meta.Basic
Lean.Meta.Diagnostics.mk.inj : ∀ {unfoldCounter unfoldAxiomCounter heuristicCounter instanceCounter : Lean.PHashMap Lean.Name ℕ}
  {synthPendingFailures : Lean.PHashMap Lean.Expr Lean.MessageData}
  {unfoldCounter_1 unfoldAxiomCounter_1 heuristicCounter_1 instanceCounter_1 : Lean.PHashMap Lean.Name ℕ}
  {synthPendingFailures_1 : Lean.PHashMap Lean.Expr Lean.MessageData},
  { unfoldCounter := unfoldCounter, unfoldAxiomCounter := unfoldAxiomCounter, heuristicCounter := heuristicCounter,
        instanceCounter := instanceCounter, synthPendingFailures := synthPendingFailures } =
      { unfoldCounter := unfoldCounter_1, unfoldAxiomCounter := unfoldAxiomCounter_1,
        heuristicCounter := heuristicCounter_1, instanceCounter := instanceCounter_1,
        synthPendingFailures := synthPendingFailures_1 } →
    unfoldCounter = unfoldCounter_1 ∧
      unfoldAxiomCounter = unfoldAxiomCounter_1 ∧
        heuristicCounter = heuristicCounter_1 ∧
          instanceCounter = instanceCounter_1 ∧ synthPendingFailures = synthPendingFailures_1
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.instDecidablePredMemSetCarrierOfNormalOfDecidableEqOfFintypeAlgEquiv : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [Normal K L] →
            [DecidableEq L] → [Fintype Gal(L/K)] → (c : ConjRootClass K L) → DecidablePred fun x => x ∈ c.carrier
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_1_comp_chainsIso₁_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : (Fin 1 → G) →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₁ B).hom)
      ((CategoryTheory.ConcreteCategory.hom ((groupHomology.chainsMap f φ).f 1)) x) =
    Finsupp.mapRange ⇑(Rep.Hom.hom φ) ⋯
      (Finsupp.mapDomain (⇑f) ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₁ A).hom) x))
-- Mathlib.GroupTheory.Nilpotent
/-- A subgroup of a nilpotent group is nilpotent.  -/
Subgroup.isNilpotent : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [hG : Group.IsNilpotent G], Group.IsNilpotent ↥H
-- Std.Time.Date.Unit.Month
_private.Std.Time.Date.Unit.Month.0.Std.Time.Month.Ordinal.cumulativeDays.eq_1 : ∀ (leap : Bool) (month : Std.Time.Month.Ordinal),
  Std.Time.Month.Ordinal.cumulativeDays leap month =
    match Std.Time.Month.Ordinal.cumulativeSizes✝ with
    | ⟨months, p⟩ =>
      let index := (Std.Time.Internal.Bounded.LE.sub month 1).toFin Std.Time.Month.Ordinal.days._proof_1✝;
      have res := months[⋯.mp index];
      res + if leap = true ∧ ↑month > 2 then 1 else 0
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
/-- The bounded continuous mapping `fun v ↦ e (L v w)` from `V` to `ℂ`.  -/
BoundedContinuousFunction.char : {V : Type u_1} →
  {W : Type u_2} →
    [inst : AddCommGroup V] →
      [inst_1 : Module ℝ V] →
        [inst_2 : TopologicalSpace V] →
          [inst_3 : AddCommGroup W] →
            [inst_4 : Module ℝ W] →
              [inst_5 : TopologicalSpace W] →
                {e : AddChar ℝ Circle} →
                  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} →
                    Continuous ⇑e → (Continuous fun p => (L p.1) p.2) → W → BoundedContinuousFunction V ℂ
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Adjunction.map_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) [F.PreservesMonomorphisms] (I : D), CategoryTheory.Injective I → CategoryTheory.Injective (G.obj I)
-- Init.Data.Nat.Gcd
Nat.gcd_sub_left_left_of_dvd : ∀ {n k : ℕ} (m : ℕ), n ≤ k → m ∣ k → (k - n).gcd m = n.gcd m
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The inclusion of `C` into `WithInitial C`.  -/
CategoryTheory.WithInitial.incl : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.WithInitial C)
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If `f` is a monotone function on a right neighborhood of `a` and the image of this neighborhood
under `f` meets every interval `(f a, b)`, `b > f a`, then `f` is continuous at `a` from the right.

The assumption `hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b` cannot be replaced by the weaker
assumption `hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b` we use for strictly monotone functions
because otherwise the function `ceil : ℝ → ℤ` would be a counter-example at `a = 0`.  -/
continuousWithinAt_right_of_monotoneOn_of_exists_between : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α},
  MonotoneOn f s →
    s ∈ nhdsWithin a (Set.Ici a) → (∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioo (f a) b) → ContinuousWithinAt f (Set.Ici a) a
-- Mathlib.Probability.Martingale.Upcrossing
/-- A variant of Doob's upcrossing estimate obtained by taking the supremum on both sides.  -/
MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ}
  {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ] (a b : ℝ),
  MeasureTheory.Submartingale f ℱ μ →
    ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), MeasureTheory.upcrossings a b f ω ∂μ ≤
      ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ