mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.Client
Lean.Lsp.Registration.mk.inj : ∀ {id method : String} {registerOptions : Option Lean.Json} {id_1 method_1 : String}
  {registerOptions_1 : Option Lean.Json},
  { id := id, method := method, registerOptions := registerOptions } =
      { id := id_1, method := method_1, registerOptions := registerOptions_1 } →
    id = id_1 ∧ method = method_1 ∧ registerOptions = registerOptions_1
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The image of a measurable set under a measurable embedding is a measurable set.  -/
MeasurableEmbedding.measurableSet_image' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β},
  MeasurableEmbedding f → ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
AlgebraicTopology.DoldKan.homotopyHσToZero.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ),
  AlgebraicTopology.DoldKan.homotopyHσToZero q = Homotopy.nullHomotopy' (AlgebraicTopology.DoldKan.hσ' q)
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n log n)`. Monadic fold over the elements of a heap in increasing order,
by repeatedly pulling the minimum element out of the heap.
 -/
Batteries.BinomialHeap.foldM : {α : Type u} →
  {le : α → α → Bool} →
    {m : Type u_1 → Type u_2} → {β : Type u_1} → [Monad m] → Batteries.BinomialHeap α le → β → (β → α → m β) → m β
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- The free-forgetful adjunction for R-modules.  -/
ModuleCat.adj : (R : Type u) → [inst : Ring R] → ModuleCat.free R ⊣ CategoryTheory.forget (ModuleCat R)
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `diff` which can be used in the absence of balance
information but still assumes the preconditions of `diff`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.diff! : {α : Type u} →
  {β : α → Type v} →
    [Ord α] → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α], Multiset.lcm 0 = 1
-- Init.Data.Array.Find
Array.findIdx?_subtype : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Array.findIdx? f xs = Array.findIdx? g xs.unattach
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct.assocInst : Lean.Meta.Grind.AC.Struct → Lean.Expr
-- Mathlib.Algebra.Algebra.Equiv
LinearEquiv.symm_conjAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₁]
  [inst_7 : Module S M₂] [inst_8 : SMulCommClass S R M₁] [inst_9 : SMulCommClass S R M₂] [inst_10 : SMul R S]
  [inst_11 : IsScalarTower R S M₁] [inst_12 : IsScalarTower R S M₂] (e : M₁ ≃ₗ[S] M₂),
  (LinearEquiv.conjAlgEquiv R e).symm = LinearEquiv.conjAlgEquiv R e.symm
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.card_image_le : ∀ {x : ZFSet.{u}} {f : ZFSet.{u} → ZFSet.{u}} [inst : ZFSet.Definable₁ f], (ZFSet.image f x).card ≤ x.card
-- Mathlib.MeasureTheory.Covering.LiminfLimsup
blimsup_cthickening_ae_eq_blimsup_thickening : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α] [BorelSpace α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] {p : ℕ → Prop}
  {s : ℕ → Set α} {r : ℕ → ℝ},
  Filter.Tendsto r Filter.atTop (nhds 0) →
    (∀ᶠ (i : ℕ) in Filter.atTop, p i → 0 < r i) →
      Filter.blimsup (fun i => Metric.cthickening (r i) (s i)) Filter.atTop p =ᵐ[μ]
        Filter.blimsup (fun i => Metric.thickening (r i) (s i)) Filter.atTop p
-- Mathlib.LinearAlgebra.Prod
LinearMap.coe_inl : ∀ {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₂], ⇑(LinearMap.inl R M M₂) = fun x => (x, 0)
-- Mathlib.Data.Matrix.Basic
AddEquiv.mapMatrix_refl : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} [inst : Add α],
  (AddEquiv.refl α).mapMatrix = AddEquiv.refl (Matrix m n α)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Identity map as a `LinearMap`  -/
LinearMap.id : {R : Type u_1} → {M : Type u_8} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] M
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffAt_mul_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G]
  {a b : G}, ContMDiffAt I I n (fun x => a * x) b
-- Mathlib.Data.Fin.Basic
Fin.val_one' : ∀ (n : ℕ) [inst : NeZero n], ↑1 = 1 % n
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
mem_subalgebraOfSubsemiring : ∀ {R : Type u_1} [inst : Semiring R] {x : R} {S : Subsemiring R}, x ∈ subalgebraOfSubsemiring S ↔ x ∈ S
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∉ m₂ → (m₁ ∩ m₂).get? k = none
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv_char_self : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), (RegularExpression.char a).deriv a = 1
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.isEmpty : Lean.Meta.FVarSubst → Bool
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.State : Type
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion 1 = 1
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.spanNorm_eq : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] (I : Ideal S),
  Ideal.spanNorm R I = (Ideal.relNorm R) I
-- Aesop.ElabM
Aesop.ElabM : Type → Type
-- Init.Core
DoResultPR.pure.sizeOf_spec : ∀ {α β σ : Type u} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ] (a : α) (a_1 : σ),
  sizeOf (DoResultPR.pure a a_1) = 1 + sizeOf a + sizeOf a_1
-- Init.Core
Setoid.mk : {α : Sort u} → (r : α → α → Prop) → Equivalence r → Setoid α
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasInitial C],
  CategoryTheory.Limits.HasZeroObject.zeroIsoInitial.hom = 0
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_eq_intervalIntegral_deriv : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E}
  [inst_5 : NormedSpace ℝ E] [inst_6 : NormedSpace ℝ F] (ω : E → E →L[𝕜] F) (γ : Path a b),
  ∫ᶜ (x : E) in γ, ω x = ∫ (t : ℝ) in 0..1, (ω (γ.extend t)) (deriv (⇑γ.extend) t)
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
IsValuativeTopology.mem_nhds_iff : ∀ {R : Type u_1} {inst : Ring R} {inst_1 : ValuativeRel R} {inst_2 : TopologicalSpace R} [self : IsValuativeTopology R]
  {s : Set R} {x : R}, s ∈ nhds x ↔ ∃ γ, (fun x_1 => x + x_1) '' {z | (ValuativeRel.valuation R) z < ↑γ} ⊆ s
-- Std.Http.Data.Method
Std.Http.instInhabitedMethod : Inhabited Std.Http.Method
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.map_id : ∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α), (MeasureTheory.OuterMeasure.map id) m = m
-- Mathlib.RingTheory.Algebraic.Basic
Polynomial.algEquivOfTranscendental_coe : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (s : S)
  (h : Transcendental R s), ↑(Polynomial.algEquivOfTranscendental R s h) = ↑(Polynomial.aeval ⟨s, ⋯⟩)
-- Mathlib.Analysis.Convex.Join
convexJoin_convexJoin_convexJoin_comm : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (s t u v : Set E),
  convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A mono factorisation of `f ≫ g`, where `g` is an isomorphism,
gives a mono factorisation of `f`.  -/
CategoryTheory.Limits.MonoFactorisation.ofCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        {Y' : C} →
          {g : Y ⟶ Y'} →
            [CategoryTheory.IsIso g] →
              CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g) →
                CategoryTheory.Limits.MonoFactorisation f
-- Mathlib.Data.Nat.Cast.Prod
Prod.snd_ofNat : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoidWithOne α] [inst_1 : AddMonoidWithOne β] (n : ℕ)
  [inst_2 : n.AtLeastTwo], (OfNat.ofNat n).2 = OfNat.ofNat n
-- Mathlib.Data.Fin.VecNotation
Matrix.range_empty : ∀ {α : Type u} (u : Fin 0 → α), Set.range u = ∅
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- A multilinear map is compatible with scalar multiplication in every argument.  -/
MultilinearMap.map_update_smul' : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (self : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R)
  (x : M₁ i), self.toFun (Function.update m i (c • x)) = c • self.toFun (Function.update m i x)
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The type family over `PrimeSpectrum R` consisting of the localization over each point.  -/
AlgebraicGeometry.StructureSheaf.Localizations : {R : Type u} →
  (M : Type u) →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → ↑(AlgebraicGeometry.PrimeSpectrum.Top R) → Type u
-- Mathlib.Analysis.AbsoluteValue.Equivalence
/-- If `v` and `w` are inequivalent absolute values and `v` is non-trivial, then we can find an `a : R`
such that `v a < 1` while `1 ≤ w a`.
 -/
AbsoluteValue.exists_lt_one_one_le_of_not_isEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : Semifield S] [inst_2 : LinearOrder S] [IsStrictOrderedRing S]
  [Archimedean S] [ExistsAddOfLE S] {v w : AbsoluteValue R S}, v.IsNontrivial → ¬v.IsEquiv w → ∃ a, v a < 1 ∧ 1 ≤ w a
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.zero_vadd : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (x : AddOreLocalization S X), 0 +ᵥ x = x
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.instHashableAbsoluteLspSemanticToken.hash : Lean.Server.FileWorker.AbsoluteLspSemanticToken → UInt64
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairEquiv_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (e : C ≌ C') (e' : D ≌ D'),
  (CategoryTheory.Join.mapPairEquiv e e').unitIso =
    CategoryTheory.Join.mapPairId.symm ≪≫
      CategoryTheory.Join.mapIsoWhiskerRight e.unitIso (CategoryTheory.Functor.id D) ≪≫
        CategoryTheory.Join.mapIsoWhiskerLeft (e.functor.comp e.inverse) e'.unitIso ≪≫
          CategoryTheory.Join.mapPairComp e.functor e'.functor e.inverse e'.inverse
-- Mathlib.ModelTheory.Basic
Equiv.inducedStructure_funMap : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] (e : M ≃ N) {n : ℕ} (f : L.Functions n)
  (x : Fin n → N), FirstOrder.Language.Structure.funMap f x = e (FirstOrder.Language.Structure.funMap f (⇑e.symm ∘ x))
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.subset_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] {s : Set α} {n : ℕ}, 0 ∈ s → n ≠ 0 → s ⊆ n • s
-- Std.Data.String.ToNat
String.toNat?_toSlice : ∀ {s : String}, s.toSlice.toNat? = s.toNat?
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instSMulCommClass_1 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
  SMulCommClass M Nᵒᵈ α
-- Mathlib.CategoryTheory.Galois.Topology
/-- We give `F.obj X  ⟶ F.obj Y` the product topology.  -/
CategoryTheory.PreGaloisCategory.instTopologicalSpaceHomFintypeCatObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) → {X Y : C} → TopologicalSpace (F.obj X ⟶ F.obj Y)
-- Mathlib.SetTheory.ZFC.Class
Class.instTop : Top Class.{u_1}
-- Init.Data.String.Termination
String.Slice.Pos.ne_endPos_of_next?_eq_some : ∀ {s : String.Slice} {p q : s.Pos}, p.next? = some q → p ≠ s.endPos
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHAddOffset_5 : HAdd Std.Time.PlainDateTime Std.Time.Second.Offset Std.Time.PlainDateTime
-- Mathlib.AlgebraicGeometry.Cover.Directed
/-- The transition map `𝒰ᵢ ⟶ 𝒰ⱼ` for `i ≤ j`.  -/
AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X} →
      {inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀} →
        [self : 𝒰.LocallyDirected] → {i j : 𝒰.I₀} → (i ⟶ j) → (𝒰.X i ⟶ 𝒰.X j)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.setPos : Lean.ParseImports.State → String.Pos.Raw → Lean.ParseImports.State
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.coe_inj : ∀ {α : Type u} {a b : α}, ↑a = ↑b ↔ a = b
-- Mathlib.Algebra.Star.StarAlgHom
/-- The identity as a `StarAlgHom`.  -/
StarAlgHom.id : (R : Type u_2) →
  (A : Type u_3) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [inst_3 : Star A] → A →⋆ₐ[R] A
-- Mathlib.Data.List.Enum
/-- Variant of `exists_mem_zipIdx` with the `zipIdx` argument specialized to `0`.  -/
List.exists_mem_zipIdx' : ∀ {α : Type u_1} {l : List α} {p : α × ℕ → Prop}, (∃ x ∈ l.zipIdx, p x) ↔ ∃ i, ∃ (x : i < l.length), p (l[i], i)
-- Mathlib.Analysis.Calculus.Taylor
/-- The Taylor polynomial of order zero evaluates to `f x`.  -/
taylor_within_zero_eval : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (s : Set ℝ) (x₀ x : ℝ),
  taylorWithinEval f 0 s x₀ x = f x₀
-- Init.Data.UInt.Basic
/-- Decides whether one 16-bit unsigned integer is strictly less than another. Usually accessed via the
`DecidableLT UInt16` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (6 : UInt16) < 7 then "yes" else "no") = "yes"`
 * `(if (5 : UInt16) < 5 then "yes" else "no") = "no"`
 * `show ¬((7 : UInt16) < 7) by decide`
 -/
UInt16.decLt : (a b : UInt16) → Decidable (a < b)
-- Mathlib.Analysis.Normed.Module.TransferInstance
/-- Transfer a `NormedAddCommGroup` across an `Equiv`  -/
Equiv.normedAddCommGroup : {α : Type u_1} → {β : Type u_2} → [NormedAddCommGroup β] → α ≃ β → NormedAddCommGroup α
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderParsedState.mk.injEq : ∀ (parserState : Lean.Parser.ModuleParserState)
  (processedSnap : Lean.Language.SnapshotTask Lean.Language.Lean.HeaderProcessedSnapshot)
  (parserState_1 : Lean.Parser.ModuleParserState)
  (processedSnap_1 : Lean.Language.SnapshotTask Lean.Language.Lean.HeaderProcessedSnapshot),
  ({ parserState := parserState, processedSnap := processedSnap } =
      { parserState := parserState_1, processedSnap := processedSnap_1 }) =
    (parserState = parserState_1 ∧ processedSnap = processedSnap_1)
-- Mathlib.AlgebraicGeometry.QuasiAffine
AlgebraicGeometry.Scheme.instIsSeparatedOfIsQuasiAffine : ∀ {X : AlgebraicGeometry.Scheme} [X.IsQuasiAffine], X.IsSeparated
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.mono_of_isZero_kernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y)
  [inst_2 : CategoryTheory.Limits.HasKernel f],
  CategoryTheory.Limits.IsZero (CategoryTheory.Limits.kernel f) → CategoryTheory.Mono f
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.ofBoolListBE.match_1.eq_1 : ∀ (motive : List Bool → Sort u_1) (h_1 : Unit → motive []) (h_2 : (b : Bool) → (bs : List Bool) → motive (b :: bs)),
  (match [] with
    | [] => h_1 ()
    | b :: bs => h_2 b bs) =
    h_1 ()
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexWF : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Ordering
-- Mathlib.Algebra.Ring.Pi
Pi.nonAssocRing : {I : Type u} → {f : I → Type v} → [(i : I) → NonAssocRing (f i)] → NonAssocRing ((i : I) → f i)
-- Mathlib.Algebra.Order.Quantale
AddQuantale.instAddRightMono : ∀ {α : Type u_1} [inst : AddSemigroup α] [inst_1 : CompleteLattice α] [IsAddQuantale α], AddRightMono α
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_eq_append : ∀ {m n : ℤ}, m + 1 < n → (m<...n).toList = (m<...n - 1).toList ++ [n - 1]
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.expandUnreachable : Lean.Macro
-- Mathlib.Geometry.Euclidean.Similarity
/-- If two triangles have two pairs equal angles, then the triangles are similar.  -/
EuclideanGeometry.similar_of_angle_angle : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedAddCommGroup V₁]
  [inst_1 : NormedAddCommGroup V₂] [inst_2 : InnerProductSpace ℝ V₁] [inst_3 : InnerProductSpace ℝ V₂]
  [inst_4 : MetricSpace P₁] [inst_5 : MetricSpace P₂] [inst_6 : NormedAddTorsor V₁ P₁] [inst_7 : NormedAddTorsor V₂ P₂]
  {a b c : P₁} {a' b' c' : P₂},
  ¬Collinear ℝ {a, b, c} →
    EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c' →
      EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a' → Similar ![a, b, c] ![a', b', c']
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hom_smul : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} {S : Type u_1} [inst_1 : Monoid S]
  [inst_2 : DistribMulAction S ↑N] [inst_3 : SMulCommClass R S ↑N] (s : S) (f : M ⟶ N),
  SemimoduleCat.Hom.hom (s • f) = s • SemimoduleCat.Hom.hom f
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.opcyclesMap_sub : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂) [inst_2 : S₁.HasRightHomology]
  [inst_3 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.opcyclesMap (φ - φ') =
    CategoryTheory.ShortComplex.opcyclesMap φ - CategoryTheory.ShortComplex.opcyclesMap φ'
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findIdx?_go_succ : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {i : ℕ},
  List.findIdx?.go p xs (i + 1) = Option.map (fun i => i + 1) (List.findIdx?.go p xs i)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
_private.Mathlib.Analysis.SpecialFunctions.Log.NegMulLog.0.Real.tendsto_deriv_mul_log_nhdsWithin_zero : Filter.Tendsto (deriv fun x => x * Real.log x) (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.mul_adjp_add_detp : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  (A : Matrix n n R), A * Matrix.adjp 1 A + Matrix.detp (-1) A • 1 = A * Matrix.adjp (-1) A + Matrix.detp 1 A • 1
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_same₁₃ : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b c : ℤ), IsEllipticNet.atomRel W a b a c = W a * W 0 * IsEllipticNet.atom W c b
-- Init.Data.UInt.Lemmas
UInt8.mul_sub : ∀ {a b c : UInt8}, a * (b - c) = a * b - a * c
-- Mathlib.Algebra.Ring.Defs
left_distrib : ∀ {R : Type v} [inst : Mul R] [inst_1 : Add R] [LeftDistribClass R] (a b c : R), a * (b + c) = a * b + a * c
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.subLeft_apply : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd G G]
  [inst_3 : IsIsometricVAdd Gᵃᵒᵖ G] (c b : G), (IsometryEquiv.subLeft c) b = c - b
-- Mathlib.Analysis.Convex.Star
StarConvex.add_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x : E} {s : Set E}, StarConvex 𝕜 x s → ∀ (z : E), StarConvex 𝕜 (x + z) ((fun x => x + z) '' s)
-- Mathlib.Order.Irreducible
infIrred_toDual : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, InfIrred (OrderDual.toDual a) ↔ SupIrred a
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- The integral of a function which is nonnegative almost everywhere is nonnegative.  -/
MeasureTheory.integral_nonneg_of_ae : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
  [ClosedIciTopology E] {f : α → E}, 0 ≤ᵐ[μ] f → 0 ≤ ∫ (x : α), f x ∂μ
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Bundled exact functors.  -/
CategoryTheory.ExactFunctor : (C : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [CategoryTheory.Category.{v₂, u₂} D] → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.Algebra.Category.Grp.Basic
/-- The forgetful functor from commutative groups to groups is fully faithful.  -/
CommGrpCat.fullyFaithfulForget₂ToGrp : (CategoryTheory.forget₂ CommGrpCat GrpCat).FullyFaithful
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIso_right_H : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : S₁.HomologyData),
  (CategoryTheory.ShortComplex.HomologyData.ofIso e h).right.H = h.right.H
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.fst_decompEquiv : ∀ (R : Type u_1) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace Q]
  [inst_10 : IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q), ((ContinuousAffineMap.decompEquiv R V Q) f).1 = f 0
-- Mathlib.RingTheory.MvPowerSeries.Substitution
/-- Families of `MvPowerSeries` that can be substituted, as an `Ideal`  -/
MvPowerSeries.hasSubstIdeal : {σ : Type u_1} → {τ : Type u_4} → {S : Type u_5} → [inst : CommRing S] → Ideal (σ → MvPowerSeries τ S)
-- Lean.Elab.DocString
/-- Returns the syntax from which a documentation argument was drawn, typically used to report errors.
 -/
Lean.Doc.DocArg.syntax : Lean.Doc.DocArg → Lean.Syntax
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- Signs for terms of Euler characteristic on complexes.  -/
ComplexShape.EulerCharSigns : {ι : Type u_1} → ComplexShape ι → Type u_1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.mergeWith_eq_mergeWith! : ∀ {α : Type u} {β : Type v} {x : Ord α} {mergeFn : α → β → β → β} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β}
  (h : t₁.Balanced),
  (Std.DTreeMap.Internal.Impl.Const.mergeWith mergeFn t₁ t₂ h).impl =
    Std.DTreeMap.Internal.Impl.Const.mergeWith! mergeFn t₁ t₂