mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.InjectivePresentation.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (J : C) →
        autoParam (CategoryTheory.Injective J) CategoryTheory.InjectivePresentation.injective._autoParam →
          (f : X ⟶ J) →
            autoParam (CategoryTheory.Mono f) CategoryTheory.InjectivePresentation.mono._autoParam →
              CategoryTheory.InjectivePresentation X
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.scottHausdorff_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsScott α Set.univ],
  Topology.scottHausdorff α Set.univ ≤ inst_1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} [inst : Inhabited β] {f : Option β → Option β},
  Std.DHashMap.Const.get! (Std.DHashMap.Const.alter m k f) k = (f (Std.DHashMap.Const.get? m k)).get!
-- Mathlib.Data.Nat.ModEq
Nat.ext_div_modEq : ∀ {n a b : ℕ}, a / n = b / n → a ≡ b [MOD n] → a = b
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.tensorObj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : P.IsMonoidalStable] (c c' : CategoryTheory.WideSubcategory P),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj c c').obj =
    CategoryTheory.MonoidalCategoryStruct.tensorObj c.obj c'.obj
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedComm_tmul_algebraMap : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GSemiring ℬ] [inst_9 : DirectSum.GAlgebra R ℬ] (a : DirectSum ι fun i => 𝒜 i) (r : R),
  (TensorProduct.gradedComm R 𝒜 ℬ) (a ⊗ₜ[R] (algebraMap R (DirectSum ι fun i => ℬ i)) r) =
    (algebraMap R (DirectSum ι fun i => ℬ i)) r ⊗ₜ[R] a
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Faithful.div_faithful : ∀ {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 E) [F.Faithful]
  (G : CategoryTheory.Functor D E) [inst_4 : G.Faithful] (obj : C → D) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X)
  (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f),
  (CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).Faithful
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.snd : ∀ {e : ONote} {n : ℕ+} {a : ONote}, (e.oadd n a).NF → a.NF
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.Iterators.Types.ULiftIterator.Monadic.modifyStep.match_1.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (it' : Std.IterM m β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Init.Data.List.Count
List.length_filterMap_eq_countP : ∀ {α : Type u_2} {β : Type u_1} {f : α → Option β} {l : List α},
  (List.filterMap f l).length = List.countP (fun a => (f a).isSome) l
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.Const.get?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (a : α) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.Const.get? ⟨{ size := size, buckets := buckets }, hm⟩ a =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ => Std.DHashMap.Internal.AssocList.get? a buckets[i]
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ico_atTop_atTop : ∀ {α : Type u_1} [inst : Preorder α], Filter.TendstoIxxClass Set.Ico Filter.atTop Filter.atTop
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.setTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → Array α → Sort u_2) (x : ℕ) (x_1 : Array α)
  (h_1 : (x : ℕ) → (x_2 : Array α) → motive [] x x_2)
  (h_2 : (head : α) → (xs : List α) → (acc : Array α) → motive (head :: xs) 0 acc)
  (h_3 : (x : α) → (xs : List α) → (n : ℕ) → (acc : Array α) → motive (x :: xs) n.succ acc),
  (match [], x, x_1 with
    | [], x, x_2 => h_1 x x_2
    | head :: xs, 0, acc => h_2 head xs acc
    | x :: xs, n.succ, acc => h_3 x xs n acc) =
    h_1 x x_1
-- Mathlib.Data.Fin.Basic
/-- `a < b` as natural numbers if and only if `a < b` in `Fin n`.  -/
Fin.val_fin_lt : ∀ {n : ℕ} {a b : Fin n}, ↑a < ↑b ↔ a < b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} {l : List α} {k : α}
  {fallback : Unit}, Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l) k fallback = ()
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- The number of sign changes does not change if we negate.  -/
Polynomial.signVariations_neg : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsOrderedRing R] (P : Polynomial R),
  (-P).signVariations = P.signVariations
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- A refinement morphism `E ⟶ F` induces a functor between the multifork indexing categories.  -/
CategoryTheory.PreOneHypercover.Hom.mapMulticospan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          E.Hom F →
            CategoryTheory.Functor (CategoryTheory.Limits.WalkingMulticospan E.multicospanShape)
              (CategoryTheory.Limits.WalkingMulticospan F.multicospanShape)
-- Mathlib.LinearAlgebra.Dimension.Localization
IsLocalizedModule.finrank_eq : ∀ {R : Type uR} {M : Type uM} {N : Type uN} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f],
  p ≤ nonZeroDivisors R → Module.finrank R N = Module.finrank R M
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
/-- A curried version of the fact that filtered colimits commute with finite limits.  -/
CategoryTheory.Limits.colimitLimitIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] →
              [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] →
                [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] →
                  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
                    CategoryTheory.Limits.colimit (CategoryTheory.Limits.limit F) ≅
                      CategoryTheory.Limits.limit (CategoryTheory.Limits.colimit F.flip)
-- Mathlib.Data.Set.Lattice
Set.iInter₂_union : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : (i : ι) → κ i → Set α) (t : Set α),
  (⋂ i, ⋂ j, s i j) ∪ t = ⋂ i, ⋂ j, s i j ∪ t
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_list : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {ps : Std.Do.PostShape} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
  (inv : Std.Do.Invariant xs β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur ⋯ b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs, property := ⋯ }, init)⦄
      forIn' xs init f ⦃(fun b => inv.1 ({ «prefix» := xs, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- Given two differentiable maps into the same fibers of a Riemannian bundle,
their scalar product is differentiable.  -/
MDifferentiable.inner_bundle : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {B : Type u_3} [inst_3 : TopologicalSpace B]
  [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F]
  {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_8 : (x : B) → NormedAddCommGroup (E x)]
  [inst_9 : (x : B) → InnerProductSpace ℝ (E x)] [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E]
  {EM : Type u_6} [inst_12 : NormedAddCommGroup EM] [inst_13 : NormedSpace ℝ EM] {HM : Type u_7}
  [inst_14 : TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [inst_15 : TopologicalSpace M]
  [inst_16 : ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB 1 F E] {b : M → B} {v w : (x : M) → E (b x)},
  (MDiff fun m => ⟨b m, v m⟩) → (MDiff fun m => ⟨b m, w m⟩) → MDiff fun b_1 => inner ℝ (v b_1) (w b_1)
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.mk.inj : ∀ {J : Type u} {inst : LinearOrder J} {inst_1 : SuccOrder J} {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} {inst_2 : OrderBot J} {val₀ : F.obj (Opposite.op ⊥)} {j : J}
  {val : F.obj (Opposite.op j)}
  {map_zero : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val = val₀}
  {map_succ :
    ∀ (i : J) (hi : i < j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val =
        d.succ i ⋯ ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val)}
  {map_limit :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij).op)) val =
        d.lift i hi
          ⟨fun x =>
            match x with
            | Opposite.op ⟨k, hk⟩ => (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val,
            ⋯⟩}
  {val_1 : F.obj (Opposite.op j)}
  {map_zero_1 : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val_1 = val₀}
  {map_succ_1 :
    ∀ (i : J) (hi : i < j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val_1 =
        d.succ i ⋯ ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val_1)}
  {map_limit_1 :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij).op)) val_1 =
        d.lift i hi
          ⟨fun x =>
            match x with
            | Opposite.op ⟨k, hk⟩ => (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val_1,
            ⋯⟩},
  { val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit } =
      { val := val_1, map_zero := map_zero_1, map_succ := map_succ_1, map_limit := map_limit_1 } →
    val = val_1
-- Mathlib.Topology.Order.IsLUB
IsLUB.mem_lowerBounds_of_tendsto : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : Preorder γ] [inst_4 : TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ},
  AntitoneOn f s → IsLUB s a → Filter.Tendsto f (nhdsWithin a s) (nhds b) → b ∈ lowerBounds (f '' s)
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The canonical isomorphism `G/⊥ ≃+ G`.  -/
QuotientAddGroup.quotientBot : {G : Type u} → [inst : AddGroup G] → G ⧸ ⊥ ≃+ G
-- Init.Data.UInt.Lemmas
UInt64.le_iff_toFin_le : ∀ {a b : UInt64}, a ≤ b ↔ a.toFin ≤ b.toFin
-- Mathlib.LinearAlgebra.Reflection
Module.reflection_inv : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} (h : f x = 2), (Module.reflection h)⁻¹ = Module.reflection h
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.map_ne_one_iff : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S) {x : R},
  f x ≠ 1 ↔ x ≠ 1
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeGPFree_smul_set : ∀ {α : Type u_2} [inst : CommMonoid α] [IsCancelMul α] {s : Set α} {a : α}, ThreeGPFree (a • s) ↔ ThreeGPFree s
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSMulCommClassForall_1 : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [inst : SMul M α] [inst_1 : SMul N β],
  SMulCommClass N Mᵈᵐᵃ (α → β)
-- Init.Data.UInt.Bitwise
USize.right_le_or : ∀ {a b : USize}, b ≤ a ||| b
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.mk.inj : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {E : Type u_2} {inst_1 : NormedAddCommGroup E}
  {inst_2 : NormedSpace 𝕜 E} {inst_3 : CompleteSpace E} {F : Type u_3} {inst_4 : NormedAddCommGroup F}
  {inst_5 : NormedSpace 𝕜 F} {inst_6 : CompleteSpace F} {G : Type u_4} {inst_7 : NormedAddCommGroup G}
  {inst_8 : NormedSpace 𝕜 G} {inst_9 : CompleteSpace G} {leftFun : E → F} {leftDeriv : E →L[𝕜] F} {rightFun : E → G}
  {rightDeriv : E →L[𝕜] G} {pt : E} {hasStrictFDerivAt_leftFun : HasStrictFDerivAt leftFun leftDeriv pt}
  {hasStrictFDerivAt_rightFun : HasStrictFDerivAt rightFun rightDeriv pt} {range_leftDeriv : (↑leftDeriv).range = ⊤}
  {range_rightDeriv : (↑rightDeriv).range = ⊤} {isCompl_ker : IsCompl (↑leftDeriv).ker (↑rightDeriv).ker}
  {leftFun_1 : E → F} {leftDeriv_1 : E →L[𝕜] F} {rightFun_1 : E → G} {rightDeriv_1 : E →L[𝕜] G} {pt_1 : E}
  {hasStrictFDerivAt_leftFun_1 : HasStrictFDerivAt leftFun_1 leftDeriv_1 pt_1}
  {hasStrictFDerivAt_rightFun_1 : HasStrictFDerivAt rightFun_1 rightDeriv_1 pt_1}
  {range_leftDeriv_1 : (↑leftDeriv_1).range = ⊤} {range_rightDeriv_1 : (↑rightDeriv_1).range = ⊤}
  {isCompl_ker_1 : IsCompl (↑leftDeriv_1).ker (↑rightDeriv_1).ker},
  { leftFun := leftFun, leftDeriv := leftDeriv, rightFun := rightFun, rightDeriv := rightDeriv, pt := pt,
        hasStrictFDerivAt_leftFun := hasStrictFDerivAt_leftFun,
        hasStrictFDerivAt_rightFun := hasStrictFDerivAt_rightFun, range_leftDeriv := range_leftDeriv,
        range_rightDeriv := range_rightDeriv, isCompl_ker := isCompl_ker } =
      { leftFun := leftFun_1, leftDeriv := leftDeriv_1, rightFun := rightFun_1, rightDeriv := rightDeriv_1, pt := pt_1,
        hasStrictFDerivAt_leftFun := hasStrictFDerivAt_leftFun_1,
        hasStrictFDerivAt_rightFun := hasStrictFDerivAt_rightFun_1, range_leftDeriv := range_leftDeriv_1,
        range_rightDeriv := range_rightDeriv_1, isCompl_ker := isCompl_ker_1 } →
    leftFun = leftFun_1 ∧ leftDeriv = leftDeriv_1 ∧ rightFun = rightFun_1 ∧ rightDeriv = rightDeriv_1 ∧ pt = pt_1
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.instTensorAddUnit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMonObj.instTensorAddUnit =
    { zero := CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C),
      add :=
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom,
      zero_add := ⋯, add_zero := ⋯, add_assoc := ⋯ }
-- Mathlib.Control.ULiftable
/-- map function that moves up universes  -/
ULiftable.upMap : {F : Type u₀ → Type u₁} →
  {G : Type (max u₀ v₀) → Type v₁} →
    [ULiftable F G] → [Functor G] → {α : Type u₀} → {β : Type (max u₀ v₀)} → (α → β) → F α → G β
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          (motive : aig.BinaryRefVec w → Sort u_1) →
            (input : aig.BinaryRefVec w) → ((lhs rhs : aig.RefVec w) → motive { lhs := lhs, rhs := rhs }) → motive input
-- Lean.Data.Json.Printer
Lean.Json.render : Lean.Json → Std.Format
-- Mathlib.Data.Multiset.Sum
Multiset.disjSum_zero : ∀ {α : Type u_1} {β : Type u_2} (s : Multiset α), s.disjSum 0 = Multiset.map Sum.inl s
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [MeasureTheory.SigmaFinite μ],
  MeasureTheory.VectorMeasure.AbsolutelyContinuous s μ.toENNRealVectorMeasure → μ.withDensityᵥ (s.rnDeriv μ) = s
-- Lean.Meta.Tactic.Grind.Arith.ModelUtil
/-- Returns `true` if `e` should be treated as an interpreted value by the arithmetic modules.
 -/
Lean.Meta.Grind.Arith.isInterpretedTerm : Lean.Expr → Bool
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.valuation_uniformizingPolynomial_lt_one : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [inst_2 : v.IsNontrivial] [inst_3 : Valuation.IsTrivialOn K v] (hle : v RatFunc.X ≤ 1),
  v ↑(RatFunc.uniformizingPolynomial hle) < 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a},
  p ∈ l → Std.Internal.List.containsKey p.fst l = true
-- Mathlib.Algebra.Notation.Support
Function.support_prodMk' : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N] (f : ι → M × N),
  Function.support f = (Function.support fun x => (f x).1) ∪ Function.support fun x => (f x).2
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.addUnits.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M),
  S.addUnits =
    { toAddSubmonoid := AddSubmonoid.comap (AddUnits.coeHom M) S ⊓ -AddSubmonoid.comap (AddUnits.coeHom M) S,
      neg_mem' := ⋯ }
-- Mathlib.Data.Set.Lattice.Image
Set.iUnion_prod_of_monotone : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SemilatticeSup α] {s : α → Set β} {t : α → Set γ},
  Monotone s → Monotone t → ⋃ x, s x ×ˢ t x = (⋃ x, s x) ×ˢ ⋃ x, t x
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] (f : β → α) {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂)
  (h₁ : s₁.Nonempty), s₂.inf' ⋯ f ≤ s₁.inf' h₁ f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.div₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β] [TopologicalSpace.MetrizableSpace β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (f / g) μ
-- Mathlib.Order.Filter.Cofinite
Set.Finite.compl_mem_cofinite : ∀ {α : Type u_2} {s : Set α}, s.Finite → sᶜ ∈ Filter.cofinite
-- Lean.Parser.Syntax
Lean.Parser.precedenceParser.parenthesizer : optParam ℕ 0 → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_eraseKey_eq_of_beq_minKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α}
  {he : (Std.Internal.List.eraseKey k l).isEmpty = false},
  (k == Std.Internal.List.minKey l ⋯) = false →
    Std.Internal.List.minKey (Std.Internal.List.eraseKey k l) he = Std.Internal.List.minKey l ⋯
-- Mathlib.Order.Hom.Basic
OrderEmbedding.coe_ofStrictMono : ∀ {α : Type u_6} {β : Type u_7} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} (h : StrictMono f),
  ⇑(OrderEmbedding.ofStrictMono f h) = f
-- Mathlib.Topology.Category.TopPair
/-- The unique morphism (X, ∅) ⟶ (X, A) that is the identity on X.  -/
TopPair.j : (X : TopPair) → TopPair.incl.obj TopPair.fst ⟶ X
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
_private.Mathlib.NumberTheory.EllipticDivisibilitySequence.0.complEDS'.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match n.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_3 n
-- Mathlib.Probability.Independence.Conditional
/-- Two sets are conditionally independent if the two measurable space structures they generate are
conditionally independent. For a set `s`, the generated measurable space structure has measurable
sets `∅, s, sᶜ, univ`.
See `ProbabilityTheory.condIndepSet_iff`.  -/
ProbabilityTheory.CondIndepSet : {Ω : Type u_1} →
  (m' : MeasurableSpace Ω) →
    {mΩ : MeasurableSpace Ω} →
      [StandardBorelSpace Ω] →
        m' ≤ mΩ →
          Set Ω →
            Set Ω →
              (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.CondIndepSet._auto_1) →
                [MeasureTheory.IsFiniteMeasure μ] → Prop
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.cyclesOpNatIso_hom_app : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] [inst_2 : CategoryTheory.CategoryWithHomology V] (i : ι)
  (X : (HomologicalComplex V c)ᵒᵖ),
  (HomologicalComplex.cyclesOpNatIso V c i).hom.app X = ((Opposite.unop X).cyclesOpIso i).hom
-- Std.Http.Data.Chunk
Std.Http.Chunk.instReprExtensionValue : Repr Std.Http.Chunk.ExtensionValue
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.instInv : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → Inv (N ⋊[φ] G)
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_comp_map_lid_symm : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {N' : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid N']
  [inst_6 : Module R N'] (f : N →ₗ[R] N'),
  ↑(TensorProduct.assoc R R M N') ∘ₗ TensorProduct.map (↑(TensorProduct.lid R M).symm) f =
    TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f) ∘ₗ
      ↑(TensorProduct.lid R (TensorProduct R M N)).symm
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.coe_iSup_of_directed : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} [Nonempty ι] {S : ι → Submonoid M},
  Directed (fun x1 x2 => x1 ≤ x2) S → ↑(⨆ i, S i) = ⋃ i, ↑(S i)
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sInf_inv : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : Group M] [MulLeftMono M] [MulRightMono M] (s : Set M),
  sInf s⁻¹ = (sSup s)⁻¹
-- Mathlib.Algebra.Group.Opposite
AddOpposite.unop_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : αᵃᵒᵖ) (b : β), AddOpposite.unop (a ^ b) = AddOpposite.unop a ^ b
-- Mathlib.Algebra.Ring.Ext
AddMonoidWithOne.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : AddMonoidWithOne R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ One.one = One.one
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsupp_apply : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : Semiring S] [inst_6 : Algebra R S] [inst_7 : Module S M] [inst_8 : IsScalarTower R S M] (f : ι →₀ M)
  (g : κ →₀ N) (i : ι) (k : κ), ((finsuppTensorFinsupp R S M N ι κ) (f ⊗ₜ[R] g)) (i, k) = f i ⊗ₜ[R] g k