mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.Main
_private.Lean.Elab.InfoTree.Main.0.Lean.Elab.formatStxRange.fmtPos : Lean.Elab.ContextInfo → String.Pos.Raw → Lean.SourceInfo → Std.Format
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_mapEquiv_iff' : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] (f : M ≃L[R] N) (s : ClosedSubmodule R M) (x : M), f x ∈ (ClosedSubmodule.mapEquiv f) s ↔ x ∈ s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.isLocalExtr_T_real : ∀ {n k : ℕ},
  n ≠ 0 →
    0 < k →
      k < n → IsLocalExtr (fun x => Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n)) (Real.cos (↑k * Real.pi / ↑n))
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.trivial_X_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.Bimon.trivial C).X.X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.isArtinianObject.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.isArtinianObject X = WellFoundedLT (CategoryTheory.Subobject X)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_mem_Ioc : ∀ (z : ℂ), z.arg ∈ Set.Ioc (-Real.pi) Real.pi
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_comm : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] {s : Finset β} {t : Finset γ} (hs : s.Nonempty)
  (ht : t.Nonempty) (f : β → γ → α), (s.sup' hs fun b => t.sup' ht (f b)) = t.sup' ht fun c => s.sup' hs fun b => f b c
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_eq_mk_of_mulArchimedean : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M}
  [MulArchimedean M], a ≠ 1 → b ≠ 1 → MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
-- Mathlib.Logic.Equiv.Set
/-- A set is equivalent to its image under an equivalence.
 -/
Equiv.image : {α : Type u_3} → {β : Type u_4} → (e : α ≃ β) → (s : Set α) → ↑s ≃ ↑(⇑e '' s)
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange_id : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (g : α →₀ M), Finsupp.mapRange id ⋯ g = g
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.IsMonoidalLeftDistrib.preservesBinaryCoproducts_tensorLeft : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C} [self : CategoryTheory.IsMonoidalLeftDistrib C] (X : C),
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)
    (CategoryTheory.MonoidalCategory.tensorLeft X)
-- Mathlib.RingTheory.Polynomial.Quotient
Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f : Polynomial R),
  I.polynomialQuotientEquivQuotientPolynomial (Polynomial.map (Ideal.Quotient.mk I) f) =
    (Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
/-- `x^n`, `n : ℕ` is strictly convex on `[0, +∞)` for all `n` greater than `2`.  -/
strictConvexOn_pow : ∀ {n : ℕ}, 2 ≤ n → StrictConvexOn ℝ (Set.Ici 0) fun x => x ^ n
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Restrict an algebra homomorphism between fields to an algebra isomorphism  -/
AlgEquiv.ofInjectiveField : {R : Type u} →
  [inst : CommSemiring R] →
    {E : Type u_1} →
      {F : Type u_2} →
        [inst_1 : DivisionRing E] →
          [inst_2 : Semiring F] →
            [Nontrivial F] → [inst_4 : Algebra R E] → [inst_5 : Algebra R F] → (f : E →ₐ[R] F) → E ≃ₐ[R] ↥f.range
-- Mathlib.Data.Set.Function
Set.InjOn.left_prodMk : ∀ {α : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s : Set α} {f₁ : α → β₁} {f₂ : α → β₂},
  Set.InjOn f₁ s → Set.InjOn (fun x => (f₁ x, f₂ x)) s
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.parse.go : Lean.TSyntax `mrefinePat → Option Lean.Parser.Tactic.MRefinePat
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inr_smul : ∀ {S : Type u_2} (R : Type u) {M : Type v} [inst : Zero R] [inst_1 : SMulZeroClass S R] [inst_2 : SMul S M] (r : S)
  (m : M), TrivSqZeroExt.inr (r • m) = r • TrivSqZeroExt.inr m
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_iff_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a : α}, a ∈ t ↔ (t.getKey? a).isSome = true
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.toList.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] (r r_1 : Std.Rci α), r = r_1 → r.toList = r_1.toList
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.inter_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp}, t₁.inter t₂ = t₁ ∩ t₂
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.prop.fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C}
  {f : X ⟶ Y} (hf : Φ.prop f) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f h =
    CategoryTheory.CategoryStruct.comp (Φ.toSucc X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)
-- Mathlib.Algebra.Lie.DirectSum
DFinsupp.lapply.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] (i : ι),
  DFinsupp.lapply i = { toFun := fun f => f i, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.map.eq_2 : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (v_3 : V)
  (h : G.Adj u v_3) (p : G.Walk v_3 v),
  SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h p) = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map f p)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.instBraidedForallPi' : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [inst_2 : (i : I) → CategoryTheory.BraidedCategory (C i)] →
          {D : Type u_1} →
            [inst_3 : CategoryTheory.Category.{v_1, u_1} D] →
              [inst_4 : CategoryTheory.MonoidalCategory D] →
                [inst_5 : CategoryTheory.BraidedCategory D] →
                  (F : (i : I) → CategoryTheory.Functor D (C i)) →
                    [(i : I) → (F i).Braided] → (CategoryTheory.Functor.pi' F).Braided
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_eq_biInter_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) (x : E) (r : ℝ), p.closedBall x r = ⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ
-- Mathlib.Order.Category.HeytAlg
HeytAlg.str : (self : HeytAlg) → HeytingAlgebra ↑self
-- Init.SimpLemmas
or_iff_right_iff_imp : ∀ {a b : Prop}, (a ∨ b ↔ b) ↔ a → b
-- Mathlib.Order.Filter.Map
Filter.map_swap_eq_comap_swap : ∀ {α : Type u_1} {β : Type u_2} {f : Filter (α × β)}, Filter.map Prod.swap f = Filter.comap Prod.swap f
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The characterization of weak convergence of finite measures by the condition that the
integrals of every continuous bounded nonnegative function are continuous.  -/
MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_lintegral : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {X : Type u_2} [inst_3 : TopologicalSpace X] {μs : X → MeasureTheory.FiniteMeasure Ω},
  Continuous μs ↔ ∀ (f : BoundedContinuousFunction Ω NNReal), Continuous fun x => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs x)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.completeFamily.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (i : NumberField.InfinitePlace K),
  NumberField.mixedEmbedding.fundamentalCone.completeFamily K i =
    if hi : i = NumberField.Units.dirichletUnitTheorem.w₀ then fun w => ↑w.mult
    else
      ↑NumberField.mixedEmbedding.fundamentalCone.expMap.symm
        (NumberField.mixedEmbedding.normAtAllPlaces
          ((NumberField.mixedEmbedding K)
            ((algebraMap (NumberField.RingOfIntegers K) K)
              ↑(NumberField.Units.fundSystem K
                  (NumberField.mixedEmbedding.fundamentalCone.equivFinRank.symm ⟨i, hi⟩)))))
-- Mathlib.Algebra.RingQuot
/-- The quotient map from a ring to its quotient, as a homomorphism of rings.
 -/
RingQuot.mkRingHom : {R : Type u_1} → [inst : Semiring R] → (r : R → R → Prop) → R →+* RingQuot r
-- Lean.Meta.Basic
Lean.Meta.modifyCache : (Lean.Meta.Cache → Lean.Meta.Cache) → Lean.MetaM Unit
-- Mathlib.Util.WhatsNew
_private.Mathlib.Util.WhatsNew.0.Mathlib.WhatsNew.mkHeader' : String → Lean.Name → List Lean.Name → Lean.Expr → Bool → Lean.CoreM Lean.MessageData
-- Mathlib.GroupTheory.OrderOfElement
Subgroup.zpowers_eq_zpowers_iff : ∀ {G : Type u_1} [inst : Group G] {x y : G},
  ¬IsOfFinOrder x → (Subgroup.zpowers x = Subgroup.zpowers y ↔ x = y ∨ x⁻¹ = y)
-- Lean.Environment
/-- Elaboration-specific extension of `Kernel.Environment` that adds tracking of asynchronously
elaborated declarations.
 -/
Lean.Environment : Type
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_subtype : ∀ {α : Sort u_1} (p : α → Prop), IsEmpty (Subtype p) ↔ ∀ (x : α), ¬p x
-- Mathlib.Algebra.Tropical.Basic
Tropical.instCommSemigroupTropical : {R : Type u} → [AddCommSemigroup R] → CommSemigroup (Tropical R)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.mk : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : PseudoEMetricSpace X] →
      [inst_1 : PseudoEMetricSpace Y] →
        (toEquiv : X ≃ Y) →
          (∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv.toFun x) (toEquiv.toFun y) = ↑r * edist x y) → X ≃ᵈ Y
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instIsStarNormal : ∀ (R : Type u_1) {A : Type u_2} [inst : Semiring R] [inst_1 : StarAddMonoid R] [inst_2 : Star A]
  [inst_3 : AddCommMonoid A] [inst_4 : Mul A] [inst_5 : SMulWithZero R A] (a : A) [IsStarNormal a], IsStarNormal ↑a
-- Mathlib.Topology.CompactOpen
ContinuousMap.coe_homeoFnOfDiscrete : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : DiscreteTopology X],
  ⇑ContinuousMap.homeoFnOfDiscrete = DFunLike.coe
-- Mathlib.RingTheory.FilteredAlgebra.Basic
/-- For a family of subsets `σ` of `A`, an increasing series of `F` in `σ` is a filtration if
there is another series `F_lt` in `σ` equal to the supremum of `F` with smaller index.

In the intended applications, `σ` is a complete lattice, and `F_lt` is uniquely-determined as
`F_lt j = ⨆ i < j, F i`. Thus `F_lt` is an implementation detail which allows us defer depending
on a complete lattice structure on `σ`. It also provides the ancillary benefit of giving us better
definition control. This is convenient e.g., when the index is `ℤ`.  -/
IsFiltration : {ι : Type u_1} → {σ : Type u_3} → [Preorder ι] → [Preorder σ] → (ι → σ) → outParam (ι → σ) → Prop
-- Mathlib.Algebra.Order.Monoid.Prod
Prod.instIsOrderedCancelMonoid : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelMonoid α]
  [inst_3 : CommMonoid β] [inst_4 : Preorder β] [IsOrderedCancelMonoid β], IsOrderedCancelMonoid (α × β)
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.zoom.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode.Path α → Sort u_2) (path : RBTree.RBNode.Path α)
  (h_1 : (path : RBTree.RBNode.Path α) → motive RBTree.RBNode.nil path)
  (h_2 :
    (n : RBTree.RBNode α) →
      (c : RBTree.RBColor) →
        (a : RBTree.RBNode α) →
          (y : α) →
            (b : RBTree.RBNode α) →
              n = RBTree.RBNode.node c a y b →
                (path : RBTree.RBNode.Path α) → motive (RBTree.RBNode.node c a y b) path),
  (match RBTree.RBNode.nil, path with
    | RBTree.RBNode.nil, path => h_1 path
    | n@h:(RBTree.RBNode.node c a y b), path => h_2 n c a y b h path) =
    h_1 path
-- Mathlib.Logic.Equiv.Option
/-- A universe-polymorphic version of `EquivFunctor.mapEquiv Option e`.  -/
Equiv.optionCongr : {α : Type u_1} → {β : Type u_2} → α ≃ β → Option α ≃ Option β
-- Mathlib.CategoryTheory.Balanced
CategoryTheory.Balanced.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] [CategoryTheory.Epi f], CategoryTheory.IsIso f) →
    CategoryTheory.Balanced C
-- Mathlib.Data.Nat.Prime.Defs
Nat.Primes.inhabitedPrimes : Inhabited Nat.Primes
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
multipliableUniformlyOn_univ_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α],
  MultipliableUniformlyOn f Set.univ ↔ MultipliableUniformly f
-- Mathlib.Data.List.Palindrome
List.Palindrome.nil : ∀ {α : Type u_1}, [].Palindrome
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.State.mk.sizeOf_spec : ∀ (rings : Array Lean.Meta.Grind.Arith.CommRing.CommRing) (typeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToRingId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ) (semirings : Array Lean.Meta.Grind.Arith.CommRing.CommSemiring)
  (stypeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToSemiringId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ) (ncRings : Array Lean.Meta.Grind.Arith.CommRing.Ring)
  (exprToNCRingId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ) (nctypeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (ncSemirings : Array Lean.Meta.Grind.Arith.CommRing.Semiring)
  (exprToNCSemiringId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ)
  (ncstypeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)) (steps : ℕ) (reportedMaxDegreeIssue : Bool),
  sizeOf
      { rings := rings, typeIdOf := typeIdOf, exprToRingId := exprToRingId, semirings := semirings,
        stypeIdOf := stypeIdOf, exprToSemiringId := exprToSemiringId, ncRings := ncRings,
        exprToNCRingId := exprToNCRingId, nctypeIdOf := nctypeIdOf, ncSemirings := ncSemirings,
        exprToNCSemiringId := exprToNCSemiringId, ncstypeIdOf := ncstypeIdOf, steps := steps,
        reportedMaxDegreeIssue := reportedMaxDegreeIssue } =
    1 + sizeOf rings + sizeOf typeIdOf + sizeOf exprToRingId + sizeOf semirings + sizeOf stypeIdOf +
                      sizeOf exprToSemiringId +
                    sizeOf ncRings +
                  sizeOf exprToNCRingId +
                sizeOf nctypeIdOf +
              sizeOf ncSemirings +
            sizeOf exprToNCSemiringId +
          sizeOf ncstypeIdOf +
        sizeOf steps +
      sizeOf reportedMaxDegreeIssue
-- Mathlib.Algebra.Order.Archimedean.Basic
eq_of_forall_lt_rat_iff_lt : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K},
  (∀ (q : ℚ), x < ↑q ↔ y < ↑q) → x = y
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- Given two locally ringed spaces `X` and `Y`, an isomorphism between `X` and `Y` as _sheafed_
spaces can be lifted to a morphism `X ⟶ Y` as locally ringed spaces.

See also `isoOfSheafedSpaceIso`.
 -/
AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso : {X Y : AlgebraicGeometry.LocallyRingedSpace} →
  (f : X.toSheafedSpace ⟶ Y.toSheafedSpace) → [CategoryTheory.IsIso f] → X ⟶ Y
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.congr_of_insert : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → (∀ y ∈ insert x s, f₁ y = f y) → ContDiffWithinAt 𝕜 n f₁ s x
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a set `s` is to the left of a set `t`, and both contain the boundary point `x`, then
the variation of `f` along `s ∪ t` is the sum of the variations.  -/
eVariationOn.union : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s t : Set α}
  {x : α}, IsGreatest s x → IsLeast t x → eVariationOn f (s ∪ t) = eVariationOn f s + eVariationOn f t
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
Topology.IsClosedEmbedding.setIntegral_map_vectorMeasure : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  [inst_6 : TopologicalSpace X] [BorelSpace X] {β : Type u_7} [inst_8 : MeasurableSpace β] [inst_9 : TopologicalSpace β]
  [BorelSpace β] {φ : X → β} {f : β → E} {s : Set β},
  MeasurableSet s →
    Topology.IsClosedEmbedding φ → ∫ᵛ (y : β) in s, f y ∂[B; μ.map φ] = ∫ᵛ (x : X) in φ ⁻¹' s, f (φ x) ∂[B; μ]
-- Init.Data.List.Sort.Lemmas
List.MergeSort.Internal.splitInTwo_fst_pairwise : ∀ {α : Type u_1} {n : ℕ} {le : α → α → Prop} (l : { l // l.length = n }),
  List.Pairwise le ↑l → List.Pairwise le ↑(List.MergeSort.Internal.splitInTwo l).1
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst_apply : ∀ (X Y : Type u) (x : X × Y),
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.binaryProductIso X Y).inv) x) =
    x.1
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_real_closedBall_eq_addHaar_real_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) (r : ℝ),
  μ.real (Metric.closedBall x r) = μ.real (Metric.ball x r)
-- Mathlib.Algebra.Group.Prod
Prod.instInvolutiveNeg.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : InvolutiveNeg M] [inst_1 : InvolutiveNeg N],
  Prod.instInvolutiveNeg = { toNeg := Prod.instNeg, neg_neg := ⋯ }
-- Aesop.Tree.Data
Aesop.Rapp.children : Aesop.Rapp → Array Aesop.MVarClusterRef
-- Mathlib.Data.Fintype.Card
set_fintype_card_eq_univ_iff : ∀ {α : Type u_1} [inst : Fintype α] (s : Set α) [inst_1 : Fintype ↑s], Fintype.card ↑s = Fintype.card α ↔ s = Set.univ
-- Mathlib.Data.Fin.Tuple.Sort
/-- The sorted version of a permutation `σ` is its inverse `σ⁻¹`.  -/
Tuple.sort_perm : ∀ {n : ℕ} (σ : Equiv.Perm (Fin n)), Tuple.sort ⇑σ = σ⁻¹
-- Mathlib.Topology.EMetricSpace.Basic
instEDistSeparationQuotient : {X : Type u_1} → [inst : PseudoEMetricSpace X] → EDist (SeparationQuotient X)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_ite : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a b : α} (p : Prop) [inst_2 : Decidable p],
  |if p then a else b|ₘ = if p then |a|ₘ else |b|ₘ
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.AddConvolutionExistsAt.distrib_add : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : AddMonoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F] [T2Space F]
  [ContinuousAdd F] {f : M → E} {g g' : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F),
  DiscreteConvolution.AddConvolutionExistsAt L f g x →
    DiscreteConvolution.AddConvolutionExistsAt L f g' x →
      DiscreteConvolution.addConvolution L f (g + g') x =
        DiscreteConvolution.addConvolution L f g x + DiscreteConvolution.addConvolution L f g' x
-- Mathlib.Order.LiminfLimsup
/-- In other words, `limsup cofinite s` is the set of elements lying inside the family `s`
infinitely often.  -/
Filter.cofinite.limsup_set_eq : ∀ {α : Type u_1} {ι : Type u_4} {s : ι → Set α}, Filter.limsup s Filter.cofinite = {x | {n | x ∈ s n}.Infinite}
-- Init.Data.UInt.Lemmas
UInt32.mul_assoc : ∀ (a b c : UInt32), a * b * c = a * (b * c)
-- Mathlib.Tactic.Algebra.Basic
/-- Evaluate constants in `A` using `norm_num`.  -/
Mathlib.Tactic.Algebra.RingCompute.derive : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          (sAlg : Q(Algebra «$R» «$A»)) →
            Mathlib.Tactic.Algebra.Cache sR →
              Mathlib.Tactic.Algebra.Cache sA →
                (x : Q(«$A»)) →
                  Lean.MetaM
                    (Mathlib.Tactic.Ring.Common.Result
                      (Mathlib.Tactic.Ring.Common.ExSum (Mathlib.Tactic.Algebra.BaseType sAlg) sA) q(«$x»))
-- Mathlib.CategoryTheory.Limits.Lattice
/-- The limit of a functor from a finite diagram into a `SemilatticeInf` with `OrderTop` is the
infimum of the objects in the image.
 -/
CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf : ∀ {α : Type u} {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J]
  [inst_2 : SemilatticeInf α] [inst_3 : OrderTop α] (F : CategoryTheory.Functor J α),
  CategoryTheory.Limits.limit F = Finset.univ.inf F.obj
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.instHasFactorizationCofibrationsTrivialFibrations : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughInjectives C],
  (HomotopicalAlgebra.cofibrations (CochainComplex.Plus C)).HasFactorization
    (HomotopicalAlgebra.trivialFibrations (CochainComplex.Plus C))
-- Mathlib.NumberTheory.Padics.PadicNumbers
Rat.padicValuation_eq_zero_iff : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {x : ℚ}, (Rat.padicValuation p) x = 0 ↔ x = 0
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- A commutative square involving the morphisms `mor₃` of two distinguished triangles
can be extended as morphism of triangles  -/
CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
  T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
      ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (c : T₁.obj₃ ⟶ T₂.obj₃),
        CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) =
            CategoryTheory.CategoryStruct.comp c T₂.mor₃ →
          ∃ b,
            CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ ∧
              CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂
-- Mathlib.RingTheory.Valuation.RamificationGroup
/-- The decomposition subgroup defined as the stabilizer of the action
on the type of all valuation subrings of the field.  -/
ValuationSubring.decompositionSubgroup : (K : Type u_1) →
  {L : Type u_2} →
    [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → ValuationSubring L → Subgroup Gal(L/K)
-- Init.Data.List.Lemmas
List.or_all_distrib_left : ∀ {α : Type u_1} {l : List α} {p : α → Bool} {q : Bool}, (q || l.all p) = l.all fun a => q || p a
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instAddCommGroupOfIsTopologicalAddGroup : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddCommGroup β] → [IsTopologicalAddGroup β] → AddCommGroup (CompactlySupportedContinuousMap α β)
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.instPartialOrder : {α : Type u_3} → PartialOrder (MeasurableSpace.DynkinSystem α)