mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_map_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k k' : α}
  {fallback : γ},
  (↑m).WF →
    m.getKey? k = some k' →
      Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.map f m) k fallback =
        (Option.map (f k') (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.totalVariation_neg : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α), (-s).totalVariation = s.totalVariation
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.isClopen_setOfPred_rel : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) (x : X), IsClopen (Set.ofPred (S.toSetoid x))
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_zero_iff' : ∀ {E : Type u_5} [inst : NormedGroup E] {a : E}, ‖a‖ ≤ 0 ↔ a = 1
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_neg : ∀ (a : UInt32), (-a).toUInt16 = -a.toUInt16
-- Mathlib.Order.Lattice.Nat
Nat.sInf_le : ∀ {s : Set ℕ} {m : ℕ}, m ∈ s → sInf s ≤ m
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap_assoc : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g)
  {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 x)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) h) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Proj 𝒜).homOfLE ⋯)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f) h)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- Constructor for morphisms from `X.cycles`.  -/
CategoryTheory.Abelian.SpectralObject.descCycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (fg : i ⟶ k) →
                    (h : CategoryTheory.CategoryStruct.comp f g = fg) →
                      {A : C} →
                        {n : ℤ} →
                          (x : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ A) →
                            CategoryTheory.CategoryStruct.comp
                                  ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) x =
                                0 →
                              (X.cycles f g n ⟶ A)
-- Mathlib.NumberTheory.Ostrowski
/-- Given any two integers `n`, `m` with `m > 1`, the absolute value of `n` is bounded by
`m + m * f m + m * (f m) ^ 2 + ... + m * (f m) ^ d` where `d` is the number of digits of the
expansion of `n` in base `m`.  -/
Rat.AbsoluteValue.apply_le_sum_digits : ∀ {f : AbsoluteValue ℚ ℝ} (n : ℕ) {m : ℕ}, 1 < m → f ↑n ≤ (List.mapIdx (fun i x => ↑m * f ↑m ^ i) (m.digits n)).sum
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_map₂ : ∀ {a b : CategoryTheory.Cat} {f g : a ⟶ b} (f_1 : f ⟶ g),
  CategoryTheory.WithInitial.prelaxfunctor.map₂ f_1 =
    CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.WithInitial.map₂ f_1.toNatTrans)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- For a functor `G : J ⥤ K ⥤ C`, its colimit `K ⥤ C` is given by `(G' : K ⥤ J ⥤ C) ⋙ colim`.
Note that this does not require `K` to be small.
 -/
CategoryTheory.Limits.colimitIsoSwapCompColim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C] →
              (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
                CategoryTheory.Limits.colimit G ≅
                  (CategoryTheory.Functor.curry.obj
                        ((CategoryTheory.Prod.swap K J).comp (CategoryTheory.Functor.uncurry.obj G))).comp
                    CategoryTheory.Limits.colim
-- Batteries.Data.List.Lemmas
List.findIdxNth_nil : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ}, List.findIdxNth p [] n = 0
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.pointwise_smul_toAddSubgroup : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] (m : M)
  (S : Subring R), (m • S).toAddSubgroup = m • S.toAddSubgroup
-- Lean.Parser.Command
Lean.Parser.Command.declValSimple.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Filter.Extr
Filter.EventuallyEq.isExtrFilter_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
  f =ᶠ[l] g → f a = g a → (IsExtrFilter f l a ↔ IsExtrFilter g l a)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyι_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) S₂.rightHomologyι =
    CategoryTheory.CategoryStruct.comp S₁.rightHomologyι (CategoryTheory.ShortComplex.opcyclesMap φ)
-- Lean.Declaration
Lean.ConstantInfo.opaqueInfo.inj : ∀ {val val_1 : Lean.OpaqueVal}, Lean.ConstantInfo.opaqueInfo val = Lean.ConstantInfo.opaqueInfo val_1 → val = val_1
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.invOneSubPow_val_one_eq_invUnitSub_one : ∀ (S : Type u_1) [inst : CommRing S], ↑(PowerSeries.invOneSubPow S 1) = PowerSeries.invUnitsSub 1
-- Init.Data.List.Lemmas
List.any_filterMap : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → Option β} {p : β → Bool},
  (List.filterMap f l).any p =
    l.any fun a =>
      match f a with
      | some b => p b
      | none => false
-- Std.Data.ExtDHashMap.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.ExtDHashMap.Const.alter : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      [EquivBEq α] →
        [LawfulHashable α] →
          {β : Type v} → (Std.ExtDHashMap α fun x => β) → α → (Option β → Option β) → Std.ExtDHashMap α fun x => β
-- Init.Grind.Module.Basic
Lean.Grind.NoNatZeroDivisors.mk : ∀ {α : Type u} [inst : Lean.Grind.NatModule α],
  (∀ (k : ℕ) (a b : α), k ≠ 0 → k • a = k • b → a = b) → Lean.Grind.NoNatZeroDivisors α
-- Mathlib.Algebra.BigOperators.Pi
prod_indicator_const_apply : ∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_5} [inst : CommSemiring R] (s : Finset ι) (f : ι → Set κ) (g : κ → R)
  (j : κ), ∏ i ∈ s, (f i).indicator g j = (⋂ x ∈ s, f x).indicator (g ^ s.card) j
-- Mathlib.Topology.NhdsWithin
nhdsWithin_pi_eq_bot : ∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] {I : Set ι} {s : (i : ι) → Set (X i)}
  {x : (i : ι) → X i}, nhdsWithin x (I.pi s) = ⊥ ↔ ∃ i ∈ I, nhdsWithin (x i) (s i) = ⊥
-- Mathlib.MeasureTheory.Measure.DiracProba
MeasureTheory.diracProba_toMeasure_apply_of_mem : ∀ {X : Type u_1} [inst : MeasurableSpace X] {x : X} {A : Set X}, x ∈ A → ↑(MeasureTheory.diracProba x) A = 1
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_npow : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → Monoid (G i)] [inst_7 : Monoid C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), MonoidHomClass (H i) (G i) C]
  (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x : DirectLimit G f)
  (n : ℕ), DirectLimit.lift f (fun x => ⇑(g x)) h (x ^ n) = DirectLimit.lift f (fun x => ⇑(g x)) h x ^ n
-- Mathlib.Data.Multiset.AddSub
Multiset.cons_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {a : α}, a ∈ s → a ::ₘ s.erase a = s
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.nullHomotopicMap'.eq_1 : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)),
  Homotopy.nullHomotopicMap' h = Homotopy.nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.models_sentence_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence}, T ⊨ᵇ φ ↔ ∀ (M : T.ModelType), ↑M ⊨ φ
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.smul.inj : ∀ {R : Type u} {ι : Type u_4} {M : Type u_5} {m : ι → M} {i : ι} {r : R} {x : M} {m_1 : ι → M} {i_1 : ι} {r_1 : R}
  {x_1 : M},
  exteriorPower.presentation.Rels.smul m i r x = exteriorPower.presentation.Rels.smul m_1 i_1 r_1 x_1 →
    m = m_1 ∧ i = i_1 ∧ r = r_1 ∧ x = x_1
-- Init.System.IO
IO.TaskState.ofNat : ℕ → IO.TaskState
-- Mathlib.Algebra.Category.FGModuleCat.Colimits
/-- Finite colimits of finite modules are finite, because we can realise them as quotients
of a finite coproduct.  -/
FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG : ∀ {J : Type} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type u} [inst_2 : Ring k]
  (F : CategoryTheory.Functor J (FGModuleCat k)),
  Module.Finite k ↑(CategoryTheory.Limits.colimit (F.comp (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))))
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_le_of_tsum_le : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
  0 < p.toReal → ∀ {C : ℝ}, 0 ≤ C → ∀ {f : ↥(lp E p)}, ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal → ‖f‖ ≤ C
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] {i j : J} (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ i)
      (CategoryTheory.eHomWhiskerLeft V (F₁.obj i) (F₂.map f)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ j)
      (CategoryTheory.eHomWhiskerRight V (F₁.map f) (F₂.obj j))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {fallback : α}, t.getKey! (t.maxKeyD fallback) = t.maxKeyD fallback
-- Mathlib.SetTheory.Ordinal.Notation
ONote.nf_mulNat : ∀ (o : ONote) [o.NF] (n : ℕ), (o.mulNat n).NF
-- Mathlib.Data.Sym.Sym2
Sym2.map_mk : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a b : α), Sym2.map f s(a, b) = s(f a, f b)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.map_vsub : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (p1 p2 : P),
  f.linearIsometry (p1 -ᵥ p2) = f p1 -ᵥ f p2
-- Mathlib.Data.ZMod.QuotientGroup
infinite_zmultiples : ∀ {α : Type u_3} [inst : AddGroup α] {a : α}, (↑(AddSubgroup.zmultiples a)).Infinite ↔ ¬IsOfFinAddOrder a
-- Init.Data.String.Lemmas.Order
String.Pos.lt_next_iff_le : ∀ {s : String} {p q : s.Pos} {h : q ≠ s.endPos}, p < q.next h ↔ p ≤ q
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCallHierarchyOutgoingCall.fromJson : Lean.Json → Except String Lean.Lsp.CallHierarchyOutgoingCall
-- Mathlib.Topology.Order
continuous_sSup_rng : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ : Set (TopologicalSpace β)}
  {t : TopologicalSpace β}, t ∈ t₂ → Continuous f → Continuous f
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.b : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.DayPeriod
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.mul_inv : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (s s' : ↥S),
  ↑s /ₒ s' * (↑s' /ₒ s) = 1
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_apply_of_mem_of_notMem : ∀ {X : Type u_1} [inst : MeasurableSpace X] {x y : X} (p : ↑unitInterval) {s : Set X},
  MeasurableSet s → x ∈ s → y ∉ s → (ProbabilityTheory.bernoulliMeasure x y p) s = ↑(unitInterval.toNNReal p)
-- Mathlib.Logic.UnivLE
UnivLE.zero : UnivLE.{0, u}
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
CFC.isStrictlyPositive_conjSqrt_iff : ∀ {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] [inst_8 : SeparatelyContinuousMul A] [IsSemitopologicalRing A] [T2Space A]
  (c a : A),
  autoParam (IsStrictlyPositive c) CFC.isStrictlyPositive_conjSqrt_iff._auto_1 →
    (IsStrictlyPositive ((CFC.conjSqrt c) a) ↔ IsStrictlyPositive a)
-- Mathlib.Algebra.Ring.Ext
NonUnitalCommRing.toNonUnitalRing_injective : ∀ {R : Type u}, Function.Injective (@NonUnitalCommRing.toNonUnitalRing R)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.congr_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) {T : Type u_3} [inst_3 : Semiring T] (w : AbsoluteValue T S) (f : R ≃+* T) (x : WithAbs w),
  (WithAbs.congr v w f).symm x = WithAbs.toAbs v (f.symm x.ofAbs)
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.innerContent_of_isCompact : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) {K : Set G} (h1K : IsCompact K)
  (h2K : IsOpen K), μ.innerContent { carrier := K, is_open' := h2K } = μ { carrier := K, isCompact' := h1K }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) l →
          k ∈ List.map Prod.fst l →
            ∀ {h' : k' ∈ Std.DHashMap.Raw.Const.insertMany m l},
              (Std.DHashMap.Raw.Const.insertMany m l).getKey k' h' = k
-- Mathlib.Data.Set.Constructions
FiniteInter.finiteInterClosure_insert : ∀ {α : Type u_1} {S : Set (Set α)} {A : Set α},
  FiniteInter S → ∀ P ∈ FiniteInter.finiteInterClosure (insert A S), P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `AddMonoidHom.pi_apply`. -/
Pi.addMonoidHom_apply : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → AddZeroClass (f i)] {γ : Type w} [inst_1 : AddZeroClass γ]
  (g : (i : I) → γ →+ f i) (x : γ) (i : I), (AddMonoidHom.pi g) x i = (g i) x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.le_maxKey!_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, k ∈ t → (cmp k t.maxKey!).isLE = true
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.index_pos : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  (K : TopologicalSpace.PositiveCompacts G) {V : Set G},
  (interior V).Nonempty → 0 < MeasureTheory.Measure.haar.index (↑K) V
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.mk.injEq : ∀ {M : Type u_1} [inst : AddZeroClass M] (toAddSubmonoid : AddSubmonoid M) (addSaturated : toAddSubmonoid.AddSaturated)
  (toAddSubmonoid_1 : AddSubmonoid M) (addSaturated_1 : toAddSubmonoid_1.AddSaturated),
  ({ toAddSubmonoid := toAddSubmonoid, addSaturated := addSaturated } =
      { toAddSubmonoid := toAddSubmonoid_1, addSaturated := addSaturated_1 }) =
    (toAddSubmonoid = toAddSubmonoid_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [inst_1 : SizeOf C] (I : C) (m : I ⟶ Y)
  [m_mono : CategoryTheory.Mono m] (e : X ⟶ I)
  (fac : autoParam (CategoryTheory.CategoryStruct.comp e m = f) CategoryTheory.Limits.MonoFactorisation.fac._autoParam),
  sizeOf { I := I, m := m, m_mono := m_mono, e := e, fac := fac } =
    1 + sizeOf I + sizeOf m + sizeOf m_mono + sizeOf e + sizeOf fac
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `CommSemiring` instance along a surjective function.  -/
Function.Surjective.commSemiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : SMul ℕ S] →
                  [inst_5 : Pow S ℕ] →
                    [inst_6 : NatCast S] →
                      [inst_7 : CommSemiring R] →
                        f 0 = 0 →
                          f 1 = 1 →
                            (∀ (x y : R), f (x + y) = f x + f y) →
                              (∀ (x y : R), f (x * y) = f x * f y) →
                                (∀ (n : ℕ) (x : R), f (n • x) = n • f x) →
                                  (∀ (x : R) (n : ℕ), f (x ^ n) = f x ^ n) → (∀ (n : ℕ), f ↑n = ↑n) → CommSemiring S
-- Mathlib.Algebra.Group.Equiv.Opposite
MulOpposite.opMulEquiv.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M], MulOpposite.opMulEquiv = { toEquiv := MulOpposite.opEquiv, map_mul' := ⋯ }
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Delaborates a finset indexing a big operator. In case the finset involves a filter,
`i` is used for the binder name.  -/
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.delabFinsetArg : Lean.Ident → Lean.PrettyPrinter.Delaborator.DelabM BigOperators.FinsetFilterResult✝
-- Mathlib.Algebra.Ring.Commute
commute_iff_lie_eq : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {x y : R}, Commute x y ↔ ⁅x, y⁆ = 0
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- An affine combination is unaffected by changing the weights to the
corresponding indicator function and adding points to the set.  -/
Finset.affineCombination_indicator_subset : ∀ {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} (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι},
  s₁ ⊆ s₂ → (Finset.affineCombination k s₁ p) w = (Finset.affineCombination k s₂ p) ((↑s₁).indicator w)
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An additive subgroup of an `AddGroup` inherits an `AddGroup` structure.  -/
AddSubgroupClass.toAddGroup : {G : Type u_1} →
  [inst : AddGroup G] → {S : Type u_4} → (H : S) → [inst_1 : SetLike S G] → [AddSubgroupClass S G] → AddGroup ↥H
-- Init.Data.String.Termination
String.Pos.wellFounded_gt : ∀ {s : String}, WellFounded fun p q => q < p
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.disjoint_torsionBySet_ideal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {P Q : Ideal R}, P ⊔ Q = ⊤ → Disjoint (Submodule.torsionBySet R M ↑P) (Submodule.torsionBySet R M ↑Q)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.ofHom_id : ∀ {X : Type u} [inst : CommGroup X],
  CommGrpCat.ofHom (MonoidHom.id X) = CategoryTheory.CategoryStruct.id (CommGrpCat.of X)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
SimpleGraph.ConnectedComponent.Represents.existsUnique_rep : ∀ {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} {c : G.ConnectedComponent},
  SimpleGraph.ConnectedComponent.Represents s C → c ∈ C → ∃! x, x ∈ s ∩ c.supp
-- Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
Subgroup.instIsCyclicOfDiscreteTopology : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [MulArchimedean G] [DiscreteTopology G], IsCyclic G
-- Mathlib.Algebra.Polynomial.Taylor
/-- The `k`th coefficient of `Polynomial.taylor r f` is `(Polynomial.hasseDeriv k f).eval r`.  -/
Polynomial.taylor_coeff : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (f : Polynomial R) (n : ℕ),
  ((Polynomial.taylor r) f).coeff n = Polynomial.eval r ((Polynomial.hasseDeriv n) f)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.isPrestackFor' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat)
  {J : CategoryTheory.GrothendieckTopology C} [F.IsPrestack J] {S : C}, ∀ R ∈ J S, F.IsPrestackFor R.arrows
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.get!_eq_getValue! : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited β] {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α},
      Std.DHashMap.Internal.Raw₀.Const.get! m a =
        Std.Internal.List.getValue! a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Lean.Meta.CtorIdxHInj
_private.Lean.Meta.CtorIdxHInj.0.Lean.Meta.mkHInjectiveTheorem?.repeatIntroSubstRefl : Lean.MVarId → Lean.MetaM Unit
-- Init.Data.List.OfFn
List.ofFnM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] {n : ℕ} {f : Fin n → α},
  (List.ofFnM fun i => pure (f i)) = pure (List.ofFn f)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_compl : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommGroup M] [inst_1 : TopologicalSpace M]
  [T2Space M] {v : MeasureTheory.VectorMeasure α M} {A : Set α}, MeasurableSet A → v Aᶜ = v Set.univ - v A
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.Coe.ringHom_apply : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (self : ↥(PadicInt.subring p)), PadicInt.Coe.ringHom self = ↑self
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- Eta-expanded form of `HasDerivAt.smul` -/
HasDerivAt.fun_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'}
  {c' : 𝕜'}, HasDerivAt c c' x → HasDerivAt f f' x → HasDerivAt (fun i => c i • f i) (c x • f' + c' • f x) x
-- Mathlib.Algebra.Group.Basic
zsmul_iterate : ∀ {G : Type u_3} [inst : AddGroup G] (k : ℤ) (n : ℕ), (fun x => k • x)^[n] = fun x => k ^ n • x
-- Mathlib.Algebra.Group.Units.Equiv
/-- Right multiplication by a unit of a monoid is a permutation of the underlying type.  -/
Units.mulRight : {M : Type u_3} → [inst : Monoid M] → Mˣ → Equiv.Perm M