mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.SupIndep
Finset.SupIndep.pairwiseDisjoint : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  s.SupIndep f → (↑s).PairwiseDisjoint f
-- Mathlib.Probability.Independence.Process.Basic
/-- Two stochastic processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ are independent if
for all $s_1, ..., s_p \in S$ and $t_1, ..., t_q \in T$ the two families
$(X_{s_1}, ..., X_{s_p})$ and $(Y_{t_1}, ..., Y_{t_q})$ are independent.

This version only requires a.e.-measurability.  -/
ProbabilityTheory.Kernel.IndepFun.process_indepFun_process₀ : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {T : Type u_5} {𝓧 : S → Type u_6} {𝓨 : T → Type u_7}
  [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : (j : T) → MeasurableSpace (𝓨 j)] {X : (i : S) → Ω → 𝓧 i}
  {Y : (j : T) → Ω → 𝓨 j},
  (∀ (i : S), AEMeasurable (X i) (P.bind ⇑κ)) →
    (∀ (j : T), AEMeasurable (Y j) (P.bind ⇑κ)) →
      (∀ (I : Finset S) (J : Finset T),
          ProbabilityTheory.Kernel.IndepFun (fun ω i => X (↑i) ω) (fun ω j => Y (↑j) ω) κ P) →
        ∀ [ProbabilityTheory.IsZeroOrMarkovKernel κ],
          ProbabilityTheory.Kernel.IndepFun (fun ω i => X i ω) (fun ω j => Y j ω) κ P
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.toTerminationMeasures : Array Lean.Elab.PreDefinition →
  Lean.Elab.FixedParamPerms →
    Array (Array Lean.Name) →
      Array (Array Lean.Elab.WF.GuessLex.BasicMeasure) →
        Array Lean.Elab.WF.GuessLex.MutualMeasure → Lean.MetaM Lean.Elab.TerminationMeasures
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.edges_eq_nil : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, p.edges = [] ↔ p.Nil
-- Lean.Meta.InferType
/-- Infer type of lambda and let expressions  -/
_private.Lean.Meta.InferType.0.Lean.Meta.inferLambdaType : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.Morita.Matrix
ModuleCat.toMatrixModCat_map : ∀ (R : Type u) (ι : Type v) [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] {X Y : ModuleCat R}
  (f : X ⟶ Y),
  (ModuleCat.toMatrixModCat R ι).map f = ModuleCat.ofHom (LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f))
-- Mathlib.Order.Birkhoff
OrderIso.supIrredLowerSet_symm_apply : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [inst_2 : Finite α] (s : { s // SupIrred s })
  [inst_3 : Fintype ↥↑s], OrderIso.supIrredLowerSet.symm s = (↑↑s).toFinset.sup id
-- Mathlib.CategoryTheory.Localization.FiniteProducts
CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] (J : Type)
  [inst_3 : CategoryTheory.Limits.HasProductsOfShape J C] [inst_4 : W.IsStableUnderProductsOfShape J]
  [inst_5 : W.ContainsIdentities] [inst_6 : Finite J] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C),
  (CategoryTheory.Localization.HasProductsOfShapeAux.adj L W J).counit.app (F.comp L) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.const (CategoryTheory.Discrete J)).map
        ((CategoryTheory.Localization.HasProductsOfShapeAux.compLimitFunctorIso L W J).hom.app F))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.compConstIso (CategoryTheory.Discrete J) L).hom.app (CategoryTheory.Limits.lim.obj F))
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.constLimAdj.counit.app F) L))
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If a power series converges at 1, it converges absolutely at all `z` of smaller norm.  -/
summable_powerSeries_of_norm_lt_one : ∀ {α : Type u_1} [inst : NormedDivisionRing α] [CompleteSpace α] {f : ℕ → α} {z : α},
  (CauchySeq fun n => ∑ i ∈ Finset.range n, f i) → ‖z‖ < 1 → Summable fun n => f n * z ^ n
-- Mathlib.Analysis.Normed.Lp.ProdLp
IsometryEquiv.withLpProdAssoc_symm_apply : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) (γ : Type u_4) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] [inst_2 : PseudoEMetricSpace γ] (x : WithLp p (α × WithLp p (β × γ))),
  (IsometryEquiv.withLpProdAssoc p α β γ).symm x = WithLp.toLp p (WithLp.toLp p (x.fst, x.snd.fst), x.snd.snd)
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Run `evalRecCall` and cache there result  -/
Lean.Elab.WF.GuessLex.RecCallCache.eval : Lean.Elab.WF.GuessLex.RecCallCache → ℕ → ℕ → Lean.MetaM Lean.Elab.WF.GuessLex.GuessLexRel
-- Mathlib.SetTheory.Ordinal.Basic
/-- An ordinal lifted to a lower or equal universe equals itself.

Unfortunately, the simp lemma doesn't work.  -/
Ordinal.lift_id' : ∀ (a : Ordinal.{max u_1 u_2}), Ordinal.lift.{u_1, max u_1 u_2} a = a
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- The map that sends `x : realSpace K` to
`Real.exp (x w₀) * ∏_{i ≠ w₀} |ηᵢ| ^ x i` where `|ηᵢ|` denote the vector of `realSpace K` given
by `w (ηᵢ)` and `ηᵢ` denote the units in `fundSystem K`, see `expMapBasis_apply'`.
 -/
NumberField.mixedEmbedding.fundamentalCone.expMapBasis : {K : Type u_1} →
  [inst : Field K] →
    [NumberField K] →
      OpenPartialHomeomorph (NumberField.mixedEmbedding.realSpace K) (NumberField.mixedEmbedding.realSpace K)
-- Lean.Util.PPExt
Lean.ppExprWithInfos : Lean.PPContext → Lean.Expr → BaseIO Lean.FormatWithInfos
-- Mathlib.Data.Set.Finite.Basic
Set.finite_range_findGreatest : ∀ {α : Type u} {P : α → ℕ → Prop} [inst : (x : α) → DecidablePred (P x)] {b : ℕ},
  (Set.range fun x => Nat.findGreatest (P x) b).Finite
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.mk.congr_simp : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (toLinearMap toLinearMap_1 : M →ₗ[R] N)
  (e_toLinearMap : toLinearMap = toLinearMap_1)
  (map_lie' : ∀ {x : L} {m : M}, toLinearMap.toFun ⁅x, m⁆ = ⁅x, toLinearMap.toFun m⁆),
  { toLinearMap := toLinearMap, map_lie' := map_lie' } = { toLinearMap := toLinearMap_1, map_lie' := ⋯ }
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.pre : Lean.Meta.Sym.Simp.Simproc
-- Mathlib.RingTheory.Derivation.MapCoeffs
Derivation.mapCoeffs_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (d : Derivation R A M) (p : Polynomial A)
  (i : ℕ), (d.mapCoeffs p).coeff i = d (p.coeff i)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- a natural transformation `ι.obj d ⊠ ι.obj d' ⟶ tensor C ⋙ ι.obj (d ⊗ d')`  -/
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit : (C : Type u₁) →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    (V : Type u₂) →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            {D : Type u₃} →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                {inst_5 : CategoryTheory.MonoidalCategoryStruct D} →
                  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] →
                    (d d' : D) →
                      CategoryTheory.MonoidalCategory.externalProduct
                          ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d)
                          ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj
                            d') ⟶
                        (CategoryTheory.MonoidalCategory.tensor C).comp
                          ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj d d'))
-- Mathlib.Order.Filter.Basic
/-- Galois insertion from sets of sets into filters.  -/
Filter.giGenerate : (α : Type u_2) → GaloisInsertion Filter.generate Filter.sets
-- Mathlib.RingTheory.Algebraic.Basic
Transcendental.aeval : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : A},
  Transcendental R r →
    ∀ (f : Polynomial R),
      f.natDegree ≠ 0 → f.leadingCoeff ∈ nonZeroDivisors R → Transcendental R ((Polynomial.aeval r) f)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Equiv.beq_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α] [inst_3 : (k : α) → BEq (β k)] {m₃ m₄ : Std.DHashMap.Internal.Raw₀ α β},
  (↑m₁).WF → (↑m₂).WF → (↑m₃).WF → (↑m₄).WF → (↑m₁).Equiv ↑m₃ → (↑m₂).Equiv ↑m₄ → m₁.beq m₂ = m₃.beq m₄
-- Mathlib.Data.List.Destutter
_private.Mathlib.Data.List.Destutter.0.List.destutter'.match_1.eq_2 : ∀ {α : Type u_1} (motive : α → List α → Sort u_2) (a h : α) (l : List α) (h_1 : (a : α) → motive a [])
  (h_2 : (a h : α) → (l : List α) → motive a (h :: l)),
  (match a, h :: l with
    | a, [] => h_1 a
    | a, h :: l => h_2 a h l) =
    h_2 a h l
-- Mathlib.Logic.Function.Basic
Function.Injective.of_comp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α},
  Function.Injective (f ∘ g) → Function.Injective g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {k : α}, (cmp t.maxKey! k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.prodMulEquiv.eq_1 : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (A : Subgroup G) (B : Subgroup H) [inst_2 : A.Normal]
  [inst_3 : B.Normal], QuotientGroup.prodMulEquiv A B = { toEquiv := QuotientGroup.prodEquiv A B, map_mul' := ⋯ }
-- Lean.Elab.Deriving.Basic
_private.Lean.Elab.Deriving.Basic.0.Lean.Elab.Term.mkInst.go : Lean.Name →
  Lean.Expr →
    Lean.Expr →
      Array Lean.Expr →
        Array Lean.BinderInfo →
          Lean.Expr →
            Lean.Name → Lean.Expr → Array Lean.MVarId → Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Term.MkInstResult✝
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_of_coprime : ∀ (n : ℕ), 1 < n → (∀ m < n, m ≠ 0 → n.Coprime m) → Nat.Prime n
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.ofFun_prod : ∀ {α : Type u_1} {ι : Type u_3} {β : Type u_4} [inst : CommMonoid β] {f : ι → α → β} (I : Finset ι),
  UniformFun.ofFun (∏ i ∈ I, f i) = ∏ i ∈ I, UniformFun.ofFun (f i)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- The ring morphism `A →+* A ⊗[R] B` sending `a` to `a ⊗ₜ 1`.  -/
GradedTensorProduct.includeLeftRingHom : {R : Type u_1} →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              [inst_9 : Module ι (Additive ℤˣ)] → A →+* GradedTensorProduct R 𝒜 ℬ
-- Mathlib.Data.Nat.Totient
Nat.prime_iff_card_units : ∀ (p : ℕ) [inst : Fintype (ZMod p)ˣ], Nat.Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
-- Mathlib.Analysis.InnerProductSpace.Adjoint
_private.Mathlib.Analysis.InnerProductSpace.Adjoint.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Analysis.Complex.Harmonic.Poisson
/-- **Poisson integral formula** for harmonic functions on arbitrary disks in the complex plane,
formulated with the Poisson kernel of integration.
 -/
InnerProductSpace.HarmonicContOnCl.circleAverage_poissonKernel_smul : ∀ {f : ℂ → ℝ} {c w : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicContOnCl f (Metric.ball c R) →
    w ∈ Metric.ball c R → Real.circleAverage (poissonKernel c w • f) c R = f w
-- Mathlib.RingTheory.MatrixAlgebra
MatrixEquivTensor.toFunBilinear_apply : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (a : A) (m : Matrix n n R), ((MatrixEquivTensor.toFunBilinear n R A) a) m = a • m.map ⇑(algebraMap R A)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.le_tan : ∀ {x : ℝ}, 0 ≤ x → x < Real.pi / 2 → x ≤ Real.tan x
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_iUnion_le_tsum : ∀ {α : Type u_1} {ι : Type u_4} (f : α → ENNReal) (t : ι → Set α),
  ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (i : ι) (x : ↑(t i)), f ↑x
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.toComp_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι) (i : ι),
  (Q.toComp P).val i = MvPolynomial.X (Sum.inr i)
-- Init.Data.Order.Ord
Std.ReflCmp.isLE_rfl : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.ReflCmp cmp] {a : α}, (cmp a a).isLE = true
-- Mathlib.Topology.Bases
/-- In a second-countable space, an open set, given as a union of open sets,
is equal to the union of countably many of those sets.
In particular, any open covering of `α` has a countable subcover: α is a Lindelöf space.  -/
TopologicalSpace.isOpen_iUnion_countable : ∀ {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {ι : Type u_1} (s : ι → Set α),
  (∀ (i : ι), IsOpen (s i)) → ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isClosedEmbedding_of_spaced_out : ∀ {β : Type v} [inst : UniformSpace β] {α : Type u_1} [inst_1 : TopologicalSpace α] [DiscreteTopology α] [T0Space β]
  {f : α → β} {s : Set (β × β)}, s ∈ uniformity β → (Pairwise fun x y => (f x, f y) ∉ s) → Topology.IsClosedEmbedding f
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.SpecTensorTo.eq_1 : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g),
  T.SpecTensorTo =
    CategoryTheory.Limits.pullback.lift
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInl) (X.fromSpecResidueField T.x))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInr) (Y.fromSpecResidueField T.y)) ⋯
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.instTopologicalSpace : {α : Type u_1} → [Preorder α] → TopologicalSpace (Topology.WithLower α)
-- Mathlib.Topology.Algebra.Ring.Basic
instContinuousMulAddOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst_1 : TopologicalSpace R] [ContinuousMul R],
  ContinuousMul Rᵃᵒᵖ
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.prod.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {H : Type u_2} [inst_2 : AddGroup H]
  [inst_3 : TopologicalSpace H] (U : OpenAddSubgroup G) (V : OpenAddSubgroup H),
  U.prod V = { toAddSubgroup := (↑U).prod ↑V, isOpen' := ⋯ }
-- Std.Time.Format.Modifier
Std.Time.OffsetX.hour.sizeOf_spec : sizeOf Std.Time.OffsetX.hour = 1
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.instPowNat : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubmonoidClass σ A] →
            {𝒜 : ι → σ} →
              (x : Submonoid A) →
                [inst_3 : AddCommMonoid ι] →
                  [inst_4 : DecidableEq ι] → [GradedRing 𝒜] → Pow (HomogeneousLocalization.NumDenSameDeg 𝒜 x) ℕ
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.op_le_op_iff : ∀ {G : Type u_2} [inst : Group G] {S₁ S₂ : Subgroup G}, S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W],
  ↑(WeierstrassCurve.valuation_Δ_aux R W) =
    (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor C (Type w)} {I : Type u₁}
  [inst_1 : CategoryTheory.Category.{v₁, u₁} I] [inst_2 : Small.{w, u₁} I] (F : CategoryTheory.Functor I A.Elements)
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I C] [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape I A],
  (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F).pt.fst =
    CategoryTheory.Limits.limit (F.comp (CategoryTheory.CategoryOfElements.π A))
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
SeparationQuotient.liftNormedAddGroupHomEquiv_symm_apply_coe : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (g : NormedAddGroupHom (SeparationQuotient M) N),
  ↑(SeparationQuotient.liftNormedAddGroupHomEquiv.symm g) = g.comp SeparationQuotient.normedMk
-- Init.Control.Except
observing : {ε α : Type u} → {m : Type u → Type v} → [Monad m] → [MonadExcept ε m] → m α → m (Except ε α)
-- Lean.Meta.MkIffOfInductiveProp
/-- Proves the left to right direction of a generated iff theorem.
`shape` is the output of a call to `constrToProp`.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.toCases : Lean.MVarId → List Lean.Meta.Shape✝ → Lean.MetaM Unit
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_filter_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    ∀ {h₁ : Std.Internal.List.containsKey k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = true}
      {h₂ : Std.Internal.List.containsKey k l₁ = true},
      Std.Internal.List.getEntry k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) h₁ =
        Std.Internal.List.getEntry k l₁ h₂
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.int_div_nonneg_of_pos_of_nonneg : ∀ {a b : ℤ}, 0 < a → 0 ≤ b → 0 ≤ a / b
-- Mathlib.Algebra.GroupWithZero.TransferInstance
/-- Transfer `CommMonoidWithZero` across an `Equiv`  -/
Equiv.commMonoidWithZero : {α : Type u} → {β : Type v} → α ≃ β → [CommMonoidWithZero β] → CommMonoidWithZero α
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_filter_eq_size_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool},
  (Std.HashSet.filter f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = true
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_splits_map_of_injective : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : IsDomain S]
  {i : R →+* S},
  Function.Injective ⇑i → (Polynomial.map i f).Splits → (∀ a ∈ (Polynomial.map i f).roots, a ∈ i.range) → f.Splits
-- Mathlib.Algebra.Group.Defs
CancelMonoid.toRightCancelMonoid : {M : Type u} → [self : CancelMonoid M] → RightCancelMonoid M
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LEquiv.onSentence_apply : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (φ : L ≃ᴸ L') (a : L.BoundedFormula Empty 0),
  φ.onSentence a = φ.toLHom.onBoundedFormula a
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.instLaxMonoidalDiscretePUnitCommMonToLaxBraidedObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (A : CategoryTheory.CommMon C) →
          (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj A).LaxMonoidal
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq.congr_simp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p q : ι}
  (h : p = q), K.XIsoOfEq h = K.XIsoOfEq h
-- Init.System.IO
/-- Opens the file `fn` with the specified `mode` and passes the resulting file handle to `f`.

The file handle is closed when the last reference to it is dropped. If references escape `f`, then
the file remains open even after `IO.FS.withFile` has finished.
 -/
IO.FS.withFile : {α : Type} → System.FilePath → IO.FS.Mode → (IO.FS.Handle → IO α) → IO α
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_insertMany_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {ρ : Type w}
  [inst : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {l : ρ} {k : α}, k ∈ m → k ∈ m.insertMany l
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.toEquiv_inj : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {e₁ e₂ : α ≃ᵢ β},
  e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂
-- Mathlib.Data.Int.ModEq
Int.left_modEq_add_iff : ∀ {n a b : ℤ}, a ≡ a + b [ZMOD n] ↔ n ∣ b
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.hasLimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  CategoryTheory.Limits.HasLimitsOfSize.{v, v, max u₁ v, max (max (max (v + 1) u) u₁) v₁} (PresheafOfModules R)
-- Mathlib.Algebra.Order.Group.Abs
div_lt_of_mabs_div_lt_right : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b c : G}, |a / b|ₘ < c → a / c < b
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.id.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (a : C),
  (CategoryTheory.WithInitial.of a).id = CategoryTheory.CategoryStruct.id a
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- Further truncation of truncated simplicial sets.  -/
SSet.Truncated.trunc : (n m : ℕ) →
  autoParam (m ≤ n) SSet.Truncated.trunc._auto_1 → CategoryTheory.Functor (SSet.Truncated n) (SSet.Truncated m)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.support_sup : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → LinearOrder (α i)]
  [∀ (i : ι), IsBotZeroClass (α i)] [inst_3 : DecidableEq ι] {f g : Π₀ (i : ι), α i},
  (f ⊔ g).support = f.support ∪ g.support
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo.declNameNonRec : Lean.Elab.WF.EqnInfo → Lean.Name
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.ofNat_ext : ∀ {α : Type u_1} (p : ℕ) [inst : Lean.Grind.Semiring α] [Lean.Grind.IsCharP α p] {x y : ℕ},
  x % p = y % p → OfNat.ofNat x = OfNat.ofNat y
-- Mathlib.GroupTheory.Submonoid.Center
AddSubsemigroup.centerToAddOpposite.eq_1 : ∀ {M : Type u_2} [inst : Add M],
  AddSubsemigroup.centerToAddOpposite =
    { toFun := fun r => ⟨AddOpposite.op ↑r, ⋯⟩, invFun := fun r => ⟨AddOpposite.unop ↑r, ⋯⟩, left_inv := ⋯,
      right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.notMem_of_dist_lt_infDist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x y : α}, dist x y < Metric.infDist x s → y ∉ s
-- Std.Data.TreeMap.Basic
/-- Compares two tree maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.TreeMap.beq : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [BEq β] → Std.TreeMap α β cmp → Std.TreeMap α β cmp → Bool