mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.leadingCoeff_expand : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ} {f : Polynomial R},
  0 < p → ((Polynomial.expand R p) f).leadingCoeff = f.leadingCoeff
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.unit_pullbackComp_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ChosenPullbacksAlong g]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)]
  {Z_1 : CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over X)}
  (h :
    (CategoryTheory.Over.map (CategoryTheory.CategoryStruct.comp f g)).comp
        ((CategoryTheory.ChosenPullbacksAlong.pullback g).comp (CategoryTheory.ChosenPullbacksAlong.pullback f)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.comp f g)).unit
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Over.map (CategoryTheory.CategoryStruct.comp f g)).whiskerLeft
          (CategoryTheory.ChosenPullbacksAlong.pullbackComp f g).hom)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.comp f g)).unit h
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.IsLocalizedModule.localized₀FrameHom_apply : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f] (M' : Submodule R M),
  (Submodule.localized₀FrameHom p f) M' = Submodule.localized₀ p f M'
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.id_app : ∀ (J : Type u_1) [inst : LinearOrder J] (x : CategoryTheory.SimplicialThickening J) (x_1 : SimplexCategoryᵒᵖ),
  (CategoryTheory.EnrichedCategory.id x).app x_1 =
    TypeCat.ofHom fun x_2 =>
      (CategoryTheory.Functor.const (Fin ((Opposite.unop x_1).len + 1))).obj (CategoryTheory.CategoryStruct.id x)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.coprodSpec_inr_assoc : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (CommRingCat.of (R × S)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.coprodSpec R S) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.snd R S))) h
-- Mathlib.Data.List.Induction
List.reverseRec.eq_2 : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive [])
  (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) (a : α) (l : List α),
  List.reverseRec nil append_singleton (a :: l) =
    ⋯ ▸ append_singleton (a :: l).dropLast ((a :: l).getLast ⋯) (List.reverseRec nil append_singleton (a :: l).dropLast)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- Characterization of differentiable functions into a vector bundle in terms
of any trivialization. Version at a point.  -/
Bundle.Trivialization.mdifferentiableAt_section_iff : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB)
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle 1 F E IB] (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e]
  (s : (b : B) → E b) {b₀ : B}, b₀ ∈ e.baseSet → (MDiffAt (T% s) b₀ ↔ (MDiffAt fun x => (↑e ⟨x, s x⟩).2) b₀)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.coe_edges_toFinset : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} (p : G.Walk u v), ↑p.edges.toFinset = p.edgeSet
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- **Alias** of `FunLike.coe_zero`. -/
ContDiffMapSupportedIn.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.Functor.KanExtension.Adjunction
/-- The left Kan extension functor `(C ⥤ H) ⥤ (D ⥤ H)` along a functor `C ⥤ D`.  -/
CategoryTheory.Functor.lan : {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) →
          {H : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] →
                CategoryTheory.Functor (CategoryTheory.Functor C H) (CategoryTheory.Functor D H)
-- Mathlib.Algebra.Colimit.Module
/-- The direct limit of a directed system is the abelian groups glued together along the maps.  -/
AddCommGroup.DirectLimit : {ι : Type u_2} →
  [inst : Preorder ι] →
    (G : ι → Type u_3) →
      [inst_1 : (i : ι) → AddCommMonoid (G i)] → [DecidableEq ι] → ((i j : ι) → i ≤ j → G i →+ G j) → Type (max u_3 u_2)
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.coordinate_eval_7 : ∀ {a0 a1 a2 a3 a4 a5 a6 a7 : ℤ} {t : List ℤ},
  (Lean.Omega.LinearCombo.coordinate 7).eval
      (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: t)) =
    a7
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
EisensteinSeries.D2.eq_1 : ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane),
  EisensteinSeries.D2 γ z =
    2 * ↑Real.pi * Complex.I * ↑(↑γ 1 0) /
      UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
Std.IterM.toList_append : ∀ {α₁ α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m] {it₁ : Std.IterM m β}
  {it₂ : Std.IterM m β},
  (it₁.append it₂).toList = do
    let l₁ ← it₁.toList
    let l₂ ← it₂.toList
    pure (l₁ ++ l₂)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.EMatchTheorems.eraseDecl : Lean.Meta.Grind.EMatchTheorems → Lean.Name → Lean.MetaM Lean.Meta.Grind.EMatchTheorems
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.ext : ∀ {n : ℕ} {x y : n.Partition}, x.parts = y.parts → x = y
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The index set which appears in the definition of split simplicial objects.  -/
CategoryTheory.SimplicialObject.Splitting.IndexSet : SimplexCategoryᵒᵖ → Type
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Subtype.preimage_closedBall : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ℝ),
  Subtype.val ⁻¹' Metric.closedBall (↑a) r = Metric.closedBall a r
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Filter.IsMeasurablyGenerated.mk : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : Filter α},
  (∀ ⦃s : Set α⦄, s ∈ f → ∃ t ∈ f, MeasurableSet t ∧ t ⊆ s) → f.IsMeasurablyGenerated
-- Init.Data.SInt.Lemmas
Int8.mod_self : ∀ {a : Int8}, a % a = 0
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.mk : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String}, s = t₁ ++ t₂ → p.offset = t₁.rawEndPos → p.Splits t₁ t₂
-- Init.Data.SInt.Lemmas
Int8.toInt_toInt64 : ∀ (x : Int8), x.toInt64.toInt = x.toInt
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.coweightHom_op : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (g : P.Aut),
  MulOpposite.unop ((RootPairing.Equiv.coweightHom P) g) = RootPairing.Equiv.coweightEquiv P P g
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNonUnitalSemiringQuotient : {R : Type u_1} → [inst : NonUnitalSemiring R] → (c : RingCon R) → NonUnitalSemiring c.Quotient
-- Std.Data.ExtDHashMap.Basic
/-- Creates a new empty hash map. The optional parameter `capacity` can be supplied to presize the
map so that it can hold the given number of mappings without reallocating. It is also possible to
use the empty collection notations `∅` and `{}` to create an empty hash map with the default
capacity.
 -/
Std.ExtDHashMap.emptyWithCapacity : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → optParam ℕ 8 → Std.ExtDHashMap α β
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- The range of a finite additive monoid under an additive monoid homomorphism is
finite.

Note: this instance can form a diamond with `Subtype.fintype` or `Subgroup.fintype` in the presence
of `Fintype N`.  -/
AddMonoidHom.fintypeMrange : {M : Type u_4} →
  {N : Type u_5} →
    [inst : AddMonoid M] →
      [inst_1 : AddMonoid N] → [Fintype M] → [DecidableEq N] → (f : M →+ N) → Fintype ↥(AddMonoidHom.mrange f)
-- Std.Http.Internal.Char
Std.Http.Internal.Char.qdtext.eq_1 : Std.Http.Internal.Char.qdtext '\t' = (true || decide ('#' ≤ '\t' ∧ '\t' ≤ '[') || decide (']' ≤ '\t' ∧ '\t' ≤ '~'))
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symm_continuousLinearEquivAt_eq' : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] {b : B}
  (hb : b ∈ e.baseSet),
  ↑(Bundle.Trivialization.continuousLinearEquivAt R e b hb).symm = Bundle.Trivialization.symmL R e b
-- Mathlib.Algebra.Torsor.Basic
Equiv.constVAdd_zero : ∀ (G : Type u_1) (P : Type u_2) [inst : AddGroup G] [inst_1 : AddTorsor G P], Equiv.constVAdd P 0 = 1
-- Mathlib.Data.Set.Image
Function.Surjective.preimage_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → Function.Injective (Set.preimage f)
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- See `rank_subsingleton` for the reason that `Nontrivial R` is needed.
Also see `rank_eq_zero_iff` for the version without `NoZeroSMulDivisor R M`.  -/
rank_zero_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M], Module.rank R M = 0 ↔ Subsingleton M
-- Std.Sync.CancellationToken
Std.CancellationToken.Consumer.select : Std.Async.Waiter Unit → Std.CancellationToken.Consumer
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.mk : ∀ {α : Type u_1} {β : Type u_2} {H G : Graph α β},
  autoParam (H.vertexSet ⊆ G.vertexSet) Graph.IsSubgraph.vertexSet_mono._autoParam →
    autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, H.IsLink e x y → G.IsLink e x y) Graph.IsSubgraph.isLink_mono._autoParam →
      H.IsSubgraph G
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
map_complEDS₂ : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {F : Type u_3} [inst_2 : FunLike F R S]
  [RingHomClass F R S] (f : F) (b c d : R) (n : ℤ), f (complEDS₂ b c d n) = complEDS₂ (f b) (f c) (f d) n
-- Mathlib.Data.Fin.Tuple.Embedding
Function.Embedding.embFinTwo_apply_one : ∀ {α : Type u_1} {a b : α} (h : a ≠ b), (Function.Embedding.embFinTwo h) 1 = b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospan_map_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  (w : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.cospan f g).map (CategoryTheory.Limits.WalkingCospan.Hom.id w) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.cospan f g).obj w)
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Given a subgroup `Γ` of a group `G`, and a function `f : G → M`, we "automorphize" `f` to a
function `G ⧸ Γ → M` by summing over `Γ` orbits, `g ↦ ∑' (γ : Γ), f(γ • g)`.  -/
QuotientGroup.automorphize : {M : Type u_11} →
  [TopologicalSpace M] → [AddCommMonoid M] → {G : Type u_13} → [inst : Group G] → {Γ : Subgroup G} → (G → M) → G ⧸ Γ → M
-- Mathlib.RingTheory.Regular.IsSMulRegular
isSMulRegular_of_ker_lsmul_eq_bot : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {r : R},
  ((LinearMap.lsmul R M) r).ker = ⊥ → IsSMulRegular M r
-- Init.Data.Order.LemmasExtra
Std.compare_eq_eq_iff_eq : ∀ {α : Type u} [inst : Ord α] [Std.LawfulEqOrd α] {a b : α}, compare a b = Ordering.eq ↔ a = b
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.limitGroup.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections],
  GrpCat.limitGroup F =
    { mul := GrpCat.limitGroup._aux_1 F, mul_assoc := ⋯, one := GrpCat.limitGroup._aux_4 F, one_mul := ⋯, mul_one := ⋯,
      npow := GrpCat.limitGroup._aux_8 F, npow_zero := ⋯, npow_succ := ⋯, inv := GrpCat.limitGroup._aux_12 F,
      div := GrpCat.limitGroup._aux_14 F, zpow := GrpCat.limitGroup._aux_16 F, div_eq_mul_inv := ⋯, zpow_zero' := ⋯,
      zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Lean.PrivateName
Lean.privateHeader : Lean.Name
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.smul_set_ae_eq : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) {s t : Set α},
  c • s =ᵐ[μ] c • t ↔ s =ᵐ[μ] t
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
DifferentiableWithinAt.cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x → DifferentiableWithinAt ℝ (fun x => Real.cos (f x)) s x
-- Mathlib.GroupTheory.Coset.Defs
/-- The equivalence relation corresponding to the partition of a group by left cosets
of a subgroup.  -/
QuotientAddGroup.leftRel : {α : Type u_1} → [inst : AddGroup α] → AddSubgroup α → Setoid α
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.iterFromIdx.eq_1 : ∀ {n : ℕ} {α : Type w} (xs : Vector α n) (pos : ℕ), xs.iterFromIdx pos = xs.toArray.iterFromIdx pos
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k} {he : t.modify k f ≠ ∅}, (t.modify k f).minKey he = t.minKey ⋯
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_le_floor : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a b : R}
  [IsStrictOrderedRing R], a ≤ b → ⌊a⌋₊ ≤ ⌊b⌋₊
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Set.toFinset_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] [inst_1 : DecidableEq β] (s : Set α) (t : Set β) [inst_2 : Fintype ↑s]
  [inst_3 : Fintype ↑t] [inst_4 : Fintype ↑(s • t)], (s • t).toFinset = s.toFinset • t.toFinset
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
_private.Mathlib.FieldTheory.IntermediateField.Adjoin.Defs.0.IntermediateField.mkInsertTerm.run.eq_def : ∀ {m : Type → Type} [inst : Monad m] [inst_1 : Lean.MonadQuotation m] (xs : Lean.TSyntaxArray `term) (i : ℕ),
  IntermediateField.mkInsertTerm.run✝ xs i =
    if h : i + 1 = Array.size xs then do
      let info ← Lean.MonadRef.mkInfoFromRefPos
      let scp ← Lean.getCurrMacroScope
      let quotCtx ← Lean.MonadQuotation.getContext
      pure
          {
            raw :=
              Lean.Syntax.node2 info `Lean.Parser.Term.app
                (Lean.Syntax.ident info "singleton".toRawSubstring' (Lean.addMacroScope quotCtx `singleton scp)
                  [Lean.Syntax.Preresolved.decl `Singleton.singleton []])
                (Lean.Syntax.node1 info `null xs[i].raw) }
    else
      if h : i < Array.size xs then do
        let __do_lift ← IntermediateField.mkInsertTerm.run✝ xs (i + 1)
        let info ← Lean.MonadRef.mkInfoFromRefPos
        let scp ← Lean.getCurrMacroScope
        let quotCtx ← Lean.MonadQuotation.getContext
        pure
            {
              raw :=
                Lean.Syntax.node2 info `Lean.Parser.Term.app
                  (Lean.Syntax.ident info "insert".toRawSubstring' (Lean.addMacroScope quotCtx `insert scp)
                    [Lean.Syntax.Preresolved.decl `Insert.insert []])
                  (Lean.Syntax.node2 info `null xs[i].raw __do_lift.raw) }
      else do
        let info ← Lean.MonadRef.mkInfoFromRefPos
        let scp ← Lean.getCurrMacroScope
        let quotCtx ← Lean.MonadQuotation.getContext
        pure
            {
              raw :=
                Lean.Syntax.ident info "EmptyCollection.emptyCollection".toRawSubstring'
                  (Lean.addMacroScope quotCtx `EmptyCollection.emptyCollection scp)
                  [Lean.Syntax.Preresolved.decl `EmptyCollection.emptyCollection []] }
-- Mathlib.Topology.Order
map_nhds_induced_of_mem : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {a : α},
  Set.range f ∈ nhds (f a) → Filter.map f (nhds a) = nhds (f a)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
_private.Mathlib.RingTheory.Polynomial.Cyclotomic.Basic.0.IsPrimitiveRoot.pow_sub_pow_eq_prod_sub_mul_field : ∀ {n : ℕ} {K : Type u_2} [inst : Field K] {ζ : K} (x y : K),
  0 < n → IsPrimitiveRoot ζ n → x ^ n - y ^ n = ∏ ζ ∈ Polynomial.nthRootsFinset n 1, (x - ζ * y)
-- Lean.Parser.Term
Lean.Parser.Term.ensureExpectedType : Lean.Parser.Parser
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula**: if `f : ℂ → E` is continuous on a closed disc of radius `R` and is
complex differentiable at all but countably many points of its interior, then for any `w` in this
interior we have $\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$.
 -/
Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {c w : ℂ} {f : ℂ → E}
  {s : Set ℂ},
  s.Countable →
    w ∈ Metric.ball c R →
      ContinuousOn f (Metric.closedBall c R) →
        (∀ x ∈ Metric.ball c R \ s, DifferentiableAt ℂ f x) →
          (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = f w
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.sum : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {ι : Type u_5} (s : Finset ι) (φ : ι → MvPolynomial σ R)
  (n : ℕ), (∀ i ∈ s, (φ i).IsHomogeneous n) → (∑ i ∈ s, φ i).IsHomogeneous n
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instFibrationSndOfIsStableUnderBaseChangeFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [inst_2 : CategoryTheory.Limits.HasPullback f g]
  [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [hf : HomotopicalAlgebra.Fibration f],
  HomotopicalAlgebra.Fibration (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.CategoryTheory.Limits.Types.Limits
/-- (internal implementation) the limit cone of a functor,
implemented as flat sections of a pi type
 -/
CategoryTheory.Limits.Types.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type (max v u))) → CategoryTheory.Limits.Cone F
-- Init.Data.Array.OfFn
_private.Init.Data.Array.OfFn.0.Array.ofFn.go.match_1.splitter : {n : ℕ} →
  (motive : (x : ℕ) → x ≤ n → Sort u_1) →
    (x : ℕ) → (x_1 : x ≤ n) → ((i : ℕ) → (h : i + 1 ≤ n) → motive i.succ h) → ((x : 0 ≤ n) → motive 0 x) → motive x x_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.getKey! a = m.getKeyD a default
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.ComonToMonOpOpObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Comon C), A.ComonToMonOpOpObj.X = Opposite.op A.X
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedMap_inducedMap`. -/
LinearOrderedField.inducedMap_inducedMap : ∀ (α : Type u_2) (β : Type u_3) (γ : Type u_4) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Field β] [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [inst_6 : Field γ]
  [inst_7 : ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] [Archimedean α] (a : α),
  ConditionallyCompleteLinearOrderedField.inducedMap β γ (ConditionallyCompleteLinearOrderedField.inducedMap α β a) =
    ConditionallyCompleteLinearOrderedField.inducedMap α γ a
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaEquiv_symm_naturality_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X X' : C} (f : X' ⟶ X)
  (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) (x : F.obj (Opposite.op X)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) (CategoryTheory.yonedaEquiv.symm x) =
    CategoryTheory.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) x)
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.mem_upShadow_iterate_iff_exists_card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ},
  t ∈ Finset.upShadow^[k] 𝒜 ↔ ∃ u, u.card = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
-- Mathlib.GroupTheory.Congruence.Basic
Con.instSMul : {α : Type u_4} →
  {M : Type u_5} →
    [inst : MulOneClass M] → [inst_1 : SMul α M] → [IsScalarTower α M M] → (c : Con M) → SMul α c.Quotient
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.infinite_sub : ∀ {α : Type u_2} [inst : AddGroup α] {s t : Set α}, (s - t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- A morphism of module objects.  -/
CategoryTheory.Mod.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} → [inst_4 : CategoryTheory.MonObj A] → CategoryTheory.Mod D A → CategoryTheory.Mod D A → Type v₂
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.addEqStep.checkDelayedThmInsts : List Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Lean.Meta.Basic
/-- Ensures that the user names of all local declarations after index `idx` have a macro scope.
 -/
Lean.MVarId.freshenLCtxUserNamesSinceIdx : {n : Type → Type} → [Monad n] → [Lean.MonadMCtx n] → [MonadLiftT Lean.MetaM n] → Lean.MVarId → ℕ → n Unit
-- Mathlib.Algebra.Group.Action.Defs
vadd_sub_assoc : ∀ {α : Type u_5} {β : Type u_6} [inst : SubNegMonoid β] [inst_1 : VAdd α β] [VAddAssocClass α β β] (r : α) (x y : β),
  (r +ᵥ x) - y = r +ᵥ x - y
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_closed_iff : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (s : Set M),
  s ∈ (FirstOrder.Language.Substructure.closure L).closed ↔
    ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f s