mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousLinearMap.norm_map_tail_le : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G)
  (m : (i : Fin n.succ) → Ei i), ‖(f (m 0)) (Fin.tail m)‖ ≤ ‖f‖ * ∏ i, ‖m i‖
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_eq_get_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {he : t.isEmpty = false}, t.minKey he = t.minKey?.get ⋯
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.InheritedFromSource.of_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  (Q Q' : CategoryTheory.MorphismProperty C), Q ≤ Q' → ∀ [P.InheritedFromSource Q'], P.InheritedFromSource Q
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.gc_saturation : ∀ (M : Type u_1) [inst : AddZeroClass M], GaloisConnection AddSubmonoid.saturation fun x => x.toAddSubmonoid
-- Init.Data.Vector.Attach
Vector.pmap_attachWith : ∀ {α : Type u_1} {n : ℕ} {q : α → Prop} {β : Type u_2} {xs : Vector α n} {p : { x // q x } → Prop}
  {f : (a : { x // q x }) → p a → β} (H₁ : ∀ x ∈ xs, q x) (H₂ : ∀ a ∈ xs.attachWith q H₁, p a),
  Vector.pmap f (xs.attachWith q H₁) H₂ = Vector.pmap (fun a h => f ⟨a, ⋯⟩ ⋯) xs ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {l : List ((a : α) × β a)} {k a : α}
  {v : β k},
  Std.Internal.List.getKey! a (Std.Internal.List.insertEntry k v l) =
    if (k == a) = true then k else Std.Internal.List.getKey! a l
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.tensorProdObjIsoPushoutObj.eq_1 : ∀ {R : CommRingCat} (S : CommRingCat) [inst : Algebra ↑R ↑S] (A : CategoryTheory.Under R),
  CommRingCat.tensorProdObjIsoPushoutObj S A = CategoryTheory.Under.isoMk ⋯.isoPushout ⋯
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_eq_floor_add_one_iff_notMem : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ Set.range Int.cast
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'.congr_simp : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (i j k : A) (h : i + j = k),
  CategoryTheory.shiftFunctorAdd' C i j k h = CategoryTheory.shiftFunctorAdd' C i j k h
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.equiv_iff_forall_mem_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α},
  m₁.WF → m₂.WF → ∀ [LawfulBEq α], m₁.Equiv m₂ ↔ ∀ (k : α), k ∈ m₁ ↔ k ∈ m₂
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.presheafFiberDesc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {T : A}
  (φ φ_1 : (X : C) → Φ.fiber.obj X → (P.obj (Opposite.op X) ⟶ T)) (e_φ : φ = φ_1)
  (hφ :
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X),
      CategoryTheory.CategoryStruct.comp (P.map f.op) (φ X x) =
        φ Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x)),
  Φ.presheafFiberDesc φ hφ = Φ.presheafFiberDesc φ_1 ⋯
-- Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
BoxIntegral.Box.iUnion_coe_splitCenterBox : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), ⋃ s, ↑(I.splitCenterBox s) = ↑I
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.cons₂.inj : ∀ {a : List ℕ} {a_1 : Turing.ToPartrec.Cont} {a_2 : List ℕ} {a_3 : Turing.ToPartrec.Cont},
  Turing.ToPartrec.Cont.cons₂ a a_1 = Turing.ToPartrec.Cont.cons₂ a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Lean.Meta.Sym.LooseBVarsS
/-- Lowers the loose bound variables `>= s` in `e` by `d`.
That is, a loose bound variable `bvar i` with `i >= s` is mapped to `bvar (i-d)`.
It assumes the input is maximally shared, and ensures the output is too.
Remark: if `s < d`, then the result is `e`.
 -/
Lean.Meta.Sym.lowerLooseBVarsS : Lean.Expr → ℕ → ℕ → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_neg₄ : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a b c d : ℤ),
  IsEllipticNet.atomRel W a b c (-d) = IsEllipticNet.atomRel W a b c d
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.aestronglyMeasurable' : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b → MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc b a))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constEntryAtIdxD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {i : ℕ} {fallback : α × β},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.entryAtIdxD t₁ i fallback = Std.DTreeMap.Raw.Const.entryAtIdxD t₂ i fallback
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.mgf_id_gaussianReal : ∀ {μ : ℝ} {v : NNReal},
  ProbabilityTheory.mgf id (ProbabilityTheory.gaussianReal μ v) = fun t => Real.exp (μ * t + ↑v * t ^ 2 / 2)
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The top right map in the associativity hexagon.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          (F : CategoryTheory.Functor C D) →
            CategoryTheory.MonoidalCategory.curriedTensorPrePre F ⟶
              CategoryTheory.MonoidalCategory.curriedTensorPrePre' F
-- Mathlib.Data.Nat.Fib.Basic
/-- See https://proofwiki.org/wiki/Fibonacci_Number_in_terms_of_Smaller_Fibonacci_Numbers  -/
Nat.fib_add : ∀ (m n : ℕ), Nat.fib (m + n + 1) = Nat.fib m * Nat.fib n + Nat.fib (m + 1) * Nat.fib (n + 1)
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- `(M × N) × N'` is diffeomorphic to `M × (N × N')`.  -/
Diffeomorph.prodAssoc : {𝕜 : 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] →
                        {G' : Type u_8} →
                          [inst_7 : TopologicalSpace G'] →
                            (I : ModelWithCorners 𝕜 E H) →
                              (J : ModelWithCorners 𝕜 F G) →
                                (J' : ModelWithCorners 𝕜 F G') →
                                  (M : Type u_9) →
                                    [inst_8 : TopologicalSpace M] →
                                      [inst_9 : ChartedSpace H M] →
                                        (N : Type u_11) →
                                          [inst_10 : TopologicalSpace N] →
                                            [inst_11 : ChartedSpace G N] →
                                              (N' : Type u_12) →
                                                [inst_12 : TopologicalSpace N'] →
                                                  [inst_13 : ChartedSpace G' N'] →
                                                    (n : WithTop ℕ∞) →
                                                      Diffeomorph ((I.prod J).prod J') (I.prod (J.prod J'))
                                                        ((M × N) × N') (M × N × N') n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.Hom.ext : ∀ {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}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} {x_1 y_1 : x.Hom y},
  x_1.fst = y_1.fst → x_1.snd = y_1.snd → x_1 = y_1
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.egirth_anti : ∀ {α : Type u_1}, Antitone SimpleGraph.egirth
-- Init.Grind.Ring.Envelope
_private.Init.Grind.Ring.Envelope.0.Lean.Grind.Ring.OfSemiring.exists_true : ∀ (α : Type u) [Lean.Grind.Semiring α], ∃ x, True
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sub_coe_pi_eq_add_coe_pi : ∀ (θ : Real.Angle), θ - ↑Real.pi = θ + ↑Real.pi
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.lift.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x x_1 : R) (e_x : x = x_1) [inst_4 : IsLocalization.Away x S] {g g_1 : R →+* P}
  (e_g : g = g_1) (hg : IsUnit (g x)), IsLocalization.Away.lift x hg = IsLocalization.Away.lift x_1 ⋯
-- Lean.Data.Lsp.Extra
/-- `meta` flag was not set on this import.  -/
Lean.Lsp.LeanImportMetaKind.nonMeta : Lean.Lsp.LeanImportMetaKind
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeFppfPrecoverage : AlgebraicGeometry.Scheme.fppfPrecoverage.IsStableUnderBaseChange
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.subtypeRestr_def : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s),
  e.subtypeRestr hs = (s.openPartialHomeomorphSubtypeCoe hs).trans e
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- A monoid is isomorphic to the opposite of its opposite.  -/
MulEquiv.opOp : (M : Type u_3) → [inst : Mul M] → M ≃* Mᵐᵒᵖᵐᵒᵖ
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit'.match_1.eq_1 : ∀ (motive : Lean.Name → Sort u_1) (pre : Lean.Name) (str : String)
  (h_1 : (pre : Lean.Name) → (str : String) → motive (pre.str str)) (h_2 : (x : Lean.Name) → motive x),
  (match pre.str str with
    | pre.str str => h_1 pre str
    | x => h_2 x) =
    h_1 pre str
-- Mathlib.Algebra.Algebra.Unitization
Unitization.mk_injective : ∀ {R : Type u_1} {A : Type u_2}, Function.Injective Unitization.mk
-- Init.Data.Int.Gcd
Int.gcd_add_self_right : ∀ (m n : ℤ), m.gcd (n + m) = m.gcd n
-- Mathlib.Data.Complex.Basic
Complex.range_re : Set.range Complex.re = Set.univ
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.succ : Nat.Primrec Nat.succ
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.piecewise_single_erase : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (x : Π₀ (i : ι), β i) (i : ι),
  (fun₀ | i => x i).piecewise (DFinsupp.erase i x) {i} = x
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.pmul_zeta : ∀ {R : Type u_1} [inst : NonAssocSemiring R] (f : ArithmeticFunction R), f.pmul ↑ArithmeticFunction.zeta = f
-- Mathlib.Order.KrullDimension
Order.krullDim_of_noMaxOrder : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] [NoMaxOrder α], Order.krullDim α = ⊤
-- Mathlib.Data.ENat.Basic
ENat.le_lift_iff : ∀ {x : ℕ} {n : ℕ∞} {h : n < ⊤}, x ≤ n.lift h ↔ ↑x ≤ n
-- Mathlib.Data.Subtype
Subtype.coind_injective_iff : ∀ {α : Sort u_4} {β : Sort u_5} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)),
  Function.Injective (Subtype.coind f h) ↔ Function.Injective f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.copy_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w u' w' : V} (h : G.Adj u v) (p : G.Walk v w) (hu : u = u') (hw : w = w'),
  (SimpleGraph.Walk.cons h p).copy hu hw = SimpleGraph.Walk.cons ⋯ (p.copy ⋯ hw)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.to_basicOpen_epi : ∀ (R : Type u) [inst : CommRing R] (r : R),
  CategoryTheory.Epi
    (CommRingCat.ofHom
      (algebraMap R ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen r)))))
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedMapOfIsTriangulatedOfFull : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] {D : Type u_4}
  [inst_7 : CategoryTheory.Category.{u_5, u_4} D] [inst_8 : CategoryTheory.Limits.HasZeroObject D]
  [inst_9 : CategoryTheory.Preadditive D] [inst_10 : CategoryTheory.HasShift D ℤ]
  [inst_11 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_12 : CategoryTheory.Pretriangulated D]
  (F : CategoryTheory.Functor C D) [inst_13 : F.CommShift ℤ] [F.IsTriangulated] [F.Full], (P.map F).IsTriangulated
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinAt.neg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E},
  HasFPowerSeriesWithinAt f pf s x → HasFPowerSeriesWithinAt (-f) (-pf) s x
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_natAbs_neg : ∀ {n : ℤ} {a : ℕ}, Mathlib.Meta.NormNum.IsInt n (Int.negOfNat a) → Mathlib.Meta.NormNum.IsNat n.natAbs a
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instIsCentralScalar : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  {R : Type u_5} [inst_3 : Zero R] [inst_4 : SMulWithZero R β] [inst_5 : SMulWithZero Rᵐᵒᵖ β]
  [inst_6 : ContinuousConstSMul R β] [inst_7 : IsCentralScalar R β],
  IsCentralScalar R (CompactlySupportedContinuousMap α β)
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- An isomorphism gives rise to a copy.  -/
SimpleGraph.Iso.toCopy : {α : Type u_4} → {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → A ≃g B → A.Copy B
-- Mathlib.Order.Filter.Map
Filter.preimage_mem_comap : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} {t : Set β}, t ∈ g → m ⁻¹' t ∈ Filter.comap m g
-- Init.Prelude
/-- Internal representation of `Void` in the compiler.  -/
lcVoid : Type
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.parseFirstByte.fun_cases_unfolding : ∀ (b : UInt8) (motive : ByteArray.utf8DecodeChar?.FirstByte → Prop),
  ((b &&& 128 == 0) = true → motive ByteArray.utf8DecodeChar?.FirstByte.done) →
    (¬(b &&& 128 == 0) = true → (b &&& 224 == 192) = true → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore) →
      (¬(b &&& 128 == 0) = true →
          ¬(b &&& 224 == 192) = true → (b &&& 240 == 224) = true → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore) →
        (¬(b &&& 128 == 0) = true →
            ¬(b &&& 224 == 192) = true →
              ¬(b &&& 240 == 224) = true →
                (b &&& 248 == 240) = true → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore) →
          (¬(b &&& 128 == 0) = true →
              ¬(b &&& 224 == 192) = true →
                ¬(b &&& 240 == 224) = true →
                  ¬(b &&& 248 == 240) = true → motive ByteArray.utf8DecodeChar?.FirstByte.invalid) →
            motive (ByteArray.utf8DecodeChar?.parseFirstByte b)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- `∏ᵖ p ∣ n, f p` is custom notation for `prodPrimeFactors f n`  -/
ArithmeticFunction.bigproddvd : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
/-- A set function is `FinMeasAdditive` if its value on the union of two disjoint measurable
sets with finite measure is the sum of its values on each set.  -/
MeasureTheory.FinMeasAdditive : {α : Type u_1} → {β : Type u_7} → [AddMonoid β] → {x : MeasurableSpace α} → MeasureTheory.Measure α → (Set α → β) → Prop
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instMin : (M : Type u_1) → [inst : AddZeroClass M] → Min (SaturatedAddSubmonoid M)
-- Lean.Level
Lean.Level.imax : Lean.Level → Lean.Level → Lean.Level
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.min?_eq_toList_head? : ∀ {α : Type u_1} {t : RBTree.RBNode α}, t.min? = t.toList.head?
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.ι_obj_fiber : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮)
  (a : ↑(F.obj { as := Opposite.op S })), ((CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).obj a).fiber = a
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- The "reproducing" property of the kernel.  -/
RKHS.kernel_inner : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (x y : X) (v w : V),
  inner 𝕜 ((RKHS.kernel H x y) v) w = inner 𝕜 ((RKHS.kerFun H y) v) ((RKHS.kerFun H x) w)
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.below.succ : ∀ {O : Set (ℕ →. ℕ)} {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop}, Nat.RecursiveIn.below ⋯
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.nsmul_inter_nsmul_covByVAdd_sq_inter_sq : ∀ {G : Type u_1} [inst : AddGroup G] {A B : Set G} {K L : ℝ} {m n : ℕ},
  IsApproximateAddSubgroup K A →
    IsApproximateAddSubgroup L B →
      2 ≤ m → 2 ≤ n → CovByVAdd G (K ^ (m - 1) * L ^ (n - 1)) (m • A ∩ n • B) (2 • A ∩ 2 • B)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_fst_comp_snd_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z),
  CategoryTheory.CartesianMonoidalCategory.lift
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst W Y) g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd W Y) g') =
    CategoryTheory.MonoidalCategoryStruct.tensorHom g g'
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.disjoint_interior_base_iUnion_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [inst : Topology.RelCWComplex C D],
  Disjoint (interior D) (⋃ n, ⋃ j, Topology.RelCWComplex.closedCell n j)
-- Init.Control.Except
_private.Init.Control.Except.0.Except.map.match_1.splitter : {ε : Type u_1} →
  {α : Type u_2} →
    (motive : Except ε α → Sort u_3) →
      (x : Except ε α) → ((err : ε) → motive (Except.error err)) → ((v : α) → motive (Except.ok v)) → motive x
-- Lean.DocString.Types
Lean.Doc.instInhabitedDescItem : {a : Type u_1} → {a_1 : Type u_2} → Inhabited (Lean.Doc.DescItem a a_1)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.iselect_nil : ∀ {F : PFunctor.{uA, uB}} [inst : DecidableEq F.A] [inst_1 : Inhabited F.M] {a : F.A} (f : F.B a → F.M),
  PFunctor.M.iselect [] (PFunctor.M.mk ⟨a, f⟩) = a
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.one_le_ofENat : ∀ {n : ℕ∞}, 1 ≤ ↑n ↔ 1 ≤ n
-- Lean.Expr
Lean.PersistentExprMap : Type → Type
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- If a sum is 0 and the function is 0 except possibly at one
point, it is 0 everywhere on the `Finset`.  -/
Finset.eq_zero_of_sum_eq_zero : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → M} {a : ι},
  ∑ x ∈ s, f x = 0 → (∀ x ∈ s, x ≠ a → f x = 0) → ∀ x ∈ s, f x = 0
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAtFilter_ofNat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (n : ℕ) [inst_7 : OfNat F n] (L : Filter (E × E)), HasFDerivAtFilter (OfNat.ofNat n) 0 L
-- Mathlib.MeasureTheory.Measure.Haar.DistribChar
MeasureTheory.distribHaarChar_eq_div : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : TopologicalSpace A] [inst_4 : IsTopologicalAddGroup A] [inst_5 : LocallyCompactSpace A]
  [inst_6 : ContinuousConstSMul G A] [inst_7 : MeasurableSpace A] [BorelSpace A] {μ : MeasureTheory.Measure A}
  [μ.IsAddHaarMeasure] [μ.Regular] {s : Set A},
  μ s ≠ 0 → μ s ≠ ⊤ → ∀ (g : G), ↑((MeasureTheory.distribHaarChar A) g) = μ (g • s) / μ s
-- Mathlib.Data.List.NodupEquivFin
List.Nodup.getEquivOfForallMemList_symm_apply_val : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (a : α),
  ↑((List.Nodup.getEquivOfForallMemList l nd h).symm a) = List.idxOf a l
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_nonempty : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β}, (s • t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Data.Option.NAry
/-- `simp`-normal form of `mem_map₂_iff`.  -/
Option.map₂_eq_some_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : Option α} {b : Option β} {c : γ},
  Option.map₂ f a b = some c ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c
-- Mathlib.Logic.Relation
Relation.ReflTransGen.cases_tail_iff : ∀ {α : Type u_1} (r : α → α → Prop) (a a_1 : α),
  Relation.ReflTransGen r a a_1 ↔ a_1 = a ∨ ∃ b, Relation.ReflTransGen r a b ∧ r b a_1
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.Rewrite.mk : Bool → Lean.Expr → Lean.Expr → ℕ → Array (Lean.MVarId × Lean.BinderInfo) → Bool → Mathlib.Tactic.LibraryRewrite.Rewrite
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.instLattice : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasPullbacks C] →
      [CategoryTheory.Limits.HasImages C] →
        [CategoryTheory.Limits.HasBinaryCoproducts C] → {B : C} → Lattice (CategoryTheory.Subobject B)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.isEmpty =
    ((t.isEmpty || t.size == 1 && Std.DTreeMap.Internal.Impl.contains k t) && (f (t.get? k)).isNone)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_natCast_lt_one_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ}, ‖↑n‖ < 1 ↔ p ∣ n
-- Lean.Class
Lean.ClassState.outLevelParamMap : Lean.ClassState → Lean.SMap Lean.Name (Array ℕ)
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.comp_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y Z : CategoryTheory.Center C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Change of variables, most common version. If `f` has continuous derivative `f'` on `[a, b]`,
and `g` is continuous, then we can substitute `u = f x` to get
`∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.

If the function `f` is monotone or antitone, see also `integral_deriv_smul_comp_of_deriv_nonneg`
and `integral_deriv_smul_comp_of_deriv_nonpos` dropping all assumptions on `g`.  -/
intervalIntegral.integral_deriv_smul_comp : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
    ContinuousOn f' (Set.uIcc a b) → Continuous g → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x