mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Sym.Sym2
Equiv.sigmaQuotientFromRel_symm_apply_coe : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (sym : Std.Symm r) {r' : Setoid β} (f : r →r ⇑r')
  (z : (b : Quotient r') × ↑(Sym2.fromRel ⋯)),
  ↑((Equiv.sigmaQuotientFromRel sym f).symm z) = Sym2.map Subtype.val ↑z.snd
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainTermGoal.mk.sizeOf_spec : ∀ (goal : String) (range : Lean.Lsp.Range), sizeOf { goal := goal, range := range } = 1 + sizeOf goal + sizeOf range
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.map_neg : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} (A' : Type u_8)
  [inst_2 : AddGroup A'] [inst_3 : DistribMulAction M A'] (B' : Type u_9) [inst_4 : AddGroup B']
  [inst_5 : DistribMulAction N B'] (f : A' →ₑ+[φ] B') (x : A'), f (-x) = -f x
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instStarSubtypePreLpMemAddSubgroup : {α : Type u_3} →
  {E : α → Type u_4} →
    {p : ENNReal} →
      [inst : (i : α) → NormedAddCommGroup (E i)] →
        [inst_1 : (i : α) → StarAddMonoid (E i)] → [∀ (i : α), NormedStarGroup (E i)] → Star ↥(lp E p)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.comp_of_natDegree_le_one_of_invertible : ∀ {R : Type u_1} [inst : CommSemiring R] {f g : Polynomial R},
  f.Splits → g.natDegree ≤ 1 → ∀ (h : Invertible g.leadingCoeff), (f.comp g).Splits
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.instNonsingularTensorObjObjSimplexCategoryStdSimplex : ∀ (n m : SimplexCategory),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj n) (SSet.stdSimplex.obj m)).Nonsingular
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative : ∀ {R : Type u} [inst : CommRing R] [NoZeroDivisors R] [CharZero R] {p : Polynomial R} {t : R} {n : ℕ},
  p ≠ 0 → (∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t) → n < Polynomial.rootMultiplicity t p
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
IsGLB.mul : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s t : Set G} {a b : G},
  IsGLB s a → IsGLB t b → IsGLB (s * t) (a * b)
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- A monoidal category with binary coproducts is right distributive
if the right tensor product functor preserves binary coproducts.  -/
CategoryTheory.IsMonoidalRightDistrib : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.MonoidalCategory C] → [CategoryTheory.Limits.HasBinaryCoproducts C] → Prop
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_smul : ∀ {α : Type u_1} {R : Type u_2} [inst : SMul R α] (c : R) (a : α), SymAlg.sym (c • a) = c • SymAlg.sym a
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_bot_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E),
  ⊥.relrank A = Module.rank F ↥A
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_map_measure : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {α' : Type u_8} [inst_2 : MeasurableSpace α'] {f : α → α'} {g : α' → ε},
  MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) →
    AEMeasurable f μ → (MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Integrable (g ∘ f) μ)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.homMk_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (τ₁ : S₁.X₁ ⟶ S₂.X₁) (τ₂ : S₁.X₂ ⟶ S₂.X₂) (τ₃ : S₁.X₃ ⟶ S₂.X₃)
  (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂)
  (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃),
  (CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).τ₃ = τ₃
-- Mathlib.Data.Sum.Basic
Sum.elim_swap : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → γ} {g : β → γ}, Sum.elim f g ∘ Sum.swap = Sum.elim g f
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.algebraToUnder_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  {X_1 Y : (CategoryTheory.coprodMonad X).Algebra} (f : X_1 ⟶ Y),
  (CategoryTheory.algebraToUnder X).map f = CategoryTheory.Under.homMk f.f ⋯
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp a (b - p) = toIocDiv hp a b - 1
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  Function.Surjective ⇑Valued.v
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  k ∉ m₂ → Std.ExtDHashMap.Const.getD (m₁.union m₂) k fallback = Std.ExtDHashMap.Const.getD m₁ k fallback
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.toOrderAddMonoidHom_apply : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  (x : ↥(↑f).domain), f.toOrderAddMonoidHom x = ↑↑f x
-- Mathlib.Algebra.Notation.Prod
Prod.fst_one : ∀ {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N], 1.1 = 1
-- Qq.Macro
/-- Maps quoted expressions (of type Level) in the old context to level parameter names in the new context  -/
Qq.Impl.UnquoteState.levelSubst : Qq.Impl.UnquoteState → Std.HashMap Lean.Expr Lean.Level
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.apply_prod_le_sum_apply : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [AddLeftMono β] (s : Finset ι) {f : ι → α} (g : α → β),
  g 1 ≤ 0 → (∀ (a b : α), g (a * b) ≤ g a + g b) → g (∏ x ∈ s, f x) ≤ ∑ x ∈ s, g (f x)
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.add_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s t : Set α},
  IsUpperSet t → IsUpperSet (s + t)
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.ae_eq : ∀ {α : Type u_1} {δ : Type u_3} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → ∀ {f g : α → δ}, f =ᵐ[ν] g → f =ᵐ[μ] g
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
IterateAddAct.instMeasurableSpace : {α : Type u_1} → {f : α → α} → MeasurableSpace (IterateAddAct f)
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `monotoneOn_toDual_comp_iff`. -/
AntitoneOn.dual_right : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn f s → MonotoneOn (⇑OrderDual.toDual ∘ f) s
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_mul_eq_mk'_of_mul : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x₁ x₂ : M) (y : ↥S), f.mk' x₂ y * f x₁ = f.mk' (x₁ * x₂) y
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDerivWithin_fun_const_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜}, iteratedDerivWithin n (fun x => 0) s x = 0
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.isIso_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g)
  [CategoryTheory.IsIso sq], CategoryTheory.IsIso (CategoryTheory.Arrow.Hom.left sq)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.zero_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ 0 = 0
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type w} [inst_1 : LinearOrder K] {x : K}
  {F G : CategoryTheory.Functor (↑(Set.Iic x)) C},
  (∀ (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x),
      CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq F G k₁ k₂ h₁₂ h₂) →
    F = G
-- Std.Time.Format.Modifier
Std.Time.instInhabitedExtendedDayPeriod.default : Std.Time.ExtendedDayPeriod
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_sum_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {ι : Type u_4} [inst : Countable ι] (κ : ProbabilityTheory.Kernel α β)
  (η : ι → ProbabilityTheory.Kernel β γ),
  (ProbabilityTheory.Kernel.sum η).comp κ = ProbabilityTheory.Kernel.sum fun i => (η i).comp κ
-- Mathlib.Order.Monotone.Monovary
/-- `f` monovaries with `g` if `g i < g j` implies `f i ≤ f j`.  -/
Monovary : {ι : Type u_1} → {α : Type u_3} → {β : Type u_4} → [Preorder α] → [Preorder β] → (ι → α) → (ι → β) → Prop
-- Lean.Meta.Tactic.Assert
/-- Convert the given goal `Ctx |- target` into `Ctx |- let name : type := val; target`.
It assumes `val` has type `type`  -/
Lean.MVarId.define : Lean.MVarId → Lean.Name → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MVarId
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.step.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α] (it : Std.Iter α),
  Std.Rxo.Iterator.step it =
    match it.internalState.next with
    | none => Std.IterStep.done
    | some next =>
      if next < it.internalState.upperBound then
        Std.IterStep.yield
          { internalState := { next := Std.PRange.succ? next, upperBound := it.internalState.upperBound } } next
      else Std.IterStep.done
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.piecewise_apply_left : ∀ {X : Type u_1} {Z : Type u_3} [inst : TopologicalSpace X] {C₁ C₂ : Set X} (h₁ : IsClosed C₁) (h₂ : IsClosed C₂)
  (h : C₁ ∪ C₂ = Set.univ) (f : LocallyConstant (↑C₁) Z) (g : LocallyConstant (↑C₂) Z)
  (hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩) [inst_1 : DecidablePred fun x => x ∈ C₁] (x : X)
  (hx : x ∈ C₁), (LocallyConstant.piecewise h₁ h₂ h f g hfg) x = f ⟨x, hx⟩
-- Lean.Elab.PreDefinition.Basic
/-- Applies `Lean.Elab.Term.levelMVarToParam` to the types of each predefinition.
 -/
Lean.Elab.levelMVarToParamTypesPreDecls : Array Lean.Elab.PreDefinition → Lean.Elab.TermElabM (Array Lean.Elab.PreDefinition)
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.IsLocal.mk : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R}, I.jacobson.IsMaximal → I.IsLocal
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittZSMul_vars : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (m : ℤ) (n : ℕ),
  (WittVector.wittZSMul p m n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.IsSRGWith.of_adj : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ},
  G.IsSRGWith n k ℓ μ → ∀ (v w : V), G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) = ℓ
-- Init.Data.Nat.Mod
Nat.div_lt_of_lt_mul : ∀ {m n k : ℕ}, m < n * k → m / n < k
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.alter.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → ∀ (f f_1 : Option β → Option β), f = f_1 → t.alter a f = t_1.alter a_1 f_1
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.subsingleton_kaehlerDifferential : ∀ {R : Type u} {A : Type v} {inst : CommRing R} {inst_1 : CommRing A} {inst_2 : Algebra R A}
  [self : Algebra.FormallyEtale R A], Subsingleton Ω[A⁄R]
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentItem.mk : Lean.Lsp.DocumentUri → String → ℕ → String → Lean.Lsp.TextDocumentItem
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_g' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).g' = 0
-- Mathlib.Analysis.Calculus.VectorField
/-- If a `C^2` map has an invertible derivative at a point, then nearby derivatives can be written
as continuous linear equivs, which depend in a `C^1` way on the point, as well as their inverse, and
moreover one can compute the derivative of the inverse.  -/
exists_continuousLinearEquiv_fderiv_symm_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace E]
  {f : E → F} {x : E},
  ContDiffAt 𝕜 2 f x →
    (fderiv 𝕜 f x).IsInvertible →
      ∃ N,
        ContDiffAt 𝕜 1 (fun y => ↑(N y)) x ∧
          ContDiffAt 𝕜 1 (fun y => ↑(N y).symm) x ∧
            (∀ᶠ (y : E) in nhds x, ↑(N y) = fderiv 𝕜 f y) ∧
              ∀ (v : E),
                (fderiv 𝕜 (fun y => ↑(N y).symm) x) v = -↑(N x).symm ∘SL (fderiv 𝕜 (fderiv 𝕜 f) x) v ∘SL ↑(N x).symm
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.ParentKind.eqBwdPattern.sizeOf_spec : sizeOf Lean.Meta.Grind.NormalizePattern.ParentKind.eqBwdPattern✝ = 1
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeGPFree.mono : ∀ {α : Type u_2} [inst : Monoid α] {s t : Set α}, t ⊆ s → ThreeGPFree s → ThreeGPFree t
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.primeHeight_strict_mono : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R} [inst_1 : I.IsPrime] [inst_2 : J.IsPrime],
  I < J → ∀ [J.FiniteHeight], Ideal.primeHeight✝ I < Ideal.primeHeight✝ J
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instEDist : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} → {μ : MeasureTheory.Measure α} → [inst : NormedAddCommGroup E] → EDist ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_inv_rpow : ∀ {x y : ℝ}, 0 ≤ x → y ≠ 0 → (x ^ y⁻¹) ^ y = x
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instMulPosReflectLT : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [inst_2 : Preorder α] [MulPosReflectLT α],
  MulPosReflectLT (WithBot α)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
UniqueDiffOn.image : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {f' : E → E →L[𝕜] F},
  UniqueDiffOn 𝕜 s → (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → (∀ x ∈ s, DenseRange ⇑(f' x)) → UniqueDiffOn 𝕜 (f '' s)
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.SmallFilteredIntermediate.instFaithfulInclusion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C),
  (CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion F).Faithful
-- Mathlib.MeasureTheory.Constructions.Pi
/-- We intentionally restrict this only to the nondependent function space, since type-class
inference cannot find an instance for `ι → ℝ` when this is stated for dependent function spaces.  -/
MeasureTheory.Pi.isInvInvariant_volume : ∀ {ι : Type u_1} [inst : Fintype ι] {α : Type u_4} [inst_1 : Group α] [inst_2 : MeasureTheory.MeasureSpace α]
  [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasurableInv α] [MeasureTheory.volume.IsInvInvariant],
  MeasureTheory.volume.IsInvInvariant
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestMatch_iff_isLongestMatch_beq : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch c pos ↔ String.Slice.Pattern.Model.IsLongestMatch (fun x => x == c) pos
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_single : ∀ {ι : Type u_2} {M : ι → Type u_6} [inst : (i : ι) → AddMonoid (M i)] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  (x : (i : ι) → M i), Finset.univ.noncommSum (fun i => Pi.single i (x i)) ⋯ = x
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instNonUnitalSemiring : {R : Type u_1} → [NonUnitalSemiring R] → NonUnitalSemiring Rᵒᵈ
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.instOrderHomClass : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂], OrderHomClass (E₁ →ₚ[R] E₂) E₁ E₂
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_compl`. -/
Set.diff_compl : ∀ {α : Type u_1} {s t : Set α}, s \ tᶜ = s ∩ t
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringRightObjIdIso_hom_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  (X : CategoryTheory.Functor E C) (X_1 : E),
  (CategoryTheory.Functor.whiskeringRightObjIdIso.hom.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.isPWO_support : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (x : HahnSeries Γ R), x.support.IsPWO
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangle_map_hom₁ : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), (F.mapTriangle.map f).hom₁ = F.map f.hom₁
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sumIsoExt_inv_app_inr : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor (A ⊕ B) C}
  (e₁ : (CategoryTheory.Sum.inl_ A B).comp F ≅ (CategoryTheory.Sum.inl_ A B).comp G)
  (e₂ : (CategoryTheory.Sum.inr_ A B).comp F ≅ (CategoryTheory.Sum.inr_ A B).comp G) (b : B),
  (CategoryTheory.Functor.sumIsoExt e₁ e₂).inv.app (Sum.inr b) = e₂.inv.app b
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedInClass.toDFunLike : {B : Type u_5} →
  {E : outParam (Type u_6)} →
    {F : outParam (Type u_7)} →
      {inst : NormedAddCommGroup E} →
        {inst_1 : NormedAddCommGroup F} →
          {inst_2 : NormedSpace ℝ E} →
            {inst_3 : NormedSpace ℝ F} →
              {n : outParam ℕ∞} →
                {K : outParam (TopologicalSpace.Compacts E)} →
                  [self : ContDiffMapSupportedInClass B E F n K] → DFunLike B E fun x => F
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.constModify₀ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β}
  {h : 0 < m.buckets.size} {a : α} {f : β → β}, m.WF → (↑(Std.DHashMap.Internal.Raw₀.Const.modify ⟨m, h⟩ a f)).WF
-- Mathlib.Topology.ExtremallyDisconnected
extremallyDisconnected_of_homeo : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [ExtremallyDisconnected X]
  (e : X ≃ₜ Y), ExtremallyDisconnected Y
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instInv : {α : Type u} → [Inv α] → Inv (WithOne α)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.prodEquiv_apply : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (A : Subgroup G) (B : Subgroup H)
  (q : (G × H) ⧸ A.prod B),
  (QuotientGroup.prodEquiv A B) q =
    Quotient.liftOn' q
      (fun x =>
        match x with
        | (g, h) => (↑g, ↑h))
      ⋯
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.sortMVarIdArrayByIndex : {m : Type → Type} → [Lean.MonadMCtx m] → [Monad m] → Array Lean.MVarId → m (Array Lean.MVarId)
-- Init.Prelude
/-- Add a new trace message, with the given trace class and message.  -/
Lean.Macro.trace : Lean.Name → String → Lean.MacroM Unit
-- Mathlib.Algebra.Opposites
AddOpposite.instInvolutiveNeg : {α : Type u_1} → [InvolutiveNeg α] → InvolutiveNeg αᵃᵒᵖ
-- Mathlib.Geometry.Euclidean.SignedDist
Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} (i : Fin (n + 1)) {p : P},
  p ∈ affineSpan ℝ (Set.range s.points) →
    |(s.signedInfDist i) p| = dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_of_isEmpty : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a fallback : α}, (↑m).isEmpty = true → m.getKeyD a fallback = fallback
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_eq_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {L : SummationFilter β}
  [L.LeAtTop] {s : Finset β}, (∀ b ∉ s, f b = 1) → ∏'[L] (b : β), f b = ∏ b ∈ s, f b
-- Aesop.Index.RulePattern
Aesop.RulePatternIndex.Entry.mk : Aesop.RuleName → Aesop.RulePattern → Aesop.RulePatternIndex.Entry
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonalEquivFin_apply_val : ∀ (n : ℕ) (x : ↥(Finset.HasAntidiagonal.antidiagonal n)), ↑((Finset.Nat.antidiagonalEquivFin n) x) = x.1.1
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.logImportFailure : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Meta.LazyDiscrTree.ImportFailure → m Unit
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq.eq_1 : ∀ {K : Type u_1} [inst : RCLike K],
  RCLike.normSq =
    { toFun := fun z => RCLike.re z * RCLike.re z + RCLike.im z * RCLike.im z, map_zero' := ⋯, map_one' := ⋯,
      map_mul' := ⋯ }
-- Mathlib.Data.Erased
Erased.map.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) (a : Erased α), Erased.map f a = a.bind (Erased.mk ∘ f)
-- Aesop.Util.Basic
Aesop.forEachExprInLDecl : {ω : Type} →
  {m : Type → Type} → [STWorld ω m] → [MonadLiftT (ST ω) m] → [Monad m] → Lean.LocalDecl → (Lean.Expr → m Unit) → m Unit
-- Mathlib.Order.SupClosed
supClosed_univ : ∀ {α : Type u_3} [inst : SemilatticeSup α], SupClosed Set.univ
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.iteratedFDerivLM_apply_of_gt : ∀ (𝕜 : 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] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} {i : ℕ}
  (f : ContDiffMapSupportedIn E F n K), n < k + ↑i → (ContDiffMapSupportedIn.iteratedFDerivLM 𝕜 n k i) f = 0