mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.useFunCC' : Lean.Meta.Grind.ENodeMap → Lean.Expr → Bool
-- Mathlib.Data.List.Dedup
/-- Note that the weaker `List.Subset.dedup_append_left` is proved later.  -/
List.Subset.dedup_append_right : ∀ {α : Type u_1} [inst : DecidableEq α] {xs ys : List α}, xs ⊆ ys → (xs ++ ys).dedup = ys.dedup
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.singleton : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} [T1Space E] {y : E}, DifferentiableWithinAt 𝕜 f {x} y
-- Mathlib.MeasureTheory.Group.FoelnerFilter
isAddFoelner_iff : ∀ (G : Type u_4) {X : Type u_5} [inst : MeasurableSpace X] (μ : MeasureTheory.Measure X) [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_6} (l : Filter ι) (F : ι → Set X),
  IsAddFoelner G μ l F ↔
    (∀ᶠ (i : ι) in l, MeasurableSet (F i)) ∧
      (∀ᶠ (i : ι) in l, μ (F i) ≠ 0) ∧
        (∀ᶠ (i : ι) in l, μ (F i) ≠ ⊤) ∧
          ∀ (g : G), Filter.Tendsto (fun i => μ (symmDiff (g +ᵥ F i) (F i)) / μ (F i)) l (nhds 0)
-- Mathlib.Order.Filter.Cofinite
Nat.eventually_pos : ∀ᶠ (k : ℕ) in Filter.atTop, 0 < k
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.Term.listDecode.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_2} (motive : List (α ⊕ (i : ℕ) × L.Functions i) → Sort u_4)
  (h_1 : Unit → motive []) (h_2 : (a : α) → (l : List (α ⊕ (i : ℕ) × L.Functions i)) → motive (Sum.inl a :: l))
  (h_3 : (n : ℕ) → (f : L.Functions n) → (l : List (α ⊕ (i : ℕ) × L.Functions i)) → motive (Sum.inr ⟨n, f⟩ :: l)),
  (match [] with
    | [] => h_1 ()
    | Sum.inl a :: l => h_2 a l
    | Sum.inr ⟨n, f⟩ :: l => h_3 n f l) =
    h_1 ()
-- Lean.Server.Rpc.RequestHandling
_private.Lean.Server.Rpc.RequestHandling.0.Lean.Server.RpcProcedure.mk.sizeOf_spec : ∀ (wrapper : UInt64 → Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Json)),
  sizeOf { wrapper := wrapper } = 1
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersion.instNormedSpaceComplement : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {H : Type u_7} →
      {G : Type u_9} →
        {E : Type u} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup E''] →
                  [inst_4 : NormedSpace 𝕜 E''] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              {N : Type u_13} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} → (h : Manifold.IsSubmersion I J n f) → NormedSpace 𝕜 h.complement
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.cof_omega_add_one : ∀ (o : Ordinal.{u_1}), (Ordinal.omega (o + 1)).cof = Cardinal.aleph (o + 1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_minKey?_eq_not_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.minKey?.isSome = !t.isEmpty
-- Mathlib.FieldTheory.Finite.Basic
/-- The sum of `x ^ i` as `x` ranges over a finite field of cardinality `q`
is equal to `0` if `i < q - 1`.  -/
FiniteField.sum_pow_lt_card_sub_one : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K], ∀ i < Fintype.card K - 1, ∑ x, x ^ i = 0
-- Mathlib.GroupTheory.Congruence.Basic
/-- The submonoid of `M × M` defined by a congruence relation on a monoid `M`.  -/
Con.submonoid : {M : Type u_1} → [inst : MulOneClass M] → Con M → Submonoid (M × M)
-- Mathlib.Combinatorics.SetFamily.HarrisKleitman
/-- **Harris-Kleitman inequality**: Any two lower sets of finsets correlate.  -/
IsLowerSet.le_card_inter_finset : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 ℬ : Finset (Finset α)} [inst_1 : Fintype α],
  IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → 𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card
-- Mathlib.Topology.NhdsSet
mem_nhdsSet_iff_forall : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, s ∈ nhdsSet t ↔ ∀ x ∈ t, s ∈ nhds x
-- Mathlib.LinearAlgebra.Goursat
Submodule.goursatFst_prod_goursatSnd_le : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (L : Submodule R (M × N)), L.goursatFst.prod L.goursatSnd ≤ L
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits of shape `Jᵒᵖ`, then `F : C ⥤ D` reflects limits
of shape `J`.  -/
CategoryTheory.Limits.reflectsLimitsOfShape_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.ReflectsColimitsOfShape Jᵒᵖ F.op], CategoryTheory.Limits.ReflectsLimitsOfShape J F
-- Mathlib.Data.Seq.Computation
Computation.get_bind : ∀ {α : Type u} {β : Type v} (s : Computation α) (f : α → Computation β) [inst : s.Terminates]
  [inst_1 : (f s.get).Terminates], (s.bind f).get = (f s.get).get
-- Mathlib.Computability.NFA
NFA.reverse_step : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (s : σ) (a : α), M.reverse.step s a = {s' | s ∈ M.step s' a}
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
LinearMap.BilinForm.tmul.congr_simp : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Algebra R A] [inst_5 : Module R M₁]
  [inst_6 : Module A M₁] [inst_7 : SMulCommClass R A M₁] [inst_8 : IsScalarTower R A M₁] [inst_9 : Module R M₂]
  (B₁ B₁_1 : LinearMap.BilinForm A M₁),
  B₁ = B₁_1 → ∀ (B₂ B₂_1 : LinearMap.BilinMap R M₂ R), B₂ = B₂_1 → B₁.tmul B₂ = B₁_1.tmul B₂_1
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.instIsScalarTower_valuationSubring : ∀ {K : outParam (Type u_5)} {L : outParam (Type u_6)} {Γ₀ : outParam (Type u_7)} [inst : Field K] [inst_1 : Field L]
  [inst_2 : Algebra K L] [inst_3 : LinearOrderedCommGroupWithZero Γ₀] (vK : Valuation K Γ₀),
  IsScalarTower (↥vK.valuationSubring) K L
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The underlying function  -/
GroupExtension.Section.toFun : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] → [inst_1 : Group E] → [inst_2 : Group G] → {S : GroupExtension N E G} → S.Section → G → E
-- Init.Data.Iterators.Basic
Std.Iterators.instProductiveOfFinte : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m],
  Std.Iterators.Productive α m
-- Mathlib.Geometry.Euclidean.Projection
Affine.Simplex.orthogonalProjectionSpan_map : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {V₂ : Type u_4} {P₂ : Type u_5} [inst_3 : NormedAddCommGroup V₂]
  [inst_4 : InnerProductSpace 𝕜 V₂] [inst_5 : MetricSpace P] [inst_6 : NormedAddTorsor V P] [inst_7 : MetricSpace P₂]
  [inst_8 : NormedAddTorsor V₂ P₂] {n : ℕ} (s : Affine.Simplex 𝕜 P n) (f : P →ᵃⁱ[𝕜] P₂) (p : P),
  ↑((s.map f.toAffineMap ⋯).orthogonalProjectionSpan (f p)) = f ↑(s.orthogonalProjectionSpan p)
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.sub : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Sub Y] ⦃f g : X → Y⦄,
  IsLocallyConstant f → IsLocallyConstant g → IsLocallyConstant (f - g)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_insertMany_list_le : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)}, (m.insertMany l).size ≤ m.size + l.length
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- A `E₂`-cohomological spectral sequence has differentials given by the
vector `(r, 1 - r)` on the `r`th page for `2 ≤ r`.  -/
CategoryTheory.E₂CohomologicalSpectralSequence : (C : Type u_1) → [inst : CategoryTheory.Category.{u_3, u_1} C] → [CategoryTheory.Abelian C] → Type (max u_1 u_3)
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
/-- The inclusion of the kernel.  -/
CategoryTheory.Triangulated.AbelianSubcategory.ιK : {C : Type u_1} →
  {A : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.HasShift C ℤ] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} A] →
          {ι : CategoryTheory.Functor A C} →
            {X₁ : A} →
              {X₃ : C} →
                (X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)) →
                  {K : A} → ((CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃) → [ι.Full] → K ⟶ X₁
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_toReal : ∀ (θ : Real.Angle), Real.cos θ.toReal = θ.cos
-- Mathlib.Algebra.Lie.Prod
LieHom.coe_snd : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], ⇑(LieHom.snd R L₁ L₂) = Prod.snd
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal : ∀ {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] (a : { p // Disjoint ↑M ↑p.asIdeal }),
  ↑((RelIso.symm (IsLocalization.primeSpectrumOrderIso M S)) a).asIdeal =
    ⋂ s, ⋂ (_ : ↑(↑a).asIdeal ⊆ ⇑(algebraMap R S) ⁻¹' ↑s), ↑s
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.isoOfEqMk_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (X : CategoryTheory.Subobject B) (f : A ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (h : X = CategoryTheory.Subobject.mk f), (X.isoOfEqMk f h).hom = X.ofLEMk f ⋯
-- Init.Data.String.Basic
String.Slice.Pos.offset_ofSlice : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos},
  (String.Slice.Pos.ofSlice pos).offset = pos.offset.offsetBy p₀.offset
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instField : {R : Type u_1} → [inst : Field R] → [inst_1 : StarRing R] → Field ↥(selfAdjoint R)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- `spectralNorm K L (-y) = spectralNorm K L y` .  -/
spectralNorm_neg : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] [IsUltrametricDist K]
  {y : L}, IsAlgebraic K y → spectralNorm K L (-y) = spectralNorm K L y
-- Mathlib.LinearAlgebra.Span.Defs
Disjoint.of_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s t : Set M},
  Disjoint (Submodule.span R s) (Submodule.span R t) → Disjoint (s \ {0}) t
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.precomp₂_map_left : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {F₀ : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  {F₁ : CategoryTheory.Functor D H} (L' : CategoryTheory.Functor D D') (α : F₀ ⟶ L.comp F₁) {X Y : L'.LeftExtension F₁}
  (f : X ⟶ Y),
  ((CategoryTheory.Functor.LeftExtension.precomp₂ L' α).map f).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.instEpiOfIsThin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [Quiver.IsThin C] (f : X ⟶ Y), CategoryTheory.Epi f
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalNormedRing.toMetricSpace : {α : Type u_5} → [self : NonUnitalNormedRing α] → MetricSpace α
-- Mathlib.Tactic.Linarith.Preprocessing
/-- The default list of preprocessors, in the order they should typically run.
 -/
Mathlib.Tactic.Linarith.defaultPreprocessors : List Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.exists_edist_eq_ediam_of_ne_top : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α], G.ediam ≠ ⊤ → ∃ u v, G.edist u v = G.ediam
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
/-- A cone for a functor `F : J ⥤ HomologicalComplex C c` which is given in degree `n` by
the limit `F ⋙ eval C c n`.  -/
HomologicalComplex.coneOfHasLimitEval : {C : Type u_1} →
  {ι : Type u_2} →
    {J : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_3} J] →
          {c : ComplexShape ι} →
            [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (F : CategoryTheory.Functor J (HomologicalComplex C c)) →
                [∀ (n : ι), CategoryTheory.Limits.HasLimit (F.comp (HomologicalComplex.eval C c n))] →
                  CategoryTheory.Limits.Cone F
-- Mathlib.MeasureTheory.Measure.Count
/-- Counting measure on any measurable space.  -/
MeasureTheory.Measure.count : {α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.Measure α
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.lift_toCoprod_eq_one : ∀ {α : Type u_1} {β : Type u_2} (rels₁ : Set (FreeGroup α)) (rels₂ : Set (FreeGroup β)),
  ∀ r ∈ ⇑(FreeGroup.map Sum.inl) '' rels₁ ∪ ⇑(FreeGroup.map Sum.inr) '' rels₂,
    (FreeGroup.lift (PresentedGroup.toCoprod rels₁ rels₂)) r = 1
-- Mathlib.RingTheory.WittVector.Complete
WittVector.quotientPEquiv_mk : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] [inst_2 : PerfectRing k p]
  (x : WittVector p k),
  WittVector.quotientPEquiv (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {↑p}))) x) = WittVector.constantCoeff x
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.instBot : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → {A : Set M} → {α : Type u₁} → Bot (L.DefinableSet A α)
-- Mathlib.Condensed.Solid
CondensedMod.IsSolid.mk : ∀ {R : Type (u + 1)} [inst : Ring R] {A : CondensedMod R},
  (∀ (X : Profinite),
      CategoryTheory.IsIso ((CategoryTheory.yoneda.obj A).map ((Condensed.profiniteSolidification R).app X).op)) →
    CondensedMod.IsSolid R A
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- Let `R` be a semiring, let `A` be an `AddZeroClass`, let `T` be an `OrderTop`,
and let `D : A → T` be a "degree" function.
For an element `f : R[A]`, the element `infDegree f : T` is the infimum of all the elements in the
support of `f`, or `⊤` if `f` is zero.
Often, the Type `T` is `WithTop A`,
If, further, `A` has a linear order, then this notion coincides with the usual one,
using the minimum of the exponents.  -/
AddMonoidAlgebra.infDegree : {R : Type u_1} →
  {A : Type u_3} →
    {T : Type u_4} →
      [inst : Semiring R] → [inst_1 : SemilatticeInf T] → [OrderTop T] → (A → T) → AddMonoidAlgebra R A → T
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_apply_pi : ∀ {ι : Type u_2} {Ω : Type u_3} [inst : Fintype ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ},
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) →
    ∀ (x y : EuclideanSpace ℝ ι),
      ((ProbabilityTheory.covarianceBilin (MeasureTheory.Measure.map (fun ω => WithLp.toLp 2 fun x => X x ω) μ)) x) y =
        ∑ i, ∑ j, x.ofLp i * y.ofLp j * ProbabilityTheory.covariance (X i) (X j) μ
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.mk.congr_simp : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (decls : Array (Std.Sat.AIG.Decl α))
  (cache cache_1 : Std.Sat.AIG.Cache α decls),
  cache = cache_1 →
    ∀ (hdag : Std.Sat.AIG.IsDAG α decls) (hzero : 0 < decls.size) (hconst : decls[0] = Std.Sat.AIG.Decl.false),
      { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst } =
        { decls := decls, cache := cache_1, hdag := hdag, hzero := hzero, hconst := hconst }
-- Mathlib.SetTheory.Lists
/-- Converts a `List` of ZFA lists to a ZFA list.  -/
Lists.ofList : {α : Type u_1} → List (Lists α) → Lists α
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.multivariateGaussian.eq_1 : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (μ : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ),
  ProbabilityTheory.multivariateGaussian μ S =
    MeasureTheory.Measure.map (fun x => μ + (Matrix.toEuclideanCLM (CFC.sqrt S)) x)
      (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι))
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
AlgebraicGeometry.Scheme.Hom.finrank_comp_left_of_isIso : ∀ {X S Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ S) [CategoryTheory.IsIso f] [AlgebraicGeometry.Flat g]
  [AlgebraicGeometry.IsFinite g],
  AlgebraicGeometry.Scheme.Hom.finrank (CategoryTheory.CategoryStruct.comp f g) = AlgebraicGeometry.Scheme.Hom.finrank g
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalAlgEquivClass.toMulActionSemiHomClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : Add A}
  {inst_1 : Mul A} {inst_2 : SMul R A} {inst_3 : Add B} {inst_4 : Mul B} {inst_5 : SMul R B} {inst_6 : EquivLike F A B}
  [self : NonUnitalAlgEquivClass F R A B], MulActionSemiHomClass F id A B
-- Lean.ToExpr
Lean.instToExprUSize : Lean.ToExpr USize
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.mem_toList_iff_mem : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {a : α}, a ∈ r.toList ↔ a ∈ r
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- `c` is a pullback cone for `p₁` and `p₂`  -/
CategoryTheory.TransitiveRelation.c : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} → {p₁ p₂ : R ⟶ X} → CategoryTheory.TransitiveRelation p₁ p₂ → CategoryTheory.Limits.PullbackCone p₂ p₁
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxEntry?.match_1.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l_1 r : Std.DTreeMap.Internal.Impl α β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_2 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1))),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1) =>
      h_3 size k v l r size_2 k_2 v_2 l_2 r_1 h) =
    h_3 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯
-- Mathlib.MeasureTheory.MeasurableSpace.Card
/-- If a sigma-algebra is generated by a set of sets `s`, then the sigma
algebra has cardinality at most `max #s 2 ^ ℵ₀`.  -/
MeasurableSpace.cardinal_measurableSet_le : ∀ {α : Type u} (s : Set (Set α)), Cardinal.mk ↑{t | MeasurableSet t} ≤ max (Cardinal.mk ↑s) 2 ^ Cardinal.aleph0
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.ControlInfo.mk : Bool → Bool → Bool → ℕ → Bool → Lean.NameSet → Lean.Elab.Do.ControlInfo
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ball_mem_nhdsWithin : ∀ {α : Type ua} [inst : UniformSpace α] {x : α} {S : Set α} ⦃V : SetRel α α⦄,
  x ∈ S → V ∈ uniformity α ⊓ Filter.principal (S ×ˢ S) → UniformSpace.ball x V ∈ nhdsWithin x S
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_image_embedding_lift : ∀ {α : Type u} {β : Type v} (f : α ↪ β) (s : Set α),
  Cardinal.lift.{u, v} (Cardinal.mk ↑(⇑f '' s)) = Cardinal.lift.{v, u} (Cardinal.mk ↑s)
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Certify `-a.subject` from a certificate for `a`.  -/
Mathlib.Tactic.Determinant.certNeg : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      Mathlib.Tactic.Determinant.Cert rα → Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.Algebra.Category.Grp.Adjunctions
/-- The abelianization functor `Group ⥤ CommGroup` sending a group `G` to its abelianization `Gᵃᵇ`.
 -/
GrpCat.abelianize : CategoryTheory.Functor GrpCat CommGrpCat
-- Mathlib.Order.Partition.Basic
Partition.existsUnique_of_mem_le : ∀ {α : Type u_1} {s x : α} [inst : CompleteLattice α] {P Q : Partition s}, P ≤ Q → x ∈ P → ∃! y, y ∈ Q ∧ x ≤ y
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.Nil.eq_copy_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.Nil), p = SimpleGraph.Walk.nil.copy ⋯ ⋯
-- Init.Core
/-- You should not use this function  -/
NonScalar.val : NonScalar → ℕ
-- Mathlib.Topology.Algebra.Indicator
ContinuousOn.continuousAt_mulIndicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  [inst_2 : One β], ContinuousOn f (interior s) → ∀ {x : α}, x ∉ frontier s → ContinuousAt (s.mulIndicator f) x
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getEntry? : {α : Type u} → {β : α → Type v} → [BEq α] → α → Std.DHashMap.Internal.AssocList α β → Option ((a : α) × β a)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- A function that modifies the level of a Dirichlet character to some multiple
of its original level.  -/
DirichletCharacter.changeLevel : {R : Type u_1} → [inst : CommMonoidWithZero R] → {n m : ℕ} → n ∣ m → DirichletCharacter R n →* DirichletCharacter R m
-- Mathlib.Data.Int.Cast.Lemmas
/-- `coe : ℤ → α` as a `RingHom`.  -/
Int.castRingHom : (α : Type u_3) → [inst : NonAssocRing α] → ℤ →+* α
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.opEquiv_apply : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G), Subgroup.opEquiv H = H.op
-- Std.Do.WP.SimpLemmas
Std.Do.WP.tryCatch_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {x : OptionT m α} {h : PUnit.{u + 1} → OptionT m α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps],
  (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q =
    (Std.Do.wp x).apply (Q.1, fun e => (Std.Do.wp (h e)).apply Q, Q.2.2)
-- Batteries.Data.MLList.Basic
/-- Take the product of two monadic lazy lists.  -/
MLList.zip : {m : Type u → Type u} → {α β : Type u} → [Monad m] → MLList m α → MLList m β → MLList m (α × β)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.of'_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (a : M), AddMonoidAlgebra.of' R M a = AddMonoidAlgebra.single a 1