mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Radical.NatInt
Nat.radical_eq_prod_primeFactors : ∀ {n : ℕ}, UniqueFactorizationMonoid.radical n = ∏ p ∈ n.primeFactors, p
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isInf.sizeOf_spec : ∀ (lhs rhs res : ℕ),
  sizeOf (Mathlib.Tactic.Order.AtomicFact.isInf lhs rhs res) = 1 + sizeOf lhs + sizeOf rhs + sizeOf res
-- Mathlib.NumberTheory.Real.Irrational
Irrational.natCast_div : ∀ {x : ℝ}, Irrational x → ∀ {m : ℕ}, m ≠ 0 → Irrational (↑m / x)
-- Mathlib.Order.Monotone.Basic
StrictAnti.ite' : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β},
  StrictAnti f →
    StrictAnti g →
      ∀ {p : α → Prop} [inst_2 : DecidablePred p],
        (∀ ⦃x y : α⦄, x < y → p y → p x) →
          (∀ ⦃x y : α⦄, p x → ¬p y → x < y → g y < f x) → StrictAnti fun x => if p x then f x else g x
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
/-- This lemma characterizes the transition functions of an open subset in terms of the transition
functions of the original space.  -/
OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : TopologicalSpace.Opens X}
  (hs : Nonempty ↥s) (f f' : OpenPartialHomeomorph X Y),
  (f.subtypeRestr hs).symm.trans (f'.subtypeRestr hs) ≈ (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)
-- Lean.Elab.Tactic.Split
_private.Lean.Elab.Tactic.Split.0.Lean.Elab.Tactic.evalSplit.throwCouldNotSplitHyp : Lean.FVarId → Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.sizeUpTo_succ : ∀ {n : ℕ} (c : Composition n) {i : ℕ} (h : i < c.length), c.sizeUpTo (i + 1) = c.sizeUpTo i + c.blocks[i]
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_ofFinsupp : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (f : Γ →₀ R) (a : Γ),
  (HahnSeries.ofFinsupp f).coeff a = f a
-- Mathlib.GroupTheory.IsSubnormal
/-- A subgroup `H` of a group `G` satisfies `IsSubnormal` if
* either `H = ⊤`;
* or there is a subgroup `K` of `G` containing `H` and such that `H` is normal in `K` and
  `K` satisfies `IsSubnormal`.

Equivalently, `H.IsSubnormal` means that there is a chain of subgroups
`H₀ ≤ H₁ ≤ ... ≤ Hₙ` such that
* `H = H₀`,
* `G = Hₙ`,
* for each `i ∈ {0, ..., n - 1}`, `Hᵢ` is a normal subgroup of `Hᵢ₊₁`.

See `isSubnormal_iff` for this characterisation.
 -/
Subgroup.IsSubnormal : {G : Type u_1} → [inst : Group G] → Subgroup G → Prop
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableAt_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {x : M} {c : M'}, (MDiffAt fun x => c) x
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHomClass.instCoeTCNonUnitalStarAlgHomOfStarHomClass : {F : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : Monoid R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : DistribMulAction R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalNonAssocSemiring B] →
                  [inst_5 : DistribMulAction R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] →
                        [NonUnitalAlgHomClass F R A B] → [StarHomClass F A B] → CoeTC F (A →⋆ₙₐ[R] B)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find?_decide_eq_dite : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p],
  (Fin.find? fun x => decide (p x)) = if h : ∃ i, p i then some (Fin.find p h) else none
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The object in the category of topological representations associated to a type equipped with a
continuous representation. This is the preferred way to construct a term of `TopRep k G`.  -/
TopRep.of : {k : Type u} →
  {G : Type v} →
    {X : Type w} →
      [inst : TopologicalSpace k] →
        [inst_1 : Ring k] →
          [inst_2 : Monoid G] →
            [inst_3 : AddCommGroup X] →
              [inst_4 : Module k X] →
                [inst_5 : TopologicalSpace X] →
                  [inst_6 : IsTopologicalAddGroup X] → [ContinuousSMul k X] → ContRepresentation k G X → TopRep k G
-- Mathlib.AlgebraicGeometry.Sites.Proetale
/-- Big pro-étale site: the pro-étale topology on the category of schemes is
generated by the pro-étale precoverage.  -/
AlgebraicGeometry.Scheme.proetaleTopology : CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme
-- Mathlib.Order.SuccPred.Basic
WithBot.instSuccOrder.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α],
  WithBot.instSuccOrder =
    {
      succ := fun x =>
        match x with
        | none => ↑⊥
        | some a => ↑(Order.succ a),
      le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.two_le_iff' : ∀ {α : Type u} (x : α), 2 ≤ Cardinal.mk α ↔ ∃ y, y ≠ x
-- Mathlib.Data.PNat.Basic
PNat.natPred_strictMono : StrictMono PNat.natPred
-- Lean.Widget.InteractiveGoal
Lean.Widget.instRpcEncodableInteractiveHypothesisBundle : Lean.Server.RpcEncodable Lean.Widget.InteractiveHypothesisBundle
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.subtype.eq_1 : ∀ {M : Type u_1} {A : Type u_3} [inst : MulOneClass M] [inst_1 : SetLike A M] [hA : SubmonoidClass A M] (S' : A),
  SubmonoidClass.subtype S' = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Logic.Small.Defs
/-- A type is `Small.{w}` if there exists an equivalence to some `S : Type w`.
 -/
Small : Type v → Prop
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.Quotient.smul_coe : ∀ {G : Type u} {X : Type v} [inst : Group G] [inst_1 : Monoid X] [inst_2 : MulAction X G] (H : Subgroup G)
  [inst_3 : MulAction.QuotientAction X H] (b : X) (g : G), b • ↑g = ↑(b • g)
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- The vertices in a copy of `⊤` are a clique.  -/
SimpleGraph.isClique_range_copy_top : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} (f : ⊤.Copy G), G.IsClique (Set.range ⇑f)
-- Mathlib.GroupTheory.Perm.List
List.formPerm_apply_getElem_length : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α) (xs : List α), (x :: xs).formPerm (x :: xs)[xs.length] = x
-- Mathlib.Analysis.Normed.Module.Connected
Submodule.connectedComponentIn_eq_self_of_one_lt_codim : ∀ {F : Type u_1} [inst : AddCommGroup F] [inst_1 : Module ℝ F] [inst_2 : TopologicalSpace F] [IsTopologicalAddGroup F]
  [ContinuousSMul ℝ F] (E : Submodule ℝ F),
  1 < Module.rank ℝ (F ⧸ E) → ∀ {x : F}, x ∉ E → connectedComponentIn (↑E)ᶜ x = (↑E)ᶜ
-- Mathlib.Algebra.Order.IsBotOne
pos_of_gt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α] [inst_1 : Zero α] [IsBotZeroClass α], a < b → 0 < b
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.isDenseEmbedding : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : Fact (1 ≤ p)], p ≠ ⊤ → IsDenseEmbedding Subtype.val
-- Mathlib.Order.WellQuasiOrder
/-- A version of **Dickson's lemma**: the Pi type `∀ i : ι, α i` is well-quasi-ordered when `ι` is
finite and each `σ i` is well-quasi-ordered. See `Set.PartiallyWellOrderedOn.pi` for the finite
product of well-quasi-ordered sets and `Pi.wellQuasiOrderedLE` when the relation is `≤`.  -/
WellQuasiOrdered.pi : ∀ {ι : Type u_3} {α : ι → Type u_4} [Finite ι] {r : (i : ι) → α i → α i → Prop} [∀ (i : ι), IsPreorder (α i) (r i)],
  (∀ (i : ι), WellQuasiOrdered (r i)) → WellQuasiOrdered fun a b => ∀ (i : ι), r i (a i) (b i)
-- Mathlib.Order.CompleteLattice.Basic
Monotone.map_iInf₂_le : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α]
  [inst_1 : CompleteLattice β] {f : α → β},
  Monotone f → ∀ (s : (i : ι) → κ i → α), f (⨅ i, ⨅ j, s i j) ≤ ⨅ i, ⨅ j, f (s i j)
-- Mathlib.Analysis.Convex.Star
StarConvex.smul_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] {x : E} {s : Set E}, StarConvex 𝕜 0 s → x ∈ s → ∀ {t : 𝕜}, 0 ≤ t → t ≤ 1 → t • x ∈ s
-- Mathlib.RingTheory.LocalProperties.IntegrallyClosed
MaximalSpectrum.toPrimeSpectrum.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (x : MaximalSpectrum R),
  x.toPrimeSpectrum = { asIdeal := x.asIdeal, isPrime := ⋯ }
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.Option.elim.match_1.eq_1 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Option α → β → (α → β) → Sort u_2) (x : α) (x_1 : β) (f : α → β)
  (h_1 : (x : α) → (x_2 : β) → (f : α → β) → motive (some x) x_2 f) (h_2 : (y : β) → (x : α → β) → motive none y x),
  (match some x, x_1, f with
    | some x, x_2, f => h_1 x x_2 f
    | none, y, x => h_2 y x) =
    h_1 x x_1 f
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.RecArgCandidate.mk.injEq : ∀ (group : Lean.Elab.Structural.IndGroupInst) (comb : Array Lean.Elab.Structural.RecArgInfo)
  (group_1 : Lean.Elab.Structural.IndGroupInst) (comb_1 : Array Lean.Elab.Structural.RecArgInfo),
  ({ group := group, comb := comb } = { group := group_1, comb := comb_1 }) = (group = group_1 ∧ comb = comb_1)
-- Mathlib.Topology.NhdsWithin
mem_nhds_subtype_iff_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {a : ↑s} {t : Set ↑s},
  t ∈ nhds a ↔ Subtype.val '' t ∈ nhdsWithin (↑a) s
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- The 2-morphisms underlying the lax naturality constraint.  -/
CategoryTheory.Lax.LaxTrans.naturality : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          (self : CategoryTheory.Lax.LaxTrans F G) →
            {a b : B} →
              (f : a ⟶ b) →
                CategoryTheory.CategoryStruct.comp (self.app a) (G.map f) ⟶
                  CategoryTheory.CategoryStruct.comp (F.map f) (self.app b)
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.finite_comap_preimage_singleton : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.QuasiFinite R S] (P : PrimeSpectrum R), (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {P}).Finite
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.contMDiffAt : ∀ {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) [inst_5 : FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] {x : M},
  ContMDiffAt I (modelWithCornersSelf ℝ ℝ) (↑⊤) (↑f) x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_diff_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → (m₁.diff m₂).getKey! k = default
-- Init.Data.Ord.SInt
Int16.instTransOrd : Std.TransOrd Int16
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The center of a semiring acts commutatively on that semiring.  -/
Subring.center.smulCommClass_left : ∀ {R : Type u_3} [inst : Ring R], SMulCommClass (↥(Subring.center R)) R R
-- Mathlib.Algebra.GroupWithZero.Action.Defs
zero_smul : ∀ (M₀ : Type u_2) {A : Type u_7} [inst : Zero M₀] [inst_1 : Zero A] [inst_2 : SMulWithZero M₀ A] (m : A), 0 • m = 0
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder : Type
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.cylinder_zero : ∀ {E : ℕ → Type u_1} (x : (n : ℕ) → E n), PiNat.cylinder x 0 = Set.univ
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntFinCoOfNatIntCast.eq_1 : ∀ {n : ℕ}, Lean.Grind.instToIntFinCoOfNatIntCast = { toInt := fun x => ↑↑x, toInt_inj := ⋯, toInt_mem := ⋯ }
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.measurePreserving_prod_add_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [ν.IsAddRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1, z.2 + z.1)) (μ.prod ν) (μ.prod ν)
-- Mathlib.Algebra.CharP.Lemmas
neg_one_pow_char_pow : ∀ (R : Type u_1) [inst : Ring R] (p n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p], (-1) ^ p ^ n = -1
-- Mathlib.Data.Pi.Interval
Pi.instLocallyFiniteOrderBot : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [Fintype ι] →
      [DecidableEq ι] →
        [(i : ι) → DecidableEq (α i)] →
          [inst : (i : ι) → PartialOrder (α i)] →
            [(i : ι) → LocallyFiniteOrderBot (α i)] → LocallyFiniteOrderBot ((i : ι) → α i)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.isoOverPullback.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong g] {P : C} {fst : P ⟶ X} {snd snd_1 : P ⟶ Y} (e_snd : snd = snd_1)
  (h : CategoryTheory.IsPullback fst snd f g), h.isoOverPullback = ⋯.isoOverPullback
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.associated_num_den_inv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x : K),
  x ≠ 0 → Associated (IsFractionRing.num A x) ↑(IsFractionRing.den A x⁻¹)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_smul_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {A : Type u_8} [inst_1 : SMulZeroClass A R] (a : A)
  (x : AddMonoidAlgebra R M) (m : M), (a • x).coeff m = a • x.coeff m
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.map.eq_def : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (x : G.Walk u v),
  SimpleGraph.Walk.map f x =
    match v, x with
    | .(u), SimpleGraph.Walk.nil => SimpleGraph.Walk.nil
    | v, SimpleGraph.Walk.cons h p => SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map f p)
-- Mathlib.Data.Nat.MaxPowDiv
Nat.divMaxPow_base_pow : ∀ {p : ℕ}, p ≠ 0 → ∀ (k : ℕ), (p ^ k).divMaxPow p = 1
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftsToLimit.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cone (K.comp F)} {t : CategoryTheory.Limits.IsLimit c}
  (toLiftableCone : CategoryTheory.LiftableCone K F c)
  (makesLimit : CategoryTheory.Limits.IsLimit toLiftableCone.liftedCone)
  (toLiftableCone_1 : CategoryTheory.LiftableCone K F c)
  (makesLimit_1 : CategoryTheory.Limits.IsLimit toLiftableCone_1.liftedCone),
  ({ toLiftableCone := toLiftableCone, makesLimit := makesLimit } =
      { toLiftableCone := toLiftableCone_1, makesLimit := makesLimit_1 }) =
    (toLiftableCone = toLiftableCone_1 ∧ makesLimit ≍ makesLimit_1)
-- Mathlib.Analysis.MeanInequalities
NNReal.Lp_add_le_tsum' : ∀ {ι : Type u} {f g : ι → NNReal} {p : ℝ},
  1 ≤ p →
    (Summable fun i => f i ^ p) →
      (Summable fun i => g i ^ p) →
        (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.instMonoid : Monoid CircleDeg1Lift
-- Mathlib.Topology.Separation.Regular
/-- **Alias** of the reverse direction of `completelyNormalSpace_iff_forall_isOpen_normalSpace`.

---

A space is completely normal iff all open subspaces are normal.
 -/
CompletelyNormalSpace.of_forall_isOpen_normalSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X], (∀ (s : Set X), IsOpen s → NormalSpace ↑s) → CompletelyNormalSpace X
-- Mathlib.MeasureTheory.Group.LIntegral
/-- The Lebesgue integral of a function with respect to an inverse invariant measure is
invariant under the change of variables x ↦ x⁻¹.  -/
MeasureTheory.lintegral_inv_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : InvolutiveInv G] [MeasurableInv G]
  [μ.IsInvInvariant] (f : G → ENNReal), ∫⁻ (x : G), f x⁻¹ ∂μ = ∫⁻ (x : G), f x ∂μ
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ' : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] [inst_4 : ι.Additive] (X : A),
  CategoryTheory.Epi ((CategoryTheory.Abelian.LeftResolution.karoubi.π' Λ).app X)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.bientails.mpr : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, (P ⊣⊢ₛ Q) → Q ⊢ₛ P
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- An element `g` that becomes invertible in `S = R[X₁, ..., Xₙ] / I`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.g : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b → P.Ring
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The center of a semiring acts commutatively on any `R`-module  -/
Subring.instSMulCommClassSubtypeMemCenter_1 : ∀ {R : Type u_3} {M : Type u_4} [inst : Ring R] [inst_1 : MulAction R M], SMulCommClass (↥(Subring.center R)) R M
-- Mathlib.Algebra.Ring.Equiv
RingEquivClass.toMulEquivClass : ∀ {F : Type u_7} {R : Type u_8} {S : Type u_9} {inst : Mul R} {inst_1 : Add R} {inst_2 : Mul S} {inst_3 : Add S}
  {inst_4 : EquivLike F R S} [self : RingEquivClass F R S], MulEquivClass F R S
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_g : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₂.g = CategoryTheory.Limits.biprod.snd
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.strictMap_sup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) (P P' : CategoryTheory.MorphismProperty C),
  (P ⊔ P').strictMap F = P.strictMap F ⊔ P'.strictMap F
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- Since the norm of the entries of a Cauchy sequence is eventually stationary,
we can lift the norm to sequences.  -/
PadicSeq.norm : {p : ℕ} → [Fact (Nat.Prime p)] → PadicSeq p → ℚ
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_eq_iff_dist_coe_center_eq : ∀ {z w : UpperHalfPlane} {r : ℝ}, dist z w = r ↔ dist ↑z ↑(w.center r) = w.im * Real.sinh r
-- Std.Http.Data.URI.Basic
Std.Http.URI.instBEqQuery : BEq Std.Http.URI.Query
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_self_zpow_atTop_pow : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (x : G) (m : ℤ),
  MapClusterPt (x ^ m) Filter.atTop fun x_1 => x ^ x_1
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.instMonoidalOppositeInverseOpOpEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.opOpEquivalence C).inverse.Monoidal
-- Mathlib.Data.NNReal.Defs
NNReal.div_lt_one_of_lt : ∀ {a b : NNReal}, a < b → a / b < 1
-- Mathlib.Data.Finset.Max
Finset.max'_le : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty) (x : α), (∀ y ∈ s, y ≤ x) → s.max' H ≤ x
-- Mathlib.RingTheory.AdicCompletion.Completeness
AdicCompletion.ofPowSMul_injective : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ), Function.Injective ⇑(AdicCompletion.ofPowSMul I M n)
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.mk.sizeOf_spec : ∀ (var : ℕ) (irrelevant : List Lean.Elab.Tactic.Omega.Fact)
  (lowerBounds upperBounds : List (Lean.Elab.Tactic.Omega.Fact × ℤ)) (lowerExact upperExact : Bool),
  sizeOf
      { var := var, irrelevant := irrelevant, lowerBounds := lowerBounds, upperBounds := upperBounds,
        lowerExact := lowerExact, upperExact := upperExact } =
    1 + sizeOf var + sizeOf irrelevant + sizeOf lowerBounds + sizeOf upperBounds + sizeOf lowerExact + sizeOf upperExact
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB5OfSize.ofShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {inst_1 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w', v, u} C}
  [self : CategoryTheory.AB5OfSize.{w, w', v, u} C] (J : Type w') [inst_2 : CategoryTheory.Category.{w, w'} J]
  [inst_3 : CategoryTheory.IsFiltered J], CategoryTheory.HasExactColimitsOfShape J C
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorHom_def_assoc : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : C}
  (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y₁ g) h)
-- Mathlib.FieldTheory.AlgebraicClosure
Transcendental.algebraicClosure : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {a : E},
  Transcendental F a → Transcendental (↥(algebraicClosure F E)) a
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.coe_continuousMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : LocallyConstant X Y),
  ⇑↑f = ⇑f
-- Init.Data.SInt.Lemmas
Int16.toInt8_ofBitVec : ∀ (b : BitVec 16), (Int16.ofBitVec b).toInt8 = Int8.ofBitVec (BitVec.signExtend 8 b)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_diff_of_contains_eq_false_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β},
        m₂.contains k = false →
          Std.DHashMap.Internal.Raw₀.Const.getD (m₁.diff m₂) k fallback =
            Std.DHashMap.Internal.Raw₀.Const.getD m₁ k fallback
-- Std.Http.Internal.Char
/-- Checks if a byte is a valid path character (`pchar`) according to RFC 3986.
`pchar = unreserved / pct-encoded / sub-delims / ":" / "@"`

Note: The percent-encoding (`pct-encoded`) is handled separately by `isEncodedChar`,
so this predicate only covers the non-percent characters.
 -/
Std.Http.Internal.Char.isPChar : UInt8 → Bool
-- Init.Data.Array.Erase
Array.mem_of_mem_eraseP : ∀ {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α}, a ∈ xs.eraseP p → a ∈ xs
-- Mathlib.Order.WithBot
WithTop.ofDual_apply_coe : ∀ {α : Type u_1} (a : αᵒᵈ), WithTop.ofDual ↑a = ↑(OrderDual.ofDual a)
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.toZeroHom_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β],
  Function.Injective MonoidWithZeroHom.toZeroHom