mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- Given a co-Cartesian morphism `φ : a ⟶ b` lying over `f : R ⟶ S` in `𝒳`, and another morphism
`φ' : a ⟶ b'` which also lifts `f`, then `IsCocartesian.map f φ φ'` is the morphism `b ⟶ b'` lying
over `𝟙 S` obtained from the universal property of `φ`.  -/
CategoryTheory.Functor.IsCocartesian.map : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        (p : CategoryTheory.Functor 𝒳 𝒮) →
          {R S : 𝒮} →
            {a b : 𝒳} →
              (f : R ⟶ S) → (φ : a ⟶ b) → [p.IsCocartesian f φ] → {b' : 𝒳} → (φ' : a ⟶ b') → [p.IsHomLift f φ'] → b ⟶ b'
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_eq_loops_of_subset : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, X ⊆ M.loops → M.closure X = M.loops
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.mk.sizeOf_spec : ∀ {α : Type u_1} {f : Filter α} [inst : SizeOf α] (σ : Type u_5) (F : CFilter (Set α) σ) (eq : F.toFilter = f),
  sizeOf { σ := σ, F := F, eq := eq } = 1 + sizeOf σ + sizeOf F + sizeOf eq
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- The lift of the identity morphism is homotopic to the identity chain map.  -/
CategoryTheory.ProjectiveResolution.liftIdHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (X : C) →
        (P : CategoryTheory.ProjectiveResolution X) →
          Homotopy (CategoryTheory.ProjectiveResolution.lift (CategoryTheory.CategoryStruct.id X) P P)
            (CategoryTheory.CategoryStruct.id P.complex)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : CommMonoid β]
  [inst_3 : ContinuousMul β] {ι : Type u_3} (s : Finset ι) (f : ι → C(α, β)), ⇑(∏ i ∈ s, f i) = ∏ i ∈ s, ⇑(f i)
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.of_algHom : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] {L : Type u_7} [inst_2 : Field L]
  [inst_3 : Algebra A K] [IsFractionRing A K] [inst_5 : Algebra A L] (f : L →ₐ[A] K), IsFractionRing A L
-- Mathlib.Topology.Algebra.MulAction
ContinuousSMul.continuousConstSMul : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : SMul M X]
  [ContinuousSMul M X], ContinuousConstSMul M X
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- The functor picking out the `i`-th object of a complex.  -/
HomologicalComplex.eval : {ι : Type u_1} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        (c : ComplexShape ι) → ι → CategoryTheory.Functor (HomologicalComplex V c) V
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.snd_comp_prodAssoc : ∀ {R : Type u} {M₂ : Type w} {M₃ : Type y} {M₁ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃],
  LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ ↑(LinearEquiv.prodAssoc R M₁ M₂ M₃) = (LinearMap.snd R M₁ M₂).prodMap LinearMap.id
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.lift_def : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u_4} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k] (F : G →* A),
  ⇑((SkewMonoidAlgebra.lift k G A) F) = ⇑(SkewMonoidAlgebra.liftNC ↑(algebraMap k A) ⇑F)
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_unitIso_inv_app_hom_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} (X_1 : CategoryTheory.Limits.Cocone K),
  (CategoryTheory.WithInitial.coconeEquiv.unitIso.inv.app X_1).hom.right = CategoryTheory.CategoryStruct.id X_1.pt.right
-- Mathlib.Algebra.GroupWithZero.Associated
associated_mul_isUnit_right_iff : ∀ {N : Type u_2} [inst : Monoid N] {a b u : N}, IsUnit u → (Associated a (b * u) ↔ Associated a b)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k k' : α},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.getKey? k l = some k' ↔ (k == k') = true ∧ k' ∈ Std.Internal.List.keys l)
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_equivProd_symm_apply : ∀ (R : Type u_1) [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R] (a : R × R × R × R),
  ((Quaternion.equivProd R).symm a).imJ = a.2.2.1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isBoundary₀_iff : ∀ (G : Type u_1) {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A] (a : A),
  groupHomology.IsBoundary₀ G a ↔ ∃ x, (x.sum fun g z => g • z - z) = a
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
/-- If `G` is `Kᵣ₊₂`-free and contains a `Wᵣ,ₖ` together with a vertex `x` adjacent to all of its common
clique vertices then there exist (not necessarily distinct) vertices `a, b, c, d`, one from each of
the four `r + 1`-cliques of `Wᵣ,ₖ`, none of which are adjacent to `x`.
 -/
_private.Mathlib.Combinatorics.SimpleGraph.FiveWheelLike.0.SimpleGraph.IsFiveWheelLike.exist_not_adj_of_adj_inter : ∀ {α : Type u_1} {G : SimpleGraph α} {r k : ℕ} {x v w₁ w₂ : α} {s t : Finset α} [inst : DecidableEq α],
  G.IsFiveWheelLike r k v w₁ w₂ s t →
    G.CliqueFree (r + 2) →
      (∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y) →
        ∃ a b c d,
          a ∈ insert w₁ s ∧
            ¬G.Adj x a ∧
              b ∈ insert w₂ t ∧
                ¬G.Adj x b ∧
                  c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- An orthonormal basis of `ℝ` is made either of the vector `1`, or of the vector `-1`.  -/
orthonormalBasis_one_dim : ∀ {ι : Type u_1} [inst : Fintype ι] (b : OrthonormalBasis ι ℝ ℝ), (⇑b = fun x => 1) ∨ ⇑b = fun x => -1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
/-- The pushforward functor on presheaves of modules for a functor `F : C ⥤ D` and
`R : Dᵒᵖ ⥤ RingCat`. On the underlying presheaves of abelian groups, it is induced
by the precomposition with `F.op`.  -/
PresheafOfModules.pushforward₀ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (R : CategoryTheory.Functor Dᵒᵖ RingCat) →
            CategoryTheory.Functor (PresheafOfModules R) (PresheafOfModules (F.op.comp R))
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_monomial_zero_mul : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (d : ℕ) (r : R),
  ((Polynomial.monomial 0) r * p).coeff d = r * p.coeff d
-- Mathlib.Tactic.FunProp.Theorems
/-- Name of lambda theorem  -/
Mathlib.Meta.FunProp.LambdaTheorem.thmName : Mathlib.Meta.FunProp.LambdaTheorem → Lean.Name
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_ofIntTruncate_of_lt : ∀ {n : ℤ}, n < 2 ^ 7 → (Int8.ofIntClamp n).toNatClampNeg = n.toNat
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmooth_stableUnderComposition : RingHom.StableUnderComposition @RingHom.IsStandardSmooth
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.postAdjunctionRight_counit_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {Y : D} {F : CategoryTheory.Functor T D} {G : CategoryTheory.Functor D T} (a : F ⊣ G)
  (A : CategoryTheory.Over ((CategoryTheory.Functor.id D).obj Y)),
  (CategoryTheory.Over.postAdjunctionRight a).counit.app A = CategoryTheory.Over.homMk (a.counit.app A.left) ⋯
-- Mathlib.Topology.CantorBendixson
CantorBendixson.iteratedDerivedSet_antitone : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), Antitone (CantorBendixson.iteratedDerivedSet s)
-- Init.Data.Nat.Lcm
Nat.lcm_eq_mul_div : ∀ (m n : ℕ), m.lcm n = m * n / m.gcd n
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.pow : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {x : B},
  IsIntegral R x → ∀ (n : ℕ), IsIntegral R (x ^ n)
-- Plausible.Gen
Plausible.instCCPOExceptGenError : {α : Type u_1} → Lean.Order.CCPO (Except Plausible.GenError α)
-- Mathlib.Order.Minimal
/-- **Alias** of `OrderIso.mapSetOfPredMaximal`.

---

If two sets are order isomorphic, their maximals are also order isomorphic.  -/
OrderIso.mapSetOfMaximal : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {s : Set α} → {t : Set β} → ↑s ≃o ↑t → ↑{x | Maximal (fun x => x ∈ s) x} ≃o ↑{x | Maximal (fun x => x ∈ t) x}
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- The structural isomorphism `d ⊙ᵣ (c ⊗ c') ≅ (d ⊙ᵣ c) ⊙ᵣ c'`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso : {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} →
        {inst_2 : CategoryTheory.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D] →
            (d : D) →
              (c c' : C) →
                CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d
                    (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') ≅
                  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj
                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c'
-- Std.Data.TreeMap.Raw.Basic
/-- Returns `true` if the tree map contains no mappings.  -/
Std.TreeMap.Raw.isEmpty : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Bool
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.add_neg : ∀ {R : Type u_2} [inst : Ring R] (a b : R), a + -b = a - b
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
/-- The Radon-Nikodym derivative `∂(μ.trim hm)/∂(ν.trim hm)` of the trimmed measures
(for `hm : m ≤ m0` stating that `m` is a sub-sigma-algebra of `m0`) is a.e.-equal to the
conditional expectation of `∂μ/∂ν` with respect to the sigma-algebra `m`.  -/
MeasureTheory.rnDeriv_trim : ∀ {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} (hm : m ≤ m𝓧)
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.SigmaFinite (ν.trim hm)],
  μ.AbsolutelyContinuous ν →
    (μ.trim hm).rnDeriv (ν.trim hm) =ᵐ[ν.trim hm] fun x => ENNReal.ofReal (ν[fun x => (μ.rnDeriv ν x).toReal | m] x)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
le_dimH_of_hausdorffMeasure_eq_top : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {s : Set X} {d : NNReal},
  (MeasureTheory.Measure.hausdorffMeasure ↑d) s = ⊤ → ↑d ≤ dimH s
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesOpIso_hom_naturality : ∀ {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₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap (CategoryTheory.ShortComplex.opMap φ))
      S₁.opcyclesOpIso.hom =
    CategoryTheory.CategoryStruct.comp S₂.opcyclesOpIso.hom (CategoryTheory.ShortComplex.cyclesMap φ).op
-- Init.Data.SInt.Lemmas
Int8.ofNat_mod : ∀ {a b : ℕ}, a < 2 ^ 7 → b < 2 ^ 7 → Int8.ofNat (a % b) = Int8.ofNat a % Int8.ofNat b
-- Init.Data.UInt.Lemmas
UInt8.toUSize_toUInt64 : ∀ (n : UInt8), n.toUInt64.toUSize = n.toUSize
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smul_finset_symmDiff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {s t : Finset β}
  {a : α}, a • symmDiff s t = symmDiff (a • s) (a • t)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Star
CliffordAlgebra.star_def' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : CliffordAlgebra Q), star x = CliffordAlgebra.involute (CliffordAlgebra.reverse x)
-- Mathlib.ModelTheory.Satisfiability
/-- A consequence of the Löwenheim–Skolem Theorem: If `κ` is a cardinal greater than the
cardinalities of `L` and an infinite `L`-structure `M`, then there is a structure of cardinality `κ`
elementarily equivalent to `M`.  -/
FirstOrder.Language.exists_elementarilyEquivalent_card_eq : ∀ (L : FirstOrder.Language) (M : Type w') [inst : L.Structure M] [Infinite M] (κ : Cardinal.{w}),
  Cardinal.aleph0 ≤ κ →
    Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
      ∃ N, L.ElementarilyEquivalent M ↑N ∧ Cardinal.mk ↑N = κ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.log_toFun_eq_toLogFun : ∀ {m : Tactic.ComputeAsymptotics.UnitMonomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis → Real.log ∘ m.toFun basis =ᶠ[Filter.atTop] m.toLogFun basis
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.rootForm_reflection_reflection_apply : ∀ {ι : 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] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (i : ι) (x y : M), (P.RootForm ((P.reflection i) x)) ((P.reflection i) y) = (P.RootForm x) y
-- Mathlib.Algebra.Star.Prod
Units.embed_product_star : ∀ {R : Type u} [inst : Monoid R] [inst_1 : StarMul R] (u : Rˣ),
  (Units.embedProduct R) (star u) = star ((Units.embedProduct R) u)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
isSMulRegular_iff_mem_nonZeroSMulDivisors : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {M : Type u_4} [inst_1 : AddGroup M] [inst_2 : DistribMulAction M₀ M]
  {m₀ : M₀}, IsSMulRegular M m₀ ↔ m₀ ∈ nonZeroSMulDivisors M₀ M
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.pow_algebraMap : ∀ {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {r s : R} {b : ℕ},
  r ^ b = s → (algebraMap R A) r ^ b = (algebraMap R A) s
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instSMulHom : {R : Type u} →
  [inst : Ring R] →
    {M N : ModuleCat R} →
      {S : Type u_1} → [inst_1 : Monoid S] → [inst_2 : DistribMulAction S ↑N] → [SMulCommClass R S ↑N] → SMul S (M ⟶ N)
-- Mathlib.Algebra.Field.Basic
sub_half : ∀ {K : Type u_1} [inst : DivisionRing K] [NeZero 2] (a : K), a - a / 2 = a / 2
-- Mathlib.Order.Closure
LowerAdjoint.mk : {α : Type u_1} →
  {β : Type u_4} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → {u : β → α} → (toFun : α → β) → GaloisConnection toFun u → LowerAdjoint u
-- Aesop.Tracing
Aesop.TraceOption.forward : Aesop.TraceOption
-- Mathlib.Topology.Sheaves.Flasque
TopCat.Presheaf.IsFlasque.mk : ∀ {X : TopCat} {C : Type v} [inst : CategoryTheory.Category.{w, v} C] {F : TopCat.Presheaf C X},
  (∀ {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V), CategoryTheory.Epi (F.map i)) → F.IsFlasque
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : CommSemiring k] {A : Type u_3} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] (a : G) (b : k) [inst_4 : MulSemiringAction G A] [inst_5 : SMulCommClass G k A],
  SkewMonoidAlgebra.single a ((algebraMap k A) b) =
    (algebraMap k (SkewMonoidAlgebra A G)) b * (SkewMonoidAlgebra.of A G) a
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.Integrable.simpleFunc_mul : ∀ {X : Type u_6} {f : X → ℝ} {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X} (g : MeasureTheory.SimpleFunc X ℝ),
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (⇑g * f) μ
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- The canonical isomorphism between
`SheafOfModules.toSheaf R ⋙ sheafToPresheaf J AddCommGrpCat.{v}`
and `SheafOfModules.forget R ⋙ PresheafOfModules.toPresheaf R.val`.  -/
SheafOfModules.toSheafCompSheafToPresheafIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) →
        (SheafOfModules.toSheaf R).comp (CategoryTheory.sheafToPresheaf J AddCommGrpCat) ≅
          (SheafOfModules.forget R).comp (PresheafOfModules.toPresheaf R.obj)
-- Mathlib.CategoryTheory.MorphismProperty.Local
/-- If `P` holds for `f : X ⟶ Y`, it also holds for `f` restricted to `Uᵢ` for any
`K`-cover `R` of `Y`.  -/
CategoryTheory.MorphismProperty.IsLocalAtTarget.pullbackSnd : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [self : P.IsLocalAtTarget K] {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X}
  {U : C} {g : U ⟶ X},
  R ∈ K.coverings X →
    R g → P f → ∀ [inst_1 : CategoryTheory.Limits.HasPullback f g], P (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
/-- For any `f`, if `F.map f` is an iso, then so was `f`.  -/
CategoryTheory.Functor.ReflectsIsomorphisms.reflects : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} (F : CategoryTheory.Functor C D) [self : F.ReflectsIsomorphisms]
  {A B : C} (f : A ⟶ B) [CategoryTheory.IsIso (F.map f)], CategoryTheory.IsIso f
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_endomorphism : ∀ {R : Type u} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : M →ₗ[R] M)
  (v : M) (p : Polynomial R), ((Polynomial.aeval f) p) v = p.sum fun n b => b • (f ^ n) v
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.keys_insertIfNew_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp] {k : α}, (t.insertIfNew k ()).keys.Perm (if k ∈ t then t.keys else k :: t.keys)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal
PresheafOfModules.instMonoidalCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierOpPushforward₀OfCommRingCat : {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 D) →
          (R : CategoryTheory.Functor Dᵒᵖ CommRingCat) → (PresheafOfModules.pushforward₀OfCommRingCat F R).Monoidal
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_mk : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗ[σ₁₂] E₂) (he : ∀ (x : E), ‖e x‖ = ‖x‖), ⇑{ toLinearEquiv := e, norm_map' := he } = ⇑e
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- **Alias** of `SimpleGraph.Walk.length_takeUntil_lt_length`. -/
SimpleGraph.Walk.length_takeUntil_lt : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} {p : G.Walk v w} (h : u ∈ p.support),
  u ≠ w → (p.takeUntil u h).length < p.length
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.of_iInf_mem : ∀ {α : Type u_2} {s : Set α} [inst : CompleteLattice α],
  (∀ (A : ℕ → α), (∀ (n : ℕ), A n ∈ s) → ⨅ n, A n ∈ s) → CountableInfClosed s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, (t₁ ∪ t₂).getKeyD k fallback = t₂.getKeyD k (t₁.getKeyD k fallback)
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `insert` which can be used in the absence of balance information but
still assumes the preconditions of `insert`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.insert! : {α : Type u} →
  {β : α → Type v} → [Ord α] → (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Lean.Elab.Do.Control
Lean.Elab.Do.EffectForwarder.mk.inj : ∀ {origCont : Lean.Elab.Do.DoElemCont} {returnBase? breakBase? continueBase? : Option Lean.Elab.Do.ControlStack}
  {liftedStack : Lean.Elab.Do.ControlStack} {liftedDoBlockResultType : Lean.Expr} {origCont_1 : Lean.Elab.Do.DoElemCont}
  {returnBase?_1 breakBase?_1 continueBase?_1 : Option Lean.Elab.Do.ControlStack}
  {liftedStack_1 : Lean.Elab.Do.ControlStack} {liftedDoBlockResultType_1 : Lean.Expr},
  { origCont := origCont, returnBase? := returnBase?, breakBase? := breakBase?, continueBase? := continueBase?,
        liftedStack := liftedStack, liftedDoBlockResultType := liftedDoBlockResultType } =
      { origCont := origCont_1, returnBase? := returnBase?_1, breakBase? := breakBase?_1,
        continueBase? := continueBase?_1, liftedStack := liftedStack_1,
        liftedDoBlockResultType := liftedDoBlockResultType_1 } →
    origCont = origCont_1 ∧
      returnBase? = returnBase?_1 ∧
        breakBase? = breakBase?_1 ∧
          continueBase? = continueBase?_1 ∧
            liftedStack = liftedStack_1 ∧ liftedDoBlockResultType = liftedDoBlockResultType_1
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.sum_le_card_nsmul : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddRightMono M] [AddLeftMono M] (l : List M) (n : M),
  (∀ x ∈ l, x ≤ n) → l.sum ≤ l.length • n
-- Mathlib.Logic.Equiv.Embedding
/-- Embeddings whose range lies within a set are equivalent to embeddings to that set.
This is `Function.Embedding.codRestrict` as an equiv.  -/
Equiv.codRestrict : (α : Type u_1) → {β : Type u_2} → (bs : Set β) → { f // ∀ (a : α), f a ∈ bs } ≃ (α ↪ ↑bs)
-- Lean.Parser.Do
/-- `debug_assert! cond` panics if `cond` evaluates to `false` and the executing code has been built
with debug assertions enabled (see the `debugAssertions` option).
 -/
Lean.Parser.Term.doDebugAssert : Lean.Parser.Parser
-- Mathlib.Data.Multiset.AddSub
Multiset.add_singleton_eq_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} {a : α}, s + {a} = t ↔ a ∈ t ∧ s = t.erase a
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingSubmonoid_antitone : ∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : MulAction M α], Antitone fun s => fixingSubmonoid M s
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.rIn_lt_rOut : ∀ {E : Type u_1} {c : E} (self : ContDiffBump c), self.rIn < self.rOut
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_const_id_atBot : ∀ {E'' : Type u_9} [inst : NormedAddCommGroup E''] (c : E''), (fun _x => c) =o[Filter.atBot] id
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_monomial : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  (f : R →+* S₁) (g : σ → S₁), MvPolynomial.eval₂ f g ((MvPolynomial.monomial s) a) = f a * s.prod fun n e => g n ^ e
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.isSimpleOrder_of_finrank_prime : ∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E],
  Nat.Prime (Module.finrank F E) → IsSimpleOrder (IntermediateField F E)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.ofSupport_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), SimpleGraph.Walk.ofSupport p.support ⋯ ⋯ = p.copy ⋯ ⋯
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Nonnegative distance between two points  -/
NNDist.nndist : {α : Type u_3} → [self : NNDist α] → α → α → NNReal
-- Mathlib.Algebra.BigOperators.Pi
eqOn_finsetSum : ∀ {ι : Type u_8} {α : Type u_9} {β : Type u_10} [inst : AddCommMonoid α] {s : Set β} {f f' : ι → β → α},
  (∀ (i : ι), Set.EqOn (f i) (f' i) s) → ∀ (v : Finset ι), Set.EqOn (∑ i ∈ v, f i) (∑ i ∈ v, f' i) s
-- Aesop.Tree.Data
Aesop.Rapp.id : Aesop.Rapp → Aesop.RappId