mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.ringEquivOfRingEquiv_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {T : Submonoid P}
  {Q : Type u_4} [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q] {j : R ≃+* P}
  (H : Submonoid.map j.toMonoidHom M = T) (x : R),
  (IsLocalization.ringEquivOfRingEquiv S Q j H) ((algebraMap R S) x) = (algebraMap P Q) (j x)
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHAddOffset_2 : HAdd Std.Time.Timestamp Std.Time.Hour.Offset Std.Time.Timestamp
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.iSup_ringCon : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R] {ι : Type u_2} (I : ι → TwoSidedIdeal R),
  (⨆ i, I i).ringCon = ⨆ i, (I i).ringCon
-- Mathlib.CategoryTheory.Generator.Presheaf
/-- The bijection `(Presheaf.freeYoneda X M ⟶ F) ≃ (M ⟶ F.obj (op X))`.  -/
CategoryTheory.Presheaf.freeYonedaHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        [inst_2 : CategoryTheory.Limits.HasCoproducts A] →
          {X : C} →
            {M : A} →
              {F : CategoryTheory.Functor Cᵒᵖ A} →
                (CategoryTheory.Presheaf.freeYoneda X M ⟶ F) ≃ (M ⟶ F.obj (Opposite.op X))
-- Mathlib.Order.Basic
/-- Given a relation `R` on `β` and a function `f : α → β`, the preimage relation on `α` is defined
by `x ≤ y ↔ f x ≤ f y`. It is the unique relation on `α` making `f` a `RelEmbedding` (assuming `f`
is injective).  -/
Order.Preimage : {α : Type u_2} → {β : Type u_3} → (α → β) → (β → β → Prop) → α → α → Prop
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isOrtho_flip : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : CommSemiring R₁]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R₁ M₁] [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  {I₁ I₁' : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M} {x y : M₁}, B.IsOrtho x y ↔ B.flip.IsOrtho y x
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.instSliceableImplRoiSlice : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      Std.Roi.Sliceable (Std.DTreeMap.Internal.Impl α fun x => β) α (Std.DTreeMap.Internal.Const.RoiSlice α β)
-- Init.Data.SInt.Basic
Int8.ofUInt8.injEq : ∀ (toUInt8 toUInt8_1 : UInt8), ({ toUInt8 := toUInt8 } = { toUInt8 := toUInt8_1 }) = (toUInt8 = toUInt8_1)
-- Mathlib.Algebra.Group.Prod
Prod.instMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N],
  Prod.instMonoid =
    { toSemigroup := Prod.instSemigroup, toOne := Prod.instMulOneClass.toOne, one_mul := ⋯, mul_one := ⋯,
      npow := fun z a => (NPow.npow z a.1, NPow.npow z a.2), npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.dep_of_not_indep : ∀ {α : Type u_1} {M : Matroid α} {D : Set α},
  ¬M.Indep D → autoParam (D ⊆ M.E) Matroid.dep_of_not_indep._auto_1 → M.Dep D
-- Mathlib.CategoryTheory.Functor.OfSequence
_private.Mathlib.CategoryTheory.Functor.OfSequence.0.CategoryTheory.Functor.OfSequence.map.match_3.eq_5 : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  (motive : (x : ℕ → C) → ((n : ℕ) → x n ⟶ x (n + 1)) → ℕ → ℕ → Sort u_3) (x : ℕ → C) (f : (n : ℕ) → x n ⟶ x (n + 1))
  (k l : ℕ) (h_1 : (x : ℕ → C) → (x_1 : (n : ℕ) → x n ⟶ x (n + 1)) → motive x x_1 0 0)
  (h_2 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → motive x f 0 1)
  (h_3 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → (l : ℕ) → motive x f 0 l.succ)
  (h_4 : (x : ℕ → C) → (x_1 : (n : ℕ) → x n ⟶ x (n + 1)) → (n : ℕ) → motive x x_1 n.succ 0)
  (h_5 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → (k l : ℕ) → motive x f k.succ l.succ),
  (match x, f, k.succ, l.succ with
    | x, x_1, 0, 0 => h_1 x x_1
    | x, f, 0, 1 => h_2 x f
    | x, f, 0, l.succ => h_3 x f l
    | x, x_1, n.succ, 0 => h_4 x x_1 n
    | x, f, k.succ, l.succ => h_5 x f k l) =
    h_5 x f k l
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.homOfLE_app_hom_apply_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} {N₁ N₂ : M.Submodule} (hle : N₁ ≤ N₂) (X : Cᵒᵖ)
  (a : ↑(N₁.toPresheafOfModules.presheaf.obj X)),
  ↑((ModuleCat.Hom.hom ((PresheafOfModules.Submodule.homOfLE hle).app X)) a) = ↑a
-- Lean.Language.Basic
/-- Option for printing end position of each message in addition to start position. Used for testing
message ranges in the test suite.  -/
Lean.Language.printMessageEndPos : Lean.Option Bool
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.valueGroup₀_equiv_extensionValuation.eq_1 : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀],
  Valued.valueGroup₀_equiv_extensionValuation = MulEquiv.ofBijective Valued.valueGroup₀_hom_extensionValuation ⋯
-- Mathlib.RingTheory.IdealFilter.Topology
/-- Under `[F.IsUniform]`, the ring filter basis obtained from `addGroupFilterBasis`.  -/
IdealFilter.ringFilterBasis : {A : Type u_1} → [inst : Ring A] → {F : IdealFilter A} → [F.IsUniform] → RingFilterBasis A
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
GaloisConnection.l_ciSup_of_directed : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α]
  [inst_1 : ConditionallyCompletePartialOrderSup β] [Nonempty ι] {l : α → β} {u : β → α},
  GaloisConnection l u →
    ∀ {f : ι → α}, Directed (fun x1 x2 => x1 ≤ x2) f → BddAbove (Set.range f) → l (⨆ i, f i) = ⨆ i, l (f i)
-- Mathlib.Order.Bounds.Basic
mem_lowerBounds : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, a ∈ lowerBounds s ↔ ∀ x ∈ s, a ≤ x
-- Init.Sym.Simp.SimprocDSL
/-- Post-processing simproc chain.  -/
Lean.Parser.Command.symSimpFieldPost : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  {x y : CategoryTheory.SimplicialObject.Homotopy f g},
  @CategoryTheory.SimplicialObject.Homotopy.h C inst X Y f g x =
      @CategoryTheory.SimplicialObject.Homotopy.h C inst X Y f g y →
    x = y
-- Plausible.Shrinkable
_private.Plausible.Shrinkable.0.Plausible.Nat.shrink.eq_def : ∀ (n : ℕ),
  Plausible.Nat.shrink n =
    if 0 < n then
      have m := n / 2;
      m :: Plausible.Nat.shrink m
    else []
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  [inst_2 : CategoryTheory.IsSplitEpi f] {c : CategoryTheory.Limits.KernelFork f} (i : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).inl = CategoryTheory.Limits.Fork.ι c
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.preUnitIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : D ≌ C),
  CategoryTheory.Grothendieck.preUnitIso F G =
    (CategoryTheory.Grothendieck.preNatIso (G.functor.comp F) G.unitIso.symm).symm
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- The tangent bundle to a manifold, as a Sigma type. Defined in terms of
`Bundle.TotalSpace` to be able to put a suitable topology on it.  -/
TangentBundle : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H →
                (M : Type u_4) → [inst : TopologicalSpace M] → [ChartedSpace H M] → Type (max u_4 u_2)
-- Mathlib.Algebra.Group.End
Equiv.Perm.ofSubtype_apply_mem_iff_mem : ∀ {α : Type u_4} {p : α → Prop} [inst : DecidablePred p] (f : Equiv.Perm (Subtype p)) (x : α),
  p ((Equiv.Perm.ofSubtype f) x) ↔ p x
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i j : ι} {f : Π₀ (i : ι), β i},
  (DFinsupp.erase i f) j = if j = i then 0 else f j
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The initial factorisation is an initial object  -/
CategoryTheory.Factorisation.IsInitial_initial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Limits.IsInitial CategoryTheory.Factorisation.initial
-- Init.Data.Sum.Lemmas
Sum.LiftRel.swap : ∀ {α : Type u_1} {α_1 : Type u_2} {r : α → α_1 → Prop} {β : Type u_3} {β_1 : Type u_4} {s : β → β_1 → Prop} {x : α ⊕ β}
  {y : α_1 ⊕ β_1}, Sum.LiftRel r s x y → Sum.LiftRel s r x.swap y.swap
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn_6.eq : ∀ {motive_1 : Lean.Elab.Term.Do.Code → Sort u}
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u}
  {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u}
  (t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) (F_1 : (t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_1 t → motive_2 t)
  (F_3 : (t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_2 t → motive_3 t)
  (F_4 : (t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_4 t → motive_5 t)
  (F_6 : (t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_5 t → motive_6 t)
  (F_7 : (t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_6 t → motive_7 t),
  Lean.Elab.Term.Do.Code.brecOn_6 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_7 t (Lean.Elab.Term.Do.Code.brecOn_6.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.isThetaTVS_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x →
    Topology.IsInducing ⇑f' → (fun x_1 => f x_1 - f x) =Θ[𝕜; nhdsWithin x s] fun x_1 => x_1 - x
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.map.eq_1 : ∀ {m : Type w → Type w'} [inst : Functor m] {α β : Type w} (f : α → β) (x : Std.Iterators.PostconditionT m α),
  Std.Iterators.PostconditionT.map f x =
    { Property := fun b => ∃ a, f ↑a = b, operation := (fun a => ⟨f ↑a, ⋯⟩) <$> x.operation }
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.instInhabitedQuotient : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (p : Submodule R M) → Inhabited (M ⧸ p)
-- Mathlib.Computability.NFA
NFA.acceptsFrom_union : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) {S T : Set σ}, M.acceptsFrom (S ∪ T) = M.acceptsFrom S + M.acceptsFrom T
-- Mathlib.Data.Ordmap.Ordnode
/-- O(m + n). Is every element of `t₁` not equivalent to any element of `t₂`?

```
disjoint {1, 3} {2, 4} = tt
disjoint {1, 2} {2, 4} = ff
```  -/
Ordnode.disjoint : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → Ordnode α → Ordnode α → Bool
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instAdd : {X : AlgebraicGeometry.Scheme} → Add X.IdealSheafData
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- The fudge factor that appears in the formula for the volume of `convexBodyLT'`.  -/
NumberField.mixedEmbedding.convexBodyLT'Factor : (K : Type u_1) → [inst : Field K] → [NumberField K] → NNReal
-- Init.Data.List.Sublist
List.drop_subset_drop_left : ∀ {α : Type u_1} (l : List α) {i j : ℕ}, i ≤ j → List.drop j l ⊆ List.drop i l
-- Init.System.IO
/-- A monad that can have side effects on the external world or throw exceptions of type `ε`.

`BaseIO` is a version of this monad that cannot throw exceptions. `IO` sets the exception type to
`IO.Error`.
 -/
EIO : Type → Type → Type
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.sumIDeriv_apply_of_le : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R} {n : ℕ},
  p.natDegree ≤ n → Polynomial.sumIDeriv p = ∑ i ∈ Finset.range (n + 1), (⇑Polynomial.derivative)^[i] p
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- A function on non-zero vectors which is independent of scale, descends to a function on the
projectivization.  -/
Projectivization.lift : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {α : Type u_3} →
            (f : { v // v ≠ 0 } → α) →
              (∀ (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b) → Projectivization K V → α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_whiskerLeft : ∀ {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 : Type u₄} {Y : Type u₅} {Z : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} Z] (U : CategoryTheory.Functor X Y) {V W : CategoryTheory.Functor Y Z}
  (α : V ⟶ W),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map (U.whiskerLeft α) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U V).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map α)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U))
        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U W).inv)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableWithinAt.inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_5} [inst_3 : NormedRing R] [HasSummableGeomSeries R]
  [inst_5 : NormedAlgebra 𝕜 R] {h : E → R} {z : E} {S : Set E},
  DifferentiableWithinAt 𝕜 h S z → IsUnit (h z) → DifferentiableWithinAt 𝕜 (fun x => Ring.inverse (h x)) S z
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.inv_inf : ∀ {G : Type u_2} [inst : Group G] (S T : Submonoid G), (S ⊓ T)⁻¹ = S⁻¹ ⊓ T⁻¹
-- Mathlib.Order.DirSupClosed
/-- A predicate for a set which is inaccessible by directed suprema of nonempty sets.
This is the complement of a `DirSupClosed` set.  -/
DirSupInacc : {α : Type u_1} → [Preorder α] → Set α → Prop
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
  [inst_7 :
    ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj
          X₃).HasMap
      r],
  CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃ =
    CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.setIntegral_restrict : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : β → E} {a : α} {s : Set β}
  (hs : MeasurableSet s) (t : Set β), ∫ (x : β) in t, f x ∂(κ.restrict hs) a = ∫ (x : β) in t ∩ s, f x ∂κ a
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Lean.MVarId.introsClean.eqImpOfIffImp : Lean.MVarId → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.LinearAlgebra.Prod
LinearMap.disjoint_inl_inr : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Disjoint (LinearMap.inl R M M₂).range (LinearMap.inr R M M₂).range
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R),
  PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑I) = I.radical
-- Mathlib.FieldTheory.Galois.Basic
AlgEquiv.restrictNormalHom.congr_simp : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} [inst_1 : Field K₁] [inst_2 : Algebra F K₁] (E : Type u_6)
  [inst_3 : Field E] [inst_4 : Algebra F E] [inst_5 : Algebra E K₁] [inst_6 : IsScalarTower F E K₁]
  [inst_7 : Normal F E], AlgEquiv.restrictNormalHom E = AlgEquiv.restrictNormalHom E
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli_comp_one_add_X : ∀ (n : ℕ), (Polynomial.bernoulli n).comp (1 + Polynomial.X) = Polynomial.bernoulli n + n • Polynomial.X ^ (n - 1)
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_eq_sub : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Ω → ℝ},
  MeasureTheory.MemLp X 2 μ → ProbabilityTheory.variance X μ = ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.right_of_union : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s t : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f (s ∪ t) μ → MeasureTheory.IntegrableOn f t μ
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_insertListConst : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)},
  Std.Internal.List.DistinctKeys l →
    List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert →
      (∀ (a : α), Std.Internal.List.containsKey a l = true → (List.map Prod.fst toInsert).contains a = false) →
        (Std.Internal.List.insertListConst l toInsert).length = l.length + toInsert.length
-- Mathlib.Order.Interval.Finset.Basic
Finset.subset_Iic_sup_id : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : OrderBot α] (s : Finset α),
  s ⊆ Finset.Iic (s.sup id)
-- Init.Data.Vector.Lemmas
Vector.toList_inj : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n}, xs.toList = ys.toList ↔ xs = ys
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_mkNormedAddGroupHom' : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (f : V₁ →+ V₂)
  (C : NNReal) (hC : ∀ (x : V₁), ‖f x‖₊ ≤ C * ‖x‖₊), ⇑(f.mkNormedAddGroupHom' C hC) = ⇑f
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.map_relationOfHasCoeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀] (r : σ),
  (MvPolynomial.map (algebraMap R₀ R)) (Algebra.Presentation.relationOfHasCoeffs R₀ r) = P.relation r
-- Lean.Elab.Command
Lean.Elab.Command.Context.cmdPos : Lean.Elab.Command.Context → String.Pos.Raw
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.mulOneClass.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : MulOneClass M₂] (f : M₁ → M₂)
  (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y),
  Function.Injective.mulOneClass f hf one mul = { toOne := inst_1, toMul := inst, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.map_equiv_eq_comap_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (f : α ≃o β)
  (L : BooleanSubalgebra α),
  BooleanSubalgebra.map
      (let __src := { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
      L =
    BooleanSubalgebra.comap
      (let __src := { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
      L
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.forget_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X Y : G.Coalgebra}
  (f : X ⟶ Y), G.forget.map f = f.f
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousAt.rpow_const : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {x : α} {p : ℝ},
  ContinuousAt f x → f x ≠ 0 ∨ 0 ≤ p → ContinuousAt (fun x => f x ^ p) x
-- Mathlib.Probability.Process.Adapted
MeasureTheory.Adapted.smul : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → MeasurableSpace (β i)] {u : (i : ι) → Ω → β i} {𝕂 : Type u_4}
  [inst_2 : MeasurableSpace 𝕂] [inst_3 : (i : ι) → SMul 𝕂 (β i)] [∀ (i : ι), MeasurableSMul 𝕂 (β i)] (c : 𝕂),
  MeasureTheory.Adapted f u → MeasureTheory.Adapted f (c • u)
-- Mathlib.RingTheory.Jacobson.Radical
Module.jacobson_pi_le : ∀ (R : Type u_1) [inst : Ring R] {ι : Type u_6} (M : ι → Type u_5) [inst_1 : (i : ι) → AddCommGroup (M i)]
  [inst_2 : (i : ι) → Module R (M i)],
  Module.jacobson R ((i : ι) → M i) ≤ Submodule.pi Set.univ fun x => Module.jacobson R (M x)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_eq_isSome_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = t[a]?.isSome
-- Mathlib.Order.WellFounded
WellFounded.wellFoundedGT_iff_exists_maximal : ∀ {α : Type u_1} [inst : Preorder α], WellFoundedGT α ↔ ∀ (s : Set α), s.Nonempty → ∃ m, Maximal (fun x => x ∈ s) m
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
/-- If a closed set has a closed thickening with finite measure, then the measure of its closed
`r`-thickenings converge to its measure as `r` tends to `0`.  -/
tendsto_measure_cthickening_of_isClosed : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  {μ : MeasureTheory.Measure α} {s : Set α},
  (∃ R > 0, μ (Metric.cthickening R s) ≠ ⊤) →
    IsClosed s → Filter.Tendsto (fun r => μ (Metric.cthickening r s)) (nhds 0) (nhds (μ s))
-- Init.Data.Nat.Basic
Nat.succ_succ_ne_one : ∀ (a : ℕ), a.succ.succ ≠ 1