mathlib-initiative/mathlib-types huggingface dataset:
-- Init.System.IO
/-- Reads the entire remaining contents of the stream until an end-of-file marker (EOF) is
encountered.

The underlying stream is not automatically closed upon encountering an EOF, and subsequent reads from
the stream may block and/or return data.
 -/
IO.FS.Stream.readBinToEndInto : IO.FS.Stream → ByteArray → IO ByteArray
-- Mathlib.Data.Set.Lattice
Set.sigmaToiUnion_injective : ∀ {α : Type u_1} {β : Type u_2} (t : α → Set β),
  Pairwise (Function.onFun Disjoint t) → Function.Injective (Set.sigmaToiUnion t)
-- Mathlib.Algebra.Group.Units.Hom
MonoidHom.toHomUnitsMulEquiv_apply : ∀ {G : Type u_1} {M : Type u_2} [inst : Group G] [inst_1 : CommMonoid M] (f : G →* M),
  MonoidHom.toHomUnitsMulEquiv f = f.toHomUnits
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
/-- **Alias** of the forward direction of `IntermediateField.adjoin_simple_eq_top_iff_of_isAlgebraic`. -/
Algebra.adjoin_eq_top_of_primitive_element : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  IsAlgebraic F x → F⟮x⟯ = ⊤ → F[x] = ⊤
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesSummable.of_smul : ∀ {f : ℕ → ℂ} {c s : ℂ}, c ≠ 0 → LSeriesSummable (c • f) s → LSeriesSummable f s
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y X' Y' : C}
  (f : X ≅ Y) (g : X' ≅ Y'),
  (CategoryTheory.MonoidalCategory.tensorIso f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.forInUncurried_eq_forIn_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : α × β → δ → m (ForInStep δ)}
  {init : δ}, Std.DTreeMap.Raw.Const.forInUncurried f init t = forIn (Std.DTreeMap.Raw.Const.toList t) init f
-- Init.Data.Int.Order
Int.sub_lt_sub_right_iff : ∀ {a b c : ℤ}, a - c < b - c ↔ a < b
-- Mathlib.MeasureTheory.Function.L2Space
_private.Mathlib.MeasureTheory.Function.L2Space.0.MeasureTheory.L2.norm_sq_eq_re_inner : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (f : ↥(MeasureTheory.Lp E 2 μ)),
  ‖f‖ ^ 2 = RCLike.re (inner 𝕜 f f)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.card_isUnramified : ∀ (k : Type u_1) [inst : Field k] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : NumberField K]
  [inst_4 : NumberField k] [IsGalois k K],
  {w | NumberField.InfinitePlace.IsUnramified k w}.card =
    {w | NumberField.InfinitePlace.IsUnramifiedIn K w}.card * Module.finrank k K
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
_private.Mathlib.NumberTheory.DiophantineApproximation.Basic.0.Real.aux₂ : ∀ {ξ : ℝ} {u v : ℤ}, 2 ≤ v → Real.ContfracLegendre.Ass ξ u v → 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
-- Mathlib.Tactic.CongrExclamation
/-- Try to apply `funext`, but only if it is an equality of two functions where at least one is
a lambda expression.

One thing this check prevents is accidentally applying `funext` to a set equality, but also when
doing congruence we don't want to apply `funext` unnecessarily.
 -/
Lean.MVarId.obviousFunext? : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.Algebra.BigOperators.Finprod
/-- See also `finprod_eq_of_bijective`, `Fintype.prod_bijective` and `Finset.prod_bij`.  -/
finprod_comp : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {g : β → M} (e : α → β),
  Function.Bijective e → ∏ᶠ (i : α), g (e i) = ∏ᶠ (j : β), g j
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- If `L : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ ℰ` is a pointwise left Kan extension
of a functor `A : C ⥤ ℰ` along the Yoneda embedding,
then `L` is a left adjoint of `restrictedULiftYoneda A : ℰ ⥤ Cᵒᵖ ⥤ Type max w v₁ v₂`  -/
CategoryTheory.Presheaf.uliftYonedaAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {ℰ : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ] →
        {A : CategoryTheory.Functor C ℰ} →
          [CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] →
            (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ) →
              (α : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) →
                [L.IsLeftKanExtension α] → L ⊣ CategoryTheory.Presheaf.restrictedULiftYoneda A
-- Init.Data.UInt.Lemmas
USize.ofBitVec_lt_iff_lt : ∀ {a b : BitVec System.Platform.numBits}, { toBitVec := a } < { toBitVec := b } ↔ a < b
-- Mathlib.Logic.Basic
/-- The constant function witnesses that
there exists a function sending a given term to a given term.

This is sometimes useful in `simp` to discharge side conditions.
 -/
exists_apply_eq : ∀ {α : Sort u_1} {β : Sort u_2} (a : α) (b : β), ∃ f, f a = b
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
CategoryTheory.reflectsIsomorphisms_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G)
  [F.ReflectsIsomorphisms], G.ReflectsIsomorphisms
-- Mathlib.Order.CompactlyGenerated.Basic
WellFoundedGT.finite_of_sSupIndep : ∀ {α : Type u_2} [inst : CompleteLattice α] [WellFoundedGT α] {s : Set α}, sSupIndep s → s.Finite
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, l.contains k = false → k ∈ Std.DHashMap.Raw.Const.insertManyIfNewUnit m l → k ∈ m
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
/-- **Alias** of `SimpleGraph.Walk.setOfPred_length_eq_zero`. -/
SimpleGraph.set_walk_self_length_zero_eq : ∀ {V : Type u} (G : SimpleGraph V) (u : V), {p | p.length = 0} = {SimpleGraph.Walk.nil}
-- Mathlib.RingTheory.RootsOfUnity.Basic
rootsOfUnity_one : ∀ (M : Type u_7) [inst : CommMonoid M], rootsOfUnity 1 M = ⊥
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.RingObjCat C} (hom : R₁.X ⟶ R₂.X)
  [isRingHom : CategoryTheory.IsRingHom hom] (hom_1 : R₁.X ⟶ R₂.X) (isRingHom_1 : CategoryTheory.IsRingHom hom_1),
  ({ hom := hom, isRingHom := isRingHom } = { hom := hom_1, isRingHom := isRingHom_1 }) = (hom = hom_1)
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sum'_obj_inr : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A C)
  (G : CategoryTheory.Functor B C) (b : B), (F.sum' G).obj (Sum.inr b) = G.obj b
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_conjTranspose : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : Star α] (A : Matrix n l α)
  (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α),
  (Matrix.fromBlocks A B C D).conjTranspose =
    Matrix.fromBlocks A.conjTranspose C.conjTranspose B.conjTranspose D.conjTranspose
-- Mathlib.Order.SymmDiff
bihimp_right_surjective : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a : α), Function.Surjective fun x => bihimp a x
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.neg_mk : ∀ {α : Type u} [inst : AddMonoid α] (x y : α) (h₁ : x + y = 0) (h₂ : y + x = 0),
  -{ val := x, neg := y, val_neg := h₁, neg_val := h₂ } = { val := y, neg := x, val_neg := h₂, neg_val := h₁ }
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.map_intCast_inj : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [CharZero R]
  {x y : Matrix.SpecialLinearGroup n ℤ},
  (Matrix.SpecialLinearGroup.map (Int.castRingHom R)) x = (Matrix.SpecialLinearGroup.map (Int.castRingHom R)) y ↔ x = y
-- Mathlib.Order.SymmDiff
himp_bihimp_left : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), a ⇨ bihimp a b = a ⇨ b
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.instInhabited : {F : Type u_1} →
  {E : Type u_2} →
    {K : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field E] →
          [inst_2 : Field K] →
            [inst_3 : Algebra F E] → [inst_4 : Algebra F K] → Inhabited (IntermediateField.Lifts F E K)
-- Mathlib.Order.Cofinal
/-- The set of "records" (the smallest inputs yielding the highest values) with respect to a
well-ordering of `α` is a cofinal set.  -/
isCofinal_setOfPred_imp_lt : ∀ {α : Type u_1} [inst : LinearOrder α] (r : α → α → Prop) [h : IsWellFounded α r],
  IsCofinal {a | ∀ (b : α), r b a → b < a}
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.ExprPair.mk.sizeOf_spec : ∀ {w : ℕ} (lhs rhs : Std.Tactic.BVDecide.BVExpr w),
  sizeOf { w := w, lhs := lhs, rhs := rhs } = 1 + sizeOf w + sizeOf lhs + sizeOf rhs
-- Mathlib.Algebra.Order.Ring.Defs
IsStrictOrderedRing.toIsOrderedCancelAddMonoid : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : PartialOrder R} [self : IsStrictOrderedRing R],
  IsOrderedCancelAddMonoid R
-- Mathlib.Data.PNat.Factors
PrimeMultiset.mem_ofNatList : ∀ {p : ℕ+} {l : List ℕ} (hl : ∀ p ∈ l, Nat.Prime p), p ∈ (PrimeMultiset.ofNatList l hl).toPNatMultiset ↔ ↑p ∈ l
-- Init.Data.Vector.Lemmas
Vector.foldl_mk : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {f : β → α → β} {b : β} {xs : Array α} (h : xs.size = n),
  Vector.foldl f b (Vector.mk xs h) = Array.foldl f b xs
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.H1π_comp_map_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : groupCohomology B 1 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.H1π A)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.map f φ 1) h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.mapCocycles₁ f φ)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.H1π B) h)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.addNewPattern : Lean.Expr → Lean.Meta.Grind.CollectorM✝ Unit
-- Init.Data.Vector.Lemmas
Vector.back_singleton : ∀ {α : Type u_1} {a : α}, #v[a].back = a
-- Mathlib.RingTheory.KrullDimension.Module
Module.supportDim_le_of_injective : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  Function.Injective ⇑f → Module.supportDim R M ≤ Module.supportDim R N
-- Init.Data.List.SplitOn.Lemmas
List.splitOnPPrepend_ne_nil : ∀ {α : Type u_1} (p : α → Bool) (xs acc : List α), List.splitOnPPrepend p xs acc ≠ []
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.GrothendieckTopology.preservesLimitsOfShape_diagramFunctor : ∀ {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)]
  (X : C) (K : Type s) [inst_3 : CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D],
  CategoryTheory.Limits.PreservesLimitsOfShape K (J.diagramFunctor D X)
-- Mathlib.Topology.Homotopy.Path
/-- If paths `p` and `q` are homotopic as paths `x ⟶ y`,
then they are homotopic as paths `x' ⟶ y'`, where `x' = x` and `y' = y`.  -/
Path.Homotopic.pathCast : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ x₂ x₃ : X} {p q : Path x₀ x₁},
  p.Homotopic q → ∀ (hsource : x₂ = x₀) (htarget : x₃ = x₁), (p.cast hsource htarget).Homotopic (q.cast hsource htarget)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.restrictScalars_curry : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] (f : TensorProduct R M N →ₗ[A] P),
  ↑R (TensorProduct.AlgebraTensorModule.curry f) = TensorProduct.curry (↑R f)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {h' : a ∈ m.erase k}, (m.erase k)[a] = m[a]
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.instLawfulForwardPatternModelForallCharProp : ∀ {p : Char → Prop} [inst : DecidablePred p], String.Slice.Pattern.Model.LawfulForwardPatternModel p
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsFragment.smul_finset : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A S : Finset G} (a : G),
  Finset.IsFragment✝ K S A → Finset.IsFragment✝ K S (a • A)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
nndist_toDual : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] (a b : X), nndist (OrderDual.toDual a) (OrderDual.toDual b) = nndist a b
-- Std.Data.TreeMap.Raw.Lemmas
_private.Std.Data.TreeMap.Raw.Lemmas.0.Std.TreeMap.Raw.equiv_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.Equiv t₂ ↔ t₁.inner.Equiv t₂.inner
-- Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization
Submonoid.LocalizationMap.eq_isUnit_map_mul_irreducible_of_irreducible_map : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoidWithZero M] [inst_1 : CommMonoidWithZero N] {S : Submonoid M}
  [WfDvdMonoid M] (f : S.LocalizationMap N) {m : M},
  Irreducible (f m) → ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ m = u * m'
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.opNorm_smul_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {𝕜' : Type u_9}
  [inst_7 : DistribSMul 𝕜' F] [inst_8 : SMulCommClass 𝕜₂ 𝕜' F] [inst_9 : SeminormedAddCommGroup 𝕜']
  [inst_10 : IsBoundedSMul 𝕜' F] (c : 𝕜') (f : E →SL[σ₁₂] F), ‖c • f‖ ≤ ‖c‖ * ‖f‖
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_eq_some_get : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α} {h' : a ∈ t}, t.get? a = some (t.get a h')
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mcasesPat#_» : Lean.ParserDescr
-- Init.Data.Vector.Lemmas
Vector.mem_cast : ∀ {α : Type u_1} {n m : ℕ} {a : α} {xs : Vector α n} {w : n = m}, a ∈ Vector.cast w xs ↔ a ∈ xs
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- Auxiliary structure used in the proof of `Scheme.Modules.isIso_fromTildeΓ_of_isQuasicoherent`.
These are conditions d1) and d2) from [Theoreme 1.4.1, grothendieck-1971].  -/
_private.Mathlib.AlgebraicGeometry.Modules.Tilde.0.AlgebraicGeometry.QuasicoherentTilde.Aux : {R : CommRingCat} → (AlgebraicGeometry.Spec R).Modules → (AlgebraicGeometry.Spec R).Opens → Prop
-- Lean.Meta.Tactic.Grind.Beta
/-- For each `lam` in `lams` s.t. `lam` and `f` are in the same equivalence class,
propagate `f args = lam args`.
 -/
Lean.Meta.Grind.propagateBetaEqs : Array Lean.Expr → Lean.Expr → Array Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.isoMk_hom : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i}
  (iso : (i : I) → X i ≅ Y i) (i : I), (CategoryTheory.Pi.isoMk iso).hom i = (iso i).hom
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The preimage of an `AddSubmonoid` along an `AddMonoidHom` is an `AddSubmonoid`.  -/
AddSubmonoid.comap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {F : Type u_4} → [inst_2 : FunLike F M N] → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid N → AddSubmonoid M
-- Mathlib.Probability.Independence.Conditional
/-- **Alias** of `ProbabilityTheory.iCondIndepFun.condIndepFun_finsetSum_of_notMem`. -/
ProbabilityTheory.iCondIndepFun.condIndepFun_finset_sum_of_notMem : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β}
  [inst_2 : AddCommMonoid β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.CondIndepFun m' hm' (∑ j ∈ s, f j) (f i) μ
-- Mathlib.Algebra.Order.Group.MinMax
max_div_div_right' : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] (a b c : α),
  max (a / c) (b / c) = max a b / c
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.of_hasTerminal : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.IsFiltered C
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Non-dependent recursion principle for localizations: given elements `f a b : p`
for all `a b`, such that `r S (a, b) (c, d)` implies `f a b = f c d`,
then `f` is defined on the whole `Localization S`.  -/
Localization.liftOn : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {p : Sort u} →
        Localization S →
          (f : M → ↥S → p) → (∀ {a c : M} {b d : ↥S}, (Localization.r S) (a, b) (c, d) → f a b = f c d) → p
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
AddCircle.measurableEquivIoc.eq_1 : ∀ (T : ℝ) [hT : Fact (0 < T)] (a : ℝ),
  AddCircle.measurableEquivIoc T a =
    { toEquiv := AddCircle.equivIoc T a, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.builder_nameSimp : Lean.ParserDescr
-- Lean.Meta.Basic
/-- "Context" for a postponed universe constraint.
`lhs` and `rhs` are the surrounding `isDefEq` call when the postponed constraint was created.
 -/
Lean.Meta.DefEqContext : Type
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.vaddConst_symm_apply : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : TopologicalSpace V₁]
  [inst_6 : IsTopologicalAddTorsor P₁] (p p' : P₁), (ContinuousAffineEquiv.vaddConst k p).symm p' = p' -ᵥ p
-- Init.Data.Nat.Basic
Nat.lt_of_not_ge : ∀ {a b : ℕ}, ¬b ≥ a → b < a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.subst.injEq : ∀ (x : Int.Internal.Linear.Var) (c₁ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr)
  (c₂ : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr) (x_1 : Int.Internal.Linear.Var)
  (c₁_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (c₂_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.subst x c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.subst x_1 c₁_1 c₂_1) =
    (x = x_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsZeroOrMarkovKernel.mk : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β},
  κ = 0 ∨ ProbabilityTheory.IsMarkovKernel κ → ProbabilityTheory.IsZeroOrMarkovKernel κ
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.centralizer_centralizer : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  (S : VonNeumannAlgebra H), (↑S).centralizer.centralizer = ↑S
-- Mathlib.Algebra.Lie.SkewAdjoint
skewAdjointLieSubalgebraEquiv_apply : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) {N : Type w} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : N ≃ₗ[R] M)
  (f : ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e))), ↑((skewAdjointLieSubalgebraEquiv B e) f) = e.lieConj ↑f
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The `n`th monomial with coefficient `a` as formal power series.  -/
PowerSeries.monomial : {R : Type u_1} → [inst : Semiring R] → ℕ → R →ₗ[R] PowerSeries R
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Context.mutableVars : Lean.Elab.Term.Do.ToCodeBlock.Context → Lean.Elab.Term.Do.VarSet
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.addAndCompileUnsafe : Lean.LocalContext × Lean.LocalInstances →
  Array Lean.Elab.PreDefinition → optParam Lean.DefinitionSafety Lean.DefinitionSafety.unsafe → Lean.Elab.TermElabM Unit
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_le_prod_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {l : List (Equiv.Perm α)},
  f ∈ l → List.Pairwise Equiv.Perm.Disjoint l → f.support ⊆ l.prod.support
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.compAlongComposition_nnnorm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
  (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n),
  ‖q.compAlongComposition p c‖₊ ≤ ‖q c.length‖₊ * ∏ i, ‖p (c.blocksFun i)‖₊
-- Mathlib.Algebra.MvPolynomial.SchwartzZippel
/-- The **Schwartz-Zippel lemma**

For a nonzero multivariable polynomial `p` over an integral domain, the probability that `p`
evaluates to zero at points drawn at random from a product of finite subsets `S i` of the integral
domain is bounded by the supremum of `∑ i, degᵢ s / #(S i)` ranging over monomials `s` of `p`.  -/
MvPolynomial.schwartz_zippel_sup_sum : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [inst_2 : DecidableEq R] {n : ℕ} {p : MvPolynomial (Fin n) R},
  p ≠ 0 →
    ∀ (S : Fin n → Finset R),
      ↑{x ∈ Fintype.piFinset fun i => S i | (MvPolynomial.eval x) p = 0}.card / ∏ i, ↑(S i).card ≤
        p.support.sup fun s => ∑ i, ↑(s i) / ↑(S i).card
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty α]
  (κ : ProbabilityTheory.Kernel α β), κ.bound = 0
-- Mathlib.Algebra.Ring.ULift
ULift.mulZeroClass : {M₀ : Type u_1} → [MulZeroClass M₀] → MulZeroClass (ULift.{u_2, u_1} M₀)
-- Mathlib.MeasureTheory.Order.Lattice
Finset.measurable_range_sup'' : ∀ {α : Type u_2} {m : MeasurableSpace α} {δ : Type u_3} [inst : MeasurableSpace δ] [inst_1 : SemilatticeSup α]
  [MeasurableSup₂ α] {f : ℕ → δ → α} {n : ℕ},
  (∀ k ≤ n, Measurable (f k)) → Measurable fun x => (Finset.range (n + 1)).sup' ⋯ fun k => f k x
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_tower`.

---

See `ramificationIdx_tower'` for a version that only assumes local flatness.  -/
Ideal.ramificationIdx'_tower : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.LiesOver q] [Module.Flat S T], r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S