mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.Hom.ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C}
  (α β : X.Hom Y) (w : α.base = β.base),
  CategoryTheory.CategoryStruct.comp α.c (CategoryTheory.Functor.whiskerRight (CategoryTheory.eqToHom ⋯) X.presheaf) =
      β.c →
    α = β
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l →
          ∀ {h : k' ∈ Std.DHashMap.Const.ofList l}, Std.DHashMap.Const.get (Std.DHashMap.Const.ofList l) k' h = v
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.bicone_ι_π_ne_assoc : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) {j j' : J},
  j ≠ j' →
    ∀ {Z : C} (h : F j' ⟶ Z),
      CategoryTheory.CategoryStruct.comp (B.ι j) (CategoryTheory.CategoryStruct.comp (B.π j') h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RingTheory.Congruence.Hom
/-- This version infers the surjectivity of the function from a RingEquiv function  -/
RingCon.comapQuotientEquivOfSurj_symm_mk' : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] (c : RingCon M) (f : N ≃+* M)
  {d : RingCon N} (hcd : d = c.comap f) (x : N), (c.comapQuotientEquivOfSurj ↑f ⋯ hcd).symm ⟦f x⟧ = ↑x
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} {I : CategoryTheory.InjectiveResolution Z} {Z' : C}
  {I' : CategoryTheory.InjectiveResolution Z'} {f : Z ⟶ Z'} (self : I.Hom I' f),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (self.hom.f 0) =
    CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0) (I'.ι.f 0)
-- Mathlib.Topology.MetricSpace.Closeds
/-- In an emetric space, the type of compact subsets is an emetric space,
where the edistance is the Hausdorff edistance  -/
TopologicalSpace.Compacts.instEMetricSpace : {α : Type u_1} → [inst : EMetricSpace α] → EMetricSpace (TopologicalSpace.Compacts α)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mk_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y), (CategoryTheory.Under.mk f).right = Y
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.comul_pow : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (a : A) (n : ℕ),
  CoalgebraStruct.comul (a ^ n) = CoalgebraStruct.comul a ^ n
-- Mathlib.Algebra.Ring.Ext
AddGroupWithOne.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : AddGroupWithOne R⦄, HAdd.hAdd = HAdd.hAdd → One.one = One.one → inst₁ = inst₂
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.vadd_right_cancel_iff : ∀ {x y : ℝ} (z : UpperHalfPlane), x +ᵥ z = y +ᵥ z ↔ x = y
-- Mathlib.Order.Interval.Set.Fin
Fin.range_natAdd_eq_Ioi : ∀ (m n : ℕ) [inst : NeZero m], Set.range (Fin.natAdd m) = Set.Ioi (Fin.castAdd n ⊤)
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.mk : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E],
  Topology.IsQuotientMap f →
    ContinuousConstVAdd G E →
      (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) →
        (∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun x => g +ᵥ x) '' U ∩ U).Nonempty → g = 0) →
          IsAddQuotientCoveringMap f G
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] [inst_1 : CategoryTheory.Abelian C] {ι' : Type u_3}
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ →
    ∀ (i₀ i₁ i₂ : ι') (h₀₁ : i₀ ≤ i₁) (h₁₂ : i₁ ≤ i₂),
      CategoryTheory.Limits.IsZero ((X'.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE h₀₁))) →
        CategoryTheory.Limits.IsZero
            ((X'.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE h₀₁))) →
          CategoryTheory.IsIso ((X'.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.toPrefunctor_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E), F.toPrefunctor ⋙q G.toPrefunctor = (F.comp G).toPrefunctor
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_eval_one : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), Polynomial.eval 1 p.mirror = Polynomial.eval 1 p
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_le_max : ∀ (a b : Cardinal.{u_1}), a + b ≤ max (max a b) Cardinal.aleph0
-- Mathlib.Data.QPF.Multivariate.Constructions.Const
/-- Constant multivariate functor  -/
MvQPF.Const : (n : ℕ) → Type u_1 → TypeVec.{u} n → Type u_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_alter_eq_sub_one : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∈ m → (f m[k]?).isNone = true → (m.alter k f).size = m.size - 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} {l : List α} {k : α} {fallback : Unit},
  Std.DHashMap.Const.getD (Std.DHashMap.Const.insertManyIfNewUnit m l) k fallback = ()
-- Mathlib.Analysis.Complex.Convex
convex_halfSpace_im_ge : ∀ (r : ℝ), Convex ℝ {c | r ≤ c.im}
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.getElem_toArray_eq : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α] {i : ℕ} {h : i < r.toArray.size},
  r.toArray[i] = (Std.PRange.least?.bind (Std.PRange.succMany? i)).get ⋯
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentBundleModelSpaceHomeomorph_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H},
  ⇑(tangentBundleModelSpaceHomeomorph I) = ⇑(Bundle.TotalSpace.toProd H E)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The weights for the centroid of some vertices of a simplex, in
terms of `pointsWithCircumcenter`.  -/
Affine.Simplex.centroidWeightsWithCircumcenter : {n : ℕ} → Finset (Fin (n + 1)) → Affine.Simplex.PointsWithCircumcenterIndex n → ℝ
-- Mathlib.Data.Finsupp.Defs
Finsupp.ofSupportFinite.congr_simp : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (f f_1 : α → M) (e_f : f = f_1) (hf : (Function.support f).Finite),
  Finsupp.ofSupportFinite f hf = Finsupp.ofSupportFinite f_1 ⋯
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Restrict a `PartialEquiv` to a pair of corresponding sets.  -/
PartialEquiv.IsImage.restr : {α : Type u_1} → {β : Type u_2} → {e : PartialEquiv α β} → {s : Set α} → {t : Set β} → e.IsImage s t → PartialEquiv α β
-- Mathlib.Analysis.Calculus.Deriv.Abs
differentiableWithinAt_abs : ∀ (s : Set ℝ) {x : ℝ}, x ≠ 0 → DifferentiableWithinAt ℝ (fun x => |x|) s x
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (S : CategoryTheory.SplitEpi f.hom) (n : ℕ) (i : Fin (n + 1)) {Z : C} (h : f.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i.succ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i) h
-- Mathlib.Algebra.BigOperators.Fin
_private.Mathlib.Algebra.BigOperators.Fin.0.List.alternatingSum.match_1.eq_2 : ∀ {G : Type u_1} (motive : List G → Sort u_2) (g : G) (h_1 : Unit → motive []) (h_2 : (g : G) → motive [g])
  (h_3 : (g h : G) → (t : List G) → motive (g :: h :: t)),
  (match [g] with
    | [] => h_1 ()
    | [g] => h_2 g
    | g :: h :: t => h_3 g h t) =
    h_2 g
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- The Fourier integral of the `n`-th derivative of a function is obtained by multiplying the
Fourier integral of the original function by `(2πI L w ⬝ )^n`.  -/
VectorFourier.fourierIntegral_iteratedFDeriv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V]
  {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {N : ℕ∞},
  ContDiff ℝ (↑N) f →
    (∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (iteratedFDeriv ℝ n f) μ) →
      ∀ {n : ℕ},
        ↑n ≤ N →
          VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L)
              (iteratedFDeriv ℝ n f) =
            fun w =>
            VectorFourier.fourierPowSMulRight (-L.flip)
              (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w n
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.const_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}
  {R : Type u_5} [inst_5 : Semiring R] [inst_6 : Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F],
  DiffContOnCl 𝕜 f s → ∀ (c : R), DiffContOnCl 𝕜 (c • f) s
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.ofLimitCone_pt : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C}
  {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t),
  (CategoryTheory.Limits.Bicone.ofLimitCone ht).pt = t.pt
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_tsum : ∀ {ι : Type u_1} {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} [CompleteSpace E] [Countable ι] {f : ι → X → E},
  (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ.variation) →
    ∑' (i : ι), ∫⁻ (a : X), ‖f i a‖ₑ ∂μ.variation ≠ ⊤ →
      ∫ᵛ (a : X), ∑' (i : ι), f i a ∂[B; μ] = ∑' (i : ι), ∫ᵛ (a : X), f i a ∂[B; μ]
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.nonneg_addConst : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A B : Finset G},
  A.Nonempty → B.Nonempty → 1 ≤ A.addConst B
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the composition `η ≪≫ θ`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.comp₂M : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
    Mathlib.Tactic.BicategoryLike.Mor₂Iso →
      Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Lean.Structure
/-- Gets the `StructureInfo` if `structName` has been declared as a structure to the elaborator.  -/
Lean.getStructureInfo? : Lean.Environment → Lean.Name → Option Lean.StructureInfo
-- Mathlib.RingTheory.TensorProduct.Basic
LinearMap.mulRight_tmul : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : SMulCommClass R A A]
  [inst_6 : SMulCommClass R B B] [inst_7 : IsScalarTower R A A] [inst_8 : IsScalarTower R B B] (a : A) (b : B),
  LinearMap.mulRight R (a ⊗ₜ[R] b) = TensorProduct.map (LinearMap.mulRight R a) (LinearMap.mulRight R b)
-- Mathlib.Topology.Category.Compactum
Compactum.instTopologicalSpaceA : {X : Compactum} → TopologicalSpace X.A
-- Mathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus
/-- The natural transformation that is part of the data of
the right derived functor `DerivedCategory.Plus C ⥤ DerivedCategory.Plus D`
when `F : C ⥤ D` is an additive functor between abelian categories and
`C` has enough injectives.  -/
CategoryTheory.Functor.rightDerivedFunctorPlusUnit : {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] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.Abelian D] →
            [inst_4 : HasDerivedCategory C] →
              [inst_5 : HasDerivedCategory D] →
                (F : CategoryTheory.Functor C D) →
                  [inst_6 : F.Additive] →
                    [inst_7 : CategoryTheory.EnoughInjectives C] →
                      F.mapHomotopyCategoryPlus.comp DerivedCategory.Plus.Qh ⟶
                        DerivedCategory.Plus.Qh.comp F.rightDerivedFunctorPlus
-- Init.Data.Int.Gcd
Int.gcd_ediv_gcd_ediv_gcd : ∀ {i j : ℤ}, 0 < i.gcd j → (i / ↑(i.gcd j)).gcd (j / ↑(i.gcd j)) = 1
-- Init.Data.Vector.Basic
instReprVector.repr : {α : Type u_1} → {n : ℕ} → [Repr α] → Vector α n → ℕ → Std.Format
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.add_measure : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.HasFiniteIntegral f ν → MeasureTheory.HasFiniteIntegral f (μ + ν)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.coe_top : ∀ {α : Type u_2} [inst : TopologicalSpace α], ↑⊤ = Set.univ
-- Mathlib.Topology.Algebra.Group.Basic
/-- Given two compact sets in a noncompact topological group, there is a translate of the second
one that is disjoint from the first one.  -/
exists_disjoint_smul_of_isCompact : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [NoncompactSpace G] {K L : Set G},
  IsCompact K → IsCompact L → ∃ g, Disjoint K (g • L)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_inv_naturality_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X X' : C}
  (f : X ⟶ X') (Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
      (CategoryTheory.MonoidalCategoryStruct.associator X' Y Z).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) Z)
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Bornology α] [inst_1 : Bornology β]
  [inst_2 : Bornology γ] [inst_3 : Bornology δ] (f : LocallyBoundedMap γ δ) (g : LocallyBoundedMap β γ)
  (h : LocallyBoundedMap α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.mutuallySingularSetSlice.congr_simp : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ κ_1 : ProbabilityTheory.Kernel α γ),
  κ = κ_1 →
    ∀ (η η_1 : ProbabilityTheory.Kernel α γ),
      η = η_1 →
        ∀ (a a_1 : α),
          a = a_1 →
            ∀ (a_2 a_3 : γ), a_2 = a_3 → κ.mutuallySingularSetSlice η a a_2 = κ_1.mutuallySingularSetSlice η_1 a_1 a_3
-- Mathlib.RingTheory.Regular.Category
ModuleCat.smulShortComplex_f_eq_smul_id : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) (r : R),
  (M.smulShortComplex r).f = r • CategoryTheory.CategoryStruct.id M
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstr.mk.injEq : ∀ (p : Lean.Grind.CommRing.Poly) (h : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof) (sugar id : ℕ)
  (p_1 : Lean.Grind.CommRing.Poly) (h_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof) (sugar_1 id_1 : ℕ),
  ({ p := p, h := h, sugar := sugar, id := id } = { p := p_1, h := h_1, sugar := sugar_1, id := id_1 }) =
    (p = p_1 ∧ h = h_1 ∧ sugar = sugar_1 ∧ id = id_1)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq.eq_def : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (i : Set α) (x : ℕ),
  MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i x =
    match x with
    | 0 => MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s (i \ ∅)
    | n.succ =>
      MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s
        (i \
          ⋃ k,
            ⋃ (H : k ≤ n),
              have this := ⋯;
              MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i k)
-- Mathlib.Logic.Unique
Unique.eq_default : ∀ {α : Sort u_1} [inst : Unique α] (a : α), a = default
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.instReprEvent : {dir : Std.Http.Protocol.H1.Direction} → Repr (Std.Http.Protocol.H1.Event dir)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_app : ∀ {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'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (x : A),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom.app x)
      (F'.map (α.left.app x)) =
    CategoryTheory.CategoryStruct.comp (α.base.app (F.obj x))
      ((CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom.app x)
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_add : ∀ (a b : BitVec 64), Int64.ofBitVec (a + b) = Int64.ofBitVec a + Int64.ofBitVec b
-- Std.Data.TreeMap.Basic
/-- Transforms a list of keys into a tree map.  -/
Std.TreeMap.unitOfList : {α : Type u} → List α → (cmp : autoParam (α → α → Ordering) Std.TreeMap.unitOfList._auto_1) → Std.TreeMap α Unit cmp
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.map_comp : ∀ {k : Type u} {G H K : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] [inst_8 : Group K] [inst_9 : TopologicalSpace K] [inst_10 : IsTopologicalGroup K]
  {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y)
  (g : TopRep.res (↑ψ) Y ⟶ Z) (n : ℕ),
  ContinuousCohomology.map (φ.comp ψ) (CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑ψ).map f) g) n =
    CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map φ f n) (ContinuousCohomology.map ψ g n)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rootSet_one : ∀ {T : Type w} [inst : CommRing T] (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S],
  Polynomial.rootSet 1 S = ∅
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.Indep.indicator_const_indepFun : ∀ {α : Type u_1} {Ω : Type u_2} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {m : MeasurableSpace Ω} {M : Type u_8} {𝓧 : Type u_9} [inst : Zero M]
  [inst_1 : MeasurableSpace M] (c : M) {m𝓧 : MeasurableSpace 𝓧} {A : Set Ω} {X : Ω → 𝓧},
  MeasurableSet A →
    ProbabilityTheory.Kernel.Indep m (MeasurableSpace.comap X m𝓧) κ μ →
      ProbabilityTheory.Kernel.IndepFun (A.indicator fun x => c) X κ μ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is `C^1` on `[a, b]`,
then `∫ y in a..b, derivWithin f (uIcc a b) y` equals `f b - f a`.  -/
intervalIntegral.integral_derivWithin_uIcc_of_contDiffOn_uIcc : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E],
  ContDiffOn ℝ 1 f (Set.uIcc a b) → ∫ (x : ℝ) in a..b, derivWithin f (Set.uIcc a b) x = f b - f a
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.oppositeShiftFunctorAdd'_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A) (a b c : A) (h : a + b = c),
  (CategoryTheory.shiftFunctorAdd' (CategoryTheory.OppositeShift C A) a b c h).hom.app X =
    ((CategoryTheory.shiftFunctorAdd' C a b c h).inv.app (Opposite.unop X)).op
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.smul_fixedBy : ∀ (α : Type u_1) {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g h : G),
  h • MulAction.fixedBy α g = MulAction.fixedBy α (h * g * h⁻¹)
-- Mathlib.CategoryTheory.Simple
CategoryTheory.mono_to_simple_zero_of_not_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  [CategoryTheory.Simple Y] {f : X ⟶ Y} [CategoryTheory.Mono f], (CategoryTheory.IsIso f → False) → f = 0
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.inverse_inverse : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂}, f.IsInvertible → f.inverse.inverse = f
-- Lean.Meta.CoeAttr
Lean.Meta.CoeFnType.ofNat_ctorIdx : ∀ (x : Lean.Meta.CoeFnType), Lean.Meta.CoeFnType.ofNat x.ctorIdx = x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLT.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (x : Std.DTreeMap.Internal.Impl α β)
  (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.getKeyLT k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      if hkky : compare k ky = Ordering.gt then Std.DTreeMap.Internal.Impl.getKeyLTD k r ky
      else Std.DTreeMap.Internal.Impl.getKeyLT k l ⋯ ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivWithinAt.snd : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G},
  HasFDerivWithinAt f₂ f₂' s x → HasFDerivWithinAt (fun x => (f₂ x).2) (ContinuousLinearMap.snd 𝕜 F G ∘SL f₂') s x