mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- **Steinhaus Theorem**.

In any locally compact group `G` with an inner regular Haar measure `μ`,
for any measurable set `E` of positive measure, the set `E - E` is a neighbourhood of `0`.  -/
MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [LocallyCompactSpace G]
  [μ.InnerRegular] (E : Set G), MeasurableSet E → 0 < μ E → E - E ∈ nhds 0
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coe_injective : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂],
  Function.Injective ContinuousLinearMap.toLinearMap
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.ext_iff : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  {I J : HomogeneousIdeal 𝒜}, I = J ↔ I.toIdeal = J.toIdeal
-- Init.Data.SInt.Lemmas
ISize.ofIntLE.congr_simp : ∀ (i i_1 : ℤ) (e_i : i = i_1) (_hl : ISize.minValue.toInt ≤ i) (_hr : i ≤ ISize.maxValue.toInt),
  ISize.ofIntLE i _hl _hr = ISize.ofIntLE i_1 ⋯ ⋯
-- Mathlib.CategoryTheory.EpiMono
/-- A composition of `SplitEpi` is a split `SplitEpi`.  -/
CategoryTheory.SplitEpi.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : Y ⟶ Z} →
          CategoryTheory.SplitEpi f →
            CategoryTheory.SplitEpi g → CategoryTheory.SplitEpi (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.RingTheory.DedekindDomain.Basic
IsLocalRing.primesOver_eq : ∀ {R : Type u_1} (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsLocalRing A] [IsDedekindDomain A]
  [inst_4 : Algebra R A] [FaithfulSMul R A] [Module.Finite R A] {p : Ideal R} [p.IsMaximal],
  p ≠ ⊥ → p.primesOver A = {IsLocalRing.maximalIdeal A}
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_reachable : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V]
  {x : V → ℝ}, (SimpleGraph.lapMatrix ℝ G).mulVec x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) Construct the lifted cocone in `Algebra T` which will be colimiting.  -/
CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          {D : CategoryTheory.Functor J T.Algebra} →
            (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) →
              CategoryTheory.Limits.IsColimit c →
                [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] →
                  [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] →
                    CategoryTheory.Limits.Cocone D
-- Mathlib.Order.Heyting.Basic
sdiff_inf_distrib : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (b c a : α), c \ (a ⊓ b) = c \ a ⊔ c \ b
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.first_den_eq : ∀ {K : Type u_1} {g : GenContFract K} [inst : DivisionRing K] {gp : GenContFract.Pair K},
  g.s.get? 0 = some gp → g.dens 1 = gp.b
-- Mathlib.Data.Rel
Monotone.relComp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_6} [inst : Preorder ι] {f : ι → SetRel α β}
  {g : ι → SetRel β γ}, Monotone f → Monotone g → Monotone fun x => (f x).comp (g x)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_iff_forall_le_2 : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {σ₁ σ₂ : Type v} {P Q : σ₁ → σ₂ → l},
  Lean.Order.PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂), Lean.Order.PartialOrder.rel (P s₁ s₂) (Q s₁ s₂)
-- Mathlib.RingTheory.PolynomialAlgebra
instIsScalarTowerPolynomial : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [IsScalarTower R S A],
  IsScalarTower R (Polynomial S) (Polynomial A)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.contains a t = false → Std.DTreeMap.Internal.Impl.Const.get? t a = none
-- Mathlib.Topology.Order.Bornology
/-- Order-bornology on a nonempty lattice. The bounded sets are the sets that are bounded both above
and below.  -/
orderBornology : {α : Type u_1} → [Lattice α] → [Nonempty α] → Bornology α
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The counit morphism of a comonoid object.  -/
CategoryTheory.ComonObj.counit : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {X : C} → [self : CategoryTheory.ComonObj X] → X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Lean.ErrorExplanation
/-- The `doc` field is deprecated and should always be the empty string  -/
Lean.ErrorExplanation.doc : Lean.ErrorExplanation → String
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.vadd_eball : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal), c +ᵥ Metric.eball x r = Metric.eball (c +ᵥ x) r
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- This can't be an instance because Lean wouldn't know how to find `N`, but we can still use
this to manually derive `SMulMemClass` on specific types.  -/
SMulMemClass.ofIsScalarTower : ∀ (S : Type u_1) (M : Type u_2) (N : Type u_3) (α : Type u_4) [inst : SetLike S α] [inst_1 : SMul M N]
  [inst_2 : SMul M α] [inst_3 : Monoid N] [inst_4 : MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α],
  SMulMemClass S M α
-- Mathlib.Topology.Order.Bornology
IsOrderBornology.cobounded_eq_atTop : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : LinearOrder α] [IsOrderBornology α] [NoMaxOrder α] [OrderBot α],
  Bornology.cobounded α = Filter.atTop
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isInt_le_true : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {a b : α} {a' b' : ℤ},
  Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (a' ≤ b') = true → a ≤ b
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
IterateMulAct.instMeasurableSpace : {α : Type u_1} → {f : α → α} → MeasurableSpace (IterateMulAct f)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.rTensor_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f g : N ≃ₗ[R] N),
  LinearEquiv.rTensor M (f * g) = LinearEquiv.rTensor M f * LinearEquiv.rTensor M g
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsAlt.sub : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B₁ B₂ : LinearMap.BilinForm R₁ M₁}, B₁.IsAlt → B₂.IsAlt → (B₁ - B₂).IsAlt
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.colimitModule : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.IsFiltered J] →
          (F : CategoryTheory.Functor J (ModuleCat R)) → Module R ↑(ModuleCat.FilteredColimits.M F)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.univ_sub_univ : ∀ {α : Type u_2} [inst : SubtractionMonoid α], Set.univ - Set.univ = Set.univ
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAt.hasDerivAt : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {g : 𝕜 → 𝕜} {g' u : 𝕜}, HasGradientAt g g' u → HasDerivAt g ((starRingEnd 𝕜) g') u
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.ωSup_def : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c : OmegaCompletePartialOrder.Chain (α →𝒄 β)),
  OmegaCompletePartialOrder.ωSup c = OmegaCompletePartialOrder.ContinuousHom.ωSup c
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → s ∈ nhds x → HasDerivAt f f' x
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.precomp_obj_left : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor C' C)
  (X : CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)),
  ((CategoryTheory.Functor.RightExtension.precomp L F G).obj X).left = X.left
-- Std.Http.Data.URI.Basic
/-- Proposition that `s` is a valid URI scheme per RFC 3986:
`scheme = ALPHA *( ALPHA / DIGIT / "+" / "-" / "." )`.

The scheme value stored in this module is normalized to lowercase.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.1
 -/
Std.Http.URI.IsValidScheme : String → Prop
-- Init.Data.Order.Ord
/-- A typeclass for functions `α → α → Ordering` which are transitive.  -/
Std.TransCmp : {α : Type u} → (α → α → Ordering) → Prop
-- Mathlib.Data.Int.Log
Int.neg_log_inv_eq_clog : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b : ℕ) (r : R), -Int.log b r⁻¹ = Int.clog b r
-- Mathlib.CategoryTheory.Discrete.SumsProducts
/-- The discrete category on a sum is equivalent to the sum of the
discrete categories.  -/
CategoryTheory.Discrete.sumEquiv : {J : Type u_1} →
  {K : Type u_2} → CategoryTheory.Discrete (J ⊕ K) ≌ CategoryTheory.Discrete J ⊕ CategoryTheory.Discrete K
-- Mathlib.MeasureTheory.Measure.Restrict
volume_set_coe_def : ∀ {α : Type u_2} [inst : MeasureTheory.MeasureSpace α] (s : Set α),
  MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.BarrierState.generationId : Std.BarrierState✝ → ℕ
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.Q_idem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Q q) (AlgebraicTopology.DoldKan.Q q) =
    AlgebraicTopology.DoldKan.Q q
-- Init.Omega.IntList
Lean.Omega.IntList.smul_nil : ∀ {i : ℤ}, i * [] = []
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieAlgebra.HasCentralRadical.mk : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.radical R L = LieAlgebra.center R L → LieAlgebra.HasCentralRadical R L
-- Mathlib.Logic.Equiv.Fin.Basic
finAddFlip_apply_mk_right : ∀ {m n k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n), finAddFlip ⟨k, h₂⟩ = ⟨k - m, ⋯⟩
-- Mathlib.Data.Rat.Floor
Rat.natFloor_natCast_div_natCast : ∀ (n d : ℕ), ⌊↑n / ↑d⌋₊ = n / d
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_empty : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V], asymptoticCone k ∅ = ∅
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j))
  ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (p : Y ⟶ (sq i₁ i₂).pullback)
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom._auto_1)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom._auto_3)
  (hp₁ :
    autoParam (CategoryTheory.CategoryStruct.comp p (sq i₁ i₂).p₁ = f₁)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom._auto_5)
  (hp₂ :
    autoParam (CategoryTheory.CategoryStruct.comp p (sq i₁ i₂).p₂ = f₂)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom._auto_7),
  CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q f₁ f₂ hf₁ hf₂ =
    CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom i₁ i₂) p f₁ f₂ ⋯ ⋯
-- Init.Data.Range.Polymorphic.SInt
Int32.instRxiHasSize : Std.Rxi.HasSize Int32
-- Mathlib.Probability.Kernel.Deterministic
ProbabilityTheory.Kernel.instIsDeterministicProdSwap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β},
  ProbabilityTheory.IsDeterministic (ProbabilityTheory.Kernel.swap α β)
-- Mathlib.RingTheory.Localization.Module
LinearIndependent.of_isLocalizedModule : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid Mₛ] [inst_7 : Module R Mₛ] [inst_8 : Module Rₛ Mₛ]
  [IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] {ι : Type u_5} {v : ι → M},
  LinearIndependent R v → LinearIndependent Rₛ (⇑f ∘ v)
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- The first leg of a pullback cone is a normal monomorphism if the left component is too.

See also `pullback.fstOfMono` for the basic monomorphism version, and
`normalOfIsPullbackSndOfNormal` for the flipped version.
 -/
CategoryTheory.normalOfIsPullbackFstOfNormal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q R S : C} →
        {f : P ⟶ Q} →
          {g : P ⟶ R} →
            {h : Q ⟶ S} →
              {k : R ⟶ S} →
                [CategoryTheory.NormalMono k] →
                  (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g comm) →
                      CategoryTheory.NormalMono f
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'}
  (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) {X'' Y'' : C} {h : X'' ⟶ Y''}
  (ψ : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk h),
  data.mapZ (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (data.mapZ φ) (data.mapZ ψ)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.natDegree_pow : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → ∀ (n : ℕ), (p ^ n).natDegree = n * p.natDegree
-- Mathlib.Logic.Encodable.Basic
Encodable.encodek₂ : ∀ {α : Type u_1} [inst : Encodable α] (a : α), Encodable.decode₂ α (Encodable.encode a) = some a
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_unitIso_inv_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (X : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (X_1 : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.equivComma.unitIso.inv.app X).app X_1 =
    (match X_1 with
      | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).inv
-- Lean.Meta.Tactic.LibrarySearch
_private.Lean.Meta.Tactic.LibrarySearch.0.Lean.Meta.LibrarySearch.isVar : Lean.Expr → Bool
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The natural transformation `S.rightHomology ⟶ S.opcycles` for all short complexes `S`.  -/
CategoryTheory.ShortComplex.rightHomologyιNatTrans : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasKernels C] →
        [inst_3 : CategoryTheory.Limits.HasCokernels C] →
          CategoryTheory.ShortComplex.rightHomologyFunctor C ⟶ CategoryTheory.ShortComplex.opcyclesFunctor C
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.hom_map_inv_map_of_iso : ∀ {V W : CategoryTheory.Quiv} (e : V ≅ W) {X Y : ↑W} (f : X ⟶ Y), e.hom.map (e.inv.map f) = Quiver.homOfEq f ⋯ ⋯
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- A point `x` in a C¹ manifold is an interior point if and only if it gets mapped to the interior
of the model space by any given chart - in other words, the notion of interior points does not
depend on any choice of charts.  -/
ModelWithCorners.isInteriorPoint_iff_of_mem_atlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M]
  {e : OpenPartialHomeomorph M H} {x : M},
  n ≠ 0 → e ∈ atlas H M → x ∈ e.source → (I.IsInteriorPoint x ↔ ↑(e.extend I) x ∈ interior (e.extend I).target)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- The target of the edge is `x₁`.  -/
SSet.Truncated.Edge.tgt_eq : ∀ {X : SSet.Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  (self : SSet.Truncated.Edge x₀ x₁),
  (CategoryTheory.ConcreteCategory.hom
        (X.map (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
      self.edge =
    x₁
-- Mathlib.Analysis.Calculus.LineDeriv.Measurable
aemeasurable_lineDeriv_uncurry : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E]
  {F : Type u_3} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  [SecondCountableTopology E] [inst_10 : MeasurableSpace F] [BorelSpace F],
  Continuous f → ∀ (μ : MeasureTheory.Measure (E × E)), AEMeasurable (fun p => lineDeriv 𝕜 f p.1 p.2) μ
-- Aesop.Index.Basic
Aesop.IndexMatchResult.instOrd : {α : Type} → [Ord α] → Ord (Aesop.IndexMatchResult α)
-- Mathlib.Combinatorics.SetFamily.LYM
/-- The downward **local LYM inequality**, with cancelled denominators. `𝒜` takes up less of `α^(r)`
(the finsets of card `r`) than `∂𝒜` takes up of `α^(r - 1)`.  -/
Finset.local_lubell_yamamoto_meshalkin_inequality_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ},
  Set.Sized r ↑𝒜 → 𝒜.card * r ≤ 𝒜.shadow.card * (Fintype.card α - r + 1)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- If the angle between two vectors is 0, the inner product equals the product of the norms.  -/
InnerProductGeometry.inner_eq_mul_norm_of_angle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  InnerProductGeometry.angle x y = 0 → inner ℝ x y = ‖x‖ * ‖y‖
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangle_obj : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  F.mapTriangle.obj T =
    CategoryTheory.Pretriangulated.Triangle.mk (F.map T.mor₁) (F.map T.mor₂)
      (CategoryTheory.CategoryStruct.comp (F.map T.mor₃) ((CategoryTheory.Functor.commShiftIso F 1).hom.app T.obj₁))
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.exists_mul_eq_one : ∀ (F : Type u_1) {K : Type u_2} [inst : Field F] [inst_1 : Ring K] [IsDomain K] [inst_3 : Algebra F K]
  [FiniteDimensional F K] {x : K}, x ≠ 0 → ∃ y, x * y = 1
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullbackOfLeft : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g)
    AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace
-- Mathlib.Data.Analysis.Topology
/-- A realizer of the neighborhood of a point.  -/
Ctop.Realizer.nhds : {α : Type u_1} → [inst : TopologicalSpace α] → Ctop.Realizer α → (a : α) → (nhds a).Realizer
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.nonempty_coe : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), (↑I).Nonempty
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- The triangle (polygon) inequality for sequences of points; `Finset.Ico` version.  -/
dist_le_Ico_sum_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (f : ℕ → α) {m n : ℕ},
  m ≤ n → dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isCofiltered_of_semilatticeInf_nonempty : ∀ (α : Type u) [inst : SemilatticeInf α] [Nonempty α], CategoryTheory.IsCofiltered α
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E` is a perfect field of exponential characteristic `p`, then the (relative) perfect closure
`perfectClosure F E` is perfect.  -/
perfectClosure.perfectRing : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (p : ℕ) [ExpChar E p]
  [PerfectRing E p], PerfectRing (↥(perfectClosure F E)) p
-- Init.Data.Nat.Power2.Lemmas
Nat.instDecidableIsPowerOfTwo : {n : ℕ} → Decidable n.isPowerOfTwo
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.instAdditiveHomologyFunctor : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C],
  (HomologicalComplex.homologyFunctor C c i).Additive
-- Mathlib.NumberTheory.Rayleigh
/-- Let `r > 1` and `1/r + 1/s = 1`. Suppose there is an integer `j` where `B_r` and `B'_s` both
jump over `j` (i.e. an anti-collision). Then this leads to a contradiction.  -/
_private.Mathlib.NumberTheory.Rayleigh.0.Beatty.no_anticollision : ∀ {r s : ℝ}, r.HolderConjugate s → ¬∃ j k m, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1 ∧ ↑m ≤ ↑j / s ∧ (↑j + 1) / s < ↑m + 1
-- Mathlib.LinearAlgebra.Transvection.Generation
LinearEquiv.le_one_add_finrank_fixedSubmodule_dilatransvection_mul : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] (e f : V ≃ₗ[K] V),
  f ∈ LinearEquiv.dilatransvections K V →
    Module.finrank K ↥(↑e).fixedSubmodule ≤ 1 + Module.finrank K ↥(↑(f * e)).fixedSubmodule