mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.prodEquivalence_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : D) (S' : D') (T : CategoryTheory.Functor C D)
  (T' : CategoryTheory.Functor C' D'),
  (CategoryTheory.StructuredArrow.prodEquivalence S S' T T').unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun f =>
        CategoryTheory.Iso.refl
          ((CategoryTheory.Functor.id (CategoryTheory.StructuredArrow (S, S') (T.prod T'))).obj f))
      ⋯
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.set_StateT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ : Type u}
  {epost : EPred} (s : σ) (post : PUnit.{u + 1} → σ → Pred), ⦃ fun x => post PUnit.unit s ⦄ set s ⦃ post; epost ⦄
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.quotientEquivOrthogonal.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], K.quotientEquivOrthogonal = K.quotientEquivOrthogonal
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `FunLike.coe_zero`. -/
AddGroupSeminorm.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
/-- **Alias** of `CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit`. -/
CategoryTheory.Functor.chosenTerminalIsTerminal : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.SemiCartesianMonoidalCategory C] →
      CategoryTheory.Limits.IsTerminal (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Group.Ext
CommMonoid.mk.congr_simp : ∀ {M : Type u} [toMonoid : Monoid M] [toMonoid_1 : Monoid M] (e_toMonoid : toMonoid = toMonoid_1)
  (mul_comm : ∀ (a b : M), a * b = b * a),
  { toMonoid := toMonoid, mul_comm := mul_comm } = { toMonoid := toMonoid_1, mul_comm := ⋯ }
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.mk_eq_one_iff : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] {p : E}, SeparationQuotient.mk p = 1 ↔ ‖p‖ = 0
-- Mathlib.Data.Int.ModEq
Int.ModEq.dvd_iff : ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → (n ∣ a ↔ n ∣ b)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- If a finset `u` is contained in the product of two sets `s / t`, we can find two finsets `s'`,
`t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' / t'`.  -/
Finset.subset_div : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {u : Finset α} {s t : Set α},
  ↑u ⊆ s / t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' / t'
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instTransVleVlt : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : ValuativeRel R] → Trans ValuativeRel.vle ValuativeRel.vlt ValuativeRel.vlt
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateMulAct.mk.injEq : ∀ {α : Type u_1} {f : α → α} (val val_1 : ℕ), ({ val := val } = { val := val_1 }) = (val = val_1)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_mul_X : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] {p : Polynomial R},
  p ≠ 0 → (p * Polynomial.X).natDegree = p.natDegree + 1
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.add_def : ∀ {K : Type u_1} [inst : CommRing K] (x x_1 : RatFunc K),
  x.add x_1 =
    match x, x_1 with
    | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p + q }
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.add.match_1.splitter : (motive : ℤ → ℤ → Sort u_1) →
  (m n : ℤ) →
    ((m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) →
      ((m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) →
        ((m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n)) →
          ((m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)) → motive m n
-- Mathlib.Algebra.Quaternion
Cardinal.mk_univ_quaternionAlgebra_of_infinite : ∀ {R : Type u_1} (c₁ c₂ c₃ : R) [Infinite R], Cardinal.mk ↑Set.univ = Cardinal.mk R
-- Mathlib.Algebra.Group.Submonoid.Operations
AddEquiv.ofLeftInverse'.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) {g : N → M}
  (h : Function.LeftInverse g ⇑f),
  AddEquiv.ofLeftInverse' f h =
    { toFun := ⇑f.mrangeRestrict, invFun := g ∘ ⇑(AddMonoidHom.mrange f).subtype, left_inv := h, right_inv := ⋯,
      map_add' := ⋯ }
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.uniqueUpToIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t),
  P.uniqueUpToIso Q = { hom := Q.liftConeMorphism s, inv := P.liftConeMorphism t, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.CategoryTheory.Filtered.Final
/-- If `C` is filtered, then `F : C ⥤ D` is final if and only if `StructuredArrow d F` is filtered
for all `d : D`.  -/
CategoryTheory.Functor.final_iff_isFiltered_structuredArrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C],
  F.Final ↔ ∀ (d : D), CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow d F)
-- Mathlib.Data.List.Triplewise
List.triplewise_cons : ∀ {α : Type u_1} {a : α} {l : List α} {p : α → α → α → Prop},
  List.Triplewise p (a :: l) ↔ List.Pairwise (p a) l ∧ List.Triplewise p l
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
TopCat.exists_mem_zeroHypercover_range : ∀ {X : TopCat} (E : TopCat.precoverage.ZeroHypercover X) (x : ↑X),
  ∃ i, x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (E.f i))
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The presheaf `presheaf data G₀` extends `G₀`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.compPresheafIso : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    (data : (X : C) → F.OneHypercoverDenseData J₀ J X) →
                      [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                        (G₀ : CategoryTheory.Sheaf J₀ A) →
                          F.op.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf data G₀) ≅ G₀.obj
-- Lean.Data.Lsp.Basic
Lean.Lsp.instDecidableEqMarkupKind : DecidableEq Lean.Lsp.MarkupKind
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Fintype.sum_eq_sum_compl_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (a : ι)
  (f : ι → M), ∑ i, f i = ∑ i ∈ {a}ᶜ, f i + f a
-- Lean.Elab.Term.TermElabM
/-- Return `autoBoundImplicits ++ xs`
This method throws an error if a variable in `autoBoundImplicits` depends on some `x` in `xs`.
The `autoBoundImplicits` may contain free variables created by the auto-implicit feature, and unassigned free variables.
It avoids the hack used at `autoBoundImplicitsOld`.

If `inlayHintPos?` is set, this function also inserts an inlay hint denoting `autoBoundImplicits`.
See `addAutoBoundImplicitsInlayHint` for more information.

Remark: we cannot simply replace every occurrence of `addAutoBoundImplicitsOld` with this one because a particular
use-case may not be able to handle the metavariables in the array being given to `k`.
 -/
Lean.Elab.Term.addAutoBoundImplicits : Array Lean.Expr → Option String.Pos.Raw → Lean.Elab.TermElabM (Array Lean.Expr)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RoiSliceData.mk.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Roi α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α β) (range_1 : Std.Roi α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.subset_add_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddZeroClass α] {s : Finset α} (t : Finset α), 0 ∈ s → t ⊆ s + t
-- Lean.Parser.Term
Lean.Parser.Term.showRhs : Lean.Parser.Parser
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsPreBrownianReal.hasLaw_eval : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P →
    ∀ (t : NNReal), ProbabilityTheory.HasLaw (B t) (ProbabilityTheory.gaussianReal 0 t) P
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Expr.toPoly.go.match_1.eq_1 : ∀ (motive : Nat.Internal.Linear.Expr → Sort u_1) (k : ℕ) (h_1 : (k : ℕ) → motive (Nat.Internal.Linear.Expr.num k))
  (h_2 : (i : Nat.Internal.Linear.Var) → motive (Nat.Internal.Linear.Expr.var i))
  (h_3 : (a b : Nat.Internal.Linear.Expr) → motive (a.add b))
  (h_4 : (k : ℕ) → (a : Nat.Internal.Linear.Expr) → motive (Nat.Internal.Linear.Expr.mulL k a))
  (h_5 : (a : Nat.Internal.Linear.Expr) → (k : ℕ) → motive (a.mulR k)),
  (match Nat.Internal.Linear.Expr.num k with
    | Nat.Internal.Linear.Expr.num k => h_1 k
    | Nat.Internal.Linear.Expr.var i => h_2 i
    | a.add b => h_3 a b
    | Nat.Internal.Linear.Expr.mulL k a => h_4 k a
    | a.mulR k => h_5 a k) =
    h_1 k
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- In an oriented inner product space, the measure coming from the canonical volume form
associated to an orientation coincides with the volume.  -/
Orientation.measure_eq_volume : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : MeasurableSpace F]
  [inst_3 : BorelSpace F] [inst_4 : FiniteDimensional ℝ F] {n : ℕ} [_i : Fact (Module.finrank ℝ F = n)]
  (o : Orientation ℝ F (Fin n)), o.volumeForm.measure = MeasureTheory.volume
-- Mathlib.RingTheory.Bialgebra.TensorProduct
/-- The base ring is a left identity for the tensor product of bialgebras, up to
bialgebra equivalence.  -/
Bialgebra.TensorProduct.lid : (R : Type u_1) →
  (B : Type u_4) →
    [inst : CommSemiring R] → [inst_1 : Semiring B] → [inst_2 : Bialgebra R B] → TensorProduct R R B ≃ₐc[R] B
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (a : CategoryTheory.Abelian.Ext X Y n), R.extAddEquivCohomologyClass a = R.extEquivCohomologyClass a
-- Init.Data.Sum.Lemmas
Sum.isRight.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (val : β), (Sum.inr val).isRight = true
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.Context.completionInfoPos : Lean.Server.Completion.Context✝ → ℕ
-- Mathlib.AlgebraicGeometry.Scheme
/-- The subset of the underlying space where the given section does not vanish.  -/
AlgebraicGeometry.Scheme.basicOpen : (X : AlgebraicGeometry.Scheme) → {U : X.Opens} → ↑(X.presheaf.obj (Opposite.op U)) → X.Opens
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.Tree.mk : {α : Type u} →
  {β : α → Type v} →
    {size : ℕ} →
      (impl : Std.DTreeMap.Internal.Impl α β) →
        impl.Balanced → impl.size = size → Std.DTreeMap.Internal.Impl.Tree α β size
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_5 : CategoryTheory.HasWeakSheafify K AddCommGrpCat] [inst_6 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_7 : K.WEqualsLocallyBijective AddCommGrpCat] [inst_8 : F.Final] {I : Type u} (i : I),
  CategoryTheory.CategoryStruct.comp ((SheafOfModules.pullback φ).map (SheafOfModules.ιFree i))
      (SheafOfModules.pullbackObjFreeIso φ I).hom =
    CategoryTheory.CategoryStruct.comp (SheafOfModules.pullbackObjUnitToUnit φ) (SheafOfModules.ιFree i)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.homologyMap_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X Y Z : SSet) (f : X ⟶ Y) (g : Y ⟶ Z) (R : C)
  [inst_3 : CategoryTheory.CategoryWithHomology C] (n : ℕ) {Z_1 : C} (h : Z.homology R n ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (SSet.homologyMap (CategoryTheory.CategoryStruct.comp f g) R n) h =
    CategoryTheory.CategoryStruct.comp (SSet.homologyMap f R n)
      (CategoryTheory.CategoryStruct.comp (SSet.homologyMap g R n) h)
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.SeenCalls : Type
-- Mathlib.Algebra.Module.LinearMap.End
DistribSMul.toLinearMap_apply : ∀ (R : Type u_1) {S : Type u_3} (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DistribSMul S M] [inst_4 : SMulCommClass S R M] (s : S) (a : M), (DistribSMul.toLinearMap R M s) a = s • a
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- Negative part of a simple function in L1 space.  -/
MeasureTheory.L1.SimpleFunc.negPart : {α : Type u_1} → {m : MeasurableSpace α} → {μ : MeasureTheory.Measure α} → ↥(α →₁ₛ[μ] ℝ) → ↥(α →₁ₛ[μ] ℝ)
-- Init.Tactics
/-- `fail_if_success t` fails if the tactic `t` succeeds.  -/
Lean.Parser.Tactic.failIfSuccess : Lean.ParserDescr
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of an additive monoid is isomorphic to the center of its opposite.  -/
AddSubmonoid.centerToAddOpposite : {M : Type u_2} → [inst : AddZeroClass M] → ↥(AddSubmonoid.center M) ≃+ ↥(AddSubmonoid.center Mᵃᵒᵖ)
-- Mathlib.Algebra.MvPolynomial.Derivation
MvPolynomial.mkDerivation_monomial : ∀ {σ : Type u_1} (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] [inst_4 : IsScalarTower R (MvPolynomial σ R) A] (f : σ → A) (s : σ →₀ ℕ)
  (r : R),
  (MvPolynomial.mkDerivation R f) ((MvPolynomial.monomial s) r) =
    r • s.sum fun i k => (MvPolynomial.monomial (s - fun₀ | i => 1)) ↑k • f i
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instReprPoly : Repr Lean.Grind.Linarith.Poly
-- Mathlib.MeasureTheory.Integral.TorusIntegral
torusIntegral_neg : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : (Fin n → ℂ) → E) (c : Fin n → ℂ)
  (R : Fin n → ℝ), (∯ (x : Fin n → ℂ) in T(c, R), -f x) = -∯ (x : Fin n → ℂ) in T(c, R), f x
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m₁ \ m₂).get? k = if k ∈ m₂ then none else m₁.get? k
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_smul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {A : Type u_8} [inst_1 : SMulZeroClass A R] (a : A) (x : M →₀ R),
  MonoidAlgebra.ofCoeff (a • x) = a • MonoidAlgebra.ofCoeff x
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- “Divide” a functor by a faithful functor.  -/
CategoryTheory.Functor.Faithful.div : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C E) →
              (G : CategoryTheory.Functor D E) →
                [G.Faithful] →
                  (obj : C → D) →
                    (∀ (X : C), G.obj (obj X) = F.obj X) →
                      (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) →
                        (∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f) → CategoryTheory.Functor C D
-- Mathlib.Analysis.Complex.IntegerCompl
Complex.mem_integerComplement_iff : ∀ {x : ℂ}, x ∈ Complex.integerComplement ↔ ¬∃ n, ↑n = x
-- Mathlib.FieldTheory.PerfectClosure
/-- Lift a function `ℕ × K → L` to a function on `PerfectClosure K p`.  -/
PerfectClosure.liftOn : {K : Type u} →
  [inst : CommRing K] →
    {p : ℕ} →
      [inst_1 : Fact (Nat.Prime p)] →
        [inst_2 : CharP K p] →
          {L : Type u_1} →
            PerfectClosure K p → (f : ℕ × K → L) → (∀ (x y : ℕ × K), PerfectClosure.R K p x y → f x = f y) → L
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
CategoryTheory.Limits.HasIterationOfShape.mk : ∀ {J : Type w} [inst : LinearOrder J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C],
  autoParam (∀ (j : J), Order.IsSuccLimit j → CategoryTheory.Limits.HasColimitsOfShape (↑(Set.Iio j)) C)
      CategoryTheory.Limits.HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit._autoParam →
    autoParam (CategoryTheory.Limits.HasColimitsOfShape J C)
        CategoryTheory.Limits.HasIterationOfShape.hasColimitsOfShape._autoParam →
      CategoryTheory.Limits.HasIterationOfShape J C
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveCodeProps : Type
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet : (α : Type u) → [BEq α] → [Hashable α] → Type u
-- Mathlib.Algebra.Module.Submodule.Equiv
/-- A linear injection `M ↪ N` restricts to an equivalence `f⁻¹ p ≃ p` for any submodule `p`
contained in its range.  -/
Submodule.comap_equiv_self_of_inj_of_le : {R : Type u_1} →
  {M : Type u_5} →
    {N : Type u_9} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {f : M →ₗ[R] N} →
                  {p : Submodule R N} → Function.Injective ⇑f → p ≤ f.range → ↥(Submodule.comap f p) ≃ₗ[R] ↥p
-- Mathlib.Topology.UniformSpace.Cauchy
CauchySeq.comp_tendsto : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [inst : Preorder β]
  [inst_1 : SemilatticeSup γ] [Nonempty γ] {f : β → α},
  CauchySeq f → ∀ {g : γ → β}, Filter.Tendsto g Filter.atTop Filter.atTop → CauchySeq (f ∘ g)
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.Impl.size_leaf : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.leaf.size = 0
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mul_mem_mul : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I J : FractionalIdeal S P} {i j : P}, i ∈ I → j ∈ J → i * j ∈ I * J
-- Mathlib.Order.CompleteLattice.Basic
Prod.instCompleteLattice : {α : Type u_1} → {β : Type u_2} → [CompleteLattice α] → [CompleteLattice β] → CompleteLattice (α × β)
-- Mathlib.FieldTheory.Finite.Trace
/-- An explicit formula for the norm map: `norm[L/K](x) = x ^ (∑ i < [L:K], (#K) ^ i)`.  -/
FiniteField.algebraMap_norm_eq_pow_sum : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [Finite L] [inst_3 : Algebra K L] (x : L),
  (algebraMap K L) ((Algebra.norm K) x) = x ^ ∑ i ∈ Finset.range (Module.finrank K L), Nat.card K ^ i
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_1 : ∀ (k : ℤ), (Lean.Grind.CommRing.Expr.num k).toPoly = Lean.Grind.CommRing.Poly.num k
-- Mathlib.Analysis.SpecialFunctions.Exp
Complex.comap_exp_cobounded : Filter.comap Complex.exp (Bornology.cobounded ℂ) = Filter.comap Complex.re Filter.atTop
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.mk.sizeOf_spec : ∀ {α : Type u_6} [inst : NonUnitalNonAssocSemiring α] [inst_1 : SizeOf α] (toAddMonoidHom : α →+ α)
  (map_mul_left' : ∀ (a b : α), (↑toAddMonoidHom).toFun (a * b) = a * (↑toAddMonoidHom).toFun b)
  (map_mul_right' : ∀ (a b : α), (↑toAddMonoidHom).toFun (a * b) = (↑toAddMonoidHom).toFun a * b),
  sizeOf { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' } =
    1 + sizeOf toAddMonoidHom
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_update : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R) (x : M →₀ R),
  AddMonoidAlgebra.ofCoeff (x.update m r) = AddMonoidAlgebra.update m r (AddMonoidAlgebra.ofCoeff x)
-- Lean.Parser.Term
Lean.Parser.Term.letId.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.smul_toOuterMeasure : ∀ {α : Type u_1} {R : Type u_6} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal]
  {_m : MeasurableSpace α} (c : R) (μ : MeasureTheory.Measure α), (c • μ).toOuterMeasure = c • μ.toOuterMeasure
-- Init.Data.Vector.Lemmas
Vector.setIfInBound_comm : ∀ {α : Type u_1} {n : ℕ} (a b : α) {i j : ℕ} {xs : Vector α n},
  i ≠ j → (xs.setIfInBounds i a).setIfInBounds j b = (xs.setIfInBounds j b).setIfInBounds i a
-- Qq.Simp
/-- For `pre` procedures, it returns the result without visiting any subexpressions.

For `post` procedures, it returns the result.
 -/
Lean.Meta.Simp.StepQ.done : {u : Lean.Level} → {α : Q(Sort u)} → {e : Q(«$α»)} → Lean.Meta.Simp.ResultQ e → Lean.Meta.Simp.StepQ e
-- Init.Data.Option.Instances
Option.isNone_iff_eq_none : ∀ {α : Type u_1} {o : Option α}, o.isNone = true ↔ o = none
-- Mathlib.GroupTheory.GroupAction.Ring
NonUnitalNonAssocSemiring.toDistribSMul : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → DistribSMul R R
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.LocalGeneratorsData.IsLocallyFreeData.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  {q : M.LocalGeneratorsData},
  autoParam (∀ (i : q.I), CategoryTheory.IsIso (q.generators i).π)
      SheafOfModules.LocalGeneratorsData.IsLocallyFreeData.isIso._autoParam →
    q.IsLocallyFreeData
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.whiskeringLeftFunctor'_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W],
  CategoryTheory.Localization.whiskeringLeftFunctor' L W E =
    (CategoryTheory.Localization.whiskeringLeftFunctor L W E).comp
      (CategoryTheory.inducedFunctor CategoryTheory.ObjectProperty.FullSubcategory.obj)