mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.isSFiniteKernel_sum_of_denumerable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Denumerable ι]
  {κs : ι → ProbabilityTheory.Kernel α β},
  (∀ (n : ι), ProbabilityTheory.IsSFiniteKernel (κs n)) →
    ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.sum κs)
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.composePath_cons : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : Quiver.Path X Y) (e : Y ⟶ Z),
  CategoryTheory.composePath (p.cons e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath p) e
-- Mathlib.RingTheory.Polynomial.Wronskian
Polynomial.wronskianBilin_apply : ∀ {R : Type u_1} [inst : CommRing R] (a b : Polynomial R), ((Polynomial.wronskianBilin R) a) b = a.wronskian b
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.weight_nil : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Monoid R] (w : {i j : V} → (i ⟶ j) → R) (a : V),
  Quiver.Path.weight (fun {i j} => w) Quiver.Path.nil = 1
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- The reflection associated to a root.  -/
RootPairing.reflection : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → ι → M ≃ₗ[R] M
-- Mathlib.Order.Irreducible
/-- In a well-founded lattice, any element is the supremum of finitely many sup-irreducible
elements. This is the order-theoretic analogue of prime factorisation.  -/
exists_supIrred_decomposition : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [WellFoundedLT α] (a : α),
  ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Methods.pre : Lean.Meta.Simp.Methods → Lean.Meta.Simp.Simproc
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.of_mem_Icc : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (a b : ℝ)
  {X : α → ℝ}, (∀ᵐ (ω : α) ∂μ, X ω ∈ Set.Icc a b) → MeasureTheory.HasFiniteIntegral X μ
-- Init.Data.UInt.Lemmas
UInt8.div_self : ∀ {a : UInt8}, a / a = if a = 0 then 0 else 1
-- Mathlib.Topology.Homeomorph.Lemmas
/-- If `h : X → Y` is a homeomorphism, `s` is σ-compact iff `h(s)` is.  -/
Homeomorph.isSigmaCompact_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y),
  IsSigmaCompact (⇑h '' s) ↔ IsSigmaCompact s
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKey?.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.leaf.minKey? = none
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_roo_eq_add : ∀ {m n i fallback : ℕ}, i < n - (m + 1) → (m<...n).toList.getD i fallback = m + 1 + i
-- Mathlib.RingTheory.Valuation.Basic
Valuation.one_apply_le_one : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [inst_2 : Nontrivial R]
  [inst_3 : NoZeroDivisors R] [inst_4 : DecidablePred fun x => x = 0] (x : R), 1 x ≤ 1
-- Init.Data.List.Lemmas
List.length_insert_pos : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α}, 0 < (List.insert a l).length
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  (h₁ h₂ : CategoryTheory.AddMonObj X), CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add → h₁ = h₂
-- Mathlib.Algebra.MonoidAlgebra.Grading
/-- Auxiliary definition; the canonical grade decomposition, used to provide
`DirectSum.decompose`.  -/
AddMonoidAlgebra.decomposeAux : {M : Type u_1} →
  {ι : Type u_2} →
    {R : Type u_3} →
      [inst : AddMonoid M] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : CommSemiring R] →
              (f : M →+ ι) → AddMonoidAlgebra R M →ₐ[R] DirectSum ι fun i => ↥(AddMonoidAlgebra.gradeBy R (⇑f) i)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullbackIso_inv_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f]
  (i : (CategoryTheory.PreZeroHypercover.pullback₂ f E).I₀),
  (CategoryTheory.PreZeroHypercover.pullbackIso f E).inv.h₀ i = (CategoryTheory.Limits.pullbackSymmetry f (E.f i)).inv
-- Mathlib.MeasureTheory.Measure.AEDisjoint
/-- **Alias** of `MeasureTheory.exists_null_pairwise_disjoint_sdiff`.

---

If `s : ι → Set α` is a countable family of pairwise a.e. disjoint sets, then there exists a
family of measurable null sets `t i` such that `s i \ t i` are pairwise disjoint.  -/
MeasureTheory.exists_null_pairwise_disjoint_diff : ∀ {ι : Type u_1} {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) s) →
    ∃ t,
      (∀ (i : ι), MeasurableSet (t i)) ∧
        (∀ (i : ι), μ (t i) = 0) ∧ Pairwise (Function.onFun Disjoint fun i => s i \ t i)
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_toDual : ∀ {α : Type u_1} [inst : Preorder α] {a b : α},
  Set.Ioo (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ioo b a
-- Init.Data.BitVec.Bitblast
BitVec.shiftLeftRec.eq_1 : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂), x.shiftLeftRec y 0 = x <<< (y &&& BitVec.twoPow w₂ 0)
-- Mathlib.Topology.Bornology.BoundedOperation
BoundedSub.isBounded_sub : ∀ {R : Type u_1} {inst : Bornology R} {inst_1 : Sub R} [self : BoundedSub R] {s t : Set R},
  Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s - t)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_filter : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {f : α → Bool} {k : α}, m.WF → (k ∈ Std.HashSet.Raw.filter f m ↔ ∃ (h' : k ∈ m), f (m.get k h') = true)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_inter_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → (m₁.inter m₂).getKey? k = none
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km : α}, t.minKey? = some km → t.contains km = true
-- Lean.Server.References
Lean.Server.DirectImports.mk : Array Lean.Server.ModuleImport → Lean.Server.ModuleImportIndex → Lean.Server.DirectImports
-- Mathlib.Analysis.LocallyConvex.PointwiseConvergence
PointwiseConvergenceCLM.isInducing_inducingFn : ∀ {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_7)
  (F : Type u_8) [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜₂ F],
  Topology.IsInducing ⇑(PointwiseConvergenceCLM.inducingFn σ E F)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
/-- `AffineSubspace.shift s c r` is an affine subspace parallel to `s`, where an arbitrary point on
`s` is moved towards `c` with linear interpolation by `r`. When `r = 0`, that point is moved onto
`c`. When `r = 1`, that point stays at the original position. A different choice of the point will
not affect the output (See `AffineSubspace.shift_eq`).

We define `AffineSubspace.shift ⊥ c r = ⊥` (See `AffineSubspace.shift_bot`).  -/
AffineSubspace.shift : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : AddTorsor V P] → [inst_3 : Module k V] → AffineSubspace k P → P → k → AffineSubspace k P
-- Init.Data.Int.LemmasAux
Int.max_assoc : ∀ (a b c : ℤ), max (max a b) c = max a (max b c)
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocInfo.mk.sizeOf_spec : ∀ (toElabInfo : Lean.Elab.ElabInfo), sizeOf { toElabInfo := toElabInfo } = 1 + sizeOf toElabInfo
-- Batteries.Data.String.Lemmas
String.set_of_valid : ∀ (cs cs' : List Char) (c' : Char),
  String.Pos.Raw.set (String.ofList (cs ++ cs')) { byteIdx := String.utf8Len cs } c' =
    String.ofList (cs ++ List.modifyHead (fun x => c') cs')
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.differentiableAt_inv_log : ∀ {x : ℝ}, x ≠ 0 → x ≠ 1 → x ≠ -1 → DifferentiableAt ℝ (fun x => (Real.log x)⁻¹) x
-- Mathlib.CategoryTheory.Generator.Basic
/-- A category with pullbacks and a small detecting set is well-powered.  -/
CategoryTheory.wellPowered_of_isDetecting : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C]
  {𝒢 : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.Small.{w, v₁, u₁} 𝒢]
  [inst_3 : CategoryTheory.LocallySmall.{w, v₁, u₁} C], 𝒢.IsDetecting → CategoryTheory.WellPowered.{w, v₁, u₁} C
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.instIsLocalizationLocalizedMonoidalToMonoidalCategory_1 : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit),
  (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).IsLocalization W
-- Mathlib.Topology.UniformSpace.Basic
top_uniformity : ∀ {α : Type ua}, uniformity α = ⊤
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.op_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (α : X ≅ Y), α.op.inv = α.inv.op
-- Mathlib.Data.Rel
SetRel.dom_mono : ∀ {α : Type u_1} {β : Type u_2} {R₁ R₂ : SetRel α β}, R₁ ⊆ R₂ → R₁.dom ⊆ R₂.dom
-- Mathlib.Algebra.Group.AddChar
AddChar.doubleDualEmb_apply : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (a : A) (ψ : AddChar A M),
  (AddChar.doubleDualEmb a) ψ = ψ a
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.mk_pow : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (n : ℕ) (f : CauSeq β abv),
  CauSeq.Completion.mk f ^ n = CauSeq.Completion.mk (f ^ n)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_eq_arccos : ∀ {x : ℝ}, 0 ≤ x → Real.arctan x = Real.arccos (√(1 + x ^ 2))⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.ofHasPullback_fst : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃) [inst_3 : CategoryTheory.Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)],
  (CategoryTheory.Functor.PullbackObjObj.ofHasPullback G f₁ f₃).fst =
    CategoryTheory.Limits.pullback.fst ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
CommGrpTypeEquivalenceCommGrp.commGrpCommGroup : (A : Type u) → [inst : CategoryTheory.GrpObj A] → [CategoryTheory.IsCommMonObj A] → CommGroup A
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
AddActionHom.zeroEmbeddingMap_bijective : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {zero : Type u_5} [inst_2 : Unique zero],
  Function.Bijective ⇑AddActionHom.zeroEmbeddingMap
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.mapToSelf : {α : Type u} →
  (xs : List ((_ : α) × α)) →
    (List.map Sigma.fst xs).Perm (List.map Sigma.snd xs) → (List.map Sigma.snd xs).Nodup → Plausible.InjectiveFunction α
-- Mathlib.Logic.Function.Iterate
Function.iterate_add : ∀ {α : Type u} (f : α → α) (m n : ℕ), f^[m + n] = f^[m] ∘ f^[n]
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instNormedCommRing : {α : Type u_1} →
  [inst : TopologicalSpace α] → [CompactSpace α] → {R : Type u_4} → [inst_2 : NormedCommRing R] → NormedCommRing C(α, R)
-- Mathlib.RingTheory.Algebraic.Basic
/-- A fraction `(a : S) / (b : S)` can be reduced to `(c : S) / (d : R)`,
if `b` is algebraic over `R`.  -/
IsAlgebraic.exists_smul_eq_mul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (a : S) {b : S},
  IsAlgebraic R b → b ∈ nonZeroDivisors S → ∃ c d, d ≠ 0 ∧ d • a = b * c
-- Mathlib.Order.UpperLower.Closure
gc_lowerClosure_coe : ∀ {α : Type u_1} [inst : Preorder α], GaloisConnection lowerClosure SetLike.coe
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- A functor is said to reflect finite colimits, if it reflects all colimits of shape `J`,
where `J : Type` is a finite category.
 -/
CategoryTheory.Limits.ReflectsFiniteColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Order.SymmDiff
symmDiff_right_comm : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b c : α), symmDiff (symmDiff a b) c = symmDiff (symmDiff a c) b
-- Mathlib.Data.List.Induction
List.twoStepInduction_cons_cons : ∀ {α : Type u_1} {motive : List α → Sort u_2} (x y : α) (xs : List α) (nil : motive [])
  (singleton : (x : α) → motive [x])
  (cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)),
  List.twoStepInduction nil singleton cons_cons (x :: y :: xs) =
    cons_cons x y xs (List.twoStepInduction nil singleton cons_cons xs) fun y =>
      List.twoStepInduction nil singleton cons_cons (y :: xs)
-- Mathlib.Data.Vector.Basic
List.Vector.naturality : ∀ {n : ℕ} {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative G]
  [LawfulApplicative F] (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : List.Vector α n),
  (fun {α} => η.app α) (List.Vector.traverse f x) = List.Vector.traverse ((fun {α} => η.app α) ∘ f) x
-- Mathlib.GroupTheory.Goursat
AddSubgroup.goursatFst.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (I : AddSubgroup (G × H)),
  I.goursatFst = AddSubgroup.map ((AddMonoidHom.fst G H).comp I.subtype) ((AddMonoidHom.snd G H).comp I.subtype).ker
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_tmod_unique : ∀ {a b r q : ℤ}, 0 ≤ a → b ≠ 0 → (a.tdiv b = q ∧ a.tmod b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < ↑b.natAbs)
-- Mathlib.NumberTheory.LSeries.Deriv
/-- If `re s` is greater than the abscissa of absolute convergence of `f`, then
the derivative of this L-series at `s` is the negative of the L-series of `log * f`.  -/
LSeries_deriv : ∀ {f : ℕ → ℂ} {s : ℂ}, LSeries.abscissaOfAbsConv f < ↑s.re → deriv (LSeries f) s = -LSeries (LSeries.logMul f) s
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.equivIcoMod.congr_simp : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), QuotientAddGroup.equivIcoMod hp a = QuotientAddGroup.equivIcoMod hp a
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjHomologySelfIso_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : C} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).inv
      (HomologicalComplex.homologyMap ((HomologicalComplex.single C c j).map f) j) =
    CategoryTheory.CategoryStruct.comp f (HomologicalComplex.singleObjHomologySelfIso c j B).inv
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `π = π'`, then `CokernelCofork.of_π π _` and `CokernelCofork.of_π π' _` are isomorphic.  -/
CategoryTheory.Limits.ofπCongr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {P : C} →
            {π π' : Y ⟶ P} →
              {w : CategoryTheory.CategoryStruct.comp f π = 0} →
                (h : π = π') →
                  CategoryTheory.Limits.CokernelCofork.ofπ π w ≅ CategoryTheory.Limits.CokernelCofork.ofπ π' ⋯
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.cg_iff_countable : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [Countable ((l : ℕ) × L.Functions l)],
  FirstOrder.Language.Structure.CG L M ↔ Countable M
-- Mathlib.Analysis.Analytic.CPolynomialDef
FormalMultilinearSeries.changeOriginSeries_sum_eq_partialSum_of_finite : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ},
  (∀ (m : ℕ), n ≤ m → p m = 0) → ∀ (k : ℕ), (p.changeOriginSeries k).sum = (p.changeOriginSeries k).partialSum (n - k)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f)
  (X : ↑(F.obj b₀)),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X)
      ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
      ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X))
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with
`[ContinuousAdd]`. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to `EReal`.  -/
UpperSemicontinuous.add : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_5} [inst_1 : AddCommMonoid γ] [inst_2 : LinearOrder γ]
  [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f g : α → γ},
  UpperSemicontinuous f → UpperSemicontinuous g → UpperSemicontinuous fun z => f z + g z
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_dirac : ∀ {E : Type u_3} [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace ℝ E]
  [OpensMeasurableSpace E] {x : E} (t : E),
  MeasureTheory.charFun (MeasureTheory.Measure.dirac x) t = Complex.exp (↑(inner ℝ x t) * Complex.I)
-- Std.Data.ByteSlice
/-- Converts a byte slice back to a byte array by copying the relevant portion.
 -/
ByteSlice.toByteArray : ByteSlice → ByteArray
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
instCompleteSpaceSubtypeMemClosedSubmodule : ∀ {𝕜 : Type u_6} {H : Type u_7} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid H] [inst_2 : UniformSpace H]
  [inst_3 : Module 𝕜 H] [CompleteSpace H] (K : ClosedSubmodule 𝕜 H), CompleteSpace ↥K
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_isOpenImmersion : ∀ {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y.toPresheafedSpace)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom Y f)
-- Mathlib.Combinatorics.Enumerative.InclusionExclusion
Finset.prod_indicator_biUnion_sub_indicator : ∀ {ι : Type u_1} {α : Type u_2} {s : Finset ι},
  s.Nonempty → ∀ (S : ι → Set α) (a : α), ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0
-- Mathlib.Order.Filter.Lift
Filter.lift'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : Filter α) (h : Set α → Set β), f.lift' h = f.lift (Filter.principal ∘ h)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- **Alias** of the reverse direction of `completeSpace_iff_isComplete_range`. -/
IsUniformInducing.completeSpace : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → IsComplete (Set.range f) → CompleteSpace α
-- Mathlib.Tactic.Measurability
/-- The tactic `measurability?` solves goals of the form `Measurable f`, `AEMeasurable f`,
`StronglyMeasurable f`, `AEStronglyMeasurable f μ`, or `MeasurableSet s` by applying lemmas tagged
with the `measurability` user attribute, and suggests a faster proof script that can be substituted
for the tactic call in case of success.  -/
Mathlib.Tactic.measurability? : Lean.ParserDescr
-- Mathlib.Logic.Function.OfArity
/-- The definitional equality between heterogeneous functions with constant
domain and `n`-ary functions with that domain.  -/
Function.FromTypes.fromTypes_fin_const_equiv : (α β : Type u) → (n : ℕ) → Function.FromTypes (fun x => α) β ≃ Function.OfArity α β n
-- Mathlib.Tactic.Bound
/-- Close numerical and other goals with `linarith`  -/
Mathlib.Tactic.Bound.boundLinarith : Aesop.RuleTac
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a b : α} {fallback : β},
  (a == b) = true → Std.DHashMap.Const.getD m a fallback = Std.DHashMap.Const.getD m b fallback
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_absolutelyContinuous : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω}, μ[|s].AbsolutelyContinuous μ
-- Mathlib.Order.Closure
/-- The identity function as a lower adjoint to itself.  -/
LowerAdjoint.id : (α : Type u_1) → [inst : Preorder α] → LowerAdjoint id
-- Mathlib.Analysis.BoundedVariation
/-- Eta-expanded form of `BoundedVariationOn.smul` -/
BoundedVariationOn.fun_smul : ∀ {α : Type u_2} [inst : LinearOrder α] {F : Type u_4} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {𝕜 : Type u_6} {f : α → 𝕜} {g : α → F} [inst_3 : NormedRing 𝕜] [inst_4 : NormedAlgebra ℝ 𝕜] [inst_5 : Module 𝕜 F]
  [NormSMulClass 𝕜 F] [IsScalarTower ℝ 𝕜 F] {s : Set α},
  BoundedVariationOn f s → BoundedVariationOn g s → BoundedVariationOn (fun i => f i • g i) s
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.lmapDomain_supported : ∀ {α : Type u_1} (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_7} (f : α → α') (s : Set α),
  Submodule.map (Finsupp.lmapDomain M R f) (Finsupp.supported M R s) = Finsupp.supported M R (f '' s)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If `f` is invariant under the action of a countable additive group `G`, and `μ`
is a `G`-invariant measure with a fundamental domain `s`, then the `essSup` of `f` restricted to
`s` is the same as that of `f` on all of its domain.  -/
MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ {f : α → ENNReal}, (∀ (γ : G) (x : α), f (γ +ᵥ x) = f x) → essSup f (μ.restrict s) = essSup f μ
-- Aesop.Rule
Aesop.RegularRule.isSafe : Aesop.RegularRule → Bool