mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrix_mem_of_ne : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [CharZero R] [IsDomain R] [Finite ι] {i j : ↥b.support},
  i ≠ j → b.cartanMatrix i j ∈ {-3, -2, -1, 0}
-- Lean.Structure
/-- Information about the structure fields, sorted by `fieldName`.  -/
Lean.StructureInfo.fieldInfo : Lean.StructureInfo → Array Lean.StructureFieldInfo
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Monomial degree of product  -/
MonomialOrder.degree_mul : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
  {f g : MvPolynomial σ R}, f ≠ 0 → g ≠ 0 → m.degree (f * g) = m.degree f + m.degree g
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instVAddCommClass_2 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd N α] [VAddCommClass M N α],
  VAddCommClass M N αᵒᵈ
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_ne_zero : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a : α} [AddRightMono α], |a| ≠ 0 ↔ a ≠ 0
-- Mathlib.Topology.Algebra.Support
hasCompactMulSupport_def : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] {f : α → β},
  HasCompactMulSupport f ↔ IsCompact (closure (Function.mulSupport f))
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv : ∀ {X : AlgebraicGeometry.Scheme} {B : CommRingCat} (φ : B ⟶ X.presheaf.obj (Opposite.op ⊤)),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso B).inv
      (AlgebraicGeometry.Scheme.Hom.appTop ((AlgebraicGeometry.ΓSpec.adjunction.homEquiv X (Opposite.op B)) φ.op)) =
    φ
-- Mathlib.RingTheory.Regular.Category
ModuleCat.smulShortComplex_g_hom_apply : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) (r : R) (a : ↑M),
  (ModuleCat.Hom.hom (M.smulShortComplex r).g) a = Submodule.Quotient.mk a
-- Mathlib.Order.WithBot
WithBot.coe_lt_coe : ∀ {α : Type u_1} {a b : α} [inst : LT α], ↑a < ↑b ↔ a < b
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_range : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {ι : Sort u_5} {f : ι → α}, -Set.range f = Set.range fun i => -f i
-- Init.Data.Format.Basic
/-- Intercalates the given list with the given `sep` format.

The list items are formatting using `ToFormat.format`.
 -/
Std.Format.joinSep : {α : Type u} → [Std.ToFormat α] → List α → Std.Format → Std.Format
-- Init.System.IO
/-- Removes (deletes) a file from the filesystem.

To remove a directory, use `IO.FS.removeDir` or `IO.FS.removeDirAll` instead.
 -/
IO.FS.removeFile : System.FilePath → IO Unit
-- Std.Data.DTreeMap.Raw.Lemmas
_private.Std.Data.DTreeMap.Raw.Lemmas.0.Break.runK.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If `p` is a finite formal multilinear series, then so is `p.changeOriginSeries k` for every
`k` in `ℕ`. More precisely, if `p m = 0` for `n ≤ m`, then `p.changeOriginSeries k m = 0` for
`n ≤ k + m`.  -/
FormalMultilinearSeries.changeOriginSeries_finite_of_finite : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ},
  (∀ (m : ℕ), n ≤ m → p m = 0) → ∀ (k : ℕ) {m : ℕ}, n ≤ k + m → p.changeOriginSeries k m = 0
-- Mathlib.Order.InitialSeg
RelEmbedding.ofIsEmpty.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : IsEmpty α],
  RelEmbedding.ofIsEmpty r s = RelEmbedding.ofIsEmpty r s
-- Mathlib.Data.List.OfFn
List.exists_iff_exists_tuple : ∀ {α : Type u} {P : List α → Prop}, (∃ l, P l) ↔ ∃ n f, P (List.ofFn f)
-- Init.Data.Int.DivMod.Lemmas
Int.negSucc_emod_negSucc_eq_zero_iff : ∀ {a b : ℕ}, Int.negSucc a % Int.negSucc b = 0 ↔ (a + 1) % (b + 1) = 0
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- For maps between vector spaces, `MDifferentiable` and `Differentiable` coincide  -/
mdifferentiable_iff_differentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'},
  MDiff f ↔ Differentiable 𝕜 f
-- Mathlib.RingTheory.HahnSeries.Binomial
HahnSeries.SummableFamily.binomialFamily_apply_of_orderTop_nonpos : ∀ {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : LinearOrder Γ] [inst_1 : AddCommMonoid Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : BinomialRing R] [inst_5 : CommRing A]
  [inst_6 : Algebra R A] {x : HahnSeries Γ A},
  ¬0 < (x - 1).orderTop → ∀ (r : R) (n : ℕ), (HahnSeries.SummableFamily.binomialFamily x r) n = 0 ^ n
-- Init.Data.Option.Lemmas
Option.isSome_eq_false_iff : ∀ {α : Type u_1} {a : Option α}, a.isSome = false ↔ a.isNone = true
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.eval₂_algebraMap_X : ∀ {R : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (p : Polynomial R)
  (f : Polynomial R →ₐ[R] A), Polynomial.eval₂ (algebraMap R A) (f Polynomial.X) p = f p
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → ∀ {t : Set E}, s ∈ nhdsWithin x t → ContDiffWithinAt 𝕜 n f t x
-- Mathlib.GroupTheory.CosetCover
Subgroup.index_le_of_leftCoset_cover_const : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {s : Finset ι} {H : Subgroup G} {g : ι → G},
  ⋃ i ∈ s, g i • ↑H = Set.univ → H.index ≤ s.card
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
/-- [Stacks Tag 01K9](https://stacks.math.columbia.edu/tag/01K9) -/
AlgebraicGeometry.isClosedMap_iff_specializingMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f], IsClosedMap ⇑f ↔ SpecializingMap ⇑f
-- Mathlib.RingTheory.Ideal.Nonunits
zero_mem_nonunits : ∀ {α : Type u_2} [inst : MonoidWithZero α], 0 ∈ nonunits α ↔ 0 ≠ 1
-- Mathlib.RingTheory.PowerSeries.Exp
/-- Power series for the exponential function at zero.  -/
PowerSeries.exp : (A : Type u_1) → [inst : Ring A] → [Algebra ℚ A] → PowerSeries A
-- Lean.Util.LeanOptions
/-- Add the options from `new`, overriding those in `self`.  -/
Lean.LeanOptions.appendArray : Lean.LeanOptions → Array Lean.LeanOption → Lean.LeanOptions
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndepOn.insert : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] {s : Set ι} {i : ι},
  AlgebraicIndepOn R x s → Transcendental (↥(Algebra.adjoin R (x '' s))) (x i) → AlgebraicIndepOn R x (insert i s)
-- Mathlib.Data.Vector.Basic
List.Vector.get_append_cons_succ : ∀ {α : Type u_1} {m n : ℕ} {x : α} (xs : List.Vector α n) (ys : List.Vector α m) {i : Fin (n + m)}
  {h : ↑i + 1 < n.succ + m}, (x ::ᵥ xs ++ ys).get ⟨↑i + 1, h⟩ = (xs ++ ys).get i
-- Mathlib.GroupTheory.Exponent
/-- Any cancellative monoid of exponent two is abelian.  -/
commMonoidOfExponentTwo : {G : Type u} → [inst : Monoid G] → [IsCancelMul G] → Monoid.exponent G = 2 → CommMonoid G
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
isNoetherian_adjoin_finset : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [IsNoetherianRing R]
  (s : Finset A), (∀ x ∈ s, IsIntegral R x) → IsNoetherian R ↥(Algebra.adjoin R ↑s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inr_isoIsPushout_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y}
  {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : CategoryTheory.IsPushout f g inl inr)
  (h' : CategoryTheory.IsPushout f g inl' inr'),
  CategoryTheory.CategoryStruct.comp inr' (CategoryTheory.IsPushout.isoIsPushout X Y h h').inv = inr
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_zero : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {x : Submonoid A}, HomogeneousLocalization.val 0 = 0
-- Mathlib.Order.Partition.Finpartition
Finpartition.copy.congr_simp : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a b : α} (P P_1 : Finpartition a),
  P = P_1 → ∀ (h : a = b), P.copy h = P_1.copy h
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.head.eq_1 : ∀ {α : Type u} (s : Stream'.WSeq α), s.head = Computation.map (fun x => Prod.fst <$> x) s.destruct
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.toRightFDRepComp_injective : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Finite G]
  {η₁ η₂ : CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)},
  η₁.hom.hom.app TannakaDuality.FiniteGroup.rightFDRep = η₂.hom.hom.app TannakaDuality.FiniteGroup.rightFDRep → η₁ = η₂
-- Mathlib.Tactic.NormNum.Irrational
/-- `norm_num` extension that proves `Irrational x ^ y` for rational `y`. `x` may be
natural or rational.  -/
Mathlib.Meta.NormNum.evalIrrationalRpow : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Tactic.Linter.FindDeprecations
/-- If `nm` is the name of a declaration, then `getDeprecatedInfo nm` returns the
`DeprecationInfo` data for `nm`.
Otherwise, it returns `none`.

If the `verbose?` input is `true`, then the command also summarizes what the data is.
 -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.getDeprecatedInfo : Lean.Name → Bool → Lean.Elab.Command.CommandElabM (Option Mathlib.Tactic.DeprecationInfo✝)
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
/-- If `R[X] → S` generates `S`, `T` is the localization of `S` away from `g` and
`f` is a pre-image of `g` in `R[X]`, this is the `R`-algebra map `R[X,Y] →ₐ[R] (R[X]/I²)[1/f]`
defined via mapping `Y` to `1/f`.  -/
Algebra.Generators.compLocalizationAwayAlgHom : {R : Type u_1} →
  {S : Type u_2} →
    (T : Type u_3) →
      {ι : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : CommRing T] →
                [inst_4 : Algebra R T] →
                  [inst_5 : Algebra S T] →
                    [inst_6 : IsScalarTower R S T] →
                      (g : S) →
                        [inst_7 : IsLocalization.Away g T] →
                          (P : Algebra.Generators R S ι) →
                            ((Algebra.Generators.localizationAway T g).comp P).Ring →ₐ[R]
                              Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g))
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.lim_of_mem_C : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P), ∀ x ∈ c.C, c.lim x = 0
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.instFaithfulSimplexCategoryToSimplexCategory : SemiSimplexCategory.toSimplexCategory.Faithful
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.union_sub : ∀ {α : Type u_2} [inst : Sub α] {s₁ s₂ t : Set α}, s₁ ∪ s₂ - t = s₁ - t ∪ (s₂ - t)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.map_op_zero : ∀ {α : Type u_2} [inst : Zero α], Finset.map AddOpposite.opEquiv.toEmbedding 0 = 0
-- Mathlib.Order.Hom.Basic
/-- Restriction of `f : α →o α →o β` to the diagonal.  -/
OrderHom.onDiag : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o α →o β) → α →o β
-- Mathlib.LinearAlgebra.Matrix.Unique
Matrix.uniqueLinearEquiv_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_4} [inst : Unique m] [inst_1 : Unique n]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid A] [inst_4 : Module R A] (a : Matrix m n A),
  Matrix.uniqueLinearEquiv a = Matrix.uniqueAddEquiv.toFun a
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
/-- the family is stable under restriction  -/
PresheafOfModules.Submodule.map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (self : M.Submodule) {X Y : Cᵒᵖ} (f : X ⟶ Y),
  self.obj X ≤ Submodule.comap (M.restrictₛₗ f) (self.obj Y)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.hom_ext : ∀ {X Y : AddSemigrp} {f g : X ⟶ Y}, AddSemigrp.Hom.hom f = AddSemigrp.Hom.hom g → f = g
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.isOrdinal_iff_mem_range_toZFSet : ∀ {x : ZFSet.{u}}, x.IsOrdinal ↔ x ∈ Set.range Ordinal.toZFSet
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.dist_map_zero_translationNumber_le : ∀ (f : CircleDeg1Lift), dist (f 0) f.translationNumber ≤ 1
-- Init.SimpLemmas
instIdempotentOpBoolOr : Std.IdempotentOp fun x1 x2 => x1 || x2
-- Mathlib.Analysis.SpecialFunctions.FrullaniIntegral
/-- If `f → R` as `x → +∞` and `f` is locally integrable on `(0, ∞)`, then the weighted integral
`∫ x in a*r..b*r, x⁻¹ • f x` converges to `log(b/a) • R` as `r → +∞`.  -/
Frullani.tendsto_integral_inv_smul_atTop : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {R : E}
  [CompleteSpace E],
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    0 < a →
      0 < b →
        Filter.Tendsto f Filter.atTop (nhds R) →
          Filter.Tendsto (fun r => ∫ (x : ℝ) in a * r..b * r, x⁻¹ • f x) Filter.atTop (nhds (Real.log (b / a) • R))
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
ContinuousLinearMap.measurable_apply₂ : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : MeasurableSpace E]
  [OpensMeasurableSpace E] [SecondCountableTopologyEither (E →L[𝕜] F) E] [inst_8 : MeasurableSpace F] [BorelSpace F],
  Measurable fun p => p.1 p.2
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- This is the same as `Matrix.l2_opNNNorm_def`, but with a more bundled RHS for square
matrices.  -/
Matrix.cstar_nnnorm_def : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n 𝕜),
  ‖A‖₊ = ‖Matrix.toEuclideanCLM A‖₊
-- Mathlib.Data.PFun
PFun.Part.bind_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (a : Part α),
  a.bind (f.comp g) = (a.bind g).bind f
-- Mathlib.Analysis.Convex.Strict
/-- Alternative definition of set strict convexity, using division.  -/
strictConvex_iff_div : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜 E] {s : Set E},
  StrictConvex 𝕜 s ↔
    s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instPropAsSPredTautologyEntailsImp : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, Std.Do.SPred.Tactic.PropAsSPredTautology (P ⊢ₛ Q) spred(P → Q)
-- Init.Data.Int.DivMod.Basic
/-- Balanced modulus.

This version of integer modulus uses the balanced rounding convention, which guarantees that
`-m / 2 ≤ Int.bmod x m < m/2` for `m ≠ 0` and `Int.bmod x m` is congruent to `x` modulo `m`.

If `m = 0`, then `Int.bmod x m = x`.

Examples:
* `(7 : Int).bmod 0 = 7`
* `(0 : Int).bmod 7 = 0`
* `(12 : Int).bmod 6 = 0`
* `(12 : Int).bmod 7 = -2`
* `(12 : Int).bmod 8 = -4`
* `(12 : Int).bmod 9 = 3`
* `(-12 : Int).bmod 6 = 0`
* `(-12 : Int).bmod 7 = 2`
* `(-12 : Int).bmod 8 = -4`
* `(-12 : Int).bmod 9 = -3`
 -/
Int.bmod : ℤ → ℕ → ℤ
-- Lean.SubExpr
Lean.SubExpr.GoalLocation.hypType.inj : ∀ {a : Lean.FVarId} {a_1 : Lean.SubExpr.Pos} {a_2 : Lean.FVarId} {a_3 : Lean.SubExpr.Pos},
  Lean.SubExpr.GoalLocation.hypType a a_1 = Lean.SubExpr.GoalLocation.hypType a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonRenameParams : Lean.FromJson Lean.Lsp.RenameParams
-- Mathlib.Probability.Independence.Conditional
/-- A family of functions defined on the same space `Ω` and taking values in possibly different
spaces, each with a measurable space structure, is conditionally independent if the family of
measurable space structures they generate on `Ω` is conditionally independent. For a function `g`
with codomain having measurable space structure `m`, the generated measurable space structure is
`m.comap g`.
See `ProbabilityTheory.iCondIndepFun_iff`.  -/
ProbabilityTheory.iCondIndepFun : {Ω : Type u_1} →
  {ι : Type u_2} →
    (m' : MeasurableSpace Ω) →
      {mΩ : MeasurableSpace Ω} →
        [StandardBorelSpace Ω] →
          m' ≤ mΩ →
            {β : ι → Type u_3} →
              [m : (x : ι) → MeasurableSpace (β x)] →
                ((x : ι) → Ω → β x) →
                  (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.iCondIndepFun._auto_1) →
                    [MeasureTheory.IsFiniteMeasure μ] → Prop
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, returning `none` if no such key exists.
 -/
Std.ExtDTreeMap.getKeyGE? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Option α
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.size.match_1.splitter : {α : Type u_1} →
  (motive : Ordnode α → Sort u_2) →
    (x : Ordnode α) →
      (Unit → motive Ordnode.nil) →
        ((sz : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node sz l x r)) → motive x
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
OrderIso.map_csInf_of_directedOn : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderInf α]
  [inst_1 : ConditionallyCompletePartialOrderInf β] (e : α ≃o β) {s : Set α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → s.Nonempty → BddBelow s → e (sInf s) = ⨅ x, e ↑x
-- Mathlib.LinearAlgebra.Trace
/-- The trace of the identity endomorphism is the dimension of the free module.  -/
LinearMap.trace_id : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M], (LinearMap.trace R M) LinearMap.id = ↑(Module.finrank R M)
-- Mathlib.Algebra.Homology.TotalComplexShift
/-- The isomorphism `((shiftFunctor₂ C y).obj K).total (up ℤ) ≅ (K.total (up ℤ))⟦y⟧`
expressing the compatibility of the total complex with the shift on the second indices.
This isomorphism involves signs: on the summand in degree `(p, q)` of `K`, it is given by the
multiplication by `(p * y).negOnePow`.  -/
HomologicalComplex₂.totalShift₂Iso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) →
        (y : ℤ) →
          [inst_2 : K.HasTotal (ComplexShape.up ℤ)] →
            ((HomologicalComplex₂.shiftFunctor₂ C y).obj K).total (ComplexShape.up ℤ) ≅
              (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).obj
                (K.total (ComplexShape.up ℤ))
-- Mathlib.RingTheory.Derivation.Basic
/-- The `LinearMap` underlying a `Derivation`.  -/
Derivation.toLinearMap : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] → [inst_4 : Module A M] → [inst_5 : Module R M] → Derivation R A M → A →ₗ[R] M
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.canonicallyOrderedAdd : CanonicallyOrderedAdd Ordinal.{u_1}
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- The condition that a pseudofunctor has effective descent
relative to a presieve.  -/
CategoryTheory.Pseudofunctor.IsStackFor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat →
      {S : C} → CategoryTheory.Presieve S → Prop
-- Mathlib.GroupTheory.GroupAction.Primitive
AddAction.IsPreprimitive.mk : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] [toIsPretransitive : AddAction.IsPretransitive G X],
  (∀ {B : Set X}, AddAction.IsBlock G B → AddAction.IsTrivialBlock B) → AddAction.IsPreprimitive G X
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balance!.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (ll lr : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (l r : Std.DTreeMap.Internal.Impl α β) →
                    motive Std.DTreeMap.Internal.Impl.leaf (Std.DTreeMap.Internal.Impl.inner size lrk lrv l r)) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (l r : Std.DTreeMap.Internal.Impl α β) →
                      motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (l r : Std.DTreeMap.Internal.Impl α β) →
                        (lrs : ℕ) →
                          (lrk : α) →
                            (lrv : β lrk) →
                              (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                                motive (Std.DTreeMap.Internal.Impl.inner size k v l r)
                                  (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)) →
                motive ll lr
-- Mathlib.Data.Num.Lemmas
Num.addMonoidWithOne : AddMonoidWithOne Num
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
/-- If `c` is a colimit cocone, then so is `coconeOfLE (ofCocone c) (le_refl j)`.  -/
CategoryTheory.SmallObject.SuccStruct.isColimitCoconeOfLEOfCocone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        {j : J} →
          {F : CategoryTheory.Functor (↑(Set.Iio j)) C} →
            {c : CategoryTheory.Limits.Cocone F} →
              CategoryTheory.Limits.IsColimit c →
                CategoryTheory.Limits.IsColimit
                  (CategoryTheory.SmallObject.coconeOfLE (CategoryTheory.SmallObject.SuccStruct.ofCocone c) ⋯)
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f g : CompleteLatticeHom α β},
  f = g ↔ ∀ (a : α), f a = g a
-- Init.Control.Lawful.Instances
ReaderT.run_seqRight : ∀ {m : Type u_1 → Type u_2} {ρ α β : Type u_1} [inst : Monad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ),
  (x *> y).run ctx = x.run ctx *> y.run ctx
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.mem_irrelevant_iff : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] (a : A), a ∈ HomogeneousIdeal.irrelevant 𝒜 ↔ (GradedRing.proj 𝒜 0) a = 0
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.Int32.beq_eq_decide_eq : ∀ {a b : Int32}, (a == b) = decide (a = b)
-- Mathlib.Algebra.Lie.Prod
LieHom.fst_surjective : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], Function.Surjective ⇑(LieHom.fst R L₁ L₂)