mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Hom
AlgHom.comp_algebraMap : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), (↑φ).comp (algebraMap R A) = algebraMap R B
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDeriv_succ_apply_right : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : ℕ} (m : Fin (n + 1) → E),
  (iteratedFDeriv 𝕜 (n + 1) f x) m = ((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) (Fin.init m)) (m (Fin.last n))
-- Init.Data.Array.Erase
Array.mem_eraseIdx_iff_getElem? : ∀ {α : Type u_1} {x : α} {xs : Array α} {k : ℕ} {h : k < xs.size}, x ∈ xs.eraseIdx k h ↔ ∃ i, i ≠ k ∧ xs[i]? = some x
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.instHPowQNat : {α : Type u} →
  [inst : Lean.Grind.CommSemiring α] →
    [Lean.Grind.CommRing (Lean.Grind.Ring.OfSemiring.Q α)] →
      HPow (Lean.Grind.Ring.OfSemiring.Q α) ℕ (Lean.Grind.Ring.OfSemiring.Q α)
-- Init.Data.UInt.Lemmas
UInt16.add_neg_eq_sub : ∀ {a b : UInt16}, a + -b = a - b
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- The underlying 2-isomorphisms of the naturality constraint.  -/
CategoryTheory.Oplax.OplaxTrans.StrongCore.naturality : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η : F ⟶ G} →
            CategoryTheory.Oplax.OplaxTrans.StrongCore η →
              {a b : B} →
                (f : a ⟶ b) →
                  CategoryTheory.CategoryStruct.comp (F.map f) (η.app b) ≅
                    CategoryTheory.CategoryStruct.comp (η.app a) (G.map f)
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.throwCongrHypothesisFailed : {α : Type} → Lean.MetaM α
-- Mathlib.Order.Interval.Set.Basic
Set.nonempty_Ico_subtype : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → Nonempty ↑(Set.Ico b a)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path₁.mk.congr_simp : ∀ {X : SSet.Truncated 1} {n : ℕ}
  (vertex vertex_1 :
    Fin (n + 1) → X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Path₁._proof_1 }))
  (e_vertex : vertex = vertex_1)
  (arrow arrow_1 : Fin n → X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Path₁._proof_2 }))
  (e_arrow : arrow = arrow_1)
  (arrow_src :
    ∀ (i : Fin n),
      (CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) SSet.Truncated.Path₁._proof_1
                  SSet.Truncated.Path₁._proof_5).op))
          (arrow i) =
        vertex i.castSucc)
  (arrow_tgt :
    ∀ (i : Fin n),
      (CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0) SSet.Truncated.Path₁._proof_1
                  SSet.Truncated.Path₁._proof_5).op))
          (arrow i) =
        vertex i.succ),
  { vertex := vertex, arrow := arrow, arrow_src := arrow_src, arrow_tgt := arrow_tgt } =
    { vertex := vertex_1, arrow := arrow_1, arrow_src := ⋯, arrow_tgt := ⋯ }
-- Mathlib.MeasureTheory.SetSemiring
/-- For some `hJ : J ⊆ C` and `j : Set α`, where `hC : IsSetSemiring C`, this is
a `Finset (Set α)` such that `K j := hC.disjointOfUnion hJ` are disjoint
and `⋃₀ K j ⊆ j`, for `j ∈ J`.
Using these we write `⋃₀ J` as a disjoint union `⋃₀ J = ⋃₀ ⋃ x ∈ J, (K x)`.
See `MeasureTheory.IsSetSemiring.disjointOfUnion_props`.  -/
MeasureTheory.IsSetSemiring.disjointOfUnion : {α : Type u_1} →
  {C : Set (Set α)} → {J : Finset (Set α)} → MeasureTheory.IsSetSemiring C → ↑J ⊆ C → Set α → Finset (Set α)
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- Given a normal subgroup `Γ` of a topological group `G` with Haar measure `μ`, which is also
right-invariant, and a finite volume fundamental domain `𝓕`, the quotient map to `G ⧸ Γ`,
properly normalized, satisfies `QuotientMeasureEqMeasurePreimage`.  -/
IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [inst_3 : IsTopologicalGroup G] [inst_4 : BorelSpace G] [inst_5 : PolishSpace G] {Γ : Subgroup G} [inst_6 : Γ.Normal]
  [inst_7 : T2Space (G ⧸ Γ)] [inst_8 : SecondCountableTopology (G ⧸ Γ)] [Countable ↥Γ] (ν : MeasureTheory.Measure G)
  [ν.IsHaarMeasure] [ν.IsMulRightInvariant] [MeasureTheory.SigmaFinite ν]
  (K : TopologicalSpace.PositiveCompacts (G ⧸ Γ)) {𝓕 : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 ν →
    ν 𝓕 ≠ ⊤ →
      MeasureTheory.QuotientMeasureEqMeasurePreimage ν
        (ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕) • MeasureTheory.Measure.haarMeasure K)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_addMonoidHom_refl : ∀ {R : Type u_4} [inst : NonAssocSemiring R], ↑(RingEquiv.refl R) = AddMonoidHom.id R
-- Mathlib.Topology.Algebra.MulAction
continuousVAdd_sInf : ∀ {M : Type u_2} {X : Type u_3} [inst : TopologicalSpace M] [inst_1 : VAdd M X] {ts : Set (TopologicalSpace X)},
  (∀ t ∈ ts, ContinuousVAdd M X) → ContinuousVAdd M X
-- Std.Http.Data.URI.Encoding
Std.Http.URI.instDecidableIsAllowedEncodedQueryChars : {r : UInt8 → Bool} → {s : ByteArray} → Decidable (Std.Http.URI.IsAllowedEncodedQueryChars r s)
-- Mathlib.Topology.UniformSpace.Separation
t0Space_iff_uniformity' : ∀ {α : Type u} [inst : UniformSpace α], T0Space α ↔ Pairwise fun x y => ∃ r ∈ uniformity α, (x, y) ∉ r
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.one_apply : ∀ {M : Type u_1} [inst : Monoid M] {A : Type u_4} [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A] (a : A),
  1 a = a
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_insert : ∀ {α : Type u_2} [inst : InvolutiveInv α] (a : α) (s : Set α), (insert a s)⁻¹ = insert a⁻¹ s⁻¹
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.mem_toList_insert_self : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {k : α} (v : β) (t : RBTree.RBMap α β cmp),
  (k, v) ∈ (t.insert k v).toList
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- **Alias** of the reverse direction of `SimpleGraph.edgeFinset_ssubset_edgeFinset`. -/
SimpleGraph.edgeFinset_strict_mono : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} [inst : Fintype ↑G₁.edgeSet] [inst_1 : Fintype ↑G₂.edgeSet],
  G₁ < G₂ → G₁.edgeFinset ⊂ G₂.edgeFinset
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedIsoClosure : ∀ {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], P.isoClosure.IsTriangulated
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.minKey.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : x.isEmpty = false),
  x.minKey x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => k
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      h_1 => l.minKey ⋯
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instSurjectiveOfIsIsoScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f], AlgebraicGeometry.Surjective f
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- Every presheaf is a sheaf for the regular topology if every object of `C` is projective.  -/
CategoryTheory.regularTopology.isSheaf_of_projective : ∀ {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] (F : CategoryTheory.Functor Cᵒᵖ D)
  [inst_2 : CategoryTheory.Preregular C] [∀ (X : C), CategoryTheory.Projective X],
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F
-- Mathlib.Order.Defs.PartialOrder
Preorder.le_refl : ∀ {α : Type u_2} [self : Preorder α] (a : α), a ≤ a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyLE_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h' : ∃ a ∈ t₁, (cmp a k).isLE = true} (h : t₁.Equiv t₂), t₁.getKeyLE k h' = t₂.getKeyLE k ⋯
-- Mathlib.Topology.Connected.Clopen
/-- In a preconnected space, given a transitive relation `P`, if `P x y` and `P y x` are true
for `y` close enough to `x`, then `P x y` holds for all `x, y`. This is a version of the fact
that, if an equivalence relation has open classes, then it has a single equivalence class.  -/
PreconnectedSpace.induction₂' : ∀ {α : Type u} [inst : TopologicalSpace α] [PreconnectedSpace α] (P : α → α → Prop),
  (∀ (x : α), ∀ᶠ (y : α) in nhds x, P x y ∧ P y x) → IsTrans α P → ∀ (x y : α), P x y
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousOn_unique : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] [inst : Unique ι]
  {F : ι → X → α} {S : Set X}, EquicontinuousOn F S ↔ ContinuousOn (F default) S
-- Mathlib.Algebra.Module.Equiv.Defs
/-- An involutive linear map is a linear equivalence.  -/
LinearEquiv.ofInvolutive : {R : Type u_1} →
  {M : Type u_7} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        {σ σ' : R →+* R} →
          [inst_2 : RingHomInvPair σ σ'] →
            [inst_3 : RingHomInvPair σ' σ] → {x : Module R M} → (f : M →ₛₗ[σ] M) → Function.Involutive ⇑f → M ≃ₛₗ[σ] M
-- Mathlib.Algebra.Group.Action.Opposite
/-- Like `AddMonoid.toAddAction`, but adds on the right.  -/
AddMonoid.toOppositeAddAction : {α : Type u_3} → [inst : AddMonoid α] → AddAction αᵃᵒᵖ α
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.MLListImpl.brecOn.go : {m : Type u → Type u} →
  {α : Type u} →
    {motive_1 : MLList.MLListImpl✝ m α → Sort u_1} →
      {motive_2 : Thunk (MLList.MLListImpl✝ m α) → Sort u_1} →
        (t : MLList.MLListImpl✝ m α) →
          ((t : MLList.MLListImpl✝ m α) → MLList.MLListImpl.below✝ t → motive_1 t) →
            ((t : Thunk (MLList.MLListImpl✝ m α)) → MLList.MLListImpl.below_1✝ t → motive_2 t) →
              motive_1 t ×' MLList.MLListImpl.below✝ t
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.instSliceableRcoSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.instSliceableRcoSlice._auto_1) →
    Std.Rco.Sliceable (Std.TreeSet.Raw α cmp) α (Std.DTreeMap.Internal.Unit.RcoSlice α)
-- Mathlib.Topology.Algebra.SeparationQuotient.Section
SeparationQuotient.mk_comp_outCLM : ∀ (K : Type u_1) (E : Type u_2) [inst : DivisionRing K] [inst_1 : AddCommGroup E] [inst_2 : Module K E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousConstSMul K E],
  SeparationQuotient.mk ∘ ⇑(SeparationQuotient.outCLM K E) = id
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- `mapMon` is functorial in the lax monoidal functor.  -/
CategoryTheory.Functor.mapMonFunctor : (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] →
            CategoryTheory.Functor (CategoryTheory.LaxMonoidalFunctor C D)
              (CategoryTheory.Functor (CategoryTheory.Mon C) (CategoryTheory.Mon D))
-- Init.Data.Vector.Lemmas
Vector.set_replicate_self : ∀ {n : ℕ} {α : Type u_1} {a : α} {i : ℕ} {h : i < n}, (Vector.replicate n a).set i a h = Vector.replicate n a
-- Mathlib.RingTheory.PowerSeries.Evaluation
/-- [Bourbaki, *Algebra*, chap. 4, §4, n°3, Prop. 4 (i) (a & b)][bourbaki1981].  -/
PowerSeries.HasEval.map : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {φ : R →+* S} [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace S], Continuous ⇑φ → ∀ {a : R}, PowerSeries.HasEval a → PowerSeries.HasEval (φ a)
-- Mathlib.RingTheory.Localization.InvSubmonoid
/-- The submonoid of `S = M⁻¹R` consisting of `{ 1 / x | x ∈ M }`.  -/
IsLocalization.invSubmonoid : {R : Type u_1} →
  [inst : CommRing R] → Submonoid R → (S : Type u_2) → [inst_1 : CommRing S] → [Algebra R S] → Submonoid S
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C}
  (c : CategoryTheory.Limits.Cocone K) (F : CategoryTheory.Functor C D) {X : D} (f : F.obj c.pt ⟶ X),
  (c.toCostructuredArrowCocone F f).pt = CategoryTheory.CostructuredArrow.mk f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.equiv_empty_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp},
  t.Equiv Std.DTreeMap.Raw.empty ↔ t.isEmpty = true
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a product of measures is a product of
characteristic functions. This is the version for Banach spaces, see `charFun_prod`
for the Hilbert space version.  -/
MeasureTheory.charFunDual_prod : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : MeasureTheory.Measure E}
  {ν : MeasureTheory.Measure F} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (L : StrongDual ℝ (E × F)),
  MeasureTheory.charFunDual (μ.prod ν) L =
    MeasureTheory.charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) *
      MeasureTheory.charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
ProbabilityTheory.iIndepFun.hasGaussianLaw_fun_sub : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E]
  {X Y : Ω → E},
  ProbabilityTheory.HasGaussianLaw X P →
    ProbabilityTheory.HasGaussianLaw Y P →
      ProbabilityTheory.IndepFun X Y P → ProbabilityTheory.HasGaussianLaw (fun ω => X ω - Y ω) P
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.eq_4 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b)))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  (match Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) => h_3 l b
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) =
    h_4 ()
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNormEssSup_indicator_const_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] (s : Set α) (c : ε),
  μ s ≠ 0 → MeasureTheory.eLpNormEssSup (s.indicator fun x => c) μ = ‖c‖ₑ
-- Batteries.Data.List.Perm
/-- The list version of `Multiset.le_iff_count`.  -/
List.subperm_ext_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ : List α},
  l₁.Subperm l₂ ↔ ∀ x ∈ l₁, List.count x l₁ ≤ List.count x l₂
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)}
  (t : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)),
  (CategoryTheory.WithTerminal.coneEquiv.inverse.obj t).pt.hom = t.π.app CategoryTheory.WithTerminal.star
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_ge_of_const_le : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f : X → E}
  {s : Set X} [ClosedIciTopology E] [CompleteSpace E] {c : E},
  MeasurableSet s →
    μ s ≠ ⊤ → (∀ x ∈ s, c ≤ f x) → MeasureTheory.IntegrableOn (fun x => f x) s μ → μ.real s • c ≤ ∫ (x : X) in s, f x ∂μ
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.adj.eq_1 : ∀ (R : Type u) [inst : Ring R],
  ModuleCat.adj R =
    CategoryTheory.Adjunction.mkOfHomEquiv
      { homEquiv := fun x x_1 => ModuleCat.freeHomEquiv, homEquiv_naturality_left_symm := ⋯,
        homEquiv_naturality_right := ⋯ }
-- Init.Data.Vector.Attach
Vector.foldr_pmap : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {γ : Type u_3} {xs : Vector α n} {P : α → Prop} {f : (a : α) → P a → β}
  (H : ∀ a ∈ xs, P a) (g : β → γ → γ) (x : γ),
  Vector.foldr g x (Vector.pmap f xs H) = Vector.foldr (fun a acc => g (f ↑a ⋯) acc) x xs.attach
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_insertIfNew_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.insertIfNew k v).contains k = true
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.llr_smul_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    ∀ (c : ENNReal),
      c ≠ 0 → c ≠ ⊤ → MeasureTheory.llr (c • μ) ν =ᵐ[μ] fun x => MeasureTheory.llr μ ν x + Real.log c.toReal
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_principal : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter α} {s : Set β},
  Filter.Tendsto f l (Filter.principal s) ↔ ∀ᶠ (a : α) in l, f a ∈ s
-- Mathlib.Order.Interval.Set.OrdConnected
Set.Icc_subset : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α) [hs : s.OrdConnected] {x y : α}, x ∈ s → y ∈ s → Set.Icc x y ⊆ s
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_add_nat : ∀ (n : ℕ), Cardinal.aleph0 + ↑n = Cardinal.aleph0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem.label : Lean.Lsp.ResolvableCompletionItem → String
-- Init.Data.UInt.Lemmas
UInt8.add_sub_cancel : ∀ (a b : UInt8), a + b - b = a
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofNat_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (n : ℕ), OfNat.ofNat n = Lean.Grind.Field.NormNum.ofRat ↑n
-- Init.Data.Option.Lemmas
Option.mem_dite_none_right : ∀ {α : Type u_1} {p : Prop} {x : α} {x_1 : Decidable p} {l : p → Option α},
  (x ∈ if h : p then l h else none) ↔ ∃ (h : p), x ∈ l h
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isPullback_resLE : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T},
  CategoryTheory.IsPullback g iY iX f →
    ∀ {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US)
      (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens}
      (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT),
      CategoryTheory.IsPullback (AlgebraicGeometry.Scheme.Hom.resLE g UX UY ⋯)
        (AlgebraicGeometry.Scheme.Hom.resLE iY UT UY ⋯) (AlgebraicGeometry.Scheme.Hom.resLE iX US UX hUSX)
        (AlgebraicGeometry.Scheme.Hom.resLE f US UT hUST)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.instGrpObj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {H : CategoryTheory.Grp C} [inst_3 : CategoryTheory.IsCommMonObj H.X],
  CategoryTheory.Grp.instGrpObj =
    { toMonObj := CategoryTheory.Grp.instMonObj,
      inv := CategoryTheory.Grp.homMk' { hom := CategoryTheory.GrpObj.inv, isMonHom_hom := ⋯ }, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- The canonical `MultilinearMap R s (⨂[R] i, s i)`.

`tprod R fun i => f i` has notation `⨂ₜ[R] i, f i`.  -/
PiTensorProduct.«term⨂ₜ[_]_,_» : Lean.ParserDescr
-- Mathlib.Algebra.Group.NatPowAssoc
npow_mul' : ∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [NatPowAssoc M] (x : M) (m n : ℕ), x ^ (m * n) = (x ^ n) ^ m
-- LeanSearchClient.Syntax
LeanSearchClient.defaultTerm : Option Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.LinearAlgebra.Dual.BaseChange
IsBaseChange.congr_simp : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} (S : Type v₃) [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (f f_1 : M →ₗ[R] N),
  f = f_1 → IsBaseChange S f = IsBaseChange S f_1
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.disjoint_toFinset : ∀ {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite}, Disjoint hs.toFinset ht.toFinset ↔ Disjoint s t
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt64.size ≤ n → (UInt64.ofNatClamp n).toBitVec = (UInt64.size - 1)#'UInt64.toBitVec_ofNatClamp_of_le._proof_1
-- Mathlib.Topology.Maps.Basic
IsClosedMap.mapClusterPt_iff_lift'_closure : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {F : Filter X},
  IsClosedMap f → Continuous f → ∀ {y : Y}, MapClusterPt y F f ↔ (F.lift' closure ⊓ Filter.principal (f ⁻¹' {y})).NeBot
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {z : M} {F' : Type u_21}
  [inst_6 : NormedField F'] [inst_7 : NormedAlgebra 𝕜 F'] {p : M → F'} {p' : TangentSpace I z →L[𝕜] F'},
  HasMFDerivAt[s] p z p' → p z ≠ 0 → HasMFDerivAt[s] p⁻¹ z (-(p z ^ 2)⁻¹ • p')
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.map_smulₛₗ : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (c : R) (x : E), f (c • x) = σ₁₂ c • f x
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- Auxiliary definition for `associator`.  -/
CategoryTheory.GradedObject.Monoidal.ρ₂₃ : {I : Type u} →
  [inst : AddMonoid I] → CategoryTheory.GradedObject.BifunctorComp₂₃IndexData CategoryTheory.GradedObject.Monoidal.r₁₂₃
-- Std.Time.Time.Unit.Second
Std.Time.Second.instToStringOrdinal : {leap : Bool} → ToString (Std.Time.Second.Ordinal leap)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_surjective : Function.Surjective ENNReal.log
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_of_lt_of_pos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b c : α},
  b < c → 0 < a → b < c + a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} (m m_1 : Std.HashMap α β) (e_m : m = m_1) (a a_1 : α)
  (e_a : a = a_1) (h : a ∈ m), m.getKey a h = m_1.getKey a_1 ⋯