mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Localization
/-- The functor `ModuleCat.{v} R ⥤ ModuleCat.{v} (Localization S)` sending
`M` to `M.localizedModule S` and `f : M1 ⟶ M2` to
`IsLocalizedModule.mapExtendScalars S _ _ (Localization S) f.hom`.  -/
ModuleCat.localizedModuleFunctor : {R : Type u} →
  [inst : CommRing R] →
    [Small.{v, u} R] → (S : Submonoid R) → CategoryTheory.Functor (ModuleCat R) (ModuleCat (Localization S))
-- Mathlib.Analysis.Normed.Module.Ball.Action
isScalarTower_sphere_closedBall_closedBall : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [inst_5 : NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E],
  IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)
-- Mathlib.Order.UpperLower.Closure
bddAbove_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddAbove ↑(lowerClosure s) ↔ BddAbove s
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsMulRightInvariant.comap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G] {H : Type u_3} [inst_3 : Group H]
  {mH : MeasurableSpace H} [MeasurableMul H] (μ : MeasureTheory.Measure H) [μ.IsMulRightInvariant] {f : G →* H},
  MeasurableEmbedding ⇑f → (MeasureTheory.Measure.comap (⇑f) μ).IsMulRightInvariant
-- Mathlib.RingTheory.Regular.Category
IsSMulRegular.smulShortComplex_shortExact : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} {r : R}, IsSMulRegular (↑M) r → (M.smulShortComplex r).ShortExact
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toHasOfPostcompProperty : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.HasTwoOutOfThreeProperty], W.HasOfPostcompProperty W
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isColimitOfConeUnopOfCocone_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneUnopOfCocone c)) (s : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.isColimitOfConeUnopOfCocone F hc).desc s =
    (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Product of seminormed groups, using the sup norm.  -/
Prod.seminormedAddCommGroup : {E : Type u_2} →
  {F : Type u_3} → [SeminormedAddCommGroup E] → [SeminormedAddCommGroup F] → SeminormedAddCommGroup (E × F)
-- Mathlib.GroupTheory.PGroup
IsPGroup.to_quotient : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], IsPGroup p G → ∀ (H : Subgroup G) [inst_1 : H.Normal], IsPGroup p (G ⧸ H)
-- Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
/-- Given a proof `e`, mark it with `Lean.Grind.nestedProof`
 -/
Lean.Meta.Grind.markProof : Lean.Expr → Lean.Meta.Grind.GrindM Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.neighborSet_boxProd : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (x : α × β),
  (G □ H).neighborSet x = G.neighborSet x.1 ×ˢ {x.2} ∪ {x.1} ×ˢ H.neighborSet x.2
-- Mathlib.Algebra.Group.Basic
Semigroup.to_isLawfulIdentity : ∀ {M : Type u_4} [inst : MulOneClass M], Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1
-- Mathlib.Topology.MetricSpace.IsometricSMul
nndist_mul_left : ∀ {M : Type u} [inst : PseudoMetricSpace M] [inst_1 : Mul M] [IsIsometricSMul M M] (a b c : M),
  nndist (a * b) (a * c) = nndist b c
-- Mathlib.Data.Int.Bitwise
Int.lor.eq_2 : ∀ (m n : ℕ), (Int.ofNat m).lor (Int.negSucc n) = Int.negSucc (n.ldiff m)
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
Complex.hasProd_of_hasSum_log : ∀ {ι : Type u_1} {f : ι → ℂ} {a : ℂ},
  (∀ (i : ι), f i ≠ 0) → HasSum (fun i => Complex.log (f i)) a → HasProd f (Complex.exp a)
-- Mathlib.Topology.Maps.Basic
IsClosedMap.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z], IsClosedMap g → IsClosedMap f → IsClosedMap (g ∘ f)
-- Init.Data.Array.Attach
Array.attach.eq_1 : ∀ {α : Type u_1} (xs : Array α), xs.attach = xs.attachWith (Membership.mem xs) ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.inr_opProdIsoCoprod_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.opProdIsoCoprod A B).inv =
    CategoryTheory.Limits.prod.snd.op
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.π_map_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (n : ℕ) (x : ↑(groupCohomology.cocycles A n)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.map f φ n))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.π A n)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.π B n))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cocyclesMap f φ n)) x)
-- Init.Data.List.Lemmas
List.sum_append : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] [Std.LawfulLeftIdentity (fun x1 x2 => x1 + x2) 0]
  [Std.Associative fun x1 x2 => x1 + x2] {l₁ l₂ : List α}, (l₁ ++ l₂).sum = l₁.sum + l₂.sum
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.norm_sub_one_lt_two_iff : ∀ {A : Type u_1} [inst : CStarAlgebra A] {u : A}, u ∈ unitary A → (‖u - 1‖ < 2 ↔ -1 ∉ spectrum ℂ u)
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.centerToAddOpposite_symm_apply_coe : ∀ {M : Type u_2} [inst : AddZeroClass M] (r : ↥(AddSubsemigroup.center Mᵃᵒᵖ)),
  ↑(AddSubmonoid.centerToAddOpposite.symm r) = AddOpposite.unop ↑r
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivAt_inr : ∀ {𝕜 : 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] {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {p : M ⊕ M'} {q' : M'},
  HasMFDerivAt% Sum.inr q' (ContinuousLinearMap.id 𝕜 (TangentSpace I p))
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor_obj_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] (U : N),
  ((CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor p).obj U).fst = p.obj U
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
_private.Mathlib.AlgebraicGeometry.Morphisms.Flat.0.CategoryTheory.Pairwise.diagramMap.match_1.splitter : {ι : Type u_1} →
  (motive : (x x_1 : CategoryTheory.Pairwise ι) → (x ⟶ x_1) → Sort u_2) →
    (x x_1 : CategoryTheory.Pairwise ι) →
      (x_2 : x ⟶ x_1) →
        ((i : ι) →
            motive (CategoryTheory.Pairwise.single i) (CategoryTheory.Pairwise.single i)
              (CategoryTheory.Pairwise.Hom.id_single i)) →
          ((i j : ι) →
              motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.pair i j)
                (CategoryTheory.Pairwise.Hom.id_pair i j)) →
            ((i j : ι) →
                motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single i)
                  (CategoryTheory.Pairwise.Hom.left i j)) →
              ((i j : ι) →
                  motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single j)
                    (CategoryTheory.Pairwise.Hom.right i j)) →
                motive x x_1 x_2
-- Std.Async.Basic
/-- Create a new `AsyncTask` that will run after `x` has finished.
If `x`:
- errors, return an `AsyncTask` that resolves to the error.
- succeeds, return an `AsyncTask` that resolves to `f x`.
 -/
Std.Async.AsyncTask.map : {α β : Type} →
  (α → β) →
    Std.Async.AsyncTask α → optParam Task.Priority Task.Priority.default → optParam Bool false → Std.Async.AsyncTask β
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_one : Nat.sqrt 1 = 1
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.isSheaf_iff_multifork : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf J P ↔
    ∀ (X : C) (S : J.Cover X), Nonempty (CategoryTheory.Limits.IsLimit (S.multifork P))
-- Init.Data.Vector.Lemmas
Vector.toList_zip : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {as : Vector α n} {bs : Vector β n},
  (as.zip bs).toList = as.toList.zip bs.toList
-- Mathlib.Data.FunLike.Graded
/-- **Alias** of the reverse direction of `Graded.map_mem_iff`. -/
Graded.map_mem_of_mem : ∀ {E : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [inst : SetLike σ A]
  [inst_1 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_2 : EquivLike E A B] [GradedEquivLike E 𝒜 ℬ] (e : E) {i : ι}
  {x : A}, x ∈ 𝒜 i → e x ∈ ℬ i
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- If the second and third components of a morphism of distinguished triangles are
isomorphisms, the first component is as well. This can be thought of as a
pretriangulated category theoretical version of the five lemma.  -/
CategoryTheory.Pretriangulated.isIso₁_of_isIso₂₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  {T T' : CategoryTheory.Pretriangulated.Triangle C} (φ : T ⟶ T'),
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
      CategoryTheory.IsIso φ.hom₂ → CategoryTheory.IsIso φ.hom₃ → CategoryTheory.IsIso φ.hom₁
-- Init.Data.Vector.Lemmas
Vector.mem_toList_iff : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n}, a ∈ xs.toList ↔ a ∈ xs
-- Mathlib.Data.Multiset.FinsetOps
Multiset.mem_ndinsert : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Multiset α}, a ∈ Multiset.ndinsert b s ↔ a = b ∨ a ∈ s
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.toTrivSqZeroExt_ι : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M)
  [inst_3 : Module Rᵐᵒᵖ M] [inst_4 : IsCentralScalar R M],
  TensorAlgebra.toTrivSqZeroExt ((TensorAlgebra.ι R) x) = TrivSqZeroExt.inr x
-- Lean.Parser.Term
Lean.Parser.Term.suffices : Lean.Parser.Parser
-- Lean.Meta.LazyDiscrTree
/-- Backing array of trie entries.  Should be owned by this trie.  -/
Lean.Meta.LazyDiscrTree.tries : {α : Type} → Lean.Meta.LazyDiscrTree α → Array (Lean.Meta.LazyDiscrTree.Trie α)
-- Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
CategoryTheory.instIsMonoidalFunctorOppositeWOfHasSheafComposeForgetOfHasEnoughPoints : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  {J : CategoryTheory.GrothendieckTopology C} (A : Type u') [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  [CategoryTheory.Limits.HasProducts A] {FC : A → A → Type u_1} {CC : A → Type w}
  [inst_6 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_7 : CategoryTheory.ConcreteCategory A FC]
  [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.forget A).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)]
  [∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  [J.HasSheafCompose (CategoryTheory.forget A)] [J.HasEnoughPoints], J.W.IsMonoidal
-- Std.Do.WP.Sound
/-- A `wp`-provable postcondition with split `.ok`/`.error` cases refines the post-run computation
`prog.run : m (Except ε α)` via `Internal.Ensures`.
 -/
Std.Do.ExceptT.ensures_of_wp_run : ∀ {m : Type u → Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Do.WP m Std.Do.PostShape.pure]
  [Std.Do.WPSound m Std.Do.PostShape.pure] {ε α : Type u} {prog : ExceptT ε m α} (P : Except ε α → Prop),
  (⊢ₛ (Std.Do.wp prog).apply (fun a => ⌜P (Except.ok a)⌝, fun e => ⌜P (Except.error e)⌝, PUnit.unit)) →
    Std.Do.Internal.Ensures P prog.run
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toNonUnitalSubring_inj : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A]
  {S U : NonUnitalSubalgebra R A}, S.toNonUnitalSubring = U.toNonUnitalSubring ↔ S = U
-- Batteries.Logic
congrArg₂ : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) {x x' : α} {y y' : β}, x = x' → y = y' → f x y = f x' y'
-- Mathlib.Logic.Encodable.Basic
Encodable.decode_one : Encodable.decode 1 = some true
-- Mathlib.Analysis.Calculus.Deriv.Support
deriv_of_notMem_tsupport : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, x ∉ tsupport f → deriv f x = 0
-- Lean.Server.FileWorker.ExampleHover
/-- Not in a code block  -/
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.RWState.normal : Lean.Server.FileWorker.Hover.RWState✝
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instAddGroupCoeOfAddSubgroupClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → AddGroup (R i)] →
              [∀ (i : ι), AddSubgroupClass (S i) (R i)] →
                AddGroup (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instInhabited : {α : Type u} → Inhabited (Std.HashSet.Raw α)
-- Init.Grind.Offset
Lean.Grind.Nat.of_lo_eq_false : ∀ (u v k : ℕ), (u + k ≤ v) = False → v ≤ u + (k - 1)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction_le : ∀ {pat : ByteArray} {stackPos : ℕ} {hst : stackPos < pat.size},
  String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat stackPos hst ≤ stackPos
-- Mathlib.Topology.UniformSpace.Ultra.Constructions
/-- The product of uniform spaces with nonarchimedean uniformities has a
nonarchimedean uniformity.  -/
IsUltraUniformity.prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : UniformSpace X] [inst_1 : UniformSpace Y] [IsUltraUniformity X]
  [IsUltraUniformity Y], IsUltraUniformity (X × Y)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {μ : MeasureTheory.Measure Ω}
  {ℱ : MeasureTheory.Filtration ι m} {τ : Ω → WithTop ι} {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [CompleteSpace E] {f : Ω → E} [inst_4 : TopologicalSpace ι] [OrderTopology ι]
  [FirstCountableTopology ι] [MeasureTheory.SigmaFiniteFiltration μ ℱ] (hτ : MeasureTheory.IsStoppingTime ℱ τ)
  [MeasureTheory.SigmaFinite (μ.trim ⋯)] (i : ι), μ[f | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = ↑i}] μ[f | ↑ℱ i]
-- Mathlib.Data.Finsupp.Single
Finsupp.embDomain_single : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ↪ β) (a : α) (m : M),
  (Finsupp.embDomain f fun₀ | a => m) = fun₀ | f a => m
-- Mathlib.Algebra.Divisibility.Basic
pow_dvd_pow_of_dvd_of_le : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α} {m n : ℕ}, a ∣ b → m ≤ n → a ^ m ∣ b ^ n
-- Init.Grind.AC
Lean.Grind.AC.Seq.unionFuel.match_3.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (fuel : ℕ) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ),
  fuel = 0 →
    (match fuel with
      | 0 => h_1 ()
      | fuel.succ => h_2 fuel) ≍
      h_1 ()
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.Hom.ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {R R' : Φ.RightResolution X₂} {x y : R.Hom R'}, x.f = y.f → x = y
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenter.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 → ∀ (signs signs_1 : Finset (Fin (n + 1))), signs = signs_1 → s.excenter signs = s_1.excenter signs_1
-- Lean.Parser.Command
Lean.Parser.Command.classInductive : Lean.Parser.Parser
-- Mathlib.Data.Nat.Prime.Nth
Nat.nth_prime_three_eq_seven : Nat.nth Nat.Prime 3 = 7
-- Mathlib.Algebra.Algebra.Hom
AlgHomClass.linearMapClass : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : FunLike F A B] [AlgHomClass F R A B],
  LinearMapClass F R A B
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpTriggerKind.triggerCharacter.sizeOf_spec : sizeOf Lean.Lsp.SignatureHelpTriggerKind.triggerCharacter = 1
-- Mathlib.Order.Filter.IndicatorFunction
Filter.EventuallyEq.of_indicator_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β] {l : Filter α} {c : β},
  c ≠ 0 → ∀ {s t : Set α}, ((s.indicator fun x => c) =ᶠ[l] t.indicator fun x => c) → s =ᶠ[l] t
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_congr : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c₁ c₂ : ℝ} {l : Filter α}
  {f₁ f₂ : α → E} {g₁ g₂ : α → F},
  c₁ = c₂ → f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → (Asymptotics.IsBigOWith c₁ l f₁ g₁ ↔ Asymptotics.IsBigOWith c₂ l f₂ g₂)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?_intermediateZip.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n' : ℕ) → motive n'.succ) → motive n
-- Mathlib.Control.Bitraversable.Instances
instBitraversableBicompr : {t : Type u → Type u → Type u} →
  [Bitraversable t] → (F : Type u → Type u) → [Traversable F] → Bitraversable (Function.bicompr F t)
-- Lean.Compiler.IR.Format
Lean.IR.instToFormatIRType : Std.ToFormat Lean.IR.IRType
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k : α} (h : m.WF),
  Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.filterMap f m) k =
    (Std.DHashMap.Raw.Const.get? m k).pbind fun x h' => f (m.getKey k ⋯) x
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.of_subsingleton : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β}
  [Subsingleton α] {K : NNReal}, AntilipschitzWith K f
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If `f` is a strictly monotone function on a left neighborhood of `a` and the image of this
neighborhood under `f` meets every interval `[b, f a)`, `b < f a`, then `f` is continuous at `a`
from the left.

The assumption `hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)` is required because otherwise the
function `f : ℝ → ℝ` given by `f x = if x < 0 then x else x + 1` would be a counter-example at
`a = 0`.  -/
StrictMonoOn.continuousWithinAt_left_of_exists_between : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α},
  StrictMonoOn f s →
    s ∈ nhdsWithin a (Set.Iic a) → (∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ico b (f a)) → ContinuousWithinAt f (Set.Iic a) a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {t : CategoryTheory.Limits.PushoutCocone f g} (ht : CategoryTheory.Limits.IsColimit t) {W : C} {k l : t.pt ⟶ W},
  CategoryTheory.CategoryStruct.comp t.inl k = CategoryTheory.CategoryStruct.comp t.inl l →
    CategoryTheory.CategoryStruct.comp t.inr k = CategoryTheory.CategoryStruct.comp t.inr l → k = l
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRight_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f g : X ⟶ Y),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) =
      CategoryTheory.MonoidalCategoryStruct.whiskerRight g (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ↔
    f = g
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns the number of mappings present in the map.  -/
Std.DTreeMap.Raw.size : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → ℕ
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.map.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] (f f_1 : R →+* S) (e_f : f = f_1) [inst_4 : IsLocalHom f],
  IsLocalRing.ResidueField.map f = IsLocalRing.ResidueField.map f_1
-- Init.Data.String.Lemmas.Order
String.Pos.sliceFrom_lt_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q},
  p₀.sliceFrom q h < p ↔ q < String.Pos.ofSliceFrom p
-- Batteries.Logic
congr_eqRec : ∀ {α : Sort u_1} {γ : Sort u_2} {x x' : α} {β : α → Sort u_3} (f : (x : α) → β x → γ) (h : x = x') (y : β x),
  f x' (h ▸ y) = f x y
-- Mathlib.GroupTheory.QuotientGroup.Finite
AddGroup.fintypeOfKerLeRange.eq_1 : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : AddGroup F] [inst_1 : AddGroup G] [inst_2 : AddGroup H]
  [inst_3 : Fintype F] [inst_4 : Fintype H] (f : F →+ G) (g : G →+ H) (h : g.ker ≤ f.range),
  AddGroup.fintypeOfKerLeRange f g h =
    Fintype.ofEquiv ((G ⧸ g.ker) × ↥g.ker) AddSubgroup.addGroupEquivQuotientProdAddSubgroup.symm
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.col_weak : ∀ {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i1 i2 j : ℕ}, i1 ≤ i2 → (i2, j) ∈ μ → T i1 j ≤ T i2 j
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.lhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig → aig.Ref
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_toArray_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α}
  {v : β},
  t.WF →
    ((k, v) ∈ Std.DTreeMap.Internal.Impl.Const.toArray t ↔
      t.getKey? k = some k ∧ Std.DTreeMap.Internal.Impl.Const.get? t k = some v)
-- Mathlib.RingTheory.Ideal.Basic
/-- Ideals of a `DivisionSemiring` are a simple order. Thanks to the way abbreviations work,
this automatically gives an `IsSimpleModule K` instance.  -/
Ideal.isSimpleOrder : ∀ {K : Type u_5} [inst : DivisionSemiring K], IsSimpleOrder (Ideal K)