mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.isoOfIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  {F : TopCat.Presheaf C X} {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {G : TopCat.Presheaf C X} (α : F ≅ G),
  TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.isoOfIso U α =
    CategoryTheory.Limits.Pi.mapIso fun x => α.app (Opposite.op (U x))
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.mkMulProof.eq_def : ∀ {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (l₁ l₂ : Mathlib.Tactic.FieldSimp.qNF M),
  Mathlib.Tactic.FieldSimp.qNF.mkMulProof iM l₁ l₂ =
    match l₁, l₂ with
    | [], l =>
      have a := l.toNF;
      q(⋯)
    | l, [] =>
      have a := l.toNF;
      q(⋯)
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
      if k₁ > k₂ then
        have pf := Mathlib.Tactic.FieldSimp.qNF.mkMulProof iM t₁ (((a₂, x₂), k₂) :: t₂);
        q(⋯)
      else
        if k₁ = k₂ then
          have pf := Mathlib.Tactic.FieldSimp.qNF.mkMulProof iM t₁ t₂;
          q(⋯)
        else
          have pf := Mathlib.Tactic.FieldSimp.qNF.mkMulProof iM (((a₁, x₁), k₁) :: t₁) t₂;
          q(⋯)
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.GoodProducts.range.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I],
  Profinite.NobelingProof.GoodProducts.range C = Set.range (Profinite.NobelingProof.GoodProducts.eval C)
-- Std.Do.WP.Sound
/-- Pure-proposition soundness for `OptionT.run`, generalizing `Option.of_wp_eq`.  -/
Std.Do.OptionT.of_wp_run : ∀ {m : Type u → Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Do.WP m Std.Do.PostShape.pure]
  [Std.Do.WPSound m Std.Do.PostShape.pure] [inst_4 : MonadAttach m] [LawfulMonadAttach m] {α : Type u}
  {prog : OptionT m α} {x : Option α} (P : Option α → Prop),
  MonadAttach.CanReturn prog.run x →
    (⊢ₛ (Std.Do.wp prog).apply (fun a => ⌜P (some a)⌝, fun x => ⌜P none⌝, PUnit.unit)) → P x
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_mul_relfinrank : ∀ {E : Type v} [inst : Field E] {A B C : Subfield E}, A ≤ B → B ≤ C → A.relfinrank B * B.relfinrank C = A.relfinrank C
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.applyCell.eq_2 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] (k : α) (size : ℕ) (k' : α) (v' : β k')
  (l_2 r : Std.DTreeMap.Internal.Impl α β)
  (f_2 :
    (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
      (Std.DTreeMap.Internal.Impl.contains' (compare k) (Std.DTreeMap.Internal.Impl.inner size k' v' l_2 r) = true →
          c.contains = true) →
        δ),
  Std.DTreeMap.Internal.Impl.applyCell k (Std.DTreeMap.Internal.Impl.inner size k' v' l_2 r) f_2 =
    match h : compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.applyCell k l_2 fun c h_1 => f_2 c ⋯
    | Ordering.eq => f_2 (Std.DTreeMap.Internal.Cell.ofEq k' v' ⋯) ⋯
    | Ordering.gt => Std.DTreeMap.Internal.Impl.applyCell k r fun c h_1 => f_2 c ⋯
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).cofan₁ =
    CategoryTheory.Limits.Cofan.mk (∐ fun i => A i.i) (CategoryTheory.Limits.Sigma.ι fun i => A i.i)
-- Mathlib.Order.Filter.IndicatorFunction
Filter.EventuallyEq.mulIndicator_one : ∀ {α : Type u_1} {β : Type u_2} [inst : One β] {l : Filter α} {f : α → β} {s : Set α},
  f =ᶠ[l] 1 → s.mulIndicator f =ᶠ[l] 1
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.isIso_eTruncLT_obj_map_truncLTπ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : EInt),
  a ≤ b → ∀ (X : C), CategoryTheory.IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι b).app X))
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.functorEquivalence_unitIso : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C],
  (CategoryTheory.ShortComplex.functorEquivalence J C).unitIso =
    CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C
-- Mathlib.Order.Ideal
Order.Ideal.isProper_iff_top_notMem : ∀ {P : Type u_1} [inst : LE P] [inst_1 : OrderTop P] {I : Order.Ideal P}, I.IsProper ↔ ⊤ ∉ I
-- Lean.Meta.Sym.SymM
/-- Returns `true` if `e` is the internalized `Bool.true` expression.   -/
Lean.Meta.Sym.isBoolTrueExpr : Lean.Expr → Lean.Meta.Sym.SymM Bool
-- Mathlib.Algebra.Ring.Equiv
/-- Two ring isomorphisms agree if they are defined by the same underlying function.  -/
RingEquiv.ext : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] {f g : R ≃+* S},
  (∀ (x : R), f x = g x) → f = g
-- Mathlib.LinearAlgebra.Ray
Module.Ray.map_refl : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M], Module.Ray.map (LinearEquiv.refl R M) = Equiv.refl (Module.Ray R M)
-- Init.Data.SInt.Lemmas
Int8.toInt64_ofIntLE : ∀ {n : ℤ} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt),
  (Int8.ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n ⋯ ⋯
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.points_vsub_eulerPoint : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.points i -ᵥ s.eulerPoint i = ((↑n - 1) / ↑n) • (s.points i -ᵥ s.mongePoint)
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
/-- Order of vanishing on a locally Noetherian integral scheme as a monoid with zero hom to `ℤᵐ⁰`.
 -/
AlgebraicGeometry.Scheme.ordHom : {X : AlgebraicGeometry.Scheme} →
  [inst : AlgebraicGeometry.IsIntegral X] →
    [AlgebraicGeometry.IsLocallyNoetherian X] →
      (z : ↥X) → Order.coheight z = 1 → ↑X.functionField →*₀ WithZero (Multiplicative ℤ)
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₂_iff : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c},
  e₁.AreComplementary e₂ → ∀ (K : HomologicalComplex C c), K.IsStrictlySupportedOutside e₂ ↔ K.IsStrictlySupported e₁
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatMk_X₂_carrier : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ X₃ : Type v} [inst_1 : AddCommGroup X₁] [inst_2 : AddCommGroup X₂]
  [inst_3 : AddCommGroup X₃] [inst_4 : Module R X₁] [inst_5 : Module R X₂] [inst_6 : Module R X₃] (f : X₁ →ₗ[R] X₂)
  (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0), ↑(CategoryTheory.ShortComplex.moduleCatMk f g hfg).X₂ = X₂
-- Mathlib.Analysis.MellinInversion
mellinInv_eq_fourierInv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (σ : ℝ) (f : ℂ → E) {x : ℝ},
  0 < x →
    mellinInv σ f x =
      ↑x ^ (-↑σ) • FourierTransformInv.fourierInv (fun y => f (↑σ + 2 * ↑Real.pi * ↑y * Complex.I)) (-Real.log x)
-- Init.Data.Int.DivMod.Lemmas
Int.add_fmod_eq_add_fmod_left : ∀ {m n k : ℤ} (i : ℤ), m.fmod n = k.fmod n → (i + m).fmod n = (i + k).fmod n
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_sigma_congr : ∀ {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι'),
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) → Cardinal.mk ((i : ι) × f i) = Cardinal.mk ((i : ι') × g i)
-- Mathlib.Algebra.Star.Subalgebra
/-- Turn a `StarSubalgebra` into a `NonUnitalStarSubalgebra` by forgetting that it contains `1`.  -/
StarSubalgebra.toNonUnitalStarSubalgebra : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Algebra R A] → [inst_5 : StarModule R A] → StarSubalgebra R A → NonUnitalStarSubalgebra R A
-- Mathlib.Analysis.Real.Pi.Irrational
/-- Auxiliary for the proof that `π` is irrational.
For a polynomial `p` with natural degree `≤ k` and integer coefficients, evaluating `p` at a
rational `a / b` gives a rational of the form `z / b ^ k`.
TODO: should this be moved elsewhere? It uses none of the pi-specific definitions.
 -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.is_integer : ∀ {p : Polynomial ℤ} (a b : ℤ) {k : ℕ},
  p.natDegree ≤ k → ∃ z, Polynomial.eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k = ↑z
-- Init.Data.Nat.ToString
Nat.digitChar_eq_star : ∀ {n : ℕ}, n.digitChar = '*' ↔ 16 ≤ n
-- Mathlib.Data.Finset.Max
Multiset.exists_min_image : ∀ {α : Type u_7} {R : Type u_8} [inst : LinearOrder R] (f : α → R) {s : Multiset α}, s ≠ 0 → ∃ y ∈ s, ∀ z ∈ s, f y ≤ f z
-- Lean.Elab.DocString
/-- The user is not editing the doc comment, and should receive suggestions as summaries.
 -/
Lean.Doc.SuggestionMode.batch : Lean.Doc.SuggestionMode
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.toLimitFun.eq_1 : ∀ (P : ProfiniteGrp.{u}), P.toLimitFun = { toFun := fun p => ⟨fun x => ↑p, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
-- Init.Data.UInt.Lemmas
UInt32.toNat_inj : ∀ {a b : UInt32}, a.toNat = b.toNat ↔ a = b
-- Mathlib.Order.Grade
/-- Lifts a graded order along a strictly monotone function.  -/
GradeBoundedOrder.liftRight : {𝕆 : Type u_1} →
  {α : Type u_3} →
    {β : Type u_4} →
      [inst : Preorder 𝕆] →
        [inst_1 : Preorder α] →
          [inst_2 : Preorder β] →
            [GradeBoundedOrder 𝕆 β] →
              (f : α → β) →
                StrictMono f →
                  (∀ (a b : α), a ⋖ b → f a ⋖ f b) →
                    (∀ (a : α), IsMin a → IsMin (f a)) → (∀ (a : α), IsMax a → IsMax (f a)) → GradeBoundedOrder 𝕆 α
-- Init.Data.List.Lemmas
List.contains_eq_mem : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (as : List α), as.contains a = decide (a ∈ as)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.smul_fin3_ext : ∀ {R : Type r} [inst : CommRing R] (P : Fin 3 → R) (u : R),
  (u • P) 0 = u * P 0 ∧ (u • P) 1 = u * P 1 ∧ (u • P) 2 = u * P 2
-- Lean.DocString.Markdown
Lean.Doc.MarkdownM.instInhabitedInlineCtx : Inhabited Lean.Doc.MarkdownM.InlineCtx
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.mk.injEq : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : LE α] (toClopens : TopologicalSpace.Clopens α)
  (upper' : IsUpperSet toClopens.carrier) (toClopens_1 : TopologicalSpace.Clopens α)
  (upper'_1 : IsUpperSet toClopens_1.carrier),
  ({ toClopens := toClopens, upper' := upper' } = { toClopens := toClopens_1, upper' := upper'_1 }) =
    (toClopens = toClopens_1)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.equivOp_apply_coe : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G) (a : ↥H), ↑(H.equivOp a) = MulOpposite.op ↑a
-- Init.Data.UInt.Lemmas
USize.add_eq_left : ∀ {a b : USize}, a + b = a ↔ b = 0
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- The category of types has `PEmpty` as an initial object.  -/
CategoryTheory.Limits.Types.initialColimitCocone : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Functor.empty (Type u))
-- Mathlib.Data.Nat.GCD.BigOperators
Nat.coprime_prod_right_iff : ∀ {ι : Type u_1} {x : ℕ} {t : Finset ι} {s : ι → ℕ}, x.Coprime (∏ i ∈ t, s i) ↔ ∀ i ∈ t, x.Coprime (s i)
-- Mathlib.Analysis.Calculus.Gradient.Basic
/-- Gradient of `f` at the point `x` within the set `s`, if it exists.  Zero otherwise.

If the derivative exists (i.e., `∃ f', HasGradientWithinAt f f' s x`), then
`f x' = f x + ⟨f', x' - x⟩ + o (x' - x)` where `x'` converges to `x` inside `s`.  -/
gradientWithin : {𝕜 : Type u_1} →
  {F : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup F] → [InnerProductSpace 𝕜 F] → [CompleteSpace F] → (F → 𝕜) → Set F → F → F
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.differentiableOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} (p : Polynomial 𝕜),
  DifferentiableOn 𝕜 (fun x => Polynomial.eval x p) s
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_le_mul_of_nonneg_of_nonpos' : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b c d : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
  [AddRightMono R] [AddRightReflectLE R], c ≤ a → b ≤ d → 0 ≤ a → d ≤ 0 → a * b ≤ c * d
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Left component of the associator as a natural isomorphism.  -/
CategoryTheory.Bicategory.associatorNatIsoLeft : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {b c d : B} →
      (a : B) →
        (g : b ⟶ c) →
          (h : c ⟶ d) →
            ((CategoryTheory.Bicategory.postcomposing a b c).obj g).comp
                ((CategoryTheory.Bicategory.postcomposing a c d).obj h) ≅
              (CategoryTheory.Bicategory.postcomposing a b d).obj (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.rightUnitor_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f
        (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Dial C))))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tanh_add_pi_mul_I : ∀ (z : ℂ), Complex.tanh (z + ↑Real.pi * Complex.I) = Complex.tanh z
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : CategoryTheory.Arrow C) {W : C}
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorRight W)],
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso X₁ X₂).hom.left =
    CategoryTheory.CategoryStruct.comp ⋯.isoPushout.hom
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          (CategoryTheory.Limits.spanExt (CategoryTheory.MonoidalCategoryStruct.associator X₁.left X₂.left W)
            (CategoryTheory.MonoidalCategoryStruct.associator X₁.right X₂.left W)
            (CategoryTheory.MonoidalCategoryStruct.associator X₁.left X₂.right W) ⋯ ⋯)).hom
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Sieve.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (S : CategoryTheory.Sieve X),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.forkMap P S.arrows)
      (CategoryTheory.Equalizer.Sieve.firstMap P S) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.forkMap P S.arrows)
      (CategoryTheory.Equalizer.Sieve.secondMap P S)
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_nsmul_le : ∀ {S : Type u_1} [inst : SeminormedAddGroup S] [IsUltrametricDist S] (x : S) (n : ℕ), ‖n • x‖₊ ≤ ‖x‖₊
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonDependencyBuildMode : Lean.FromJson Lean.Lsp.DependencyBuildMode
-- Mathlib.Order.SymmDiff
symmDiff_right_surjective : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a : α), Function.Surjective fun x => symmDiff a x
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Is a prefix of `n₁` related to a prefix of `n₂`?  -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.DirectoryDependency.NamePrefixRel.contains : Mathlib.Linter.DirectoryDependency.NamePrefixRel✝ → Lean.Name → Lean.Name → Bool
-- Mathlib.Computability.AkraBazzi.AkraBazzi
AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_sub_smoothingFn : ∀ {p : ℝ},
  p ≠ 0 →
    (fun x => ‖deriv (fun z => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) x‖) =Θ[Filter.atTop] fun z =>
      z ^ (p - 1)
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_equivCongr : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  (f g : α ≃ β) (p : Equiv.Perm α),
  Equiv.Perm.sign ((f.equivCongr g) p) = Equiv.Perm.sign p * Equiv.Perm.sign (f.symm.trans g)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Radon-Nikodym derivative of the scalar multiple of a measure.
See also `rnDeriv_smul_left`, which has no hypothesis on `μ` but requires finite `ν`.  -/
MeasureTheory.Measure.rnDeriv_smul_left' : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite ν]
  [MeasureTheory.SigmaFinite μ] (r : NNReal), (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintTooltip.plaintext.inj : ∀ {text text_1 : String},
  Lean.Lsp.InlayHintTooltip.plaintext text = Lean.Lsp.InlayHintTooltip.plaintext text_1 → text = text_1
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.le_map_of_comap_le_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {p : Submodule R M} {q : Submodule R₂ M₂} [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Surjective ⇑f → Submodule.comap f q ≤ p → q ≤ Submodule.map f p
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_lpPiLpₗᵢ : ∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [inst_1 : Fintype α]
  {𝕜 : Type u_3} [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : α) → NormedSpace 𝕜 (E i)] [inst_4 : Fact (1 ≤ p)]
  (f : ↥(lp E p)), ((lpPiLpₗᵢ E 𝕜) f).ofLp = ↑f
-- Mathlib.Topology.Separation.Basic
Specializes.eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X}, x ⤳ y → x = y
-- Init.SizeOf
Char.mk.congr_simp : ∀ (val val_1 : UInt32) (e_val : val = val_1) (valid : val.isValidChar),
  { val := val, valid := valid } = { val := val_1, valid := ⋯ }
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.instNonemptyOfIsFibrant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y],
  Nonempty (HomotopicalAlgebra.FibrantBrownFactorization f)
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.fibres_surjective : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} (π : T → S × Option X),
  Function.Surjective π →
    ∀ (σ : Option X → S → T),
      (∀ (x : Option X) (s : S), (π (σ x s)).1 = s) →
        (∀ (x : Option X) (s : S), (π (σ x s)).2 = x) → Function.Surjective fun x => π ↑x
-- Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
AlgebraicGeometry.continuousMapPresheaf_map : ∀ (T : Type v) [inst : TopologicalSpace T] {U V : AlgebraicGeometry.Schemeᵒᵖ} (f : U ⟶ V),
  (AlgebraicGeometry.continuousMapPresheaf T).map f = TypeCat.ofHom fun g => g.comp (TopCat.Hom.hom f.unop.base)
-- Mathlib.Data.Finset.Sum
Finset.toRight_subset_toRight : ∀ {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)}, u ⊆ v → u.toRight ⊆ v.toRight
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.norm_LpToLpOfMeasureLeSMul_le : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {ν : MeasureTheory.Measure α} {c : ENNReal}
  [inst_2 : Fact (1 ≤ p)] (hc : c ≠ ⊤) (h : μ ≤ c • ν),
  ‖MeasureTheory.Lp.LpToLpOfMeasureLeSMul hc h‖ ≤ c.toReal ^ (1 / p).toReal
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.zero_ne_of : ∀ {α : Type u_1} (a : α), 0 ≠ FreeAddMonoid.of a
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.direction_sInf_of_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (t : Set (AffineSubspace k P)) (p : P),
  (∀ s ∈ t, p ∈ s) → (sInf t).direction = ⨅ s ∈ t, s.direction
-- Std.Time.Zoned.Database.TzIf
/-- The total number of characters used in abbreviations.
 -/
Std.Time.TimeZone.TZif.Header.charcnt : Std.Time.TimeZone.TZif.Header → UInt32
-- Mathlib.Algebra.Group.Torsion
neg_ne_self : ∀ {G : Type u_2} [inst : AddGroup G] [IsAddTorsionFree G] {a : G}, -a ≠ a ↔ a ≠ 0
-- Mathlib.Order.Filter.Basic
Filter.Eventually.filter_mono : ∀ {α : Type u} {f₁ f₂ : Filter α}, f₁ ≤ f₂ → ∀ {p : α → Prop}, (∀ᶠ (x : α) in f₂, p x) → ∀ᶠ (x : α) in f₁, p x
-- Mathlib.Algebra.Ring.Hom.Defs
/-- The identity ring homomorphism from a semiring to itself.  -/
RingHom.id : (α : Type u_5) → [inst : NonAssocSemiring α] → α →+* α
-- Init.Data.BitVec.Basic
BitVec.append_eq : ∀ {w v : ℕ} (x : BitVec w) (y : BitVec v), x.append y = x ++ y
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withNewBinderInfosImp : {α : Type} → Array (Lean.FVarId × Lean.BinderInfo) → Lean.MetaM α → Lean.MetaM α
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsStrictRestriction.of_ssubset : ∀ {α : Type u_1} {R R' : Set α} (M : Matroid α), R ⊂ R' → (M.restrict R).IsStrictRestriction (M.restrict R')
-- Mathlib.MeasureTheory.Integral.CircleTransform
Complex.circleTransform.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (R : ℝ) (z w : ℂ) (f : ℂ → E) (θ : ℝ),
  Complex.circleTransform R z w f θ =
    (2 * ↑Real.pi * Complex.I)⁻¹ • deriv (circleMap z R) θ • (circleMap z R θ - w)⁻¹ • f (circleMap z R θ)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_diff! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.Const.get? (m₁.diff! m₂) k =
          if Std.DTreeMap.Internal.Impl.contains k m₂ = true then none else Std.DTreeMap.Internal.Impl.Const.get? m₁ k
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj_hom_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant X] {Y : C}
  {f g : X ⟶ HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj Y},
  HomotopicalAlgebra.LeftHomotopyRel
      (CategoryTheory.CategoryStruct.comp f (HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj Y))
      (CategoryTheory.CategoryStruct.comp g (HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj Y)) →
    HomotopicalAlgebra.CofibrantObject.toHoCat.map (HomotopicalAlgebra.CofibrantObject.homMk f) =
      HomotopicalAlgebra.CofibrantObject.toHoCat.map (HomotopicalAlgebra.CofibrantObject.homMk g)