mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
/-- **Alias** of `SSet.Homotopy.congr_homologyMap`.

---

Homotopic maps of simplicial sets induce the same map on homology of the singular
chain complex (with coefficients in `R`).
 -/
SSet.Homotopy.congr_homologyMap_singularChainComplexFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasCoproducts C] {X Y : SSet} {f g : X ⟶ Y}
  [inst_3 : CategoryTheory.CategoryWithHomology C] (H : SSet.Homotopy f g) (R : C) (n : ℕ),
  SSet.homologyMap f R n = SSet.homologyMap g R n
-- Mathlib.RingTheory.Valuation.Integers
Valuation.leIdeal_map_algebraMap_eq_leSubmodule_min : ∀ {Γ₀ : Type v} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_1} [inst_1 : Field K] (v : Valuation K Γ₀)
  (γ : Γ₀), Submodule.map (Algebra.linearMap (↥v.integer) K) (v.leIdeal γ) = v.leSubmodule (min 1 γ)
-- Mathlib.Topology.Order.ExtrClosure
IsLocalMaxOn.closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Preorder Y]
  [OrderClosedTopology Y] {f : X → Y} {s : Set X} {a : X},
  IsLocalMaxOn f s a → ContinuousOn f (closure s) → IsLocalMaxOn f (closure s) a
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.toSubgroup_le : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {U V : OpenSubgroup G}, ↑U ≤ ↑V ↔ U ≤ V
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.toPrenex.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (t₁ t₂ : L.Term (α ⊕ Fin x)),
  (FirstOrder.Language.BoundedFormula.equal t₁ t₂).toPrenex = t₁.bdEqual t₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.sinh_pos_iff : ∀ {x : ℝ}, 0 < Real.sinh x ↔ 0 < x
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.dvdNotUnit_setGcd_insert : ∀ {s : Set ℕ} {n : ℕ}, ¬Nat.setGcd s ∣ n → DvdNotUnit (Nat.setGcd (insert n s)) (Nat.setGcd s)
-- Init.Data.SInt.Lemmas
Int32.ofInt_toInt : ∀ (x : Int32), Int32.ofInt x.toInt = x
-- Lean.Compiler.ExternAttr
Lean.getExternAttrData? : Lean.Environment → Lean.Name → Option Lean.ExternAttrData
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- The projections from the weighted limit.  -/
CategoryTheory.Functor.weightedLimObjObjπ : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        (W : CategoryTheory.Functor J (Type w)) →
          (F : CategoryTheory.Functor J C) →
            [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] →
              ⦃j : J⦄ → W.obj j → (W.weightedLimObjObj F ⟶ F.obj j)
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_idem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C},
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty AlgebraicTopology.DoldKan.PInfty =
    AlgebraicTopology.DoldKan.PInfty
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.hausdorffEDist_prod_le : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {s₁ t₁ : Set α}
  {s₂ t₂ : Set β},
  Metric.hausdorffEDist (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) ≤ max (Metric.hausdorffEDist s₁ t₁) (Metric.hausdorffEDist s₂ t₂)
-- Std.Data.ExtDTreeMap.Basic
/-- Removes all mappings of the map for which the given function returns `false`.  -/
Std.ExtDTreeMap.filter : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → ((a : α) → β a → Bool) → Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α β cmp
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
multiplication on `𝕜`, then it acts distributively on `WeakDual 𝕜 E`.  -/
WeakDual.instDistribMulAction : {𝕜 : Type u_2} →
  {E : Type u_4} →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] →
                [inst_6 : TopologicalSpace E] →
                  (M : Type u_6) →
                    [inst_7 : Monoid M] →
                      [inst_8 : DistribMulAction M 𝕜] →
                        [SMulCommClass 𝕜 M 𝕜] → [ContinuousConstSMul M 𝕜] → DistribMulAction M (WeakDual 𝕜 E)
-- Init.Data.UInt.Bitwise
UInt64.not_or_self : ∀ {a : UInt64}, ~~~a ||| a = -1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.keys_filter_key : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {f : α → Bool},
  (↑(Std.DHashMap.Internal.Raw₀.filter (fun k x => f k) m)).keys.Perm (List.filter f (↑m).keys)
-- Lean.DocString.Parser
Lean.Doc.Parser.InlineCtxt.mk : Bool → ℕ → Option ℕ → Option ℕ → Bool → Lean.Doc.Parser.InlineCtxt
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toAlgEquiv_ofAlgEquiv : ∀ {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Star A] [inst_6 : Star B] (f : A ≃ₐ[R] B)
  (map_star : ∀ (x : A), f (star x) = star (f x)), (StarAlgEquiv.ofAlgEquiv f map_star).toAlgEquiv = f
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {a : α}, Std.Internal.List.getEntry? a [] = none
-- Mathlib.Analysis.Matrix.PosDef
/-- The eigenvalues of a positive semi-definite matrix are non-negative  -/
Matrix.PosSemidef.eigenvalues_nonneg : ∀ {n : Type u_2} {𝕜 : Type u_3} [inst : Fintype n] [inst_1 : RCLike 𝕜] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.PosSemidef) (i : n), 0 ≤ ⋯.eigenvalues i
-- Mathlib.Computability.RegularExpressions
RegularExpression.instPowNat : {α : Type u_1} → Pow (RegularExpression α) ℕ
-- Mathlib.CategoryTheory.Subobject.Basic
/-- The category of subobjects is equivalent to the `MonoOver` category. It is more convenient to
use the former due to the partial order instance, but oftentimes it is easier to define structures
on the latter.  -/
CategoryTheory.Subobject.equivMonoOver : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (X : C) → CategoryTheory.Subobject X ≌ CategoryTheory.MonoOver X
-- Init.Data.Array.Lemmas
Array.forall_mem_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {P : β → Prop},
  (∀ i ∈ Array.filterMap f xs, P i) ↔ ∀ j ∈ xs, ∀ (b : β), f j = some b → P b
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.keyAtIdxD : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → ℕ → α → α
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiff_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  ContDiff 𝕜 0 f ↔ Continuous f
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.smul_mem_iff : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : GroupWithZero S] [inst_1 : Monoid R] [inst_2 : MulAction R M]
  [inst_3 : SMul S R] [inst_4 : MulAction S M] [IsScalarTower S R M] (p : SubMulAction R M) {s : S} {x : M},
  s ≠ 0 → (s • x ∈ p ↔ x ∈ p)
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.mul_right : ∀ {D : Type u_1} {Q : Type u_2} [inst : Group D] [inst_1 : Group Q] (a b : D ≀ᵣ Q), (a * b).right = a.right * b.right
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates colimits and `F ≅ G`, then `G` creates colimits.  -/
CategoryTheory.createsColimitsOfNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} →
          (F ≅ G) →
            [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
              CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G
-- Lean.Elab.AutoBound
Lean.Elab.instEmptyCollectionAutoBoundImplicitContext : EmptyCollection Lean.Elab.AutoBoundImplicitContext
-- Mathlib.Algebra.Order.Module.Defs
Pi.instSMulPosReflectLE : ∀ {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [inst : Preorder α] [inst_1 : (i : ι) → Preorder (β i)]
  [inst_2 : (i : ι) → SMul α (β i)] [inst_3 : (i : ι) → Zero (β i)] [∀ (i : ι), SMulPosReflectLE α (β i)],
  SMulPosReflectLE α ((i : ι) → β i)
-- Init.Data.Vector.Lex
Vector.instLawfulOrderLTOfAsymmLt : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2], Std.LawfulOrderLT (Vector α n)
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_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.Opposite.OpOpCommShift.iso_hom_app._auto_1),
  (CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso C n).hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).hom.app (Opposite.op X)).op
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app (Opposite.op (Opposite.op X)))
-- Init.Data.Order.PackageFactories
/-- If `LT` can be characterized in terms of a decidable `LE`, then `LT` is decidable either.  -/
Std.FactoryInstances.decidableLTOfLE : {α : Type u} → [inst : LE α] → {x : LT α} → [DecidableLE α] → [Std.LawfulOrderLT α] → DecidableLT α
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  {X Y : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C} (f : X ⟶ Y) (X_1 : SimplexCategoryᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.functor.map f).left.app X_1 =
    f.app
      (match CategoryTheory.WithTerminal.incl.obj X_1 with
      | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
      | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star)
-- Init.Data.UInt.Lemmas
UInt32.div_self : ∀ {a : UInt32}, a / a = if a = 0 then 0 else 1
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.isUniformInducing_coe : ∀ (α : Type u_1) [inst : UniformSpace α], IsUniformInducing UniformSpace.Completion.coe'
-- Std.Time.Date.Unit.Month
Std.Time.Month.instTransOrdQuarter : Std.TransOrd Std.Time.Month.Quarter
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, returning `none` if no such key exists.
 -/
Std.TreeMap.getKeyGE? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → Option α
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkAllIndStx : Lean.Meta.Try.Info → Lean.TSyntax `tactic → Lean.MetaM (Lean.TSyntax `tactic)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz
/-- `zarankiewicz m n s t` is at most `x` if and only if every
`completeBipartiteGraph α β`-free bipartite graph `G` has at most `x` edges.  -/
SimpleGraph.zarankiewicz_le_iff : ∀ {m n s t : ℕ} {V : Type u_1} {W : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : Fintype α] [inst_3 : Fintype β],
  Fintype.card V = m →
    Fintype.card W = n →
      Fintype.card α = s →
        Fintype.card β = t →
          ∀ (x : ℕ),
            SimpleGraph.zarankiewicz m n s t ≤ x ↔
              ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst_4 : DecidableRel G.Adj],
                G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → G.edgeFinset.card ≤ x
-- Init.MetaTypes
/-- When `true` (default: `true`), the bitvector simprocs use `BitVec.ofNat` for representing
bitvector literals.
 -/
Lean.Meta.Simp.Config.bitVecOfNat : Lean.Meta.Simp.Config → Bool
-- Mathlib.Data.List.Sort
_private.Mathlib.Data.List.Sort.0.List.«term_≼__1» : Lean.TrailingParserDescr
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.of_terminates_iff_of_rat_terminates : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] [IsStrictOrderedRing K] {v : K}
  {q : ℚ}, v = ↑q → ((GenContFract.of v).Terminates ↔ (GenContFract.of q).Terminates)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.semilatticeSup : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : SemilatticeSup β] →
        [inst_2 : Zero β] →
          [inst_3 : TopologicalSpace β] → [ContinuousSup β] → SemilatticeSup (CompactlySupportedContinuousMap α β)
-- Mathlib.Order.Category.PartOrd
PartOrd.ofHom_id : ∀ {X : Type u} [inst : PartialOrder X],
  PartOrd.ofHom OrderHom.id = CategoryTheory.CategoryStruct.id { carrier := X, str := inst }
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.symm_toEquiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n),
  h.symm.toEquiv = h.symm
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ x * y` is quasi-measure-preserving.  -/
MeasureTheory.quasiMeasurePreserving_mul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [ν.IsMulLeftInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.1 * p.2) (μ.prod ν) ν
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductLimitCone.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)),
  CategoryTheory.FunctorToTypes.binaryProductLimitCone F G =
    { cone := CategoryTheory.FunctorToTypes.binaryProductCone F G,
      isLimit := CategoryTheory.FunctorToTypes.binaryProductLimit F G }
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- A function is `m`-`AEStronglyMeasurable` with respect to a measure `μ` if it is almost
everywhere equal to the limit of a sequence of `m`-simple functions.  -/
MeasureTheory.«termAEStronglyMeasurable[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.hasLimits : CategoryTheory.Limits.HasLimits CommMonCat
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.restrictFreeVar.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (x : ℕ) (t₁ t₂ : L.Term (α ⊕ Fin x))
  (f : ↥(FirstOrder.Language.BoundedFormula.equal t₁ t₂).freeVarFinset → β),
  (FirstOrder.Language.BoundedFormula.equal t₁ t₂).restrictFreeVar f =
    FirstOrder.Language.BoundedFormula.equal (t₁.restrictVarLeft (f ∘ Set.inclusion ⋯))
      (t₂.restrictVarLeft (f ∘ Set.inclusion ⋯))
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- **Alias** of `SimpleGraph.IsBridge.anti`. -/
SimpleGraph.IsBridge.anti_of_mem_edgeSet : ∀ {V : Type u} {G G' : SimpleGraph V} {e : Sym2 V}, G ≤ G' → G'.IsBridge e → G.IsBridge e
-- Init.Data.List.Attach
List.attach_append : ∀ {α : Type u_1} {xs ys : List α},
  (xs ++ ys).attach =
    List.map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        xs.attach ++
      List.map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        ys.attach
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instAddGroup : {k : Type u_1} → {G : Type u_2} → [inst : AddGroup k] → AddGroup (SkewMonoidAlgebra k G)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.instInhabitedHomOfHom : {B : Type u} → [inst : Quiver B] → (a b : B) → [Inhabited (a ⟶ b)] → Inhabited (CategoryTheory.FreeBicategory.Hom a b)
-- Mathlib.CategoryTheory.Sites.Descent.IsStack
/-- Version of `isStackFor` for a sieve instead of a presieve.  -/
CategoryTheory.Pseudofunctor.isStackFor' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat)
  {J : CategoryTheory.GrothendieckTopology C} [F.IsStack J] {S : C}, ∀ R ∈ J S, F.IsStackFor R.arrows
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- If `G` preserves the kernel of `f`, then the kernel comparison map for `G` at `f` is
an isomorphism.
 -/
CategoryTheory.Limits.PreservesKernel.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (G : CategoryTheory.Functor C D) →
              [G.PreservesZeroMorphisms] →
                {X Y : C} →
                  (f : X ⟶ Y) →
                    [inst_5 : CategoryTheory.Limits.HasKernel f] →
                      [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)] →
                        [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G] →
                          G.obj (CategoryTheory.Limits.kernel f) ≅ CategoryTheory.Limits.kernel (G.map f)
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- Given `(k, a) : Unitization 𝕜 A`, the second coordinate of `Unitization.splitMul (k, a)` is
the natural representation of `Unitization 𝕜 A` on `A` given by multiplication on the left in
`A →L[𝕜] A`; note that this is not just `NonUnitalAlgHom.Lmul` for a few reasons: (a) that would
either be `A` acting on `A`, or (b) `Unitization 𝕜 A` acting on `Unitization 𝕜 A`, and (c) that's a
`NonUnitalAlgHom` but here we need an `AlgHom`. In addition, the first coordinate of
`Unitization.splitMul (k, a)` should just be `k`. See `Unitization.splitMul_apply` also.  -/
Unitization.splitMul : (𝕜 : Type u_1) →
  (A : Type u_2) →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : IsScalarTower 𝕜 A A] → [inst_4 : SMulCommClass 𝕜 A A] → Unitization 𝕜 A →ₐ[𝕜] 𝕜 × (A →L[𝕜] A)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
MulActionHom.oneEmbeddingMap.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {one : Type u_5} [inst_2 : Unique one],
  MulActionHom.oneEmbeddingMap = { toFun := Function.Embedding.oneEmbeddingEquiv.toFun, map_smul' := ⋯ }
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.integrable_toReal_rnDeriv_mul_iff : ∀ {α : Type u_3} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν]
  [MeasureTheory.SigmaFinite μ],
  μ.AbsolutelyContinuous ν →
    ∀ {f : α → ℝ}, MeasureTheory.Integrable (fun x => (μ.rnDeriv ν x).toReal * f x) ν ↔ MeasureTheory.Integrable f μ
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.LocallyQuasiFinite.comp_iff : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.LocallyQuasiFinite g],
  AlgebraicGeometry.LocallyQuasiFinite (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.LocallyQuasiFinite f
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.monoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst_1 : One M₂] [inst_2 : Pow M₂ ℕ] [inst_3 : Monoid M₁]
  (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n),
  Function.Surjective.monoid f hf one mul npow =
    { toSemigroup := Function.Surjective.semigroup f hf mul,
      toOne := (Function.Surjective.mulOneClass f hf one mul).toOne, one_mul := ⋯, mul_one := ⋯,
      npow := fun n x => x ^ n, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_star : ∀ (x : GaussianInt), GaussianInt.toComplex (star x) = (starRingEnd ℂ) (GaussianInt.toComplex x)
-- Mathlib.Order.Interval.Set.Nat
Set.ncard_Ioc_nat : ∀ (a b : ℕ), (Set.Ioc a b).ncard = b - a
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.piAdditive_apply : ∀ {ι : Type u_1} (K : ι → Type u_4) [inst : (i : ι) → Mul (K i)] (x : Additive ((i : ι) → K i)) (i : ι),
  (AddEquiv.piAdditive K) x i = Additive.ofMul (Additive.toMul x i)
-- Std.Http.Data.Headers.Value
Std.Http.Header.instHashableValue : Hashable Std.Http.Header.Value
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.binop.sizeOf_spec : ∀ (ref : Lean.Syntax) (f : Lean.Expr) (lhs rhs : FBinopElab.Tree✝),
  sizeOf (FBinopElab.Tree.binop✝ ref f lhs rhs) = 1 + sizeOf ref + sizeOf f + sizeOf lhs + sizeOf rhs
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- If `it` is an iterator, then `it.mapM f` is another iterator that applies a monadic
function `f` to all values emitted by `it` and emits the result.

The base iterator `it` being monadic in `m`, `f` can return values in any monad `n` for which a
`MonadLiftT m n` instance is available.

If `f` is pure, then the simpler variant `it.map` can be used instead.

**Marble diagram (without monadic effects):**

```text
it          ---a --b --c --d -e ----⊥
it.mapM     ---a'--b'--c'--d'-e'----⊥
```

(given that `f a = pure a'`, `f b = pure b'` etc.)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is productive

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and
will always fail, then `it.mapM` will be finite even if `it` isn't. In such cases, the termination
proof needs to be done manually.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
Std.IterM.mapM : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      [Std.Iterator α m β] →
        [inst : Monad n] →
          [inst_1 : MonadAttach n] → [inst_2 : MonadLiftT m n] → (f : β → n γ) → Std.IterM m β → Std.IterM n γ
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsIsoOfEquiv_hom_apply : ∀ {R S : Type v} [inst : Ring R] [inst_1 : Ring S] (e : R ≃+* S) (x : S),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.restrictScalarsIsoOfEquiv e).hom) x = e.symm x
-- Aesop.Rule.Name
Aesop.instInhabitedScopeName.default : Aesop.ScopeName
-- Mathlib.Geometry.Convex.Cone.DualFinite
/-- The dual of a finite set is dually finitely generated.  -/
PointedCone.DualFG.dual_of_finset : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  (p : M →ₗ[R] N →ₗ[R] R) (s : Finset M), PointedCone.DualFG p (PointedCone.dual p ↑s)