mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Constructions.SumProd
ContinuousAt.comp₂ : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : Y × Z → W} {g : X → Y} {h : X → Z} {x : X},
  ContinuousAt f (g x, h x) → ContinuousAt g x → ContinuousAt h x → ContinuousAt (fun x => f (g x, h x)) x
-- Lean.Server.FileWorker.SemanticHighlighting
/-- In case of overlap, higher-priority tokens will take precedence  -/
Lean.Server.FileWorker.AbsoluteLspSemanticToken.priority : Lean.Server.FileWorker.AbsoluteLspSemanticToken → ℕ
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.mem_mk : ∀ {K : Type u} [inst : DivisionRing K] {S : Subring K} {x : K} (h : ∀ x ∈ S.carrier, x⁻¹ ∈ S.carrier),
  x ∈ { toSubring := S, inv_mem' := h } ↔ x ∈ S
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `hasFDerivAtFilter_sub_const_iff`. -/
HasFDerivAtFilter.sub_const : ∀ {𝕜 : 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}
  {f' : E →L[𝕜] F} {L : Filter (E × E)} (c : F), HasFDerivAtFilter f f' L → HasFDerivAtFilter (fun x => f x - c) f' L
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
/-- Consider a commutative square in the category `CochainComplex C ℤ`
where `C` is an abelian category.
```
   t
 A ⟶ X
i|   |p
 v   v
 B ⟶ Y
   b
```
Assume that there exists a degreewise lifting `B.X n ⟶ X.X n` for any `n : ℤ`,
that `Q` is a cokernel of `i`, and `K` is a kernel of `p`.
If the cocycle `cocycle₁ sq hsq hQ hK : Cocycle Q K 1` is a coboundary,
we show that the square admits a lifting `B ⟶ X`.  -/
CochainComplex.Lifting.hasLift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b)
  (hsq : (n : ℤ) → ⋯.LiftStruct) {Q : CochainComplex C ℤ} {π : B ⟶ Q} {hπ : CategoryTheory.CategoryStruct.comp i π = 0}
  (hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ)) {K : CochainComplex C ℤ}
  {ι : K ⟶ X} {hι : CategoryTheory.CategoryStruct.comp ι p = 0}
  (hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι))
  (α : CochainComplex.HomComplex.Cochain Q K 0),
  CochainComplex.HomComplex.δ 0 1 α = ↑(CochainComplex.Lifting.cocycle₁ sq hsq hQ hK) → sq.HasLift
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_mul_mod_two : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W),
  cs.length (w₁ * w₂) % 2 = (cs.length w₁ + cs.length w₂) % 2
-- Init.Data.String.Search
String.Internal.anyImpl : String → (Char → Bool) → Bool
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.l_sInf_u_image : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisInsertion l u) (s : Set β), l (sInf (u '' s)) = sInf s
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.mulThms? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option Lean.Meta.Grind.Arith.Cutsat.ToIntThms
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.binaryCoproductCocone_ι_app : ∀ (X Y : Type u) (x : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
  (CategoryTheory.Limits.Types.binaryCoproductCocone X Y).ι.app x =
    match x.as with
    | CategoryTheory.Limits.WalkingPair.left => TypeCat.ofHom Sum.inl
    | CategoryTheory.Limits.WalkingPair.right => TypeCat.ofHom Sum.inr
-- Lean.Parser.Level
Lean.Parser.Level.paren.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_map_right : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  {Y X :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L')}
  (f : Y ⟶ X), ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).inverse.map f).right = f.right
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDerivWithin_vcomp_three : ∀ {𝕜 : 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] {g : E → F} {f : 𝕜 → E}
  {s : Set 𝕜} {t : Set E} {x : 𝕜},
  ContDiffWithinAt 𝕜 3 g t (f x) →
    ContDiffWithinAt 𝕜 3 f s x →
      UniqueDiffOn 𝕜 t →
        UniqueDiffOn 𝕜 s →
          x ∈ s →
            Set.MapsTo f s t →
              iteratedDerivWithin 3 (g ∘ f) s x =
                ((iteratedFDerivWithin 𝕜 3 g t (f x)) fun x_1 => derivWithin f s x) +
                      (iteratedFDerivWithin 𝕜 2 g t (f x)) ![iteratedDerivWithin 2 f s x, derivWithin f s x] +
                    2 • (iteratedFDerivWithin 𝕜 2 g t (f x)) ![derivWithin f s x, iteratedDerivWithin 2 f s x] +
                  (fderivWithin 𝕜 g t (f x)) (iteratedDerivWithin 3 f s x)
-- Batteries.Data.List.Basic
List.fillNones.eq_4 : ∀ {α : Type u_1} (as : List (Option α)) (a : α) (as' : List α),
  (none :: as).fillNones (a :: as') = a :: as.fillNones as'
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.updateCell.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l.size - 1) (l.size + 1) → Sort u_3)
  (newL : Std.DTreeMap.Internal.Impl α β) (h₁ : newL.Balanced) (h₂ : l.size - 1 ≤ newL.size)
  (h₃ : newL.size ≤ l.size + 1)
  (h_1 :
    (newL : Std.DTreeMap.Internal.Impl α β) →
      (h₁ : newL.Balanced) →
        (h₂ : l.size - 1 ≤ newL.size) →
          (h₃ : newL.size ≤ l.size + 1) →
            motive { impl := newL, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ }),
  (match { impl := newL, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ } with
    | { impl := newL, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ } => h_1 newL h₁ h₂ h₃) =
    h_1 newL h₁ h₂ h₃
-- Mathlib.Algebra.Free
FreeMagma.instMonad : Monad FreeMagma
-- Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
/-- Let `G` be a nonarchimedean abelian group, and let `f : ℕ → G` be a function
such that the quotients `f (n + 1) / f n` tend to one. Then the function is a Cauchy sequence.  -/
NonarchimedeanGroup.cauchySeq_of_tendsto_div_nhds_one : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : UniformSpace G] [IsUniformGroup G] [NonarchimedeanGroup G] {f : ℕ → G},
  Filter.Tendsto (fun n => f (n + 1) / f n) Filter.atTop (nhds 1) → CauchySeq f
-- Mathlib.Algebra.Module.LocalizedModule.Int
IsLocalizedModule.isInteger_add : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') {x y : M'},
  IsLocalizedModule.IsInteger f x → IsLocalizedModule.IsInteger f y → IsLocalizedModule.IsInteger f (x + y)
-- Mathlib.Data.Rel
SetRel.id_subset_iff : ∀ {α : Type u_1} {R : SetRel α α}, SetRel.id ⊆ R ↔ R.IsRefl
-- Init.Data.FloatArray.Basic
FloatArray.instForInFloatOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m FloatArray Float
-- Init.PropLemmas
forall_self_imp : ∀ (P : Prop) (Q : P → Prop), (∀ (p : P), P → Q p) ↔ ∀ (p : P), Q p
-- Std.Data.DTreeMap.Internal.Operations
/-- The tree is balanced.  -/
Std.DTreeMap.Internal.Impl.Tree.balanced_impl : ∀ {α : Type u} {β : α → Type v} {size : ℕ} (self : Std.DTreeMap.Internal.Impl.Tree α β size), self.impl.Balanced
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.GrpCat.Hom.mk.injEq : ∀ {A B : GrpCat} (hom' hom'_1 : ↑A →* ↑B), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingConeHomOfDegreewiseSplitXIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting)
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (p q : ℤ) (hpq : p + 1 = q),
  CochainComplex.mappingConeHomOfDegreewiseSplitXIso S σ p q hpq =
    {
      hom :=
        CategoryTheory.CategoryStruct.comp
            ((↑(CochainComplex.mappingCone.fst (CochainComplex.homOfDegreewiseSplit S σ))).v p q hpq) (σ q).s -
          CategoryTheory.CategoryStruct.comp
            ((CochainComplex.mappingCone.snd (CochainComplex.homOfDegreewiseSplit S σ)).v p p ⋯)
            ((CochainComplex.HomComplex.Cochain.ofHom S.f).v (p + 1) q ⋯),
      inv :=
        CategoryTheory.CategoryStruct.comp (S.g.f q)
            ((CochainComplex.mappingCone.inl (CochainComplex.homOfDegreewiseSplit S σ)).v q p ⋯) -
          CategoryTheory.CategoryStruct.comp (σ q).r
            (CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq S.X₁ ⋯).hom
              ((CochainComplex.mappingCone.inr (CochainComplex.homOfDegreewiseSplit S σ)).f p)),
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.untopD_natCast : ∀ {α : Type u} [inst : NatCast α] (d : α) (n : ℕ), WithTop.untopD d ↑n = ↑n
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.hom_inv_id : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cocone F} (f : c ≅ d),
  CategoryTheory.CategoryStruct.comp f.hom.hom f.inv.hom = CategoryTheory.CategoryStruct.id c.pt
-- Mathlib.Order.BooleanAlgebra.Set
Set.himp_def : ∀ {α : Type u_1} {s t : Set α}, s ⇨ t = t ∪ sᶜ
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.smul_mk : ∀ {ι : Type u_1} {α : Type u_3} {A : ι → Type u_2} [inst : (i : ι) → SMul α (A i)] {i : ι} (c : α) (a : A i),
  c • GradedMonoid.mk i a = GradedMonoid.mk i (c • a)
-- Mathlib.Algebra.Group.Prod
Prod.instInvolutiveInv : {M : Type u_3} → {N : Type u_4} → [InvolutiveInv M] → [InvolutiveInv N] → InvolutiveInv (M × N)
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.dpreDefault : Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whisker_assoc : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
  CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h))
        (CategoryTheory.Bicategory.associator f g' h).inv)
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.int_div_nonneg_of_nonneg_of_pos : ∀ {a b : ℤ}, 0 ≤ a → 0 < b → 0 ≤ a / b
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- The morphism `(A₁ ×_X A₂) ×_{A₁} (A₁ ×_X A₃) ⟶ A₁`.  -/
CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          [inst_2 : F.Full] →
            {A₁ A₂ A₃ : C} →
              {X : D} →
                {f₁ : F.obj A₁ ⟶ X} →
                  (hf₁ : F.relativelyRepresentable f₁) →
                    (f₂ : F.obj A₂ ⟶ X) →
                      (f₃ : F.obj A₃ ⟶ X) →
                        [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] →
                          hf₁.pullback₃ f₂ f₃ ⟶ A₁
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.smul_mem : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m),
  0 < m →
    ∀
      (q :
        ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace)
      (c x : A),
      x ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q →
        c • x ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q
-- Mathlib.CategoryTheory.Filtered.Final
/-- If `C` is filtered, then every functor `F : C ⥤ Discrete PUnit` is final.  -/
CategoryTheory.Functor.final_of_isFiltered_of_pUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFiltered C]
  (F : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{u_1 + 1})), F.Final
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_right_inj : ∀ {a b c : Ordinal.{u_1}}, 1 < a → (a ^ b = a ^ c ↔ b = c)
-- Batteries.Recycling.RBTree.Alter
/-- Descend into the left subtree of a red node.  -/
RBTree.RBNode.Path.Balanced.redL : ∀ {c₀ : RBTree.RBColor} {n₀ : ℕ} {α : Type u_1} {y : RBTree.RBNode α} {n : ℕ} {parent : RBTree.RBNode.Path α} {v : α},
  y.Balanced RBTree.RBColor.black n →
    RBTree.RBNode.Path.Balanced c₀ n₀ parent RBTree.RBColor.red n →
      RBTree.RBNode.Path.Balanced c₀ n₀ (RBTree.RBNode.Path.left RBTree.RBColor.red parent v y) RBTree.RBColor.black n
-- Mathlib.GroupTheory.ResiduallyFinite
Group.instResiduallyFiniteOfFinite : ∀ {G : Type u_1} [inst : Group G] [Finite G], Group.ResiduallyFinite G
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- An opaque variable. This key only matches with `Key.star`.  -/
Lean.Meta.RefinedDiscrTree.Key.opaque : Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_associator_hom_eq_associator_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V] (D : Type u₃)
  [inst_4 : CategoryTheory.Category.{v₃, u₃} D] [inst_5 : CategoryTheory.MonoidalCategoryStruct D]
  [inst_6 : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] (d d' d'' : D)
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_8 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)],
  (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map
      (CategoryTheory.MonoidalCategoryStruct.associator d d' d'').hom =
    (CategoryTheory.MonoidalCategory.DayConvolution.associator
        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d)
        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d')
        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d'')).hom
-- Lean.Elab.DefView
/-- Syntax of definition body, for checking reuse of `bodySnap`.  -/
Lean.Elab.HeaderProcessedSnapshot.bodyStx : Lean.Elab.HeaderProcessedSnapshot → Lean.Syntax
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
/-- Fibers of `grothendieckProj L` are isomorphic to the projection `proj L X`.  -/
CategoryTheory.CostructuredArrow.ιCompGrothendieckProj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          (X : D) →
            (CategoryTheory.Grothendieck.ι (CategoryTheory.CostructuredArrow.functor L) X).comp
                (CategoryTheory.CostructuredArrow.grothendieckProj L) ≅
              CategoryTheory.CostructuredArrow.proj L X
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Option.getD.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : α) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match some x with
    | some x => h_1 x
    | none => h_2 ()) =
    h_1 x
-- Mathlib.Data.List.Basic
List.forall_map_iff : ∀ {α : Type u} {β : Type v} {l : List α} {p : β → Prop} (f : α → β),
  List.Forall p (List.map f l) ↔ List.Forall (p ∘ f) l
-- Aesop.Tree.Data
Aesop.NormalizationState.isProvenByNormalization : Aesop.NormalizationState → Bool
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- If `f : X → Z` is a Borel measurable map from a standard Borel space to a
countably separated measurable space then the preimage of a set `s` is measurable
if and only if the set is measurable in `Set.range f`.  -/
Measurable.measurableSet_preimage_iff_preimage_val : ∀ {X : Type u_3} {Z : Type u_5} [inst : MeasurableSpace X] [StandardBorelSpace X] [inst_2 : MeasurableSpace Z]
  {f : X → Z} [MeasurableSpace.CountablySeparated ↑(Set.range f)],
  Measurable f → ∀ {s : Set Z}, MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (Subtype.val ⁻¹' s)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates limits, then `F : C ⥤ D` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOfSizeOfOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op] →
            CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- Transports an inverse for `hom` along an equality of 1-simplices `hom = hom'`.
I.e. constructs an inverse for `hom'` from an inverse for `hom`.  -/
SSet.Edge.InvStruct.ofEq : {X : SSet} →
  {x₀ x₁ y₀ y₁ : X.obj (Opposite.op { len := 0 })} →
    {hom : SSet.Edge x₀ x₁} → {hom' : SSet.Edge y₀ y₁} → hom.InvStruct → hom.edge = hom'.edge → hom'.InvStruct
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.variance_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {f : α → ℝ} {g : β → ℝ},
  ProbabilityTheory.IdentDistrib f g μ ν → ProbabilityTheory.variance f μ = ProbabilityTheory.variance g ν
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.instHtmlEvalHtml : ProofWidgets.HtmlEval ProofWidgets.Html
-- Lean.Util.PPExt
Lean.ppConstNameWithInfos : Lean.PPContext → Lean.Name → BaseIO Lean.FormatWithInfos
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance.eq_def : ∀ (pat : String.Slice) (patByte : UInt8) (table : Array ℕ) (ht : table.size ≤ pat.utf8ByteSize)
  (h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i) (guess : ℕ) (hg : guess < table.size),
  String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ pat patByte table ht h guess hg =
    if pat.getUTF8Byte { byteIdx := guess } ⋯ = patByte then ⟨guess + 1, ⋯⟩
    else
      if h₀ : guess = 0 then ⟨0, ⋯⟩
      else
        have this := ⋯;
        String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ pat patByte table ht h table[guess - 1] ⋯
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `lt_tsub_iff_left_of_le` for a weaker statement in a partial order.  -/
lt_tsub_iff_left : ∀ {α : Type u_1} {a b c : α} [inst : LinearOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α],
  a < b - c ↔ c + a < b
-- Mathlib.Data.Set.Pairwise.Lattice
Set.PairwiseDisjoint.subset_of_biUnion_subset_biUnion : ∀ {α : Type u_1} {ι : Type u_2} {f : ι → Set α} {s t : Set ι},
  (s ∪ t).PairwiseDisjoint f → (∀ i ∈ s, (f i).Nonempty) → ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i → s ⊆ t
-- Mathlib.Algebra.Order.Group.PosPart
negPart_eq_neg_inf_zero : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α), a⁻ = -(a ⊓ 0)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited β],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false →
        Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.Const.insertMany t l) k = Std.DTreeMap.Raw.Const.get! t k
-- Mathlib.Combinatorics.Matroid.Map
/-- Map `M : Matroid α` across an equivalence `α ≃ β`  -/
Matroid.mapEquiv : {α : Type u_1} → {β : Type u_2} → Matroid α → α ≃ β → Matroid β
-- Mathlib.Order.Fin.InsertNth
Fin.insertNth.hcongr_6 : ∀ (n n' : ℕ),
  n = n' →
    ∀ (α : Fin (n + 1) → Sort u_1) (α' : Fin (n' + 1) → Sort u_1),
      α ≍ α' →
        ∀ (i : Fin (n + 1)) (i' : Fin (n' + 1)),
          i ≍ i' →
            ∀ (x : α i) (x' : α' i'),
              x ≍ x' →
                ∀ (p : (j : Fin n) → α (i.succAbove j)) (p' : (j : Fin n') → α' (i'.succAbove j)),
                  p ≍ p' → ∀ (j : Fin (n + 1)) (j' : Fin (n' + 1)), j ≍ j' → i.insertNth x p j ≍ i'.insertNth x' p' j'
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidalFunctorComp.eq_1 : ∀ {M : Type u} [inst : AddMonoid M] {N : Type u'} [inst_1 : AddMonoid N] {K : Type u} [inst_2 : AddMonoid K]
  (F : M →+ N) (G : N →+ K),
  CategoryTheory.Discrete.addMonoidalFunctorComp F G =
    CategoryTheory.Iso.refl
      ((CategoryTheory.Discrete.addMonoidalFunctor F).comp (CategoryTheory.Discrete.addMonoidalFunctor G))
-- Mathlib.Tactic.Algebra.Basic
Mathlib.Tactic.Algebra.BaseType.mk.injEq : ∀ {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)}
  {sAlg : Q(Algebra «$R» «$A»)} (r : Q(«$R»)) (x x_1 : Mathlib.Tactic.Ring.ExSum q(«$sR») r),
  (Mathlib.Tactic.Algebra.BaseType.mk r x = Mathlib.Tactic.Algebra.BaseType.mk r x_1) = (x = x_1)
-- Init.Core
/-- Computes `{ a ∈ c | p a }`.  -/
Sep.sep : {α : outParam (Type u)} → {γ : Type v} → [self : Sep α γ] → (α → Prop) → γ → γ
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDF.mk : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  Measurable f →
    (∀ (a : α), ∀ᵐ (b : β) ∂ν a, ProbabilityTheory.IsRatStieltjesPoint f (a, b)) →
      (∀ (a : α) (q : ℚ), MeasureTheory.Integrable (fun b => f (a, b) q) (ν a)) →
        (∀ (a : α) {s : Set β},
            MeasurableSet s → ∀ (q : ℚ), ∫ (b : β) in s, f (a, b) q ∂ν a = (κ a).real (s ×ˢ Set.Iic ↑q)) →
          ProbabilityTheory.IsRatCondKernelCDF f κ ν
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
/-- Morphisms `Y ⟶ M` act on morphisms `Y ⟶ X` via the internal additive action.  -/
CategoryTheory.Hom.instVAddHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {M : C} →
        [inst_2 : CategoryTheory.AddMonObj M] →
          {X : C} → [CategoryTheory.AddModObj M X] → (Y : C) → VAdd (Y ⟶ M) (Y ⟶ X)
-- Mathlib.Probability.Density
ProbabilityTheory.IndepFun.mul_hasPDF' : ∀ {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [inst : Group G]
  {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant]
  {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ],
  MeasureTheory.SigmaFinite (MeasureTheory.Measure.map X ℙ) →
    MeasureTheory.SigmaFinite (MeasureTheory.Measure.map Y ℙ) →
      ProbabilityTheory.IndepFun X Y ℙ → MeasureTheory.HasPDF (X * Y) ℙ μ