mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.point_notMem_interior : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.points i ∉ s.interior
-- Mathlib.Topology.Order
isOpen_induced_eq : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {s : Set α},
  IsOpen s ↔ s ∈ Set.preimage f '' {s | IsOpen s}
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.cokernelBiproductιIso_inv : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J)
  [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)],
  (CategoryTheory.Limits.cokernelBiproductιIso f i).inv =
    (CategoryTheory.Limits.biproduct.isColimitToSubtype f i).desc
      (CategoryTheory.Limits.colimit.cocone
        (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.ι f i) 0))
-- Mathlib.CategoryTheory.Shift.InducedShiftSequence
CategoryTheory.Functor.ShiftSequence.induced_isoShiftZero_hom_app_obj : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D A} {G : CategoryTheory.Functor C A} (e : L.comp F ≅ G)
  (M : Type u_4) [inst_3 : AddMonoid M] [inst_4 : CategoryTheory.HasShift C M] [inst_5 : G.ShiftSequence M]
  (F' : M → CategoryTheory.Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m)
  [inst_6 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Full]
  [inst_7 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Faithful] [inst_8 : CategoryTheory.HasShift D M]
  [inst_9 : L.CommShift M] (X : C),
  (F.isoShiftZero M).hom.app (L.obj X) =
    CategoryTheory.CategoryStruct.comp ((e' 0).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((G.isoShiftZero M).hom.app X) (e.inv.app X))
-- Mathlib.Analysis.Normed.Module.Convex
convex_ball : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (a : E) (r : ℝ),
  Convex ℝ (Metric.ball a r)
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_sdiff_comm : ∀ {α : Type u_1} {s t u : Set α}, (s \ t) \ u = (s \ u) \ t
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.equiv_shift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (W : CategoryTheory.MorphismProperty C) {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [inst_5 : L.IsLocalization W]
  [inst_6 : L.CommShift M] {X Y : C} [inst_7 : W.IsCompatibleWithShift M] {a : M}
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y]
  (f : CategoryTheory.Localization.SmallShiftedHom W X Y a) (n a' : M) (h : a + n = a'),
  (CategoryTheory.Localization.SmallShiftedHom.equiv W L) (f.shift n a' h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso L n).hom.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Localization.SmallShiftedHom.equiv W L) f))
        ((CategoryTheory.shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)))
-- Mathlib.Algebra.Group.Units.Defs
/-- Additive units of an additive monoid have a zero.  -/
AddUnits.instZero : {α : Type u} → [inst : AddMonoid α] → Zero (AddUnits α)
-- Mathlib.Order.Hom.Lattice
InfHom.coe_const : ∀ (α : Type u_2) {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] (b : β),
  ⇑(InfHom.const α b) = Function.const α b
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csSup_inv : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : Group M] [MulLeftMono M] [MulRightMono M]
  {s : Set M}, s.Nonempty → BddBelow s → sSup s⁻¹ = (sInf s)⁻¹
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeftIso_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (W : C) {X Y : C}
  (f : X ≅ Y),
  (CategoryTheory.MonoidalCategory.whiskerLeftIso W f).symm = CategoryTheory.MonoidalCategory.whiskerLeftIso W f.symm
-- Mathlib.Order.Hom.Order
OrderHom.iterate_sup_le_sup_iff : ∀ {α : Type u_3} [inst : SemilatticeSup α] (f : α →o α),
  (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂) ↔
    ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
ChainComplex.isIso_homologyι₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : ChainComplex C ℕ) [inst_2 : HomologicalComplex.HasHomology K 0],
  CategoryTheory.IsIso (HomologicalComplex.homologyι K 0)
-- Init.Data.Array.Attach
Array.map_unattach : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : Array (Subtype P)} {f : α → β},
  Array.map f xs.unattach =
    Array.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
      xs
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.soln_dist_to_a : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2),
  (Polynomial.aeval a) F ≠ 0 →
    ‖soln_gen✝ hnorm - a‖ = ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The underlying monoidal category  -/
Bimod.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → {A B : CategoryTheory.Mon C} → Bimod A B → C
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.UniversallyEffectiveEquivalenceRelation.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R A : C} {p₁ p₂ : R ⟶ A} [inst_1 : SizeOf C]
  (toEffectiveEquivalenceRelation : CategoryTheory.EffectiveEquivalenceRelation p₁ p₂)
  (universally_effectiveEpi_π :
    CategoryTheory.MorphismProperty.universally (fun x x_1 f => CategoryTheory.EffectiveEpi f)
      toEffectiveEquivalenceRelation.π),
  sizeOf
      { toEffectiveEquivalenceRelation := toEffectiveEquivalenceRelation,
        universally_effectiveEpi_π := universally_effectiveEpi_π } =
    1 + sizeOf toEffectiveEquivalenceRelation
-- Mathlib.Topology.Constructible
IsRetrocompact.finsetSup : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Type u_4} {s : Finset ι} {t : ι → Set X},
  (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.sup t)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_mul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α], UniformContinuous fun p => p.1 * p.2
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.sub_eq_sub_iff_of_isAddUnit : ∀ {M : Type u_1} [inst : SubtractionMonoid M] {a b c d : M},
  AddCommute b d → IsAddUnit b → IsAddUnit d → (a - b = c - d ↔ a + d = c + b)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.one_apply : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁] (x : A₁), 1 x = x
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.toGL_inj : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (g g' : Matrix.SpecialLinearGroup n R), Matrix.SpecialLinearGroup.toGL g = Matrix.SpecialLinearGroup.toGL g' ↔ g = g'
-- Mathlib.Data.DFinsupp.Order
DFinsupp.add_eq_zero_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [∀ (i : ι), CanonicallyOrderedAdd (α i)] (f g : Π₀ (i : ι), α i), f + g = 0 ↔ f = 0 ∧ g = 0
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.toZeroHypercover_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  (E : J.OneHypercover S), E.toZeroHypercover.toPreZeroHypercover = E.toPreZeroHypercover
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.isTotallyReal_maximalRealSubfield : ∀ {K : Type u_2} [inst : Field K] [inst_1 : CharZero K] [Algebra.IsAlgebraic ℚ K],
  NumberField.IsTotallyReal ↥(NumberField.maximalRealSubfield K)
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
AlgebraicIndependent.algebraicClosure : ∀ {ι : Type u_1} {F : Type u_5} {E : Type u_6} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : ι → E},
  AlgebraicIndependent F x → AlgebraicIndependent (↥(algebraicClosure F E)) x
-- Mathlib.Algebra.Module.Rat
SMulCommClass.nnrat : ∀ {α : Type u} {M : Type v} [inst : AddCommMonoid M] [inst_1 : DistribSMul α M] [inst_2 : Module ℚ≥0 M],
  SMulCommClass ℚ≥0 α M
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.map_symm_eq_iff_eq_map : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] {L : BooleanSubalgebra α}
  {M : BooleanSubalgebra β} {e : β ≃o α},
  BooleanSubalgebra.map
        (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        L =
      M ↔
    L =
      BooleanSubalgebra.map
        (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        M
-- Mathlib.Data.Tree.Basic
BinaryTree.id_map : ∀ {α : Type u} (t : BinaryTree α), BinaryTree.map id t = t
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.inv_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] (h : X ≃ₜ X), h⁻¹ = h.symm
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.NoetherianSpace.of_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] {W V : Set α} [TopologicalSpace.NoetherianSpace ↑W],
  V ⊆ W → TopologicalSpace.NoetherianSpace ↑V
-- Init.ByCases
ite_id : ∀ {c : Prop} [inst : Decidable c] {α : Sort u_1} (t : α), (if c then t else t) = t
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionHomologyIso_inv_homologyι_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j k : ι) (hi : c.prev j = i)
  (hk : c.next j = k) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i')
  (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j'] [inst_4 : (K.restriction e).HasHomology j] {Z : C}
  (h : (K.restriction e).opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv
      (CategoryTheory.CategoryStruct.comp ((K.restriction e).homologyι j) h) =
    CategoryTheory.CategoryStruct.comp (K.homologyι j')
      (CategoryTheory.CategoryStruct.comp (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv h)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfMulEquiv_mk' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {T : Submonoid P} {Q : Type u_4} [inst_3 : CommMonoid Q]
  {k : T.LocalizationMap Q} {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T) (x : M) (y : ↥S),
  (f.mulEquivOfMulEquiv k H) (f.mk' x y) = k.mk' (j x) ⟨j ↑y, ⋯⟩
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function is monotonous.
 -/
Function.locallyFinsuppWithin.logCounting_mono : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E] {D : Function.locallyFinsupp E ℤ},
  0 ≤ D → MonotoneOn (Function.locallyFinsuppWithin.logCounting D) (Set.Ioi 0)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.UniversallyEffectiveEquivalenceRelation.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R A : C} {p₁ p₂ : R ⟶ A}
  (toEffectiveEquivalenceRelation : CategoryTheory.EffectiveEquivalenceRelation p₁ p₂)
  (universally_effectiveEpi_π :
    CategoryTheory.MorphismProperty.universally (fun x x_1 f => CategoryTheory.EffectiveEpi f)
      toEffectiveEquivalenceRelation.π)
  (toEffectiveEquivalenceRelation_1 : CategoryTheory.EffectiveEquivalenceRelation p₁ p₂)
  (universally_effectiveEpi_π_1 :
    CategoryTheory.MorphismProperty.universally (fun x x_1 f => CategoryTheory.EffectiveEpi f)
      toEffectiveEquivalenceRelation_1.π),
  ({ toEffectiveEquivalenceRelation := toEffectiveEquivalenceRelation,
        universally_effectiveEpi_π := universally_effectiveEpi_π } =
      { toEffectiveEquivalenceRelation := toEffectiveEquivalenceRelation_1,
        universally_effectiveEpi_π := universally_effectiveEpi_π_1 }) =
    (toEffectiveEquivalenceRelation = toEffectiveEquivalenceRelation_1)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.hom_ext_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃}
  {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
  [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄}
  {f g : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ⟶ A},
  f = g ↔
    ∀ (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j),
      CategoryTheory.CategoryStruct.comp ⋯ f = CategoryTheory.CategoryStruct.comp ⋯ g
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.smul_injective : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f]
  (s : ↥S), Function.Injective fun m => s • m
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- Type check a morphism of schemes as a morphism in `AffineScheme`.  -/
AlgebraicGeometry.AffineScheme.ofHom : {X Y : AlgebraicGeometry.Scheme} →
  [inst : AlgebraicGeometry.IsAffine X] →
    [inst_1 : AlgebraicGeometry.IsAffine Y] →
      (X ⟶ Y) → (AlgebraicGeometry.AffineScheme.of X ⟶ AlgebraicGeometry.AffineScheme.of Y)
-- Mathlib.RepresentationTheory.Basic
Representation.instIsTrivialTrivial : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V], (Representation.trivial k G V).IsTrivial
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- **Alias** of `MeasureTheory.condExp_finsetSum`. -/
MeasureTheory.condExp_finset_sum : ∀ {α : Type u_1} {E : Type u_3} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_5} {s : Finset ι} {f : ι → α → E},
  (∀ i ∈ s, MeasureTheory.Integrable (f i) μ) → ∀ (m : MeasurableSpace α), μ[∑ i ∈ s, f i | m] =ᵐ[μ] ∑ i ∈ s, μ[f i | m]
-- Mathlib.Logic.Function.Defs
Function.Bijective.comp : ∀ {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : β → φ} {f : α → β},
  Function.Bijective g → Function.Bijective f → Function.Bijective (g ∘ f)
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.mk_X_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0),
  (CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 1 = X₁
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_mono_null : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  s₁ ⊆ s₂ → μ.real s₂ = 0 → autoParam (μ s₂ ≠ ⊤) MeasureTheory.measureReal_mono_null._auto_1 → μ.real s₁ = 0
-- Mathlib.Order.UpperLower.Closure
upperClosure_sUnion : ∀ {α : Type u_1} [inst : Preorder α] (S : Set (Set α)), upperClosure (⋃₀ S) = ⨅ s ∈ S, upperClosure s
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.cont_eval_fix : ∀ {f : Turing.ToPartrec.Code} {k : Turing.ToPartrec.Cont} {v : List ℕ},
  f.Ok →
    StateTransition.eval Turing.ToPartrec.step (Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.fix f k) v) = do
      let v ← f.fix.eval v
      StateTransition.eval Turing.ToPartrec.step (Turing.ToPartrec.Cfg.ret k v)
-- Init.Data.Ord.Basic
Ordering.then'.eq_1 : ∀ (a b : Ordering), a.then' b = Ordering.rec a b a a
-- Mathlib.ModelTheory.Basic
/-- The homomorphism sends related elements to related elements  -/
FirstOrder.Language.StrongHomClass.map_rel : ∀ {L : outParam FirstOrder.Language} {F : Type u_3} {M : outParam (Type u_4)} {N : outParam (Type u_5)}
  {inst : FunLike F M N} {inst_1 : L.Structure M} {inst_2 : L.Structure N} [self : L.StrongHomClass F M N] (φ : F)
  {n : ℕ} (r : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.nat_sub : ∀ {p x : ℝ}, LiouvilleWith p x → ∀ (n : ℕ), LiouvilleWith p (↑n - x)
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.snd_iso_of_left_embedding_range_subset : ∀ {X Y S : TopCat} {f : X ⟶ S},
  Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) →
    ∀ (g : Y ⟶ S),
      Set.range ⇑(CategoryTheory.ConcreteCategory.hom g) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f) →
        CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.toAddMonoidHom_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x : M), f.toAddMonoidHom x = f x
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
/-- The exponential map $θ ↦ c + R e^{θi}$. The range of this map is the circle in `ℂ` with center
`c` and radius `|R|`.  -/
circleMap : ℂ → ℝ → ℝ → ℂ
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX_XIsoBiprod_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ j)
      (HomologicalComplex.homotopyCofiber.XIsoBiprod φ j i hij).hom =
    CategoryTheory.Limits.biprod.inr
-- Mathlib.Topology.Algebra.Ring.Basic
/-- In a topological semiring, the right-multiplication `AddMonoidHom` is continuous.  -/
mulRight_continuous : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocRing R] [IsSemitopologicalRing R] (x : R),
  Continuous ⇑(AddMonoidHom.mulRight x)
-- Mathlib.Computability.StateTransition
/-- Reflexivity of `EvalsToInTime` in 0 steps.  -/
StateTransition.EvalsToInTime.refl : {σ : Type u_1} → (f : σ → Option σ) → (a : σ) → StateTransition.EvalsToInTime f a (some a) 0
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.disjoint_closure_of_disjoint_support : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {S T : Set (Equiv.Perm α)},
  (∀ a ∈ S, ∀ b ∈ T, Disjoint a.support b.support) → Disjoint (Subgroup.closure S) (Subgroup.closure T)
-- Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_homEquiv : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.eHomEquiv C) f = CategoryTheory.MonoidalClosed.curry' f
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.atBot_basis' : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] (a : α), Filter.atBot.HasBasis (fun x => x ≤ a) Set.Iic
-- Init.Data.Array.Lemmas
Array.decide_exists_mem : ∀ {α : Type u_1} {xs : Array α} {p : α → Prop} [inst : DecidablePred p],
  decide (∃ x ∈ xs, p x) = xs.any fun b => decide (p b)
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
Real.eulerMascheroniConstant_eq_neg_deriv : Real.eulerMascheroniConstant = -deriv Real.Gamma 1
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.supportsStmt_move : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} {S : Finset (Turing.TM1to1.Λ' Γ Λ σ)} {d : Turing.Dir}
  {q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ},
  Turing.TM1.SupportsStmt S (Turing.TM1to1.move n d q) = Turing.TM1.SupportsStmt S q
-- Mathlib.Data.Fin.FlagRange
/-- Let `f : Fin (n + 1) → α` be an `(n + 1)`-tuple `(f₀, …, fₙ)` such that
- `f₀ = ⊥` and `fₙ = ⊤`;
- `fₖ₊₁` weakly covers `fₖ` for all `0 ≤ k < n`;
  this means that `fₖ ≤ fₖ₊₁` and there is no `c` such that `fₖ<c<fₖ₊₁`.

Then the range of `f` is a maximal chain.  -/
IsMaxChain.range_fin_of_covBy : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {n : ℕ} {f : Fin (n + 1) → α},
  f 0 = ⊥ →
    f (Fin.last n) = ⊤ → (∀ (k : Fin n), f k.castSucc ⩿ f k.succ) → IsMaxChain (fun x1 x2 => x1 ≤ x2) (Set.range f)
-- Aesop.Tree.Data
_private.Aesop.Tree.Data.0.Aesop.Iteration.ofNat : ℕ → Aesop.Iteration
-- Mathlib.Topology.Maps.Basic
isClosedMap_iff_closure_image : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f ↔ ∀ (s : Set X), closure (f '' s) ⊆ f '' closure s
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.one_coe_eq_one : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne], ⇑1 = 1
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicatorHom.eq_1 : ∀ {α : Type u_6} (M : Type u_7) [inst : MulOneClass M] (s : Set α),
  Set.mulIndicatorHom M s = { toFun := s.mulIndicator, map_one' := ⋯, map_mul' := ⋯ }
-- Init.Data.UInt.Lemmas
UInt16.pos_iff_ne_zero : ∀ {a : UInt16}, 0 < a ↔ a ≠ 0
-- Init.Omega.Int
Lean.Omega.Int.ofNat_snd_mk : ∀ {α : Type u_1} {x : α} {y : ℕ}, ↑(x, y).2 = ↑y
-- Mathlib.Analysis.Complex.Circle
Circle.exp_intCast_mul : ∀ (x : ℝ) (z : ℤ), Circle.exp (↑z * x) = Circle.exp x ^ z
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.toList_riiIter : ∀ {α : Type u_1} {β : α → Type u_2} {t : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.riiIterator t).toList = t.toList