mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.lintegral_deterministic_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : α → β} (hf : Measurable f) (κ : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsSFiniteKernel κ] (a : α) {g : β × γ → ENNReal},
  Measurable g →
    ∫⁻ (p : β × γ), g p ∂((ProbabilityTheory.Kernel.deterministic f hf).prod κ) a = ∫⁻ (c : γ), g (f a, c) ∂κ a
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.cancelCommMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : CancelCommMonoid M] {S : Submonoid M} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N), f.cancelCommMonoid = { toCommMonoid := inst_1, toIsLeftCancelMul := ⋯ }
-- Aesop.Check
Aesop.Check.get : Lean.Options → Aesop.Check → Bool
-- Init.Data.Array.Lemmas
Array.extract_loop_zero : ∀ {α : Type u_1} {xs ys : Array α} {start : ℕ}, Array.extract.loop xs 0 start ys = ys
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_eq_mod_65536_iff : ∀ (a : UInt16) (b : UInt64), a.toUInt64 = b % 65536 ↔ a = b.toUInt16
-- Init.Data.BitVec.Basic
BitVec.append_ofBool : ∀ {w : ℕ} (msbs : BitVec w) (lsb : Bool), msbs ++ BitVec.ofBool lsb = msbs.concat lsb
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_inv_hom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f.inv)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom h f.hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id W))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom h (CategoryTheory.CategoryStruct.id W))
-- Std.Do.WP.SimpLemmas
Std.Do.WP.liftWith_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (f : ({β : Type u} → ExceptT ε m β → m (Except ε β)) → m α),
  (Std.Do.wp (MonadControl.liftWith f)).apply Q = (Std.Do.wp (f fun {β} x => x.run)).apply (Q.1, Q.2.2)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_down : ∀ {α : Type u_1} [inst : MeasurableSpace α], Measurable ULift.down
-- Mathlib.CategoryTheory.LocallyDirected
CategoryTheory.Functor.IsLocallyDirected.mk : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {F : CategoryTheory.Functor J (Type u_2)},
  (∀ {i j k : J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j),
      (CategoryTheory.ConcreteCategory.hom (F.map fi)) xi = (CategoryTheory.ConcreteCategory.hom (F.map fj)) xj →
        ∃ l fli flj x,
          (CategoryTheory.ConcreteCategory.hom (F.map fli)) x = xi ∧
            (CategoryTheory.ConcreteCategory.hom (F.map flj)) x = xj) →
    F.IsLocallyDirected
-- Mathlib.Topology.Algebra.Group.Basic
Subgroup.isClosed_topologicalClosure : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G] (s : Subgroup G),
  IsClosed ↑s.topologicalClosure
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.loopyOn_spanning_iff : ∀ {α : Type u_2} {X E : Set α}, (Matroid.loopyOn E).Spanning X ↔ X ⊆ E
-- Init.Data.Option.Lemmas
Option.getD_join : ∀ {α : Type u_1} {x : Option (Option α)} {default : α}, x.join.getD default = (x.getD (some default)).getD default
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.lift.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {W : C} (a : W ⟶ Y) (b : W ⟶ Z)
  (h : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g),
  CategoryTheory.ChosenPullbacksAlong.lift a b h =
    CategoryTheory.Over.Hom.left
      (((CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj g).homEquiv (CategoryTheory.Over.mk b)
          (CategoryTheory.Over.mk f))
        (CategoryTheory.Over.homMk a ⋯))
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileSystemWatcher.kind? : Lean.Lsp.FileSystemWatcher → Option ℕ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.empty_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp}, ∅ = t ↔ t = ∅
-- Mathlib.Topology.Algebra.Constructions
Units.continuous_iff : ∀ {M : Type u_1} {X : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : TopologicalSpace X]
  {f : X → Mˣ}, Continuous f ↔ Continuous (Units.val ∘ f) ∧ Continuous fun x => ↑(f x)⁻¹
-- Mathlib.Order.Filter.Germ.Basic
/-- **Alias** of the reverse direction of `Filter.Germ.coe_eq`. -/
Filter.EventuallyEq.germ_eq : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β}, f =ᶠ[l] g → ↑f = ↑g
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.isoNerve_hom_app_apply : ∀ {n d : ℕ} (s : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d })) (i : Fin (d + 1)),
  ((CategoryTheory.ConcreteCategory.hom ((SSet.stdSimplex.isoNerve.{u} n).hom.app (Opposite.op { len := d }))) s).obj
      i =
    { down := s i }
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.toAddSubgroup_toAddSubmonoid : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M),
  p.toAddSubgroup.toAddSubmonoid = p.toAddSubmonoid
-- Lean.Elab.Arg
Lean.Elab.Term.instInhabitedNamedArg.default : Lean.Elab.Term.NamedArg
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.FormallySmooth.of_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  Function.Bijective ⇑f → f.FormallySmooth
-- Mathlib.Topology.LocallyFinite
LocallyFinite.nhdsWithin_iUnion : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
  LocallyFinite f → ∀ (a : X), nhdsWithin a (⋃ i, f i) = ⨆ i, nhdsWithin a (f i)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.mul_modByMonic : ∀ {R : Type u} [inst : CommRing R] (p₁ p₂ q : Polynomial R), p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q
-- Mathlib.Probability.Kernel.RadonNikodym
/-- Radon-Nikodym derivative of the kernel `κ` with respect to the kernel `η`.  -/
ProbabilityTheory.Kernel.rnDeriv : {α : Type u_3} →
  {γ : Type u_4} →
    {mα : MeasurableSpace α} →
      {mγ : MeasurableSpace γ} →
        [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] →
          ProbabilityTheory.Kernel α γ → ProbabilityTheory.Kernel α γ → α → γ → ENNReal
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.E'.eq_1 : ∀ (r : ℕ+), ADEInequality.E' r = {2, 3, r}
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct
SSet.innerAnodyneExtensions_unionProd_ι : ∀ {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex),
  SSet.innerAnodyneExtensions B.ι → SSet.innerAnodyneExtensions (A.unionProd B).ι
-- Mathlib.Order.Interval.Multiset
Multiset.Ioo_eq_zero_of_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, b ≤ a → Multiset.Ioo a b = 0
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.mk_coe : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (f : A →⋆ₐ[R] B) (h₁ : f 1 = 1)
  (h₂ :
    ∀ (x y : A),
      { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) =
        { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y)
  (h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0)
  (h₄ :
    ∀ (x y : A),
      (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) =
        (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x +
          (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y)
  (h₅ :
    ∀ (r : R),
      (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) =
        (algebraMap R B) r)
  (h₆ :
    ∀ (x : A),
      (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                    commutes' := h₅ }.toRingHom).toFun
          (star x) =
        star
          ((↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                      commutes' := h₅ }.toRingHom).toFun
            x)),
  { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆ } = f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_alter_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {k : α} {f : Option β → Option β} (h : m.WF)
  {hc : k ∈ Std.DHashMap.Raw.Const.alter m k f},
  Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.Const.alter m k f) k hc = (f (Std.DHashMap.Raw.Const.get? m k)).get ⋯
-- Lean.Meta.Tactic.Grind.MarkAccessible
/-- Helper tactic for marking accessible names in the local context.
This is a trick used during `grind` preprocessing when `clean := false`.
Recall that during preprocessing, `grind` reverts all hypotheses and reintroduce them while normalizing and
performing eager case splitting.
When `clean := false`, we create a fresh user name unless the name was "marked" by this function.
 -/
Lean.MVarId.markAccessible : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCompletionList.fromJson : Lean.Json → Except String Lean.Lsp.CompletionList
-- Mathlib.Data.Erased
/-- `(<$>)` operation on `Erased`.

This is a separate definition because `α` and `β` can live in different
universes (the universe is fixed in `Functor`).
 -/
Erased.map : {α : Sort u_1} → {β : Sort u_2} → (α → β) → Erased α → Erased β
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β)
  (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.RingTheory.DedekindDomain.Dvr
/-- The localization of a Dedekind domain at every nonzero prime ideal is a Dedekind domain.  -/
IsLocalization.AtPrime.isDedekindDomain : ∀ (A : Type u_1) [inst : CommRing A] [IsDomain A] [IsDedekindDomain A] (P : Ideal A) [inst_3 : P.IsPrime]
  (Aₘ : Type u_2) [inst_4 : CommRing Aₘ] [IsDomain Aₘ] [inst_6 : Algebra A Aₘ] [IsLocalization.AtPrime Aₘ P],
  IsDedekindDomain Aₘ
-- Mathlib.Data.Analysis.Filter
CFilter.pt : {α : Type u_1} → {σ : Type u_2} → [inst : PartialOrder α] → CFilter α σ → σ
-- Mathlib.Combinatorics.HalesJewett
/-- The **Hales-Jewett theorem**: For any finite types `α` and `κ`, there exists a finite type `ι`
such that whenever the hypercube `ι → α` is `κ`-colored, there is a monochromatic combinatorial
line.  -/
Combinatorics.Line.exists_mono_in_high_dimension : ∀ (α : Type u) [Finite α] (κ : Type v) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, Combinatorics.Line.IsMono C l
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.tendsto_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X}, x ∈ e.source → Filter.Tendsto (↑e.symm) (nhds (↑e x)) (nhds x)
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_le_sup : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G), ⁅H₁, H₂⁆ ≤ H₁ ⊔ H₂
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct
SSet.innerAnodyneExtensions_pushoutObjObjι : ∀ {X₁ X₂ Y₁ Y₂ : SSet} {i : X₁ ⟶ Y₁} {j : X₂ ⟶ Y₂}
  (sq₁₂ : (CategoryTheory.MonoidalCategory.curriedTensor SSet).PushoutObjObj i j) [CategoryTheory.Mono i],
  SSet.innerAnodyneExtensions j → SSet.innerAnodyneExtensions sq₁₂.ι
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.idealOpensGI_choice : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [inst_2 : CompactSpace X]
  [inst_3 : T2Space X] (I : Ideal C(X, 𝕜)) (x : ContinuousMap.idealOfSet 𝕜 ↑(ContinuousMap.opensOfIdeal I) ≤ I),
  (ContinuousMap.idealOpensGI X 𝕜).choice I x = ContinuousMap.opensOfIdeal I.closure
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.FreeVarMap : Type
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.Std.Slice.toList.eq_1 : ∀ {γ : Type u_1} {α β : Type u_2} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  (s : Std.Slice γ), s.toList = (Std.Slice.Internal.iter s).toList
-- Init.Data.List.TakeDrop
List.take_append_getLast? : ∀ {α : Type u_1} (l : List α), List.take (l.length - 1) l ++ l.getLast?.toList = l
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.refl : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} (m : Std.DHashMap α β), m.Equiv m
-- Mathlib.Analysis.Calculus.FDeriv.Defs
fderiv_def : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_6} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E → F) (x : E), fderiv 𝕜 f x = fderivWithin 𝕜 f Set.univ x
-- Init.Data.List.Sublist
List.subset_of_cons_subset : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, a :: l₁ ⊆ l₂ → l₁ ⊆ l₂
-- Mathlib.Data.Tree.Basic
BinaryTree.left.eq_2 : ∀ {α : Type u} (a : α) (l r : BinaryTree α), (BinaryTree.node a l r).left = l
-- Mathlib.Data.Num.Basic
/-- Auxiliary definition for `sqrtAux`.  -/
_private.Mathlib.Data.Num.Basic.0.PosNum.sqrtAux1 : PosNum → Num → Num → Num × Num
-- Mathlib.RingTheory.Coalgebra.Basic
Prod.instCoalgebraStruct : (R : Type u) →
  (A : Type v) →
    (B : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] → [Coalgebra R A] → [Coalgebra R B] → CoalgebraStruct R (A × B)
-- Init.Grind.AC
Lean.Grind.AC.diseq_simp_rhs_exact : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (lhs₁ rhs₁ lhs₂ : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
    Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx lhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₁
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.multiset_sum : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid β] (m : Multiset (α → β)),
  (∀ f ∈ m, HasCompactSupport f) → HasCompactSupport m.sum
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S),
  f.mk' x y = f x * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y)⁻¹
-- Mathlib.Algebra.Module.BigOperators
Fintype.sum_single_smul : ∀ {ι : Type u_1} {α : Type u_3} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : AddCommMonoid α] {R : Type u_7}
  [inst_3 : Semiring R] [inst_4 : Module R α] (f : ι → α) (r : R) (i₀ : ι), ∑ i, Pi.single i₀ r i • f i = r • f i₀
-- Mathlib.Data.Set.Lattice
Set.subset_iInter_iff : ∀ {α : Type u_1} {ι : Sort u_5} {s : Set α} {t : ι → Set α}, s ⊆ ⋂ i, t i ↔ ∀ (i : ι), s ⊆ t i
-- Init.Data.Int.Bitwise.Lemmas
Int.le_shiftRight_of_nonpos : ∀ {n : ℤ} {s : ℕ}, n ≤ 0 → n ≤ n >>> s
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (h : Topology.IsOpenEmbedding f) [inst_2 : Nonempty X] {x : X},
  ↑(Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h).symm (f x) = x
-- Init.Data.AC
Lean.Data.AC.instReprExpr.repr : Lean.Data.AC.Expr → ℕ → Std.Format
-- Mathlib.Data.Finset.Image
Finset.subtype_mono : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p], Monotone (Finset.subtype p)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.image_symm_image : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (s : Set N),
  ⇑h '' ⇑h.symm '' s = s
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.term_welldef : ∀ {n : ℕ},
  0 < n → ∀ {s : ℝ}, 0 < s → IntervalIntegrable (fun x => (x - ↑n) / x ^ (s + 1)) MeasureTheory.volume (↑n) (↑n + 1)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.IntegrableOn.continuousOn_mul : ∀ {X : Type u_1} {R : Type u_8} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] {K : Set X} [inst_3 : NormedRing R] [SecondCountableTopologyEither X R] {g g' : X → R}
  [T2Space X],
  ContinuousOn g K →
    MeasureTheory.IntegrableOn g' K μ → IsCompact K → MeasureTheory.IntegrableOn (fun x => g x * g' x) K μ
-- Mathlib.Algebra.Group.Basic
leftInverse_add_left_sub : ∀ {G : Type u_3} [inst : AddGroup G] (c : G), Function.LeftInverse (fun x => x + c) fun x => x - c
-- Lean.Expr
/-- Lean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
 -/
Lean.Expr : Type
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
aemeasurable_pi_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {δ : Type u_6} {X : δ → Type u_7}
  {mX : (a : δ) → MeasurableSpace (X a)} [Countable δ] {g : α → (a : δ) → X a},
  AEMeasurable g μ ↔ ∀ (a : δ), AEMeasurable (fun x => g x a) μ
-- Lean.Elab.Command.Scope
/-- `omit`ted section variable names (from `varUIds`)  -/
Lean.Elab.Command.Scope.omittedVars : Lean.Elab.Command.Scope → List Lean.Name
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_eq_getD_default : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {a : α}, m[a]! = m.getD a default
-- Mathlib.Algebra.Group.Pi.Basic
Pi.divisionMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → DivisionMonoid (f i)],
  Pi.divisionMonoid = { toDivInvMonoid := Pi.divInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }
-- Lean.Parser.Command
Lean.Parser.Command.withExporting.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.ι₂_desc : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃),
  CategoryTheory.CategoryStruct.comp SSet.horn₃₁.ι₂ (SSet.horn₃₁.desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃) = f₂
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisor.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] (g : PowerSeries A) [inst_1 : IsLocalRing A],
  g.IsWeierstrassDivisor = g.IsWeierstrassDivisorAt (IsLocalRing.maximalIdeal A)
-- Init.Conv
Lean.Parser.Tactic.Conv.convSeq : Lean.ParserDescr
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
Lean.Meta.RefinedDiscrTree.ModuleDiscrTreeRef.mk : {α : Type} → IO.Ref (Lean.Meta.RefinedDiscrTree α) → Lean.Meta.RefinedDiscrTree.ModuleDiscrTreeRef α
-- Mathlib.LinearAlgebra.Ray
/-- A vector is in the same ray as a positive multiple of itself.  -/
SameRay.sameRay_pos_smul_right : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {S : Type u_5} [inst_5 : CommSemiring S] [inst_6 : PartialOrder S]
  [inst_7 : Algebra S R] [inst_8 : Module S M] [SMulPosMono S R] [IsScalarTower S R M] {a : S} (v : M),
  0 < a → SameRay R v (a • v)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.addActionHom_of_embedding.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] (α : Type u_2) [inst_1 : AddAction G α] (n : ℕ) [inst_2 : DecidableEq α],
  Set.powersetCard.addActionHom_of_embedding G α n = { toFun := Set.powersetCard.ofFinEmb n α, map_vadd' := ⋯ }
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
/-- Put the same topological space structure on `Mᵈᵐᵃ` as on the original space.  -/
DomMulAct.instTopologicalSpace : {M : Type u_1} → [TopologicalSpace M] → TopologicalSpace Mᵈᵐᵃ
-- Mathlib.Order.Hom.Lattice
SupHom.coe_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] (f g : SupHom α β), ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_insertMany_list : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List ((a : α) × β a)},
      List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
        (∀ a ∈ m, (List.map Sigma.fst l).contains a = false) → (m.insertMany l).size = m.size + l.length
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesAt.fderiv_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E},
  HasFPowerSeriesAt f p x → fderiv 𝕜 f x = (continuousMultilinearCurryFin1 𝕜 E F) (p 1)
-- Mathlib.Order.Antisymmetrization
toAntisymmetrization_mono : ∀ {α : Type u_1} [inst : Preorder α], Monotone (toAntisymmetrization fun x1 x2 => x1 ≤ x2)
-- Mathlib.Algebra.Order.Hom.Ring
/-- `OrderRingIso α β`, denoted as `α ≃+*o β`,
is the type of order-preserving semiring isomorphisms between `α` and `β`.

When possible, instead of parametrizing results over `(f : OrderRingIso α β)`,
you should parametrize over `(F : Type*) [OrderRingIsoClass F α β] (f : F)`.

When you extend this structure, make sure to extend `OrderRingIsoClass`.  -/
OrderRingIso : (α : Type u_6) → (β : Type u_7) → [Mul α] → [Add α] → [Mul β] → [Add β] → [LE α] → [LE β] → Type (max u_6 u_7)
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
/-- If `B` is faithfully flat over `A`, every prime of `A` comes from a prime of `B`.  -/
Ideal.exists_isPrime_liesOver_of_faithfullyFlat : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Module.FaithfullyFlat A B] (p : Ideal A) [p.IsPrime], ∃ P, P.IsPrime ∧ P.LiesOver p
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)],
  (((HomologicalComplex₂.shiftFunctor₂ C y).comp (HomologicalComplex₂.shiftFunctor₁ C x)).obj K).HasTotal
    (ComplexShape.up ℤ)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precompose.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : G ⟶ F),
  CategoryTheory.Limits.Cocone.precompose α =
    { obj := fun c => { pt := c.pt, ι := CategoryTheory.CategoryStruct.comp α c.ι },
      map := fun {Y X} f => { hom := f.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }