mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.Split.Pred
String.Slice.Pattern.Model.split_bool_eq_internal : ∀ {p : Char → Bool} {s : String.Slice} (f curr : s.Pos) (hle : f ≤ curr),
  String.Slice.Pattern.Model.split p f curr hle =
    if h : curr = s.endPos then [s.subslice f curr hle]
    else
      if p (curr.get h) = true then
        s.subslice f curr hle :: String.Slice.Pattern.Model.split p (curr.next h) (curr.next h) ⋯
      else String.Slice.Pattern.Model.split p f (curr.next h) ⋯
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsStrictMinor.ssubset : ∀ {α : Type u_1} {M N : Matroid α}, N <m M → N.E ⊂ M.E
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.le_degree_of_ne_zero : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.coeff n ≠ 0 → ↑n ≤ p.degree
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  [inst : Inhabited α] {f : (a : α) → β a → γ a} {k : α}, (Std.DTreeMap.map f t).getKey! k = t.getKey! k
-- Init.Grind.Interactive
Lean.Parser.Tactic.grindLemma : Lean.ParserDescr
-- Mathlib.Geometry.Euclidean.Projection
/-- The reflection of a point in a subspace is contained in any larger
subspace containing both the point and the subspace reflected in.  -/
EuclideanGeometry.reflection_mem_of_le_of_mem : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s₁ s₂ : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s₁] [inst_6 : s₁.direction.HasOrthogonalProjection],
  s₁ ≤ s₂ → ∀ {p : P}, p ∈ s₂ → (EuclideanGeometry.reflection s₁) p ∈ s₂
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.FinMeasSupp.integrable : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {f : MeasureTheory.SimpleFunc α E}, f.FinMeasSupp μ → MeasureTheory.Integrable (⇑f) μ
-- Mathlib.Data.List.MinMax
List.not_lt_minimum_of_mem' : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] {l : List α} {a : α}, a ∈ l → ¬↑a < l.minimum
-- Init.Control.Lawful.Instances
StateT.instLawfulMonad : ∀ {m : Type u_1 → Type u_2} {σ : Type u_1} [inst : Monad m] [LawfulMonad m], LawfulMonad (StateT σ m)
-- Mathlib.RingTheory.Flat.Basic
Module.flat_iff : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.Flat R M ↔
    ∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] [Module.Finite R P] (N : Submodule R P),
      N.FG → Function.Injective ⇑(LinearMap.rTensor M N.subtype)
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.mk.inj : ∀ {α : Type u} {β : Type v} {cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw._auto_1}
  {inner inner_1 : Std.DTreeMap.Raw α (fun x => β) cmp}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.Order.CompleteBooleanAlgebra
/-- A complete distributive lattice is a complete lattice whose `⊔` and `⊓` respectively
distribute over `⨅` and `⨆`.  -/
CompleteDistribLattice : Type u_1 → Type u_1
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- Two morphisms `f : X ⟶ Z` and `g : Y ⟶ Z` have a weak pullback if the diagram
`cospan f g` has a weak limit.  -/
CategoryTheory.Limits.HasWeakPullback : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {X Y Z : C} → (X ⟶ Z) → (Y ⟶ Z) → Prop
-- Init.Data.UInt.Lemmas
UInt16.toFin_ofFin : ∀ (n : Fin UInt16.size), (UInt16.ofFin n).toFin = n
-- Mathlib.NumberTheory.FLT.Basic
fermatLastTheoremFor_iff_nat : ∀ {n : ℕ}, FermatLastTheoremFor n ↔ FermatLastTheoremWith ℕ n
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.neg_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Neg A] (M : CStarMatrix m n A) (i : m) (j : n), (-M) i j = -M i j
-- Std.Time.Format.Modifier
Std.Time.Modifier.Z.sizeOf_spec : ∀ (presentation : Std.Time.OffsetZ), sizeOf (Std.Time.Modifier.Z presentation) = 1 + sizeOf presentation
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_algebraMap : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] {x : NNReal} {y : ℝ}, (algebraMap NNReal A) x ^ y = (algebraMap NNReal A) (x ^ y)
-- Mathlib.GroupTheory.QuotientGroup.Finite
/-- If `ker(G →* H)` and `H` are finite, then `G` is finite.  -/
Group.fintypeOfKerOfCodom : {G : Type u_2} →
  {H : Type u_3} → [inst : Group G] → [inst_1 : Group H] → [Fintype H] → (g : G →* H) → [Fintype ↥g.ker] → Fintype G
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.lift_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {α : Sort u_2}
  (f : R → ↥(ValuativeRel.posSubmonoid R) → α)
  (hf : ∀ (x y : R) (t s : ↥(ValuativeRel.posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t),
  ValuativeRel.ValueGroupWithZero.lift f hf 1 = f 1 1
-- Std.Http.Transport
/-- Closes the mock server and client.
 -/
Std.Http.Internal.Mock.Server.close : Std.Http.Internal.Mock.Server → IO Unit
-- Std.Data.ExtHashMap.Lemmas
/-- Simpler variant of `getElem_filterMap` when `LawfulBEq` is available.  -/
Std.ExtHashMap.getElem_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  {f : α → β → Option γ} {k : α} {h : k ∈ Std.ExtHashMap.filterMap f m},
  (Std.ExtHashMap.filterMap f m)[k] = (f k m[k]).get ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_add_one_eq_top : ∀ {f : ℕ → ENNReal}, ∑' (n : ℕ), f n = ⊤ → f 0 ≠ ⊤ → ∑' (n : ℕ), f (n + 1) = ⊤
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_list_equiv_foldl : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m₁ : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {l : List α},
  (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m₁ l)).Equiv
    (List.foldl (fun acc a => acc.insertIfNew a ()) (↑m₁) l)
-- Init.Data.String.Defs
String.append_right_inj : ∀ (s : String) {t₁ t₂ : String}, s ++ t₁ = s ++ t₂ ↔ t₁ = t₂
-- Std.Data.TreeSet.Slice
Std.TreeSet.instSliceableRicSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.instSliceableRicSlice._auto_1) →
    Std.Ric.Sliceable (Std.TreeSet α cmp) α (Std.DTreeMap.Internal.Unit.RicSlice α)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.atom_pf' : ∀ {R : Type u_1} [inst : CommSemiring R] {a a' b : R},
  a = a' → ∀ {e : ℕ}, Nat.rawCast 1 = e → a' ^ e * Nat.rawCast 1 = b → a = b + 0
-- Init.Internal.Order.Lemmas
Lean.Order.Functor.monotone_map : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] [LawfulMonad m] (f : γ → m α) (g : α → β),
  Lean.Order.monotone f → Lean.Order.monotone fun x => g <$> f x
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piComparison_comp_π_apply : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C)
  [inst_2 : CategoryTheory.Limits.HasProduct f] [inst_3 : CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (b : β)
  {F : D → D → Type uF} {carrier : D → Type w_1} {instFunLike : (X Y : D) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_4 : CategoryTheory.ConcreteCategory D F] (x : carrier (G.obj (∏ᶜ f))),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun b => G.obj (f b)) b))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.piComparison G f)) x) =
    (CategoryTheory.ConcreteCategory.hom (G.map (CategoryTheory.Limits.Pi.π f b))) x
-- Init.Data.Iterators.Basic
/-- The iterator is a plausible successor of one of the current iterator's successors.  -/
Std.IterM.IsPlausibleIndirectSuccessorOf.cons_right : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {it'' it' it : Std.IterM m β},
  it''.IsPlausibleIndirectSuccessorOf it' → it'.IsPlausibleSuccessorOf it → it''.IsPlausibleIndirectSuccessorOf it
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.mk : UInt64 →
  UInt64 →
    UInt64 →
      UInt64 →
        UInt64 →
          UInt64 →
            UInt64 →
              UInt64 →
                UInt64 → UInt64 → UInt64 → UInt64 → UInt64 → UInt64 → UInt64 → UInt64 → Std.Internal.UV.System.RUsage
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestRevMatchAt_iff_isLongestRevMatchAt_ofSliceTo : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {base : s.Pos}
  {startPos endPos : (s.sliceTo base).Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos ↔
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat (String.Slice.Pos.ofSliceTo startPos)
      (String.Slice.Pos.ofSliceTo endPos)
-- Mathlib.Combinatorics.Optimization.ValuedCSP
FractionalOperation.tt.eq_1 : ∀ {D : Type u_1} {m : ℕ} {ι : Type u_3} (ω : FractionalOperation D m) (x : Fin m → ι → D),
  ω.tt x = Multiset.map (fun g i => g (Function.swap x i)) ω
-- Init.Internal.Order.Basic
_private.Init.Internal.Order.Basic.0.EST.bind.match_1.eq_2 : ∀ {ε σ α : Type} (motive : EST.Out ε σ α → Sort u_1) (e : ε) (s : Void σ)
  (h_1 : (a : α) → (s : Void σ) → motive (EST.Out.ok a s)) (h_2 : (e : ε) → (s : Void σ) → motive (EST.Out.error e s)),
  (match EST.Out.error e s with
    | EST.Out.ok a s => h_1 a s
    | EST.Out.error e s => h_2 e s) =
    h_2 e s
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.eventually_le_exp : ∀ {u : ℕ → ENNReal} {a : EReal}, ExpGrowth.expGrowthSup u < a → ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ (a * ↑n).exp
-- Mathlib.Analysis.Fourier.RiemannLebesgueLemma
/-- The Riemann-Lebesgue lemma, formulated in terms of `VectorFourier.fourierIntegral` (with the
pairing in the definition of `fourierIntegral` taken to be the canonical pairing between `V` and
its dual space).  -/
Real.zero_at_infty_vector_fourierIntegral : ∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : V → E)
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [IsTopologicalAddGroup V] [T2Space V]
  [inst_6 : MeasurableSpace V] [BorelSpace V] [inst_8 : Module ℝ V] [ContinuousSMul ℝ V] [FiniteDimensional ℝ V]
  (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure],
  Filter.Tendsto (VectorFourier.fourierIntegral Real.fourierChar μ (topDualPairing ℝ V).flip f)
    (Filter.cocompact (StrongDual ℝ V)) (nhds 0)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum over `{x ∈ s | pred x}` equals one over `s` if all the weights at indices in `s`
not satisfying `pred` are zero.  -/
Finset.weightedVSubOfPoint_filter_of_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) {pred : ι → Prop}
  [inst_3 : DecidablePred pred],
  (∀ i ∈ s, w i ≠ 0 → pred i) → ({x ∈ s | pred x}.weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w
-- Init.Data.Slice.Array.Lemmas
Subarray.toArray_mkSlice_roc : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = (Std.Slice.toArray xs).extract (lo + 1) (hi + 1)
-- Mathlib.Algebra.Category.Ring.Under.Property
CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective : ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] {A B : CategoryTheory.Under R} {f g : A ⟶ B},
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g))
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- If `q` and `r` are quotient and remainder in the Weierstrass division `0 / g`, then they are
equal to `0`.  -/
PowerSeries.IsWeierstrassDivision.eq_zero : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {g : PowerSeries A},
  (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 →
    ∀ [IsHausdorff (IsLocalRing.maximalIdeal A) A] {q : PowerSeries A} {r : Polynomial A},
      PowerSeries.IsWeierstrassDivision 0 g q r → q = 0 ∧ r = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.maxKey? = some k ↔
    (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorCompIsoId_naturality_1 : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) (i j : A) (hij : i + j = 0),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C i j hij).inv.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f))
        ((CategoryTheory.shiftFunctorCompIsoId C i j hij).hom.app Y)) =
    f
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
/-- Given an A-linear map between M₁ and M₂, `primaryComponent.map` is the
restriction to the I-primaryComponent components of M₁ and M₂.  -/
Ideal.primaryComponent.map : {A : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommRing A] →
        (I : Ideal A) →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : Module A M₁] →
                [inst_4 : Module A M₂] →
                  (M₁ →ₗ[A] M₂) → ↥(Ideal.primaryComponent M₁ I) →ₗ[A] ↥(Ideal.primaryComponent M₂ I)
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedCommGroup.ofMulDist'.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : CommGroup E] [inst_2 : PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 1 x)
  (h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y),
  SeminormedCommGroup.ofMulDist' h₁ h₂ =
    { toNorm := (SeminormedGroup.ofMulDist' h₁ h₂).toNorm, toGroup := (SeminormedGroup.ofMulDist' h₁ h₂).toGroup,
      mul_comm := ⋯, toPseudoMetricSpace := (SeminormedGroup.ofMulDist' h₁ h₂).toPseudoMetricSpace, dist_eq := ⋯ }
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.instInhabitedSpaceResult : Inhabited Std.Format.SpaceResult✝
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [inst_2 : S₁.HasLeftHomology]
  [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.leftHomologyMap φ =
    CategoryTheory.CategoryStruct.comp h₁.leftHomologyIso.hom
      (CategoryTheory.CategoryStruct.comp γ.φH h₂.leftHomologyIso.inv)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_differentiableWithinAt_iff : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} {x : G},
  DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The image of `p` in the universal factorization ring of `p`.  -/
Polynomial.UniversalFactorizationRing.monicDegreeEq : {R : Type u_1} →
  [inst : CommRing R] →
    {n : ℕ} →
      (m k : ℕ) →
        (hn : n = m + k) →
          (p : Polynomial.MonicDegreeEq R n) →
            Polynomial.MonicDegreeEq (Polynomial.UniversalFactorizationRing m k hn p) n
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Colorable.mono_left : ∀ {V : Type u} {G G' : SimpleGraph V}, G ≤ G' → ∀ {n : ℕ}, G'.Colorable n → G.Colorable n
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₁ → (m₁ \ m₂).get? k = none
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.AddSubgroup.index_mul_measure : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G] (H : AddSubgroup G) [H.FiniteIndex],
  MeasurableSet ↑H → ∀ (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant], ↑H.index * μ ↑H = μ Set.univ
-- Mathlib.Order.Basic
/-- An order is dense if there is an element between any pair of distinct comparable elements.  -/
DenselyOrdered : (α : Type u_5) → [LT α] → Prop
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.contDiff : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n), ContDiff ℝ ↑n ⇑f
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
CategoryTheory.IsGrothendieckAbelian.instIsLeftAdjointModuleCatMulOppositeEndTensorObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G : C},
  (CategoryTheory.IsGrothendieckAbelian.tensorObj G).IsLeftAdjoint
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.toMultiplicativeAlgEquiv_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M] (m : M) (a : A),
  (AddMonoidAlgebra.toMultiplicativeAlgEquiv R A M) (AddMonoidAlgebra.single m a) =
    MonoidAlgebra.single (Multiplicative.ofAdd m) a
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- Stalks of a locally ringed space are local rings.  -/
AlgebraicGeometry.LocallyRingedSpace.isLocalRing : ∀ (self : AlgebraicGeometry.LocallyRingedSpace) (x : ↑↑self.toPresheafedSpace), IsLocalRing ↑(self.presheaf.stalk x)
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_mkSlice_rco : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...hi) = List.drop lo (List.take hi (Std.Slice.toList xs))
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.inlX_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder] (i j : ι)
  (hij : c.Rel j i) {Z : C} (h : K.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inlX K i j hij)
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.cylinder.π K).f j) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
/-- This is a type class recording that a commutative monoid `M` contains primitive `n`th
roots of unity and such that the group of `n`th roots of unity is cyclic.

Such monoids are suitable targets in the context of duality statements for groups
of exponent `n`.  -/
HasEnoughRootsOfUnity : (M : Type u_1) → [CommMonoid M] → ℕ → Prop
-- Mathlib.Data.Ordmap.Ordset
Ordnode.insertWith.eq_2 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (f : α → α) (x : α) (sz : ℕ) (l : Ordnode α) (x_2 : α)
  (r : Ordnode α),
  Ordnode.insertWith f x (Ordnode.node sz l x_2 r) =
    match cmpLE x x_2 with
    | Ordering.lt => (Ordnode.insertWith f x l).balanceL x_2 r
    | Ordering.eq => Ordnode.node sz l (f x_2) r
    | Ordering.gt => l.balanceR x_2 (Ordnode.insertWith f x r)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.mk_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (x y : CochainComplex.HomComplex.Cocycle K L n),
  CochainComplex.HomComplex.CohomologyClass.mk (x + y) =
    CochainComplex.HomComplex.CohomologyClass.mk x + CochainComplex.HomComplex.CohomologyClass.mk y
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_lt_iff_one_lt_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b : α}, a⁻¹ < b ↔ 1 < b * a
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.mono_homOfLE : ∀ {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂), CategoryTheory.Mono (SSet.Subcomplex.homOfLE h)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.eLpNorm'_eq_lintegral_enorm : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] (f : α → ε) (q : ℝ)
  (μ : MeasureTheory.Measure α), MeasureTheory.eLpNorm' f q μ = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CategoryTheory.Injective.under.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.EnoughInjectives C] (X X_1 : C),
  X = X_1 → CategoryTheory.Injective.under X = CategoryTheory.Injective.under X_1
-- Mathlib.Order.Filter.AtTopBot.ModEq
Filter.nonneg_of_eventually_pow_nonneg : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α},
  (∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ a ^ n) → 0 ≤ a
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.support_sum : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {ι₁ : Type u₁} [inst_1 : DecidableEq ι₁] {β₁ : ι₁ → Type v₁}
  [inst_2 : (i₁ : ι₁) → Zero (β₁ i₁)] [inst_3 : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)]
  [inst_4 : (i : ι) → AddCommMonoid (β i)] [inst_5 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i₁ : ι₁), β₁ i₁}
  {g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i}, (f.sum g).support ⊆ f.support.biUnion fun i => (g i (f i)).support
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarSpaceCoord_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (a : NumberField.mixedEmbedding.mixedSpace K),
  ↑(NumberField.mixedEmbedding.polarSpaceCoord K) a =
    (NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace K) (a.1, Pi.map (fun i => ↑Complex.polarCoord) a.2)
-- Mathlib.Tactic.Ring.Common
/-- Inverts a polynomial `va` to get a normalized result polynomial.

* `c⁻¹ = (c⁻¹)` if `c` is a constant
* `(a ^ b * c)⁻¹ = a⁻¹ ^ b * c⁻¹`
 -/
Mathlib.Tactic.Ring.Common.ExProd.evalInv : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            (dsα : Q(Semifield «$α»)) →
              {a : Q(«$α»)} →
                Option Q(CharZero «$α») →
                  Mathlib.Tactic.Ring.Common.ExProd bt sα a →
                    Mathlib.Tactic.AtomM
                      (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExProd bt sα) q(«$a»⁻¹))