mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapₗ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (ε : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
  (X : C),
  (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapₗ ε).app X =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight ε (F.obj X)
-- Mathlib.Order.Basic
not_lt_iff_not_le_or_ge : ∀ {α : Type u_2} [inst : Preorder α] {a b : α}, ¬a < b ↔ ¬a ≤ b ∨ b ≤ a
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- The functor `M ↦ R[M]`, from the category of magmas to the category of non-unital,
non-associative algebras over `R` is adjoint to the forgetful functor in the other direction.  -/
MonoidAlgebra.liftMagma : (R : Type u_1) →
  {A : Type u_4} →
    {M : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : Mul M] →
          [inst_2 : NonUnitalNonAssocSemiring A] →
            [inst_3 : Module R A] →
              [IsScalarTower R A A] → [SMulCommClass R A A] → (M →ₙ* A) ≃ (MonoidAlgebra R M →ₙₐ[R] A)
-- Mathlib.Order.WellFoundedSet
Set.wellFoundedOn_insert : ∀ {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α} {a : α},
  (insert a s).WellFoundedOn r ↔ s.WellFoundedOn r
-- Lean.Data.PrefixTree
/-- Similar to trie, but for arbitrary keys  -/
Lean.PrefixTreeNode : (α : Type u) → Type v → (α → α → Ordering) → Type (max u v)
-- Mathlib.FieldTheory.KummerPolynomial
root_X_pow_sub_C_ne_zero_iff : ∀ {K : Type u} [inst : Field K] {n : ℕ} {a : K},
  Irreducible (Polynomial.X ^ n - Polynomial.C a) → (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ≠ 0 ↔ a ≠ 0)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextDocumentRegistrationOptions : Lean.FromJson Lean.Lsp.TextDocumentRegistrationOptions
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `Left.inv_le_one_iff`.

---

Uses `left` co(ntra)variant.  -/
inv_le_one' : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a : α}, a⁻¹ ≤ 1 ↔ 1 ≤ a
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddSemigroupOfAddHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → AddSemigroup (G i)] →
                  [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] → AddSemigroup (DirectLimit G f)
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.snd_mem_orbit_of_mem_orbit : ∀ {M : Type u} [inst : AddMonoid M] {α : Type v} [inst_1 : AddAction M α] {β : Type u_1} [inst_2 : AddAction M β]
  {x y : α × β}, x ∈ AddAction.orbit M y → x.2 ∈ AddAction.orbit M y.2
-- Mathlib.ModelTheory.Basic
/-- A homomorphism between first-order structures is a function that commutes with the
interpretations of functions and maps tuples in one structure where a given relation is true to
tuples in the second structure where that relation is still true.  -/
FirstOrder.«term_→[_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.faithful_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  (CategoryTheory.MonoOver.map f).Faithful
-- Lean.Elab.Term.TermElabM
/-- Use tactic to synthesize value for metavariable.

If `delayOnMVars` is true, the tactic will not be executed until the goal is free of unassigned
expr metavariables.
 -/
Lean.Elab.Term.SyntheticMVarKind.tactic : Lean.Syntax →
  Lean.Elab.Term.SavedContext → Lean.Elab.Term.TacticMVarKind → optParam Bool false → Lean.Elab.Term.SyntheticMVarKind
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.CliqueFree.mem_of_sup_edge_isNClique : ∀ {α : Type u_1} {G : SimpleGraph α} {x y : α} {t : Finset α} {n : ℕ},
  G.CliqueFree n → (G ⊔ SimpleGraph.edge x y).IsNClique n t → x ∈ t
-- Mathlib.CategoryTheory.Galois.Basic
/-- If `F` is a fiber functor and `E` is an equivalence between categories of finite types,
then `F ⋙ E` is again a fiber functor.  -/
CategoryTheory.PreGaloisCategory.FiberFunctor.comp_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (E : CategoryTheory.Functor FintypeCat FintypeCat) [E.IsEquivalence],
  CategoryTheory.PreGaloisCategory.FiberFunctor (F.comp E)
-- Init.Data.Rat.Lemmas
Rat.ofScientific_def : ∀ {m : ℕ} {s : Bool} {e : ℕ}, Rat.ofScientific m s e = if s = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- Any continuous ring homomorphism commutes with `NormedSpace.exp`.  -/
NormedSpace.map_exp_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} {𝔹 : Type u_3} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedRing 𝔹] [inst_3 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [Algebra 𝕂 𝔹] [CharZero 𝕂] {F : Type u_4}
  [inst_7 : FunLike F 𝔸 𝔹] [RingHomClass F 𝔸 𝔹] (f : F),
  Continuous ⇑f → ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius, f (NormedSpace.exp x) = NormedSpace.exp (f x)
-- Mathlib.Analysis.SumIntegralComparisons
AntitoneOn.integral_le_sum : ∀ {x₀ : ℝ} {a : ℕ} {f : ℝ → ℝ},
  AntitoneOn f (Set.Icc x₀ (x₀ + ↑a)) → ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i ∈ Finset.range a, f (x₀ + ↑i)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon C),
  ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso C).inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.zsmul_left : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → ∀ (m : ℤ), AddCommute (m • a) b
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.openCoverDomain.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.RationalMap Y),
  f.openCoverDomain =
    { I₀ := ↑{x | ∃ g, ∃ (_ : g.toRationalMap = f), g.domain = x}, X := fun U => ↑↑U, f := fun U => X.homOfLE ⋯,
      mem₀ := ⋯ }
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Returns the continuants `⟨Aₙ, Bₙ⟩` of `g`.  -/
GenContFract.conts : {K : Type u_2} → [DivisionRing K] → GenContFract K → Stream' (GenContFract.Pair K)
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
ruzsaSzemerediNumberNat_le : ∀ {n : ℕ}, ruzsaSzemerediNumberNat n ≤ n.choose 3
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instVAdd : {M : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] → [inst_1 : VAdd M X] → [ContinuousConstVAdd M X] → VAdd M (SeparationQuotient X)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.two_mul_T_eq_U_sub_U : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  2 * Polynomial.Chebyshev.T R (n + 2) = Polynomial.Chebyshev.U R (n + 2) - Polynomial.Chebyshev.U R n
-- Mathlib.NumberTheory.Multiplicity
Nat.emultiplicity_pow_sub_pow : ∀ {p : ℕ},
  Nat.Prime p →
    Odd p →
      ∀ {x y : ℕ},
        p ∣ x - y → ¬p ∣ x → ∀ (n : ℕ), emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
-- Mathlib.Data.Finset.Image
Finset.map_sdiff : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α),
  Finset.map f (s₁ \ s₂) = Finset.map f s₁ \ Finset.map f s₂
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.Regular.inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [ContinuousInv G] [μ.Regular], μ.inv.Regular
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_eq_ltensor : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] (f : M →ₗ[R] N), ⇑(LinearMap.baseChange A f) = ⇑(LinearMap.lTensor A f)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- An additive action is `2`-pretransitive iff
it can move any two distinct elements to any two distinct elements.  -/
AddAction.is_two_pretransitive_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α],
  AddAction.IsMultiplyPretransitive G α 2 ↔ ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g +ᵥ a = c ∧ g +ᵥ b = d
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
/-- Variant of `Module.rankAtStalk_eq` for better rewriting.  -/
Ideal.finrank_fiber_eq_rankAtStalk : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M] (p : Ideal R) [hp : p.IsPrime],
  Module.finrank p.ResidueField (p.Fiber M) = Module.rankAtStalk M { asIdeal := p, isPrime := hp }
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.fst_ne_snd : ∀ {V : Type u_1} {G : SimpleGraph V} (d : G.Dart), d.toProd.1 ≠ d.toProd.2
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.idealFactorsEquivOfQuotEquiv_is_dvd_iso`. -/
idealFactorsEquivOfQuotEquiv_is_dvd_iso : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} [inst_3 : IsDedekindDomain R] (f : R ⧸ I ≃+* A ⧸ J) {L M : Ideal R} (hL : L ∣ I) (hM : M ∣ I),
  ↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ∣
      ↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ↔
    L ∣ M
-- Mathlib.Combinatorics.Colex
/-- The initial segment of the colexicographic order on sets with `#s` elements and ending at
`s`.  -/
Finset.Colex.initSeg : {α : Type u_1} → [LinearOrder α] → [Fintype α] → Finset α → Finset (Finset α)
-- Init.TacticsExtra
/-- Normalize casts in the goal and the given expression, then `apply` the expression to the goal.
 -/
Lean.Parser.Tactic.tacticApply_mod_cast_ : Lean.ParserDescr
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_ofIntLE : ∀ {n : ℤ} (h₁ : Int64.minValue.toInt ≤ n) (h₂ : n ≤ Int64.maxValue.toInt),
  (Int64.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.instIsLocalizedFullyFaithfulOppositeOpOp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.IsLocalizedFullyFaithful],
  Φ.op.IsLocalizedFullyFaithful
-- Init.Data.SInt.Bitwise
Int32.ofBitVec_not : ∀ (a : BitVec 32), Int32.ofBitVec (~~~a) = ~~~Int32.ofBitVec a
-- Mathlib.Topology.Bornology.Constructions
instBornologyOrderDual : {α : Type u_1} → [Bornology α] → Bornology αᵒᵈ
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- A category that has larger colimits also has smaller colimits.  -/
CategoryTheory.Limits.hasColimitsOfSizeOfUnivLE : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [UnivLE.{v₂, v₁}] [UnivLE.{u₂, u₁}]
  [CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C], CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v, u} C
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- The embedding `v.Completion →+* ℂ` is an isometry.  -/
NumberField.InfinitePlace.Completion.isometry_extensionEmbedding : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K),
  Isometry ⇑(NumberField.InfinitePlace.Completion.extensionEmbedding v)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- An action of a group on a type `α` is `n`-pretransitive
if the associated action on `Fin n ↪ α` is pretransitive.  -/
MulAction.IsMultiplyPretransitive : (G : Type u_1) → (α : Type u_2) → [inst : Group G] → [MulAction G α] → ℕ → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.hom_ext : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f g : Z ⟶ X ⊞ Y),
  CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst =
      CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.fst →
    CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd =
        CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.snd →
      f = g
-- Plausible.Testable
Plausible.Configuration.numRetries : Plausible.Configuration → ℕ
-- Batteries.Data.String.Lemmas
String.Pos.Raw.valid_rawEndPos : ∀ {s : String}, String.Pos.Raw.Valid s s.rawEndPos
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_vadd : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : VAdd M G] (n : M) (f : α → G), ↑(n +ᵥ f) = n +ᵥ ↑f
-- Mathlib.Order.SuccPred.Basic
SuccOrder.ofOrderIso.eq_1 : ∀ {X : Type u_3} {Y : Type u_4} [inst : Preorder X] [inst_1 : Preorder Y] [inst_2 : SuccOrder X] (f : X ≃o Y),
  SuccOrder.ofOrderIso f =
    { succ := fun y => f (SuccOrder.succ (f.symm y)), le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfOrdArgs.mk.injEq : ∀ {α : Type u} (toLinearPreorderOfOrdArgs : Std.Packages.LinearPreorderOfOrdArgs α)
  (eq_of_compare :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      let this_1 := toLinearPreorderOfOrdArgs.le;
      ∀ (a b : α), compare a b = Ordering.eq → a = b)
      Std.Packages.LinearOrderOfOrdArgs.eq_of_compare._autoParam)
  (min :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      Min α)
      Std.Packages.LinearOrderOfOrdArgs.min._autoParam)
  (max :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      Max α)
      Std.Packages.LinearOrderOfOrdArgs.max._autoParam)
  (min_eq :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      let this_1 := toLinearPreorderOfOrdArgs.le;
      let this_2 := min;
      have this_3 := ⋯;
      ∀ (a b : α), a ⊓ b = if (compare a b).isLE = true then a else b)
      Std.Packages.LinearOrderOfOrdArgs.min_eq._autoParam)
  (max_eq :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      let this_1 := toLinearPreorderOfOrdArgs.le;
      let this_2 := max;
      have this_3 := ⋯;
      ∀ (a b : α), a ⊔ b = if (compare a b).isGE = true then a else b)
      Std.Packages.LinearOrderOfOrdArgs.max_eq._autoParam)
  (toLinearPreorderOfOrdArgs_1 : Std.Packages.LinearPreorderOfOrdArgs α)
  (eq_of_compare_1 :
    autoParam
      (let this := toLinearPreorderOfOrdArgs_1.ord;
      let this_1 := toLinearPreorderOfOrdArgs_1.le;
      ∀ (a b : α), compare a b = Ordering.eq → a = b)
      Std.Packages.LinearOrderOfOrdArgs.eq_of_compare._autoParam)
  (min_1 :
    autoParam
      (let this := toLinearPreorderOfOrdArgs_1.ord;
      Min α)
      Std.Packages.LinearOrderOfOrdArgs.min._autoParam)
  (max_1 :
    autoParam
      (let this := toLinearPreorderOfOrdArgs_1.ord;
      Max α)
      Std.Packages.LinearOrderOfOrdArgs.max._autoParam)
  (min_eq_1 :
    autoParam
      (let this := toLinearPreorderOfOrdArgs_1.ord;
      let this_1 := toLinearPreorderOfOrdArgs_1.le;
      let this_2 := min_1;
      have this_3 := ⋯;
      ∀ (a b : α), a ⊓ b = if (compare a b).isLE = true then a else b)
      Std.Packages.LinearOrderOfOrdArgs.min_eq._autoParam)
  (max_eq_1 :
    autoParam
      (let this := toLinearPreorderOfOrdArgs_1.ord;
      let this_1 := toLinearPreorderOfOrdArgs_1.le;
      let this_2 := max_1;
      have this_3 := ⋯;
      ∀ (a b : α), a ⊔ b = if (compare a b).isGE = true then a else b)
      Std.Packages.LinearOrderOfOrdArgs.max_eq._autoParam),
  ({ toLinearPreorderOfOrdArgs := toLinearPreorderOfOrdArgs, eq_of_compare := eq_of_compare, min := min, max := max,
        min_eq := min_eq, max_eq := max_eq } =
      { toLinearPreorderOfOrdArgs := toLinearPreorderOfOrdArgs_1, eq_of_compare := eq_of_compare_1, min := min_1,
        max := max_1, min_eq := min_eq_1, max_eq := max_eq_1 }) =
    (toLinearPreorderOfOrdArgs = toLinearPreorderOfOrdArgs_1 ∧ min = min_1 ∧ max = max_1)
-- Mathlib.Data.Set.MulAntidiagonal
Set.swap_mem_antidiagonal : ∀ {α : Type u_1} [inst : AddCommMagma α] {s t : Set α} {a : α} {x : α × α},
  x.swap ∈ s.antidiagonal t a ↔ x ∈ t.antidiagonal s a
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.isOrderedAddMonoid : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddCommGroup (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedAddMonoid (α i)],
  IsOrderedAddMonoid (Lex (Π₀ (i : ι), α i))
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `intCast_apply`. -/
ContinuousLinearMap.intCast_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : IntCast F} {inst_2 : SMul ℤ α}
  [self : IsIntCastApply F α] (n : ℤ) (x : α), ↑n x = n • x
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instEmptyCollection : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → EmptyCollection (Std.DTreeMap.Raw α β cmp)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The action by a subsemiring is the action by the underlying semiring.  -/
Subsemiring.instMulSemiringActionSubtypeMem : {R' : Type u_1} →
  {α : Type u_2} →
    [inst : Semiring R'] →
      [inst_1 : Semiring α] → [MulSemiringAction R' α] → (S : Subsemiring R') → MulSemiringAction (↥S) α
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.antilipschitz : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [IsometryClass F α β] (f : F), AntilipschitzWith 1 ⇑f
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearEquiv.congrQuadraticMap_symm : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid P]
  [inst_6 : Module R P] (e : N ≃ₗ[R] P), e.congrQuadraticMap.symm = e.symm.congrQuadraticMap
-- Mathlib.Probability.Independence.InfinitePi
/-- Random variables are independent iff their joint distribution is the product measure. This
is a version where the random variable `ω ↦ (Xᵢ(ω))ᵢ` is almost everywhere measurable.
See `iIndepFun_iff_map_fun_eq_infinitePi_map₀'` for a version which only assumes that
each `Xᵢ` is almost everywhere measurable and that `ι` is countable.  -/
ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀ : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : ι → Type u_3}
  {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} [MeasureTheory.IsProbabilityMeasure P],
  AEMeasurable (fun ω i => X i ω) P →
    (ProbabilityTheory.iIndepFun X P ↔
      MeasureTheory.Measure.map (fun ω i => X i ω) P =
        MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.map (X i) P)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instIsNegApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}, IsNegApply (SlashInvariantForm Γ k) UpperHalfPlane ℂ
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Cylinder.LeftHomotopy.leftHomotopyRel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {X Y : C} {f g : X ⟶ Y} {P : HomotopicalAlgebra.Cylinder X} (h : P.LeftHomotopy f g),
  HomotopicalAlgebra.LeftHomotopyRel f g
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valued.toNormedField.setOfPred_mem_integer_eq_closedBall : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne], {x | x ∈ Valued.v.integer} = Metric.closedBall 0 1
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- Given a subgroups basis, the basis elements as open additive subgroups in the associated
topology.  -/
RingSubgroupsBasis.openAddSubgroup : {A : Type u_1} →
  {ι : Type u_2} →
    [inst : Ring A] →
      [inst_1 : Nonempty ι] → {B : ι → AddSubgroup A} → (hB : RingSubgroupsBasis B) → ι → OpenAddSubgroup A
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.homMk_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (f : K.toGradedObject ⟶ L.toGradedObject)
  (comm₁ :
    ∀ (i₁ i₁' : I₁) (i₂ : I₂),
      c₁.Rel i₁ i₁' →
        CategoryTheory.CategoryStruct.comp (f (i₁, i₂)) ((L.d i₁ i₁').f i₂) =
          CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (f (i₁', i₂)))
  (comm₂ :
    ∀ (i₁ : I₁) (i₂ i₂' : I₂),
      c₂.Rel i₂ i₂' →
        CategoryTheory.CategoryStruct.comp (f (i₁, i₂)) ((L.X i₁).d i₂ i₂') =
          CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (f (i₁, i₂')))
  (i₁ : I₁) (i₂ : I₂), ((HomologicalComplex₂.homMk f comm₁ comm₂).f i₁).f i₂ = f (i₁, i₂)
-- Mathlib.Algebra.Homology.Refinements
HomologicalComplex.comp_homologyπ_eq_iff_up_to_refinements : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι),
  c.prev j = i →
    ∀ {A : C} (z₂ z₂' : A ⟶ K.cycles j),
      CategoryTheory.CategoryStruct.comp z₂ (K.homologyπ j) = CategoryTheory.CategoryStruct.comp z₂' (K.homologyπ j) ↔
        ∃ A' π,
          ∃ (_ : CategoryTheory.Epi π),
            ∃ x₁,
              CategoryTheory.CategoryStruct.comp π z₂ =
                CategoryTheory.CategoryStruct.comp π z₂' + CategoryTheory.CategoryStruct.comp x₁ (K.toCycles i j)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
min_le_of_add_le_two_nsmul : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b c : M},
  a + b ≤ 2 • c → min a b ≤ c
-- Mathlib.NumberTheory.Bernoulli
bernoulli_eq_bernoulli'_of_ne_one : ∀ {n : ℕ}, n ≠ 1 → bernoulli n = bernoulli' n
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.supDegree_esymm : ∀ {R : Type u_3} {n m : ℕ} [inst : CommSemiring R] {i : Fin n} [Nontrivial R],
  ↑i < m →
    ⇑(ofLex (AddMonoidAlgebra.supDegree (⇑toLex) (MvPolynomial.esymm (Fin m) R (↑i + 1)))) =
      (Fin.accumulate n m) ⇑fun₀ | i => 1
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
FDerivMeasurableAux.le_of_mem_A : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {r ε : ℝ} {L : E →L[𝕜] F} {x : E},
  x ∈ FDerivMeasurableAux.A f L r ε →
    ∀ {y z : E}, y ∈ Metric.closedBall x (r / 2) → z ∈ Metric.closedBall x (r / 2) → ‖f z - f y - L (z - y)‖ ≤ ε * r
-- Mathlib.Algebra.Category.Grp.EpiMono
/-- Let `τ` be the permutation on `X'` exchanging `f.hom.range` and the point at infinity.
 -/
GrpCat.SurjectiveOfEpiAuxs.tau : {A B : GrpCat} → (f : A ⟶ B) → Equiv.Perm (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity f)
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.toSpanSingleton_eq_zero_iff : ∀ (R : Type u_1) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M},
  LinearMap.toSpanSingleton R M x = 0 ↔ x = 0
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.Gamma_integrand_deriv_integrable_B : ∀ {s : ℂ},
  0 < s.re →
    ∀ {Y : ℝ}, 0 ≤ Y → IntervalIntegrable (fun x => ↑(Real.exp (-x)) * (s * ↑x ^ (s - 1))) MeasureTheory.volume 0 Y