mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Any.eq_2 : ∀ {α : Type u_1} (p : α → Prop) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  RBTree.RBNode.Any p (RBTree.RBNode.node c l v r) = (p v ∨ RBTree.RBNode.Any p l ∨ RBTree.RBNode.Any p r)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instRingOfMulOpposite : {M : Type u_1} → [Ring Mᵐᵒᵖ] → Ring Mᵈᵐᵃ
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_sub : ∀ {k : Type u_1} {G : Type u_2} [inst : AddGroup k] (a b : SkewMonoidAlgebra k G), (a - b).coeff = a.coeff - b.coeff
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- Hamiltonian paths are paths.  -/
SimpleGraph.Walk.IsHamiltonian.isPath : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b}, p.IsHamiltonian → p.IsPath
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.IntFractPair.exists_nth_stream_eq_none_of_rat : ∀ (q : ℚ), ∃ n, GenContFract.IntFractPair.stream q n = none
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The category of functors `WithTerminal C ⥤ D` is equivalent to the category
`Comma (𝟭 (C ⥤ D)) (const C) `.  -/
CategoryTheory.WithTerminal.equivComma : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Functor (CategoryTheory.WithTerminal C) D ≌
          CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C)
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.cardHom_apply : ∀ {α : Type u_1} (a : Multiset α), Multiset.cardHom a = a.card
-- Init.Data.Order.LemmasExtra
Std.instLawfulBEqOrdOfLawfulOrderOrdOfLawfulOrderBEq : ∀ {α : Type u} [inst : Ord α] [inst_1 : BEq α] [inst_2 : LE α] [Std.LawfulOrderOrd α] [Std.LawfulOrderBEq α],
  Std.LawfulBEqOrd α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.nonsingular_iff : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} (x y : R),
  W.Nonsingular x y ↔ W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ y ≠ -y - W.a₁ * x - W.a₃)
-- Mathlib.Order.Interval.Lex
NonemptyInterval.instLTLex : {α : Type u_1} → [LT α] → [inst : LE α] → LT (Lex (NonemptyInterval α))
-- Mathlib.Tactic.Linter.Multigoal
/-- `getManyGoals t` returns the syntax nodes of the `InfoTree` `t` corresponding to tactic calls
which
* leave at least one goal that was present before it ran
  (with the exception of tactics that leave the sole goal unchanged);
* are not excluded through `exclusions` or `ignoreBranch`;

together with the number of goals before the tactic,
the number of goals after the tactic, and the number of unaffected goals.
 -/
_private.Mathlib.Tactic.Linter.Multigoal.0.Mathlib.Linter.Style.multiGoal.getManyGoals : Lean.Elab.InfoTree → Array (Lean.Syntax × ℕ × ℕ × ℕ)
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_subset_Ioo_left : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₁ < a₂ → Set.Ico a₂ b ⊆ Set.Ioo a₁ b
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mapRingHom.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] {S : Type u_7} [inst_1 : CommSemiring S] (f : R →+* S),
  CommRing.Pic.mapRingHom f = CommRing.Pic.mapAlgebra R S
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} [inst_1 : Inhabited (β k)], k ∉ m₁ → (m₁ ∪ m₂).get! k = m₂.get! k
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Differentiable.sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ},
  Differentiable ℝ f → Differentiable ℝ fun x => Real.sinh (f x)
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
panicking if no such pair exists.
 -/
Std.ExtDTreeMap.getEntryGT! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited (Sigma β)] → Std.ExtDTreeMap α β cmp → α → (a : α) × β a
-- Mathlib.Dynamics.OmegaLimit
instInhabitedElemSetSets : {τ : Type u_1} → (f : Filter τ) → Inhabited ↑f.sets
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {e : OpenPartialHomeomorph M H},
  e ∈ IsManifold.maximalAtlas I 1 M →
    x ∈ e.source →
      (MDiffAt[s] f x ↔ MDiffAt[↑(e.extend I).symm ⁻¹' s ∩ Set.range ↑I] (f ∘ ↑(e.extend I).symm) (↑(e.extend I) x))
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivWithinAt.fun_sum : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F},
  (∀ i ∈ u, HasDerivWithinAt (A i) (A' i) s x) → HasDerivWithinAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) s x
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.mk.inj : ∀ {R : Type u} {inst : CommRing R} {M : Type v} {inst_1 : AddCommGroup M} {inst_2 : Module R M} {k : ℕ}
  {toSubmodule : Submodule R M} {finite_quotient : Module.Finite R (M ⧸ toSubmodule)}
  {projective_quotient : Module.Projective R (M ⧸ toSubmodule)}
  {rankAtStalk_eq : ∀ (p : PrimeSpectrum R), Module.rankAtStalk (M ⧸ toSubmodule) p = k} {toSubmodule_1 : Submodule R M}
  {finite_quotient_1 : Module.Finite R (M ⧸ toSubmodule_1)}
  {projective_quotient_1 : Module.Projective R (M ⧸ toSubmodule_1)}
  {rankAtStalk_eq_1 : ∀ (p : PrimeSpectrum R), Module.rankAtStalk (M ⧸ toSubmodule_1) p = k},
  { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
        rankAtStalk_eq := rankAtStalk_eq } =
      { toSubmodule := toSubmodule_1, finite_quotient := finite_quotient_1,
        projective_quotient := projective_quotient_1, rankAtStalk_eq := rankAtStalk_eq_1 } →
    toSubmodule = toSubmodule_1
-- Lean.Data.Options
Lean.MonadOptions : (Type → Type) → Type
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the forward direction of `uniqueMDiffOn_iff_uniqueDiffOn`. -/
UniqueMDiffOn.uniqueDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, UniqueMDiff[s] → UniqueDiffOn 𝕜 s
-- Init.Data.Option.Lemmas
Option.choice_eq_none_iff_not_nonempty : ∀ {α : Type u_1}, Option.choice α = none ↔ ¬Nonempty α
-- Mathlib.Topology.Sheaves.Sheafify
/-- The sheafification of a `Type`-valued presheaf, defined as the functions into the stalks which
are locally equal to germs.
 -/
TopCat.Presheaf.sheafify : {X : TopCat} → TopCat.Presheaf (Type v) X → TopCat.Sheaf (Type v) X
-- Mathlib.Topology.ContinuousMap.Compact
/-- The pointwise distance is controlled by the distance between functions, by definition.  -/
ContinuousMap.dist_apply_le_dist : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  {f g : C(α, β)} (x : α), dist (f x) (g x) ≤ dist f g
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.step_flatMap : ∀ {α β α₂ γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] {f : β → Std.Iter γ}
  {it₁ : Std.Iter β},
  (Std.Iter.flatMap f it₁).step =
    match it₁.step with
    | ⟨Std.IterStep.yield it₁' b, h⟩ => Std.PlausibleIterStep.skip (Std.Iter.flatMapAfter f it₁' (some (f b))) ⋯
    | ⟨Std.IterStep.skip it₁', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.flatMapAfter f it₁' none) ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
-- Mathlib.LinearAlgebra.Complex.Module
realPart_apply_coe : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  (a : A), ↑(realPart a) = 2⁻¹ • (a + star a)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A non-standard definition of the `n`-skeleton of a CW complex for `n ∈ ℕ ∪ {∞}`.
This allows the base case of induction to be about the base instead of being about the union of
the base and some points.
The standard `skeleton` is defined in terms of `skeletonLT`. `skeletonLT` is preferred
in statements. You should then derive the statement about `skeleton`.  -/
Topology.RelCWComplex.skeletonLT : {X : Type u_1} →
  [t : TopologicalSpace X] →
    [T2Space X] →
      (C : Set X) → {D : Set X} → [inst : Topology.RelCWComplex C D] → ℕ∞ → Topology.RelCWComplex.Subcomplex C
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  P.fullsubcategory.mapComp f g = CategoryTheory.Cat.Hom.isoMk (P.mapComp f g)
-- Mathlib.Topology.Algebra.Group.Basic
Filter.HasBasis.nhds_of_zero : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {ι : Sort u_1} {p : ι → Prop}
  {s : ι → Set G}, (nhds 0).HasBasis p s → ∀ (x : G), (nhds x).HasBasis p fun i => {y | y - x ∈ s i}
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.η_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Grp.forget₂Mon C) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Grp.forget₂Mon C).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Grp C)))
-- Mathlib.GroupTheory.Divisible
/-- If `f : A → B` is a surjective homomorphism and `A` is `α`-divisible, then `B` is also
`α`-divisible.  -/
Function.Surjective.divisibleBy : {A : Type u_1} →
  {B : Type u_2} →
    {α : Type u_3} →
      [inst : Zero α] →
        [inst_1 : AddMonoid A] →
          [inst_2 : AddMonoid B] →
            [inst_3 : SMul α A] →
              [inst_4 : SMul α B] →
                [DivisibleBy A α] →
                  (f : A → B) → Function.Surjective f → (∀ (a : A) (n : α), f (n • a) = n • f a) → DivisibleBy B α
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.lift_comp_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P), (Monoid.Coprod.lift f g).comp Monoid.Coprod.inl = f
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.add_eq_sup : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p q : Submodule R M), p + q = p ⊔ q
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.instPowReal : Pow NNReal ℝ
-- Init.Data.UInt.Lemmas
UInt32.one_mul : ∀ (a : UInt32), 1 * a = a
-- Init.Data.SInt.Bitwise
Int64.not_inj : ∀ {a b : Int64}, ~~~a = ~~~b ↔ a = b
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
Lean.Meta.Grind.Arith.Linear.isHomoMulInst : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr → Bool
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β k}, (t.insert k v).get k ⋯ = v
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.lid_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M),
  (TensorProduct.lid R M).symm m = 1 ⊗ₜ[R] m
-- Mathlib.Data.Set.Function
Set.prod_surjOn_snd : ∀ {β₁ : Type u_8} {β₂ : Type u_9} {t₁ : Set β₁} {t₂ : Set β₂}, t₁.Nonempty → Set.SurjOn Prod.snd (t₁ ×ˢ t₂) t₂
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given Localization maps `f : M →+ N` for a Submonoid `S ⊆ M` and
`k : M →+ Q` for a Submonoid `T ⊆ M`, such that `S ≤ T`, and we have
`l : M →+ A`, the composition of the induced map `f.lift` for `k` with
the induced map `k.lift` for `l` is equal to the induced map `f.lift` for `l`  -/
AddSubmonoid.LocalizationMap.lift_comp_lift : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {T : AddSubmonoid M} (hST : S ≤ T) {Q : Type u_4} [inst_2 : AddCommMonoid Q]
  (k : T.LocalizationMap Q) {A : Type u_5} [inst_3 : AddCommMonoid A] {l : M →+ A} (hl : ∀ (w : ↥T), IsAddUnit (l ↑w)),
  (k.lift hl).comp (f.lift ⋯) = f.lift ⋯
-- Mathlib.Data.Nat.Cast.Commute
Nat.addCommute_cast : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (m n : ℕ), AddCommute ↑m ↑n
-- Mathlib.Order.SuccPred.Basic
Order.le_pred_iff_of_not_isMin' : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, ¬IsMin b → (b ≤ Order.pred a ↔ b < a)
-- Mathlib.Algebra.Homology.Localization
HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C]
  [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization],
  (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy HomologicalComplexUpToQuasiIso.Q
-- Mathlib.Algebra.Order.CauSeq.Basic
IsCauSeq.bounded' : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β},
  IsCauSeq abv f → ∀ (x : α), ∃ r > x, ∀ (i : ℕ), abv (f i) < r
-- Mathlib.Topology.Order.Real
EReal.instTopologicalSpace : TopologicalSpace EReal
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry?.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))),
  x = Std.DTreeMap.Internal.Impl.leaf →
    (match x with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
      | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
        h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h) ≍
      h_1 ()
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The empty word `[]` only reduces to itself.  -/
FreeAddGroup.Red.nil_iff : ∀ {α : Type u} {L : List (α × Bool)}, FreeAddGroup.Red [] L ↔ L = []
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_iff_isSome_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  a ∈ t ↔ (t.getKey? a).isSome = true
-- Mathlib.NumberTheory.Height.NumberField
/-- The multiplicative height of a rational number is the maximum of the absolute value of
its numerator and its denominator.  -/
Rat.mulHeight₁_eq_max : ∀ (q : ℚ), Height.mulHeight₁ q = ↑(max q.num.natAbs q.den)
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_succ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (h : autoParam (n + (i + 1) = m) CategoryTheory.SimplicialObject.σ₀Iter_succ._auto_1) {Z : C}
  (h_1 : X.obj (Opposite.op { len := m }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.σ₀Iter (i + 1) h) h_1 =
    CategoryTheory.CategoryStruct.comp (X.σ 0) (CategoryTheory.CategoryStruct.comp (X.σ₀Iter i ⋯) h_1)
-- Mathlib.Topology.Order.LowerUpperTopology
/-- If `α` is equipped with the lower topology, then it is homeomorphic to `WithLower α`.
 -/
Topology.IsLower.withLowerHomeomorph : {α : Type u_1} → [inst : Preorder α] → [inst_1 : TopologicalSpace α] → [Topology.IsLower α] → Topology.WithLower α ≃ₜ α
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.setLIntegral_deterministic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} {a : α}
  (hg : Measurable g) [MeasurableSingletonClass β] (s : Set β) [inst : Decidable (g a ∈ s)],
  ∫⁻ (x : β) in s, f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0
-- Mathlib.Order.Bounds.Basic
IsCofinalFor.union_left : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, IsCofinalFor s t → IsCofinalFor (s ∪ t) t
-- Init.Data.List.Zip
List.zipWith_map : ∀ {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {β : Type u_4} {μ : Type u_5} {f : γ → δ → μ} {g : α → γ} {h : β → δ}
  {l₁ : List α} {l₂ : List β},
  List.zipWith f (List.map g l₁) (List.map h l₂) = List.zipWith (fun a b => f (g a) (h b)) l₁ l₂
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.singleton_prod_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α) (y : β),
  {x} ×ˢ {y} = {(x, y)}
-- Mathlib.Condensed.Light.InternallyProjective
LightCondensed.ihomPoints_apply : ∀ (R : Type u) [inst : CommRing R] (A B : LightCondMod R) (S : LightProfinite) (x : ↑((A ⟹ B).obj.obj (Opposite.op S))),
  (LightCondensed.ihomPoints R A B S) x =
    CategoryTheory.MonoidalClosed.uncurry
      (((LightCondensed.freeForgetAdjunction R).homEquiv ((CategoryTheory.coherentTopology LightProfinite).yoneda.obj S)
            (A ⟹ B)).symm
        ((CategoryTheory.coherentTopology LightProfinite).yonedaEquiv.symm x))
-- Lean.Meta.InferType
/-- Ensure `MetaM` configuration is strong enough for inferring/checking types.
For example, `beta := true` is essential when type checking.

Remark: we previously used the default configuration here, but this is problematic
because it overrides unrelated configurations.
 -/
Lean.Meta.withInferTypeConfig : {α : Type} → Lean.MetaM α → Lean.MetaM α
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_mono : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] {f : F}
  {I J : Ideal R}, I ≤ J → Ideal.map f I ≤ Ideal.map f J
-- Mathlib.Order.Hom.Basic
OrderHom.dual_id : ∀ {α : Type u_2} [inst : Preorder α], OrderHom.dual OrderHom.id = OrderHom.id
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
groupCohomology.δ.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) (i j : ℕ) (hij : i + 1 = j), groupCohomology.δ hX i j hij = groupCohomology.δ hX i j hij
-- Mathlib.Combinatorics.Graph.Delete
Graph.edgeSet_restrict : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (E₀ : Set β), (G.restrict E₀).edgeSet = G.edgeSet ∩ E₀
-- Mathlib.RingTheory.HahnSeries.Basic
/-- The coefficient function of a Hahn Series.  -/
HahnSeries.coeff : {Γ : Type u_1} → {R : Type u_2} → [inst : PartialOrder Γ] → [inst_1 : Zero R] → HahnSeries Γ R → Γ → R
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.instMonadNormalExprMonoidalM : Mathlib.Tactic.BicategoryLike.MonadNormalExpr Mathlib.Tactic.Monoidal.MonoidalM
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instEssentiallySmallTopOfEssentiallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} ⊤
-- Init.Data.String.Basic
String.Pos.byteIdx_lt_utf8ByteSize : ∀ {s : String} (p : s.Pos), p ≠ s.endPos → p.offset.byteIdx < s.utf8ByteSize
-- Lean.Util.ParamMinimizer
Lean.Util.ParamMinimizer.Status.approx.sizeOf_spec : sizeOf Lean.Util.ParamMinimizer.Status.approx = 1
-- Mathlib.Order.CompleteLattice.Basic
iSup_ite : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (p : ι → Prop) [inst_1 : DecidablePred p] (f g : ι → α),
  (⨆ i, if p i then f i else g i) = (⨆ i, ⨆ (_ : p i), f i) ⊔ ⨆ i, ⨆ (_ : ¬p i), g i
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- The Legendre symbol of `a : ℤ` and a prime `p`, `legendreSym p a`,
is an integer defined as

* `0` if `a` is `0` modulo `p`;
* `1` if `a` is a nonzero square modulo `p`
* `-1` otherwise.

Note the order of the arguments! The advantage of the order chosen here is
that `legendreSym p` is a multiplicative function `ℤ → ℤ`.
 -/
legendreSym : (p : ℕ) → [Fact (Nat.Prime p)] → ℤ → ℤ
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvex_closed_sInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] [inst_4 : TopologicalSpace E] {S : Set (Set E)},
  (∀ s ∈ S, AbsConvex 𝕜 s ∧ IsClosed s) → AbsConvex 𝕜 (⋂₀ S) ∧ IsClosed (⋂₀ S)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instRingOfAddOpposite : {M : Type u_1} → [Ring Mᵃᵒᵖ] → Ring Mᵈᵃᵃ
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.isOpen_inter_nonempty_of_isOpen : ∀ {α : Type u_1} [inst : UniformSpace α] {s : Set α}, IsOpen s → IsOpen {t | (↑t ∩ s).Nonempty}
-- Mathlib.Order.WithBot
WithTop.comp_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (x : WithTop α),
  WithTop.map (h ∘ g) x = WithTop.map h (WithTop.map g x)
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf_assoc : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) (i : ι)
  {Z : CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ (Type u)} (h : F.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.yoneda.map (AlgebraicGeometry.Scheme.LocalRepresentability.toGlued hf i))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf).hom
        h) =
    CategoryTheory.CategoryStruct.comp (f i) h
-- Mathlib.Analysis.Seminorm
Seminorm.ball_finset_sup_eq_iInter : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ},
  0 < r → (s.sup p).ball x r = ⋂ i ∈ s, (p i).ball x r
-- Mathlib.Data.Finset.Lattice.Fold
Finset.exists_inf_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf β] [inst_1 : OrderTop β] [WellFoundedLT β] (f : α → β),
  ∃ t, ∀ (a : α), t.inf f ≤ f a
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- The morphism `ιObj I κ f` is a relative `I`-cell complex.  -/
CategoryTheory.SmallObject.relativeCellComplexιObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [inst_3 : I.IsCardinalForSmallObjectArgument κ] →
              {X Y : C} →
                (f : X ⟶ Y) →
                  HomotopicalAlgebra.RelativeCellComplex (fun x => I.homFamily) (CategoryTheory.SmallObject.ιObj I κ f)