mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.FinitelyGenerated
/-- An equivalent expression of `Structure.FG` in terms of `Set.Finite` instead of `Finset`.  -/
FirstOrder.Language.Structure.fg_iff : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M],
  FirstOrder.Language.Structure.FG L M ↔ ∃ S, S.Finite ∧ (FirstOrder.Language.Substructure.closure L).toFun S = ⊤
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.Data.Fintype.Basic
PUnit.fintype : Fintype PUnit.{u_4 + 1}
-- Mathlib.Topology.ContinuousMap.Algebra
AlgHom.compLeftContinuous_apply_apply : ∀ (R : Type u_2) [inst : CommSemiring R] {A : Type u_3} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsTopologicalSemiring A] {A₂ : Type u_4} [inst_5 : TopologicalSpace A₂]
  [inst_6 : Semiring A₂] [inst_7 : Algebra R A₂] [inst_8 : IsTopologicalSemiring A₂] {α : Type u_5}
  [inst_9 : TopologicalSpace α] (g : A →ₐ[R] A₂) (hg : Continuous ⇑g) (f : C(α, A)) (a : α),
  ((AlgHom.compLeftContinuous R g hg) f) a = g (f a)
-- Mathlib.GroupTheory.Finiteness
/-- An additive submonoid of `N` is finitely generated if it is the closure of a
finite subset of `M`.  -/
AddSubmonoid.FG : {M : Type u_1} → [inst : AddMonoid M] → AddSubmonoid M → Prop
-- Mathlib.Order.CompleteLattice.Basic
Prod.supSet.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : SupSet α] [inst_1 : SupSet β],
  Prod.supSet α β = { sSup := fun s => (sSup (Prod.fst '' s), sSup (Prod.snd '' s)) }
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.analyticAt_cgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) → AnalyticAt ℝ (ProbabilityTheory.cgf X μ) v
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_add_compl : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s →
    μ.Integrable f → ∫ᵛ (x : X) in s, f x ∂[B; μ] + ∫ᵛ (x : X) in sᶜ, f x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ]
-- Mathlib.RingTheory.Artinian.Module
isArtinian_iSup : ∀ {R : Type u_1} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup P] [inst_2 : Module R P] {ι : Type u_5}
  [Finite ι] {M : ι → Submodule R P} [∀ (i : ι), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_le_tsub_iff_right : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, c ≤ b → (a - c ≤ b - c ↔ a ≤ b)
-- Mathlib.Data.List.Range
_private.Mathlib.Data.List.Range.0.List.ranges.match_1.eq_1 : ∀ (motive : List ℕ → Sort u_1) (h_1 : Unit → motive []) (h_2 : (a : ℕ) → (l : List ℕ) → motive (a :: l)),
  (match [] with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_1 ()
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquiv_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (Q : Type u_4) [inst_4 : CommSemiring Q] [inst_5 : Algebra R Q]
  [inst_6 : IsLocalization M Q] (a : Q),
  (IsLocalization.algEquiv M S Q).symm a = (IsLocalization.map S (RingHom.id R) ⋯) a
-- Mathlib.Algebra.Module.Submodule.Invariant
/-- **Alias** of the reverse direction of `Module.End.mem_invtSubmodule_iff_mapsTo`.

---

`p` is `f` invariant if and only if `Set.MapsTo f p p`.  -/
Set.Mapsto.mem_invtSubmodule : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p : Submodule R M}, Set.MapsTo ⇑f ↑p ↑p → p ∈ f.invtSubmodule
-- Mathlib.Data.List.Dedup
List.nodup_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.dedup.Nodup
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.NatOffset.const.inj : ∀ {n n_1 : ℕ}, Nat.NatOffset.const✝ n = Nat.NatOffset.const✝ n_1 → n = n_1
-- Mathlib.Order.Lattice
sup_inf_right : ∀ {α : Type u} [inst : DistribLattice α] (a b c : α), a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_zpow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionMonoid α] (s : Finset α) (n : ℤ), ↑(s ^ n) = ↑s ^ n
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `(F ⋙ forget CommGrpCat).sections` is `u`-small, `F` has a limit.  -/
CommGrpCat.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections], CategoryTheory.Limits.HasLimit F
-- Mathlib.Order.Hom.CompleteLattice
map_iSup₂ : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} {κ : ι → Sort u_7} [inst : FunLike F α β]
  [inst_1 : SupSet α] [inst_2 : SupSet β] [sSupHomClass F α β] (f : F) (g : (i : ι) → κ i → α),
  f (⨆ i, ⨆ j, g i j) = ⨆ i, ⨆ j, f (g i j)
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.le_Φ_coeff_generatorIndex_natDegree : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  (RatFunc.Luroth.f✝ E).natDegree ≤ ((RatFunc.Luroth.Φ✝ E).coeff (RatFunc.Luroth.generatorIndex✝ h)).natDegree
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
/-- The bifunctor `tensorBifunctor` on `LocalizedMonoidal L W ε` is induced by
`curriedTensor C`.  -/
CategoryTheory.Localization.Monoidal.tensorBifunctorIso : {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) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      (((CategoryTheory.Functor.whiskeringLeft₂ D).obj
                                  (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)).obj
                              (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)).obj
                          (CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε) ≅
                        (CategoryTheory.Functor.postcompose₂.obj
                              (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)).obj
                          (CategoryTheory.MonoidalCategory.curriedTensor C)
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.cuspFunction_sub : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2}
  [inst_1 : FunLike G UpperHalfPlane ℂ],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b],
        UpperHalfPlane.cuspFunction h (⇑f - ⇑g) = UpperHalfPlane.cuspFunction h ⇑f - UpperHalfPlane.cuspFunction h ⇑g
-- Mathlib.Algebra.Polynomial.Div
Polynomial.divByMonic_one : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), p /ₘ 1 = p
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.isBaseChange_of_isFractionRing : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (R' : Type u_4)
  (S' : Type u_5) [inst_3 : CommRing S'] [FaithfulSMul R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S]
  [inst_6 : Algebra S S'] [IsFractionRing S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R S S']
  [inst_10 : CommRing R'] [inst_11 : Algebra R R'] [IsFractionRing R R'] [inst_13 : Module R' S']
  [inst_14 : IsScalarTower R R' S'], IsBaseChange R' (IsScalarTower.toAlgHom R S S').toLinearMap
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- For any functor `K : J ⥤ Under X`, there is a canonical extension
`WithInitial J ⥤ C`, that sends `star` to `X`.  -/
CategoryTheory.WithInitial.liftFromUnder : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          CategoryTheory.Functor (CategoryTheory.Functor J (CategoryTheory.Under X))
            (CategoryTheory.Functor (CategoryTheory.WithInitial J) C)
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.mulI_orthogonal : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H),
  Sᗮ.mulI = S.mulIᗮ
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.closure_eq_image_sum : ∀ {M : Type u_1} [inst : AddMonoid M] (s : Set M), ↑(AddSubmonoid.closure s) = List.sum '' {l | ∀ x ∈ l, x ∈ s}
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_conjTranspose : ∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R] [inst_3 : StarRing R]
  (M : Matrix m m R), M.conjTranspose.det = star M.det
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.nat_card_ofStabilizer_add_zero_eq : ∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] [Finite α] (a : α),
  Nat.card ↥(SubAddAction.ofStabilizer G a) + 1 = Nat.card α
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.le_traceDual_comm : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] {I J : Submodule B L},
  I ≤ Submodule.traceDual A K J ↔ J ≤ Submodule.traceDual A K I
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralNorm.eq_1 : ∀ (K : Type u_2) [inst : NormedField K] (L : Type u_3) [inst_1 : Field L] [inst_2 : Algebra K L] (y : L),
  spectralNorm K L y = spectralValue (minpoly K y)
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.instCompactSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [CompactSpace M], CompactSpace Mᵃᵒᵖ
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.constAddMonoidHom.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddZeroClass Y],
  LocallyConstant.constAddMonoidHom = { toFun := LocallyConstant.const X, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.one_ne_of : ∀ {α : Type u_1} (a : α), 1 ≠ FreeMonoid.of a
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.weierstrassDiv_zero_left : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (g : PowerSeries A)
  [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A], 0 /ʷ g = 0
-- Mathlib.Algebra.Quaternion
Quaternion.imK_mul : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R),
  (a * b).imK = a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re
-- Batteries.Data.List.Basic
/-- `countBefore a xs n` counts the number of `x` in `xs` before the
`i`th index for which `x == a` is true.

For example:
```
countBefore 1 [5, 1, 3, 2, 4, 0, 1, 4] 6 = 1
```
 -/
List.countBefore : {α : Type u_1} → [BEq α] → α → List α → ℕ → ℕ
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.instMulHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier : (X : TopCat) → (R : TopCommRingCat) → Mul (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.basis_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R},
  (WeierstrassCurve.Affine.CoordinateRing.basis W') 0 = 1
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
CochainComplex.instLinearIntFunctorSingleFunctors : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (R : Type u_1) [inst_3 : Ring R] (n : ℤ)
  [inst_4 : CategoryTheory.Linear R C], CategoryTheory.Functor.Linear R ((CochainComplex.singleFunctors C).functor n)
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the first commutative square of a triangle morphism  -/
CategoryTheory.Pretriangulated.TriangleMorphism.comm₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} (self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂),
  CategoryTheory.CategoryStruct.comp T₁.mor₁ self.hom₂ = CategoryTheory.CategoryStruct.comp self.hom₁ T₂.mor₁
-- Mathlib.ModelTheory.Bundled
/-- The type of nonempty models of a first-order theory.  -/
FirstOrder.Language.Theory.ModelType : {L : FirstOrder.Language} → L.Theory → Type (max (max u v) (w + 1))
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.mk.inj : ∀ {base : Lean.VisibilityMap✝ Lean.Kernel.Environment} {serverBaseExts : Array Lean.EnvExtensionState}
  {checked : Task Lean.Kernel.Environment} {asyncConstsMap : Lean.VisibilityMap✝ Lean.AsyncConsts✝}
  {asyncCtx? : Option Lean.AsyncContext✝} {importRealizationCtx? : Option Lean.RealizationContext✝}
  {localRealizationCtxMap : Lean.NameMap Lean.RealizationContext✝}
  {allRealizations : Task (Lean.NameMap Lean.AsyncConst✝)} {isExporting : Bool}
  {base_1 : Lean.VisibilityMap✝ Lean.Kernel.Environment} {serverBaseExts_1 : Array Lean.EnvExtensionState}
  {checked_1 : Task Lean.Kernel.Environment} {asyncConstsMap_1 : Lean.VisibilityMap✝ Lean.AsyncConsts✝}
  {asyncCtx?_1 : Option Lean.AsyncContext✝} {importRealizationCtx?_1 : Option Lean.RealizationContext✝}
  {localRealizationCtxMap_1 : Lean.NameMap Lean.RealizationContext✝}
  {allRealizations_1 : Task (Lean.NameMap Lean.AsyncConst✝)} {isExporting_1 : Bool},
  { base := base, serverBaseExts := serverBaseExts, checked := checked, asyncConstsMap := asyncConstsMap,
        asyncCtx? := asyncCtx?, importRealizationCtx? := importRealizationCtx?,
        localRealizationCtxMap := localRealizationCtxMap, allRealizations := allRealizations,
        isExporting := isExporting } =
      { base := base_1, serverBaseExts := serverBaseExts_1, checked := checked_1, asyncConstsMap := asyncConstsMap_1,
        asyncCtx? := asyncCtx?_1, importRealizationCtx? := importRealizationCtx?_1,
        localRealizationCtxMap := localRealizationCtxMap_1, allRealizations := allRealizations_1,
        isExporting := isExporting_1 } →
    base = base_1 ∧
      serverBaseExts = serverBaseExts_1 ∧
        checked = checked_1 ∧
          asyncConstsMap = asyncConstsMap_1 ∧
            asyncCtx? = asyncCtx?_1 ∧
              importRealizationCtx? = importRealizationCtx?_1 ∧
                localRealizationCtxMap = localRealizationCtxMap_1 ∧
                  allRealizations = allRealizations_1 ∧ isExporting = isExporting_1
-- Lean.Environment
Lean.instInhabitedAsyncConstantInfo.default : Lean.AsyncConstantInfo
-- Init.Data.UInt.Bitwise
UInt64.ofBitVec_shiftLeft_mod : ∀ (a : BitVec 64) (b : ℕ), { toBitVec := a <<< (b % 64) } = { toBitVec := a } <<< UInt64.ofNat b
-- Init.Data.UInt.Bitwise
UInt32.not_and_self : ∀ {a : UInt32}, ~~~a &&& a = 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
CFC.conjSqrt.congr_simp : ∀ {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] [inst_8 : SeparatelyContinuousMul A] (c c_1 : A),
  c = c_1 → CFC.conjSqrt c = CFC.conjSqrt c_1
-- Mathlib.CategoryTheory.Limits.EpiMono
CategoryTheory.epi_iff_inl_eq_inr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : X ⟶ Y}
  {c : CategoryTheory.Limits.PushoutCocone f f} (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.Epi f ↔ c.inl = c.inr
-- Mathlib.Geometry.Manifold.ChartedSpace
mem_chart_source : ∀ (H : Type u_5) {M : Type u_6} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (x : M), x ∈ (chartAt H x).source
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {retraction : Y ⟶ X}
  {id :
    autoParam (CategoryTheory.CategoryStruct.comp f retraction = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.SplitMono.id._autoParam}
  {retraction_1 : Y ⟶ X}
  {id_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f retraction_1 = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.SplitMono.id._autoParam},
  { retraction := retraction, id := id } = { retraction := retraction_1, id := id_1 } → retraction = retraction_1
-- Init.Prelude
Lean.instHashableName : Hashable Lean.Name
-- Mathlib.Computability.Primrec.Basic
Primrec.ofNat_iff : ∀ {α : Type u_4} {β : Type u_5} [inst : Denumerable α] [inst_1 : Primcodable β] {f : α → β},
  Primrec f ↔ Primrec fun n => f (Denumerable.ofNat α n)
-- Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
/-- If the coproduct `Y ⨿ Z` and the coequalizer of `f ≫ ι₁` and `g ≫ ι₂` exist, then the
pushout of `f` and `g` exists: It is given by composing the inclusions with the coequalizer.  -/
CategoryTheory.Limits.hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair : ∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair Y Z)]
  [CategoryTheory.Limits.HasColimit
      (CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.coprod.inl)
        (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inr))],
  CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)
-- Init.Data.Array.Lemmas
Array.back_replicate : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (w : 0 < n), (Array.replicate n xs).back ⋯ = xs
-- Batteries.Data.String.Lemmas
String.foldrAux_of_valid : ∀ {α : Type u_1} (f : Char → α → α) (l m r : List Char) (a : α),
  String.Legacy.foldrAux f a (String.ofList (l ++ m ++ r)) { byteIdx := String.utf8Len l + String.utf8Len m }
      { byteIdx := String.utf8Len l } =
    List.foldr f a m
-- Init.Data.Nat.Lemmas
Nat.add_pos_left : ∀ {m : ℕ}, 0 < m → ∀ (n : ℕ), 0 < m + n
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instZero : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} → [GradedRing 𝒜] → (x : Submonoid A) → Zero (HomogeneousLocalization 𝒜 x)
-- Mathlib.Algebra.Ring.GeomSum
Commute.geom_sum₂_comm : ∀ {R : Type u_1} [inst : Semiring R] {x y : R} (n : ℕ),
  Commute x y → ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ Finset.range n, y ^ i * x ^ (n - 1 - i)
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat}
  {α : (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.comp X.presheaf ⟶ F}
  (H : CategoryTheory.NatTrans.Coequifibered α),
  AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData H =
    { functor := F.rightOp.comp AlgebraicGeometry.Scheme.Spec,
      natTrans :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.rightOp α) AlgebraicGeometry.Scheme.Spec)
          (AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec X).inv,
      equifibered := ⋯ }
-- Lean.Meta.Match.MatcherApp.Transform
/-- Arguments for `instantiateLambda` on the original alternative (see example above).
May include non-fvar values like `Unit.unit` for thunked alternatives.  -/
Lean.Meta.MatcherApp.TransformAltFVars.args : Lean.Meta.MatcherApp.TransformAltFVars → Array Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.conj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.GrpObj G],
  CategoryTheory.GrpObj.conj G =
    CategoryTheory.SemiCartesianMonoidalCategory.fst G G * CategoryTheory.SemiCartesianMonoidalCategory.snd G G *
      (CategoryTheory.SemiCartesianMonoidalCategory.fst G G)⁻¹
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.universallyInjective_isStableUnderComposition : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.UniversallyInjective
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.subsemigroup_eq_addSubgroup : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  {s : UpperSet (FiniteArchimedeanClass M)},
  ↑(ArchimedeanClass.subsemigroup (FiniteArchimedeanClass.toUpperSetAddArchimedeanClass s)) =
    ↑(FiniteArchimedeanClass.addSubgroup s)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.isLocalizationMap_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {N : Type u_2} [inst_1 : AddCommMonoid N] (S : AddSubmonoid M) (f : M → N),
  S.IsLocalizationMap f ↔
    (∀ (y : ↥S), IsAddUnit (f ↑y)) ∧
      (∀ (z : N), ∃ x, z + f ↑x.2 = f x.1) ∧ ∀ {x y : M}, f x = f y → ∃ c, ↑c + x = ↑c + y
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.instIsOpenImmersionAppOverSchemeOpensDiagramι : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (i : I)
  (U : (D.obj i).Opens) (j : CategoryTheory.Over i),
  AlgebraicGeometry.IsOpenImmersion ((AlgebraicGeometry.opensDiagramι D i U).app j)
-- Init.Data.SInt.Lemmas
Int16.le_of_lt : ∀ {a b : Int16}, a < b → a ≤ b
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.mk.sizeOf_spec : ∀ (p : Int.Internal.Linear.Poly) (h : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof),
  sizeOf { p := p, h := h } = 1 + sizeOf p + sizeOf h
-- Lean.LocalContext
Lean.LocalContext.get! : Lean.LocalContext → Lean.FVarId → Lean.LocalDecl
-- Init.Data.Int.Lemmas
Int.mul_eq_zero : ∀ {a b : ℤ}, a * b = 0 ↔ a = 0 ∨ b = 0
-- Init.Data.Range.Polymorphic.UInt
UInt8.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite UInt8
-- Mathlib.Analysis.Complex.Schwarz
/-- **Alias** of `Complex.dist_le_dist_of_mapsTo_ball`.

---

The **Schwarz Lemma**. Let `f : E → F` be a complex analytic function
on an open ball with center `c`.
If `f` sends this ball to a closed ball with center `f c` and the same radius,
then for any `z` in the former ball we have `dist (f z) (f c) ≤ dist z c`.
 -/
Complex.dist_le_dist_of_mapsTo_ball_self : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {R : ℝ} {f : E → F} {c z : E},
  DifferentiableOn ℂ f (Metric.ball c R) →
    Set.MapsTo f (Metric.ball c R) (Metric.closedBall (f c) R) → z ∈ Metric.ball c R → dist (f z) (f c) ≤ dist z c
-- Mathlib.Order.Interval.Finset.Basic
Finset.filter_ge_eq_Iic : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] {a : α} [inst_2 : Fintype α]
  [inst_3 : DecidablePred fun x => x ≤ a], {x | x ≤ a} = Finset.Iic a
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.CofibrantObject C), HomotopicalAlgebra.Cofibration X.iBifibrantResolutionObj.hom