mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.homCategory.ext : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} (α β : F ⟶ G),
  α.toNatTrans = β.toNatTrans → α = β
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.PositivityExt.mk.inj : ∀
  {eval eval_1 :
    {u : Lean.Level} →
      {α : Q(Type u)} →
        (zα : Q(Zero «$α»)) →
          (pα? : Option Q(PartialOrder «$α»)) →
            (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?)},
  { eval := eval } = { eval := eval_1 } → eval = eval_1
-- Mathlib.Data.Fin.Basic
Fin.val_sub_lt_of_lt_of_le : ∀ {n m : ℕ} {a b : Fin n}, ↑a < m → b ≤ a → ↑(a - b) < m
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.leftUnitor_hom_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitor α).hom.τr = (CategoryTheory.Bicategory.rightUnitor α.r).inv
-- Mathlib.Order.SuccPred.Basic
PredOrder.ext : ∀ {α : Type u_3} {inst : Preorder α} {x y : PredOrder α}, PredOrder.pred = PredOrder.pred → x = y
-- Lean.Parser.Extension
Lean.Parser.parserOfStack : ℕ → optParam ℕ 0 → Lean.Parser.Parser
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal_empty : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] (μ : (i : δ) → MeasureTheory.Measure (X i))
  [inst_1 : DecidableEq δ] (f : ((i : δ) → X i) → ENNReal), ∫⋯∫⁻_∅, f ∂μ = f
-- Lean.Environment
/-- Assuming `Lean.addDecl` has been run for the constant to be added on the async environment branch,
commits the full constant info from that call to the main environment, (asynchronously) waits for
the final kernel environment resulting from the `addDecl` call, and commits it to the main branch as
well, unblocking kernel additions there. All `commitConst` preconditions apply.
 -/
Lean.Environment.AddConstAsyncResult.commitCheckEnv : Lean.Environment.AddConstAsyncResult → Lean.Environment → IO Unit
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.contains_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  (Std.DHashMap.Const.alter m k f).contains k = (f (Std.DHashMap.Const.get? m k)).isSome
-- Batteries.Data.Array.Merge
/-- `O(|xs|)`. Deduplicate a sorted array. The array must be sorted with to an order which agrees with
`==`, i.e. whenever `x == y` then `compare x y == .eq`.
 -/
Array.dedupSorted : {α : Type u_1} → [eq : BEq α] → Array α → Array α
-- Lean.MonadEnv
Lean.matchConstInduct : {m : Type → Type} →
  {α : Type} →
    [Monad m] → [Lean.MonadEnv m] → Lean.Expr → (Unit → m α) → (Lean.InductiveVal → List Lean.Level → m α) → m α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} {f : β k → β k}, (t.modify k f).getKey? k = if k ∈ t then some k else none
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsAddTorsion.quotient_iff`.

---

The image of a quotient is torsion iff the additive group is torsion.  -/
AddIsTorsion.quotient_iff : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] {N : AddSubgroup G} [inst_1 : AddGroup H] {f : G →+ H},
  Function.Surjective ⇑f → N = f.ker → IsAddTorsion ↥N → (IsAddTorsion H ↔ IsAddTorsion G)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Sheaf J RingCat}
  (F : CategoryTheory.Functor D (SheafOfModules R))
  [∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (SheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj.obj X)))).sections]
  [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrpCat], CategoryTheory.Limits.HasLimit F
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.IsPartition.nonempty_boxes : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I}, π.IsPartition → π.boxes.Nonempty
-- Init.Data.String.Basic
/-- Given a position in `s`, obtain the corresponding position in `s.slice! p₀ p₁ h`, or panic if
taking `s.slice! p₀ p₁` already panicked or if the position is not between `p₀` and `p₁`.
 -/
String.Slice.Pos.slice! : {s : String.Slice} → s.Pos → (p₀ p₁ : s.Pos) → (s.slice! p₀ p₁).Pos
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instSMulPosMono : ∀ {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [inst : Semiring α] [inst_1 : Preorder α]
  [inst_2 : (i : ι) → AddCommMonoid (β i)] [inst_3 : (i : ι) → Preorder (β i)] [inst_4 : (i : ι) → Module α (β i)]
  [∀ (i : ι), SMulPosMono α (β i)], SMulPosMono α (Π₀ (i : ι), β i)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.mk.inj : ∀ {M : Type u_10} {N : Type u_11} {inst : AddZero M} {inst_1 : AddZero N} {toZeroHom : ZeroHom M N}
  {map_add' : ∀ (x y : M), toZeroHom.toFun (x + y) = toZeroHom.toFun x + toZeroHom.toFun y} {toZeroHom_1 : ZeroHom M N}
  {map_add'_1 : ∀ (x y : M), toZeroHom_1.toFun (x + y) = toZeroHom_1.toFun x + toZeroHom_1.toFun y},
  { toZeroHom := toZeroHom, map_add' := map_add' } = { toZeroHom := toZeroHom_1, map_add' := map_add'_1 } →
    toZeroHom = toZeroHom_1
-- Aesop.Rule
Aesop.instInhabitedSafety.default : Aesop.Safety
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
/-- Given two morphisms `f` and `g` in `A.toFunctor ⟶ F₂`, if `φ : G ⟶ A.toFunctor`
is such that `φ ≫ f = φ ≫ g`, then this is the lifted morphism
`G ⟶ (Subfunctor.equalizer f g).toFunctor`. This is part of the universal
property of the equalizer that is satisfied by
the functor `(Subfunctor.equalizer f g).toFunctor`.  -/
CategoryTheory.Subfunctor.equalizer.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F₁ F₂ : CategoryTheory.Functor C (Type w)} →
      {A : CategoryTheory.Subfunctor F₁} →
        (f g : A.toFunctor ⟶ F₂) →
          {G : CategoryTheory.Functor C (Type w)} →
            (φ : G ⟶ A.toFunctor) →
              CategoryTheory.CategoryStruct.comp φ f = CategoryTheory.CategoryStruct.comp φ g →
                (G ⟶ (CategoryTheory.Subfunctor.equalizer f g).toFunctor)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] (a : A) (x : TensorProduct R M N),
  a • x = (LinearMap.rTensor N ((Algebra.lsmul R R M) a)) x
-- Mathlib.Topology.Algebra.Group.Units
ContinuousMulEquiv.piUnits.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : (i : ι) → TopologicalSpace (M i)],
  ContinuousMulEquiv.piUnits = { toMulEquiv := MulEquiv.piUnits, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg_of_not_isPrime : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S],
  ¬q.IsPrime → q.inertiaDeg R = 0
-- Mathlib.Algebra.Lie.UniversalEnveloping
/-- The quotient map from the tensor algebra to the universal enveloping algebra as a morphism of
associative algebras.  -/
UniversalEnvelopingAlgebra.mkAlgHom : (R : Type u₁) →
  (L : Type u₂) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → TensorAlgebra R L →ₐ[R] UniversalEnvelopingAlgebra R L
-- Mathlib.RingTheory.Multiplicity
emultiplicity_pos_of_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a ∣ b → 0 < emultiplicity a b
-- Lean.Elab.Command.Scope
/-- The component of the `namespace` or `section` that this scope is associated to.
For example, `section a.b.c` and `namespace a.b.c` each create three scopes with headers
named `a`, `b`, and `c`.
This is used for checking the `end` command. The "base scope" has `""` as its header.
 -/
Lean.Elab.Command.Scope.header : Lean.Elab.Command.Scope → String
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_associator_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.LaxFunctor B C} (x_3 : CategoryTheory.LaxFunctor B C) (η : x ⟶ x_1) (θ : x_1 ⟶ x_2)
  (ι : x_2 ⟶ x_3) (a : B),
  (CategoryTheory.Bicategory.associator η θ ι).hom.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (i₁ i₁' : I₁) (i₂ : I₂),
  (((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).d i₁ i₁').f i₂ = (F.map (K₁.d i₁ i₁')).app (K₂.X i₂)
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {E : Type u_2}
  {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : Ω → E}
  [inst_3 : NormedSpace ℝ E] {Y : Ω → E},
  AEMeasurable X P →
    AEMeasurable Y P →
      ProbabilityTheory.IndepFun X Y P →
        MeasureTheory.charFunDual (MeasureTheory.Measure.map (X + Y) P) =
          MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) *
            MeasureTheory.charFunDual (MeasureTheory.Measure.map Y P)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both summable, then the sum of the
`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) is
`∑' n, f n + ∑' n, g n`.  -/
tsum_int_rec : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f g : ℕ → M},
  Summable f → Summable g → ∑' (n : ℤ), Int.rec f g n = ∑' (n : ℕ), f n + ∑' (n : ℕ), g n
-- Mathlib.Topology.MetricSpace.Closeds
/-- **Alias** of `TopologicalSpace.NonemptyCompacts.isometry_toCloseds`.

---

`NonemptyCompacts.toCloseds` is an isometry  -/
EMetric.NonemptyCompacts.isometry_toCloseds : ∀ {α : Type u_1} [inst : EMetricSpace α], Isometry TopologicalSpace.NonemptyCompacts.toCloseds
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The functor sending `(X, n)` to the coproduct of copies of `X` indexed by `n`.  -/
CategoryTheory.Limits.sigmaConst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] → CategoryTheory.Functor C (CategoryTheory.Functor (Type w) C)
-- Batteries.Recycling.RBTree.Basic
/-- Fold a monadic function on the values from left to right (in increasing order).  -/
RBTree.RBNode.foldlM : {m : Type u_1 → Type u_2} → {σ : Type u_1} → {α : Type u_3} → [Monad m] → (σ → α → m σ) → σ → RBTree.RBNode α → m σ
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.image_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y),
  ⇑h '' ⇑h ⁻¹' s = s
-- Lean.Data.Json.FromToJson.Basic
/-- Note that `USize`s and `UInt64`s are stored as strings because JavaScript
cannot represent 64-bit numbers.  -/
Lean.bignumFromJson? : Lean.Json → Except String ℕ
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.get_rowLens : ∀ {μ : YoungDiagram} {i : ℕ} {h : i < μ.rowLens.length}, μ.rowLens[i] = μ.rowLen i
-- Mathlib.Algebra.Category.ModuleCat.Injective
Module.injective_object_of_injective_module : ∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inj : Module.Injective R M], CategoryTheory.Injective (ModuleCat.of R M)
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (x : CategoryTheory.Abelian.Ext X Y n), R.extEquivCohomologyClass (-x) = -R.extEquivCohomologyClass x
-- Mathlib.Algebra.Group.Pointwise.Set.Small
small_div : ∀ {α : Type u_1} (s t : Set α) [inst : Div α] [Small.{u, u_1} ↑s] [Small.{u, u_1} ↑t], Small.{u, u_1} ↑(s / t)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁_map_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X₁ Y₁ : C}
  (φ : X₁ ⟶ Y₁) (X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁ C).map φ).app X₂).app X₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ X₃ X₁).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₃ φ))
        (CategoryTheory.MonoidalCategoryStruct.associator X₂ X₃ Y₁).inv)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.mem_edgeSet : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {v w : V}, s(v, w) ∈ G'.edgeSet ↔ G'.Adj v w
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ),
  ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₁ =
    n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivision.isUnit_of_map_ne_zero : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {g q : PowerSeries A} {r : Polynomial A},
  (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 →
    (PowerSeries.X ^ ((PowerSeries.map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r → IsUnit q
-- Mathlib.Order.CompleteLattice.Defs
toDual_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : InfSet α] (f : ι → α), OrderDual.toDual (⨅ i, f i) = ⨆ i, OrderDual.toDual (f i)
-- Mathlib.Analysis.BoxIntegral.Partition.Split
/-- **Alias** of `BoxIntegral.Prepartition.exists_iUnion_eq_sdiff`.

---

For every prepartition `π` of `I` there exists a prepartition that covers exactly
`I \ π.iUnion`.  -/
BoxIntegral.Prepartition.exists_iUnion_eq_diff : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [Finite ι] (π : BoxIntegral.Prepartition I), ∃ π', π'.iUnion = ↑I \ π.iUnion
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddCommMonoidOfContinuousAdd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : AddCommMonoid β] → [ContinuousAdd β] → AddCommMonoid C(α, β)
-- Mathlib.Topology.ContinuousOn
ContinuousOn.matrixVecCons : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {n : ℕ} {f : α → β}
  {g : α → Fin n → β} {s : Set α},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun a => Matrix.vecCons (f a) (g a)) s
-- Mathlib.Algebra.Group.Basic
div_mul_cancel_left : ∀ {G : Type u_3} [inst : CommGroup G] (a b : G), a / (a * b) = b⁻¹
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_functor_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).functor.obj X).hom =
    CategoryTheory.CategoryStruct.comp (i.inv.app X.left) X.hom
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_self : ∀ {a : Ordinal.{u_4}}, a ≠ 0 → a / a = 1
-- Mathlib.Order.WithBot
WithBot.nontrivial : ∀ {α : Type u_1} [Nonempty α], Nontrivial (WithBot α)
-- Mathlib.Algebra.Group.Prod
mulMulHom.eq_1 : ∀ {α : Type u_6} [inst : CommSemigroup α], mulMulHom = { toFun := fun a => a.1 * a.2, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.of_arrow_iso_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Y X Y' X' B A : C} (i : A ⟶ B) {p : X ⟶ Y}
  {p' : X' ⟶ Y'} (e : CategoryTheory.Arrow.mk p ≅ CategoryTheory.Arrow.mk p')
  [hip : CategoryTheory.HasLiftingProperty i p], CategoryTheory.HasLiftingProperty i p'
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasCondSubgaussianMGF.congr_simp : ∀ {Ω : Type u_1} (m m_1 : MeasurableSpace Ω) (e_m : m = m_1) {mΩ : MeasurableSpace Ω} (hm : m ≤ mΩ)
  [inst : StandardBorelSpace Ω] (X X_1 : Ω → ℝ),
  X = X_1 →
    ∀ (c c_1 : NNReal),
      c = c_1 →
        ∀ (μ μ_1 : MeasureTheory.Measure Ω) (e_μ : μ = μ_1) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
          ProbabilityTheory.HasCondSubgaussianMGF m hm X c μ = ProbabilityTheory.HasCondSubgaussianMGF m_1 ⋯ X_1 c_1 μ_1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂},
  (m₁ ∪ m₂).getKey k h' = m₁.getKey k ⋯
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
/-- When `c` is negative, `‖f x‖ ≤ c * ‖g x‖` is nonsense and forces both `f` and `g` to have an
`eLpNorm` of `0`.  -/
MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg : ∀ {α : Type u_1} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G} {c : ℝ},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖) →
    c < 0 → ∀ (p : ENNReal), MeasureTheory.eLpNorm f p μ = 0 ∧ MeasureTheory.eLpNorm g p μ = 0
-- Mathlib.Order.RelIso.Basic
/-- `Sum.map` as a relation embedding between `Sum.LiftRel` relations.  -/
RelEmbedding.sumLiftRelMap : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {δ : Type u_4} →
        {r : α → α → Prop} →
          {s : β → β → Prop} →
            {t : γ → γ → Prop} → {u : δ → δ → Prop} → r ↪r s → t ↪r u → Sum.LiftRel r t ↪r Sum.LiftRel s u
-- Lean.Meta.AppBuilder
/-- Given `h₁ : a ≍ b`, `h₂ : b ≍ c`, returns a proof of `a ≍ c`.  -/
Lean.Meta.mkHEqTrans : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId : ∀ (x : CategoryTheory.LocallyDiscrete CommRingCat),
  CommRingCat.moduleCatExtendScalarsPseudofunctor.mapId x =
    CategoryTheory.Cat.Hom.isoMk (ModuleCat.extendScalarsId ↑x.as)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPullback_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Sieve X),
  CategoryTheory.Sieve.functorPullback (CategoryTheory.Functor.id C) R = R
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterMatrix.IsLiftable.eq_1 : ∀ {B : Type u_1} {G : Type u_5} [inst : Monoid G] (M : CoxeterMatrix B) (f : B → G),
  M.IsLiftable f = ∀ (i i' : B), (f i * f i') ^ M.M i i' = 1
-- Mathlib.FieldTheory.Galois.NormalBasis
_private.Mathlib.FieldTheory.Galois.NormalBasis.0.exists_linearIndependent_algEquiv_apply_of_finite : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Finite L],
  ∃ x, LinearIndependent K fun σ => σ x
-- Lean.Parser.Term
Lean.Parser.Term.letOptZeta.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Algebra.Monoid
tendsto_list_sum : ∀ {ι : Type u_1} {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [ContinuousAdd M]
  {f : ι → α → M} {x : Filter α} {a : ι → M} (l : List ι),
  (∀ i ∈ l, Filter.Tendsto (f i) x (nhds (a i))) →
    Filter.Tendsto (fun b => (List.map (fun c => f c b) l).sum) x (nhds (List.map a l).sum)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  (f : C(α, β)) (h : HasCompactSupport ⇑f), ⇑{ toContinuousMap := f, hasCompactSupport' := h } = ⇑f
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.PreservesMonomorphisms.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.PreservesMonomorphisms] (α : F ≅ G), G.PreservesMonomorphisms
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` and `K / E` are both purely inseparable extensions, then `K / F` is also
purely inseparable.  -/
IsPurelyInseparable.trans : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [h1 : IsPurelyInseparable F E]
  [h2 : IsPurelyInseparable E K], IsPurelyInseparable F K
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestMatch_of_ofSliceTo : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {p : s.Pos}
  {pos : (s.sliceTo p).Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat (String.Slice.Pos.ofSliceTo pos) →
    String.Slice.Pattern.Model.IsLongestMatch pat pos
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.values_empty : ∀ {α : Type u} {β : Type v}, ∅.values = []
-- Mathlib.Analysis.Fourier.ZMod
/-- The discrete Fourier transform of `Φ` is even if and only if `Φ` itself is.  -/
ZMod.dft_even_iff : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ}, Function.Even (ZMod.dft Φ) ↔ Function.Even Φ
-- Mathlib.Data.ENNReal.Real
ENNReal.toNNReal_mono : ∀ {a b : ENNReal}, b ≠ ⊤ → a ≤ b → a.toNNReal ≤ b.toNNReal
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.isSubordinate_toBumpCovering : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} [inst_6 : T2Space M]
  [inst_7 : IsManifold I (↑⊤) M] {f : SmoothBumpCovering ι I M s} {U : M → Set M},
  (f.toBumpCovering.IsSubordinate fun i => U (f.c i)) ↔ f.IsSubordinate U
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.of_mul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [NoZeroDivisors R]
  {y z : S}, y ∈ nonZeroDivisors S → IsAlgebraic R y → IsAlgebraic R (y * z) → IsAlgebraic R z