mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.eraseKey.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (x : List ((a : α) × β a)),
  Std.Internal.List.eraseKey k x =
    match x with
    | [] => []
    | ⟨k', v'⟩ :: l => bif k' == k then l else ⟨k', v'⟩ :: Std.Internal.List.eraseKey k l
-- Std.Async.System
/-- Time spent in user mode.
 -/
Std.Async.System.CPUTimes.userTime : Std.Async.System.CPUTimes → Std.Time.Millisecond.Offset
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (A B : Subalgebra R S),
  A.LinearDisjoint B = (Subalgebra.toSubmodule A).LinearDisjoint (Subalgebra.toSubmodule B)
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
/-- The homeomorphism between the topological realization of a standard simplex
in `SSet` and the corresponding topological standard simplex.  -/
SimplexCategory.toTopHomeo : (n : SimplexCategory) → ↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) ≃ₜ ↑(stdSimplex ℝ (Fin (n.len + 1)))
-- Mathlib.Algebra.Homology.LocalCohomology
/-- Local cohomology (defined in terms of powers of `J`) agrees with local
cohomology computed over all ideals with radical containing `J`.  -/
localCohomology.isoSelfLERadical : {R : Type u} →
  [inst : CommRing R] →
    (J : Ideal R) → [IsNoetherian R R] → (i : ℕ) → localCohomology.ofSelfLERadical J i ≅ localCohomology J i
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.gc : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A],
  GaloisConnection (StarAlgebra.adjoin R) SetLike.coe
-- Mathlib.AlgebraicGeometry.Scheme
/-- A variant of `mem_basicOpen` without the `x ∈ U` assumption.  -/
AlgebraicGeometry.Scheme.mem_basicOpen'' : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↥X),
  x ∈ X.basicOpen f ↔ ∃ (m : x ∈ U), IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x m)) f)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul.go : ℕ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.wOppSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SOppSide x y → s.WOppSide x y
-- Mathlib.CategoryTheory.Limits.Cones
/-- `functoriality F _ ⋙ precompose (whiskerLeft F _)` simplifies to `functoriality F _`.  -/
CategoryTheory.Functor.functorialityCompPrecompose : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {F : CategoryTheory.Functor J C} →
              {H H' : CategoryTheory.Functor C D} →
                (α : H ≅ H') →
                  (CategoryTheory.Limits.Cocone.functoriality F H).comp
                      (CategoryTheory.Limits.Cocone.precompose (F.whiskerLeft α.inv)) ≅
                    CategoryTheory.Limits.Cocone.functoriality F H'
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.mk'.injEq : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (toIntertwiningMap : ρ.IntertwiningMap σ) (invFun : W → V)
  (left_inv : autoParam (Function.LeftInverse invFun toIntertwiningMap.toFun) Equiv.left_inv._autoParam)
  (right_inv : autoParam (Function.RightInverse invFun toIntertwiningMap.toFun) Equiv.right_inv._autoParam)
  (toIntertwiningMap_1 : ρ.IntertwiningMap σ) (invFun_1 : W → V)
  (left_inv_1 : autoParam (Function.LeftInverse invFun_1 toIntertwiningMap_1.toFun) Equiv.left_inv._autoParam)
  (right_inv_1 : autoParam (Function.RightInverse invFun_1 toIntertwiningMap_1.toFun) Equiv.right_inv._autoParam),
  ({ toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1,
        right_inv := right_inv_1 }) =
    (toIntertwiningMap = toIntertwiningMap_1 ∧ invFun = invFun_1)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Stmt.write.inj : ∀ {Γ : Type u_1} {a a_1 : Γ}, Turing.TM0.Stmt.write a = Turing.TM0.Stmt.write a_1 → a = a_1
-- Init.Data.String.Lemmas.Order
String.Pos.slice_lt_slice_iff : ∀ {s : String} {p₀ p₁ q r : s.Pos} {h₁ : p₀ ≤ q} {h₁' : p₀ ≤ r} {h₂ : q ≤ p₁} {h₂' : r ≤ p₁},
  q.slice p₀ p₁ h₁ h₂ < r.slice p₀ p₁ h₁' h₂' ↔ q < r
-- Mathlib.Logic.Basic
exists_exists_exists_and_eq : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β → γ} {p : γ → Prop},
  (∃ c, (∃ a b, f a b = c) ∧ p c) ↔ ∃ a b, p (f a b)
-- Mathlib.CategoryTheory.Limits.FullSubcategory
/-- If `P` is closed under colimits of shape `J`, then the inclusion creates such colimits.  -/
CategoryTheory.Limits.createsColimitFullSubcategoryInclusionOfClosed : (J : Type w) →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (P : CategoryTheory.ObjectProperty C) →
          [P.IsClosedUnderColimitsOfShape J] →
            (F : CategoryTheory.Functor J P.FullSubcategory) →
              [CategoryTheory.Limits.HasColimit (F.comp P.ι)] → CategoryTheory.CreatesColimit F P.ι
-- Batteries.Data.Fin.Lemmas
Fin.bind_find?_isSome : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, (Fin.find? fun i => (f i).isSome).bind f = Fin.findSome? f
-- Mathlib.Algebra.Category.Grp.Basic
AddEquiv.toAddCommGrpIso_hom : ∀ {X Y : AddCommGrpCat} (e : ↑X ≃+ ↑Y), e.toAddCommGrpIso.hom = AddCommGrpCat.ofHom e.toAddMonoidHom
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.isTheta : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → u =Θ[l] v
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgEquiv.toCoalgIso_refl : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  [inst_3 : Coalgebra R X], (CoalgEquiv.refl R X).toCoalgIso = CategoryTheory.Iso.refl (CoalgCat.of R X)
-- Mathlib.Topology.Connected.Basic
isPreconnected_iUnion : ∀ {α : Type u} [inst : TopologicalSpace α] {ι : Sort u_3} {s : ι → Set α},
  (⋂ i, s i).Nonempty → (∀ (i : ι), IsPreconnected (s i)) → IsPreconnected (⋃ i, s i)
-- Init.Data.Array.Count
Array.count_append : ∀ {α : Type u_1} [inst : BEq α] {a : α} {xs ys : Array α},
  Array.count a (xs ++ ys) = Array.count a xs + Array.count a ys
-- Mathlib.RingTheory.LocalRing.Module
IsLocalRing.map_tensorProduct_mk_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] {N : Submodule R M} [Module.Finite R M],
  Submodule.map ((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) N = ⊤ ↔ N = ⊤
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.liftH_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k : A ⟶ h.Q)
  (hk : CategoryTheory.CategoryStruct.comp k h.g' = 0) {Z : C} (h_1 : h.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (h.liftH k hk) (CategoryTheory.CategoryStruct.comp h.ι h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.RingTheory.RingHom.OpenImmersion
RingHom.IsStandardOpenImmersion.toAlgebra : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.IsStandardOpenImmersion → Algebra.IsStandardOpenImmersion R S
-- Mathlib.Algebra.Group.Defs
/-- Auxiliary tail-recursive implementation for `npowBinRec`.  -/
npowBinRec.go : {M : Type u_2} → [Mul M] → ℕ → M → M → M
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_inter_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k fallback : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.inter m₂ ⋯).getKeyD k fallback = fallback
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.norm : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β}, MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.HasFiniteIntegral (fun a => ‖f a‖) μ
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.map_map : ∀ {ι : Type u_1} {inst : Preorder ι} {F : ι → Type u_4} {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} [self : InverseSystem f]
  ⦃k j i : ι⦄ (hkj : k ≤ j) (hji : j ≤ i) (x : F i), f hkj (f hji x) = f ⋯ x
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.δ₀_spineToSimplex : ∀ {X : SSet} (h : (n : ℕ) → X.StrictSegalCore n) {n : ℕ} (p : X.Path (n + 1)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0))
      (SSet.StrictSegalCore.spineToSimplex h p) =
    SSet.StrictSegalCore.spineToSimplex h (p.interval 1 n ⋯)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.inverse_counitInv_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (Y : D) {Z : C} (h : e.inverse.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counitInv.app Y))
      (CategoryTheory.CategoryStruct.comp (e.unitInv.app (e.inverse.obj Y)) h) =
    h
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The `f` in the Weierstrass preparation theorem.  -/
PowerSeries.weierstrassDistinguished : {A : Type u_1} →
  [inst : CommRing A] →
    [inst_1 : IsLocalRing A] →
      [IsAdicComplete (IsLocalRing.maximalIdeal A) A] →
        (g : PowerSeries A) → (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 → Polynomial A
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.plusPlusSheaf_preservesZeroMorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [inst_3 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms] [inst_8 : CategoryTheory.Preadditive D],
  (CategoryTheory.plusPlusSheaf J D).PreservesZeroMorphisms
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.block_stabilizerOrderIso.eq_1 : ∀ (G : Type u_1) [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] [htGX : MulAction.IsPretransitive G X]
  (a : X),
  MulAction.block_stabilizerOrderIso G a =
    {
      toFun := fun x =>
        match x with
        | ⟨B, ⋯⟩ => ⟨MulAction.stabilizer G B, ⋯⟩,
      invFun := fun x =>
        match x with
        | ⟨H, hH⟩ => ⟨MulAction.orbit (↥H) a, ⋯⟩,
      left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mul_add_inv_left : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {P : Type u_3} [inst_1 : CommSemiring P] {g : R →+* P}
  (h : ∀ (y : ↥M), IsUnit (g ↑y)) (y : ↥M) (w z₁ z₂ : P),
  w * ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ + z₁ = z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂
-- Mathlib.SetTheory.ZFC.Rank
/-- The ordinal rank of a pre-set  -/
PSet.rank : PSet.{u} → Ordinal.{u}
-- Mathlib.LinearAlgebra.LinearPMap
Submodule.mem_graph_toLinearPMap : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {g : Submodule R (E × F)},
  (∀ x ∈ g, x.1 = 0 → x.2 = 0) → ∀ (x : ↥(Submodule.map (LinearMap.fst R E F) g)), (↑x, ↑g.toLinearPMap x) ∈ g
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C n}
  (app app_1 : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i) (e_app : app = app_1)
  (w :
    ∀ (i : ℕ) (hi : i < n),
      CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩) =
        CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩) (G.map' i (i + 1) ⋯ hi)),
  CategoryTheory.ComposableArrows.homMk app w = CategoryTheory.ComposableArrows.homMk app_1 ⋯
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- If `2` is invertible in `R`, then it is also invertible in `End R M`.  -/
QuadraticMap.instInvertibleEndOfNat : {R : Type u_3} →
  {M : Type u_4} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [Invertible 2] → Invertible 2
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_X_empty : ∀ {R : Type u_1} [inst : Semiring R], 1 = 0 → SkewPolynomial.X.support = ∅
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.stdBasis.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.stdBasis K = NumberField.mixedEmbedding.stdBasis K
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.spanNorm_mul_spanNorm_le : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] (I J : Ideal S),
  Ideal.spanNorm R I * Ideal.spanNorm R J ≤ Ideal.spanNorm R (I * J)
-- Lean.DocString.Types
Lean.Doc.instOrdDescItem : {α : Type u_1} → {β : Type u_2} → [Ord α] → [Ord β] → Ord (Lean.Doc.DescItem α β)
-- Std.Data.HashMap.Lemmas
Std.HashMap.equiv_iff_toList_perm : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ ↔ m₁.toList.Perm m₂.toList
-- Mathlib.Analysis.Normed.Group.Int
Int.norm_natCast : ∀ (n : ℕ), ‖↑n‖ = ↑n
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (l : List α), (t₁.insertMany l).Equiv (t₂.insertMany l)
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- The q-expansion of a pointwise product of two modular-form-class objects is the product of
their q-expansions. Works for any `ModularFormClass` (e.g. a `CuspForm` times a `ModularForm`).  -/
ModularForm.qExpansion_mul_coe : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2}
  [inst_1 : FunLike G UpperHalfPlane ℂ],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b],
        UpperHalfPlane.qExpansion h (⇑f * ⇑g) = UpperHalfPlane.qExpansion h ⇑f * UpperHalfPlane.qExpansion h ⇑g
-- Lean.Attributes
Lean.instInhabitedParametricAttribute.default : {α : Type} → Lean.ParametricAttribute α
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.from_middle_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  {S : J.Cover X} {T : (I : S.Arrow) → J.Cover I.Y} (I : (S.bind T).Arrow), (↑S).arrows I.fromMiddleHom
-- Mathlib.Topology.Algebra.Ring.Ideal
topologicalRing_quotient : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] (N : Ideal R) [IsTopologicalRing R],
  IsTopologicalRing (R ⧸ N)
-- Mathlib.Analysis.Normed.Group.AddTorsor
NormedAddTorsor.dist_eq_norm' : ∀ {V : outParam (Type u_1)} {P : Type u_2} {inst : SeminormedAddCommGroup V} {inst_1 : PseudoMetricSpace P}
  [self : NormedAddTorsor V P] (x y : P), dist x y = ‖x -ᵥ y‖
-- Mathlib.Data.NNReal.Defs
Set.OrdConnected.image_coe_nnreal_real : ∀ {t : Set NNReal}, t.OrdConnected → (NNReal.toReal '' t).OrdConnected
-- Init.Meta.Defs
/-- Syntax that represents an element of a `do` sequence.
 -/
Lean.Syntax.DoElem : Type
-- Mathlib.Order.Monotone.Basic
antitone_add_nat_iff_antitoneOn_nat_Ici : ∀ {α : Type u} [inst : Preorder α] {f : ℕ → α} {k : ℕ}, (Antitone fun n => f (n + k)) ↔ AntitoneOn f {x | k ≤ x}
-- Lean.Environment
_private.Lean.Environment.0.Lean.instNonemptyVisibilityMap : ∀ {α : Type} [Nonempty α], Nonempty (Lean.VisibilityMap✝ α)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Hom.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Lax.LaxTrans.Hom η θ}, x.as = y.as → x = y
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.1}
  {c₂ : CategoryTheory.Limits.Cofan F.obj} (s t : c₁.pt ⟶ c₂.pt)
  (hs :
    ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
      CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) s =
        CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.ι.app { as := f.fst.2 }))
  (ht :
    ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
      CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 })
  (i : CategoryTheory.Limits.Cofork s t),
  (CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit s t hs ht i).pt = i.pt
-- Mathlib.Topology.FiberBundle.Trivialization
/-- For fixed `v ∈ F`, `x ↦ e.symm (x,v)` is continuous on `e.baseSet`.  -/
Bundle.Trivialization.continuousOn_symm_prodMk_left : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {v : F},
  ContinuousOn (fun x => ↑e.symm (x, v)) e.baseSet
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.leftHomologyData_H : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k)
  (hk' : c'.next j' = k') (h : (K.sc' i j k).LeftHomologyData),
  (HomologicalComplex.extend.leftHomologyData K e hj' hi hi' hk hk' h).H = h.H
-- Mathlib.MeasureTheory.Measure.WithDensity
/-- If `μ` is an `s`-finite measure, then so is `μ.withDensity f`.  -/
MeasureTheory.Measure.withDensity.instSFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {f : α → ENNReal},
  MeasureTheory.SFinite (μ.withDensity f)
-- Mathlib.Topology.CompactOpen
ContinuousMap.toEquiv_homeoFnOfDiscrete : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : DiscreteTopology X],
  ContinuousMap.homeoFnOfDiscrete.toEquiv = ContinuousMap.equivFnOfDiscrete
-- Mathlib.Algebra.Order.Ring.Basic
Even.add_pow_le : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a b : R} {n : ℕ}
  [ExistsAddOfLE R], Even n → (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)
-- Init.Data.BitVec.Lemmas
BitVec.cons_and_cons : ∀ {w : ℕ} (x y : BitVec w) (a b : Bool), BitVec.cons a x &&& BitVec.cons b y = BitVec.cons (a && b) (x &&& y)
-- Mathlib.Algebra.Ring.Action.Submonoid
FixedPoints.addSubgroup_toAddSubmonoid : ∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : AddGroup α] [inst_2 : DistribMulAction M α],
  (FixedPoints.addSubgroup M α).toAddSubmonoid = FixedPoints.addSubmonoid M α
-- Init.Prelude
/-- The constant function that ignores its argument.

If `a : α`, then `Function.const β a : β → α` is the “constant function with value `a`”. For all
arguments `b : β`, `Function.const β a b = a`. It is often written directly as `fun _ => a`.

Examples:
 * `Function.const Bool 10 true = 10`
 * `Function.const Bool 10 false = 10`
 * `Function.const String 10 "any string" = 10`
 -/
Function.const : {α : Sort u} → (β : Sort v) → α → β → α
-- Mathlib.Algebra.Group.Hom.Defs
/-- The proposition that the function preserves 1  -/
OneHom.map_one' : ∀ {M : Type u_10} {N : Type u_11} [inst : One M] [inst_1 : One N] (self : OneHom M N), self.toFun 1 = 1
-- Mathlib.Topology.EMetricSpace.Lipschitz
locallyLipschitzOn_iff_restrict : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {s : Set α} {f : α → β},
  LocallyLipschitzOn s f ↔ LocallyLipschitz (s.domRestrict f)
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Pullback `PosMulMono`.  -/
Function.Injective.posMulMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [PosMulMono α] {β : Type u_2} [inst_4 : Zero β]
  [inst_5 : Mul β] [inst_6 : Preorder β] (f : β → α),
  f 0 = 0 → (∀ (x y : β), f (x * y) = f x * f y) → (∀ {x y : β}, f x ≤ f y ↔ x ≤ y) → PosMulMono β
-- Mathlib.Order.Filter.Cofinite
/-- Given finite families of maps `f i : α i → β i` and of filters `l i : Filter (α i)`,
the indexed product of `f i`s maps the indexed product of the filters `l i`
to the indexed products of their pushforwards under individual `f i`s.

See also `map_piMap_pi` for a more general case.
 -/
Filter.map_piMap_pi_finite : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [Finite ι] (f : (i : ι) → α i → β i)
  (l : (i : ι) → Filter (α i)), Filter.map (Pi.map f) (Filter.pi l) = Filter.pi fun i => Filter.map (f i) (l i)
-- Lean.Meta.Tactic.Assert
/-- Finds the `LocalDecl` for the FVar in `e` with the highest index.  -/
_private.Lean.Meta.Tactic.Assert.0.Lean.MVarId.assertAfter'.findMaxFVar : Lean.Expr → StateRefT' IO.RealWorld Lean.LocalDecl Lean.MetaM Unit
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.inv_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} (e : X ⟶ Y) [inst_3 : CategoryTheory.IsIso e],
  (CategoryTheory.inv e).left = CategoryTheory.inv e.left
-- Mathlib.GroupTheory.PGroup
IsPGroup.comap_of_ker_isPGroup : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H : Subgroup G},
  IsPGroup p ↥H → ∀ {K : Type u_2} [inst_1 : Group K] (ϕ : K →* G), IsPGroup p ↥ϕ.ker → IsPGroup p ↥(Subgroup.comap ϕ H)
-- Aesop.Tree.Check
Aesop.MVarClusterRef.checkInvariants : Aesop.MVarClusterRef → Lean.Meta.SavedState → Lean.MetaM Unit
-- Mathlib.Algebra.Star.Basic
MulOpposite.op_star : ∀ {R : Type u} [inst : Star R] (r : R), MulOpposite.op (star r) = star (MulOpposite.op r)