mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_nonneg : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] {a : A} {y : ℝ}, 0 ≤ a ^ y
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus : ∀ {X : AlgebraicGeometry.Scheme} (self : X.IdealSheafData), self.supportSet = ⋂ U, X.zeroLocus ↑(self.ideal U)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.brecOn.eq : ∀ {motive : Int.Internal.Linear.Poly → Sort u} (t : Int.Internal.Linear.Poly)
  (F_1 : (t : Int.Internal.Linear.Poly) → Int.Internal.Linear.Poly.below t → motive t),
  Int.Internal.Linear.Poly.brecOn t F_1 = F_1 t (Int.Internal.Linear.Poly.brecOn.go t F_1).2
-- Std.Http.Data.Method
Std.Http.instReprMethod.repr : Std.Http.Method → ℕ → Std.Format
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂_fderiv_undef : ∀ (z : ℂ) {τ : ℂ}, τ.im ≤ 0 → jacobiTheta₂_fderiv z τ = 0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_functor_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  {Y X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T} (f : Y ⟶ X),
  ((CategoryTheory.StructuredArrow.mapNatIso i).functor.map f).left = CategoryTheory.CategoryStruct.id Y.left
-- Mathlib.NumberTheory.Divisors
Nat.image_snd_divisorsAntidiagonal : ∀ {n : ℕ}, Finset.image Prod.snd n.divisorsAntidiagonal = n.divisors
-- Mathlib.Topology.Semicontinuity.Basic
Continuous.comp_lowerSemicontinuousOn_antitone : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  Continuous g → LowerSemicontinuousOn f s → Antitone g → UpperSemicontinuousOn (g ∘ f) s
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instSMulNNRat : {R : Type u_1} → [inst : Field R] → [inst_1 : StarRing R] → SMul ℚ≥0 ↥(selfAdjoint R)
-- Init.Data.Array.Basic
Array.findIdx?.loop : {α : Type u} → (α → Bool) → Array α → ℕ → Option ℕ
-- Mathlib.Order.Fin.Basic
/-- `Fin.rev n` as an order-reversing isomorphism.  -/
Fin.revOrderIso : {n : ℕ} → (Fin n)ᵒᵈ ≃o Fin n
-- Lean.Data.DeclarationRange
Lean.instReprDeclarationRange : Repr Lean.DeclarationRange
-- Mathlib.RingTheory.SimpleModule.Basic
/-- **Schur's Lemma** for linear maps between (possibly distinct) simple modules  -/
LinearMap.bijective_or_eq_zero : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSimpleModule R M] [IsSimpleModule R N] (f : M →ₗ[R] N),
  Function.Bijective ⇑f ∨ f = 0
-- Mathlib.RingTheory.MvPowerSeries.Trunc
/-- A coefficient of a product of truncated power series equals the coefficient of the untruncated
product, with the two truncation levels `n₁` and `n₂` allowed to differ.  -/
MvPowerSeries.coeff_trunc'_mul_trunc'_eq_coeff_mul₂ : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (n₁ n₂ : σ →₀ ℕ)
  (f g : MvPowerSeries σ R) {m : σ →₀ ℕ},
  m ≤ n₁ →
    m ≤ n₂ →
      MvPolynomial.coeff m ((MvPowerSeries.trunc' R n₁) f * (MvPowerSeries.trunc' R n₂) g) =
        (MvPowerSeries.coeff m) (f * g)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.closedInterior.eq_1 : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} (s : Affine.Simplex k P n),
  s.closedInterior = Affine.Simplex.setInterior (Set.Icc 0 1) s
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.coe_id : ∀ (X : ProfiniteAddGrp.{u_1}), ⇑(ProfiniteAddGrp.Hom.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Data.Fintype.EquivFin
/-- Embedding of `ℕ` into an infinite type.  -/
Infinite.natEmbedding : (α : Type u_4) → [Infinite α] → ℕ ↪ α
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.dfinsupp_ext_iff : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : Type uN} [Finite ι]
  [inst : Semiring R] [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_2 : AddCommMonoid N]
  [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_4 : Module R N] [inst_5 : (i : ι) → DecidableEq (κ i)]
  {f g : MultilinearMap R (fun i => Π₀ (j : κ i), M i j) N},
  f = g ↔
    ∀ (p : (i : ι) → κ i),
      (f.compLinearMap fun i => DFinsupp.lsingle (p i)) = g.compLinearMap fun i => DFinsupp.lsingle (p i)
-- Mathlib.Algebra.Ring.Defs
/-- Zero is a left absorbing element for multiplication  -/
Semiring.zero_mul : ∀ {α : Type u} [self : Semiring α] (a : α), 0 * a = 0
-- Lean.Meta.Tactic.Intro
/-- Introduce as many binders as possible without unfolding definitions.
 -/
Lean.MVarId.intros : Lean.MVarId → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- ProofWidgets.Data.Html
ProofWidgets.Html.brecOn.eq : ∀ {motive_1 : ProofWidgets.Html → Sort u} {motive_2 : Array ProofWidgets.Html → Sort u}
  {motive_3 : List ProofWidgets.Html → Sort u} (t : ProofWidgets.Html)
  (F_1 : (t : ProofWidgets.Html) → t.below → motive_1 t)
  (F_2 : (t : Array ProofWidgets.Html) → ProofWidgets.Html.below_1 t → motive_2 t)
  (F_3 : (t : List ProofWidgets.Html) → ProofWidgets.Html.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (ProofWidgets.Html.brecOn.go t F_1 F_2 F_3).2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertMany_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {l : List (α × β)} {k k' : α} {v fallback : β},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
      (k, v) ∈ l →
        Std.DTreeMap.Internal.Impl.Const.getD (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k' fallback = v
-- Mathlib.RingTheory.Ideal.Defs
Ideal.coe_mem_inertia : ∀ {α : Type u} [inst : Ring α] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulAction G α] {I : Ideal α} {H : Subgroup G}
  {σ : ↥H}, ↑σ ∈ Ideal.inertia G I ↔ σ ∈ Ideal.inertia (↥H) I
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.List.forIn'_eq_foldlM.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (b : ForInStep β) → ((b : β) → motive (ForInStep.yield b)) → ((b : β) → motive (ForInStep.done b)) → motive b
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Measure.lintegral_condKernel : ∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ]
  {f : β × Ω → ENNReal}, Measurable f → ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω), f x ∂ρ
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.ofFreeGroup_apply : ∀ {X : Type u_5} (x : X), (FreeGroupBasis.ofFreeGroup X) x = FreeGroup.of x
-- Lean.DocString.Types
Lean.Doc.Inline.link.sizeOf_spec : ∀ {i : Type u} [inst : SizeOf i] (content : Array (Lean.Doc.Inline i)) (url : String),
  sizeOf (Lean.Doc.Inline.link content url) = 1 + sizeOf content + sizeOf url
-- Init.Data.Iterators.Consumers.Access
/-- If possible, takes `n` steps with the iterator `it` and
returns the `n`-th emitted value, or `none` if `it` finished
before emitting `n` values.

If the iterator is not productive, this function might run forever in an endless loop of iterator
steps. The variant `it.ensureTermination.atIdxSlow?` is guaranteed to terminate after finitely many
steps.
 -/
Std.Iter.Partial.atIdxSlow? : {α β : Type u_1} → [Std.Iterator α Id β] → ℕ → Std.Iter.Partial β → Option β
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_add_single : ∀ {R : Type u} {σ : Type u_1} {a : R} {e : ℕ} {n : σ} {s : σ →₀ ℕ} [inst : CommSemiring R],
  (MvPolynomial.monomial (s + fun₀ | n => e)) a = (MvPolynomial.monomial s) a * MvPolynomial.X n ^ e
-- Batteries.Control.AlternativeMonad
/-- `orElse` is associative.  -/
LawfulAlternative.orElse_assoc : ∀ {m : Type u_1 → Type u_2} {inst : Alternative m} [self : LawfulAlternative m] {α : Type u_1} (x y z : m α),
  (x <|> y <|> z) = ((x <|> y) <|> z)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.IsLimit.lift_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.IsLimit.lift h f g) s.snd = g
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.I_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] (K : CochainComplex C ℤ) (x x_1 : ℤ),
  (CochainComplex.cm5b.I K).d x x_1 = 0
-- Mathlib.RepresentationTheory.Action
/-- The counit of the linearize functor.  -/
Representation.LinearizeMonoidal.ε : (k : Type u) →
  (G : Type v) →
    [inst : Monoid G] →
      [inst_1 : Semiring k] →
        (Representation.trivial k G k).IntertwiningMap
          (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type w) G)))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.instAdd : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Projective F} → Add W.Point
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.LogConfig.logDir? : Lean.Lsp.LogConfig → Option System.FilePath
-- ImportGraph.Tools.MinImports
/-- Return the names of the modules in which constants used in the current file were defined,
with modules already transitively imported removed.

Note that this will *not* account for tactics and syntax used in the file,
so the results may not suffice as imports.
 -/
Lean.Environment.minimalRequiredModules : Lean.Environment → Array Lean.Name
-- Mathlib.Order.Interval.Finset.Defs
instFiniteSubtypeLeOfLocallyFiniteOrderTop : ∀ {α : Type u_1} [inst : Preorder α] {y : α} [LocallyFiniteOrderTop α], Finite { x // y ≤ x }
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Limits.coequalizer.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f f_1 : X ⟶ Y) (e_f : f = f_1) (g g_1 : X ⟶ Y)
  (e_g : g = g_1) [inst_1 : CategoryTheory.Limits.HasCoequalizer f g],
  CategoryTheory.Limits.coequalizer f g = CategoryTheory.Limits.coequalizer f_1 g_1
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instBot.eq_1 : ∀ {α : Type u_1} [inst : LE α], LowerSet.instBot = { bot := { carrier := ∅, lower' := ⋯ } }
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.kernelOpUnop.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.kernelOpUnop f =
    { hom := (CategoryTheory.Limits.kernel.lift f.op (CategoryTheory.Limits.cokernel.π f).op ⋯).unop,
      inv := CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.kernel.ι f.op).unop ⋯, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_of_subsingleton : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α} [Subsingleton E'], f' =O[l] g'
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get!_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∉ t₁ → (t₁ \ t₂).get! k = default
-- Mathlib.Data.Set.Basic
Set.isEmpty_coe_sort : ∀ {α : Type u} {s : Set α}, IsEmpty ↑s ↔ s = ∅
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.unitsEquivAut_symm_apply : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : ContinuousMul R] (e : R ≃L[R] R),
  ↑((ContinuousLinearEquiv.unitsEquivAut R).symm e) = e 1
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_sub : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : AddGroup α]
  (M N : o → Matrix m n α), Matrix.blockDiagonal (M - N) = Matrix.blockDiagonal M - Matrix.blockDiagonal N
-- Lean.Meta.IndPredBelow
/-- Parameters of the mutual inductive  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.params : Lean.Meta.IndPredBelow.Context✝ → Array Lean.Expr
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Syntax of the semantic token.  -/
Lean.Server.FileWorker.LeanSemanticToken.stx : Lean.Server.FileWorker.LeanSemanticToken → Lean.Syntax
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.eval_xor : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVBinOp.xor.eval = fun x1 x2 => x1 ^^^ x2
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'_add_zero_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A) (X : C),
  (CategoryTheory.shiftFunctorAdd' C a 0 a ⋯).inv.app X =
    (CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C a).obj X)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instAdd : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → Add (DoubleCentralizer 𝕜 A)
-- Init.Data.Iterators.Lemmas.Combinators.Take
Std.Iter.toListRev_take_of_finite : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {n : ℕ} [Std.Iterators.Finite α Id] {it : Std.Iter β},
  (Std.Iter.take n it).toListRev = List.drop (it.toList.length - n) it.toListRev
-- Mathlib.RingTheory.Smooth.IntegralClosure
/-- "Base change preserves integral closure" can be checked Zariski-locally.  -/
TensorProduct.toIntegralClosure_bijective_of_isLocalizationAway : ∀ {R : Type u_1} {S : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] {s : Set S},
  Ideal.span s = ⊤ →
    ∀ (Sᵣ : ↑s → Type u_4) [inst_5 : (r : ↑s) → CommRing (Sᵣ r)] [inst_6 : (r : ↑s) → Algebra S (Sᵣ r)]
      [inst_7 : (r : ↑s) → Algebra R (Sᵣ r)] [∀ (r : ↑s), IsScalarTower R S (Sᵣ r)]
      [∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)],
      (∀ (r : ↑s), Function.Bijective ⇑(TensorProduct.toIntegralClosure R (Sᵣ r) B)) →
        Function.Bijective ⇑(TensorProduct.toIntegralClosure R S B)
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mergeParams : Array Lean.Syntax → Array Lean.Syntax → Array Lean.Syntax
-- Mathlib.Tactic.Translate.Core
/-- Implementation function for `shouldTranslate`.
Returning `none` means that `e` contains no constant that blocks translation.
We cache previous applications of the function, using an expression cache using ptr equality
to avoid visiting the same subexpression many times.

Note that this function is still called many times by `applyReplacementFun`
and we're not remembering the cache between these calls.  -/
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.shouldTranslateUnsafe : Lean.Environment →
  Mathlib.Tactic.Translate.TranslateData → Lean.Expr → Mathlib.Tactic.Translate.ReplacementM (Option Lean.Expr)
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.card_mul_addConst : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G), ↑A.card * A.addConst B = ↑(A + B).card
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Init.Data.Option.Basic
Option.get.congr_simp : ∀ {α : Type u} (o o_1 : Option α) (e_o : o = o_1) (a : o.isSome = true), o.get a = o_1.get ⋯
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
/-- The canonical inclusion from `SimplexCategory` to `AugmentedSimplexCategory`.  -/
AugmentedSimplexCategory.inclusion : CategoryTheory.Functor SimplexCategory AugmentedSimplexCategory
-- Mathlib.Data.Finmap
Finmap.lookup_erase_ne : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {s : Finmap β},
  a ≠ a' → Finmap.lookup a (Finmap.erase a' s) = Finmap.lookup a s
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.instUnique : {α : Type u₁} → [Unique α] → Unique (CategoryTheory.Discrete α)
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.unique_nonDegenerate_simplex : ∀ (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })) {m : ℕ} (f₁ : { len := n } ⟶ { len := m })
  [CategoryTheory.Epi f₁] (y₁ : ↑(X.nonDegenerate m)),
  x = (CategoryTheory.ConcreteCategory.hom (X.map f₁.op)) ↑y₁ →
    ∀ (f₂ : { len := n } ⟶ { len := m }) (y₂ : ↑(X.nonDegenerate m)),
      x = (CategoryTheory.ConcreteCategory.hom (X.map f₂.op)) ↑y₂ → y₁ = y₂
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.foldr.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} (f : (a : α) → β a → δ → δ) (init : δ)
  (as : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.foldr f init as =
    (Std.DHashMap.Internal.AssocList.foldrM (fun x1 x2 x3 => pure (f x1 x2 x3)) init as).run
-- Mathlib.Data.DFinsupp.Defs
/-- A dependent function `Π i, β i` with finite support, with notation `Π₀ i, β i`.

Note that `DFinsupp.support` is the preferred API for accessing the support of the function,
`DFinsupp.support'` is an implementation detail that aids computability; see the implementation
notes in this file for more information.  -/
DFinsupp : {ι : Type u} → (β : ι → Type v) → [(i : ι) → Zero (β i)] → Type (max u v)
-- Mathlib.Data.Nat.Prime.Factorial
Nat.Prime.dvd_factorial : ∀ {n p : ℕ}, Nat.Prime p → (p ∣ n.factorial ↔ p ≤ n)
-- Mathlib.CategoryTheory.Adjunction.Evaluation
/-- See also the file `Mathlib/CategoryTheory/Limits/FunctorCategory/EpiMono.lean`
for a similar result under a `HasPullbacks` assumption.  -/
CategoryTheory.NatTrans.mono_iff_mono_app' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D] {F G : CategoryTheory.Functor C D} (η : F ⟶ G),
  CategoryTheory.Mono η ↔ ∀ (c : C), CategoryTheory.Mono (η.app c)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [inst_2 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [h : CategoryTheory.HasExt D] (X Y : C),
  CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso D (ComplexShape.up ℤ)) ℤ
    ((F.comp (CochainComplex.singleFunctor D 0)).obj X) ((F.comp (CochainComplex.singleFunctor D 0)).obj Y)
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.iff_of_openCover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (𝒰 : Y.OpenCover)
  [inst : ∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)],
  P f ↔ ∀ (i : 𝒰.toPreZeroHypercover.1), Q (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i)
-- Mathlib.Algebra.Order.CauSeq.Basic
/-- Given a Cauchy sequence `f`, create a Cauchy sequence from a sequence `g` with
the same values as `f`.  -/
CauSeq.ofEq : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → (f : CauSeq β abv) → (g : ℕ → β) → (∀ (i : ℕ), ↑f i = g i) → CauSeq β abv
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.IsSymm.adjugate : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] {A : Matrix n n α},
  A.IsSymm → A.adjugate.IsSymm
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.alt.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (ctorName : Lean.Name) (params : Array (Lean.Compiler.LCNF.Param pu))
  (code : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Alt._auto_1),
  sizeOf (Lean.Compiler.LCNF.Alt.alt ctorName params code h) =
    1 + sizeOf ctorName + sizeOf params + sizeOf code + sizeOf h
-- Mathlib.Algebra.Order.Group.DenselyOrdered
exists_lt_pow_of_lt_one : ∀ {M : Type u_2} [inst : LinearOrder M] [DenselyOrdered M] {x : M} [inst_2 : CommGroup M] [IsOrderedCancelMonoid M],
  x < 1 → ∀ (n : ℕ), ∃ y < 1, x < y ^ n
-- Mathlib.Analysis.Asymptotics.Theta
/-- **Alias** of the reverse direction of `Asymptotics.isTheta_norm_left`. -/
Asymptotics.IsTheta.norm_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, f' =Θ[l] g → (fun x => ‖f' x‖) =Θ[l] g
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.ofLower_inj : ∀ {α : Type u_1} {a b : Topology.WithLower α}, Topology.WithLower.ofLower a = Topology.WithLower.ofLower b ↔ a = b
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.isGroupLikeElem_iff_mem_range_of : ∀ {R : Type u_1} {M : Type u_8} [inst : CommRing R] [IsDomain R] [inst_2 : MulOneClass M] {x : MonoidAlgebra R M},
  IsGroupLikeElem R x ↔ x ∈ Set.range ⇑(MonoidAlgebra.of R M)
-- Init.Data.List.Sublist
List.infix_filterMap_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l₁ : List α} {l₂ : List β},
  l₂ <:+: List.filterMap f l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = List.filterMap f l
-- Mathlib.Topology.Maps.Basic
Topology.IsCoinducing.of_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsCoinducing f → (Topology.IsCoinducing (g ∘ f) ↔ Topology.IsCoinducing g)
-- Mathlib.Tactic.CategoryTheory.Coherence.Basic
/-- Transform an equality between 2-morphisms into the equality between their normalizations.  -/
Mathlib.Tactic.BicategoryLike.normalForm : (ρ : Type) →
  [Mathlib.Tactic.BicategoryLike.Context ρ] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
          [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
            [Mathlib.Tactic.BicategoryLike.MkMor₂ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
              [Mathlib.Tactic.BicategoryLike.MonadMor₂ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
                Lean.Name → Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Computability.TuringMachine.Computable
Turing.FinTM2.inhabitedCfg : (tm : Turing.FinTM2) → Inhabited tm.Cfg
-- Mathlib.LinearAlgebra.Matrix.Defs
IsSMulRegular.matrix : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [inst : SMul R S] {k : R},
  IsSMulRegular S k → IsSMulRegular (Matrix m n S) k
-- Init.Data.String.Basic
String.offsetOfPos : String → String.Pos.Raw → ℕ
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.coe_id_continuousOrderHom : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α], ↑(EsakiaHom.id α) = ContinuousOrderHom.id α