mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_dep_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {M : Matroid α} {hf : Set.InjOn f M.E} {D : Set β},
  (M.map f hf).Dep D ↔ ∃ D₀, M.Dep D₀ ∧ D = f '' D₀
-- Mathlib.Analysis.Normed.Group.Continuity
NormedAddGroup.toENormedAddMonoid : {F : Type u_7} → [inst : NormedAddGroup F] → ENormedAddMonoid F
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.id
      ((CategoryTheory.CategoryStruct.id (F.obj b)).toFunctor.obj ((F.map f).toFunctor.obj X)) =
    CategoryTheory.CategoryStruct.comp ((F.mapId b).toNatTrans.app ((F.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).toNatTrans.app X)
        ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X))
-- Mathlib.Order.Filter.Basic
Filter.instNeBotTop : ∀ {α : Type u} [Nonempty α], ⊤.NeBot
-- Mathlib.Algebra.Ring.Commute
Commute.add_sq : ∀ {R : Type u} [inst : Semiring R] {a b : R}, Commute a b → (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_inter_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], (m₁ ∩ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∉ m₂
-- Mathlib.Algebra.Prime.Lemmas
IsRelPrime.of_map : ∀ {M : Type u_3} {N : Type u_4} {F : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : FunLike F M N]
  [MulHomClass F M N] (f : F) [IsLocalHom f] {a b : M}, IsRelPrime (f a) (f b) → IsRelPrime a b
-- Mathlib.Topology.Sheaves.CommRingCat
/-- `F(U ⊔ V)` is isomorphic to the `eq_locus` of the two maps `F(U) × F(V) ⟶ F(U ⊓ V)`.  -/
TopCat.Sheaf.objSupIsoProdEqLocus : {X : TopCat} →
  (F : TopCat.Sheaf CommRingCat X) →
    (U V : TopologicalSpace.Opens ↑X) →
      F.obj.obj (Opposite.op (U ⊔ V)) ≅
        CommRingCat.of
          ↥(((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp
                  (RingHom.fst ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))).eqLocus
              ((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp
                (RingHom.snd ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))))
-- Mathlib.RingTheory.LocalProperties.Reduced
/-- `R` is reduced if `Rₘ` is reduced for all maximal ideal `m`.  -/
isReduced_ofLocalizationMaximal : OfLocalizationMaximal fun R x => IsReduced R
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E},
  ProbabilityTheory.IsAEKolmogorovProcess X P p q M →
    ∀ {s t : T}, edist s t = 0 → ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.bijective_comp_algebraMap : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  (L : Type u_2) [inst_4 : Field L] [PerfectField L], Function.Bijective fun f => f.comp (algebraMap F E)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedState.default : Lean.Elab.Term.State
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.trans.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (h1 : M ≃* N)
  (h2 : N ≃* P), h1.trans h2 = { toEquiv := h1.trans h2.toEquiv, map_mul' := ⋯ }
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropEndWhile_dropEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, (s.dropEndWhile pat).dropEndWhile pat = s.dropEndWhile pat
-- Mathlib.Combinatorics.SimpleGraph.Sum
_private.Mathlib.Combinatorics.SimpleGraph.Sum.0.SimpleGraph.edgeSetSumEquiv.match_1.eq_1 : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}
  (motive : (x x_1 : V ⊕ W) → (G ⊕g H).Adj x x_1 → Sort u_3) (u v : V) (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inl v))
  (h_1 : (u v : V) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)) → motive (Sum.inl u) (Sum.inl v) h)
  (h_2 : (u v : W) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)) → motive (Sum.inr u) (Sum.inr v) h)
  (h_3 : (u : V) → (v : W) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)) → motive (Sum.inl u) (Sum.inr v) h)
  (h_4 : (u : W) → (v : V) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)) → motive (Sum.inr u) (Sum.inl v) h),
  (match Sum.inl u, Sum.inl v, h with
    | Sum.inl u, Sum.inl v, h => h_1 u v h
    | Sum.inr u, Sum.inr v, h => h_2 u v h
    | Sum.inl u, Sum.inr v, h => h_3 u v h
    | Sum.inr u, Sum.inl v, h => h_4 u v h) =
    h_1 u v h
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.le_inf_support_coeff_finsetProd`. -/
AddMonoidAlgebra.le_inf_support_finset_prod : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} {ι : Type u_6} [inst : SemilatticeInf T] [inst_1 : OrderTop T]
  [inst_2 : CommSemiring R] [inst_3 : AddCommMonoid A] [inst_4 : AddCommMonoid T] [AddLeftMono T] [AddRightMono T]
  {degt : A → T},
  0 ≤ degt 0 →
    (∀ (a b : A), degt a + degt b ≤ degt (a + b)) →
      ∀ (s : Finset ι) (f : ι → AddMonoidAlgebra R A),
        ∑ i ∈ s, (f i).coeff.support.inf degt ≤ (∏ i ∈ s, f i).coeff.support.inf degt
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_adjugate : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  (h : IsUnit A.det), A.adjugate⁻¹ = h.unit⁻¹ • A
-- Init.Data.SInt.Lemmas
Int32.zero_div : ∀ {a : Int32}, 0 / a = 0
-- Mathlib.Topology.EMetricSpace.Defs
/-- Creating a uniform space from an extended distance.  -/
uniformSpaceOfEDist : {α : Type u} →
  (edist : α → α → ENNReal) →
    (∀ (x : α), edist x x = 0) →
      (∀ (x y : α), edist x y = edist y x) → (∀ (x y z : α), edist x z ≤ edist x y + edist y z) → UniformSpace α
-- Aesop.RuleTac.Forward.Basic
/-- Depths of the hypotheses that have already been added by forward reasoning.
 -/
Aesop.ForwardHypData.depths : Aesop.ForwardHypData → Std.HashMap Lean.FVarId ℕ
-- Init.System.ST
ST.Prim.Ref.modifyUnsafe : {σ α : Type} → ST.Ref σ α → (α → α) → ST σ Unit
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgEquiv.toCoalgIso_hom : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module R Y] [inst_5 : Coalgebra R X] [inst_6 : Coalgebra R Y] (e : X ≃ₗc[R] Y),
  e.toCoalgIso.hom = CoalgCat.ofHom ↑e
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAdd : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [Add M] → Add (l.Germ M)
-- Mathlib.Data.List.Nodup
List.Nodup.mem_sdiff_iff : ∀ {α : Type u} {l₁ l₂ : List α} {a : α} [inst : BEq α] [LawfulBEq α], l₁.Nodup → (a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ a ∉ l₂)
-- Init.Data.SInt.Basic
instOrOpInt16 : OrOp Int16
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {i : Set α},
  MeasurableSet i → μ.toENNRealVectorMeasure i = μ i
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanIleanInfoParams.mk : ℕ → Lean.Lsp.ModuleRefs → Lean.Lsp.Decls → Lean.Lsp.LeanIleanInfoParams
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- A commutative ring object in a cartesian monoidal category is a
ring object such that the multiplicative law is commutative.  -/
CategoryTheory.CommRingObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → [CategoryTheory.BraidedCategory C] → C → Type v
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyMap_sub : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ ψ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i],
  HomologicalComplex.homologyMap (φ - ψ) i = HomologicalComplex.homologyMap φ i - HomologicalComplex.homologyMap ψ i
-- Lean.LocalContext
Lean.LocalContext.renameUserName : Lean.LocalContext → Lean.Name → Lean.Name → Lean.LocalContext
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueSums.of_injective_addHom : ∀ {G : Type u} {H : Type v} [inst : Add G] [inst_1 : Add H] (f : H →ₙ+ G),
  Function.Injective ⇑f → UniqueSums G → UniqueSums H
-- Mathlib.Topology.Order.LeftRightLim
Monotone.tendsto_leftLim_within : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f →
    ∀ [inst_4 : TopologicalSpace α] [OrderTopology α] (x : α),
      Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhdsWithin (Function.leftLim f x) (Set.Iic (Function.leftLim f x)))
-- Mathlib.Analysis.Analytic.Constructions
analyticAt_inv_one_add : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] (𝕝 : Type u_8) [inst_1 : NormedDivisionRing 𝕝]
  [inst_2 : NormedAlgebra 𝕜 𝕝], AnalyticAt 𝕜 (fun x => (1 + x)⁻¹) 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_drop : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.drop n).IsSubwalk p
-- Mathlib.RingTheory.Polynomial.ShiftedLegendre
Polynomial.natDegree_shiftedLegendre : ∀ (n : ℕ), (Polynomial.shiftedLegendre n).natDegree = n
-- Mathlib.Topology.Category.Born
Born.instInhabited : Inhabited Born
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.eq_of_src : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C},
  CategoryTheory.Limits.IsZero X → ∀ (f g : X ⟶ Y), f = g
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMkSucc.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C (n + 1)}
  (α α_1 : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯) (e_α : α = α_1) (β β_1 : F.δ₀ ≅ G.δ₀) (e_β : β = β_1)
  (w :
    CategoryTheory.CategoryStruct.comp (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)
        (CategoryTheory.ComposableArrows.app' β.hom 0 ⋯) =
      CategoryTheory.CategoryStruct.comp α.hom (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)),
  CategoryTheory.ComposableArrows.isoMkSucc α β w = CategoryTheory.ComposableArrows.isoMkSucc α_1 β_1 ⋯
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The canonical linear map interpreting an element of `M` as
a section of the structure sheaf.  -/
AlgebraicGeometry.StructureSheaf.toOpenₗ : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
          M →ₗ[R] (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op U)
-- Mathlib.Data.UInt
/-- To use this instance, use `open scoped UInt16.CommRing`.

See the module docstring for an explanation -/
UInt16.instCommRing : CommRing UInt16
-- Mathlib.Algebra.Notation
/-- The *positive part* of an element `a`.  -/
«term_⁺ᵐ» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.nearestPtInd.congr_simp : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  (e e_1 : ℕ → α),
  e = e_1 →
    ∀ (a a_1 : ℕ), a = a_1 → MeasureTheory.SimpleFunc.nearestPtInd e a = MeasureTheory.SimpleFunc.nearestPtInd e_1 a_1
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.ofBoolListBE.match_1.splitter : (motive : List Bool → Sort u_1) →
  (x : List Bool) → (Unit → motive []) → ((b : Bool) → (bs : List Bool) → motive (b :: bs)) → motive x
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instZero : {α : Type u_1} → [AddCommGroup α] → [inst : Preorder α] → Zero (UpperSet α)
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- The ring homomorphism version of `FractionalIdeal.extended`.
See `FractionalIdeal.extendedHom` for a more convenient version that is often enough.
 -/
FractionalIdeal.extendedHom' : {A : Type u_1} →
  [inst : CommRing A] →
    {B : Type u_2} →
      [inst_1 : CommRing B] →
        {f : A →+* B} →
          {K : Type u_3} →
            {M : Submonoid A} →
              [inst_2 : CommRing K] →
                [inst_3 : Algebra A K] →
                  [IsLocalization M K] →
                    (L : Type u_4) →
                      {N : Submonoid B} →
                        [inst_5 : CommRing L] →
                          [inst_6 : Algebra B L] →
                            [IsLocalization N L] → M ≤ Submonoid.comap f N → FractionalIdeal M K →+* FractionalIdeal N L
-- Mathlib.MeasureTheory.PiSystem
/-- A π-system is a collection of subsets of `α` that is closed under binary intersection of
non-disjoint sets. Usually it is also required that the collection is nonempty, but we don't do
that here.  -/
IsPiSystem : {α : Type u_1} → Set (Set α) → Prop
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.apply_none : ∀ {α : Type u_5} {ι : Type u_6} (l : Combinatorics.Line α ι) (x : α) (i : ι), l.idxFun i = none → ↑l x i = x
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
HasDerivWithinAt.clog_real : ∀ {f : ℝ → ℂ} {s : Set ℝ} {x : ℝ} {f' : ℂ},
  HasDerivWithinAt f f' s x → f x ∈ Complex.slitPlane → HasDerivWithinAt (fun t => Complex.log (f t)) (f' / f x) s x
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_inv_eq : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → z ≠ 0 → (x ^ z⁻¹ = y ↔ x = y ^ z)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.comp_zero : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₂ V₃), f.comp 0 = 0
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_tsupport : ∀ {X : Type u_1} {M : Type u_5} [inst : NormedAddCommGroup M] [inst_1 : NormedSpace ℝ M] {mX : MeasurableSpace X}
  {ν : MeasureTheory.Measure X} {F : X → M} [inst_2 : TopologicalSpace X],
  ∫ (x : X) in tsupport F, F x ∂ν = ∫ (x : X), F x ∂ν
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.add_add_of_nonneg : ∀ {α : Type u_1} {u v t w : α → ℝ} {l : Filter α},
  0 ≤ v →
    0 ≤ w → Asymptotics.IsEquivalent l u v → Asymptotics.IsEquivalent l t w → Asymptotics.IsEquivalent l (u + t) (v + w)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.toList.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DHashMap.Internal.AssocList.nil.toList = []
-- Std.Sat.AIG.RelabelNat
/-- `relabelNat` preserves unsatisfiablility.
 -/
Std.Sat.AIG.relabelNat_unsat_iff : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {idx : ℕ} {invert : Bool} {aig : Std.Sat.AIG α}
  {hidx1 : idx < aig.relabelNat.decls.size} {hidx2 : idx < aig.decls.size},
  aig.relabelNat.UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2
-- Mathlib.Order.Irreducible
/-- An inf-prime element is a non-top element which isn't bigger than the infimum of anything
bigger.  -/
InfPrime : {α : Type u_2} → [SemilatticeInf α] → α → Prop
-- Init.Data.Vector.Lemmas
Vector.sum_eq_foldl : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] [inst_1 : Add α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0] {xs : Vector α n}, xs.sum = Vector.foldl (fun x1 x2 => x1 + x2) 0 xs
-- Mathlib.Probability.Kernel.Condexp
MeasureTheory.StronglyMeasurable.integral_condExpKernel : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F}
  [inst_3 : NormedSpace ℝ F],
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
/-- The linear map from a given `R`-module in the diagram to the colimit module.  -/
ModuleCat.FilteredColimits.coconeMorphism : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.IsFiltered J] →
          (F : CategoryTheory.Functor J (ModuleCat R)) → (j : J) → F.obj j ⟶ ModuleCat.FilteredColimits.colimit F
-- Mathlib.Data.Seq.Computation
Computation.mem_map : ∀ {α : Type u} {β : Type v} (f : α → β) {a : α} {s : Computation α}, a ∈ s → f a ∈ Computation.map f s
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.Plus.instIsIsoAppOfInjectiveXIntAsHomologicalComplexUpHomotopicObjPlus : ∀ {C : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} H] [CategoryTheory.EnoughInjectives C]
  (F : CategoryTheory.Functor (HomotopyCategory.Plus C) H) [inst_4 : HasDerivedCategory C]
  (F' : CategoryTheory.Functor (DerivedCategory.Plus C) H) (α : F ⟶ DerivedCategory.Plus.Qh.comp F')
  [F'.IsRightDerivedFunctor α (HomotopyCategory.Plus.quasiIso C)] (K : HomotopyCategory.Plus C)
  [∀ (n : ℤ), CategoryTheory.Injective (K.obj.as.X n)], CategoryTheory.IsIso (α.app K)
-- Init.Data.UInt.Lemmas
UInt16.toNat_mod_lt : ∀ {m : ℕ} (u : UInt16), 0 < m → (u % UInt16.ofNat m).toNat < m
-- Mathlib.Logic.ExistsUnique
existsUnique_congr : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∃! a, p a) ↔ ∃! a, q a)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.mem_edgeSet : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {e : Sym2 V}, e ∈ p.edgeSet ↔ e ∈ p.edges
-- Aesop.Index.Basic
Aesop.IndexingMode.or : Array Aesop.IndexingMode → Aesop.IndexingMode
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.summable_exp_nat_mul_iff : ∀ {a : ℝ}, (Summable fun n => Real.exp (↑n * a)) ↔ a < 0
-- Init.Data.Int.Order
Int.mul_pos : ∀ {a b : ℤ}, 0 < a → 0 < b → 0 < a * b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_le_size_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)}, t.size - 1 ≤ (t.alter k f).size
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_const_nsmul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] (n : ℕ),
  UniformContinuous fun x => n • x
-- Init.WFExtrinsicFix
WellFounded.partialExtrinsicFix₃_eq_fix : ∀ {α : Sort u_2} {β : α → Sort u_4} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_1}
  [inst : ∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)]
  {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
  {F :
    (a : α) →
      (b : β a) →
        (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c}
  (wf : WellFounded R) {a : α} {b : β a} {c : γ a b},
  WellFounded.partialExtrinsicFix₃ R F a b c =
    wf.fix (fun x G => F x.fst x.snd.fst x.snd.snd fun a b c h => G ⟨a, ⟨b, c⟩⟩ h) ⟨a, ⟨b, c⟩⟩
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.beq.match_1.splitter : (motive : Lean.Name → Lean.Name → Sort u_1) →
  (x x_1 : Lean.Name) →
    (Unit → motive Lean.Name.anonymous Lean.Name.anonymous) →
      ((p₁ : Lean.Name) → (s₁ : String) → (p₂ : Lean.Name) → (s₂ : String) → motive (p₁.str s₁) (p₂.str s₂)) →
        ((p₁ : Lean.Name) → (n₁ : ℕ) → (p₂ : Lean.Name) → (n₂ : ℕ) → motive (p₁.num n₁) (p₂.num n₂)) →
          ((x x_2 : Lean.Name) →
              (x = Lean.Name.anonymous → x_2 = Lean.Name.anonymous → False) →
                (∀ (p₁ : Lean.Name) (s₁ : String) (p₂ : Lean.Name) (s₂ : String),
                    x = p₁.str s₁ → x_2 = p₂.str s₂ → False) →
                  (∀ (p₁ : Lean.Name) (n₁ : ℕ) (p₂ : Lean.Name) (n₂ : ℕ), x = p₁.num n₁ → x_2 = p₂.num n₂ → False) →
                    motive x x_2) →
            motive x x_1
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : outParam (C → C → Type u_1)} →
      {CC : outParam (C → Type w)} →
        [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] →
          (hom : {X Y : C} → (X ⟶ Y) → FC X Y) →
            (ofHom : {X Y : C} → FC X Y → (X ⟶ Y)) →
              autoParam (∀ {X Y : C} (f : FC X Y), hom (ofHom f) = f)
                  CategoryTheory.ConcreteCategory.hom_ofHom._autoParam →
                autoParam (∀ {X Y : C} (f : X ⟶ Y), ofHom (hom f) = f)
                    CategoryTheory.ConcreteCategory.ofHom_hom._autoParam →
                  autoParam (∀ {X : C} (x : CC X), (hom (CategoryTheory.CategoryStruct.id X)) x = x)
                      CategoryTheory.ConcreteCategory.id_apply._autoParam →
                    autoParam
                        (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X),
                          (hom (CategoryTheory.CategoryStruct.comp f g)) x = (hom g) ((hom f) x))
                        CategoryTheory.ConcreteCategory.comp_apply._autoParam →
                      CategoryTheory.ConcreteCategory C FC
-- Mathlib.Order.Filter.AtTopBot.Finite
Nat.eventually_mul_pow_lt_factorial_sub : ∀ (a c d : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, a * c ^ n < (n - d).factorial
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SSameSide.left_notMem : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SSameSide x y → x ∉ s
-- Lean.Elab.PreDefinition.EqnsUtils
/-- Delta reduce the equation left-hand-side  -/
Lean.Elab.Eqns.deltaLHS : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.dual_injective_of_surjective : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {B : Type uB} [inst_2 : AddCommGroup B]
  [inst_3 : Module R A] [inst_4 : Module R B] (f : A →ₗ[R] B),
  Function.Surjective ⇑f → Function.Injective ⇑(CharacterModule.dual f)
-- Mathlib.Order.Bounds.Basic
isGLB_lt_isLUB_of_ne : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {a b : α},
  IsGLB s a → IsLUB s b → ∀ {x y : α}, x ∈ s → y ∈ s → x ≠ y → a < b
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b),
  sizeOf (CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv f) = 1 + sizeOf a + sizeOf b + sizeOf f
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (retraction : Y ⟶ X)
  (id :
    autoParam (CategoryTheory.CategoryStruct.comp f retraction = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.SplitMono.id._autoParam)
  (retraction_1 : Y ⟶ X)
  (id_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f retraction_1 = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.SplitMono.id._autoParam),
  ({ retraction := retraction, id := id } = { retraction := retraction_1, id := id_1 }) = (retraction = retraction_1)
-- Init.Data.List.Find
List.findIdx?_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} {p : α → Bool},
  List.findIdx? p (List.replicate n a) = if 0 < n ∧ p a = true then some 0 else none
-- Mathlib.RingTheory.Discriminant
Algebra.discr.congr_simp : ∀ {ι : Type w} {inst : DecidableEq ι} [inst_1 : DecidableEq ι] (A : Type u) {B : Type v} [inst_2 : CommRing A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] [inst_5 : Fintype ι] (b b_1 : ι → B),
  b = b_1 → Algebra.discr A b = Algebra.discr A b_1