mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Data.Status
Std.Http.Status.processing.sizeOf_spec : sizeOf Std.Http.Status.processing = 1
-- Init.Data.SInt.Lemmas
Int32.ofInt_eq_ofIntLE_mod : ∀ {a b : ℤ} (ha₁ : Int32.minValue.toInt ≤ a) (ha₂ : a ≤ Int32.maxValue.toInt) (hb₁ : Int32.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int32.maxValue.toInt), Int32.ofInt (a.tmod b) = Int32.ofIntLE a ha₁ ha₂ % Int32.ofIntLE b hb₁ hb₂
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.dense : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : Fact (1 ≤ p)], p ≠ ⊤ → Dense ↑(MeasureTheory.Lp.simpleFunc E p μ)
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.coeff_zero_prod : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] (f : ι → Polynomial R),
  (∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.Context.mk.injEq : ∀ (elaborator : Lean.Name) (recover : Bool) (elaborator_1 : Lean.Name) (recover_1 : Bool),
  ({ elaborator := elaborator, recover := recover } = { elaborator := elaborator_1, recover := recover_1 }) =
    (elaborator = elaborator_1 ∧ recover = recover_1)
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.denoteN.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α),
  Lean.Grind.Linarith.Poly.denoteN ctx Lean.Grind.Linarith.Poly.nil = 0
-- Mathlib.Algebra.Lie.Prod
LieHom.ker_fst : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂],
  LieIdeal.toLieSubalgebra R (L₁ × L₂) (LieHom.fst R L₁ L₂).ker = (LieHom.inr R L₁ L₂).range
-- Init.Data.List.OfFn
List.ofFnM_pure_comp : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] {n : ℕ} {f : Fin n → α},
  List.ofFnM (pure ∘ f) = pure (List.ofFn f)
-- Lean.Declaration
Lean.RecursorVal.mk.sizeOf_spec : ∀ (toConstantVal : Lean.ConstantVal) (all : List Lean.Name) (numParams numIndices numMotives numMinors : ℕ)
  (rules : List Lean.RecursorRule) (k isUnsafe : Bool),
  sizeOf
      { toConstantVal := toConstantVal, all := all, numParams := numParams, numIndices := numIndices,
        numMotives := numMotives, numMinors := numMinors, rules := rules, k := k, isUnsafe := isUnsafe } =
    1 + sizeOf toConstantVal + sizeOf all + sizeOf numParams + sizeOf numIndices + sizeOf numMotives +
            sizeOf numMinors +
          sizeOf rules +
        sizeOf k +
      sizeOf isUnsafe
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app._auto_1),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app (Opposite.unop X)).op
      ((CategoryTheory.shiftFunctor C n).map
          ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app X).unop).op
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.submoduleMap_injective_of_injOn : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {p : Submodule R M} {f : M →ₛₗ[σ₁₂] M₂},
  Set.InjOn ⇑f ↑p → Function.Injective ⇑(f.submoduleMap p)
-- Mathlib.GroupTheory.Rank
AddGroup.rank_eq_zero : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : Subsingleton G], AddGroup.rank G = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
/-- The inclusion `(S.unionProd T).toSSet ⟶ X ⊗ Y` is isomorphic to the pushout-product
`S.ι □ T.ι`.  -/
SSet.Subcomplex.unionProd.ιIso : {X Y : SSet} →
  (S : X.Subcomplex) →
    (T : Y.Subcomplex) →
      CategoryTheory.Arrow.mk (S.unionProd T).ι ≅ CategoryTheory.Arrow.mk S.ι □ CategoryTheory.Arrow.mk T.ι
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.neg_eq_self : ∀ {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
  -p = p
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_nil : ∀ {α : Type u} {β : Type v} [inst : BEq α] {a : α} {fallback : β}, Std.Internal.List.getValueD a [] fallback = fallback
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- The type of morphisms in `SemimoduleCat R`.  -/
SemimoduleCat.Hom : {R : Type u} → [inst : Semiring R] → SemimoduleCat R → SemimoduleCat R → Type v
-- Mathlib.CategoryTheory.Action.Limits
/-- `F.mapAction : Action V G ⥤ Action W G` preserves limits of some size if
`V` has limits of that size and `F` preserves limits of that size.  -/
Action.Functor.preservesLimitsOfSize_of_preserves : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_2, u_3} W] (F : CategoryTheory.Functor V W) (G : Type u_4) [inst_2 : Monoid G]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{w₂, w₁, v_1, v_2, u_1, u_3} F]
  [CategoryTheory.Limits.HasLimitsOfSize.{w₂, w₁, v_1, u_1} V],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w₂, w₁, v_1, v_2, max (max u_1 u_4) v_1, max (max u_3 u_4) v_2}
    (F.mapAction G)
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instCofibrationInrOfIsStableUnderCobaseChangeCofibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [inst_2 : CategoryTheory.Limits.HasPushout f g]
  [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [hf : HomotopicalAlgebra.Cofibration f],
  HomotopicalAlgebra.Cofibration (CategoryTheory.Limits.pushout.inr f g)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSpanningSubgraph.mk : ∀ {α : Type u_1} {β : Type u_2} {H G : Graph α β}, H.IsSubgraph G → H.vertexSet = G.vertexSet → H ≤s G
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.mul_def : ∀ {D : Type u_1} {Q : Type u_2} [inst : Group D] [inst_1 : Group Q] (a b : D ≀ᵣ Q),
  a * b = { left := a.left * fun x => b.left (a.right⁻¹ * x), right := a.right * b.right }
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_add_zero_eventuallyLE : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : Filter α}
  {f g : α → M}, Filter.Tendsto f l Filter.atTop → 0 ≤ᶠ[l] g → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
-- Mathlib.Data.List.Lex
_private.Mathlib.Data.List.Lex.0.List.Lex.asymm.aux : ∀ {α : Type u} (r : α → α → Prop) [Std.Asymm r] (x x_1 : List α), List.Lex r x x_1 → List.Lex r x_1 x → False
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.beth_one : Cardinal.beth 1 = Cardinal.continuum
-- Mathlib.Analysis.Complex.Arg
Complex.norm_sub_eq_iff : ∀ {x y : ℂ}, ‖x - y‖ = |‖x‖ - ‖y‖| ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
-- Mathlib.RingTheory.FiniteLength
instIsArtinianOfIsSemisimpleModuleOfFinite : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  [Module.Finite R M], IsArtinian R M
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.coe_divLeft : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] (a : G),
  ⇑(Homeomorph.divLeft a) = fun x => a / x
-- Mathlib.NumberTheory.SmoothNumbers
/-- `m` is `n`-smooth if and only if all prime divisors of `m` are less than `n`.  -/
Nat.mem_smoothNumbers' : ∀ {n m : ℕ}, m ∈ n.smoothNumbers ↔ ∀ (p : ℕ), Nat.Prime p → p ∣ m → p < n
-- Mathlib.Topology.Algebra.Module.PerfectPairing
LinearMap.IsContPerfPair.bijective_left : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {inst : CommRing R} {inst_1 : TopologicalSpace R}
  {inst_2 : AddCommGroup M} {inst_3 : Module R M} {inst_4 : TopologicalSpace M} {inst_5 : AddCommGroup N}
  {inst_6 : Module R N} {inst_7 : TopologicalSpace N} (p : M →ₗ[R] N →ₗ[R] R) [self : p.IsContPerfPair],
  Function.Bijective fun x => { toLinearMap := p x, cont := ⋯ }
-- Mathlib.CategoryTheory.Yoneda
/-- The representing object for the representable functor `F`.  -/
CategoryTheory.Functor.reprX : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (F : CategoryTheory.Functor Cᵒᵖ (Type v)) → [hF : F.IsRepresentable] → C
-- Mathlib.RingTheory.Multiplicity
emultiplicity_add_of_gt : ∀ {α : Type u_1} [inst : Ring α] {p a b : α},
  emultiplicity p b < emultiplicity p a → emultiplicity p (a + b) = emultiplicity p b
-- Mathlib.Data.Num.Basic
/-- Auxiliary definition for `Num.gcd`.  -/
Num.gcdAux : ℕ → Num → Num → Num
-- Mathlib.Topology.Sheaves.Stalks
/-- The germ of a global section of a presheaf at a point.  -/
TopCat.Presheaf.Γgerm : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X : TopCat} → (F : TopCat.Presheaf C X) → (x : ↑X) → F.obj (Opposite.op ⊤) ⟶ F.stalk x
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.kerGen.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) (i : σ),
  Algebra.Generators.PresentationOfFreeCotangent.Aux.kerGen✝ D i =
    ⟨↑(Algebra.Generators.PresentationOfFreeCotangent.Aux.f✝ D (b i)), ⋯⟩
-- Mathlib.Data.Seq.Computation
/-- left map of `⊕`  -/
Computation.lmap : {α : Type u} → {β : Type v} → {γ : Type w} → (α → β) → α ⊕ γ → β ⊕ γ
-- Mathlib.Topology.MetricSpace.Isometry
/-- The (bundled) homeomorphism associated to an isometric isomorphism.  -/
IsometryEquiv.toHomeomorph : {α : Type u} → {β : Type v} → [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → α ≃ᵢ β → α ≃ₜ β
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.associator_hom_apply_2_1 : ∀ {X Y Z : Type u}
  {x :
    (fun X => X)
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)},
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) x).2.1 = x.1.2
-- Aesop.Frontend.Extension
Aesop.Frontend.isRuleSetDeclared : Aesop.RuleSetName → IO Bool
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedFunctionTheorem : Inhabited Mathlib.Meta.FunProp.FunctionTheorem
-- Init.Data.Slice.Array.Basic
instSliceableSubarrayNat_5 : {α : Type u} → Std.Roi.Sliceable (Subarray α) ℕ (Subarray α)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instMonoidWithZero : (R : Type u_1) → (X : Type u_2) → [inst : CommSemiring R] → MonoidWithZero (FreeAlgebra R X)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Icc_castAdd : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n),
  ∏ i ∈ Finset.Icc (Fin.castAdd m a) (Fin.castAdd m b), f i = ∏ i ∈ Finset.Icc a b, f (Fin.castAdd m i)
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- If `f` has derivative `f'` within `s` at `x`, then for any `r > ‖f'‖` the ratio
`(‖f z‖ - ‖f x‖) / ‖z - x‖` is less than `r` in some neighborhood of `x` within `s`.
In other words, the limit superior of this ratio as `z` tends to `x` along `s`
is less than or equal to `‖f'‖`.

This lemma is a weaker version of `HasDerivWithinAt.limsup_norm_slope_le`
where `‖f z‖ - ‖f x‖` is replaced by `‖f z - f x‖`.  -/
HasDerivWithinAt.limsup_slope_norm_le : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {f' : E} {s : Set ℝ} {x r : ℝ},
  HasDerivWithinAt f f' s x → ‖f'‖ < r → ∀ᶠ (z : ℝ) in nhdsWithin x s, ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
-- Init.Notation
/-- Subtraction of priorities. This is normally used only for offsetting, e.g. `default - 1`.  -/
Lean.Parser.Syntax.subPrio : Lean.TrailingParserDescr
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.coe_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β],
  ⇑⊥ = ⊥
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instLocallyOfFiniteType : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsFinite f], AlgebraicGeometry.LocallyOfFiniteType f
-- Lean.Parser.Extension
Lean.Parser.commandParser : optParam ℕ 0 → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLE_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} {X Y : CategoryTheory.Subobject B} (h : X ≤ Y),
  CategoryTheory.CategoryStruct.comp (X.ofLE Y h) Y.arrow = X.arrow
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.State.ngen : Lean.MetavarContext.MkBinding.State → Lean.NameGenerator
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.IsAffineOpen.isCompact_pullback_inf : ∀ {X Y Z : AlgebraicGeometry.Scheme} {f : X ⟶ Z} {g : Y ⟶ Z} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : Y.Opens},
      IsCompact ↑V →
        ∀ {W : Z.Opens},
          AlgebraicGeometry.IsAffineOpen W →
            U ≤ (TopologicalSpace.Opens.map f.base).obj W →
              V ≤ (TopologicalSpace.Opens.map g.base).obj W →
                IsCompact
                  (↑((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.fst f g).base).obj U) ⊓
                    ↑((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.snd f g).base).obj V))
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_of_linearEquiv : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module S P] {σ : R →+* S}
  {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ] (f : M ≃ₛₗ[σ] P) [IsNoetherian R M],
  IsNoetherian S P
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- **Alias** of `ChartedSpace.sumOfNonempty`.

---

The disjoint union of two charted spaces modelled on a non-empty space `H`
is a charted space over `H`.  -/
ChartedSpace.sum_of_nonempty : {H : Type u} →
  {M : Type u_2} →
    {M' : Type u_3} →
      [inst : TopologicalSpace H] →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : TopologicalSpace M'] →
            [cm : ChartedSpace H M] → [cm' : ChartedSpace H M'] → [Nonempty H] → ChartedSpace H (M ⊕ M')
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
IsInertiaField.ringEquiv.eq_1 : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (E : Type u_6) [inst_4 : Field E] [inst_5 : Algebra E L]
  [inst_6 : MulSemiringAction Gal(L/K) B] (E' : Type u_9) [inst_7 : Field E'] [inst_8 : Algebra E' L]
  [inst_9 : IsInertiaField K L P E] [inst_10 : IsInertiaField K L P E'],
  IsInertiaField.ringEquiv K L P E E' = IsGaloisGroup.ringEquiv (↥(Ideal.inertia Gal(L/K) P)) E E' L
-- Mathlib.Analysis.Fourier.Convolution
SchwartzMap.fourier_convolution_apply : ∀ {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst : NormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E]
  [inst_5 : NormedAddCommGroup F₁] [inst_6 : NormedSpace ℂ F₁] [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace ℂ F₂] [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace ℂ F₃] [CompleteSpace F₃]
  [CompleteSpace F₁] [CompleteSpace F₂] (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) (f : SchwartzMap E F₁) (g : SchwartzMap E F₂)
  (x : E),
  (FourierTransform.fourier (((SchwartzMap.convolution B) f) g)) x =
    FourierTransform.fourier (MeasureTheory.convolution (⇑f) (⇑g) B MeasureTheory.volume) x
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_erase : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, (m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)
-- Std.Sat.CNF.Basic
Std.Sat.CNF.eval.eq_1 : ∀ {α : Type u_1} (a : α → Bool) (f : Std.Sat.CNF α),
  Std.Sat.CNF.eval a f = f.clauses.all fun c => Std.Sat.CNF.Clause.eval a c
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInfEntourage_univ : ∀ {X : Type u_1} {F : Set X} (T : X → X), F.Nonempty → Dynamics.coverEntropyInfEntourage T F Set.univ = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mem_map_equiv : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] {f : M ≃+ N} {K : AddSubmonoid M}
  {x : N}, x ∈ AddSubmonoid.map f.toAddMonoidHom K ↔ f.symm x ∈ K
-- Std.Time.Time.Unit.Minute
/-- Creates an `Offset` from an integer.
 -/
Std.Time.Minute.Offset.ofInt : ℤ → Std.Time.Minute.Offset
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_C_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (N n : ℕ) {c : R},
  Polynomial.reflect N (Polynomial.C c * Polynomial.X ^ n) = Polynomial.C c * Polynomial.X ^ (Polynomial.revAt N) n
-- Init.Grind.Ring.Basic
/-- Exponentiation by a natural number.  -/
Lean.Grind.Semiring.npow : {α : Type u} → [self : Lean.Grind.Semiring α] → HPow α ℕ α
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_iff_measurable : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} [μ.IsComplete], AEMeasurable f μ ↔ Measurable f
-- Lean.DocString.Types
Lean.Doc.Inline.other.inj : ∀ {i : Type u} {container : i} {content : Array (Lean.Doc.Inline i)} {container_1 : i}
  {content_1 : Array (Lean.Doc.Inline i)},
  Lean.Doc.Inline.other container content = Lean.Doc.Inline.other container_1 content_1 →
    container = container_1 ∧ content = content_1
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.toAddEquiv_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β],
  Function.Injective OrderAddMonoidIso.toAddEquiv
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairOfIsCosplitPairOfReflectsLimitOfIsCosplitPair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g]
  [CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair F],
  CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.parallelPair f g) F
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.minKey he ∈ t
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableOn_finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ},
  DifferentiableOn 𝕜 (fun x => Fin.cons (φ x) (φs x)) s ↔ DifferentiableOn 𝕜 φ s ∧ DifferentiableOn 𝕜 φs s
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Scheme.Hom.cover_f : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (hf : P f)
  [inst : AlgebraicGeometry.Surjective f] (x : PUnit.{v + 1}), (AlgebraicGeometry.Scheme.Hom.cover f hf).f x = f
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofHom_id : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {Y : Type w} [inst_2 : AddCommGroup Y]
  [inst_3 : Module k Y] {σ : Representation k G Y},
  Rep.ofHom (Representation.IntertwiningMap.id σ) = CategoryTheory.CategoryStruct.id (Rep.of σ)
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.instMembershipSet.eq_1 : ∀ {G : Type u} [inst : AddGroup G], AddGroupFilterBasis.instMembershipSet = { mem := fun f s => s ∈ f.sets }
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMapZero.mul_nonUnitalStarAlgHom_apply_eq_zero : ∀ {𝕜 : Type u_2} {A : Type u_3} [inst : RCLike 𝕜] [inst_1 : NonUnitalSemiring A] [inst_2 : Star A]
  [inst_3 : TopologicalSpace A] [SeparatelyContinuousMul A] [T2Space A] [inst_6 : DistribMulAction 𝕜 A]
  [SMulCommClass 𝕜 A A] {s : Set 𝕜} [inst_8 : Fact (0 ∈ s)] [CompactSpace ↑s] (φ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A)
  (a : A),
  a * φ (ContinuousMapZero.id s) = 0 →
    a * φ (star (ContinuousMapZero.id s)) = 0 → Continuous ⇑φ → ∀ (f : ContinuousMapZero (↑s) 𝕜), a * φ f = 0
-- Mathlib.Order.RelIso.Basic
RelIso.symm_trans_self : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s), e.symm.trans e = RelIso.refl s
-- Mathlib.Topology.Germ
/-- The map `Germ (𝓝 x) E → E` as a ring homomorphism  -/
Filter.Germ.valueRingHom : {X : Type u_4} → {E : Type u_5} → [inst : Semiring E] → [inst_1 : TopologicalSpace X] → {x : X} → (nhds x).Germ E →+* E
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Theory.realize_sentence_of_mem : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (T : L.Theory) [M ⊨ T] {φ : L.Sentence}, φ ∈ T → M ⊨ φ
-- Lean.Parser.Command
Lean.Parser.Command.unlock_limits.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Module.Submodule.Range
/-- The range of a linear map is finite if the domain is finite.
Note: this instance can form a diamond with `Subtype.fintype` in the
  presence of `Fintype M₂`.  -/
LinearMap.fintypeRange : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_5} →
      {M₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {τ₁₂ : R →+* R₂} →
                      [Fintype M] →
                        [DecidableEq M₂] → [inst_8 : RingHomSurjective τ₁₂] → (f : M →ₛₗ[τ₁₂] M₂) → Fintype ↥f.range
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The binary cofan constructed from the coprojection maps is a colimit.  -/
CategoryTheory.Limits.coprodIsCoprod : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X Y : C) →
      [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] →
        CategoryTheory.Limits.IsColimit
          (CategoryTheory.Limits.BinaryCofan.mk CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The right unitor as a term of `normalExpr`.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.rightUnitorM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] →
        Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.NormalExpr
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.le_max_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} (hc : k ∈ t),
  (cmp k (t.max ⋯)).isLE = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp] {k : α}, k ∉ t₁ → (t₁ \ t₂).getKey! k = default
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The kernel of the morphism `X ⟶ image f` is just the kernel of `f`.  -/
CategoryTheory.Limits.kernelFactorThruImage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            [inst_3 : CategoryTheory.Limits.HasImage f] →
              [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.factorThruImage f)] →
                CategoryTheory.Limits.kernel (CategoryTheory.Limits.factorThruImage f) ≅ CategoryTheory.Limits.kernel f