mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
/-- The projection `U.power α ⟶ U` for each `a : α`.  -/
CategoryTheory.Limits.FormalCoproduct.powerπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (U : CategoryTheory.Limits.FormalCoproduct C) →
      {α : Type} → [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] → α → (U.power α ⟶ U)
-- Mathlib.Algebra.NoZeroSMulDivisors.Defs
noZeroSMulDivisors_iff_right_eq_zero_of_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMul R M],
  NoZeroSMulDivisors R M ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0
-- Mathlib.Data.Set.Card
Set.Finite.finite_of_encard_le : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s.Finite → t.encard ≤ s.encard → t.Finite
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.aeval_iterate_derivative_of_ge : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_3) [inst_1 : CommRing A] [inst_2 : Algebra R A] (p : Polynomial R)
  (q : ℕ) {k : ℕ},
  q ≤ k →
    ∃ gp,
      gp.natDegree ≤ p.natDegree - k ∧
        ∀ (r : A), (Polynomial.aeval r) ((⇑Polynomial.derivative)^[k] p) = q.factorial • (Polynomial.aeval r) gp
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.add_const : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f : α → M}
  [MeasurableAdd M], Measurable f → ∀ (c : M), Measurable fun x => f x + c
-- Mathlib.Tactic.Linarith.Datatypes
/-- The strength of the comparison, `<`, `≤`, or `=`.  -/
Mathlib.Tactic.Linarith.Comp.str : Mathlib.Tactic.Linarith.Comp → Mathlib.Ineq
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.coe_mul : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrderedCommMonoidWithZero α] [inst_1 : LinearOrderedCommMonoidWithZero β]
  (f g : α →*₀o β), ⇑(f * g) = ⇑f * ⇑g
-- Mathlib.Analysis.Convex.BetweenList
List.wbtw_nil : ∀ (R : Type u_1) {V : Type u_2} (P : Type u_4) [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P], List.Wbtw R []
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.μ_δ_assoc : ∀ {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 D}
  (F : CategoryTheory.Functor C D) [self : F.Monoidal] (X Y : C) {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) h) =
    h
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_le_comm : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, a - b ≤ c ↔ a - c ≤ b
-- Mathlib.Data.Fin.VecNotation
/-- The core logic of `loop` is that `loop 0 ![] = ![a 0, a 1, a 2] = loop 1 ![a 2]`, where
recursion starts from the end. In this example, on the right-hand side, the variable `rest := 1`
tracks the length of the current generated notation `![a 2]`, and the last used index is
`n - rest` (`= 3 - 1 = 2`).  -/
_private.Mathlib.Data.Fin.VecNotation.0.PiFin.mkLiteralQ.loop : {u : Lean.Level} → {α : Q(Type u)} → {n : ℕ} → (Fin n → Q(«$α»)) → (i : ℕ) → Q(Fin «$i» → «$α») → Q(Fin «$n» → «$α»)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.associator_hom_right_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'')
  (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') (x : C),
  (φ.associator φ' φ'').hom.right.app x =
    CategoryTheory.CategoryStruct.id (φ''.right.obj (φ'.right.obj (φ.right.obj x)))
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_add_omega0_opow : ∀ (o : Ordinal.{u_1}), Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) (Ordinal.omega0 ^ o)
-- Lean.Meta.Basic
Lean.PPContext.runCoreM : {α : Type} → Lean.PPContext → Lean.CoreM α → IO α
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- **Alias** of `AddHom.domRestrict`.

---

Restriction of an AddSemigroup hom to an `AddSubsemigroup` of the domain.  -/
AddHom.restrict : {M : Type u_1} →
  {σ : Type u_4} →
    [inst : Add M] →
      {N : Type u_5} →
        [inst_1 : Add N] → [inst_2 : SetLike σ M] → [inst_3 : AddMemClass σ M] → (M →ₙ+ N) → (S : σ) → ↥S →ₙ+ N
-- Aesop.Tree.Tracing
_private.Aesop.Tree.Tracing.0.Aesop.Goal.traceMetadata.trc : Aesop.TraceOption → Lean.MessageData → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- Notation for the CoGrothendieck category associated to a pseudofunctor `F`.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.«term∫ᶜ_» : Lean.ParserDescr
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_zsmul_add' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIcoMod hp (m • p + a) b = m • p + toIcoMod hp a b
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_eq_back_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {he : t.isEmpty = false},
  t.max he = t.toArray.back ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.existsMulOfLe : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [ExistsAddOfLE α], ExistsMulOfLE (Multiplicative α)
-- Mathlib.Geometry.Manifold.HasGroupoid
Structomorph.mk.injEq : ∀ {H : Type u} [inst : TopologicalSpace H] {G : StructureGroupoid H} {M : Type u_5} {M' : Type u_6}
  [inst_1 : TopologicalSpace M] [inst_2 : TopologicalSpace M'] [inst_3 : ChartedSpace H M] [inst_4 : ChartedSpace H M']
  (toHomeomorph : M ≃ₜ M')
  (mem_groupoid :
    ∀ (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H),
      c ∈ atlas H M → c' ∈ atlas H M' → c.symm.trans (toHomeomorph.toOpenPartialHomeomorph.trans c') ∈ G)
  (toHomeomorph_1 : M ≃ₜ M')
  (mem_groupoid_1 :
    ∀ (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H),
      c ∈ atlas H M → c' ∈ atlas H M' → c.symm.trans (toHomeomorph_1.toOpenPartialHomeomorph.trans c') ∈ G),
  ({ toHomeomorph := toHomeomorph, mem_groupoid := mem_groupoid } =
      { toHomeomorph := toHomeomorph_1, mem_groupoid := mem_groupoid_1 }) =
    (toHomeomorph = toHomeomorph_1)
-- Init.Data.List.Count
List.count_singleton : ∀ {α : Type u_1} [inst : BEq α] {a b : α}, List.count a [b] = if (b == a) = true then 1 else 0
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.add_of : ∀ {A : Type u_1} [inst : AddMonoid A] (a b : A), a + b = a + b
-- Mathlib.Topology.Algebra.Monoid
addHomOfMemClosureRangeCoe_apply : ∀ {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂] [inst_2 : Add M₁] [inst_3 : Add M₂]
  [inst_4 : ContinuousAdd M₂] {F : Type u_8} [inst_5 : FunLike F M₁ M₂] [inst_6 : AddHomClass F M₁ M₂] (f : M₁ → M₂)
  (hf : f ∈ closure (Set.range fun f x => f x)), ⇑(addHomOfMemClosureRangeCoe f hf) = f
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation) The map from `i'` to `i`. See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.hii' : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} →
            [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] →
              [inst_2 : CategoryTheory.IsCofiltered I] →
                [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] →
                  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) → A.i' ⟶ A.i
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.equivOfEquivalence_symm_apply : ∀ {α : Type u₁} {β : Type u₂} (h : CategoryTheory.Discrete α ≌ CategoryTheory.Discrete β) (a : β),
  (CategoryTheory.Discrete.equivOfEquivalence h).symm a =
    (CategoryTheory.Discrete.as ∘ h.inverse.obj ∘ CategoryTheory.Discrete.mk) a
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.handleIn : Lean.Linter.MissingDocs.Handler
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.jp.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {decl decl_1 : Lean.Compiler.LCNF.FunDecl pu},
  Lean.Compiler.LCNF.CodeDecl.jp decl = Lean.Compiler.LCNF.CodeDecl.jp decl_1 → decl = decl_1
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.epiModSerre.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P P_1 : CategoryTheory.ObjectProperty C) (e_P : P = P_1) [inst_2 : P.IsSerreClass] ⦃X Y : C⦄ (x x_1 : X ⟶ Y),
  x = x_1 → P.epiModSerre x = P_1.epiModSerre x_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [Std.TransCmp cmp], t.WF → ∀ {k : α}, t.keys.contains k = t.contains k
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_iff_ne_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a : α} [inst_2 : OrderBot α], Order.pred a < a ↔ a ≠ ⊥
-- Std.Http.Internal.IndexMultiMap
/-- Converts the multimap to a list of key-value pairs (flattened).
 -/
Std.Internal.IndexMultiMap.toList : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → List (α × β)
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- A proof that `g` is meromorphic in normal form on `closedBall 0 R`.  -/
Complex.CanonicalDecomp.meromorphicNFOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {R : ℝ},
  Complex.CanonicalDecomp f g R → MeromorphicNFOn g (Metric.closedBall 0 R)
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.State.mk.injEq : ∀ (varMap : Lean.Meta.KExprMap ℕ) (vars : Array Lean.Expr) (varMap_1 : Lean.Meta.KExprMap ℕ) (vars_1 : Array Lean.Expr),
  ({ varMap := varMap, vars := vars } = { varMap := varMap_1, vars := vars_1 }) = (varMap = varMap_1 ∧ vars = vars_1)
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor I C) [inst_2 : CategoryTheory.Limits.HasColimit F] (i : I)
  {Z : CategoryTheory.Functor C (Type u₂)} (h : CategoryTheory.coyoneda.obj (Opposite.op (F.obj i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π (F.op.comp CategoryTheory.coyoneda) (Opposite.op i)) h
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.coe_algebraMap_eq_CC : ∀ {R : Type u_1} [inst : CommSemiring R], ⇑(algebraMap R (Polynomial (Polynomial R))) = Polynomial.CC
-- Mathlib.LinearAlgebra.AffineSpace.Ceva
/-- A version of **Ceva's theorem** for an arbitrary indexed affinely independent family of points:
consider some lines, each through one of the points and an affine combination of the points, and
suppose they concur at `p'`; then `p'` is an affine combination of the points with weights
proportional to those in the respective affine combinations.  -/
AffineIndependent.exists_affineCombination_eq_smul_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] {p : ι → P},
  AffineIndependent k p →
    ∀ {s : Set ι},
      s.Nonempty →
        ∀ {fs : ↑s → Finset ι} {w : ↑s → ι → k},
          (∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1) →
            ∀ {p' : P},
              (∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]) →
                ∃ w' fs',
                  ∑ j ∈ fs', w' j = 1 ∧
                    (Finset.affineCombination k fs' p) w' = p' ∧
                      ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑fs' \ {↑i}).indicator w' j
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.toProd_comp_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.toProd.comp Monoid.Coprod.inl = MonoidHom.inl M N
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.piecewise_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (x y : Π₀ (i : ι), β i) (s : Set ι)
  [inst_1 : (i : ι) → Decidable (i ∈ s)] (i : ι), (x.piecewise y s) i = if i ∈ s then x i else y i
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_rcc_eq_zero_iff : ∀ {m n i : ℕ}, (m...=n).toList[i]! = 0 ↔ n + 1 ≤ i + m ∨ m = 0 ∧ i = 0
-- Std.Internal.UV.TCP
/-- Sends data through a TCP socket.
 -/
Std.Internal.UV.TCP.Socket.send : Std.Internal.UV.TCP.Socket → Array ByteArray → IO (IO.Promise (Except IO.Error Unit))
-- Init.Data.RArray
Lean.RArray.leaf : {α : Type u} → α → Lean.RArray α
-- Mathlib.Data.Finsupp.Basic
Nat.cast_finsuppProd : ∀ {α : Type u_1} {M : Type u_5} {R : Type u_10} [inst : Zero M] (f : α →₀ M) [inst_1 : CommSemiring R] (g : α → M → ℕ),
  ↑(f.prod g) = f.prod fun a b => ↑(g a b)
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.to_addSubmonoid_inj : ∀ {M : Type u_1} [inst : AddZeroClass M] (c d : AddCon M), ↑c = ↑d → c = d
-- Init.Data.SInt.Lemmas
Int64.minValue_div_neg_one : Int64.minValue / -1 = Int64.minValue
-- Init.Meta.Defs
Lean.Meta.instReprTransparencyMode.repr : Lean.Meta.TransparencyMode → ℕ → Std.Format
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `coeq₃ f g h`, for morphisms `f g h : j₁ ⟶ j₂`, is an arbitrary choice of object
which admits a morphism `coeq₃Hom f g h : j₂ ⟶ coeq₃ f g h` such that
`coeq₃_condition₁`, `coeq₃_condition₂` and `coeq₃_condition₃` are satisfied.
Its existence is ensured by `IsFiltered`.
 -/
CategoryTheory.IsFiltered.coeq₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsFilteredOrEmpty C] → {j₁ j₂ : C} → (j₁ ⟶ j₂) → (j₁ ⟶ j₂) → (j₁ ⟶ j₂) → C
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.lim_zero_bounded_linear_map : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F},
  IsBoundedLinearMap 𝕜 f → Filter.Tendsto f (nhds 0) (nhds 0)
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasStrictDerivAt.iterate : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {f : 𝕜 → 𝕜} {f' : 𝕜},
  HasStrictDerivAt f f' x → f x = x → ∀ (n : ℕ), HasStrictDerivAt f^[n] (f' ^ n) x
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- We say that there exists an absolute left Kan extension of `g` along `f` if any 1-morphism `h`
commutes with the left Kan extension `f⁺ g`.  -/
CategoryTheory.Bicategory.HasAbsLeftKanExtension : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b c : B} → (a ⟶ b) → (a ⟶ c) → Prop
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- Given a gcf `g = [h; (a₀, b₀), (a₁, b₁), ...]`, we have
- `squashGCF g 0 = [h + a₀ / b₀; (a₁, b₁), ...]`,
- `squashGCF g (n + 1) = ⟨g.h, squashSeq g.s n⟩`
 -/
GenContFract.squashGCF : {K : Type u_1} → [DivisionRing K] → GenContFract K → ℕ → GenContFract K
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.mkMetric_top : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X],
  (MeasureTheory.Measure.mkMetric fun x => ⊤) = ⊤
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_zero_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β),
  MeasureTheory.Measure.compProd 0 κ = 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- An induction principle for span membership. If `p` holds for all elements of `s` and is
preserved under certain affine combinations, then `p` holds for all elements of the span of `s`.  -/
affineSpan_induction : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {x : P} {s : Set P} {p : P → Prop},
  x ∈ affineSpan k s → (∀ x ∈ s, p x) → (∀ (c : k) (u v w : P), p u → p v → p w → p (c • (u -ᵥ v) +ᵥ w)) → p x
-- Mathlib.MeasureTheory.Order.Group.Lattice
Measurable.leOnePart : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Group α] [inst_2 : MeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} [MeasurableInv α] [MeasurableSup α],
  Measurable f → Measurable fun x => (f x)⁻ᵐ
-- Mathlib.Algebra.MvPolynomial.Eval
/-- If `f : S₁ →ₐ[R] S₂` is a morphism of `R`-algebras, then so is `MvPolynomial.map f`.  -/
MvPolynomial.mapAlgHom : {R : Type u} →
  {S₁ : Type v} →
    {S₂ : Type w} →
      {σ : Type u_1} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S₁] →
            [inst_2 : CommSemiring S₂] →
              [inst_3 : Algebra R S₁] →
                [inst_4 : Algebra R S₂] → (S₁ →ₐ[R] S₂) → MvPolynomial σ S₁ →ₐ[R] MvPolynomial σ S₂
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEnd.map_π : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] {G : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  (f : F ⟶ G) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.map f) (CategoryTheory.Limits.chosenEnd.π G j) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.π F j) ((f.app (Opposite.op j)).app j)
-- Mathlib.CategoryTheory.Sites.JointlySurjective
CategoryTheory.instIsStableUnderBaseChangeJointlySurjectivePrecoverage : CategoryTheory.Types.jointlySurjectivePrecoverage.IsStableUnderBaseChange
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.compare_minKey_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {he : (Std.DTreeMap.Const.modify t k f).isEmpty = false},
  cmp ((Std.DTreeMap.Const.modify t k f).minKey he) (t.minKey ⋯) = Ordering.eq
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instZero : {R : Type u_1} →
  [inst : CommRing R] →
    (S : Submonoid R) → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → Zero (FractionalIdeal S P)
-- Mathlib.AlgebraicGeometry.Restrict
/-- Given a morphism `f : X ⟶ Y` and an open set `U ⊆ Y`, we have `X ×[Y] U ≅ X |_{f ⁻¹ U}`  -/
AlgebraicGeometry.pullbackRestrictIsoRestrict : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → (U : Y.Opens) → CategoryTheory.Limits.pullback f U.ι ≅ ↑((TopologicalSpace.Opens.map f.base).obj U)
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instBot.eq_1 : ∀ {α : Type u} [inst : Group α],
  GroupTopology.instBot = { bot := { toTopologicalSpace := ⊥, toIsTopologicalGroup := ⋯ } }
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insertMax.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (r' : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl.Tree α β (r'.size + 1) → Sort u_3) (r'' : Std.DTreeMap.Internal.Impl α β)
  (hr''₁ : r''.Balanced) (hr''₂ : r''.size = r'.size + 1)
  (h_1 :
    (r'' : Std.DTreeMap.Internal.Impl α β) →
      (hr''₁ : r''.Balanced) →
        (hr''₂ : r''.size = r'.size + 1) → motive { impl := r'', balanced_impl := hr''₁, size_impl := hr''₂ }),
  (match { impl := r'', balanced_impl := hr''₁, size_impl := hr''₂ } with
    | { impl := r'', balanced_impl := hr''₁, size_impl := hr''₂ } => h_1 r'' hr''₁ hr''₂) =
    h_1 r'' hr''₁ hr''₂
-- Std.Http.Protocol.H1
/-- Returns `true` if the writer is waiting for headers of a new message.
 -/
Std.Http.Protocol.H1.Machine.isWaitingMessage : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.equivIocMod_coe : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), (QuotientAddGroup.equivIocMod hp a) ↑b = ⟨toIocMod hp a b, ⋯⟩
-- Mathlib.Analysis.Calculus.DSlope
eqOn_dslope_sub_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (a : 𝕜), Set.EqOn (dslope (fun x => (x - a) • f x) a) f {a}ᶜ
-- Lean.DocString.Markdown
/-- Applies one prefix to the first line and a different prefix to subsequent lines. Used for list items,
where the first line gets `"* "` / `"1. "` and the continuation lines get `"  "` / `"   "`.
 -/
Lean.Doc.prefixListLines : String → String → Array String → Array String
-- Lean.Server.References
/-- Updates the worker references in `self` with the `refs` of the worker managing the module `name`.
Replaces the current references with `refs` if `version` is newer than the current version managed
in `refs` and otherwise merges the reference data if `version` is equal to the current version.
 -/
Lean.Server.References.updateWorkerRefs : Lean.Server.References →
  Lean.Name → Lean.Lsp.DocumentUri → ℕ → Lean.Lsp.ModuleRefs → Lean.Lsp.Decls → IO Lean.Server.References
-- Lean.Expr
Lean.Int.mkInstHSub : Lean.Expr
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_one : ∀ {R : Type u} [inst : Semiring R] {n : ℕ}, Polynomial.coeff 1 n = if n = 0 then 1 else 0
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toContinuousLinearEquiv_refl : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E],
  ↑(LinearIsometryEquiv.refl R E) = ContinuousLinearEquiv.refl R E
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- If `f` has sum `a`, then `exp ∘ f` has product `exp a`.  -/
HasSum.cexp : ∀ {ι : Type u_1} {f : ι → ℂ} {a : ℂ}, HasSum f a → HasProd (Complex.exp ∘ f) (Complex.exp a)
-- Mathlib.Order.Filter.Lift
Filter.lift'_iInf_of_map_univ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → Filter α} {g : Set α → Set β},
  (∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t) → g Set.univ = Set.univ → (iInf f).lift' g = ⨅ i, (f i).lift' g
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.coe_toSubgroup : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {U : OpenSubgroup G}, ↑↑U = ↑U
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The induced map from the quotient by the kernel is injective.  -/
RingHom.kerLift_injective : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] (f : R →+* S), Function.Injective ⇑f.kerLift
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.isRightCancelMul : ∀ {α : Type u} [inst : Add α] [IsRightCancelAdd α], IsRightCancelMul (Multiplicative α)
-- Mathlib.Data.List.Sym
List.Sublist.sym : ∀ {α : Type u_1} (n : ℕ) {xs ys : List α}, xs.Sublist ys → (List.sym n xs).Sublist (List.sym n ys)