mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Term.TermElabM
/-- If `expectedType?` is `some t`, then ensures `t` and `eType` are definitionally equal by inserting a coercion if necessary.

Argument `f?` is used only for generating error messages when inserting coercions fails.
 -/
Lean.Elab.Term.ensureHasType : Option Lean.Expr →
  Lean.Expr → optParam (Option String) none → optParam (Option Lean.Expr) none → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_smul' : ∀ {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V) (a : K),
  Submodule.map (a • f) p = ⨆ (_ : a ≠ 0), Submodule.map f p
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- The canonical map on sheafifications induced by a morphism.  -/
CategoryTheory.sheafifyMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_2 : CategoryTheory.HasWeakSheafify J D] →
            {P Q : CategoryTheory.Functor Cᵒᵖ D} → (P ⟶ Q) → (CategoryTheory.sheafify J P ⟶ CategoryTheory.sheafify J Q)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.mk : {X : Type u} →
  [inst : TopologicalSpace X] →
    {C : Set X} →
      (cell : ℕ → Type u) →
        (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) →
          (∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) →
            (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) →
              (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) →
                (Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) →
                  (∀ (n : ℕ) (i : cell n),
                      ∃ I,
                        Set.MapsTo (↑(map n i)) (Metric.sphere 0 1)
                          (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' Metric.closedBall 0 1)) →
                    (∀ A ⊆ C,
                        (∀ (n : ℕ) (j : cell n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) → IsClosed A) →
                      ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C → Topology.CWComplex C
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.map_sub : ∀ (R : Type u_1) [inst : CommSemiring R] {S : Type u_3} [inst_1 : Ring S] [inst_2 : TopologicalSpace S]
  [inst_3 : Algebra R S] {B : Type u_4} [inst_4 : Ring B] [inst_5 : TopologicalSpace B] [inst_6 : Algebra R B]
  (f : S →A[R] B) (x y : S), f (x - y) = f x - f y
-- Mathlib.Data.Finset.Prod
Finset.diag_empty : ∀ {α : Type u_1}, ∅.diag = ∅
-- Mathlib.LinearAlgebra.Matrix.DotProduct
/-- Note that this applies to `ℂ` via `RCLike.toStarOrderedRing`.  -/
dotProduct_self_star_eq_zero : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : PartialOrder R] [inst_2 : NonUnitalRing R]
  [inst_3 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {v : n → R}, v ⬝ᵥ star v = 0 ↔ v = 0
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₁.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
  {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G)
  (p : CategoryTheory.OverPresheafAux.YonedaCollection F X),
  CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p =
    CategoryTheory.OverPresheafAux.YonedaCollection.mk p.fst
      ((CategoryTheory.ConcreteCategory.hom (η.app (Opposite.op (CategoryTheory.CostructuredArrow.mk p.fst)))) p.snd)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformity_edist_aux : ∀ {α : Type u_3} (d : α → α → NNReal),
  ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | ↑(d p.1 p.2) < ε} =
    ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | ↑(d p.1 p.2) < ε}
-- Lean.Elab.Command
/-- The declaration name of the macro.  -/
Lean.Elab.Command.MacroExpandedSnapshot.macroDecl : Lean.Elab.Command.MacroExpandedSnapshot → Lean.Name
-- Std.Http.Data.Headers.Basic
/-- Serializes an `Expect` header.
 -/
Std.Http.Header.Expect.serialize : Std.Http.Header.Expect → Std.Http.Header.Name × Std.Http.Header.Value
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_else_ite : ∀ {α : Sort u_1} (cond : Bool) {a b c : α}, (bif cond then a else bif cond then b else c) = bif cond then a else c
-- Mathlib.Analysis.Normed.Group.Constructions
/-- The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.  -/
Pi.sum_nnnorm_apply_le_nnnorm' : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i),
  ∑ i, ‖f i‖₊ ≤ Fintype.card ι • ‖f‖₊
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.measurable_rangeSplitting : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β},
  MeasurableEmbedding f → Measurable (Set.rangeSplitting f)
-- Init.Data.UInt.Bitwise
instAssociativeUInt32HAnd : Std.Associative fun x1 x2 => x1 &&& x2
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- If `χ` and `ψ` are multiplicative characters of order dividing `n` on a finite field `F`
with values in an integral domain `R` and `μ` is a primitive `n`th root of unity in `R`,
then `J(χ,ψ) = -1 + z*(μ - 1)^2` for some `z ∈ ℤ[μ] ⊆ R`. (We assume that `#F ≡ 1 mod n`.)
Note that we do not state this as a divisibility in `R`, as this would give a weaker statement.  -/
exists_jacobiSum_eq_neg_one_add : ∀ {F : Type u_1} {R : Type u_2} [inst : Field F] [inst_1 : CommRing R] [IsDomain R] [inst_3 : Fintype F] {n : ℕ},
  2 < n →
    ∀ {χ ψ : MulChar F R} {μ : R},
      χ ^ n = 1 →
        ψ ^ n = 1 → n ∣ Fintype.card F - 1 → IsPrimitiveRoot μ n → ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2
-- Mathlib.Algebra.Order.Group.Lattice
div_sup : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a b c : α),
  c / (a ⊔ b) = c / a ⊓ c / b
-- Init.Data.String.Lemmas.Order
String.Pos.lt_endPos_iff : ∀ {s : String} (p : s.Pos), p < s.endPos ↔ p ≠ s.endPos
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The word of length `m` that alternates between `i` and `i'`, ending with `i'`.  -/
CoxeterSystem.alternatingWord : {B : Type u_1} → B → B → ℕ → List B
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.commaFromUnder_obj_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (K : CategoryTheory.Functor J (CategoryTheory.Under X)) (a : J),
  (CategoryTheory.WithInitial.commaFromUnder.obj K).hom.app a = (K.obj a).hom
-- Mathlib.Order.Interval.Finset.Defs
/-- A constructor from a definition of `Finset.Icc` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrder.ofIcc`, this one requires `DecidableLE` but
only `Preorder`.  -/
LocallyFiniteOrder.ofIcc' : (α : Type u_1) →
  [inst : Preorder α] →
    [DecidableLE α] →
      (finsetIcc : α → α → Finset α) → (∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b) → LocallyFiniteOrder α
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.main.unpack : {α : Type} → Lean.Expr → (Array Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.mk : {α : Type} → Std.Mutex (Std.Bounded.State✝ α) → Std.Bounded✝ α
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.contractibleTriangleFunctor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  (CategoryTheory.Pretriangulated.contractibleTriangleFunctor C).obj X =
    CategoryTheory.Pretriangulated.contractibleTriangle X
-- Mathlib.Algebra.CharP.Subring
/-- The characteristic of a division ring is equal to the characteristic
of its center  -/
CharP.charP_center_iff : ∀ {R : Type u} [inst : Ring R] {p : ℕ}, CharP (↥(Subring.center R)) p ↔ CharP R p
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves binary biproducts of `X` and `Y` if `F` maps every bilimit bicone over
`X` and `Y` to a bilimit bicone over `F.obj X` and `F.obj Y`.  -/
CategoryTheory.Limits.PreservesBinaryBiproduct.preserves : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {X Y : C}
  {F : CategoryTheory.Functor C D} {inst_4 : F.PreservesZeroMorphisms}
  [self : CategoryTheory.Limits.PreservesBinaryBiproduct X Y F] {b : CategoryTheory.Limits.BinaryBicone X Y}
  (a : b.IsBilimit), Nonempty (F.mapBinaryBicone b).IsBilimit
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_eq_getElem! : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α} {h' : a ∈ m}, m[a] = m[a]!
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.isAddUnit : ∀ {M : Type u_6} [inst : AddMonoid M] {x : M}, IsOfFinAddOrder x → IsAddUnit x
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_9 : HAdd Std.Time.Millisecond.Offset Std.Time.Hour.Offset Std.Time.Millisecond.Offset
-- Mathlib.Topology.Algebra.Group.Basic
/-- An additive monoid homomorphism (a bundled morphism of a type that implements
`AddMonoidHomClass`) from an additive topological group to an additive topological monoid is
continuous provided that it is continuous at zero. See also
`uniformContinuous_of_continuousAt_zero`.  -/
continuous_of_continuousAt_zero : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {M : Type u_1}
  {hom : Type u_2} [inst_3 : AddZeroClass M] [inst_4 : TopologicalSpace M] [ContinuousAdd M] [inst_6 : FunLike hom G M]
  [AddMonoidHomClass hom G M] (f : hom), ContinuousAt (⇑f) 0 → Continuous ⇑f
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
/-- Noncomputably determines the multiset of prime factors.  -/
UniqueFactorizationMonoid.normalizedFactors : {α : Type u_1} →
  [inst : CommMonoidWithZero α] → [NormalizationMonoid α] → [UniqueFactorizationMonoid α] → α → Multiset α
-- Mathlib.Topology.Category.TopPair
TopPair.isEmbedding_map : ∀ (X : TopPair), Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)
-- Mathlib.Topology.Sets.Compacts
/-- The image of a compact set under a continuous function.  -/
TopologicalSpace.Compacts.map : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        (f : α → β) → Continuous f → TopologicalSpace.Compacts α → TopologicalSpace.Compacts β
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_norm_eq : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) (n : ℕ),
  ‖newton_seq_gen✝ hnorm (n + 1) - newton_seq_gen✝ hnorm n‖ =
    ‖(Polynomial.aeval (newton_seq_gen✝ hnorm n)) F‖ /
      ‖(Polynomial.aeval (newton_seq_gen✝ hnorm n)) (Polynomial.derivative F)‖