mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.BoxIntegral.Box.Basic
/-- The set underlying this box: `⊥` is mapped to `∅`.  -/
BoxIntegral.Box.withBotToSet : {ι : Type u_1} → WithBot (BoxIntegral.Box ι) → Set (ι → ℝ)
-- Mathlib.Data.Set.Pairwise.Lattice
Pairwise.subset_of_biUnion_subset_biUnion : ∀ {α : Type u_1} {ι : Type u_2} {f : ι → Set α} {s t : Set ι},
  Pairwise (Function.onFun Disjoint f) → (∀ i ∈ s, (f i).Nonempty) → ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i → s ⊆ t
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.instIsLocallyFiniteMeasureVolume : MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.volume
-- Lean.Widget.InteractiveGoal
/-- An interactive term-mode goal.  -/
Lean.Widget.InteractiveTermGoal : Type
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.multiset_prod_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) {m : Multiset A}, (∀ x ∈ m, x ∈ S) → m.prod ∈ S
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.instIsRegularEpiOfIsSplitEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsSplitEpi f],
  CategoryTheory.IsRegularEpi f
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Equivalence.pi_unitIso : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (E : (i : I) → C i ≌ D i),
  (CategoryTheory.Equivalence.pi E).unitIso = CategoryTheory.NatIso.pi fun i => (E i).unitIso
-- Mathlib.Tactic.Nontriviality.Core
/-- Elaborator for the `nontriviality` tactic.  -/
Mathlib.Tactic.Nontriviality.elabNontriviality : Lean.Elab.Tactic.Tactic
-- Mathlib.Analysis.Convex.Function
/-- A strictly concave function on an open segment is strictly lower-bounded by the min of its
endpoints.  -/
StrictConcaveOn.lt_on_open_segment' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  StrictConcaveOn 𝕜 s f →
    ∀ {x y : E}, x ∈ s → y ∈ s → x ≠ y → ∀ {a b : 𝕜}, 0 < a → 0 < b → a + b = 1 → min (f x) (f y) < f (a • x + b • y)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.proj.eq_1 : ∀ {P : ProfiniteGrp.{u}} (U : OpenNormalSubgroup ↑P.toProfinite.toTop),
  ProfiniteGrp.proj U =
    ProfiniteGrp.ofHom { toFun := QuotientGroup.mk, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.homologyMap'_congr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData),
  CategoryTheory.ShortComplex.homologyMap' φ₁ h₁ h₂ = CategoryTheory.ShortComplex.homologyMap' φ₂ h₁ h₂
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
/-- Variant of `MemLp.mul` where the function is written as `fun x ↦ φ x * f x`
instead of `φ * f`.  -/
MeasureTheory.MemLp.mul' : ∀ {α : Type u_1} {x : MeasurableSpace α} {𝕜 : Type u_2} [inst : NormedRing 𝕜] {μ : MeasureTheory.Measure α}
  {p q r : ENNReal} {f φ : α → 𝕜},
  MeasureTheory.MemLp f q μ →
    MeasureTheory.MemLp φ p μ → ∀ [hpqr : p.HolderTriple q r], MeasureTheory.MemLp (fun x => φ x * f x) r μ
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- A `G`-diffeomorphism between two charted spaces is a homeomorphism which, when read in the
charts, belongs to `G`. We avoid the word diffeomorph as it is too related to the smooth category,
and use structomorph instead.  -/
Structomorph : {H : Type u} →
  [inst : TopologicalSpace H] →
    StructureGroupoid H →
      (M : Type u_5) →
        (M' : Type u_6) →
          [inst_1 : TopologicalSpace M] →
            [inst_2 : TopologicalSpace M'] → [ChartedSpace H M] → [ChartedSpace H M'] → Type (max u_5 u_6)
-- Mathlib.Topology.Sheaves.Flasque
/-- If the unique map from `A` to the terminal object is an epimorphism, then the skyscraper sheaf
valued in `A` supported at an arbitrary point is a flasque sheaf.
 -/
isFlasque_skyscraperSheaf_of_epi_from : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [CategoryTheory.Epi (CategoryTheory.Limits.terminalIsTerminal.from A)], (skyscraperSheaf p₀ A).IsFlasque
-- Mathlib.Algebra.DirectSum.Ring
/-- The canonical map from ℕ to a graded semiring respects zero.  -/
DirectSum.GSemiring.natCast_zero : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  [self : DirectSum.GSemiring A], DirectSum.GSemiring.natCast 0 = 0
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- **Alias** of `IsGaloisGroup.mulEquivCongr_apply_smul`. -/
IsGaloisGroup.mulEquivCongr'_apply_smul : ∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : IsDomain B] [inst_5 : Algebra A B] [inst_6 : FaithfulSMul A B]
  [inst_7 : MulSemiringAction G B] [inst_8 : MulSemiringAction G' B] [inst_9 : IsGaloisGroup G A B]
  [inst_10 : IsGaloisGroup G' A B] [inst_11 : Finite G] [inst_12 : Finite G'] (g : G) (x : B),
  (IsGaloisGroup.mulEquivCongr G G' A B) g • x = g • x
-- Mathlib.Algebra.Group.Basic
mul_eq_of_eq_div' : ∀ {G : Type u_3} [inst : CommGroup G] {a b c : G}, b = c / a → a * b = c
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.instCompactSpaceM : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_4} {H : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {s : SingularManifold X k I}, CompactSpace s.M
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.sInf_empty : sInf ∅ = 0
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformlyOn.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β]
  {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [inst_2 : UniformSpace γ] {G : ι → α → γ} {g : α → γ},
  TendstoLocallyUniformlyOn F f p s →
    TendstoLocallyUniformlyOn G g p s → TendstoLocallyUniformlyOn (fun n x => (F n x, G n x)) (fun x => (f x, g x)) p s
-- Mathlib.Order.Bounds.Basic
IsGreatest.isGreatest_iff_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {a b : α}, IsGreatest s a → (IsGreatest s b ↔ a = b)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal_eq_iff_associated : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (x y : R),
  (IsDiscreteValuationRing.addVal R) x = (IsDiscreteValuationRing.addVal R) y ↔ Associated x y
-- Mathlib.LinearAlgebra.BilinearMap
/-- Given a linear map from `M` to linear maps from `N` to `P`, i.e., a bilinear map from `M × N` to
`P`, change the order of variables and get a linear map from `N` to linear maps from `M` to `P`.  -/
LinearMap.flip : {R : Type u_1} →
  {R₂ : Type u_2} →
    {S : Type u_3} →
      {S₂ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : Semiring S] →
              [inst_3 : Semiring S₂] →
                {M : Type u_5} →
                  {N : Type u_7} →
                    {P : Type u_9} →
                      [inst_4 : AddCommMonoid M] →
                        [inst_5 : AddCommMonoid N] →
                          [inst_6 : AddCommMonoid P] →
                            [inst_7 : Module R M] →
                              [inst_8 : Module S N] →
                                [inst_9 : Module R₂ P] →
                                  [inst_10 : Module S₂ P] →
                                    [inst_11 : SMulCommClass S₂ R₂ P] →
                                      {ρ₁₂ : R →+* R₂} →
                                        {σ₁₂ : S →+* S₂} → (M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) → N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.compl₂_apply : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : CommMonoid P] [inst_3 : MulOneClass Q] (f : M →* N →* P) (g : Q →* N) (m : M) (q : Q),
  ((f.compl₂ g) m) q = (f m) (g q)
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
instIsLocalHomOfMonoidWithZeroHomClassOfNontrivial : ∀ {M₀ : Type u_2} {G₀ : Type u_3} {F : Type u_6} [inst : MonoidWithZero M₀] [inst_1 : GroupWithZero G₀]
  [inst_2 : FunLike F G₀ M₀] [MonoidWithZeroHomClass F G₀ M₀] [Nontrivial M₀] (f : F), IsLocalHom f
-- Mathlib.Topology.Separation.Hausdorff
/-- The map from a topological space to its largest T2 quotient.  -/
T2Quotient.mk : {X : Type u_1} → [inst : TopologicalSpace X] → X → T2Quotient X
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_alter_le_size : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (Std.DTreeMap.Const.alter t k f).size ≤ t.size + 1
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.exists_vadd_of_last_eq : ∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] [AddAction.IsPretransitive G α] {n : ℕ}
  (a : α) (x : Fin n.succ ↪ α), ∃ g y, g +ᵥ x = SubAddAction.ofStabilizer.snoc y
-- Lean.Meta.Tactic.Grind.Proof
Lean.Meta.Grind.mkHEqProofImpl : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
WittVector.inverseCoeff.eq_2 : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (a : kˣ)
  (A : WittVector p k) (n : ℕ),
  WittVector.inverseCoeff a A n.succ = WittVector.succNthValUnits n a A fun i => WittVector.inverseCoeff a A ↑i
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- The kernel of a zero map is preserved by any functor which preserves zero morphisms.  -/
CategoryTheory.Limits.preservesKernel_zero' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {X Y : C} (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] (f : X ⟶ Y),
  f = 0 → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularRing.mk : ∀ {R : Type u_2} [inst : CommRing R] [toIsNoetherian : IsNoetherian R R],
  (∀ (p : Ideal R) [inst_1 : p.IsPrime], IsRegularLocalRing (Localization.AtPrime p)) → IsRegularRing R
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.BinaryBicone.ofLimitCone_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)} (ht : CategoryTheory.Limits.IsLimit t),
  (CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).fst = t.π.app { as := CategoryTheory.Limits.WalkingPair.left }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_modify_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : β k → β k}, (m.modify k f).getKey? k = if k ∈ m then some k else none
-- Mathlib.Data.Sum.Interval
Finset.mem_sumLift₂ : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  {f : α₁ → β₁ → Finset γ₁} {g : α₂ → β₂ → Finset γ₂} {a : α₁ ⊕ α₂} {b : β₁ ⊕ β₂} {c : γ₁ ⊕ γ₂},
  c ∈ Finset.sumLift₂ f g a b ↔
    (∃ a₁ b₁ c₁, a = Sum.inl a₁ ∧ b = Sum.inl b₁ ∧ c = Sum.inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = Sum.inr a₂ ∧ b = Sum.inr b₂ ∧ c = Sum.inr c₂ ∧ c₂ ∈ g a₂ b₂
-- Init.Data.Ord.Basic
List.isLE_compareLex_nil_left : ∀ {α : Type u_1} {cmp : α → α → Ordering} {xs : List α}, (List.compareLex cmp [] xs).isLE = true
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_shiftLeft' : ∀ {w₁ w₂ w₃ : ℕ} {x : BitVec w₁} {y : BitVec w₂} {z : BitVec w₃}, x <<< y <<< z = x <<< (y.toNat + z.toNat)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_elim_l : ∀ {σs : List (Type u)} {Q R : Std.Do.SPred σs} {φ : Prop}, (φ → Q ⊢ₛ R) → ⌜φ⌝ ∧ Q ⊢ₛ R
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.finMulAntidiag_zero_left : ∀ {n : ℕ}, n ≠ 1 → Nat.finMulAntidiag 0 n = ∅
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Lax associativity.  -/
CategoryTheory.LaxFunctor.map₂_associator_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.LaxFunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : self.obj a ⟶ self.obj d}
  (h_1 : self.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h))
      (CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h)
        (CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom) h_1)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h))
        (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)) h_1))
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.functorCategory_monomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type u'') [inst_1 : CategoryTheory.Category.{v'', u''} J]
  [CategoryTheory.Limits.HasPullbacks C],
  (CategoryTheory.MorphismProperty.monomorphisms C).functorCategory J =
    CategoryTheory.MorphismProperty.monomorphisms (CategoryTheory.Functor J C)
-- Mathlib.Topology.UniformSpace.Ultra.Completion
IsUltraUniformity.cauchyFilter : ∀ {X : Type u_1} [inst : UniformSpace X] [IsUltraUniformity X], IsUltraUniformity (CauchyFilter X)
-- Mathlib.Topology.UniformSpace.Defs
/-- **Alias** of the forward direction of `UniformSpace.isCover_iff_subset_iUnion_ball`. -/
SetRel.IsCover.subset_iUnion_ball : ∀ {β : Type ub} {U : SetRel β β} [U.IsSymm] {s N : Set β}, U.IsCover s N → s ⊆ ⋃ y ∈ N, UniformSpace.ball y U
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a `CommGroup` is a `CommGroup`.  -/
SubgroupClass.toCommGroup : {S : Type u_4} →
  (H : S) → {G : Type u_5} → [inst : CommGroup G] → [inst_1 : SetLike S G] → [SubgroupClass S G] → CommGroup ↥H
-- Aesop.Util.UnionFind
Aesop.UnionFind.sets : {α : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Aesop.UnionFind α → Array (Array α) × Aesop.UnionFind α
-- Lean.Util.ForEachExprWhere
_private.Lean.Util.ForEachExprWhere.0.Lean.ForEachExprWhere.visit.go : {ω : Type} →
  {m : Type → Type} →
    [STWorld ω m] →
      [MonadLiftT (ST ω) m] →
        [Monad m] →
          (Lean.Expr → Bool) → (Lean.Expr → m Unit) → Bool → Lean.Expr → StateRefT' ω Lean.ForEachExprWhere.State m Unit
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Ioc_add_one_left_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {a b : α},
  a < b → insert (a + 1) (Set.Ioc (a + 1) b) = Set.Ioc a b
-- Mathlib.Topology.Semicontinuity.Basic
LowerSemicontinuous.isClosed_preimage : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] {f : α → γ},
  LowerSemicontinuous f → ∀ (y : γ), IsClosed (f ⁻¹' Set.Iic y)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α}, (t.erase k).getKey? a = if cmp k a = Ordering.eq then none else t.getKey? a
-- Mathlib.Algebra.Order.Field.Power
zpow_eq_one_iff_cases₀ : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ},
  a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- **Fundamental theorem of calculus-2**, on semi-infinite intervals `(-∞, a)`.
When a function has a limit `m` at `-∞`, and its derivative is integrable, then the
integral of the derivative on `(-∞, a)` is `f a - m`. Version assuming differentiability
on `(-∞, a]`.

Note that such a function always has a limit at minus infinity,
see `tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic`.  -/
MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto' : ∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} {m : E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E],
  (∀ x ∈ Set.Iic a, HasDerivAt f (f' x) x) →
    MeasureTheory.IntegrableOn f' (Set.Iic a) MeasureTheory.volume →
      Filter.Tendsto f Filter.atBot (nhds m) → ∫ (x : ℝ) in Set.Iic a, f' x = f a - m
-- Mathlib.Topology.Order.OrderClosed
Ico_mem_nhdsGT_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b c : α},
  b ∈ Set.Ico c a → Set.Ico c a ∈ nhdsWithin b (Set.Ioi b)
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ico_eq_add_neg : ∀ {δ : Type u_4} [inst : AddCommGroup δ] (f : ℕ → δ) {m n : ℕ},
  m ≤ n → ∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range n, f k + -∑ k ∈ Finset.range m, f k
-- Init.Data.Vector.Lemmas
Vector.mem_iff_append : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n},
  a ∈ xs ↔ ∃ m k, ∃ (w : m + 1 + k = n), ∃ ys zs, xs = Vector.cast w (ys.push a ++ zs)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- Note: This function is only for reasoning about semantics. Its efficiency doesn't actually matter  -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.toList : {n : ℕ} → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → List (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsGEObj₃ObjTriangleTriangleLTGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ), t.IsGE ((t.triangleLTGE n).obj X).obj₃ n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.equiv_iff_toList_perm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp},
  t₁.Equiv t₂ ↔ t₁.toList.Perm t₂.toList
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : autoParam (n₀ + 1 = n₁) DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff._auto_1),
      CategoryTheory.Mono ((DerivedCategory.homologyFunctor C n₁).map T.mor₁) ↔
        DerivedCategory.HomologySequence.δ T n₀ n₁ h = 0
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.inter_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s ∩ ∅ = ∅
-- Mathlib.Analysis.Complex.Basic
Complex.one_mem_slitPlane : 1 ∈ Complex.slitPlane
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
_private.Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber.0.CircleDeg1Lift.termτ : Lean.ParserDescr
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_sdiff_of_sdiff_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} [T2Space M] {A B : Set α},
  MeasurableSet A → MeasurableSet B → v (B \ A) = 0 → v (A \ B) + v B = v A
-- Init.Data.SInt.Basic
ISize.instOfNat : {n : ℕ} → OfNat ISize n
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
minpolyDiv_eq_of_isIntegrallyClosed : ∀ {R : Type u_1} (K : Type u_3) {S : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : CommRing S]
  [inst_3 : Algebra R S] {x : S},
  IsIntegral R x →
    ∀ [IsDomain R] [IsIntegrallyClosed R] [IsDomain S] [inst_7 : Algebra R K] [inst_8 : Algebra K S]
      [IsScalarTower R K S] [IsFractionRing R K], minpolyDiv R x = minpolyDiv K x
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.mapRingHom_comp_mapDomainRingHom`. -/
MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Monoid M] [inst_3 : Monoid N] (f : R →+* S) (g : M →* N),
  (MonoidAlgebra.mapRingHom N f).comp (MonoidAlgebra.mapDomainRingHom R g) =
    (MonoidAlgebra.mapDomainRingHom S g).comp (MonoidAlgebra.mapRingHom M f)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_inverse_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D))}
  (φ : X ⟶ Y) (x : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.equivComma.inverse.map φ).app x =
    match x with
    | CategoryTheory.WithInitial.of x => φ.right.app x
    | CategoryTheory.WithInitial.star => φ.left
-- Mathlib.Computability.Language
Language.reverse_iInf : ∀ {α : Type u_1} {ι : Sort u_4} (l : ι → Language α), (⨅ i, l i).reverse = ⨅ i, (l i).reverse
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure.eq_1 : ∀ {G : Type u_1} [inst : Group G] (k : Set G), Subgroup.closure k = sInf {K | k ⊆ ↑K}
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.lift.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M''] [inst_3 : Module R M] [inst_4 : Module R M''] (g g_1 : M →ₗ[R] M''),
  g = g_1 →
    ∀ (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)),
      LocalizedModule.lift S g h = LocalizedModule.lift S g_1 h
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- Oplax unity.  -/
CategoryTheory.Pseudofunctor.StrongTrans.naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (self : F.StrongTrans G) (a : B),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)).hom
      (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (self.app a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom
        (CategoryTheory.Bicategory.rightUnitor (self.app a)).inv)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- Uniform integrability in the measure theory sense.

A sequence of functions `f` is said to be uniformly integrable if for all `ε > 0`, there exists
some `δ > 0` such that for all sets `s` with measure less than `δ`, the Lp-norm of `f i`
restricted to `s` is less than `ε`.

Uniform integrability is also known as uniformly absolutely continuous integrals.  -/
MeasureTheory.UnifIntegrable : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_3} →
      [NormedAddCommGroup β] → {x : MeasurableSpace α} → (ι → α → β) → ENNReal → MeasureTheory.Measure α → Prop
-- Mathlib.CategoryTheory.Action.Basic
/-- The action defined by sending every monoid element to the identity.  -/
Action.trivial : {V : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} V] → (G : Type u_2) → [inst_1 : Monoid G] → V → Action V G