mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.associatorNatIsoLeftCat_hom_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a : B) {b c d : B} (g : b ⟶ c) (h : c ⟶ d)
  (X : ↑(CategoryTheory.Cat.of (a ⟶ b))),
  (CategoryTheory.Bicategory.associatorNatIsoLeftCat a g h).hom.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator X g h).hom
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The restriction of scalars by a ring morphism that is the identity identifies to the
identity functor.  -/
ModuleCat.restrictScalarsId' : {R : Type u₁} →
  [inst : Ring R] →
    (f : R →+* R) → f = RingHom.id R → (ModuleCat.restrictScalars f ≅ CategoryTheory.Functor.id (ModuleCat R))
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.resolutionMap_zero : ∀ {k : Type u} {G H : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y),
  ContinuousCohomology.resolutionMap φ f 0 = f
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- A variant of `CategoryTheory.Limits.Cone.ext` specialized to produce
isomorphisms of wedges.  -/
CategoryTheory.Limits.Wedge.ext : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          {W₁ W₂ : CategoryTheory.Limits.Wedge F} →
            (e : W₁.pt ≅ W₂.pt) →
              autoParam
                  (∀ (j : J),
                    CategoryTheory.Limits.Multifork.ι W₁ j =
                      CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.Limits.Multifork.ι W₂ j))
                  CategoryTheory.Limits.Wedge.ext._auto_1 →
                (W₁ ≅ W₂)
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.zeroHom_apply : ∀ (X Y : AddMonCat) (x : ↑X), (AddMonCat.Hom.hom 0) x = 0
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- Let `R` be a semiring, let `A` be an `AddZeroClass`, let `B` be an `OrderBot`,
and let `D : A → B` be a "degree" function.
For an element `f : R[A]`, the element `supDegree f : B` is the supremum of all the elements in the
support of `f`, or `⊥` if `f` is zero.
Often, the Type `B` is `WithBot A`,
If, further, `A` has a linear order, then this notion coincides with the usual one,
using the maximum of the exponents.

If `A := σ →₀ ℕ` then `R[A] = MvPolynomial σ R`, and if we equip `σ` with a linear order then
the induced linear order on `Lex A` equips `MvPolynomial` ring with a
[monomial order](https://en.wikipedia.org/wiki/Monomial_order) (i.e. a linear order on `A`, the
type of (monic) monomials in `R[A]`, that respects addition). We make use of this monomial order
by taking `D := toLex`, and different monomial orders could be accessed via different type
synonyms once they are added.  -/
AddMonoidAlgebra.supDegree : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_5} →
      [inst : Semiring R] → [inst_1 : SemilatticeSup B] → [OrderBot B] → (A → B) → AddMonoidAlgebra R A → B
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is differentiable at every `x` in `(a, b)` and
its derivative is integrable on `[a, b]`, then `∫ y in a..b, deriv f y` equals `f b - f a`.  -/
intervalIntegral.integral_deriv_eq_sub_uIoo : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f : ℝ → E},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.uIoo a b, DifferentiableAt ℝ f x) →
      IntervalIntegrable (deriv f) MeasureTheory.volume a b → ∫ (y : ℝ) in a..b, deriv f y = f b - f a
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.edist_def : ∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [inst : Encodable ι]
  [inst_1 : (i : ι) → PseudoEMetricSpace (Y i)] (x y : Metric.PiNatEmbed X Y f),
  edist x y = ∑' (i : ι), min (2⁻¹ ^ Encodable.encode i) (edist (f i x.ofPiNat) (f i y.ofPiNat))
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.limitRecOn_zero : ∀ {motive : Ordinal.{u_4} → Sort u_5} (H₁ : motive 0) (H₂ : (o : Ordinal.{u_4}) → motive o → motive (o + 1))
  (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o),
  Ordinal.limitRecOn 0 H₁ H₂ H₃ = H₁
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pos.revFind?_char_eq_revFind?_beq : ∀ {c : Char} {s : String.Slice} {p : s.Pos}, p.revFind? c = p.revFind? fun x => x == c
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat : ∀ {X : AlgebraicGeometry.Scheme} [CompactSpace ↥X], AlgebraicGeometry.QuasiCompact X.toSpecΓ
-- Mathlib.RingTheory.Localization.Integer
IsLocalization.isInteger_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  IsLocalization.IsInteger R 0
-- Init.Data.Array.Zip
Array.lt_size_right_of_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {i : ℕ} {as : Array α} {bs : Array β},
  i < (Array.zipWith f as bs).size → i < bs.size
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.unit_eq : ∀ {α : outParam (Type u)} {β : Type v} [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] (l : Std.Sat.Literal α),
  Std.Tactic.BVDecide.LRAT.Internal.Clause.toList (Std.Tactic.BVDecide.LRAT.Internal.Clause.unit l) = [l]
-- Mathlib.Algebra.Group.AddChar
/-- Interpret an additive character as a monoid homomorphism.  -/
AddChar.toMonoidHom : {A : Type u_1} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : Monoid M] → AddChar A M → Multiplicative A →* M
-- Init.Data.List.Basic
List.findIdx?.go : {α : Type u} → (α → Bool) → List α → ℕ → Option ℕ
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.congrHash : Lean.Meta.Grind.ENodeMap → Lean.Expr → UInt64
-- Init.Data.Array.Erase
Array.eraseP_filter : ∀ {α : Type u_1} {p f : α → Bool} {xs : Array α},
  (Array.filter f xs).eraseP p = Array.filter f (xs.eraseP fun x => p x && f x)
-- Mathlib.Data.Nat.Totient
Nat.totient_lt : ∀ (n : ℕ), 1 < n → n.totient < n
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_mem_cycles₁_of_mem_invariants : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g : G),
  ∀ a ∈ A.ρ.invariants, (fun₀ | g => a) ∈ groupHomology.cycles₁ A
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.preimage_mul_left_closedEBall`. -/
EMetric.preimage_mul_left_closedBall : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ENNReal),
  (fun x => a * x) ⁻¹' Metric.closedEBall b r = Metric.closedEBall (a⁻¹ * b) r
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.le_measure_sdiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, μ s₁ - μ s₂ ≤ μ (s₁ \ s₂)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app_assoc : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (m₁ m₂ m₃ : A) (X : C) {Z : C}
  (h :
    (CategoryTheory.shiftFunctor C m₁).obj
        ((CategoryTheory.shiftFunctor C m₃).obj ((CategoryTheory.shiftFunctor C m₂).obj X)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C m₁).map ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app X)) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app ((CategoryTheory.shiftFunctor C m₁).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C m₃).map ((CategoryTheory.shiftFunctorComm C m₁ m₂).hom.app X))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctorComm C m₁ m₃).hom.app ((CategoryTheory.shiftFunctor C m₂).obj X)) h))
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic_right : ∀ {F : Type u_1} [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K)
  [halg : Algebra.IsAlgebraic F ↥L], (IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.instSigmaFiniteProdVolume : ∀ {α : Type u_4} {β : Type u_5} [inst : MeasureTheory.MeasureSpace α] [MeasureTheory.SigmaFinite MeasureTheory.volume]
  [inst_2 : MeasureTheory.MeasureSpace β] [MeasureTheory.SigmaFinite MeasureTheory.volume],
  MeasureTheory.SigmaFinite MeasureTheory.volume
-- Aesop.Util.UnorderedArraySet
Aesop.UnorderedArraySet.instToMessageData : {α : Type} → [inst : BEq α] → [Lean.ToMessageData α] → Lean.ToMessageData (Aesop.UnorderedArraySet α)
-- Init.Data.UInt.Lemmas
UInt8.one_def : 1 = { toBitVec := 1 }
-- Mathlib.Data.Fintype.Defs
/-- Construct a fintype from a finset with the same elements.  -/
Fintype.ofFinset : {α : Type u_1} → {p : Set α} → (s : Finset α) → (∀ (x : α), x ∈ s ↔ x ∈ p) → Fintype ↑p
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.refl_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂), (CategoryTheory.ShortComplex.Homotopy.refl φ).h₃ = 0
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Hom.comp_toFun' : ∀ {X Y Z : Pointed} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).toFun = g.toFun ∘ f.toFun
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fdiv_cancel_of_dvd : ∀ {a b : ℤ}, b ∣ a → b * a.fdiv b = a
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.cases : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (α : W.LeftFraction X Y), ∃ Y' f s, ∃ (hs : W s), α = { Y' := Y', f := f, s := s, hs := hs }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensRangeParams.textDocument : Lean.Lsp.SemanticTokensRangeParams → Lean.Lsp.TextDocumentIdentifier
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences_fst_le_snd : ∀ {x y : NNReal} (n m : ℕ), (x.agmSequences y n).1 ≤ (x.agmSequences y m).2
-- Init.Data.SInt.Lemmas
ISize.toInt_ofIntLE : ∀ {x : ℤ} {h₁ : ISize.minValue.toInt ≤ x} {h₂ : x ≤ ISize.maxValue.toInt}, (ISize.ofIntLE x h₁ h₂).toInt = x
-- Mathlib.Topology.Algebra.ConstMulAction
IsUnit.isQuotientMap_smul : ∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α] {S : Type u_4} {β : Type u_5} [inst_4 : SMul S M] [inst_5 : SMul S α] [IsScalarTower S M α]
  [inst_7 : SMul S β] (f : α →ₑ[id] β) [inst_8 : TopologicalSpace β],
  Topology.IsQuotientMap ⇑f → ∀ (c : S), IsUnit (c • 1) → Topology.IsQuotientMap fun x => c • x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {a : α}, Std.DTreeMap.Raw.Const.get? ∅ a = none
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.spineToSimplex_zero : ∀ {X : SSet} (h : (n : ℕ) → X.StrictSegalCore n) (p : X.Path 0), SSet.StrictSegalCore.spineToSimplex h p = p.vertex 0
-- Init.Grind.AC
Lean.Grind.AC.Seq.unionFuel_k_eq_unionFuel : ∀ (fuel : ℕ) (s₁ s₂ : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.unionFuel_k fuel s₁ s₂ = Lean.Grind.AC.Seq.unionFuel fuel s₁ s₂
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.map_bijective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X Y : C), Function.Bijective F.map
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- If `X ⟶ Spec A` is a morphism of schemes, then `Spec` of `specTargetImage f` is the
scheme-theoretic image of `f` and `f` factors as
`specTargetImageFactorization f ≫ Spec.map (specTargetImageRingHom f)`
(see `specTargetImageFactorization_comp`).  -/
AlgebraicGeometry.specTargetImage : {X : AlgebraicGeometry.Scheme} → {A : CommRingCat} → (X ⟶ AlgebraicGeometry.Spec A) → CommRingCat
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- A modification `Γ` between oplax natural transformations `η` and `θ` consists of a family of
2-morphisms `Γ.app a : η.app a ⟶ θ.app a`, which satisfies the equation
`(F.map f ◁ app b) ≫ θ.naturality f = η.naturality f ≫ (app a ▷ G.map f)`
for each 1-morphism `f : a ⟶ b`.
 -/
CategoryTheory.Oplax.OplaxTrans.Modification : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → (F ⟶ G) → (F ⟶ G) → Type (max u₁ w₂)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
/-- Extension for the `positivity` tactic: `SzemerediRegularity.bound` is always positive.  -/
Mathlib.Meta.Positivity.evalBound : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.coe_subtype : ∀ {R : Type u_1} [inst : Ring R] (I : TwoSidedIdeal R), ⇑I.subtype = Subtype.val
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.map_involutive : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {f : α → α}, Function.Involutive f → Function.Involutive fun M => M.map f
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.hasSum_inner_mul_inner : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (x y : E),
  HasSum (fun i => inner 𝕜 x (b i) * inner 𝕜 (b i) y) (inner 𝕜 x y)
-- Aesop.Tree.Traversal
Aesop.preTraverseDown : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT (ST IO.RealWorld) m] →
      (Aesop.GoalRef → m Bool) → (Aesop.RappRef → m Bool) → (Aesop.MVarClusterRef → m Bool) → Aesop.TreeRef → m Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The multifork associated to the multiequalizer.  -/
CategoryTheory.Limits.Multiequalizer.multifork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        [CategoryTheory.Limits.HasMultiequalizer I] → CategoryTheory.Limits.Multifork I
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {f : E → ContinuousMultilinearMap 𝕜 G H} {f' : E →L[𝕜] ContinuousMultilinearMap 𝕜 G H}
  {g : (i : ι) → E → F i →L[𝕜] G i} {g' : (i : ι) → E →L[𝕜] F i →L[𝕜] G i} {s : Set E} {x : E} [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι],
  HasFDerivWithinAt f f' s x →
    (∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x) →
      HasFDerivWithinAt (fun x => (f x).compContinuousLinearMap fun x_1 => g x_1 x)
        ((ContinuousMultilinearMap.compContinuousLinearMapL fun x_1 => g x_1 x) ∘SL f' +
          ((f x).fderivCompContinuousLinearMap fun x_1 => g x_1 x) ∘SL ContinuousLinearMap.pi g')
        s x
-- Mathlib.Algebra.Order.Field.Basic
lt_of_neg_of_one_div_lt_one_div : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  b < 0 → 1 / a < 1 / b → b < a
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C)
  (x : CategoryTheory.Limits.WalkingReflexivePair),
  (CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair F).inv.app x =
    match x with
    | CategoryTheory.Limits.WalkingReflexivePair.zero =>
      CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
    | CategoryTheory.Limits.WalkingReflexivePair.one =>
      CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingReflexivePair.one)
-- Mathlib.Algebra.Module.Presentation.Cokernel
/-- The presentation of the cokernel of a linear map `f : M₁ →ₗ[A] M₂` that is obtained
from a presentation `pres₂` of `M₂`, a choice of generators `g₁ : ι → M₁` of `M₁`,
and an additional data in `pres₂.CokernelData f g₁`.  -/
Module.Presentation.cokernel : {A : Type u} →
  [inst : Ring A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module A M₁] →
            [inst_3 : AddCommGroup M₂] →
              [inst_4 : Module A M₂] →
                (pres₂ : Module.Presentation A M₂) →
                  {f : M₁ →ₗ[A] M₂} →
                    {ι : Type w₁} →
                      {g₁ : ι → M₁} →
                        pres₂.CokernelData f g₁ →
                          Submodule.span A (Set.range g₁) = ⊤ → Module.Presentation A (M₂ ⧸ f.range)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.adj_congr : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {G H : Graph α β},
  x ∈ H.vertexSet → y ∈ H.vertexSet → H.IsInducedSubgraph G → (H.Adj x y ↔ G.Adj x y)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.isEmpty_inter_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∩ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∉ m₂
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets.eq_1 : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} (s1 s2 : Set (Set Ω)) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.IndepSets s1 s2 μ =
    ProbabilityTheory.Kernel.IndepSets s1 s2 (ProbabilityTheory.Kernel.const Unit μ) (MeasureTheory.Measure.dirac ())
-- Init.Data.Array.Lemmas
Array.exists_of_mem_map : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {l : Array α} {b : α_1}, b ∈ Array.map f l → ∃ a ∈ l, f a = b
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.iff_smoothOfRelativeDimension_zero : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Etale f ↔ AlgebraicGeometry.SmoothOfRelativeDimension 0 f
-- Mathlib.Algebra.Module.ZMod
ZMod.map_smul : ∀ {n : ℕ} {M : Type u_1} {M₁ : Type u_2} {F : Type u_3} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₁]
  [inst_2 : FunLike F M M₁] [AddMonoidHomClass F M M₁] [inst_4 : Module (ZMod n) M] [inst_5 : Module (ZMod n) M₁]
  (f : F) (c : ZMod n) (x : M), f (c • x) = c • f x
-- Lean.Data.PersistentArray
Lean.PersistentArray.instToStringStats : ToString Lean.PersistentArray.Stats
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instIsScalarTowerOfSMul : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)]
  [inst_1 : (i : ι) → SMul N (α i)] [inst_2 : SMul M N] [∀ (i : ι), IsScalarTower M N (α i)],
  IsScalarTower M N ((i : ι) × α i)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- `evalOp(F)` preserves arbitrary products.  -/
CategoryTheory.Limits.FormalCoproduct.isLimitEvalMapConeCofanOp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_2 : CategoryTheory.Limits.HasProducts A] →
          (J : Type w) →
            (f : J → CategoryTheory.Limits.FormalCoproduct C) →
              (F : CategoryTheory.Functor Cᵒᵖ A) →
                CategoryTheory.Limits.IsLimit
                  (((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F).mapCone
                    (CategoryTheory.Limits.FormalCoproduct.cofan J f).op)
-- Mathlib.Order.Lattice
/-- **Alias** of the reverse direction of `pairwise_iff_gt`. -/
Pairwise.of_gt : ∀ {α : Type u} [inst : LinearOrder α] {p : α → α → Prop} [Std.Symm p], (∀ ⦃a b : α⦄, b < a → p a b) → Pairwise p
-- Mathlib.Order.Northcott
Northcott.mk : ∀ {α : Type u_1} {β : Type u_2} {h : α → β} [inst : LE β], (∀ (b : β), {a | h a ≤ b}.Finite) → Northcott h
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit.eq_1 : ∀ {α : Type u} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ α] (t : Std.DTreeMap.Internal.Impl α fun x => Unit)
  (l : ρ) (h : t.Balanced),
  Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l h =
    (have r := ⟨t, ⋯⟩;
      do
      let __s ←
        forIn l r fun a __s =>
            let r := __s;
            have hr := ⋯;
            have r := ⟨(Std.DTreeMap.Internal.Impl.insertIfNew a () (↑r) hr).impl, ⋯⟩;
            pure (ForInStep.yield r)
      have r : Std.DTreeMap.Internal.Impl.Const.IteratedUnitInsertionInto t := __s
      pure r).run
-- Mathlib.Algebra.Group.Semiconj.Basic
/-- **Alias** of the reverse direction of `AddSemiconjBy.neg_right_iff`. -/
AddSemiconjBy.neg_right : ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy a x y → AddSemiconjBy a (-x) (-y)
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.hasCoeToSort : {B : Type u_1} →
  {C : Type u_2} →
    {F : B → C} → {α : Sort u_3} → [CoeSort C α] → CoeSort (CategoryTheory.Bicategory.InducedBicategory C F) α
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.dist_map : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (x y : P),
  dist (e x) (e y) = dist x y
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The over category has any connected limit which the original category has.  -/
CategoryTheory.Over.hasLimitsOfShape_of_isConnected : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {B : C} [CategoryTheory.IsConnected J] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Over B)
-- Mathlib.Order.RelSeries
RelSeries.head_mem : ∀ {α : Type u_1} {r : SetRel α α} (x : RelSeries r), x.head ∈ x
-- Mathlib.Data.Finset.Lattice.Fold
Finset.apply_sup_eq_sup_comp_of_nonempty : ∀ {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : LinearOrder α] {s : Finset ι} {f : ι → α} [inst_1 : OrderBot α]
  [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β] {g : α → β}, Monotone g → s.Nonempty → g (s.sup f) = s.sup (g ∘ f)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelFactorThruImage_hom_comp_ι : ∀ {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.CategoryStruct.comp (CategoryTheory.Limits.kernelFactorThruImage f).hom
      (CategoryTheory.Limits.kernel.ι f) =
    CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.factorThruImage f)
-- Init.Data.String.Basic
/-- Given a slice and a valid position within the slice, obtain a new slice on the same underlying
string by replacing the start of the slice with the given position.  -/
String.Slice.sliceFrom : (s : String.Slice) → s.Pos → String.Slice