mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Protocol.H1
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.hostAuthorityMatchesConnectAuthority : Std.Http.URI.Authority → Std.Http.Header.Host → Bool
-- Mathlib.Analysis.Calculus.SmoothSeries
deriv_tsum_apply : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [inst_4 : NormedSpace 𝕜 F] {g : α → 𝕜 → F} {y₀ : 𝕜},
  Summable u →
    (∀ (n : α), Differentiable 𝕜 (g n)) →
      (∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n) →
        (Summable fun n => g n y₀) → ∀ (y : 𝕜), deriv (fun z => ∑' (n : α), g n z) y = ∑' (n : α), deriv (g n) y
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instCommMonoidWithZeroValueGroupWithZero : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : ValuativeRel R] → CommMonoidWithZero (ValuativeRel.ValueGroupWithZero R)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.toList_insert_perm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp] {k : α} {v : β},
  (t.insert k v).toList.Perm ((k, v) :: List.filter (fun x => decide ¬(k == x.1) = true) t.toList)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Under.isoMk_hom_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : Q.RespectsIso] {A B : P.Under Q X} (f : A.right ≅ B.right)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp A.hom f.hom = B.hom)
      CategoryTheory.MorphismProperty.Under.isoMk._auto_1),
  (CategoryTheory.MorphismProperty.Under.isoMk f w).hom.right = f.hom
-- Mathlib.Algebra.Module.Card
/-- The cardinality of a nontrivial torsion-free module over a domain is at least the cardinality of
the ring.  -/
Cardinal.mk_le_of_module : ∀ (R : Type u) (E : Type v) [inst : AddCommGroup E] [inst_1 : Ring R] [IsDomain R] [inst_3 : Module R E] [Nontrivial E]
  [Module.IsTorsionFree R E], Cardinal.lift.{v, u} (Cardinal.mk R) ≤ Cardinal.lift.{u, v} (Cardinal.mk E)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.const_seq : ∀ {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} {c : ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.const (basis_hd :: basis_tl) c).seq =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const basis_hd basis_tl c
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R]
  {I J : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ},
  (ClassGroup.mk (FractionRing R)) I = (ClassGroup.mk (FractionRing R)) J ↔
    ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_image_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t : Set β}, (fun x => x.1 +ᵥ x.2) '' s ×ˢ t = s +ᵥ t
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residue_residueFieldCongr : ∀ (X : AlgebraicGeometry.Scheme) {x y : ↥X} (h : x = y),
  CategoryTheory.CategoryStruct.comp (X.residue x) (AlgebraicGeometry.Scheme.residueFieldCongr h).hom =
    CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom (X.residue y)
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.token.sizeOf_spec : ∀ (val : Lean.Parser.Token), sizeOf (Lean.Parser.ParserExtension.OLeanEntry.token val) = 1 + sizeOf val
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.Plus.quasiIso_iff : ∀ (A : Type u_3) [inst : CategoryTheory.Category.{v_3, u_3} A] [inst_1 : CategoryTheory.Abelian A]
  {K L : HomotopyCategory.Plus A} (f : K ⟶ L),
  HomotopyCategory.Plus.quasiIso A f ↔ HomotopyCategory.quasiIso A (ComplexShape.up ℤ) f.hom
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.extend_isColimit_desc_app_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A) (η : A ⟶ B) [inst_1 : CategoryTheory.IsIso η]
  (s : CategoryTheory.Limits.Cocone (P.F.comp CategoryTheory.yoneda)) (X : Cᵒᵖ) (a : (P.cocone.extend η).pt.obj X),
  (CategoryTheory.ConcreteCategory.hom (((P.extend η).isColimit.desc s).app X)) a =
    ((P.coconeIsColimit.desc s).app X).hom' ((CategoryTheory.inv (η.app X)).hom' a)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono φ h).φQ = CategoryTheory.CategoryStruct.id h.Q
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The intersection of the translates of a *finite* subset which contain a given point
is a block (Wielandt, th. 7.3).  -/
MulAction.IsBlock.of_subset : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] [MulAction.IsPretransitive G X] {B : Set X}
  (a : X), B.Finite → MulAction.IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.π_comp_colimitLeftOpIsoUnopLimit_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j).unop
      (CategoryTheory.Limits.colimitLeftOpIsoUnopLimit F).inv =
    CategoryTheory.Limits.colimit.ι F.leftOp (Opposite.op j)
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.exists_linearEquiv_dfinsupp : ∀ (R : Type u_2) [inst : Ring R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsSemisimpleModule R M], ∃ s x, sSupIndep s ∧ ∀ (m : ↑s), IsSimpleModule R ↥↑m
-- Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
/-- The ring isomorphism between a DVR `A` and the valuation subring of a field of fractions
of `A` endowed with the adic valuation of the maximal ideal.  -/
IsDiscreteValuationRing.equivValuationSubring : {A : Type u_1} →
  {K : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : IsDomain A] →
        [inst_2 : IsDiscreteValuationRing A] →
          [inst_3 : Field K] →
            [inst_4 : Algebra A K] →
              [inst_5 : IsFractionRing A K] →
                A ≃+*
                  ↥(IsDedekindDomain.HeightOneSpectrum.valuation K
                        (IsDiscreteValuationRing.maximalIdeal A)).valuationSubring
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.dist_lt_iff_of_nonempty_compact : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β} {C : ℝ} [Nonempty α] [CompactSpace α],
  dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C
-- Std.Http.Protocol.H1.Reader
/-- Parse the next chunk-size line in chunked transfer encoding.
 -/
Std.Http.Protocol.H1.Reader.BodyState.chunkedSize : Std.Http.Protocol.H1.Reader.BodyState
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.instIsLinearOrderQ : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : Std.IsLinearOrder α]
  [inst_3 : Lean.Grind.OrderedAdd α], Std.IsLinearOrder (Lean.Grind.IntModule.OfNatModule.Q α)
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomAddAct.instAddActionAEEqFun : {M : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : AddMonoid M] →
              [inst_3 : AddAction M α] →
                [MeasurableConstVAdd M α] → [MeasureTheory.VAddInvariantMeasure M α μ] → AddAction Mᵈᵃᵃ (α →ₘ[μ] β)
-- Mathlib.Algebra.Order.Antidiag.Finsupp
/-- The finset of functions `ι →₀ μ` with support contained in `s` and sum equal to `n`.  -/
Finset.finsuppAntidiag : {ι : Type u_1} →
  {μ : Type u_2} →
    [DecidableEq ι] →
      [inst : AddCommMonoid μ] → [Finset.HasAntidiagonal μ] → [DecidableEq μ] → Finset ι → μ → Finset (ι →₀ μ)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, `Hⁱ(G, A)` is isomorphic
to the homology of the short complex of `k`-modules `A --N--> A --(ρ(g) - 𝟙)--> A` when `i` is
odd.  -/
Rep.FiniteCyclicGroup.groupHomologyIsoOdd : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      [inst_2 : Fintype G] →
        (A : Rep.{u, u, u} k G) →
          (g : G) →
            [DecidableEq G] →
              (∀ (x : G), x ∈ Subgroup.zpowers g) →
                (i : ℕ) → Odd i → (groupHomology A i ≅ (Rep.FiniteCyclicGroup.normHomCompSub A g).homology)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.mul.inj : ∀ {J : Type v} {inst : CategoryTheory.SmallCategory J} {F : CategoryTheory.Functor J RingCat}
  {a a_1 a_2 a_3 : RingCat.Colimits.Prequotient F}, a.mul a_1 = a_2.mul a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orInR.injEq : ∀ (p p_1 : Mathlib.Tactic.ITauto.Proof), (p.orInR = p_1.orInR) = (p = p_1)
-- Mathlib.FieldTheory.IsPerfectClosure
IsPRadical.ker_le : ∀ {K : Type u_1} {L : Type u_2} [inst : CommSemiring K] [inst_1 : CommSemiring L] (i : K →+* L) (p : ℕ)
  [IsPRadical i p], RingHom.ker i ≤ pNilradical K p
-- Mathlib.CategoryTheory.Category.Pairwise
/-- Auxiliary definition for `cocone`.  -/
CategoryTheory.Pairwise.coconeιApp : {ι : Type v} →
  {α : Type u} →
    (U : ι → α) →
      [inst : CompleteLattice α] → (o : CategoryTheory.Pairwise ι) → CategoryTheory.Pairwise.diagramObj U o ⟶ iSup U
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- A variant of `app_inv_app` that gives an `eqToHom` instead of `homOfLe`.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y)
  (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) {Z : C}
  (h :
    Y.presheaf.obj
        (Opposite.op
          ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj
            ((TopologicalSpace.Opens.map f.base).obj U))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.base).obj U)) h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) h
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
RingHom.IsIntegralElem.mul : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {x y : S},
  f.IsIntegralElem x → f.IsIntegralElem y → f.IsIntegralElem (x * y)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.isMonHom_pullbackFst_id_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X R : C}
  {f : R ⟶ X} [inst_2 : CategoryTheory.MonObj (CategoryTheory.Over.mk f)],
  CategoryTheory.IsMonHom
    (CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.fst f (CategoryTheory.CategoryStruct.id X)) ⋯)
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.instHasLimitDiscreteWalkingPairCompPairEval : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.pair K L).comp (HomologicalComplex.eval C c i))
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.ISize.toBitVec_ite : ∀ {c : Prop} {t e : ISize} [inst : Decidable c], (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
-- Mathlib.FieldTheory.RatFunc.Basic
/-- [Stacks Tag 09FK](https://stacks.math.columbia.edu/tag/09FK) -/
RatFunc.instField : (K : Type u) → [inst : CommRing K] → [IsDomain K] → Field (RatFunc K)
-- Init.Data.Fin.Lemmas
Fin.forall_fin_two : ∀ {p : Fin 2 → Prop}, (∀ (i : Fin 2), p i) ↔ p 0 ∧ p 1
-- Init.PropLemmas
Decidable.or_iff_not_imp_left : ∀ {a b : Prop} [Decidable a], a ∨ b ↔ ¬a → b
-- Mathlib.Order.KrullDimension
Order.height_of_noMinOrder : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α] (a : α), Order.height a = ⊤
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.le_coeffsIn_pow : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {M : Submodule R S} {n : ℕ}, MvPolynomial.coeffsIn σ M ^ n ≤ MvPolynomial.coeffsIn σ (M ^ n)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits of shape `Jᵒᵖ`, then `F.unop : C ⥤ D` reflects colimits
of shape `J`.  -/
CategoryTheory.Limits.reflectsColimitsOfShape_unop : ∀ {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] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)
  [CategoryTheory.Limits.ReflectsLimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.ReflectsColimitsOfShape J F.unop
-- Std.Async.Signal
Std.Async.Signal.sigsys.sizeOf_spec : sizeOf Std.Async.Signal.sigsys = 1
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrix_nondegenerate : ∀ {ι : 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] [CharZero R] [IsDomain R] [inst_7 : Finite ι]
  {P : RootPairing ι R M N} [P.IsRootSystem] [inst_9 : P.IsCrystallographic] (b : P.Base), b.cartanMatrix.Nondegenerate
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- A short complex `S` has right homology when there exists a `S.RightHomologyData`  -/
CategoryTheory.ShortComplex.HasRightHomology : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → Prop
-- Mathlib.Algebra.Order.Hom.Basic
/-- `NonnegHomClass F α β` states that `F` is a type of nonnegative morphisms.  -/
NonnegHomClass : (F : Type u_7) → (α : outParam (Type u_8)) → (β : outParam (Type u_9)) → [Zero β] → [LE β] → [FunLike F α β] → Prop
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.le_comap_mk' : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [inst_1 : N.Normal] (H : Subgroup (G ⧸ N)),
  N ≤ Subgroup.comap (QuotientGroup.mk' N) H
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.FunctorExtension₁.obj_obj_p : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D))
  (P : CategoryTheory.Idempotents.Karoubi C),
  ((CategoryTheory.Idempotents.FunctorExtension₁.obj F).obj P).p = (F.map P.p).f
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.FiniteMeasure.map_snd_prod : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β), (μ.prod ν).map Prod.snd = μ Set.univ • ν
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.mul_coeff_one : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p * q).coeff 1 = p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.prodMk_left : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (a : α),
  LipschitzWith 1 (Prod.mk a)
-- Mathlib.RingTheory.OreLocalization.Ring
/-- The universal lift from a ring homomorphism `f : R →+* T`, which maps elements in `S` to
units of `T`, to a ring homomorphism `R[S⁻¹] →+* T`. This extends the construction on
monoids.  -/
OreLocalization.universalHom : {R : Type u_1} →
  [inst : Semiring R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {T : Type u_3} →
          [inst_2 : Semiring T] →
            (f : R →+* T) → (fS : ↥S →* Tˣ) → (∀ (s : ↥S), f ↑s = ↑(fS s)) → OreLocalization S R →+* T
-- Init.Data.Vector.Attach
Vector.getElem_unattach : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector { x // p x } n} (i : ℕ) (h : i < n), xs.unattach[i] = ↑xs[i]
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Bool} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.filter f m).get? k = Option.filter (f k) (m.get? k)
-- Mathlib.SetTheory.Cardinal.Regular
/-- A singular cardinal is infinite.  -/
Cardinal.IsSingular.aleph0_le : ∀ {c : Cardinal.{u_1}}, c.IsSingular → Cardinal.aleph0 ≤ c
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.false_or : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, ⌜False⌝ ∨ P ⊣⊢ₛ P
-- Init.Data.BitVec.Lemmas
BitVec.toInt_pos_iff : ∀ {w : ℕ} {x : BitVec w}, 0 ≤ x.toInt ↔ 2 * x.toNat < 2 ^ w
-- Mathlib.Algebra.Order.Hom.Monoid
/-- `α ≃+o β` is the type of isomorphisms `α ≃ β` that preserve the ordered additive monoid
structure.

`OrderAddMonoidIso` is also used for ordered group isomorphisms.

When possible, instead of parametrizing results over `(f : α ≃+o β)`,
you should parametrize over
`(F : Type*) [FunLike F M N] [AddEquivClass F M N] [OrderIsoClass F M N] (f : F)`.  -/
OrderAddMonoidIso : (α : Type u_6) → (β : Type u_7) → [Preorder α] → [Preorder β] → [Add α] → [Add β] → Type (max u_6 u_7)
-- Mathlib.Order.Fin.InsertNth
Fin.strictMono_insertNth : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α},
  StrictMono f → ∀ (i : Fin n) (x : α), f i.castSucc < x → x < f i.succ → StrictMono (i.castSucc.succ.insertNth x f)
-- Mathlib.RingTheory.Ideal.NatInt
Ideal.isPrime_int_iff : ∀ {P : Ideal ℤ}, P.IsPrime ↔ P = ⊥ ∨ ∃ p, Nat.Prime p ∧ P = Ideal.span {↑p}
-- Batteries.Data.List.Basic
List.sections.eq_def : ∀ {α : Type u_1} (x : List (List α)),
  x.sections =
    match x with
    | [] => [[]]
    | l :: L => List.flatMap (fun s => List.map (fun a => a :: s) l) L.sections
-- Mathlib.Topology.MetricSpace.Polish
/-- Given a closed embedding into a Polish space, the source space is also Polish.  -/
Topology.IsClosedEmbedding.polishSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [PolishSpace β] {f : α → β},
  Topology.IsClosedEmbedding f → PolishSpace α
-- Mathlib.Algebra.Polynomial.Lifts
/-- A polynomial that lifts can be lifted to a polynomial of the same support.  -/
Polynomial.exists_support_eq_of_mem_lifts : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial S},
  p ∈ Polynomial.lifts f → ∃ q, Polynomial.map f q = p ∧ q.support = p.support
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.congr_of_mem : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → (∀ x ∈ s, f₁ x = f x) → x ∈ s → HasDerivWithinAt f₁ f' s x
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.Limits.coneOfSectionCompYoneda_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections),
  (CategoryTheory.Limits.coneOfSectionCompYoneda F X s).pt = Opposite.op X
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.repr_range : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (hv : LinearIndependent R v), hv.repr.range = ⊤
-- Mathlib.Order.SupClosed
infClosure_prod : ∀ {α : Type u_3} {β : Type u_4} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] (s : Set α) (t : Set β),
  infClosure (s ×ˢ t) = infClosure s ×ˢ infClosure t
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aevalTower_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S : Type u_2} {A : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring A] [inst_3 : Algebra S R] [inst_4 : Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R),
  (MvPolynomial.aevalTower g y) (MvPolynomial.C x) = g x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C),
  (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.functor.obj F).X =
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
-- Init.Data.Vector.Lemmas
Vector.eq_push_append_of_mem : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x : α},
  x ∈ xs → ∃ n₁ n₂ as bs, ∃ (h : n₁ + 1 + n₂ = n), xs = Vector.cast h (as.push x ++ bs) ∧ x ∉ as
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- A variant of `limitIsoFlipCompLim` where the arguments of `F` are flipped.  -/
CategoryTheory.Limits.limitFlipIsoCompLim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] →
              (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) →
                CategoryTheory.Limits.limit F.flip ≅ F.comp CategoryTheory.Limits.lim
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.Isocrystal.mk : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {k : Type u_1} →
      [inst_1 : CommRing k] →
        [inst_2 : CharP k p] →
          [inst_3 : PerfectRing k p] →
            {V : Type u_2} →
              [inst_4 : AddCommGroup V] →
                [toModule : Module (FractionRing (WittVector p k)) V] →
                  (V ≃ₛₗ[WittVector.FractionRing.frobeniusRingHom p k] V) → WittVector.Isocrystal p k V
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Endomorphisms of a free module of rank one are homotheties.  -/
LinearEquiv.smul_id_of_finrank_eq_one : {R : Type u_2} →
  [inst : CommSemiring R] →
    [StrongRankCondition R] →
      {M : Type u_3} →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : Module R M] → [Module.Free R M] → Module.finrank R M = 1 → R ≃ₗ[R] M →ₗ[R] M
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
CategoryTheory.instPreservesLimitsOfShapeHomologicalComplexMapHomologicalComplexOfHasLimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [inst_4 : F.PreservesZeroMorphisms]
  {J : Type u_4} [inst_5 : CategoryTheory.Category.{v_3, u_4} J] [CategoryTheory.Limits.HasLimitsOfShape J C]
  [CategoryTheory.Limits.PreservesLimitsOfShape J F],
  CategoryTheory.Limits.PreservesLimitsOfShape J (F.mapHomologicalComplex c)
-- Mathlib.SetTheory.Cardinal.Pigeonhole
/-- A weaker version of `exists_infinite_fiber` that requires codomain to be infinite.  -/
Cardinal.exists_infinite_fiber' : ∀ {β α : Type u} (f : β → α), Cardinal.mk α < Cardinal.mk β → ∀ [Infinite α], ∃ a, Infinite ↑(f ⁻¹' {a})
-- Init.Data.Nat.Gcd
Nat.gcd_mul_right_sub_left : ∀ {m n k : ℕ}, n ≤ k * m → (k * m - n).gcd m = n.gcd m