mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- `NonUnitalAlgHomClass F R A B` asserts `F` is a type of bundled algebra homomorphisms
from `A` to `B` which are `R`-linear.

  This is an abbreviation to `NonUnitalAlgSemiHomClass F (MonoidHom.id R) A B`  -/
NonUnitalAlgHomClass : (F : Type u_1) →
  (R : outParam (Type u_2)) →
    (A : outParam (Type u_3)) →
      (B : outParam (Type u_4)) →
        [inst : Monoid R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : NonUnitalNonAssocSemiring B] →
              [DistribMulAction R A] → [DistribMulAction R B] → [FunLike F A B] → Prop
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.unop_injective : ∀ {G : Type u_2} [inst : AddGroup G], Function.Injective AddSubgroup.unop
-- Init.Data.UInt.Lemmas
instAssociativeUInt32HMul : Std.Associative fun x1 x2 => x1 * x2
-- Init.Data.List.Basic
List.flatten_nil : ∀ {α : Type u}, [].flatten = []
-- Std.Do.Triple.SpecLemmas
List.Cursor.pos_le_length : ∀ {α : Type u_1} {l : List α} {c : l.Cursor}, c.pos ≤ l.length
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.MethodsRef : Type
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_a : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (V : CategoryTheory.Endofunctor.Coalgebra G),
  ((CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf adj).obj V).a = V.V
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_iSup : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] {ι : Sort uι} (t : Submodule R A) (s : ι → Submodule R A), t * ⨆ i, s i = ⨆ i, t * s i
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_val_map_subtype_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] (f : α → β) (p : α → Prop) [inst_1 : DecidablePred p]
  [inst_2 : Fintype { a // p a }],
  Multiset.map (Subtype.restrict p f) Finset.univ.val = Multiset.map f (Finset.filter p Finset.univ).val
-- Mathlib.Order.OrderIsoNat
Nat.orderEmbeddingOfSet_range : ∀ (s : Set ℕ) [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s], Set.range ⇑(Nat.orderEmbeddingOfSet s) = s
-- Mathlib.Combinatorics.Enumerative.Schroder
_private.Mathlib.Combinatorics.Enumerative.Schroder.0.Nat.smallSchroder.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ => h_3 n) =
    h_2 ()
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.forall_mem_mem : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ {x : α}, (∀ t ∈ l, x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i
-- Mathlib.Topology.UniformSpace.HeineCantor
HasCompactMulSupport.uniformContinuous_of_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} [inst_2 : One β],
  HasCompactMulSupport f → Continuous f → UniformContinuous f
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- Given a presheaf of modules `M`, `s : M.sections` and `X : Cᵒᵖ`, this is the induced
element in `M.obj X`.  -/
PresheafOfModules.sections.eval : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M : PresheafOfModules R} → M.sections → (X : Cᵒᵖ) → ↑(M.obj X)
-- Mathlib.Combinatorics.Graph.Subgraph
_private.Mathlib.Combinatorics.Graph.Subgraph.0.Graph.IsLink.anti_of_mem : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β},
  G.IsLink e x y → H ≤ G → e ∈ H.edgeSet → H.IsLink e x y
-- Lean.Data.Options
Lean.OptionDecl.mk.injEq : ∀ (name : Lean.Name) (declName : autoParam Lean.Name Lean.OptionDecl.declName._autoParam) (defValue : Lean.DataValue)
  (descr : String) (deprecation? : Option Lean.OptionDeprecation) (name_1 : Lean.Name)
  (declName_1 : autoParam Lean.Name Lean.OptionDecl.declName._autoParam) (defValue_1 : Lean.DataValue)
  (descr_1 : String) (deprecation?_1 : Option Lean.OptionDeprecation),
  ({ name := name, declName := declName, defValue := defValue, descr := descr, deprecation? := deprecation? } =
      { name := name_1, declName := declName_1, defValue := defValue_1, descr := descr_1,
        deprecation? := deprecation?_1 }) =
    (name = name_1 ∧ declName = declName_1 ∧ defValue = defValue_1 ∧ descr = descr_1 ∧ deprecation? = deprecation?_1)
-- Mathlib.Topology.GDelta.Basic
/-- **Alias** of `IsGδ.preimage`.

---

The preimage of a Gδ set under a continuous map is Gδ.  -/
isGδ_induced : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  Continuous f → IsGδ s → IsGδ (f ⁻¹' s)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.zero_lt_lift_iff : ∀ {a : Cardinal.{u}}, 0 < Cardinal.lift.{v, u} a ↔ 0 < a
-- Mathlib.Data.Matrix.Mul
add_dotProduct : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring α] (u v w : m → α),
  (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.boolean : Lean.Lsp.SymbolKind
-- Mathlib.RingTheory.WittVector.Defs
/-- Let `φ` be a family of polynomials, indexed by natural numbers, whose variables come from the
disjoint union of `k` copies of `ℕ`, and let `xᵢ` be a Witt vector for `0 ≤ i < k`.

`eval φ x` evaluates `φ` mapping the variable `X_(i, n)` to the `n`th coefficient of `xᵢ`.

Instantiating `φ` with certain polynomials defined in
`Mathlib/RingTheory/WittVector/StructurePolynomial.lean` establishes the
ring operations on `𝕎 R`. For example, `WittVector.wittAdd` is such a `φ` with `k = 2`;
evaluating this at `(x₀, x₁)` gives us the sum of two Witt vectors `x₀ + x₁`.
 -/
WittVector.eval : {p : ℕ} →
  {R : Type u_1} → [CommRing R] → {k : ℕ} → (ℕ → MvPolynomial (Fin k × ℕ) ℤ) → (Fin k → WittVector p R) → WittVector p R
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `none` if no such pair exists.
 -/
Std.TreeMap.getEntryGT? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → Option (α × β)
-- Mathlib.Topology.Homotopy.HomotopyGroup
Cube.insertAt_boundary : ∀ {N : Type u_1} [inst : DecidableEq N] (i : N) {t₀ : ↑unitInterval} {t : { j // j ≠ i } → ↑unitInterval},
  (t₀ = 0 ∨ t₀ = 1) ∨ t ∈ Cube.boundary { j // j ≠ i } → (Cube.insertAt i) (t₀, t) ∈ Cube.boundary N
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.π.eq_1 : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Cofork f g),
  t.π = t.ι.app CategoryTheory.Limits.WalkingParallelPair.one
-- Mathlib.Algebra.Order.Group.DenselyOrdered
_private.Mathlib.Algebra.Order.Group.DenselyOrdered.0.exists_mul_left_lt : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LT α] [DenselyOrdered α] [MulRightStrictMono α] {a b c : α},
  a * b < c → ∃ a' > a, a' * b < c
-- Mathlib.Topology.Algebra.GroupWithZero
Filter.Tendsto.div_const : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : DivInvMonoid G₀] [inst_1 : TopologicalSpace G₀] [SeparatelyContinuousMul G₀]
  {f : α → G₀} {l : Filter α} {x : G₀},
  Filter.Tendsto f l (nhds x) → ∀ (y : G₀), Filter.Tendsto (fun a => f a / y) l (nhds (x / y))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.comp_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 Y Z : CategoryTheory.Limits.CategoricalPullback F G} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).fst = CategoryTheory.CategoryStruct.comp f.fst g.fst
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAgainst.isStableUnderBaseChangeAlong : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P P' : CategoryTheory.MorphismProperty C}
  [self : P.IsStableUnderBaseChangeAgainst P'] ⦃X Y : C⦄ (f : X ⟶ Y), P' f → P.IsStableUnderBaseChangeAlong f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedFunDecl.default_1 : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu
-- Lean.DocString.Types
Lean.Doc.Inline.concat.sizeOf_spec : ∀ {i : Type u} [inst : SizeOf i] (content : Array (Lean.Doc.Inline i)),
  sizeOf (Lean.Doc.Inline.concat content) = 1 + sizeOf content
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] [AlgebraicGeometry.LocallyOfFiniteType f]
  [inst_3 : CategoryTheory.IsCofiltered I] [inst_4 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)]
  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) [∀ (i : I), AlgebraicGeometry.IsAffineHom (A.c.π.app i)]
  (j : A.𝒰D.I₀),
  ∃ k hki',
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j)
        (CategoryTheory.CategoryStruct.comp (D.map (CategoryTheory.CategoryStruct.comp hki' A.hii')) A.a) =
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j)
        (CategoryTheory.CategoryStruct.comp (D.map (CategoryTheory.CategoryStruct.comp hki' A.hii')) A.b)
-- Mathlib.Algebra.Category.Ring.Limits
/-- Auxiliary lemma to prove the cone induced by `limitCone` is a limit cone.
 -/
SemiRingCat.forget₂AddCommMonPreservesLimitsAux : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J SemiRingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] →
        CategoryTheory.Limits.IsLimit
          ((CategoryTheory.forget₂ SemiRingCat AddCommMonCat).mapCone (SemiRingCat.HasLimits.limitCone F))
-- Mathlib.Logic.Function.Basic
Function.surjective_iff_hasRightInverse : ∀ {α : Sort u} {β : Sort v} {f : α → β}, Function.Surjective f ↔ Function.HasRightInverse f
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.congr_of_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → g =ᶠ[nhdsWithin x s] f → g x = f x → ContinuousWithinAt g s x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.le_maxKeyD_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → ∀ {fallback : α}, (cmp k (t.maxKeyD fallback)).isLE = true
-- Mathlib.Util.AtomM.Recurse
/-- The monad for `AtomM.Recurse` contains, in addition to the `AtomM` state,
a simp context for the main traversal and a cleanup function to simplify evaluation results.  -/
Mathlib.Tactic.AtomM.RecurseM : Type → Type
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.mulEquivSubgroup_symm_apply : ∀ {G : Type u_2} [inst : Group G] {H K : Subgroup G} [inst_1 : H.Normal] (h : H.IsComplement' K) (b : G),
  (SemidirectProduct.mulEquivSubgroup h).symm b = Function.surjInv ⋯ b
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instAddMonoid : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} → [inst_1 : AddOreLocalization.AddOreSet S] → AddMonoid (AddOreLocalization S R)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} (h' : k ∈ t), t.getKey k h' = k
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  Set.range ⇑(CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι) = X.zeroLocus ↑(I.ideal U) ∩ ↑↑U
-- Lean.Widget.InteractiveGoal
Lean.Widget.instAppendInteractiveGoals : Append Lean.Widget.InteractiveGoals
-- Std.Data.Internal.List.Associative
Std.Internal.List.contains_insertList_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true ↔
    Std.Internal.List.containsKey k l = true ∨ Std.Internal.List.containsKey k toInsert = true
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
instInhabitedTensorAlgebra : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_2) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Inhabited (TensorAlgebra R M)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
m_Birkhoff_inequalities : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b c : α),
  |(a ⊔ c) / (b ⊔ c)|ₘ ⊔ |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.toSubtype'.match_1.eq_1 : ∀
  (motive :
    (n : ℕ) →
      (α : TypeVec.{u_1} n) →
        (p : (α.prod α).Arrow (TypeVec.repeat n Prop)) →
          (x : Fin2 n) → { x_1 // TypeVec.ofRepeat (p x (TypeVec.prod.mk x x_1.1 x_1.2)) } → Sort u_2)
  (n : ℕ) (α : TypeVec.{u_1} (n + 1)) (p : (α.prod α).Arrow (TypeVec.repeat (n + 1) Prop)) (i : Fin2 n)
  (x : { x // TypeVec.ofRepeat (p i.fs (TypeVec.prod.mk i.fs x.1 x.2)) })
  (h_1 :
    (n : ℕ) →
      (α : TypeVec.{u_1} (n + 1)) →
        (p : (α.prod α).Arrow (TypeVec.repeat (n + 1) Prop)) →
          (i : Fin2 n) →
            (x : { x // TypeVec.ofRepeat (p i.fs (TypeVec.prod.mk i.fs x.1 x.2)) }) → motive (n + 1) α p i.fs x)
  (h_2 :
    (n : ℕ) →
      (α : TypeVec.{u_1} (n + 1)) →
        (p : (α.prod α).Arrow (TypeVec.repeat (n + 1) Prop)) →
          (x : { x // TypeVec.ofRepeat (p Fin2.fz (TypeVec.prod.mk Fin2.fz x.1 x.2)) }) → motive (n + 1) α p Fin2.fz x),
  (match n + 1, α, p, i.fs, x with
    | .(n + 1), α, p, i.fs, x => h_1 n α p i x
    | .(n + 1), α, p, Fin2.fz, x => h_2 n α p x) =
    h_1 n α p i x
-- Init.Data.List.Erase
List.eraseIdx_eq_take_drop_succ : ∀ {α : Type u_1} (l : List α) (i : ℕ), l.eraseIdx i = List.take i l ++ List.drop (i + 1) l
-- Init.Prelude
Inv.mk : {α : Type u} → (α → α) → Inv α
-- Mathlib.Topology.Algebra.UniformMulAction
UniformContinuousConstSMul.mk : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : SMul M X],
  (∀ (c : M), UniformContinuous fun x => c • x) → UniformContinuousConstSMul M X
-- Mathlib.GroupTheory.Index
/-- Relative version of `AddSubgroup.index_dvd_two_iff'`.  -/
AddSubgroup.relIindex_dvd_two_iff' : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.relIndex K ∣ 2 ↔ ∃ a ∈ K, ∀ b ∈ K, a + b ∈ H ∨ b ∈ H
-- Lean.Elab.Tactic.SolveByElim
_private.Lean.Elab.Tactic.SolveByElim.0.Lean.Elab.Tactic.SolveByElim.elabConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Lean.Meta.SolveByElim.SolveByElimConfig
-- Init.Data.Int.DivMod.Basic
Int.fdiv.eq_5 : ∀ (m n : ℕ), (Int.negSucc m).fdiv (Int.ofNat n.succ) = Int.negSucc (m / n.succ)
-- Std.Http.Data.URI.Encoding
Char.ofUInt8.eq_1 : ∀ (n : UInt8), Char.ofUInt8 n = { val := n.toUInt32, valid := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The identification `mop X ⊗ mop Y = mop (Y ⊗ X)` as a natural isomorphism.  -/
CategoryTheory.MonoidalOpposite.tensorIso : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.MonoidalCategory.tensor Cᴹᵒᵖ ≅
        ((CategoryTheory.unmopFunctor C).prod (CategoryTheory.unmopFunctor C)).comp
          ((CategoryTheory.Prod.swap C C).comp
            ((CategoryTheory.MonoidalCategory.tensor C).comp (CategoryTheory.mopFunctor C)))
-- Init.Data.String.Defs
String.Slice.instDecidableEqPos.decEq : {s : String.Slice} → (x x_1 : s.Pos) → Decidable (x = x_1)
-- Lean.Meta.Constructions.BRecOn
Lean.mkBRecOn : Lean.Name → Lean.MetaM Unit
-- Mathlib.Analysis.SpecificLimits.Basic
tsum_geometric_of_lt_one : ∀ {r : ℝ}, 0 ≤ r → r < 1 → ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
-- Mathlib.RingTheory.SimpleModule.IsAlgClosed
/-- The **Wedderburn–Artin Theorem** over algebraically closed fields: a finite-dimensional
simple algebra over an algebraically closed field is isomorphic to a matrix algebra over the field.
 -/
IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed : ∀ (F : Type u_1) (R : Type u_2) [inst : Field F] [IsAlgClosed F] [inst_2 : Ring R] [inst_3 : Algebra F R]
  [IsSimpleRing R] [FiniteDimensional F R], ∃ n, ∃ (_ : NeZero n), Nonempty (R ≃ₐ[F] Matrix (Fin n) (Fin n) F)
-- Lean.Parser.Command
Lean.Parser.Command.docs_to_verso.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Probability.Kernel.CondDistrib
/-- The conditional expectation of a function `f` of the product `(X, Y)` is almost everywhere equal
to the integral of `y ↦ f(X, y)` against the `condDistrib` kernel.  -/
ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib₀ : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F}
  [inst_5 : NormedSpace ℝ F] [CompleteSpace F],
  Measurable X →
    AEMeasurable Y μ →
      MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
        MeasureTheory.Integrable (fun a => f (X a, Y a)) μ →
          μ[fun a => f (X a, Y a) | MeasurableSpace.comap X mβ] =ᵐ[μ] fun a =>
            ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
-- Mathlib.Algebra.Module.Submodule.Ker
Submodule.ker_subtype : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submodule R M), p.subtype.ker = ⊥
-- Mathlib.Order.Interval.Finset.Defs
/-- Given an order embedding `α ↪o β`, pulls back the `LocallyFiniteOrder` on `β` to `α`.  -/
OrderEmbedding.locallyFiniteOrder : {α : Type u_1} →
  {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → [LocallyFiniteOrder β] → α ↪o β → LocallyFiniteOrder α
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.q : {A : Type u} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          (self : Algebra.Smooth.DescentAux✝ A B) →
            Algebra.Smooth.DescentAux.vars✝ self →
              MvPolynomial (Algebra.Smooth.DescentAux.rels✝ self) (Algebra.Smooth.DescentAux.P✝ self).Ring
-- Mathlib.Data.Finset.Defs
Finset.notMem_mono : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → ∀ {a : α}, a ∉ t → a ∉ s
-- Mathlib.Topology.Category.TopCat.Basic
/-- Replace a function coercion for a morphism `TopCat.of X ⟶ TopCat.of Y` with the definitionally
equal function coercion for a continuous map `C(X, Y)`.
 -/
TopCat.coe_of_of : ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  {x : (CategoryTheory.forget TopCat).obj (TopCat.of X)}, (TopCat.ofHom f) x = f x
-- Mathlib.RepresentationTheory.Rep.Iso
/-- The categorical equivalence `Rep k G ≌ ModuleCat k[G]`.  -/
Rep.equivalenceModuleMonoidAlgebra : {k : Type u} →
  {G : Type v} → [inst : CommRing k] → [inst_1 : Monoid G] → Rep.{w, u, v} k G ≌ ModuleCat (MonoidAlgebra k G)
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.isIso_factorThruImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {P Q : C}
  (f : P ⟶ Q) [CategoryTheory.Mono f], CategoryTheory.IsIso (CategoryTheory.Abelian.factorThruImage f)
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.heq_of_cons_eq_cons : ∀ {V : Type u} [inst : Quiver V] {a b c d : V} {p : Quiver.Path a b} {p' : Quiver.Path a c} {e : b ⟶ d} {e' : c ⟶ d},
  p.cons e = p'.cons e' → p ≍ p'
-- Aesop.Builder.Cases
Aesop.RuleBuilder.cases : Aesop.RuleBuilder
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_dirac : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) (x : X) (v : F),
  (MeasureTheory.VectorMeasure.dirac x v).transpose B = MeasureTheory.VectorMeasure.dirac x (B.flip v)
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_bitVecToNat : ∀ (n : BitVec 32), UInt32.ofNatLT n.toNat ⋯ = { toBitVec := n }
-- Init.Data.Array.Subarray
/-- Folds an operation from right to left over the elements in a subarray.

An accumulator of type `β` is constructed by starting with `init` and combining each element of the
subarray with the current accumulator value in turn, moving from the end to the start.

Examples:
 * `#["red", "green", "blue"].toSubarray.foldr (·.length + ·) 0 = 12`
 * `#["red", "green", "blue"].toSubarray.popFront.foldr (·.length + ·) 0 = 9`
 -/
Subarray.foldr : {α : Type u} → {β : Type v} → (α → β → β) → β → Subarray α → β
-- Mathlib.Data.Real.ConjExponents
NNReal.holderConjugate_comm : ∀ {p q : NNReal}, p.HolderConjugate q ↔ q.HolderConjugate p
-- Mathlib.Data.Multiset.Sym
Multiset.sym2_mono : ∀ {α : Type u_1} {m m' : Multiset α}, m ≤ m' → m.sym2 ≤ m'.sym2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_le_pi : ∀ (θ : Real.Angle), θ.toReal ≤ Real.pi
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- A polynomial `q` that satisfies `φ * q = (generator E).minpolyX`.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.q : {K : Type u_1} → [inst : Field K] → (E : IntermediateField K (RatFunc K)) → Polynomial ↥E
-- Mathlib.Data.Set.Basic
Set.inter_self : ∀ {α : Type u} (a : Set α), a ∩ a = a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a fallback : α}, (m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right]
  {K₁ K₂ :
    CategoryTheory.Limits.Fork
      (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
        (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))
      (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
        (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))}
  (f : K₁ ⟶ K₂), (I.multiforkEquivPiFork.inverse.map f).hom = f.hom
-- Mathlib.Data.Nat.Digits.Defs
/-- Interpreting as a base `p` number and dividing by `p^i` is the same as dropping `i`.
 -/
Nat.ofDigits_div_pow_eq_ofDigits_drop : ∀ {p : ℕ} (i : ℕ),
  0 < p →
    ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → Nat.ofDigits p digits / p ^ i = Nat.ofDigits p (List.drop i digits)
-- Mathlib.Algebra.Order.Archimedean.Basic
instIsDirectedOrder : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R], IsDirectedOrder R
-- Mathlib.Order.Basic
Prod.le_def : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] {x y : α × β}, x ≤ y ↔ x.1 ≤ y.1 ∧ x.2 ≤ y.2
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- The `Submonoid.closure` of a set is the union of `{1}` and its `Subsemigroup.closure`.  -/
Submonoid.closure_eq_one_union : ∀ {M : Type u_1} [inst : MulOneClass M] (s : Set M), ↑(Submonoid.closure s) = {1} ∪ ↑(Subsemigroup.closure s)