mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Submodule
IsFractionRing.coeSubmodule_le_coeSubmodule : ∀ {R : Type u_3} {K : Type u_4} [inst : CommRing R] [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {I J : Ideal R}, IsLocalization.coeSubmodule K I ≤ IsLocalization.coeSubmodule K J ↔ I ≤ J
-- Mathlib.Order.Antichain
IsStrongAntichain.flip : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Symm r], IsStrongAntichain r s → IsStrongAntichain (flip r) s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.comment : Lean.Lsp.SemanticTokenType
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.isNormal_beth : Order.IsNormal Cardinal.beth
-- Batteries.Lean.EStateM
EStateM.run'_seqRight : ∀ {ε σ α β : Type u_1} (x : EStateM ε σ α) (y : EStateM ε σ β) (s : σ),
  (x *> y).run' s =
    match x.run s with
    | EStateM.Result.ok a s => y.run' s
    | EStateM.Result.error a a_1 => none
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
CategoryTheory.extendFan_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C}
  (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt),
  (CategoryTheory.extendFan c₁ c₂).pt = c₂.pt
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- The constant presheaf on `X` with value `Z`.  -/
AlgebraicGeometry.PresheafedSpace.const : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → TopCat → C → AlgebraicGeometry.PresheafedSpace C
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.congrLeftRingEquiv_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6}
  [inst_2 : Semiring Z] (e : X ≃ₜ Y) (g : LocallyConstant X Z) (a : Y),
  ((LocallyConstant.congrLeftRingEquiv e) g) a = g (e.symm a)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.isoMk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type u_1} (X Y : CategoryTheory.GradedObject β C)
  (e : (i : β) → X i ≅ Y i) (i : β), (X.isoMk Y e).hom i = (e i).hom
-- Init.Data.List.Nat.Range
List.count_range' : ∀ {a s n step : ℕ},
  autoParam (0 < step) List.count_range'._auto_1 →
    List.count a (List.range' s n step) = if ∃ i < n, a = s + step * i then 1 else 0
-- Std.Data.DHashMap.Internal.AssocList.Basic
_private.Std.Data.DHashMap.Internal.AssocList.Basic.0.Std.DHashMap.Internal.AssocList.map.go : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} →
      ((a : α) → β a → γ a) →
        Std.DHashMap.Internal.AssocList α γ → Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α γ
-- Mathlib.Algebra.Module.PUnit
/-- The one-element type acts trivially on every element.  -/
PUnit.smul_eq' : ∀ {R : Type u_1} (r : PUnit.{u_3 + 1}) (a : R), r • a = a
-- Mathlib.RingTheory.LittleWedderburn
_private.Mathlib.RingTheory.LittleWedderburn.0.LittleWedderburn.center_eq_top : ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D], Subring.center D = ⊤
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.add.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} [inst_1 : SizeOf J]
  (a a_1 : RingCat.Colimits.Prequotient F), sizeOf (a.add a_1) = 1 + sizeOf a + sizeOf a_1
-- Init.Data.Nat.ToString
Nat.c_eq_digitChar : ∀ {n : ℕ}, 'c' = n.digitChar ↔ n = 12
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_le_iff : ∀ {u : ℕ → EReal} {a : EReal}, LinearGrowth.linearGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ b * ↑n
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.card_smul_finset_le : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset β} {a : α}, (a • s).card ≤ s.card
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.comap_comap : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {N : Type u_2} [inst_2 : Group N]
  [inst_3 : TopologicalSpace N] {P : Type u_3} [inst_4 : Group P] [inst_5 : TopologicalSpace P] (K : OpenSubgroup P)
  (f₂ : N →* P) (hf₂ : Continuous ⇑f₂) (f₁ : G →* N) (hf₁ : Continuous ⇑f₁),
  OpenSubgroup.comap f₁ hf₁ (OpenSubgroup.comap f₂ hf₂ K) = OpenSubgroup.comap (f₂.comp f₁) ⋯ K
-- Mathlib.Data.Fintype.Defs
Fintype.decidableForallFintype : {α : Type u_1} → {p : α → Prop} → [DecidablePred p] → [Fintype α] → Decidable (∀ (a : α), p a)
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCardAux_zero : ∀ {α : Type u_1} (l : List α), Multiset.powersetCardAux 0 l = [0]
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
AffineBasis.toMatrix_self : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) [inst_4 : DecidableEq ι], b.toMatrix ⇑b = 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.carrier_eq_coe : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : AffineSubspace k P), s.carrier = ↑s
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.instUnitizationNormedRing : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [IsScalarTower 𝕜 A A] → [SMulCommClass 𝕜 A A] → NormedRing (WithLp 1 (Unitization 𝕜 A))
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_uInt16ToBitVec : ∀ (n : UInt16), { toBitVec := BitVec.setWidth 8 n.toBitVec } = n.toUInt8
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `zero_apply`. -/
GroupSeminorm.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Std.Http.Protocol.H1
/-- Parses one response start-line in client mode and initializes
`reader.messageHead` for header parsing.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processSendingStartLine : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.sending →
  Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.sending
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {km : α}, t.maxKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Topology.Instances.ENat
ENat.tendsto_nhds_top_iff_natCast_lt : ∀ {α : Type u_1} {l : Filter α} {f : α → ℕ∞}, Filter.Tendsto f l (nhds ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a
-- Mathlib.Algebra.Ring.Equiv
/-- If two rings are isomorphic, and the second is a domain, then so is the first.  -/
MulEquiv.isDomain : ∀ {A : Type u_7} (B : Type u_8) [inst : Semiring A] [inst_1 : Semiring B] [IsDomain B] (e : A ≃* B), IsDomain A
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instLipschitzAdd : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : AddMonoid β]
  [inst_3 : LipschitzAdd β], LipschitzAdd (BoundedContinuousFunction α β)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hasZeroObject : CategoryTheory.Limits.HasZeroObject SemiNormedGrp
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_prod_iff : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {ι : Type u_4} {f : ι → Polynomial R} {s : Finset ι},
  (∀ i ∈ s, f i ≠ 0) → ((∏ x ∈ s, f x).Splits ↔ ∀ x ∈ s, (f x).Splits)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.iInf_toNonUnitalSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {ι : Sort u_1} (S : ι → NonUnitalStarSubalgebra R A),
  (⨅ i, S i).toNonUnitalSubalgebra = ⨅ i, (S i).toNonUnitalSubalgebra
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.fromLeftInv_one : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M), S.fromLeftInv 1 = 1
-- Init.Data.List.ToArray
List.size_toArrayAux : ∀ {α : Type u_1} {as : List α} {xs : Array α}, (as.toArrayAux xs).size = xs.size + as.length
-- Mathlib.Order.BooleanAlgebra.Defs
/-- `x ⇨ y` is equal to `y ⊔ xᶜ`  -/
BooleanAlgebra.himp_eq : ∀ {α : Type u} [self : BooleanAlgebra α] (x y : α), x ⇨ y = y ⊔ xᶜ
-- Init.Data.BitVec.Lemmas
BitVec.replicate_zero : ∀ {w : ℕ} {x : BitVec w}, BitVec.replicate 0 x = 0#0
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fundamentalDomain_pi_basisFun : ∀ {ι : Type u_2} [inst : Fintype ι], ZSpan.fundamentalDomain (Pi.basisFun ℝ ι) = Set.univ.pi fun x => Set.Ico 0 1
-- Mathlib.Analysis.Convex.BetweenList
List.sbtw_singleton : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ : P), List.Sbtw R [p₁]
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
measurable_coe_nnreal_ennreal : Measurable ENNReal.ofNNReal
-- Mathlib.Data.ENat.BigOperators
ENat.toNat_prod : ∀ {ι : Type u_2} {s : Finset ι} {f : ι → ℕ∞}, (∏ i ∈ s, f i).toNat = ∏ i ∈ s, (f i).toNat
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.empty_notMem : ∀ {α : Type u} {f : Ultrafilter α}, ∅ ∉ f
-- Mathlib.Data.Set.Image
Set.preimage_eq_preimage' : ∀ {α : Type u_1} {β : Type u_2} {s t : Set α} {f : β → α},
  s ⊆ Set.range f → t ⊆ Set.range f → (f ⁻¹' s = f ⁻¹' t ↔ s = t)
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.instCoeSortType : CoeSort NonemptyFinLinOrd (Type u_1)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerLeft_trans_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G H K : CategoryTheory.Functor D E} (α : G ≅ H) (β : H ≅ K) {Z : CategoryTheory.Functor C E} (h : F.comp K ≅ Z),
  F.isoWhiskerLeft (α ≪≫ β) ≪≫ h = F.isoWhiskerLeft α ≪≫ F.isoWhiskerLeft β ≪≫ h
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
/-- If `H' : D' ⥤ V` is a pointwise left Kan extension along `L : D ⥤ D'` at `(d : D')`
and if tensoring right with an object preserves colimits in `V`,
then `H' ⊠ K : D' × E ⥤ V` is a pointwise left Kan extension along `L × (𝟭 E)` at `(d, e)`
for every `e : E`.  -/
CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionAtExtensionUnitLeft : {V : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {D : Type u₂} →
        {D' : Type u₃} →
          {E : Type u₄} →
            [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} D'] →
                [inst_4 : CategoryTheory.Category.{v₄, u₄} E] →
                  {H : CategoryTheory.Functor D V} →
                    {L : CategoryTheory.Functor D D'} →
                      (H' : CategoryTheory.Functor D' V) →
                        (α : H ⟶ L.comp H') →
                          (K : CategoryTheory.Functor E V) →
                            (d : D') →
                              (CategoryTheory.Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d →
                                (e : E) →
                                  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow L d)
                                        (CategoryTheory.MonoidalCategory.tensorRight (K.obj e))] →
                                    (CategoryTheory.Functor.LeftExtension.mk
                                          (CategoryTheory.MonoidalCategory.externalProduct H' K)
                                          (CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft H' α
                                            K)).IsPointwiseLeftKanExtensionAt
                                      (d, e)
-- Std.Tactic.BVDecide.Syntax
Lean.Elab.Tactic.BVDecide.SolverMode.noConfusionType : Sort v✝ → Lean.Elab.Tactic.BVDecide.SolverMode → Lean.Elab.Tactic.BVDecide.SolverMode → Sort v✝
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instAddCommGroupHom : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] → [inst_1 : Ring k] → [inst_2 : Monoid G] → (A B : TopRep k G) → AddCommGroup (A ⟶ B)
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.eq_X_add_C_of_degree_eq_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.degree = 1 → p = Polynomial.C p.leadingCoeff * Polynomial.X + Polynomial.C (p.coeff 0)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree : ∀ {n : ℕ}, n ≠ 0 → (ArithmeticFunction.cardDistinctFactors n = ArithmeticFunction.cardFactors n ↔ Squarefree n)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_of_div_tendsto_nhds_of_ne_zero : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜} {a : 𝕜},
  Filter.Tendsto (fun x => g x / f x) l (nhds a) → a ≠ 0 → f =O[l] g
-- Mathlib.AlgebraicGeometry.Birational.Dominant
AlgebraicGeometry.Scheme.instIsDominantToRationalMapOfIsDominantHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) [AlgebraicGeometry.IsDominant f.hom], f.toRationalMap.IsDominant
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.Order.Frame.MinimalAxioms.inf_iSup₂_eq : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : CompleteLattice α],
  Order.Frame.MinimalAxioms α → ∀ {f : (i : ι) → κ i → α} (a : α), a ⊓ ⨆ i, ⨆ j, f i j = ⨆ i, ⨆ j, a ⊓ f i j
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.one_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A] (x : A), 1 x = x
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_or_inv_mem' : ∀ {K : Type u} [inst : Field K] (self : ValuationSubring K) (x : K), x ∈ self.carrier ∨ x⁻¹ ∈ self.carrier
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Finset.sum_smul_sum_eq_sum_perm : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : AddCommMonoid β] [inst_2 : Module α β]
  {s : Finset ι} {σ : Equiv.Perm ι},
  σ.IsCycleOn ↑s →
    ∀ (f : ι → α) (g : ι → β), (∑ i ∈ s, f i) • ∑ i ∈ s, g i = ∑ k ∈ Finset.range s.card, ∑ i ∈ s, f i • g ((σ ^ k) i)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (n : ℤ)
  {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app Y) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X)
      ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop).op
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.mem_set_smul_of_mem_mem : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] {s : Set S} {N : Submodule R M} {r : S} {m : M},
  r ∈ s → m ∈ N → r • m ∈ s • N
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.map_op_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] (s t : Finset α),
  Finset.map MulOpposite.opEquiv.toEmbedding (s * t) =
    Finset.map MulOpposite.opEquiv.toEmbedding t * Finset.map MulOpposite.opEquiv.toEmbedding s
-- Mathlib.Algebra.Algebra.Equiv
/-- Promotes a linear `RingEquiv` to an `AlgEquiv`.  -/
AlgEquiv.ofRingEquiv : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] →
            [inst_3 : Algebra R A₁] →
              [inst_4 : Algebra R A₂] →
                {f : A₁ ≃+* A₂} → (∀ (x : R), f ((algebraMap R A₁) x) = (algebraMap R A₂) x) → A₁ ≃ₐ[R] A₂
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.norm_argSelfAdjoint : ∀ {A : Type u_1} [inst : CStarAlgebra A] {u : ↥(unitary A)},
  ‖↑u - 1‖ < 2 → ‖Unitary.argSelfAdjoint u‖ = Real.arccos (1 - ‖↑u - 1‖ ^ 2 / 2)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Right.one_le_pow_of_le : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulRightMono M] {x : M}, 1 ≤ x → ∀ {n : ℕ}, 1 ≤ x ^ n
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.inv : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : Inv γ] [MeasurableInv γ],
  ProbabilityTheory.IdentDistrib f g μ ν → ProbabilityTheory.IdentDistrib f⁻¹ g⁻¹ μ ν
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_union!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.union! m₂).get? k = m₁.get? k
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- The object function for the right adjoint to the comparison functor.  -/
CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (adj : F ⊣ G) →
              (A : adj.toComonad.Coalgebra) →
                [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.1 A.A))] → C
-- Mathlib.Topology.ContinuousMap.Bounded.Star
BoundedContinuousFunction.instStarAddMonoid : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : SeminormedAddCommGroup β] →
        [inst_2 : StarAddMonoid β] → [NormedStarGroup β] → StarAddMonoid (BoundedContinuousFunction α β)
-- Mathlib.Algebra.CharZero.Defs
NeZero.charZero : ∀ {M : Type u_2} {n : ℕ} [NeZero n] [inst : AddMonoidWithOne M] [CharZero M], NeZero ↑n
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.norm_setIntegral_le_of_norm_le_const_ae : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {C : ℝ} [h : MeasureTheory.IsFiniteMeasure (μ.variation.restrict s)],
  (∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ ≤ C) → ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real s
-- Init.Data.List.OfFn
List.getLast_ofFn : ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α} (h : List.ofFn f ≠ []), (List.ofFn f).getLast h = f ⟨n - 1, ⋯⟩
-- Mathlib.Algebra.Ring.Defs
NonAssocRing.toIntCast : {α : Type u_1} → [self : NonAssocRing α] → IntCast α
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
Finset.abs_prod : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] (s : Finset ι)
  (f : ι → R), |∏ x ∈ s, f x| = ∏ x ∈ s, |f x|
-- Init.Data.SInt.Basic
/-- Converts an arbitrary-precision integer to an 8-bit integer, wrapping on overflow or underflow.

Examples:
* `Int.toInt8 48 = 48`
* `Int.toInt8 (-115) = -115`
* `Int.toInt8 (-129) = 127`
* `Int.toInt8 (128) = -128`
 -/
Int.toInt8 : ℤ → Int8
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- An affine isomorphism between the domains and a linear isomorphism between the codomains of two
spaces of affine maps give a linear isomorphism between the two function spaces.

See also `AffineEquiv.arrowCongrEquiv` and `AffineEquiv.arrowCongr`.  -/
AffineEquiv.arrowCongrₗ : {P₁ : Type u_2} →
  {P₂ : Type u_3} →
    {V₁ : Type u_6} →
      {V₂ : Type u_7} →
        {V₃ : Type u_8} →
          {V₄ : Type u_9} →
            [inst : AddCommGroup V₁] →
              [inst_1 : AddCommGroup V₂] →
                [inst_2 : AddCommGroup V₃] →
                  [inst_3 : AddCommGroup V₄] →
                    [inst_4 : AddTorsor V₁ P₁] →
                      [inst_5 : AddTorsor V₂ P₂] →
                        {R : Type u_10} →
                          [inst_6 : CommRing R] →
                            [inst_7 : Module R V₁] →
                              [inst_8 : Module R V₂] →
                                [inst_9 : Module R V₃] →
                                  [inst_10 : Module R V₄] →
                                    (P₁ ≃ᵃ[R] P₂) → (V₃ ≃ₗ[R] V₄) → (P₁ →ᵃ[R] V₃) ≃ₗ[R] P₂ →ᵃ[R] V₄
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cocone F},
  H.mapCoconePrecomposeEquivalenceFunctor.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
-- Mathlib.Analysis.Complex.Positivity
/-- An entire function whose iterated derivatives at `c` are all real with alternating signs
(except possibly the value itself) has values of the form `f c + nonneg. real` along the
set `c - ℝ≥0`.  -/
Differentiable.apply_le_of_iteratedDeriv_alternating : ∀ {f : ℂ → ℂ} {c : ℂ},
  Differentiable ℂ f → (∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c) → ∀ ⦃z : ℂ⦄, z ≤ c → f c ≤ f z
-- Lean.Elab.BindersUtil
/-- Expand a match alternative such as `| 0 | 1 => rhs` to an array containing `| 0 => rhs` and `| 1 => rhs`.
 -/
Lean.Elab.Term.expandMatchAlt : Lean.TSyntax `Lean.Parser.Term.matchAlt → Array (Lean.TSyntax `Lean.Parser.Term.matchAlt)
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Entry.measure : {α : Type u_1} → {β : Type u_2} → Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → ℕ
-- Mathlib.Topology.Algebra.Monoid
ContinuousWithinAt.pow : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Monoid M]
  [ContinuousMul M] {f : X → M} {x : X} {s : Set X},
  ContinuousWithinAt f s x → ∀ (n : ℕ), ContinuousWithinAt (f ^ n) s x
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) Construct the lifted cocone in `Coalgebra T` which will be colimiting.  -/
CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          (D : CategoryTheory.Functor J T.Coalgebra) →
            (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) →
              CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.Cocone D
-- Lean.Data.Name
Lean.Name.isPrefixOf : Lean.Name → Lean.Name → Bool
-- Mathlib.Probability.Distributions.Cauchy
/-- `cauchyPDFReal` is positive for `γ > 0`.  -/
ProbabilityTheory.cauchyPDF_pos : ∀ (x₀ : ℝ) {γ : NNReal}, γ ≠ 0 → ∀ (x : ℝ), 0 < ProbabilityTheory.cauchyPDFReal x₀ γ x
-- Mathlib.GroupTheory.OrderOfElement
mem_zpowers_zpow_iff : ∀ {G : Type u_1} [inst : Group G] {g : G} {k : ℤ}, g ∈ Subgroup.zpowers (g ^ k) ↔ k.gcd ↑(orderOf g) = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∪ t₂).getKey! k = t₂.getKeyD k (t₁.getKey! k)
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.evalₐ_liftRingHom : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m)
  (n : ℕ) (x : R), (AdicCompletion.evalₐ I n) ((AdicCompletion.liftRingHom I f ⋯) x) = (f n) x