mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Basic
/-- The kernel from `Bool` that sends `false` to `μ` and `true` to `ν`.  -/
ProbabilityTheory.Kernel.boolKernel : {α : Type u_1} →
  {mα : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → ProbabilityTheory.Kernel Bool α
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_rev_Iic : ∀ {n : ℕ} (i : Fin n), Fin.rev ⁻¹' Set.Iic i = Set.Ici i.rev
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Zipper.consEntries.injEq : ∀ {α : Type u} {β : Type v} (a : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)))
  (a_1 : Lean.PersistentHashMap.Zipper α β)
  (a_2 : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)))
  (a_3 : Lean.PersistentHashMap.Zipper α β),
  (Lean.PersistentHashMap.Zipper.consEntries a a_1 = Lean.PersistentHashMap.Zipper.consEntries a_2 a_3) =
    (a = a_2 ∧ a_1 = a_3)
-- Lean.Setup
Lean.ImportArtifacts.ofArrays.injEq : ∀ (toArrays toArrays_1 : Array (Array System.FilePath)),
  ({ toArrays := toArrays } = { toArrays := toArrays_1 }) = (toArrays = toArrays_1)
-- Mathlib.Data.ENat.Lattice
ENat.iInf_add_iInf_of_monotone : ∀ {ι : Type u_4} [inst : Preorder ι] [IsCodirectedOrder ι] {f g : ι → ℕ∞},
  Monotone f → Monotone g → iInf f + iInf g = ⨅ a, f a + g a
-- Mathlib.RingTheory.Coalgebra.TensorProduct
_private.Mathlib.RingTheory.Coalgebra.TensorProduct.0.Coalgebra.«term_◁_» : Lean.TrailingParserDescr
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_sphere : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.sphere x ε ↔ dist y x = ε
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of `hasDerivWithinAt_sdiff_singleton`. -/
hasDerivWithinAt_diff_singleton : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' (s \ {x}) x ↔ HasDerivWithinAt f f' s x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.toList_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (m : Std.DHashMap.Internal.Raw₀ α β)
  {f : (a : α) → β a → Option (γ a)},
  (↑(Std.DHashMap.Internal.Raw₀.filterMap f m)).toList.Perm
    (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) (↑m).toList)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.verts_sSup : ∀ {V : Type u} {G : SimpleGraph V} (s : Set G.Subgraph), (sSup s).verts = ⋃ G' ∈ s, G'.verts
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.prod_inter_normalizedFactors_ne_zero : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : DecidableEq α]
  [inst_3 : NormalizationMonoid α] [Nontrivial α] (a b : α),
  (UniqueFactorizationMonoid.normalizedFactors a ∩ UniqueFactorizationMonoid.normalizedFactors b).prod ≠ 0
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.HasIntegral.mono : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F} {l₁ l₂ : BoxIntegral.IntegrationParams},
  BoxIntegral.HasIntegral I l₁ f vol y → l₂ ≤ l₁ → BoxIntegral.HasIntegral I l₂ f vol y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.minKeyD_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β},
  Std.ExtDTreeMap.Const.modify t k f ≠ ∅ →
    ∀ {fallback : α},
      (Std.ExtDTreeMap.Const.modify t k f).minKeyD fallback =
        if cmp (t.minKeyD fallback) k = Ordering.eq then k else t.minKeyD fallback
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.forgetToSheafModuleCat_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) {X_1 Y : SheafOfModules R}
  (f : X_1 ⟶ Y),
  ((SheafOfModules.forgetToSheafModuleCat R X hX).map f).hom =
    (PresheafOfModules.forgetToPresheafModuleCat X hX).map f.val
-- Mathlib.Algebra.Regular.Pi
Pi.isRegular_iff : ∀ {ι : Type u_1} {R : ι → Type u_3} [inst : (i : ι) → Mul (R i)] {a : (i : ι) → R i},
  IsRegular a ↔ ∀ (i : ι), IsRegular (a i)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.ε₁_def : ∀ {I : Type u_7} [inst : AddMonoid I] (c : ComplexShape I) [inst_1 : c.TensorSigns] (x : I × I),
  TotalComplexShape.ε₁ c c c x = 1
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOf_isMulCommutative : ∀ {G : Type u_1} [inst : Group G] (K H : Subgroup G) [IsMulCommutative ↥H], IsMulCommutative ↥(H.subgroupOf K)
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Presheaf.classifier_χ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {U X : CategoryTheory.Functor Cᵒᵖ (Type (max u v))} (m : U ⟶ X)
  (x : CategoryTheory.Mono m), (CategoryTheory.Presheaf.classifier C).χ m = CategoryTheory.Presheaf.χ m
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedMap_one`. -/
LinearOrderedField.inducedMap_one : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α],
  ConditionallyCompleteLinearOrderedField.inducedMap α β 1 = 1
-- Init.Data.String.Iterator
/-- Checks whether the iterator is at or before the string's last character.
 -/
String.Legacy.Iterator.hasNext : String.Legacy.Iterator → Bool
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.updateFap! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu → Lean.Name → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Data.Finset.Card
Finset.card_erase_add_one : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], a ∈ s → (s.erase a).card + 1 = s.card
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.isNormal' : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] (self : OpenNormalSubgroup G),
  (↑self.toOpenSubgroup).Normal
-- Mathlib.Data.Nat.Digits.Defs
Nat.nat_repr_len_aux : ∀ (n b e : ℕ), 0 < b → n < b ^ e.succ → n / b < b ^ e
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The right diagonal datum `(H₂, Δ, H₂)`. Not an instance, since `H₁` cannot be inferred.  -/
IsHeckeTriple.diag_right : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} [IsHeckeTriple Δ H₁ H₂], IsHeckeTriple Δ H₂ H₂
-- Mathlib.Tactic.Translate.Reorder
/-- A permutation, represented using cycle notation.  -/
Mathlib.Tactic.Translate.Permutation : Type
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instAddQuotient : {S : Type u_2} →
  (M : Type u_3) → [inst : SMul S M] → [inst_1 : Add M] → (c : ModuleCon S M) → Add (ModuleCon.Quotient M c)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.kernelSequence_X₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShortComplex.kernelSequence f).X₃ = Y
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_eq_subst'_cert.eq_1 : ∀ (a b : ℤ) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_eq_subst'_cert a b p₁ p₂ p₃ = p₃.beq' (Int.Internal.Linear.Poly.combine_mul_k b (-a) p₁ p₂)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_finCongr_Iio : ∀ {n m : ℕ} (h : n = m) (i : Fin n), Finset.map (finCongr h).toEmbedding (Finset.Iio i) = Finset.Iio (Fin.cast h i)
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- If `ringChar F = 2`, then `quadraticChar F` takes the value `1` on nonzero elements.  -/
quadraticChar_eq_one_of_char_two : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F = 2 → ∀ {a : F}, a ≠ 0 → (quadraticChar F) a = 1
-- Mathlib.Data.Set.Image
/-- We make this the simp lemma instead of `range_coe`. The reason is that if we write
for `s : Set α` the function `(↑) : s → α`, then the inferred implicit arguments of `(↑)` are
`↑α (fun x ↦ x ∈ s)`.  -/
Subtype.range_coe_subtype : ∀ {α : Type u_1} {p : α → Prop}, Set.range Subtype.val = {x | p x}
-- Lean.Parser.Syntax
/-- Parses the literal symbol.

The symbol is automatically included in the set of reserved tokens ("keywords").
Keywords cannot be used as identifiers, unless the identifier is otherwise escaped.
For example, `"fun"` reserves `fun` as a keyword; to refer an identifier named `fun` one can write `«fun»`.
Adding a `&` prefix prevents it from being reserved, for example `&"true"`.

Whitespace before or after the atom is used as a pretty printing hint.
For example, `" + "` parses `+` and pretty prints it with whitespace on both sides.
The whitespace has no effect on parsing behavior.
 -/
Lean.Parser.Syntax.atom : Lean.Parser.Parser
-- Mathlib.Probability.Kernel.Disintegration.Integral
ProbabilityTheory.setLIntegral_condKernel_univ_left : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {κ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] {f : β × Ω → ENNReal},
  Measurable f →
    ∀ (a : α) {t : Set Ω},
      MeasurableSet t →
        ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : SeminormedAddGroup E]
  {ι : Type u_3} [Nonempty ι] [inst_2 : LinearOrder ι] {f : ι → α → E} {p : ℝ} {f_lim : α → E},
  (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) →
    MeasureTheory.eLpNorm' f_lim p μ = (∫⁻ (a : α), Filter.liminf (fun x => ‖f x a‖ₑ ^ p) Filter.atTop ∂μ) ^ (1 / p)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.MonObj A] → CategoryTheory.Category.{v₂, max u₂ v₂} (CategoryTheory.Mod D A)
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
/-- The spectral radius of a self-adjoint operator on a complete space equals the norm.  -/
ContinuousLinearMap.spectralRadius_eq_nnnorm : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) [inst_3 : CompleteSpace E], IsSelfAdjoint T → spectralRadius 𝕜 T = ↑‖T‖₊
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.partialMatch_prefixFunction_sub_one : ∀ {pat : ByteArray} {stackPos : ℕ} {hst : stackPos - 1 < pat.size},
  0 < stackPos →
    String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat
      (String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat (stackPos - 1) hst) stackPos
-- Mathlib.CategoryTheory.Category.ULift
/-- `ULiftHom.{w} C` is an alias for `C`, which is endowed with a category instance
whose morphisms are obtained by applying `ULift.{w}` to the morphisms from `C`.
 -/
CategoryTheory.ULiftHom : Type u → Type u
-- Init.Data.String.Slice
/-- Checks whether the slice can be interpreted as the decimal representation of an integer.

A slice can be interpreted as a decimal integer if it only consists of at least one decimal digit
and optionally `-` in front. Leading `+` characters are not allowed.

Use `String.Slice.toInt?` or `String.toInt!` to convert such a string to an integer.

Examples:

* `"".toSlice.isInt = false`

* `"-".toSlice.isInt = false`

* `"0".toSlice.isInt = true`

* `"-0".toSlice.isInt = true`

* `"5".toSlice.isInt = true`

* `"587".toSlice.isInt = true`

* `"-587".toSlice.isInt = true`

* `"+587".toSlice.isInt = false`

* `" 5".toSlice.isInt = false`

* `"2-3".toSlice.isInt = false`

* `"0xff".toSlice.isInt = false`

* `"-0_1".toSlice.isInt = true`

* `"-_1".toSlice.isInt = false`
 -/
String.Slice.isInt : String.Slice → Bool
-- Lean.Environment
Lean.instNonemptyEnvExtensionEntry : Nonempty Lean.EnvExtensionEntry
-- Init.Data.Int.Linear
Int.Internal.Linear.le_of_le_diseq_cert.eq_1 : ∀ (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.le_of_le_diseq_cert p₁ p₂ p₃ =
    (p₂.beq' p₁ || p₂.beq' (p₁.mul_k (-1))).and' (p₃.beq' (p₁.addConst_k 1))
-- Mathlib.GroupTheory.GroupAction.Iwasawa
/-- The conjugacy property of the subgroups  -/
MulAction.IwasawaStructure.is_conj : ∀ {M : Type u_1} [inst : Group M] {α : Type u_2} [inst_1 : MulAction M α] (self : MulAction.IwasawaStructure M α)
  (g : M) (x : α), self.T (g • x) = MulAut.conj g • self.T x
-- Mathlib.Order.BoundedOrder.Basic
eq_bot_of_bot_eq_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ⊥ = ⊤ → ∀ (x : α), x = ⊥
-- Lean.Parser.Basic
Lean.Parser.instReprRecoveryContext.repr : Lean.Parser.RecoveryContext → ℕ → Std.Format
-- Mathlib.RingTheory.Trace.Quotient
_private.Mathlib.RingTheory.Trace.Quotient.0.termP : Lean.ParserDescr
-- Lean.Meta.Constructions.SparseCasesOn
Lean.Meta.SparseCasesOnInfo.majorPos : Lean.Meta.SparseCasesOnInfo → ℕ
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedResponse : {a : Type u_1} → [Inhabited a] → Inhabited (Lean.JsonRpc.Response a)
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.mk.inj : ∀ {D : Type u_1} {Q : Type u_2} {left : Q → D} {right : Q} {left_1 : Q → D} {right_1 : Q},
  { left := left, right := right } = { left := left_1, right := right_1 } → left = left_1 ∧ right = right_1
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasProjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X)
  (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    ∀ {Z : HomotopyCategory C (ComplexShape.down ℕ)} (h : (CategoryTheory.projectiveResolutions C).obj Y ⟶ Z),
      CategoryTheory.CategoryStruct.comp P.iso.inv
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.projectiveResolutions C).map f) h) =
        CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ)
          (CategoryTheory.CategoryStruct.comp Q.iso.inv h)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- A monoid object as a module over itself.  -/
CategoryTheory.Mod.regular : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (A : C) → [inst_2 : CategoryTheory.MonObj A] → CategoryTheory.Mod C A
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.injectiveₛ : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S], (∀ m ∈ M, IsRegular m) → Function.Injective ⇑(algebraMap R S)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_map_fst : ∀ {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) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  {x y : X} (f : x ⟶ y),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).map f).fst =
    S.fst.map f
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsProperLinearSet.isProperSemilinearSet : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, IsProperLinearSet s → IsProperSemilinearSet s
-- Mathlib.Order.Minimal
/-- **Alias** of `OrderEmbedding.maximal_apply_mem_iff`. -/
OrderEmbedding.maximal_apply_iff : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {f : α ↪o β} {t : Set β},
  t ⊆ Set.range ⇑f → (Maximal (fun x => x ∈ t) (f x) ↔ Maximal (fun x => f x ∈ t) x)
-- Mathlib.Geometry.Euclidean.Altitude
/-- An altitude is one-dimensional (i.e., a line).  -/
Affine.Simplex.finrank_direction_altitude : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  Module.finrank ℝ ↥(s.altitude i).direction = 1
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- The map `ZSpan.fractRestrict` defines an equiv map between `E ⧸ span ℤ (Set.range b)`
and `ZSpan.fundamentalDomain b`.  -/
ZSpan.quotientEquiv : {E : Type u_1} →
  {ι : Type u_2} →
    {K : Type u_3} →
      [inst : NormedField K] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace K E] →
            (b : Module.Basis ι K E) →
              [inst_3 : LinearOrder K] →
                [IsStrictOrderedRing K] →
                  [FloorRing K] → [Fintype ι] → E ⧸ Submodule.span ℤ (Set.range ⇑b) ≃ ↑(ZSpan.fundamentalDomain b)
-- Mathlib.Topology.Constructions
tendsto_pi_nhds : ∀ {Y : Type v} {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {f : Y → (i : ι) → A i}
  {g : (i : ι) → A i} {u : Filter Y},
  Filter.Tendsto f u (nhds g) ↔ ∀ (x : ι), Filter.Tendsto (fun i => f i x) u (nhds (g x))
-- Mathlib.Topology.Sheaves.Sheafify
/-- The isomorphism between a stalk of the sheafification and the original stalk.
 -/
TopCat.Presheaf.sheafifyStalkIso : {X : TopCat} → (F : TopCat.Presheaf (Type v) X) → (x : ↑X) → F.sheafify.presheaf.stalk x ≅ F.stalk x
-- Mathlib.Topology.Homotopy.HSpaces
IsTopologicalGroup.one_eq_hSpace_e : ∀ {G : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G], 1 = HSpace.e
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.bayesRisk_compProd_le_bayesRisk : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u_3} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓧' : MeasurableSpace 𝓧'} {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧)
  [ProbabilityTheory.IsSFiniteKernel P] (π : MeasureTheory.Measure Θ) (η : ProbabilityTheory.Kernel (Θ × 𝓧) 𝓧')
  [ProbabilityTheory.IsMarkovKernel η],
  ProbabilityTheory.bayesRisk ℓ (P.compProd η) π ≤ ProbabilityTheory.bayesRisk ℓ P π
-- Init.Data.Int.Order
Int.mul_nonpos_of_nonneg_of_nonpos : ∀ {a b : ℤ}, 0 ≤ a → b ≤ 0 → a * b ≤ 0
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.nullHomotopic_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0)
  (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ = h₀ + CategoryTheory.CategoryStruct.comp S₁.f h₁
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.denom_one : ∀ {K : Type u} [inst : Field K], RatFunc.denom 1 = 1
-- Mathlib.Algebra.Group.Subgroup.Finite
AddMonoidHom.fintypeRange.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_3} [inst_1 : AddGroup N] [inst_2 : Fintype G] [inst_3 : DecidableEq N]
  (f : G →+ N), f.fintypeRange = Set.fintypeRange ⇑f
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.coeff_frobenius : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x : WittVector p R) (n : ℕ),
  (WittVector.frobenius x).coeff n = (MvPolynomial.aeval x.coeff) (WittVector.frobeniusPoly p n)
-- Lean.Message
Lean.MessageData.brecOn.go : {motive_1 : Lean.MessageData → Sort u} →
  {motive_2 : Array Lean.MessageData → Sort u} →
    {motive_3 : List Lean.MessageData → Sort u} →
      (t : Lean.MessageData) →
        ((t : Lean.MessageData) → t.below → motive_1 t) →
          ((t : Array Lean.MessageData) → Lean.MessageData.below_1 t → motive_2 t) →
            ((t : List Lean.MessageData) → Lean.MessageData.below_2 t → motive_3 t) → motive_1 t ×' t.below
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.mem_neLocus : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → Zero (N a)] {f g : Π₀ (a : α), N a} {a : α}, a ∈ f.neLocus g ↔ f a ≠ g a
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.intMaxSealed_def : ∀ {n : ℕ}, BitVec.Signed.intMaxSealed✝ n = ↑(2 ^ (n - 1) - 1)
-- Mathlib.Data.Multiset.Fold
Multiset.fold_eq_foldl : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b : α) (s : Multiset α),
  Multiset.fold op b s = Multiset.foldl op b s
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Cylinders are closed when `A` is a T1 Space.  -/
SymbolicDynamics.FullShift.isClosed_cylinder : ∀ {A : Type u_1} {G : Type u_2} [inst : TopologicalSpace A] [T1Space A] (U : Finset G) (x : G → A),
  IsClosed (SymbolicDynamics.FullShift.cylinder U x)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.mk.inj : ∀ {M : Type u_1} {inst : Add M} {toSetoid : Setoid M}
  {add' : ∀ {w x y z : M}, toSetoid w x → toSetoid y z → toSetoid (w + y) (x + z)} {toSetoid_1 : Setoid M}
  {add'_1 : ∀ {w x y z : M}, toSetoid_1 w x → toSetoid_1 y z → toSetoid_1 (w + y) (x + z)},
  { toSetoid := toSetoid, add' := add' } = { toSetoid := toSetoid_1, add' := add'_1 } → toSetoid = toSetoid_1
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.InfoCacheKey.mk.injEq : ∀ (configKey : UInt64) (expr : Lean.Expr) (nargs? : Option ℕ) (configKey_1 : UInt64) (expr_1 : Lean.Expr)
  (nargs?_1 : Option ℕ),
  ({ configKey := configKey, expr := expr, nargs? := nargs? } =
      { configKey := configKey_1, expr := expr_1, nargs? := nargs?_1 }) =
    (configKey = configKey_1 ∧ expr = expr_1 ∧ nargs? = nargs?_1)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.int_cyclotomic_spec : ∀ (n : ℕ),
  Polynomial.map (Int.castRingHom ℂ) (Polynomial.cyclotomic n ℤ) = Polynomial.cyclotomic' n ℂ ∧
    (Polynomial.cyclotomic n ℤ).degree = (Polynomial.cyclotomic' n ℂ).degree ∧ (Polynomial.cyclotomic n ℤ).Monic
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.sameCycle_inv`. -/
Equiv.Perm.SameCycle.inv : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → f⁻¹.SameCycle x y
-- Mathlib.Topology.LocallyFinsupp
/-- A function with locally finite support is a function with locally finite support within
`⊤ : Set X`.
 -/
Function.locallyFinsupp : (X : Type u_1) → [TopologicalSpace X] → (Y : Type u_2) → [Zero Y] → Type (max u_1 u_2)
-- Mathlib.Order.Minimal
/-- If `P` is down-closed, then minimal elements satisfying `P` are exactly the globally minimal
elements satisfying `P`.  -/
minimal_iff_isMin : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α], (∀ ⦃x y : α⦄, P y → x ≤ y → P x) → (Minimal P x ↔ P x ∧ IsMin x)