mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The `DistribMulActionHom` underlying a `LinearMap`.  -/
LinearMap.toDistribMulActionHom : {R : Type u_1} →
  {S : Type u_5} →
    {M : Type u_8} →
      {M₃ : Type u_11} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] → [inst_5 : Module S M₃] → {σ : R →+* S} → (M →ₛₗ[σ] M₃) → M →ₑ+[↑σ] M₃
-- Init.Data.Nat.Mod
Nat.mod_pow_succ : ∀ {x b k : ℕ}, x % b ^ (k + 1) = x % b ^ k + b ^ k * (x / b ^ k % b)
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- The colimit of the constant `⊥_ C` functor is `⊥_ C`.  -/
CategoryTheory.Limits.colimitConstInitial : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasInitial C] →
          CategoryTheory.Limits.colimit ((CategoryTheory.Functor.const J).obj (⊥_ C)) ≅ ⊥_ C
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.reverse_injective : ∀ {T : Type u_1} {N : Type u_2}, Function.Injective ContextFreeRule.reverse
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_div : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] {K' : Type u_5} [inst_5 : Field K'] [inst_6 : Algebra R₁ K']
  [inst_7 : IsFractionRing R₁ K'] (I J : FractionalIdeal (nonZeroDivisors R₁) K) (h : K ≃ₐ[R₁] K'),
  FractionalIdeal.map (↑h) (I / J) = FractionalIdeal.map (↑h) I / FractionalIdeal.map (↑h) J
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.finSuccEquiv_apply : ∀ (R : Type u) [inst : CommSemiring R] (n : ℕ) (p : MvPolynomial (Fin (n + 1)) R),
  (MvPolynomial.finSuccEquiv R n) p =
    (MvPolynomial.eval₂Hom (Polynomial.C.comp MvPolynomial.C) fun i =>
        Fin.cases Polynomial.X (fun k => Polynomial.C (MvPolynomial.X k)) i)
      p
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An additive submonoid contains `0`.  -/
AddSubmonoid.zero_mem' : ∀ {M : Type u_3} [inst : AddZeroClass M] (self : AddSubmonoid M), 0 ∈ self.carrier
-- Mathlib.Topology.UniformSpace.Basic
iInf_uniformity : ∀ {α : Type ua} {ι : Sort u_2} {u : ι → UniformSpace α}, uniformity α = ⨅ i, uniformity α
-- Init.Data.Order.Classes
Std.LawfulOrderLeftLeaningMax.max_eq_left : ∀ {α : Type u} {inst : Max α} {inst_1 : LE α} [self : Std.LawfulOrderLeftLeaningMax α] (a b : α), b ≤ a → a ⊔ b = a
-- Init.Data.SInt.Lemmas
Int8.ofInt_neg : ∀ (a : ℤ), Int8.ofInt (-a) = -Int8.ofInt a
-- Batteries.Data.List.Lemmas
List.pairwise_cons_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α},
  List.Pairwise R (a :: b :: l) ↔ R a b ∧ List.Pairwise R (a :: l) ∧ List.Pairwise R (b :: l)
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.integral_tilted_mul_eq_mgf : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : Ω → E),
  (∫ (ω : Ω), g ω ∂μ.tilted fun x => t * X x) = ∫ (ω : Ω), (Real.exp (t * X ω) / ProbabilityTheory.mgf X μ t) • g ω ∂μ
-- Aesop.Tree.State
Aesop.TreeRef.markSubtreeIrrelevant : Aesop.TreeRef → BaseIO Unit
-- Lean.Elab.Command
Lean.Elab.Command.instMonadLogCommandElabM : Lean.MonadLog Lean.Elab.Command.CommandElabM
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.State.map : Lean.Meta.Sym.State✝ → Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Expr
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.approxOn.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] (f f_1 : β → α) (e_f : f = f_1) (hf : Measurable f)
  (s s_1 : Set α) (e_s : s = s_1) (y₀ y₀_1 : α) (e_y₀ : y₀ = y₀_1) (h₀ : y₀ ∈ s)
  [inst_4 : TopologicalSpace.SeparableSpace ↑s] (n n_1 : ℕ),
  n = n_1 → MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n = MeasureTheory.SimpleFunc.approxOn f_1 ⋯ s_1 y₀_1 ⋯ n_1
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.restr_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : LieAlgebra R L] (N : LieSubmodule R L M)
  (H : LieSubalgebra R L), ↑(N.restr H) = ↑N
-- Mathlib.Data.List.Chain
List.isChain_of_isChain_map : ∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} {S : β → β → Prop} (f : α → β),
  (∀ (a b : α), S (f a) (f b) → R a b) → ∀ {l : List α}, List.IsChain S (List.map f l) → List.IsChain R l
-- Init.Data.Order.Lemmas
Std.instAntisymmOfAsymm : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Asymm r], Std.Antisymm r
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.Pseudofunctor B C} (θ : G ⟶ H) {a b : B} {a' : C} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h)
  {Z : a' ⟶ H.obj b}
  (h_1 : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (θ.app a) (H.map h)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) (θ.app b)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality h).hom) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.map₂ β))) h_1)
-- Std.Internal.UV.UDP
/-- Binds an UDP socket to a specific address. Address reuse is enabled to allow rebinding the
same address.
 -/
Std.Internal.UV.UDP.Socket.bind : Std.Internal.UV.UDP.Socket → Std.Net.SocketAddress → IO Unit
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- Move everything from the `rev` stack to the `main` stack (reversed).  -/
Turing.PartrecToTM2.unrev : Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Λ'
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Sigma.isoColimit.eq_1 : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }]
  [inst_2 : CategoryTheory.Limits.HasColimit X],
  CategoryTheory.Limits.Sigma.isoColimit X =
    (CategoryTheory.Limits.coproductIsCoproduct' X).coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit X)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.mk : Option Std.Time.Year.Era →
  Option Std.Time.Year.Offset →
    Option Std.Time.Year.Offset →
      Option Std.Time.Year.Offset →
        Option (Sigma Std.Time.Day.Ordinal.OfYear) →
          Option Std.Time.Month.Ordinal →
            Option Std.Time.Month.Ordinal →
              Option Std.Time.Day.Ordinal →
                Option Std.Time.Month.Quarter →
                  Option Std.Time.Month.Quarter →
                    Option Std.Time.Week.OfYear.Ordinal →
                      Option Std.Time.Week.Ordinal →
                        Option Std.Time.Weekday →
                          Option Std.Time.Weekday →
                            Option Std.Time.Weekday →
                              Option (Std.Time.Internal.Bounded.LE 1 5) →
                                Option Std.Time.HourMarker →
                                  Option Std.Time.DayPeriod →
                                    Option Std.Time.ExtendedDayPeriod →
                                      Option (Std.Time.Internal.Bounded.LE 1 12) →
                                        Option (Std.Time.Internal.Bounded.LE 0 11) →
                                          Option (Std.Time.Internal.Bounded.LE 1 24) →
                                            Option Std.Time.Hour.Ordinal →
                                              Option Std.Time.Minute.Ordinal →
                                                Option (Std.Time.Second.Ordinal true) →
                                                  Option Std.Time.Nanosecond.Ordinal →
                                                    Option Std.Time.Millisecond.Offset →
                                                      Option Std.Time.Nanosecond.Ordinal →
                                                        Option Std.Time.Nanosecond.Offset →
                                                          Option String →
                                                            Option String →
                                                              Option String →
                                                                Option String →
                                                                  Option Std.Time.TimeZone.Offset →
                                                                    Option Std.Time.TimeZone.Offset →
                                                                      Option Std.Time.TimeZone.Offset →
                                                                        Option Std.Time.TimeZone.Offset →
                                                                          Std.Time.GenericFormat.DateBuilder✝
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- The natural map from a nonsingular projective point representative on a Weierstrass curve to its
corresponding nonsingular point in affine coordinates.  -/
WeierstrassCurve.Projective.Point.toAffine : {F : Type u} → [inst : Field F] → (W : WeierstrassCurve.Projective F) → (Fin 3 → F) → W.toAffine.Point
-- Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
/-- Given a measurable function `f` with values in `ℝ≥0` in a sigma-finite space, there exists a
lower semicontinuous function `g > f` with integral arbitrarily close to that of `f`.
Formulation in terms of `lintegral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`.  -/
MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α)
  [μ.WeaklyRegular] [MeasureTheory.SigmaFinite μ] (f : α → NNReal),
  Measurable f →
    ∀ {ε : ENNReal},
      ε ≠ 0 → ∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
-- Lean.Structure
/-- Gets the constructor of an inductive type that has exactly one constructor.
This is meant to be used with types that have had been registered as a structure by `registerStructure`,
but this is not checked.

Warning: this does not check that the type has no indices.
 -/
Lean.getStructureCtor : Lean.Environment → Lean.Name → Lean.ConstructorVal
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- If one controls the norm of every `A x`, then one controls the norm of `A`.  -/
_private.Mathlib.Analysis.Distribution.SchwartzSpace.Basic.0.SchwartzMap.seminormAux_le_bound : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (k n : ℕ) (f : SchwartzMap E F) {M : ℝ},
  0 ≤ M → (∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M) → SchwartzMap.seminormAux✝ k n f ≤ M
-- Init.Core
/-- `spawn fn : Task α` constructs and immediately launches a new task for
evaluating the function `fn () : α` asynchronously.

`prio`, if provided, is the priority of the task.
 -/
Task.spawn : {α : Type u} → (Unit → α) → optParam Task.Priority Task.Priority.default → Task α
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.isConstructible_of_subset_of_isCompact : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X} [PrespectralSpace X] [QuasiSeparatedSpace X],
  Topology.IsLocallyConstructible s → s ⊆ t → IsCompact t → Topology.IsConstructible s
-- Mathlib.Data.List.SplitLengths
List.splitLengths_nil : ∀ {α : Type u_1} (l : List α), [].splitLengths l = []
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.mk.inj : ∀ {α : Type u_2} {toFilter : Filter α} {neBot' : toFilter.NeBot}
  {le_of_le : ∀ (g : Filter α), g.NeBot → g ≤ toFilter → toFilter ≤ g} {toFilter_1 : Filter α}
  {neBot'_1 : toFilter_1.NeBot} {le_of_le_1 : ∀ (g : Filter α), g.NeBot → g ≤ toFilter_1 → toFilter_1 ≤ g},
  { toFilter := toFilter, neBot' := neBot', le_of_le := le_of_le } =
      { toFilter := toFilter_1, neBot' := neBot'_1, le_of_le := le_of_le_1 } →
    toFilter = toFilter_1
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.toUniformSpace : {R : Type u} →
  {inst : Ring R} →
    {Γ₀ : outParam (Type v)} → {inst_1 : LinearOrderedCommGroupWithZero Γ₀} → [self : Valued R Γ₀] → UniformSpace R
-- Mathlib.Algebra.BigOperators.Ring.Finset
Int.sum_div : ∀ {ι : Type u_5} {s : Finset ι} {f : ι → ℤ} {n : ℤ}, (∀ i ∈ s, n ∣ f i) → (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
-- Mathlib.Order.Interval.Set.Basic
Set.notMem_Ioc_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, c ≤ a → c ∉ Set.Ioc a b
-- Mathlib.CategoryTheory.SingleObj
CategoryTheory.SingleObj.inv_as_inv : ∀ (G : Type u) [inst : Group G] {x y : CategoryTheory.SingleObj G} (f : x ⟶ y), CategoryTheory.inv f = f⁻¹
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.lift₂Expand_of : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_3}
  [inst_2 : MulAction R X] {C : Sort u_2} {P : X → ↥S → X → ↥S → C}
  {hP :
    ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
      P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩}
  (r₁ : X) (s₁ : ↥S) (r₂ : X) (s₂ : ↥S), OreLocalization.lift₂Expand P hP (r₁ /ₒ s₁) (r₂ /ₒ s₂) = P r₁ s₁ r₂ s₂
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- If `p` is an independent family of submodules of an `R`-finite module `M`, then the
number of nontrivial subspaces in the family `p` is bounded above by the dimension of `M`.

Note that the `Fintype` hypothesis required here can be provided by
`iSupIndep.fintypeNeBotOfFiniteDimensional`.  -/
iSupIndep.subtype_ne_bot_le_finrank : ∀ {ι : Type w} {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] [Module.Finite R M] [StrongRankCondition R] {p : ι → Submodule R M},
  iSupIndep p → ∀ [inst_7 : Fintype { i // p i ≠ ⊥ }], Fintype.card { i // p i ≠ ⊥ } ≤ Module.finrank R M
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.instLTQOfOrderedAdd : {α : Type u} →
  [inst : Lean.Grind.NatModule α] →
    [inst_1 : LE α] →
      [inst_2 : Std.IsPreorder α] → [Lean.Grind.OrderedAdd α] → LT (Lean.Grind.IntModule.OfNatModule.Q α)
-- Mathlib.Topology.NhdsWithin
nhdsWithin_restrict : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} (s : Set α) {t : Set α},
  a ∈ t → IsOpen t → nhdsWithin a s = nhdsWithin a (s ∩ t)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ico₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {c : G₀} (a b : G₀),
  0 < c → (fun x => x * c) ⁻¹' Set.Ico a b = Set.Ico (a / c) (b / c)
-- Mathlib.LinearAlgebra.Finsupp.SumProd
Finsupp.sigmaFinsuppLEquivPiFinsupp_apply : ∀ (R : Type u_5) [inst : Semiring R] {η : Type u_7} [inst_1 : Fintype η] {M : Type u_9} {ιs : η → Type u_10}
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (f : (j : η) × ιs j →₀ M) (j : η) (i : ιs j),
  ((Finsupp.sigmaFinsuppLEquivPiFinsupp R) f j) i = f ⟨j, i⟩
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasKernel S.g] (hf : S.f = 0),
  (CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel S hf).p = CategoryTheory.CategoryStruct.id S.X₂
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.ExprWithHoles.mk.inj : ∀ {ref : Lean.Syntax} {expr : Lean.Expr} {ref_1 : Lean.Syntax} {expr_1 : Lean.Expr},
  { ref := ref, expr := expr } = { ref := ref_1, expr := expr_1 } → ref = ref_1 ∧ expr = expr_1
-- Mathlib.SetTheory.ZFC.Class
Class.mem_wf : WellFounded fun x1 x2 => x1 ∈ x2
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_X₃ : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' pq'' : κ) (i₀' i₀ i₁ i₂ i₃ : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃
        hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).X₃ =
    CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX X data r pq'' ⋯
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.IsClosedUnderQuotients.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f], P X → P Y) → P.IsClosedUnderQuotients
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.symm : ∀ {V : Type u} {G : SimpleGraph V} (self : G.Subgraph), Std.Symm self.Adj
-- Init.Data.Dyadic.Basic
Dyadic.instHShiftRightInt : HShiftRight Dyadic ℤ Dyadic
-- Mathlib.Analysis.Meromorphic.Basic
/-- `MeromorphicAt` is invariant under translation.  -/
meromorphicAt_comp_add_const_iff_meromorphicAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x c : 𝕜} {f : 𝕜 → E}, MeromorphicAt (f ∘ fun x => x + c) x ↔ MeromorphicAt f (x + c)
-- Mathlib.RingTheory.PrincipalIdealDomain
Prime.coprime_iff_not_dvd : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] [IsDomain R] {p n : R}, Prime p → (IsCoprime p n ↔ ¬p ∣ n)
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_div_ball : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E), {x} / Metric.ball y δ = Metric.ball (x / y) δ
-- Mathlib.Analysis.MeanInequalitiesPow
ENNReal.rpow_add_rpow_le_add : ∀ {p : ℝ} (a b : ENNReal), 1 ≤ p → (a ^ p + b ^ p) ^ (1 / p) ≤ a + b
-- Mathlib.Tactic.Choose
/-- A wrapper around `choose1` that parses identifiers, adds variable info to new variables,
and optionally checks the type annotation.  -/
Mathlib.Tactic.Choose.choose1WithInfo : Lean.MVarId →
  Bool →
    Option Lean.Expr →
      Mathlib.Tactic.Choose.ChooseArg → Lean.Elab.TermElabM (Mathlib.Tactic.Choose.ElimStatus × Lean.MVarId)
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongr_apply : ∀ {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂),
  ⇑(e₁.prodCongr e₂) = Prod.map ⇑e₁ ⇑e₂
-- Std.Data.DHashMap.Basic
/-- Checks whether a key is present in a map and inserts a value for the key if it was not found.

If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`, then
the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.
 -/
Std.DHashMap.containsThenInsertIfNew : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → (a : α) → β a → Bool × Std.DHashMap α β
-- Mathlib.Data.Analysis.Filter
/-- Construct a realizer for `comap m f` given a realizer for `f`  -/
Filter.Realizer.comap : {α : Type u_1} → {β : Type u_2} → (m : α → β) → {f : Filter β} → f.Realizer → (Filter.comap m f).Realizer
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_add_int_mul_two_pi : ∀ (x : ℂ) (n : ℤ), Complex.sin (x + ↑n * (2 * ↑Real.pi)) = Complex.sin x
-- Init.Data.Option.Monadic
Option.forM_some : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] (f : α → m PUnit.{u_1 + 1}) (a : α), forM (some a) f = f a
-- Init.Data.String.Lemmas.Pattern.Find.String
_private.Init.Data.String.Lemmas.Pattern.Find.String.0.String.Slice.isInfix_toList_iff : ∀ {t s : String}, t.toList <:+: s.toList ↔ ∃ s₁ s₂, s = s₁ ++ t ++ s₂
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.symm_image_target_eq_source : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), ↑e.symm '' e.target = e.source
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.isClosed_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α},
  IsClosed s ↔ ∀ (a : α), (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_union_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ ↔ k ∈ t₁ ∨ k ∈ t₂
-- Std.Time.Format.Basic
Std.Time.GenericFormat.mk.injEq : ∀ {awareness : Std.Time.Awareness} (config : Std.Time.FormatConfig) (string : Std.Time.FormatString)
  (config_1 : Std.Time.FormatConfig) (string_1 : Std.Time.FormatString),
  ({ config := config, string := string } = { config := config_1, string := string_1 }) =
    (config = config_1 ∧ string = string_1)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mem_top : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (x : R), x ∈ ⊤
-- Std.Do.PredTrans
/-- The predicate transformer that asserts the first exception condition.
 -/
Std.Do.PredTrans.throw : {ps : Std.Do.PostShape} → {α ε : Type u} → ε → Std.Do.PredTrans (Std.Do.PostShape.except ε ps) α
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.Forall.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : α) (h_1 : Unit → motive []) (h_2 : (x : α) → motive [x])
  (h_3 : (x : α) → (l : List α) → motive (x :: l)),
  (match [x] with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: l => h_3 x l) =
    h_2 x
-- Mathlib.CategoryTheory.Square
CategoryTheory.Functor.mapSquare_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) (sq : CategoryTheory.Square C), F.mapSquare.obj sq = sq.map F
-- Lean.CoreM
/-- Execute `x`. If it throws an error, indent and prepend `msg` to it.   -/
Lean.Core.prependError : {m : Type → Type u_1} → {α : Type} → [MonadControlT Lean.CoreM m] → [Monad m] → Lean.MessageData → m α → m α
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function is monotonous.
 -/
ValueDistribution.logCounting_monotoneOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E} {e : WithTop E},
  MonotoneOn (ValueDistribution.logCounting f e) (Set.Ioi 0)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Multiset.count_sum' : ∀ {ι : Type u_1} {α : Type u_6} [inst : DecidableEq α] {s : Finset ι} {a : α} {f : ι → Multiset α},
  Multiset.count a (∑ x ∈ s, f x) = ∑ x ∈ s, Multiset.count a (f x)
-- Mathlib.Analysis.RCLike.Basic
RCLike.add_conj : ∀ {K : Type u_1} [inst : RCLike K] (z : K), z + (starRingEnd K) z = 2 * ↑(RCLike.re z)