mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.count_withDensity' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {f : α → ENNReal},
  Measurable f →
    MeasureTheory.Measure.count.withDensity f = MeasureTheory.Measure.sum fun a => f a • MeasureTheory.Measure.dirac a
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzOnWith.add : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E} {s : Set α},
  LipschitzOnWith Kf f s → LipschitzOnWith Kg g s → LipschitzOnWith (Kf + Kg) (fun x => f x + g x) s
-- Mathlib.Topology.Order.OrderClosed
continuous_if_le : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α]
  {f g : β → α} [inst_3 : TopologicalSpace β] [inst_4 : TopologicalSpace γ] [inst_5 : (x : β) → Decidable (f x ≤ g x)]
  {f' g' : β → γ},
  Continuous f →
    Continuous g →
      ContinuousOn f' {x | f x ≤ g x} →
        ContinuousOn g' {x | g x ≤ f x} →
          (∀ (x : β), f x = g x → f' x = g' x) → Continuous fun x => if f x ≤ g x then f' x else g' x
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compMeasurable.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] [inst_3 : MeasurableSpace β]
  [inst_4 : TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : BorelSpace β] [inst_6 : MeasurableSpace γ]
  [inst_7 : TopologicalSpace.PseudoMetrizableSpace γ] [inst_8 : OpensMeasurableSpace γ]
  [inst_9 : SecondCountableTopology γ] (g g_1 : β → γ) (e_g : g = g_1) (hg : Measurable g) (f f_1 : α →ₘ[μ] β),
  f = f_1 → MeasureTheory.AEEqFun.compMeasurable g hg f = MeasureTheory.AEEqFun.compMeasurable g_1 ⋯ f_1
-- Mathlib.ModelTheory.ElementarySubstructures
/-- The closure of a set meeting definable sets is equal to itself.  -/
FirstOrder.Language.MeetsDefinable.closure_eq_self : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {A : Set M},
  FirstOrder.Language.MeetsDefinable A → ↑((FirstOrder.Language.Substructure.closure L).toFun A) = A
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.funLike : {E : Type u_3} → [inst : AddGroup E] → FunLike (NonarchAddGroupSeminorm E) E ℝ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.norm : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E},
  IntervalIntegrable f μ a b → IntervalIntegrable (fun x => ‖f x‖) μ a b
-- Mathlib.Combinatorics.Quiver.Path.Vertices
/-- `split_at_vertex` decomposes a path `p` at the vertex sitting in
position `i` of its `vertices`  -/
Quiver.Path.exists_eq_comp_and_length_eq_of_lt_length : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) (n : ℕ) (hn : n < p.vertices.length),
  ∃ v p₁ p₂, p = p₁.comp p₂ ∧ p₁.length = n ∧ v = p.vertices[n]
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.liftWith_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (f : ({β : Type u} → ExceptT ε m β → m (Except ε β)) → m α),
  ⦃(Std.Do.wp (f fun {β} x => x.run)).apply (Q.1, Q.2.2)⦄ MonadControl.liftWith f ⦃Q⦄
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- The additive submonoid fixing a set under an `AddAction`.  -/
fixingAddSubmonoid : (M : Type u_1) → {α : Type u_2} → [inst : AddMonoid M] → [AddAction M α] → Set α → AddSubmonoid M
-- Mathlib.Data.Part
Part.sdiff_def : ∀ {α : Type u_1} [inst : SDiff α] (a b : Part α),
  a \ b = do
    let y ← a
    Part.map (fun x => y \ x) b
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_toInt : ∀ (x : Int32), Int32.ofIntLE x.toInt ⋯ ⋯ = x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {l : List α},
  (t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condExpKernel_comp_trim : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ mΩ),
  (μ.trim hm).bind ⇑(ProbabilityTheory.condExpKernel μ m) = μ
-- Mathlib.Topology.Separation.Hausdorff
T2Quotient.mk_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X},
  T2Quotient.mk x = T2Quotient.mk y ↔ ∀ (s : Setoid X), T2Space (Quotient s) → s x y
-- Mathlib.CategoryTheory.ObjectProperty.Orthogonal
CategoryTheory.ObjectProperty.instContainsZeroRightOrthogonalOfHasZeroObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C], P.rightOrthogonal.ContainsZero
-- Batteries.Data.UInt
instLawfulOrdUSize : Std.LawfulOrd USize
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddCommGrpCat.FilteredColimits.colimitCocone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddCommGrpCat),
  AddCommGrpCat.FilteredColimits.colimitCocone F =
    { pt := AddCommGrpCat.FilteredColimits.colimit F,
      ι :=
        {
          app := fun J_1 =>
            AddCommGrpCat.ofHom
              (AddGrpCat.Hom.hom
                ((AddGrpCat.FilteredColimits.colimitCocone
                        (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat))).ι.app
                  J_1)),
          naturality := ⋯ } }
-- Mathlib.Data.Fin.Tuple.Reflection
/-- Produce a term of the form `f 0 + f 1 + ... + f (n - 1)` and an application of `FinVec.sum_eq`
that shows it is equal to `∑ i, f i`.  -/
FinVec.mkSumEqQ : {u : Lean.Level} →
  {α : Q(Type u)} →
    (inst : Q(AddCommMonoid «$α»)) →
      (n : ℕ) → (f : Q(Fin «$n» → «$α»)) → Lean.MetaM ((val : Q(«$α»)) × Q(∑ i, «$f» i = «$val»))
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.neg_mem_iff : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : SubMulAction R M)
  {x : M}, -x ∈ p ↔ x ∈ p
-- Init.Grind.ToInt
Lean.Grind.IntInterval.wrap.eq_2 : ∀ (x lo : ℤ), (Lean.Grind.IntInterval.ci lo).wrap x = max x lo
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
/-- The product of localizations at all maximal ideals of a commutative semiring.  -/
MaximalSpectrum.PiLocalization : (R : Type u_1) → [CommSemiring R] → Type u_1
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.apply_pure_cons_entails_r : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs} {φ : Prop} {σ : Type u} {s : σ}, (P ⊢ₛ ⌜φ⌝) → P ⊢ₛ ⌜φ⌝ s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k k' fallback : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
          k ∈ List.map Sigma.fst l → (m.insertMany l).getKeyD k' fallback = k
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.IsDetpBalanced.of_eq : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] {A : Matrix n n R}
  {a b : R}, Matrix.detp 1 A = Matrix.detp (-1) A → A.IsDetpBalanced a b
-- Mathlib.Algebra.Algebra.Equiv
/-- The proposition that the function preserves addition  -/
AlgEquiv.map_add' : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (self : A ≃ₐ[R] B) (x y : A),
  self.toFun (x + y) = self.toFun x + self.toFun y
-- Mathlib.NumberTheory.Dioph
Dioph.pell_dioph : Dioph
  {v |
    ∃ (h : 1 < v (Fin2.ofNat' 0)),
      Pell.xn h (v (Fin2.ofNat' 1)) = v (Fin2.ofNat' 2) ∧ Pell.yn h (v (Fin2.ofNat' 1)) = v (Fin2.ofNat' 3)}
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- A cocone is a colimit cocone iff it is initial.  -/
CategoryTheory.Limits.Cocone.isColimitEquivIsInitial : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) → CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsInitial c
-- Init.Data.Iterators.ToIterator
/-- Replaces `ToIterator.iter` with its definition.  -/
Std.ToIterator.iter_eq : ∀ {γ : Type u} {x : γ} {α β : Type v} {it : γ → Std.IterM Id β}, Std.ToIterator.iter x = (it x).toIter
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- `G.CliqueFreeOn s n` means that `G` has no `n`-cliques contained in `s`.  -/
SimpleGraph.CliqueFreeOn : {α : Type u_1} → SimpleGraph α → Set α → ℕ → Prop
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.overEquivalence_unitIso_hom_app_left : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) (X_1 : CategoryTheory.Over U),
  (U.overEquivalence.unitIso.hom.app X_1).left = CategoryTheory.eqToHom ⋯
-- Init.Data.List.Monadic
List.foldlM_attachWith : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {l : List α} {q : α → Prop}
  (H : ∀ a ∈ l, q a) {f : β → { x // q x } → m β} {b : β},
  List.foldlM f b (l.attachWith q H) =
    List.foldlM
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b l.attach
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonRenameFile.fromJson : Lean.Json → Except String Lean.Lsp.RenameFile
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α], Associates.factors 0 = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The binary product functor.  -/
CategoryTheory.Limits.prod.functor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasBinaryProducts C] → CategoryTheory.Functor C (CategoryTheory.Functor C C)
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.uIoc_subset_of_mem_disjWithin : ∀ {a b : ℝ} {n : ℕ} {I : ℕ → ℝ × ℝ},
  (n, I) ∈ AbsolutelyContinuousOnInterval.disjWithin a b → ∀ {i : ℕ}, i < n → Set.uIoc (I i).1 (I i).2 ⊆ Set.uIoc a b
-- Mathlib.LinearAlgebra.TensorProduct.Defs
instAddZeroClassTensorProduct : (R : Type u_3) →
  [inst : CommSemiring R] →
    (M : Type u_1) →
      (N : Type u_2) →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → AddZeroClass (TensorProduct R M N)
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.ShortComplex.exact_cokernel : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y),
  { X₁ := X, X₂ := Y, X₃ := CategoryTheory.Limits.cokernel f, f := f, g := CategoryTheory.Limits.cokernel.π f,
      zero := ⋯ }.Exact
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.HasEval.hpow : ∀ {σ : Type u_1} {S : Type u_3} [inst : CommRing S] [inst_1 : TopologicalSpace S] {a : σ → S},
  MvPowerSeries.HasEval a → ∀ (s : σ), IsTopologicallyNilpotent (a s)
-- Mathlib.Algebra.Group.Conj
AddConjClasses.instDecidableEqOfDecidableRelIsAddConj.eq_1 : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : DecidableRel IsAddConj],
  AddConjClasses.instDecidableEqOfDecidableRelIsAddConj = AddConjClasses.instDecidableEqOfDecidableRelIsAddConj._aux_1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeReachable.refl : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ} (u : V), G.IsEdgeReachable k u u
-- Init.Data.Array.Range
Array.range'_zero : ∀ {s step : ℕ}, Array.range' s 0 step = #[]
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Module.FaithfullyFlat.bijective_of_tensorProduct : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_3}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Module.FaithfullyFlat R S],
  Function.Bijective ⇑(algebraMap S (TensorProduct R S T)) → Function.Bijective ⇑(algebraMap R T)
-- Std.Data.TreeMap.Raw.Lemmas
/-- Variant of `getElem?_map` that holds without `LawfulEqCmp`.  -/
Std.TreeMap.Raw.getElem?_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α} (h : t.WF),
  (Std.TreeMap.Raw.map f t)[k]? = Option.pmap (fun v h' => f (t.getKey k h') v) t[k]? ⋯
-- Init.Data.SInt.Lemmas
Int16.sub_nonneg_of_le : ∀ {a b : Int16}, 0 ≤ b → b ≤ a → 0 ≤ a - b
-- Mathlib.Algebra.GroupWithZero.NeZero
inv_mul_cancel₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a⁻¹ * a = 1
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.eventuallyEq_of_mem_source : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) {x : M} [inst_5 : FiniteDimensional ℝ E],
  x ∈ (chartAt H c).source → ↑f =ᶠ[nhds x] ↑f.toContDiffBump ∘ ↑(extChartAt I c)
-- Mathlib.Combinatorics.Graph.Basic
/-- The vertex set.  -/
Graph.vertexSet : {α : Type u_3} → {β : Type u_4} → Graph α β → Set α
-- Mathlib.Order.CompleteLattice.Basic
Antitone.map_sSup_le : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {s : Set α} {f : α → β},
  Antitone f → f (sSup s) ≤ ⨅ a ∈ s, f a
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.lift_rank_of_isFractionRing : ∀ (R : Type u_1) [inst : CommRing R] (R' : Type u_4) (S : Type u) [inst_1 : CommRing R'] [inst_2 : CommRing S]
  [inst_3 : Algebra R S] [inst_4 : Algebra R R'] [IsFractionRing R R'] [FaithfulSMul R S] [Algebra.IsAlgebraic R S]
  [NoZeroDivisors S] (S' : Type v) [inst_9 : CommRing S'] [inst_10 : Algebra R S'] [inst_11 : Algebra S S']
  [inst_12 : Module R' S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsFractionRing S S'],
  Cardinal.lift.{u, v} (Module.rank R' S') = Cardinal.lift.{v, u} (Module.rank R S)
-- Mathlib.NumberTheory.SelbergSieve
/-- An approximation to `∑ i in support, weights i`, i.e. the size of the unsifted set. A bad
approximation will yield a weak statement in the final theorem.  -/
BoundingSieve.totalMass : BoundingSieve → ℝ
-- Mathlib.Data.List.Permutation
List.permutationsAux_nil : ∀ {α : Type u_1} (is : List α), [].permutationsAux is = []
-- Mathlib.RingTheory.Frobenius
/-- A Frobenius element at `Q` restricts to an automorphism of `S_Q`.  -/
AlgHom.IsArithFrobAt.localize : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {φ : S →ₐ[R] S} →
            {Q : Ideal S} →
              φ.IsArithFrobAt Q → [inst_3 : Q.IsPrime] → Localization.AtPrime Q →ₐ[R] Localization.AtPrime Q
-- Mathlib.RingTheory.Flat.Localization
Module.flat_of_isLocalized_maximal : ∀ {R : Type u_1} (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower R S M]
  (Mₚ : (P : Ideal S) → [P.IsMaximal] → Type u_4) [inst_7 : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_8 : (P : Ideal S) → [inst_8 : P.IsMaximal] → Module R (Mₚ P)]
  [inst_9 : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)]
  [∀ (P : Ideal S) [inst_10 : P.IsMaximal], IsScalarTower R S (Mₚ P)]
  (f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P)
  [∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)],
  (∀ (P : Ideal S) [inst_12 : P.IsMaximal], Module.Flat R (Mₚ P)) → Module.Flat R M
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {a : α},
  ∅[a]! = default
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.eq_of_le_of_card_ge : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [Finite ↥K], H ≤ K → Nat.card ↥K ≤ Nat.card ↥H → H = K
-- Mathlib.Algebra.Group.Subgroup.Even
Submonoid.square.eq_1 : ∀ (M : Type u_1) [inst : CommMonoid M], Submonoid.square M = { toSubsemigroup := Subsemigroup.square M, one_mem' := ⋯ }
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.linearIndependent_pair_of_ne : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  {i j : ↥b.support}, i ≠ j → LinearIndependent R ![P.root ↑i, P.root ↑j]
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.subsemigroupMap_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (M' : AddSubsemigroup M),
  Function.Surjective ⇑(f.subsemigroupMap M')
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_eq_single : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {s : Finset ι} {f : ι → M} (a : ι),
  (∀ b ∈ s, b ≠ a → f b = 1) → (a ∉ s → f a = 1) → ∏ x ∈ s, f x = f a
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasLaw.hasGaussianLaw : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : TopologicalSpace E]
  [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E] {mE : MeasurableSpace E} {X : Ω → E} {μ : MeasureTheory.Measure E},
  ProbabilityTheory.HasLaw X μ P → ∀ [ProbabilityTheory.IsGaussian μ], ProbabilityTheory.HasGaussianLaw X P
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- Polynomial evaluation commutes with `List.sum`.  -/
Polynomial.eval_listSum : ∀ {R : Type u} [inst : Semiring R] (l : List (Polynomial R)) (x : R),
  Polynomial.eval x l.sum = (List.map (Polynomial.eval x) l).sum
-- Mathlib.Analysis.Normed.Group.Pointwise
neg_closedBall : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), -Metric.closedBall x δ = Metric.closedBall (-x) δ
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.mem_smul_iff : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i j : ι} {m₁ : M i} {m₂ : M j} {w : Monoid.CoprodI.Word M},
  ⟨i, m₁⟩ ∈ (Monoid.CoprodI.of m₂ • w).toList ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ w.toList.tail ∨
            (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
/-- Given `X : DerivedCategory.Plus C` and `n : ℤ`, this property means
that `X` is `≥ n` for the canonical t-structure.  -/
DerivedCategory.Plus.IsGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → [inst_2 : HasDerivedCategory C] → DerivedCategory.Plus C → ℤ → Prop
-- Aesop.Forward.Match
_private.Aesop.Forward.Match.0.Aesop.forwardRuleMatchesToRules? : {α : Type} → Array Aesop.ForwardRuleMatch → (Aesop.ForwardRuleMatch → Option α) → Option (Array (Aesop.Rule α))
-- Mathlib.Analysis.Fourier.ZMod
ZMod.invDFT_def : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Ψ : ZMod N → E),
  ZMod.dft.symm Ψ = fun k => (↑N)⁻¹ • ∑ j, ZMod.stdAddChar (j * k) • Ψ j
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_right_cancel_iff_of_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b c : α} [inst_1 : PartialOrder α] [MulPosReflectLE α],
  0 < b → (a * b = c * b ↔ a = c)
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigO_norm_norm`. -/
Asymptotics.IsBigO.of_norm_norm : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α}, ((fun x => ‖f' x‖) =O[l] fun x => ‖g' x‖) → f' =O[l] g'
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofLeGe.sizeOf_spec : ∀ (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofLeGe c₁ c₂) = 1 + sizeOf c₁ + sizeOf c₂
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.ind : ∀ {M : Type u_1} [inst : AddCommMonoid M] {motive : DivisibleHull M → Prop},
  (∀ (num : M) (den : ℕ+), motive (DivisibleHull.mk num den)) → ∀ (x : DivisibleHull M), motive x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_filter_key_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → Bool},
  (Std.DHashMap.filter (fun a x => f a) m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) = false
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Given three points on a circle, the radius of that circle may be expressed explicitly as half
the distance between two of those points divided by the absolute value of the sine of the angle
at the third point (a version of the law of sines or sine rule).  -/
EuclideanGeometry.Sphere.dist_div_sin_oangle_div_two_eq_radius : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
  p₁ ∈ s →
    p₂ ∈ s →
      p₃ ∈ s → p₁ ≠ p₂ → p₁ ≠ p₃ → p₂ ≠ p₃ → dist p₁ p₃ / |(EuclideanGeometry.oangle p₁ p₂ p₃).sin| / 2 = s.radius
-- Mathlib.Analysis.Normed.Group.Pointwise
smul_sphere_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), x • Metric.sphere 1 δ = Metric.sphere x δ
-- Mathlib.CategoryTheory.Adjunction.Quadruple
/-- Structure containing the three adjunctions of an adjoint quadruple `L ⊣ F ⊣ G ⊣ R`.  -/
CategoryTheory.Adjunction.Quadruple : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.Functor D C →
            CategoryTheory.Functor C D → CategoryTheory.Functor D C → Type (max (max (max u₁ u₂) v₁) v₂)
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageKind.response : Lean.JsonRpc.MessageKind
-- Mathlib.RingTheory.Localization.Algebra
IsLocalization.map_linearMap_eq_toLinearMap_mapₐ : ∀ {R : Type u_5} [inst : CommSemiring R] (M : Submonoid R) {A : Type u_6} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] (Rₚ : Type u_8) [inst_3 : CommSemiring Rₚ] [inst_4 : Algebra R Rₚ]
  [inst_5 : IsLocalization M Rₚ] (Aₚ : Type u_9) [inst_6 : CommSemiring Aₚ] [inst_7 : Algebra R Aₚ]
  [inst_8 : Algebra A Aₚ] [inst_9 : IsScalarTower R A Aₚ]
  [inst_10 : IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] [inst_11 : Algebra Rₚ Aₚ]
  [inst_12 : IsScalarTower R Rₚ Aₚ],
  (IsLocalizedModule.map M (Algebra.linearMap R Rₚ) (IsScalarTower.toAlgHom R A Aₚ).toLinearMap)
      (Algebra.linearMap R A) =
    ↑R (IsLocalization.mapₐ M Rₚ Rₚ Aₚ (Algebra.ofId R A)).toLinearMap
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.leadingCoeff.eq_1 : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  (D : A → B) [inst_3 : Nonempty A] (f : AddMonoidAlgebra R A),
  AddMonoidAlgebra.leadingCoeff D f = f.coeff (Function.invFun D (AddMonoidAlgebra.supDegree D f))
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasurableEmbedding.mutuallySingular_map : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {β : Type u_2} {x : MeasurableSpace β}
  {f : α → β},
  MeasurableEmbedding f →
    μ.MutuallySingular ν → (MeasureTheory.Measure.map f μ).MutuallySingular (MeasureTheory.Measure.map f ν)
-- Mathlib.Algebra.Group.Defs
pow_mul : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ m) ^ n
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.self_trans_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : Add R] [inst_1 : Add S] [inst_2 : Mul R] [inst_3 : Mul S] (e : R ≃+* S),
  e.trans e.symm = RingEquiv.refl R
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.instFunLike : (M : Type u_4) → [inst : MulOne M] → FunLike (Monoid.End M) M M