mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.HasSubst.X_comp : ∀ {σ : Type u_1} {τ : Type u_2} (f : σ → τ) [Filter.TendstoCofinite f] {R : Type u_6} [inst : CommRing R],
  MvPowerSeries.HasSubst (MvPowerSeries.X ∘ f)
-- Mathlib.Order.Directed
exists_lt_of_directed_le : ∀ (β : Type u_2) [inst : PartialOrder β] [Nontrivial β] [IsDirectedOrder β], ∃ a b, b < a
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.support_mul_subset_right : ∀ {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β] {g₁ g₂ : α →₀ β}, (g₁ * g₂).support ⊆ g₂.support
-- Mathlib.Algebra.BigOperators.Ring.List
List.sum_map_mul_left : ∀ {ι : Type u_1} {R : Type u_5} [inst : NonUnitalNonAssocSemiring R] (l : List ι) (f : ι → R) (r : R),
  (List.map (fun b => r * f b) l).sum = r * (List.map f l).sum
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indep_comap_process_of_prod_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {m mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [MeasureTheory.IsProbabilityMeasure P],
  m ≤ mΩ →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (A : Set Ω),
          MeasurableSet A →
            ∀ (I : Finset S) (f : (s : ↥I) → BoundedContinuousFunction (E ↑s) ℝ),
              ∫ (ω : Ω) in A, ∏ s, (f s) (X (↑s) ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X (↑s) ω) ∂P) →
        ProbabilityTheory.Indep m (MeasurableSpace.comap (fun ω s => X s ω) MeasurableSpace.pi) P
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.eq_curry_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y : C}
  [inst_2 : CategoryTheory.Closed A] (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ X) (g : Y ⟶ A ⟹ X),
  g = CategoryTheory.MonoidalClosed.curry f ↔ CategoryTheory.MonoidalClosed.uncurry g = f
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.toRat.match_1.eq_3 : ∀ (motive : Dyadic → Sort u_1) (n : ℤ) (k : ℕ) (hn : n % 2 = 1) (h_1 : Unit → motive Dyadic.zero)
  (h_2 : (n : ℤ) → (k : ℕ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n (Int.ofNat k) hn))
  (h_3 : (n : ℤ) → (k : ℕ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n (Int.negSucc k) hn)),
  (match Dyadic.ofOdd n (Int.negSucc k) hn with
    | Dyadic.zero => h_1 ()
    | Dyadic.ofOdd n (Int.ofNat k) hn => h_2 n k hn
    | Dyadic.ofOdd n (Int.negSucc k) hn => h_3 n k hn) =
    h_3 n k hn
-- Mathlib.Data.ENat.Basic
ENat.self_le_mul_right : ∀ {c : ℕ∞} (a : ℕ∞), c ≠ 0 → a ≤ a * c
-- Mathlib.Analysis.Real.Sqrt
Real.mul_self_sqrt : ∀ {x : ℝ}, 0 ≤ x → √x * √x = x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- If `G` preserves the coproduct of `(X,Y)`, then the coproduct comparison map for `G` at `(X,Y)` is
an isomorphism.
 -/
CategoryTheory.Limits.PreservesColimitPair.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          (X Y : C) →
            [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y] →
              [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)] →
                [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G] →
                  G.obj X ⨿ G.obj Y ≅ G.obj (X ⨿ Y)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.sq_norm_lt_one : ∀ (z : Complex.UnitClosedDisc), ‖↑z‖ ^ 2 ≤ 1
-- Std.Data.HashMap.Basic
Std.HashMap.instInsertProd : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Insert (α × β) (Std.HashMap α β)
-- Aesop.Rule.Forward
Aesop.ForwardRulePriority.unsafe.inj : ∀ {p p_1 : Aesop.Percent}, Aesop.ForwardRulePriority.unsafe p = Aesop.ForwardRulePriority.unsafe p_1 → p = p_1
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instDistrib : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : Distrib R] → [ContinuousMul R] → [ContinuousAdd R] → Distrib (SeparationQuotient R)
-- Mathlib.Algebra.Category.Grp.FilteredColimits
CommGrpCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget CommGrpCat)
-- Init.Data.BitVec.Lemmas
BitVec.lt_of_getElem?_eq_some : ∀ {w : ℕ} {b : Bool} (x : BitVec w) (i : ℕ), x[i]? = some b → i < w
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- Integral of a 1-form `ω : E → E →L[𝕜] F` along a path `γ`,
defined as $\int_0^1 \omega(\gamma(t))(\gamma'(t))$.

The actual definition uses `curveIntegralFun` which uses `Path.extend γ`
and `derivWithin (Path.extend γ) (Set.Icc 0 1) t`,
because calculus-related definitions in Mathlib expect globally defined functions as arguments.  -/
«term∫ᶜ_In_,_» : Lean.ParserDescr
-- Lean.Compiler.IR.Format
_private.Lean.Compiler.IR.Format.0.Lean.IR.formatIRType : Lean.IR.IRType → Std.Format
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂Iso_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : C ≌ A} {G : D ≌ B}
  (α : F.functor.comp U ⟶ S.comp G.functor) (α' : F.inverse.comp S ⟶ U.comp G.inverse)
  (hα'α :
    CategoryTheory.CategoryStruct.comp S.leftUnitor.hom
        (CategoryTheory.CategoryStruct.comp S.rightUnitor.inv
          (CategoryTheory.CategoryStruct.comp (S.whiskerLeft G.unitIso.hom) (S.associator G.functor G.inverse).inv)) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom S)
        (CategoryTheory.CategoryStruct.comp (F.functor.associator F.inverse S).hom
          (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft α')
            (CategoryTheory.CategoryStruct.comp (F.functor.associator U G.inverse).inv
              (CategoryTheory.Functor.whiskerRight α G.inverse)))))
  (hαα' :
    CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft α)
        (CategoryTheory.CategoryStruct.comp (F.inverse.associator S G.functor).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α' G.functor)
            (CategoryTheory.CategoryStruct.comp (U.associator G.inverse G.functor).hom
              (U.whiskerLeft G.counitIso.hom)))) =
      CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor U).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.counitIso.hom U)
          (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv)))
  (β : G.functor.obj T ⟶ V) (β' : G.inverse.obj V ⟶ T)
  (hββ' : CategoryTheory.CategoryStruct.comp (G.inverse.map β) β' = G.unitIso.inv.app T)
  (hβ'β : CategoryTheory.CategoryStruct.comp (G.functor.map β') β = G.counitIso.hom.app V),
  (CategoryTheory.CostructuredArrow.map₂Iso α α' hα'α hαα' β β' hββ' hβ'β).unitIso =
    (CategoryTheory.CostructuredArrow.map₂IdIso (CategoryTheory.CategoryStruct.comp S.leftUnitor.hom S.rightUnitor.inv)
          T (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id D).obj T)) ⋯ ⋯).symm ≪≫
      CategoryTheory.CostructuredArrow.map₂Congr (CategoryTheory.CategoryStruct.comp S.leftUnitor.hom S.rightUnitor.inv)
          (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id D).obj T)) F.unitIso G.unitIso
          (CategoryTheory.CategoryStruct.comp (F.functor.associator F.inverse S).hom
            (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft α')
              (CategoryTheory.CategoryStruct.comp (F.functor.associator U G.inverse).inv
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α G.inverse)
                  (S.associator G.functor G.inverse).hom))))
          (CategoryTheory.CategoryStruct.comp (G.inverse.map β) β') ⋯ ⋯ ≪≫
        (CategoryTheory.CostructuredArrow.map₂CompMap₂Iso α' β' α β).symm
-- Std.Internal.UV.System
/-- Gets the path to the current user's home directory.
 -/
Std.Internal.UV.System.osHomedir : IO String
-- Init.Data.List.Sublist
List.IsInfix.eq_1 : ∀ {α : Type u} (l₁ l₂ : List α), (l₁ <:+: l₂) = ∃ s t, s ++ l₁ ++ t = l₂
-- Mathlib.Tactic.Simproc.Factors
/-- A proof of the partial computation of `primeFactorsList`.
Asserts that `l` is a sorted list of primes multiplying to `n` and lower bounded by a prime `p`.  -/
Mathlib.Meta.Simproc.FactorsHelper : ℕ → ℕ → List ℕ → Prop
-- Mathlib.Order.SuccPred.Limit
Order.isPredLimit_toDual_iff : ∀ {α : Type u_1} {a : α} [inst : Preorder α], Order.IsPredLimit (OrderDual.toDual a) ↔ Order.IsSuccLimit a
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.signalInterest : {m : Type → Type} →
  [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → [MonadLiftT BaseIO m] → Std.AtomicT Std.Http.Body.Channel.State✝ m Unit
-- Mathlib.Algebra.Lie.Weights.Killing
/-- If the Killing form of a Lie algebra is non-singular, it remains non-singular when restricted
to a Cartan subalgebra.  -/
LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsKilling R L] [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra],
  LinearMap.ker ((killingForm R L).restrict H.toSubmodule) = ⊥
-- Mathlib.Data.PFun
PFun.preimage_mono : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) {s t : Set β}, s ⊆ t → f.preimage s ⊆ f.preimage t
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.homMk_id : ∀ {V : SSet.Truncated 2} (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })),
  SSet.Truncated.HomotopyCategory.homMk (SSet.Truncated.Edge.id x) =
    CategoryTheory.CategoryStruct.id (SSet.Truncated.HomotopyCategory.mk x)
-- Mathlib.Analysis.Normed.Ring.Basic
enorm_one : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] [inst_1 : One G] [NormOneClass G], ‖1‖ₑ = 1
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Typecheck an `IntertwiningMap` as a morphism in `Rep`.  -/
Rep.ofHom : {k : Type u} →
  {G : Type v} →
    [inst : Semiring k] →
      [inst_1 : Monoid G] →
        {X Y : Type w} →
          [inst_2 : AddCommGroup X] →
            [inst_3 : AddCommGroup Y] →
              [inst_4 : Module k X] →
                [inst_5 : Module k Y] →
                  {ρ : Representation k G X} → {σ : Representation k G Y} → ρ.IntertwiningMap σ → (Rep.of ρ ⟶ Rep.of σ)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.instInhabited : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : Zero R] → Inhabited (HahnSeries Γ R)
-- Mathlib.Topology.Algebra.ConstMulAction
IsUnit.smul_mem_nhds_smul_iff : ∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α] {c : M}, IsUnit c → ∀ {s : Set α} {a : α}, c • s ∈ nhds (c • a) ↔ s ∈ nhds a
-- Mathlib.Algebra.Star.Pointwise
Set.star_add : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] (s t : Set α), star (s + t) = star s + star t
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapPreimage.eq_1 : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type w} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N} (hf : Function.Surjective ⇑f)
  (x : AdicCompletion.AdicCauchySequence I N), AdicCompletion.mapPreimage✝ hf x Nat.zero = ⟨⋯.choose, ⋯⟩
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor on `AddCommGrpCat.{u}` creates `u`-small limits.  -/
AddCommGrpCat.instCreatesLimitsOfSizeUliftFunctor : CategoryTheory.CreatesLimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} AddCommGrpCat.uliftFunctor
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.existsUnique_isPrime : ∀ (R : Type u_1) [inst : CommSemiring R] [Ring.KrullDimLE 0 R] [IsLocalRing R], ∃! I, I.IsPrime
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ψ_zero : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.ψ 0 = 0
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- **The Jordan decomposition theorem**: Given a signed measure `s`, there exists a pair of
mutually singular measures `μ` and `ν` such that `s = μ - ν`. In this case, the measures `μ`
and `ν` are given by `s.toJordanDecomposition.posPart` and
`s.toJordanDecomposition.negPart` respectively.

Note that we use `MeasureTheory.JordanDecomposition.toSignedMeasure` to represent the
signed measure corresponding to
`s.toJordanDecomposition.posPart - s.toJordanDecomposition.negPart`.  -/
MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
  s.toJordanDecomposition.toSignedMeasure = s
-- Init.Data.String.Decode
Char.utf8Size.fun_cases_unfolding : ∀ (c : Char) (motive : ℕ → Prop),
  (have v := c.val;
    v ≤ UInt32.ofNatLT 127 Char.utf8Size._proof_1 → motive 1) →
    (have v := c.val;
      ¬v ≤ UInt32.ofNatLT 127 Char.utf8Size._proof_1 → v ≤ UInt32.ofNatLT 2047 Char.utf8Size._proof_2 → motive 2) →
      (have v := c.val;
        ¬v ≤ UInt32.ofNatLT 127 Char.utf8Size._proof_1 →
          ¬v ≤ UInt32.ofNatLT 2047 Char.utf8Size._proof_2 →
            v ≤ UInt32.ofNatLT 65535 Char.utf8Size._proof_3 → motive 3) →
        (have v := c.val;
          ¬v ≤ UInt32.ofNatLT 127 Char.utf8Size._proof_1 →
            ¬v ≤ UInt32.ofNatLT 2047 Char.utf8Size._proof_2 →
              ¬v ≤ UInt32.ofNatLT 65535 Char.utf8Size._proof_3 → motive 4) →
          motive c.utf8Size
-- Lean.Parser.Types
Lean.Parser.ParserState.pos : Lean.Parser.ParserState → String.Pos.Raw
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.eval₂_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* S) (k : σ → τ) (g : τ → S) (p : MvPolynomial σ R),
  MvPolynomial.eval₂ f g ((MvPolynomial.rename k) p) = MvPolynomial.eval₂ f (g ∘ k) p
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instDivInvMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivInvMonoid α],
  Lex.instDivInvMonoid =
    { toMonoid := Lex.instMonoid, toInv := Lex.instInv, toDiv := Lex.instDiv, toZPow := ZPow.ofPow, div_eq_mul_inv := ⋯,
      zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯ }
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsExistential.of_isQF : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsQF → φ.IsExistential
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorObjImpl.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  X.tensorObjImpl Y =
    { src := X.src ⨯ Y.src, tgt := X.tgt ⨯ Y.tgt,
      rel :=
        (CategoryTheory.Subobject.pullback
                (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)).obj
            X.rel ⊓
          (CategoryTheory.Subobject.pullback
                (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)).obj
            Y.rel }
-- Init.Data.Vector.Lemmas
/-- Variant of `any_eq` in terms of membership rather than an array index.  -/
Vector.any_eq' : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, xs.any p = decide (∃ x ∈ xs, p x = true)
-- Mathlib.Algebra.GradedMonoid
SetLike.pow_mem_graded : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Monoid R] [inst_2 : AddMonoid ι]
  {A : ι → S} [SetLike.GradedMonoid A] (n : ℕ) {r : R} {i : ι}, r ∈ A i → r ^ n ∈ A (n • i)
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.forget_preservesFilteredColimits : ∀ {R : Type u} [inst : Ring R], CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget (ModuleCat R))
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.requestCancelled.sizeOf_spec : sizeOf Lean.JsonRpc.ErrorCode.requestCancelled = 1
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.AbelianStruct.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          (kernelFork : CategoryTheory.Limits.KernelFork f) →
            CategoryTheory.Limits.IsLimit kernelFork →
              (cokernelCofork : CategoryTheory.Limits.CokernelCofork f) →
                CategoryTheory.Limits.IsColimit cokernelCofork →
                  (image : C) →
                    (imageπ : X ⟶ image) →
                      (ι_imageπ :
                          autoParam
                            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kernelFork) imageπ = 0)
                            CategoryTheory.Abelian.AbelianStruct.ι_imageπ._autoParam) →
                        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ imageπ ι_imageπ) →
                          (imageι : image ⟶ Y) →
                            (imageι_π :
                                autoParam
                                  (CategoryTheory.CategoryStruct.comp imageι
                                      (CategoryTheory.Limits.Cofork.π cokernelCofork) =
                                    0)
                                  CategoryTheory.Abelian.AbelianStruct.imageι_π._autoParam) →
                              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι imageι imageι_π) →
                                autoParam (CategoryTheory.CategoryStruct.comp imageπ imageι = f)
                                    CategoryTheory.Abelian.AbelianStruct.fac._autoParam →
                                  CategoryTheory.Abelian.AbelianStruct f
-- Init.Data.Iterators.Lemmas.Combinators.Append
Std.Iter.toArray_append : ∀ {α₁ α₂ β : Type w} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [Std.Iterators.Finite α₁ Id]
  [Std.Iterators.Finite α₂ Id] {it₁ : Std.Iter β} {it₂ : Std.Iter β},
  (it₁.append it₂).toArray = it₁.toArray ++ it₂.toArray
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
/-- The monad for the Simplex Algorithm.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmM : (matType : ℕ → ℕ → Type) → [Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] → Type → Type
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoend.map_comp : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C]
  {G H : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (f : F ⟶ G) (g : G ⟶ H),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.map f)
      (CategoryTheory.Limits.chosenCoend.map g) =
    CategoryTheory.Limits.chosenCoend.map (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.GroupTheory.Index
Subgroup.index_antitone : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ K → ∀ [H.FiniteIndex], K.index ≤ H.index
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_inv_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.mop =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor { unmop := X }).inv
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.IsGeneratedBy.iSup_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  {G : CategoryTheory.Subfunctor F} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)},
  G.IsGeneratedBy x → ⨆ i, CategoryTheory.Subfunctor.ofSection (x i) = G
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- The inclusion `(P^(i + 1) / P^e) ⊂ (P^i / P^e)`.  -/
Ideal.powQuotSuccInclusion : {R : Type u} →
  [inst : CommRing R] →
    {S : Type v} →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : Ideal R) →
            (P : Ideal S) →
              (i : ℕ) →
                ↥(Ideal.map (Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (P ^ (i + 1))) →ₗ[R ⧸ p]
                  ↥(Ideal.map (Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (P ^ i))
-- Init.Data.Int.Lemmas
Ne.eq_1 : ∀ {α : Sort u} (a b : α), (a ≠ b) = ¬a = b
-- Mathlib.Data.Seq.Computation
Computation.liftRelAux_inl_inr : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {C : Computation α → Computation β → Prop} {a : α} {cb : Computation β},
  Computation.LiftRelAux R C (Sum.inl a) (Sum.inr cb) = ∃ b ∈ cb, R a b
-- Init.Data.String.Basic
String.Pos.cast_le_cast_iff : ∀ {s t : String} {pos pos' : s.Pos} {h : s = t}, pos.cast h ≤ pos'.cast h ↔ pos ≤ pos'
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.instEpiFromFreeYonedaCoproduct : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R), CategoryTheory.Epi M.fromFreeYonedaCoproduct
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
/-- The projections maps assemble into a wedge.  -/
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.hπ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  (self : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) (c : C) ⦃i j : C⦄ (f : i ⟶ j) {Z : V}
  (h : F.obj i ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.π c i)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ihom (F.obj i)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))) h) =
    CategoryTheory.CategoryStruct.comp (self.π c j)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalClosed.pre (F.map f)).app
          (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c)))
        h)
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.collect : Lean.Level → Lean.CollectLevelParams.Visitor
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.CollectDecVars.CollectDecVarsM.run : Lean.Meta.Grind.Arith.CollectDecVarsM Unit → Lean.FVarIdSet → Lean.FVarIdSet
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.div_vle_one_iff : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {a b : K}, b ≠ 0 → (a / b ≤ᵥ 1 ↔ a ≤ᵥ b)
-- Mathlib.Order.Category.PartOrdEmb
/-- Given a predicate `P : Set α → Prop` on the underlying type of `α : PartOrdEmb.{u}`,
this is the cocone with point `α` given by all the inclusions of the subsets
satisfying `P`.  -/
PartOrdEmb.coconeOfPredicateSet : {α : PartOrdEmb} → (P : Set ↑α → Prop) → CategoryTheory.Limits.Cocone (PartOrdEmb.functorOfPredicateSet P)
-- Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
IsDiscreteValuationRing.intValuation_maximalIdeal : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsDiscreteValuationRing A] (x : A),
  (IsDiscreteValuationRing.maximalIdeal A).intValuation x =
    (ENat.recTopCoe 0 (fun x => ↑(Multiplicative.ofAdd ↑x)) ((IsDiscreteValuationRing.addVal A) x))⁻¹
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
/-- Construct an object of the small affine étale site.  -/
AlgebraicGeometry.Scheme.AffineEtale.mk : {S : AlgebraicGeometry.Scheme} →
  {R : CommRingCat} → (f : AlgebraicGeometry.Spec R ⟶ S) → [AlgebraicGeometry.Etale f] → S.AffineEtale
-- Mathlib.Algebra.Ring.Defs
/-- One is a right neutral element for multiplication  -/
NonAssocRing.mul_one : ∀ {α : Type u_1} [self : NonAssocRing α] (a : α), a * 1 = a