mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Restrict a `Trivialization` to an open set in the base.  -/
Bundle.Trivialization.restrOpen : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              Bundle.Trivialization F proj → (s : Set B) → IsOpen s → Bundle.Trivialization F proj
-- Mathlib.GroupTheory.Index
AddSubgroup.exists_nsmul_mem_of_relIndex_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G},
  H.relIndex K ≠ 0 → ∀ {a : G}, a ∈ K → ∃ n, 0 < n ∧ n ≤ H.relIndex K ∧ n • a ∈ H ⊓ K
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Real.diam_Ico : ∀ {a b : ℝ}, a ≤ b → Metric.diam (Set.Ico a b) = b - a
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_zero_iff_subsingleton : ∀ {R : Type u} [inst : Semiring R], Polynomial.Monic 0 ↔ Subsingleton R
-- Init.Data.SInt.Lemmas
Int16.toBitVec_ofIntTruncate : ∀ {n : ℤ}, Int16.minValue.toInt ≤ n → n ≤ Int16.maxValue.toInt → (Int16.ofIntClamp n).toBitVec = BitVec.ofInt 16 n
-- Mathlib.Data.FP.Basic
FP.divNatLtTwoPow : ℕ → ℕ → ℤ → Bool
-- Mathlib.Data.Set.Basic
Set.subset_empty_iff : ∀ {α : Type u} {s : Set α}, s ⊆ ∅ ↔ s = ∅
-- Mathlib.RingTheory.DedekindDomain.Factorization
IsDedekindDomain.HeightOneSpectrum.equivPrimesOver.congr_simp : ∀ {A : Type u_4} [inst : CommRing A] {p : Ideal A} [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B]
  [inst_2 : IsDedekindDomain B] [inst_3 : Algebra A B] [inst_4 : IsDomain A] [inst_5 : Module.IsTorsionFree A B]
  (hp : p ≠ 0),
  IsDedekindDomain.HeightOneSpectrum.equivPrimesOver B hp = IsDedekindDomain.HeightOneSpectrum.equivPrimesOver B hp
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E), Meromorphic f = ∀ (x : 𝕜), MeromorphicAt f x
-- Mathlib.GroupTheory.GroupAction.Hom
IsSMulRegular.of_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : SMul R M] {N : Type u_3} {F : Type u_4} [inst_1 : SMul R N]
  [inst_2 : FunLike F M N] [MulActionHomClass F R M N] (f : F) {r : R},
  Function.Injective ⇑f → IsSMulRegular N r → IsSMulRegular M r
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_coe : ∀ {M : Type u_3} [inst : AddCommMonoid M] (l : List M), (↑l).sum = l.sum
-- Mathlib.Order.Filter.Basic
Filter.isCompl_principal : ∀ {α : Type u} (s : Set α), IsCompl (Filter.principal s) (Filter.principal sᶜ)
-- Mathlib.Algebra.Module.SnakeLemma
/-- Suppose we have an exact commutative diagram
```
        K₂ -F-→ K₃
        |       |
        ι₂      ι₃
        ↓       ↓
M₁ -f₁→ M₂ -f₂→ M₃
|       |       |
i₁      i₂      i₃
↓       ↓       ↓
N₁ -g₁→ N₂ -g₂→ N₃
|
π₁
↓
C₁

```
such that `f₂` is surjective with a (set-theoretic) section `σ`, `g₁` is injective with a
(set-theoretic) retraction `ρ`, and `ι₃` is injective, then `K₂ -F→ K₃ -δ→ C₁` is exact.
 -/
SnakeLemma.exact_δ_right : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6}
  {N₃ : Type u_7} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂]
  [inst_5 : AddCommGroup M₃] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup N₂] [inst_10 : Module R N₂] [inst_11 : AddCommGroup N₃] [inst_12 : Module R N₃]
  (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃) (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃)
  (hf : Function.Exact ⇑f₁ ⇑f₂) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (hg : Function.Exact ⇑g₁ ⇑g₂)
  (h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁) (h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂) (σ : M₃ → M₂) (hσ : ⇑f₂ ∘ σ = id) (ρ : N₂ → N₁)
  (hρ : ρ ∘ ⇑g₁ = id) {K₂ : Type u_8} {K₃ : Type u_9} {C₁ : Type u_10} [inst_13 : AddCommGroup K₂]
  [inst_14 : Module R K₂] [inst_15 : AddCommGroup K₃] [inst_16 : Module R K₃] [inst_17 : AddCommGroup C₁]
  [inst_18 : Module R C₁] (ι₂ : K₂ →ₗ[R] M₂),
  Function.Exact ⇑ι₂ ⇑i₂ →
    ∀ (ι₃ : K₃ →ₗ[R] M₃) (hι₃ : Function.Exact ⇑ι₃ ⇑i₃) (π₁ : N₁ →ₗ[R] C₁) (hπ₁ : Function.Exact ⋯ ⋯) (F : ⋯), ⋯
-- Mathlib.Logic.Function.OfArity
Function.FromTypes.fromTypes_fin_const : ∀ (α β : Type u) (n : ℕ), Function.FromTypes (fun x => α) β = Function.OfArity α β n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.foldr_eq_foldr_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  {f : α → β → δ → δ} {init : δ},
  Std.DTreeMap.foldr f init t = List.foldr (fun a b => f a.1 a.2 b) init (Std.DTreeMap.Const.toList t)
-- Mathlib.CategoryTheory.Preadditive.Projective.Internal
CategoryTheory.InternallyProjective.ofRetract : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] {X Y : C} (r : CategoryTheory.Retract Y X)
  [CategoryTheory.InternallyProjective X], CategoryTheory.InternallyProjective Y
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
_private.Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints.0.discrim.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (a b c : R), discrim a b c = b ^ 2 - 4 * a * c
-- Mathlib.Tactic.Bound
Mathlib.Tactic.Bound.le_max_of_le_left_or_le_right : ∀ {α : Type} [inst : LinearOrder α] {a b c : α}, a ≤ b ∨ a ≤ c → a ≤ max b c
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.isBuiltin : Lean.Name → Bool
-- Init.Core
/-- Any two elements of a subsingleton are equal.  -/
Subsingleton.allEq : ∀ {α : Sort u} [self : Subsingleton α] (a b : α), a = b
-- Lean.Expr
/-- Given `a b : Int`, returns `a % b`  -/
Lean.mkIntMod : Lean.Expr → Lean.Expr → Lean.Expr
-- Std.Http.Data.URI.Basic
Std.Http.URI.Authority.mk : Option Std.Http.URI.UserInfo → Std.Http.URI.Host → Std.Http.URI.Port → Std.Http.URI.Authority
-- Mathlib.Analysis.Real.Pi.Bounds
Real.pi_gt_sqrtTwoAddSeries : ∀ (n : ℕ), 2 ^ (n + 1) * √(2 - Real.sqrtTwoAddSeries 0 n) < Real.pi
-- Init.Data.List.Lemmas
List.filter_congr : ∀ {α : Type u_1} {p q : α → Bool} {l : List α}, (∀ x ∈ l, p x = q x) → List.filter p l = List.filter q l
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.instVAddCommClass : ∀ {G : Type u_1} {G' : Type u_2} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup G']
  [inst_2 : AddAction G β] [inst_3 : AddAction G' β] [VAddCommClass G G' β], VAddCommClass G G' (α ↪ β)
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.Path.brecOn.go : {n : ℕ} →
  {P : MvPFunctor.{u} (n + 1)} →
    {motive : (a : P.last.M) → (a_1 : Fin2 n) → MvPFunctor.M.Path P a a_1 → Sort u_1} →
      {a : P.last.M} →
        {a_1 : Fin2 n} →
          (t : MvPFunctor.M.Path P a a_1) →
            ((a : P.last.M) →
                (a_2 : Fin2 n) → (t : MvPFunctor.M.Path P a a_2) → MvPFunctor.M.Path.below t → motive a a_2 t) →
              motive a a_1 t ×' MvPFunctor.M.Path.below t
-- Mathlib.Order.RelIso.Basic
RelEmbedding.isPreorder : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [IsPreorder β s], IsPreorder α r
-- Mathlib.Analysis.Meromorphic.Order
/-- Equivalent to `meromorphicOrderAt_deriv_eq_sub_one` with a slightly different statement so the
conclusion matches more targets  -/
meromorphicOrderAt_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜} {n : ℤ},
  ↑(n + 1) ≠ 0 → meromorphicOrderAt f x = ↑(n + 1) → meromorphicOrderAt (deriv f) x = ↑n
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.image_Ioi : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (a : α),
  ⇑e '' Set.Ioi a = Set.Ioi (e a)
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.mulComm : FirstOrder.Field.FieldAxiom
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [inst_1 : SizeOf C] (mid : C)
  (ι : X ⟶ mid) (π : mid ⟶ Y)
  (ι_π : autoParam (CategoryTheory.CategoryStruct.comp ι π = f) CategoryTheory.Factorisation.ι_π._autoParam),
  sizeOf { mid := mid, ι := ι, π := π, ι_π := ι_π } = 1 + sizeOf mid + sizeOf ι + sizeOf π + sizeOf ι_π
-- Mathlib.Topology.Category.TopCat.OpenNhds
/-- An inducing map `f : X ⟶ Y` induces a functor `OpenNhds x ⥤ OpenNhds (f x)`.  -/
Topology.IsInducing.functorNhds : {X Y : TopCat} →
  {f : X ⟶ Y} →
    Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f) →
      (x : ↑X) →
        CategoryTheory.Functor (TopologicalSpace.OpenNhds x)
          (TopologicalSpace.OpenNhds ((CategoryTheory.ConcreteCategory.hom f) x))
-- Mathlib.Topology.Constructions.SumProd
/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`.  -/
Homeomorph.prodProdProdComm : (X : Type u) →
  (Y : Type v) →
    (W : Type u_1) →
      (Z : Type u_2) →
        [inst : TopologicalSpace X] →
          [inst_1 : TopologicalSpace Y] →
            [inst_2 : TopologicalSpace Z] → [inst_3 : TopologicalSpace W] → (X × Y) × W × Z ≃ₜ (X × W) × Y × Z
-- Init.Data.BitVec.Lemmas
BitVec.udiv_zero : ∀ {n : ℕ} {x : BitVec n}, x / 0#n = 0#n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_le_maxKeyD_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β k} {fallback : α},
        (compare (t.maxKeyD fallback) ((Std.DTreeMap.Internal.Impl.insert! k v t).maxKeyD fallback)).isLE = true
-- Mathlib.Algebra.Ring.Parity
Even.sub_odd : ∀ {α : Type u_2} [inst : Ring α] {a b : α}, Even a → Odd b → Odd (a - b)
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.BoundedFormula.castLE.match_1.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x x_1 : ℕ) → x ≤ x_1 → L.BoundedFormula α x → Sort u_4)
  (_m _n : ℕ) (h : _m ≤ _n) (f : L.BoundedFormula α (_m + 1))
  (h_1 : (_m _n : ℕ) → (_h : _m ≤ _n) → motive _m _n _h FirstOrder.Language.BoundedFormula.falsum)
  (h_2 :
    (_m _n : ℕ) →
      (h : _m ≤ _n) → (t₁ t₂ : L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (_m _n : ℕ) →
      (h : _m ≤ _n) →
        (l : ℕ) →
          (R : L.Relations l) →
            (ts : Fin l → L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (_m _n : ℕ) → (h : _m ≤ _n) → (f₁ f₂ : L.BoundedFormula α _m) → motive _m _n h (f₁.imp f₂))
  (h_5 : (_m _n : ℕ) → (h : _m ≤ _n) → (f : L.BoundedFormula α (_m + 1)) → motive _m _n h f.all),
  (match _m, _n, h, f.all with
    | _m, _n, _h, FirstOrder.Language.BoundedFormula.falsum => h_1 _m _n _h
    | _m, _n, h, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 _m _n h t₁ t₂
    | _m, _n, h, FirstOrder.Language.BoundedFormula.rel R ts => h_3 _m _n h l R ts
    | _m, _n, h, f₁.imp f₂ => h_4 _m _n h f₁ f₂
    | _m, _n, h, f.all => h_5 _m _n h f) =
    h_5 _m _n h f
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraComplex.toComplex_comp_ofComplex : CliffordAlgebraComplex.toComplex.comp CliffordAlgebraComplex.ofComplex = AlgHom.id ℝ ℂ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
le_self_nsmul : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] {a : M} {n : ℕ}, 0 ≤ a → n ≠ 0 → a ≤ n • a
-- Mathlib.MeasureTheory.Covering.Differentiation
VitaliFamily.ae_tendsto_limRatioMeas : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α]
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ),
  ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ρ a / μ a) (v.filterAt x) (nhds (v.limRatioMeas hρ x))
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurable_of_Ioi : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δ → α},
  (∀ (x : α), MeasurableSet (f ⁻¹' Set.Ioi x)) → Measurable f
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.ιMapBifunctorMapObj.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K) (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂)
  [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] (i : I) (j : J) (k : K)
  (h : p (i, j) = k),
  CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k h =
    CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k h
-- Init.Data.List.Lemmas
/-- Variant of `foldr_cons_eq_append` specalized to `f = id`.  -/
List.foldr_cons_eq_append' : ∀ {β : Type u_1} {l l' : List β}, List.foldr List.cons l' l = l ++ l'
-- Mathlib.Util.Tactic
/-- `modifyMetavarDecl mvarId f` updates the `MetavarDecl` for `mvarId` with `f`.
Conditions on `f`:

- The target of `f mdecl` is defeq to the target of `mdecl`.
- The local context of `f mdecl` must contain the same fvars as the local
  context of `mdecl`. For each fvar in the local context of `f mdecl`, the type
  (and value, if any) of the fvar must be defeq to the corresponding fvar in
  the local context of `mdecl`.

If `mvarId` does not refer to a declared metavariable, nothing happens.
 -/
Mathlib.Tactic.modifyMetavarDecl : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MVarId → (Lean.MetavarDecl → Lean.MetavarDecl) → m Unit
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.Context.mk.sizeOf_spec : ∀ (indInfo : Lean.InductiveVal) (sizeOfFns : Array Lean.Name) (ctorName : Lean.Name)
  (params localInsts : Array Lean.Expr) (recMap : Lean.NameMap Lean.Name),
  sizeOf
      { indInfo := indInfo, sizeOfFns := sizeOfFns, ctorName := ctorName, params := params, localInsts := localInsts,
        recMap := recMap } =
    1 + sizeOf indInfo + sizeOf sizeOfFns + sizeOf ctorName + sizeOf params + sizeOf localInsts + sizeOf recMap
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A point in a set is in its affine span.  -/
mem_affineSpan : ∀ (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] {p : P} {s : Set P}, p ∈ s → p ∈ affineSpan k s
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term_neg : ∀ {α : Type u_1} [inst : AddCommGroup α] (n : ℤ) (x a : α) (n' : ℤ) (a' : α),
  -n = n' → -a = a' → -Mathlib.Tactic.Abel.termg n x a = Mathlib.Tactic.Abel.termg n' x a'
-- Mathlib.Topology.Connected.Clopen
/-- The connected component of a point is always a subset of the intersection of all its clopen
neighbourhoods.  -/
connectedComponent_subset_iInter_isClopen : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, connectedComponent x ⊆ ⋂ Z, ↑Z
-- Mathlib.Topology.Separation.Hausdorff
SeparatedNhds.of_singleton_finset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {x : X} {s : Finset X}, x ∉ s → SeparatedNhds {x} ↑s
-- Mathlib.CategoryTheory.Category.Preorder
/-- The category structure coming from a preorder. There is a morphism `X ⟶ Y` if and only if `X ≤ Y`.

Because we don't allow morphisms to live in `Prop`,
we have to define `X ⟶ Y` as `ULift (PLift (X ≤ Y))`.
See `CategoryTheory.homOfLE` and `CategoryTheory.leOfHom`.  -/
Preorder.smallCategory : (α : Type u) → [Preorder α] → CategoryTheory.SmallCategory α
-- Mathlib.Order.RelIso.Basic
RelHom.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : r →r s}, f = g ↔ ∀ (x : α), f x = g x
-- Mathlib.Topology.Algebra.Support
tsupport_zero : ∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X], tsupport 0 = ∅
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.pullbackAssoc_hom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)]
  {Z : C} (h : X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst f₁
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₁ f₂) h)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.lt_ceil : ∀ {r : ENNReal} {n : ℕ∞}, n < ⌈r⌉ₑ ↔ ↑n < r
-- Mathlib.Data.Part
Part.instInhabited : {α : Type u_1} → Inhabited (Part α)
-- Mathlib.Condensed.Explicit
/-- A `CondensedSet` version of `Condensed.ofSheafCompHaus`.  -/
CondensedSet.ofSheafCompHaus : (F : CategoryTheory.Functor CompHausᵒᵖ (Type (u + 1))) →
  [CategoryTheory.Limits.PreservesFiniteProducts F] → CategoryTheory.regularTopology.EqualizerCondition F → CondensedSet
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_eq_setToFun_transpose : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {f : X → E},
  μ.Integrable f → ∫ᵛ (x : X), f x ∂[B; μ] = MeasureTheory.setToFun (μ.transpose B).variation ⇑(μ.transpose B) ⋯ f
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Ici_add_Ici_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [inst_2 : DecidableEq α] [AddLeftMono α] [AddRightMono α]
  [inst_5 : LocallyFiniteOrderTop α] (a b : α), Finset.Ici a + Finset.Ici b ⊆ Finset.Ici (a + b)
-- Mathlib.Data.Sum.Order
Sum.instReflLex_mathlib : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Refl r] [Std.Refl s], Std.Refl (Sum.Lex r s)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.exists_isCompact_not_null : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegular], (∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0
-- Mathlib.Analysis.Distribution.DerivNotation
/-- The line derivative is continuous.
 -/
ContinuousLineDeriv : (V : Type u) →
  (E : Type v) → (F : outParam (Type w)) → [TopologicalSpace E] → [TopologicalSpace F] → [LineDeriv V E F] → Prop
-- Init.Data.UInt.Lemmas
instAssociativeUSizeHMul : Std.Associative fun x1 x2 => x1 * x2
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.divConst_inv_right : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G), A.divConst B⁻¹ = A.mulConst B
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.mk.inj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' : Φ.LeftResolution X₂} {f : L.X₁ ⟶ L'.X₁}
  {comm :
    autoParam (CategoryTheory.CategoryStruct.comp (Φ.functor.map f) L'.w = L.w)
      CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comm._autoParam}
  {f_1 : L.X₁ ⟶ L'.X₁}
  {comm_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (Φ.functor.map f_1) L'.w = L.w)
      CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comm._autoParam},
  { f := f, comm := comm } = { f := f_1, comm := comm_1 } → f = f_1
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.mk'_s : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x : ↥X) (y : ↥Y) (h : f x = g y),
  (AlgebraicGeometry.Scheme.Pullback.Triplet.mk' x y h).s = g y
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.congr_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  {Φ₁ Φ₂ : S₁ ⟶ S₂}, Φ₁ = Φ₂ → ∀ (n : ℕ), Φ₁.f n = Φ₂.f n
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.instInhabitedOLeanEntry : Inhabited Lean.Parser.ParserExtension.OLeanEntry
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_ne_zero_iff_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {a p : α},
  a ≠ 0 → Irreducible p → ((Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ p ∣ a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.smul_fin3 : ∀ {R : Type r} [inst : CommRing R] (P : Fin 3 → R) (u : R), u • P = ![u ^ 2 * P 0, u ^ 3 * P 1, u * P 2]
-- Mathlib.Tactic.FunProp.Theorems
/-- Extension storing all function theorems.  -/
Mathlib.Meta.FunProp.functionTheoremsExt : Mathlib.Meta.FunProp.FunctionTheoremsExt
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.EditableDocument.toEditableDocumentCore : Lean.Server.FileWorker.EditableDocument → Lean.Server.FileWorker.EditableDocumentCore
-- Mathlib.MeasureTheory.Measure.Regular
/-- See also `IsCompact.measure_closure` for a version
that assumes the `σ`-algebra to be the Borel `σ`-algebra but makes no assumptions on `μ`.  -/
MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [R1Space α]
  [μ.OuterRegular] {k : Set α}, IsCompact k → μ (closure k) = μ k
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.coe_listProd : ∀ {ι : Type u_1} {S : Type u_2} [inst : Add S] [inst_1 : Monoid S] (t : RingCon S) (l : List ι) (f : ι → S),
  ↑(List.map f l).prod = (List.map (fun i => ↑(f i)) l).prod
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
/-- `SeparationQuotient.mk` as a `RingHom`.  -/
SeparationQuotient.mkRingHom : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonAssocSemiring R] → [inst_2 : IsTopologicalSemiring R] → R →+* SeparationQuotient R
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.lipschitz_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {s : Set E} {c : NNReal}, ApproximatesLinearOn f f' s c → LipschitzWith c fun x => f ↑x - f' ↑x
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.cuspFunction_smul : ∀ {h : ℝ} {f : ℂ → ℂ},
  ContinuousAt (Function.Periodic.cuspFunction h f) 0 →
    ∀ (a : ℂ), Function.Periodic.cuspFunction h (a • f) = a • Function.Periodic.cuspFunction h f
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Coevaluation of an exact pairing.  -/
CategoryTheory.ExactPairing.coevaluation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        [CategoryTheory.ExactPairing X Y] →
          CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for negation of `BitVec`s.  -/
BitVec.reduceNeg : Lean.Meta.Simp.DSimproc