mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_zero' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [inst : ProbabilityTheory.IsSFiniteKernel κ], (κ.withDensity fun x x_1 => 0) = 0
-- Mathlib.NumberTheory.Primorial
Nat.Prime.dvd_primorial_iff : ∀ {p n : ℕ}, Nat.Prime p → (p ∣ primorial n ↔ p ≤ n)
-- Lean.Message
Lean.MessageData.ofWidget.sizeOf_spec : ∀ (a : Lean.Widget.WidgetInstance) (a_1 : Lean.MessageData),
  sizeOf (Lean.MessageData.ofWidget a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Algebra.Order.Star.Basic
star_left_conjugate_le_conjugate : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a b : R}, a ≤ b → ∀ (c : R), star c * a * c ≤ star c * b * c
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.zpow_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H] (f : X ⟶ G) (n : ℤ) (g : G ⟶ H)
  [CategoryTheory.IsMonHom g] {Z : C} (h : H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f ^ n) (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g ^ n) h
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_range_inr : ∀ {α : Type u} {β : Type v}, Cardinal.mk ↑(Set.range Sum.inr) = Cardinal.lift.{u, v} (Cardinal.mk β)
-- Lean.Parser.Command
Lean.Parser.Term.set_option.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Limits.Cones
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.ConeMorphism.w_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.ConeMorphism A B)
  (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp (B.π.app j) h) =
    CategoryTheory.CategoryStruct.comp (A.π.app j) h
-- Mathlib.Order.Max
IsTop.not_isBot : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α} [Nontrivial α], IsTop a → ¬IsBot a
-- Mathlib.Order.Category.BddOrd
bddOrd_dual_comp_forget_to_bipointed : BddOrd.dual.comp (CategoryTheory.forget₂ BddOrd Bipointed) =
  (CategoryTheory.forget₂ BddOrd Bipointed).comp Bipointed.swap
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Alternative form for the difference between `f - f₀` and its modified term.  -/
WeakFEPair.f_modif_aux1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E),
  Set.EqOn (fun x => P.f_modif x - P.f x + P.f₀)
    (((Set.Ioo 0 1).indicator fun x => P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) + {1}.indicator fun x => P.f₀ - P.f 1)
    (Set.Ioi 0)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : ↑X.affineOpens),
  AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom h U =
    AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom h U
-- Init.Data.String.Lemmas.Order
String.Pos.le_slice_iff : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁},
  p ≤ q.slice p₀ p₁ h₀ h₁ ↔ String.Pos.ofSlice p ≤ q
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
/-- A monoid homomorphism from a monoid `M` to a group `G` lifts to a group homomorphism from the
Grothendieck group of `M` to `G`.  -/
Algebra.GrothendieckAddGroup.lift : {M : Type u_1} →
  {G : Type u_2} →
    [inst : AddCommMonoid M] → [inst_1 : AddCommGroup G] → (M →+ G) ≃ (Algebra.GrothendieckAddGroup M →+ G)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.mapDomain_smul : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {G' : Type u_3} {f : G → G'} {v : SkewMonoidAlgebra k G}
  {R : Type u_5} [inst_1 : Monoid R] [inst_2 : DistribMulAction R k] {b : R},
  (SkewMonoidAlgebra.mapDomain f) (b • v) = b • (SkewMonoidAlgebra.mapDomain f) v
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrLeft.eq_1 : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [inst : MulOneClass M₁] [inst_1 : MulOneClass M₂]
  [inst_2 : CommMonoid N] (e : M₁ ≃* M₂), e.monoidHomCongrLeft = { toEquiv := e.monoidHomCongrLeftEquiv, map_mul' := ⋯ }
-- Lean.Util.ParamMinimizer
/-- Budget. That is, the maximum number of calls to `test` that we are willing to perform.
`0` means unbounded.
 -/
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.Context.maxCalls : {m : Type → Type} → Lean.Util.ParamMinimizer.Context✝ m → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- The embedding of `G` into `G ⊕g H`.  -/
SimpleGraph.Embedding.sumInl : {V : Type u_3} → {W : Type u_5} → {G : SimpleGraph V} → {H : SimpleGraph W} → G ↪g G ⊕g H
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.instPartialOrder.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.instPartialOrder = PartialOrder.ofSetLike (AddSubgroup G) G
-- Init.Data.AC
Lean.Data.AC.EvalInformation.evalOp : {α : Sort u} → {β : Sort v} → [self : Lean.Data.AC.EvalInformation α β] → α → β → β → β
-- Mathlib.MeasureTheory.Measure.Tight
/-- A set of measures `S` is tight if for all `0 < ε`, there exists a compact set `K` such that
for all `μ ∈ S`, `μ Kᶜ ≤ ε`.  -/
MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [inst : TopologicalSpace 𝓧],
  MeasureTheory.IsTightMeasureSet S ↔ ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
-- Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup
/-- A projective special linear group is the quotient of a special linear group by its center.  -/
Matrix.ProjectiveSpecialLinearGroup : (n : Type u) → [DecidableEq n] → [Fintype n] → (R : Type v) → [CommRing R] → Type (max (max u v) v u)
-- Init.Data.ByteArray.Basic
ByteArray.findFinIdx?.loop : (a : ByteArray) → (UInt8 → Bool) → ℕ → Option (Fin a.size)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeReachable.rfl : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u : V}, G.IsEdgeReachable k u u
-- Mathlib.Order.Bounded
Set.unbounded_le_iff : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α], Set.Unbounded (fun x1 x2 => x1 ≤ x2) s ↔ ∀ (a : α), ∃ b ∈ s, a < b
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.map_id : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (C : PointedCone R E), PointedCone.map LinearMap.id C = C
-- Mathlib.Algebra.Polynomial.Monic
/-- `X ^ n - a` is monic.  -/
Polynomial.monic_X_pow_sub_C : ∀ {R : Type u} [inst : Ring R] (a : R) {n : ℕ}, n ≠ 0 → (Polynomial.X ^ n - Polynomial.C a).Monic
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.hp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C}
  {f : X ⟶ Y} (self : W₁.MapFactorizationData W₂ f), W₂ self.p
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonMarkupContent : Lean.ToJson Lean.Lsp.MarkupContent
-- Batteries.Data.Fin.Coding
Fin.encodeSubtype_succ_neg : ∀ {n : ℕ} {P : Fin (n + 1) → Prop} [inst : DecidablePred P] (h₀ : ¬P 0) {i : Fin n} (h : P i.succ),
  Fin.encodeSubtype P ⟨i.succ, h⟩ = Fin.cast ⋯ (Fin.encodeSubtype (fun i => P i.succ) ⟨i, h⟩)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.inter_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp}, t₁.inter t₂ = t₁ ∩ t₂
-- Mathlib.Data.Int.Log
Int.neg_clog_inv_eq_log : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b : ℕ) (r : R), -Int.clog b r⁻¹ = Int.log b r
-- Mathlib.Order.Heyting.Basic
compl_le_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ b → bᶜ ≤ aᶜ
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.instQuiverMonad : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → Quiver (CategoryTheory.Monad C)
-- Mathlib.Tactic.Push
/-- Try to rewrite using a `pull` lemma.  -/
Mathlib.Tactic.Push.pullStep : Mathlib.Tactic.Push.Head → Lean.Meta.Simp.Simproc
-- Init.Data.Array.MapIdx
Array.back_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : ℕ → α → β} (h : 0 < (Array.mapIdx f xs).size),
  (Array.mapIdx f xs).back h = f (xs.size - 1) (xs.back ⋯)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.restrictMonoidHom_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommGroup Y] {V : Set X}
  (D : Function.locallyFinsuppWithin U Y) (h : V ⊆ U),
  (Function.locallyFinsuppWithin.restrictMonoidHom h) D = D.restrict h
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.pretrivializationAt : {B : Type u_2} →
  {F : Type u_3} →
    {E : B → Type u_5} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : (x : B) → TopologicalSpace (E x)] →
            FiberPrebundle F E → B → Bundle.Pretrivialization F Bundle.TotalSpace.proj
-- Init.Data.List.Lemmas
List.getLast!_eq_getLast?_getD : ∀ {α : Type u_1} [inst : Inhabited α] {l : List α}, l.getLast! = l.getLast?.getD default
-- Mathlib.Algebra.Group.Subgroup.Finite
MonoidHom.decidableMemRange : {G : Type u_1} →
  [inst : Group G] →
    {N : Type u_3} →
      [inst_1 : Group N] → (f : G →* N) → [Fintype G] → [DecidableEq N] → DecidablePred fun x => x ∈ f.range
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.Functor Cᵒᵖ (Type u_4)},
  CategoryTheory.regularTopology.EqualizerCondition P →
    ∀ {X B : C} (π : X ⟶ B) [CategoryTheory.EffectiveEpi π] [inst_2 : CategoryTheory.Limits.HasPullback π π],
      Function.Bijective
        ⇑(CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.regularTopology.mapToEqualizer P π (CategoryTheory.Limits.pullback.fst π π)
              (CategoryTheory.Limits.pullback.snd π π) ⋯))
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_lt : ∀ {a b : UInt64}, a.toUInt16 < b.toUInt16 ↔ a % 65536 < b % 65536
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The empty set is collinear.  -/
collinear_empty : ∀ (k : Type u_1) {V : Type u_2} (P : Type u_3) [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P], Collinear k ∅
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Stream.cons.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (v : α) (r : RBTree.RBNode α) (tail : RBTree.RBNode.Stream α),
  sizeOf (RBTree.RBNode.Stream.cons v r tail) = 1 + sizeOf v + sizeOf r + sizeOf tail
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceParams.context : Lean.Lsp.ReferenceParams → Lean.Lsp.ReferenceContext
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.extFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (n : ℕ) (X : Cᵒᵖ),
  (CategoryTheory.Abelian.extFunctor n).obj X = CategoryTheory.Abelian.extFunctorObj (Opposite.unop X) n
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- The empty set is a measurable set. Use `MeasurableSet.empty` instead.  -/
MeasurableSpace.measurableSet_empty : ∀ {α : Type u_7} (self : MeasurableSpace α), MeasurableSpace.MeasurableSet' self ∅
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.ratio_le_opNorm : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i), ‖f m‖ / ∏ i, ‖m i‖ ≤ ‖f‖
-- Mathlib.Data.Prod.TProd
Set.tprod.eq_def : ∀ {ι : Type u} {α : ι → Type v} (x : List ι) (x_1 : (i : ι) → Set (α i)),
  Set.tprod x x_1 =
    match x, x_1 with
    | [], x => Set.univ
    | i :: is, t => t i ×ˢ Set.tprod is t
-- Aesop.Search.Expansion.Simp
Aesop.SimpResult.simplified : Lean.MVarId → Lean.Meta.Simp.UsedSimps → Aesop.SimpResult
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `sInf s = 0` when `s` is a set of reals that's either empty or unbounded below,
it suffices to show that all elements of `s` are nonpositive to show that `sInf s ≤ 0`.  -/
Real.sInf_nonpos : ∀ {s : Set ℝ}, (∀ x ∈ s, x ≤ 0) → sInf s ≤ 0
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.toListModel_replicate_nil : ∀ {α : Type u} {β : α → Type v} {c : ℕ},
  Std.DHashMap.Internal.toListModel (Array.replicate c Std.DHashMap.Internal.AssocList.nil) = []
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonTextDocumentContentChangeEvent : Lean.FromJson Lean.Lsp.TextDocumentContentChangeEvent
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_inf : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜]
  (I J : HomogeneousIdeal 𝒜), (I ⊓ J).toIdeal = I.toIdeal ⊓ J.toIdeal
-- Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
SSet.Subcomplex.unionProd.pushoutObjObj_ι : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex),
  (SSet.Subcomplex.unionProd.pushoutObjObj S T).ι = (S.unionProd T).ι
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_rcc_eq_some_iff : ∀ {k m n : ℤ} {i : ℕ}, (m...=n).toArray[i]? = some k ↔ i < (n + 1 - m).toNat ∧ m + ↑i = k
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasStrictFDerivAt.const_cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E}
  {c : ℂ},
  HasStrictFDerivAt f f' x → c ≠ 0 ∨ f x ≠ 0 → HasStrictFDerivAt (fun x => c ^ f x) ((c ^ f x * Complex.log c) • f') x
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- The matrices `Matrix n n ℂ` with the L2 operator norm form a `CStarAlgebra`.  -/
Matrix.instCStarAlgebra : {n : Type u_6} → [Fintype n] → [DecidableEq n] → CStarAlgebra (Matrix n n ℂ)
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.one_of_isUnit : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R],
  v.Integers O → ∀ {x : O}, IsUnit x → v ((algebraMap O R) x) = 1
-- Mathlib.Algebra.Homology.LeftResolution.Basic
/-- The isomorphism which gives the inductive step of the construction of `Λ.chainComplex X`.  -/
CategoryTheory.Abelian.LeftResolution.chainComplexXIso : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          (Λ : CategoryTheory.Abelian.LeftResolution ι) →
            (X : A) →
              [inst_2 : ι.Full] →
                [inst_3 : ι.Faithful] →
                  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] →
                    [inst_5 : CategoryTheory.Abelian A] →
                      (n : ℕ) →
                        (Λ.chainComplex X).X (n + 2) ≅
                          Λ.F.obj (CategoryTheory.Limits.kernel (ι.map ((Λ.chainComplex X).d (n + 1) n)))
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.add.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- action on 1-morphisms  -/
CategoryTheory.StrictlyUnitaryLaxFunctorCore.map : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (self : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) → {X Y : B} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
/-- The addition of morphisms in `D`, when `L : C ⥤ D` is a localization
functor, `C` is preadditive and there is a left calculus of fractions.  -/
CategoryTheory.Localization.Preadditive.add : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.Preadditive C] →
          {L : CategoryTheory.Functor C D} →
            (W : CategoryTheory.MorphismProperty C) →
              [L.IsLocalization W] →
                [W.HasLeftCalculusOfFractions] →
                  {X Y : C} → {X' Y' : D} → (L.obj X ≅ X') → (L.obj Y ≅ Y') → (X' ⟶ Y') → (X' ⟶ Y') → (X' ⟶ Y')
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induceHom_injective : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ : G →g G')
  (φst : Set.MapsTo (⇑φ) s t), Set.InjOn (⇑φ) s → Function.Injective ⇑(SimpleGraph.induceHom φ φst)
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.add.inj : ∀ {a b a_1 b_1 : Int.Internal.Linear.Expr}, a.add b = a_1.add b_1 → a = a_1 ∧ b = b_1
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {l : List α} {k k' : α},
  (k == k') = true →
    k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertManyIfNewUnit l).getKey! k' = k
-- Batteries.Recycling.RBTree.Depth
RBTree.RBNode.size_lt_depth : ∀ {α : Type u_1} (t : RBTree.RBNode α), t.size < 2 ^ t.depth
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.last.eq_def : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (x x_1 : ι) (x_2 : Monoid.CoprodI.NeWord M x x_1),
  x_2.last =
    match x, x_1, x_2 with
    | x, .(x), Monoid.CoprodI.NeWord.singleton x_3 _hne1 => x_3
    | x, x_3, _w₁.append _hne w₂ => w₂.last
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
/-- An invariant inner product on the coweight space.  -/
RootPairing.CorootForm : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] → RootPairing ι R M N → [Fintype ι] → LinearMap.BilinForm R N
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_insertMany_list_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α}, (t.insertMany l).size ≤ t.size + l.length
-- Lean.Util.Sorry
Lean.Expr.hasNonSyntheticSorry : Lean.Expr → Bool
-- Init.Data.Vector.Lemmas
Vector.append_empty : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs ++ #v[] = xs
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.instUniqueHomLeftRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : C} → {Y : D} → Unique (CategoryTheory.Join.left X ⟶ CategoryTheory.Join.right Y)
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.instMonadMor₂BicategoryM : Mathlib.Tactic.BicategoryLike.MonadMor₂ Mathlib.Tactic.Bicategory.BicategoryM
-- Mathlib.Topology.MetricSpace.HolderNorm
MemHolder.nsmul : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : NormedAddCommGroup Y] {r : NNReal} {f : X → Y}
  [NormedSpace ℝ Y] (n : ℕ), MemHolder r f → MemHolder r (n • f)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- A function is differentiable on a union of open sets `s i`
iff it is differentiable on each `s i`.  -/
mdifferentiableOn_iUnion_iff_of_isOpen : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {ι : Type u_11}
  {s : ι → Set M}, (∀ (i : ι), IsOpen (s i)) → (MDiff[⋃ i, s i] f ↔ ∀ (i : ι), MDiff[s i] f)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.isEquivalent_iff_tendsto_one : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] {u v : α → β} {l : Filter α},
  (∀ᶠ (x : α) in l, v x ≠ 0) → (Asymptotics.IsEquivalent l u v ↔ Filter.Tendsto (u / v) l (nhds 1))
-- Mathlib.Data.Fin.Basic
Fin.val_sub_one_of_ne_zero : ∀ {n : ℕ} {i : Fin n}, i ≠ 0 → ↑(i - 1) = ↑i - 1
-- Init.Data.UInt.Lemmas
USize.ofNatTruncate_eq_ofNat : ∀ n < USize.size, USize.ofNatClamp n = USize.ofNat n
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The universal morphism from any other cone to a limit cone.  -/
CategoryTheory.Limits.IsLimit.liftConeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit t → (s : CategoryTheory.Limits.Cone F) → s ⟶ t
-- Mathlib.Logic.Equiv.Defs
Equiv.sumIsRight_apply : ∀ {α : Type u_1} {β : Type u_2} (x : { x // x.isRight = true }), Equiv.sumIsRight x = (↑x).getRight ⋯
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.of_image_filter : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] [inst_2 : DecidableEq H] (f : G →ₙ+ H) {A B : Finset G}
  {aG bG : G} {aH bH : H},
  f aG = aH →
    f bG = bH →
      UniqueAdd (Finset.image (⇑f) A) (Finset.image (⇑f) B) aH bH →
        UniqueAdd ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG → UniqueAdd A B aG bG
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
/-- Composition of two open partial homeomorphisms when the target of the first and the source of
the second coincide.  -/
OpenPartialHomeomorph.trans' : {X : Type u_1} →
  {Y : Type u_3} →
    {Z : Type u_5} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] →
            (e : OpenPartialHomeomorph X Y) →
              (e' : OpenPartialHomeomorph Y Z) → e.target = e'.source → OpenPartialHomeomorph X Z
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.Opens.partialIsoOfDense_iso : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (hU : Dense ↑U), (U.partialIsoOfDense hU).iso = (↑U).topIso
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.coe_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β], ⇑0 = 0
-- Lean.Parser.Basic
Lean.Parser.numLitFn : Lean.Parser.ParserFn
-- Mathlib.FieldTheory.NormalizedTrace
Algebra.normalizedTrace_algebraMap_apply : ∀ (F : Type u_3) (E : Type u_4) (K : Type u_5) [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra E K] [inst_5 : Algebra F K] [IsScalarTower F E K]
  [inst_7 : Algebra.IsIntegral F E] [inst_8 : Algebra.IsIntegral F K] [inst_9 : CharZero F] (a : E),
  (Algebra.normalizedTrace F K) ((algebraMap E K) a) = (Algebra.normalizedTrace F E) a
-- Mathlib.Order.Lattice
sup_left_right_swap : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ b ⊔ c = c ⊔ b ⊔ a
-- Mathlib.NumberTheory.PythagoreanTriples
/-- Pythagorean triples are interchangeable, i.e `x * x + y * y = y * y + x * x = z * z`.
This comes from additive commutativity.  -/
pythagoreanTriple_comm : ∀ {x y z : ℤ}, PythagoreanTriple x y z ↔ PythagoreanTriple y x z
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_of_div_tendsto_nhds_ne_zero : ∀ {α : Type u_1} {𝕜 : Type u_14} [inst : NormedField 𝕜] {l : Filter α} {c : 𝕜} {f g : α → 𝕜},
  Filter.Tendsto (fun x => g x / f x) l (nhds c) → c ≠ 0 → f =Θ[l] g