mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.failedToGenHInj : {α : Type} → Lean.ConstructorVal → Lean.MetaM α
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.map_distinguished : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] [inst_6 : CategoryTheory.Limits.HasZeroObject D]
  [inst_7 : CategoryTheory.Preadditive C] [inst_8 : CategoryTheory.Preadditive D]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_11 : CategoryTheory.Pretriangulated C]
  [inst_12 : CategoryTheory.Pretriangulated D] [F.IsTriangulated],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Aesop.Util.EqualUpToIds
_private.Aesop.Util.EqualUpToIds.0.Aesop.EqualUpToIds.lctxDecls : Lean.LocalContext → Aesop.EqualUpToIdsM (Array Lean.LocalDecl)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induceHomOfLE_apply : ∀ {V : Type u_1} (G : SimpleGraph V) {s s' : Set V} (h : s ⊆ s') (v : ↑s), (G.induceHomOfLE h) v = Set.inclusion h v
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.comp_id : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β)),
  f.comp (ContinuousMap.id α) = f
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that all denominators are nonnegative.  -/
GenContFract.zero_le_of_den : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K], 0 ≤ (GenContFract.of v).dens n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A kernel fork for the kernel of `biprod.snd`. It consists of the
morphism `biprod.inl`.  -/
CategoryTheory.Limits.biprod.sndKernelFork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
          CategoryTheory.Limits.KernelFork CategoryTheory.Limits.biprod.snd
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_sInf : ∀ {G : Type u_1} [inst : AddGroup G] {Hs : Set (AddSubgroup G)}, (∀ H ∈ Hs, H.Characteristic) → (sInf Hs).Characteristic
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.cokernelUnopUnop_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  (CategoryTheory.cokernelUnopUnop g).hom =
    CategoryTheory.Limits.cokernel.desc g.unop (CategoryTheory.Limits.kernel.ι g).unop ⋯
-- Lean.Parser.Basic
Lean.Parser.RecoveryContext.mk : String.Pos.Raw → ℕ → Lean.Parser.RecoveryContext
-- Mathlib.CategoryTheory.Adjunction.Quadruple
/-- Adjunction `F ⊣ G` of the adjoint quadruple `L ⊣ F ⊣ G ⊣ R`.  -/
CategoryTheory.Adjunction.Quadruple.adj₂ : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {F : CategoryTheory.Functor D C} →
            {G : CategoryTheory.Functor C D} →
              {R : CategoryTheory.Functor D C} → CategoryTheory.Adjunction.Quadruple L F G R → (F ⊣ G)
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientEquivProdOfLE_apply : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (h_le : s ≤ t) (a : α ⧸ s),
  (Subgroup.quotientEquivProdOfLE h_le) a =
    (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨(Quotient.mk'' g).out⁻¹ * g, ⋯⟩) ⋯ a)
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
StandardSubspace.mk : {H : Type u_1} →
  [inst : NormedAddCommGroup H] →
    [inst_1 : InnerProductSpace ℂ H] →
      (toClosedSubmodule : ClosedSubmodule ℝ H) →
        toClosedSubmodule ⊓ toClosedSubmodule.mulI = ⊥ →
          toClosedSubmodule ⊔ toClosedSubmodule.mulI = ⊤ → StandardSubspace H
-- Lean.Widget.InteractiveGoal
/-- The hypothesis is a typeclass instance.  -/
Lean.Widget.InteractiveHypothesisBundle.isInstance? : Lean.Widget.InteractiveHypothesisBundle → Option Bool
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- The component 1-morphisms of an oplax transformation.  -/
CategoryTheory.Lax.OplaxTrans.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → CategoryTheory.Lax.OplaxTrans F G → (a : B) → F.obj a ⟶ G.obj a
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_eq_some_getElem!_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α}, m.contains a = true → m[a]? = some m[a]!
-- Lean.Elab.Binders
Lean.Elab.Term.LetIdDeclView : Type
-- Mathlib.Data.Int.Init
Int.inductionOn'.neg.hcongr_5 : ∀ (motive motive' : ℤ → Sort u_1),
  motive = motive' →
    ∀ (b b' : ℤ),
      b = b' →
        ∀ (zero : motive b) (zero' : motive' b'),
          zero ≍ zero' →
            ∀ (pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1))
              (pred' : (k : ℤ) → k ≤ b' → motive' k → motive' (k - 1)),
              pred ≍ pred' →
                ∀ (n n' : ℕ), n = n' → Int.inductionOn'.neg b zero pred n ≍ Int.inductionOn'.neg b' zero' pred' n'
-- Mathlib.Order.CountableSupClosed
/-- **Alias** of the reverse direction of `countableInfClosed_preimage_ofDual`. -/
CountableSupClosed.dual : ∀ {α : Type u_2} [inst : LE α] {s : Set α}, CountableSupClosed s → CountableInfClosed (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
IsBilinearMap.toContinuousBilinearMap_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2} [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [inst_5 : IsTopologicalAddGroup E] [inst_6 : ContinuousSMul 𝕜 E]
  [inst_7 : FiniteDimensional 𝕜 E] [inst_8 : T2Space E] {F : Type u_3} [inst_9 : AddCommGroup F] [inst_10 : Module 𝕜 F]
  [inst_11 : TopologicalSpace F] [inst_12 : IsTopologicalAddGroup F] [inst_13 : ContinuousSMul 𝕜 F]
  [inst_14 : FiniteDimensional 𝕜 F] [inst_15 : T2Space F] {G : Type u_4} [inst_16 : AddCommGroup G]
  [inst_17 : Module 𝕜 G] [inst_18 : TopologicalSpace G] [inst_19 : IsTopologicalAddGroup G]
  [inst_20 : ContinuousSMul 𝕜 G] {f : E → F → G} (h : IsBilinearMap 𝕜 f) (x : E) (y : F),
  (h.toContinuousBilinearMap x) y = f x y
-- Init.Data.List.Lemmas
List.mem_of_mem_getLast? : ∀ {α : Type u_1} {l : List α} {a : α}, a ∈ l.getLast? → a ∈ l
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.homeomorph_comp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f → ∀ {Y : Type u_3} [inst_2 : TopologicalSpace Y] (g : X ≃ₜ Y), IsCoveringMap (⇑g ∘ f)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.instIteratorIteratorIdOfUpwardEnumerable.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α],
  Std.Rxi.instIteratorIteratorIdOfUpwardEnumerable =
    { IsPlausibleStep := fun it step => step = Std.Rxi.Iterator.Monadic.step it,
      step := fun it => pure (Std.Shrink.deflate ⟨Std.Rxi.Iterator.Monadic.step it, ⋯⟩) }
-- Std.Time.Time.Unit.Basic
/-- Converts an `Hour.Offset` to a `Nanosecond.Offset`.
 -/
Std.Time.Nanosecond.Offset.ofHours : Std.Time.Hour.Offset → Std.Time.Nanosecond.Offset
-- Mathlib.Logic.Encodable.Basic
Encodable.encodeSum.eq_2 : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Encodable β] (b : β),
  Encodable.encodeSum (Sum.inr b) = 2 * Encodable.encode b + 1
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalSubst : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_add_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (n : σ) (f g : MvPolynomial σ R),
  MvPolynomial.degreeOf n (f + g) ≤ max (MvPolynomial.degreeOf n f) (MvPolynomial.degreeOf n g)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The `Subsemiring` generated by a set.  -/
Subsemiring.closure : {R : Type u} → [inst : NonAssocSemiring R] → Set R → Subsemiring R
-- Init.Data.List.Control
List.forIn' : {α : Type u} →
  {β : Type v} → {m : Type v → Type w} → [Monad m] → (as : List α) → β → ((a : α) → a ∈ as → β → m (ForInStep β)) → m β
-- Mathlib.Topology.Order.MonotoneConvergence
Pi.supConvergenceClass' : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder α] [inst_1 : TopologicalSpace α] [SupConvergenceClass α],
  SupConvergenceClass (ι → α)
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.isRightInversion_simple_iff_isRightDescent : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B),
  cs.IsRightInversion w (cs.simple i) ↔ cs.IsRightDescent w i
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k : α}
  {h' : k ∈ Std.HashMap.Raw.filterMap f m} (h : m.WF), (Std.HashMap.Raw.filterMap f m).getKey k h' = m.getKey k ⋯
-- Mathlib.Topology.Instances.CantorSet
/-- The ternary Cantor set is closed.  -/
isClosed_cantorSet : IsClosed cantorSet
-- Mathlib.Analysis.Real.Sqrt
Filter.Tendsto.sqrt : ∀ {α : Type u_1} {f : α → ℝ} {l : Filter α} {x : ℝ},
  Filter.Tendsto f l (nhds x) → Filter.Tendsto (fun x => √(f x)) l (nhds √x)
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer.ι_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer.ι f g) A.ι =
    (CategoryTheory.Subfunctor.equalizer f g).ι
-- Mathlib.Order.Category.BoolAlg
_private.Mathlib.Order.Category.BoolAlg.0.BoolAlg.Hom.mk : {X Y : BoolAlg} → BoundedLatticeHom ↑X ↑Y → X.Hom Y
-- Batteries.Data.String.Matcher
/-- Returns true iff `pattern` occurs as a substring of `s`.
 -/
Substring.Raw.containsSubstr : Substring.Raw → Substring.Raw → Bool
-- Init.Data.String.Basic
String.lt_next : ∀ (s : String) (i : String.Pos.Raw), i.byteIdx < (String.Pos.Raw.next s i).byteIdx
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The type of morphisms in the category `Over`.  -/
CategoryTheory.Over.Hom : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} → CategoryTheory.Over X → CategoryTheory.Over X → Type (max v₁ 0)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.HasFiniteIntegral.restrict_of_bounded_enorm : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {C : ENNReal},
  autoParam (‖C‖ₑ ≠ ⊤) MeasureTheory.HasFiniteIntegral.restrict_of_bounded_enorm._auto_1 →
    autoParam (μ s ≠ ⊤) MeasureTheory.HasFiniteIntegral.restrict_of_bounded_enorm._auto_3 →
      (∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ₑ ≤ C) → MeasureTheory.HasFiniteIntegral f (μ.restrict s)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.UnfoldLift.monadLift_refl : ∀ {m : Type u → Type v} {α : Type u} (x : m α), monadLift x = x
-- Mathlib.Algebra.Module.BigOperators
Multiset.sum_smul_sum : ∀ {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Multiset R}
  {t : Multiset M}, s.sum • t.sum = (Multiset.map (fun p => p.1 • p.2) (s ×ˢ t)).sum
-- Mathlib.Topology.Instances.AddCircle.Defs
_private.Mathlib.Topology.Instances.AddCircle.Defs.0.AddCircle.term𝕋 : Lean.ParserDescr
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.le_of_le_cert.match_1.splitter : (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) →
  (p₁ p₂ : Int.Internal.Linear.Poly) →
    ((k : ℤ) →
        (v : Int.Internal.Linear.Var) →
          (p : Int.Internal.Linear.Poly) →
            (k_1 : ℤ) → motive (Int.Internal.Linear.Poly.add k v p) (Int.Internal.Linear.Poly.num k_1)) →
      ((k k_1 : ℤ) →
          (v : Int.Internal.Linear.Var) →
            (p : Int.Internal.Linear.Poly) →
              motive (Int.Internal.Linear.Poly.num k) (Int.Internal.Linear.Poly.add k_1 v p)) →
        ((c₁ c₂ : ℤ) → motive (Int.Internal.Linear.Poly.num c₁) (Int.Internal.Linear.Poly.num c₂)) →
          ((a₁ : ℤ) →
              (x₁ : Int.Internal.Linear.Var) →
                (p₁ : Int.Internal.Linear.Poly) →
                  (a₂ : ℤ) →
                    (x₂ : Int.Internal.Linear.Var) →
                      (p₂ : Int.Internal.Linear.Poly) →
                        motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)) →
            motive p₁ p₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a fallback : α}, Std.DTreeMap.Internal.Impl.contains a t = true → t.getKey? a = some (t.getKeyD a fallback)
-- Mathlib.RepresentationTheory.Coinduced
/-- If `φ : G →* H` and `A : Rep k G` then `coind' φ A`, the coinduction of `A` along `φ`,
is defined as an `H`-action on `Hom_{k[G]}(k[H], A)`. If `f : k[H] → A` is `G`-equivariant
then `(h • f) (r • h₁) := r • f (h₁ * h)`, where `r : k`.
 -/
Rep.coind' : {k : Type u} →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] → [inst_2 : Monoid H] → (G →* H) → Rep.{max u w, u, v} k G → Rep.{max u w, u, w} k H
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm of an integer is at most `1`.  -/
padicNorm.of_int : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ), padicNorm p ↑z ≤ 1
-- Lean.Elab.Deriving.Basic
Lean.Elab.derivingHandlersRef : IO.Ref (Lean.NameMap (List Lean.Elab.DerivingHandler))
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.coeq.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  {k k' : ℕ} {hk : k < n} {hk' : k' < n} {j : (X k hk).fst} {j' : (X k' hk').fst}
  {a a_1 : (X k hk).snd j ⟶ (X k' hk').snd j'} {k_1 k'_1 : ℕ} {hk_1 : k_1 < n} {hk'_1 : k'_1 < n}
  {j_1 : (X k_1 hk_1).fst} {j'_1 : (X k'_1 hk'_1).fst} {a_2 a_3 : (X k_1 hk_1).snd j_1 ⟶ (X k'_1 hk'_1).snd j'_1},
  CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.coeq✝ hk hk' j j' a a_1 =
      CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.coeq✝ hk_1 hk'_1 j_1 j'_1 a_2 a_3 →
    k = k_1 ∧ k' = k'_1 ∧ j ≍ j_1 ∧ j' ≍ j'_1 ∧ a ≍ a_2 ∧ a_1 ≍ a_3
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_bind_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.minKey?.bind t.getKey? = t.minKey?
-- Lean.Parser.Command
/-- Syntax quotation for terms.  -/
Lean.Parser.Term.quot : Lean.Parser.Parser
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.Indep.contract_indep_iff : ∀ {α : Type u_1} {M : Matroid α} {I J : Set α}, M.Indep I → ((M.contract I).Indep J ↔ Disjoint J I ∧ M.Indep (J ∪ I))
-- Mathlib.Data.List.Lex
List.instLinearOrder : {α : Type u} → [LinearOrder α] → LinearOrder (List α)
-- Mathlib.Computability.RE
Computable.computablePred : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop} [inst_1 : DecidablePred p],
  (Computable fun a => decide (p a)) → ComputablePred p
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.instAddCommGroup : {ι : Type u_1} →
  {I₀ : WithTop (BoxIntegral.Box ι)} →
    {M : Type u_4} → [inst : AddCommGroup M] → AddCommGroup (BoxIntegral.BoxAdditiveMap ι M I₀)
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_toUInt32 : ∀ (n : USize) (h : System.Platform.numBits = 32), n.toUInt32.toBitVec = BitVec.setWidth 32 (n.toBitVec32 h)
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.card_interedges_le_mul : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β),
  (Rel.interedges r s t).card ≤ s.card * t.card
-- Init.Data.Int.LemmasAux
Int.lt_toNat : ∀ {m : ℕ} {n : ℤ}, m < n.toNat ↔ ↑m < n
-- Mathlib.Algebra.Group.Prod
Prod.instIsAddTorsionFree : ∀ {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N] [IsAddTorsionFree M] [IsAddTorsionFree N],
  IsAddTorsionFree (M × N)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.lift_id : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x : N), (f.lift ⋯) x = x
-- Mathlib.Order.Minimal
OrderEmbedding.inter_preimage_setOfPred_minimal_eq_of_subset : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α ↪o β} {t : Set β},
  t ⊆ ⇑f '' s → (x ∈ s ∩ ⇑f ⁻¹' {y | Minimal (fun x => x ∈ t) y} ↔ Minimal (fun x => x ∈ s ∩ ⇑f ⁻¹' t) x)
-- Init.System.IOError
/-- A necessary resource is no longer available.

This corresponds to POSIX errors `ECONNRESET`, `EIDRM`, `ENETDOWN`, `ENETRESET`, `ENOLINK`, and
`EPIPE`.
 -/
IO.Error.resourceVanished : UInt32 → String → IO.Error
-- Std.Http.Data.Method
Std.Http.Method.bind.sizeOf_spec : sizeOf Std.Http.Method.bind = 1
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_zero : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv], CauSeq.Completion.ofRat 0 = 0
-- Mathlib.CategoryTheory.Comma.Basic
/-- `Comma.post` is a particular case of `Comma.map`, but with better definitional properties.  -/
CategoryTheory.Comma.postIso : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {C : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C] →
                (L : CategoryTheory.Functor A T) →
                  (R : CategoryTheory.Functor B T) →
                    (F : CategoryTheory.Functor T C) →
                      CategoryTheory.Comma.post L R F ≅
                        CategoryTheory.Comma.map (L.comp F).leftUnitor.hom (R.comp F).leftUnitor.inv
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.Tendsto.atTop_zsmul_neg_const : ∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [inst : AddCommGroup R] [inst_1 : LinearOrder R]
  [IsOrderedAddMonoid R] [Archimedean R] {f : α → ℤ},
  r < 0 → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x • r) l Filter.atBot
-- Mathlib.Algebra.Group.AddChar
/-- Composing an `AddChar` with an `AddMonoidHom` yields another `AddChar`.  -/
AddChar.compAddMonoidHom : {A : Type u_1} →
  {B : Type u_2} →
    {M : Type u_3} →
      [inst : AddMonoid A] → [inst_1 : AddMonoid B] → [inst_2 : Monoid M] → AddChar B M → (A →+ B) → AddChar A M
-- Mathlib.Control.Functor
Functor.Comp.functor_id_comp : ∀ {F : Type u_1 → Type u_2} [AF : Functor F] [LawfulFunctor F], Functor.Comp.functor = AF
-- Mathlib.Data.Finmap
Finmap.decidableEq : {α : Type u} → {β : α → Type v} → [DecidableEq α] → [(a : α) → DecidableEq (β a)] → DecidableEq (Finmap β)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso_inv_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  [inst_4 : CategoryTheory.Limits.HasKernels Cᵒᵖ] [inst_5 : CategoryTheory.Limits.HasCokernels Cᵒᵖ]
  (X : (CategoryTheory.ShortComplex C)ᵒᵖ),
  (CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso C).inv.app X = (Opposite.unop X).leftHomologyOpIso.hom
-- Mathlib.GroupTheory.NoncommCoprod
MulHom.comp_noncommCoprod : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Semigroup P] (f : M →ₙ* P)
  (g : N →ₙ* P) {Q : Type u_4} [inst_3 : Semigroup Q] (h : P →ₙ* Q) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)),
  h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯
-- Batteries.Data.List.Lemmas
List.foldlIdx_cons : ∀ {α : Type u_1} {x : α} {xs : List α} {α_1 : Sort u_2} {f : ℕ → α_1 → α → α_1} {i : α_1} {s : ℕ},
  List.foldlIdx f i (x :: xs) s = List.foldlIdx f (f s i x) xs (s + 1)
-- Mathlib.Algebra.Lie.Ideal
/-- The condition that the range of a morphism of Lie algebras is an ideal.  -/
LieHom.IsIdealMorphism : {R : Type u} →
  {L : Type v} →
    {L' : Type w₂} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieRing L'] → [inst_3 : LieAlgebra R L'] → [inst_4 : LieAlgebra R L] → (L →ₗ⁅R⁆ L') → Prop
-- Init.Data.Int.Order
Int.ofNat_zero_le : ∀ (n : ℕ), 0 ≤ ↑n
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
/-- The injective seminorm on `⨂[𝕜] i, Eᵢ`. Morally, it sends `x` in `⨂[𝕜] i, Eᵢ` to the
`sup` of the operator norms of the `PiTensorProduct.toDualContinuousMultilinearMap F x`, for all
normed vector spaces `F`. In fact, we only take in the same universe as `⨂[𝕜] i, Eᵢ`, and then
prove in `PiTensorProduct.norm_eval_le_injectiveSeminorm` that this gives the same result.
 -/
PiTensorProduct.injectiveSeminorm : {ι : Type u_2} →
  [Fintype ι] →
    {𝕜 : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        {E : ι → Type u_4} →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] → Seminorm 𝕜 (PiTensorProduct 𝕜 fun i => E i)
-- Lean.Linter.Init
/-- Insert a set into a `LinterSets` map.

`entry.1` is the name of the linter set,
`entry.2` contains the names of the set's linter options.
 -/
Lean.Linter.insertLinterSetEntry : Lean.Linter.LinterSets → Lean.Name → Lean.NameSet → Lean.Linter.LinterSets
-- Mathlib.Order.Interval.Multiset
Multiset.Icc.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α), Multiset.Icc a b = (Finset.Icc a b).val
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.num_neg : ∀ {a : ℚ}, a.num < 0 ↔ a < 0
-- Mathlib.Analysis.Normed.Group.Constructions
norm_toMul : ∀ {E : Type u_2} [inst : Norm E] (x : Additive E), ‖Additive.toMul x‖ = ‖x‖
-- Mathlib.Algebra.Group.Defs
neg_one_zsmul : ∀ {G : Type u_1} [inst : SubNegMonoid G] (x : G), -1 • x = -x
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.minimalCover_subset : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal}, Metric.minimalCover ε A ⊆ A
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.closure_singleton_le_iff_mem : ∀ {M : Type u_1} [inst : MulOneClass M] (m : M) (p : Submonoid M), Submonoid.closure {m} ≤ p ↔ m ∈ p
-- Mathlib.FieldTheory.Finite.GaloisField
instAlgebraZModGaloisField : (p : ℕ) → [inst : Fact (Nat.Prime p)] → (n : ℕ) → Algebra (ZMod p) (GaloisField p n)
-- Mathlib.Topology.Category.TopCat.Opens
TopCat.Hom.coe_frameHom_toFun : ∀ {X Y : TopCat} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑Y),
  ↑((TopCat.Hom.frameHom f) U) = ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' ↑U
-- Std.Data.DHashMap.Internal.AssocList.Iterator
Std.DHashMap.Internal.AssocList.instFiniteAssocListIteratorIdSigma : ∀ {α : Type u_1} {β : α → Type u_2}, Std.Iterators.Finite (Std.DHashMap.Internal.AssocList.AssocListIterator α β) Id
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_roc_eq_some_iff : ∀ {k m n : ℤ} {i : ℕ}, (m<...=n).toArray[i]? = some k ↔ i < (n - m).toNat ∧ m + 1 + ↑i = k