mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.facePairComplIso_hom_ι : ∀ {n : ℕ} (i j : Fin (n + 3)) (h : i < j),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.facePairComplIso i j h).hom (SSet.stdSimplex.face {i, j}ᶜ).ι =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ (i.castPred ⋯)) (SSet.stdSimplex.δ j)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_7} {F : Type u_8} [inst_2 : CommRing S]
  [inst_3 : IsDomain S] [inst_4 : FunLike F R S] [inst_5 : MonoidHomClass F R S] {n : ℕ} [inst_6 : NeZero n] {f : F}
  (hf : Function.Injective ⇑f) (hζ : (primitiveRoots n R).Nonempty) (a : ↥(rootsOfUnity n R)),
  ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ) a) = f ↑↑a
-- Batteries.Util.ProofWanted
instance_wanted.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.curry_neg : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : (a : α) → (b : β a) → Neg (γ a b)]
  (x : (i : (a : α) × β a) → γ i.fst i.snd), Sigma.curry (-x) = -Sigma.curry x
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.nnqsmul_eq_C_mul : ∀ {R : Type u} [inst : DivisionSemiring R] (q : ℚ≥0) (f : Polynomial R), q • f = Polynomial.C ↑q * f
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- `comapDomain` as an `AddMonoidHom`.  -/
MonoidAlgebra.comapDomainAddMonoidHom : {R : Type u_3} →
  {M : Type u_6} →
    {N : Type u_7} → [inst : Semiring R] → (f : M → N) → Function.Injective f → MonoidAlgebra R N →+ MonoidAlgebra R M
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.instDecidableEqValue : DecidableEq Fin.Value✝
-- Mathlib.RingTheory.Valuation.Integers
/-- **Alias** of `Valuation.Integers.isPrincipal_iff_exists_eq_setOfPred_valuation_le`. -/
Valuation.Integers.isPrincipal_iff_exists_eq_setOf_valuation_le : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O →
    ∀ {I : Ideal O}, Submodule.IsPrincipal I ↔ ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
polarCoord_apply : ∀ (q : ℝ × ℝ), ↑polarCoord q = (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)
-- Lean.Structure
Lean.StructureResolutionOrderResult.conflicts : Lean.StructureResolutionOrderResult → Array Lean.StructureResolutionOrderConflict
-- Mathlib.Order.Filter.IsBounded
Filter.isCobounded_top : ∀ {α : Type u_1} {r : α → α → Prop}, Filter.IsCobounded r ⊤ ↔ Nonempty α
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivWithinAt_sdiff_singleton_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' (s \ {x}) x ↔ HasFDerivWithinAt f f' s x
-- Mathlib.RingTheory.Ideal.Over
Ideal.IsPrime.under : ∀ (A : Type u_2) [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B)
  [hP : P.IsPrime], (Ideal.under A P).IsPrime
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.support_subset_of_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X} {t : Set X},
  IsClosed t → t ∈ MeasureTheory.ae μ → μ.support ⊆ t
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientMap_comp_mk : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] {J : Ideal R} {I : Ideal S} [inst_2 : I.IsTwoSided]
  [inst_3 : J.IsTwoSided] {f : R →+* S} (H : J ≤ Ideal.comap f I),
  (Ideal.quotientMap I f H).comp (Ideal.Quotient.mk J) = (Ideal.Quotient.mk I).comp f
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.projVandermonde_comp : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} {v w : Fin n → R} (f : Fin n → Fin n),
  Matrix.projVandermonde (v ∘ f) (w ∘ f) = (Matrix.projVandermonde v w).submatrix f id
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Eta-expanded form of `Measurable.div` -/
Measurable.fun_div : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Div G] {m : MeasurableSpace α} {f g : α → G}
  [MeasurableDiv₂ G], Measurable f → Measurable g → Measurable fun i => f i / g i
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_filter_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  (Std.DTreeMap.filter f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f k (t.get k h) = true
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.antilipschitz : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), AntilipschitzWith 1 ⇑e
-- Batteries.Data.PairingHeap
/-- Amortized `O(log n)`. Find and remove the the minimum element from the heap.  -/
Batteries.PairingHeapImp.Heap.deleteMin : {α : Type u_1} → (α → α → Bool) → Batteries.PairingHeapImp.Heap α → Option (α × Batteries.PairingHeapImp.Heap α)
-- Init.Data.Nat.Basic
Nat.ne_of_gt : ∀ {a b : ℕ}, b < a → a ≠ b
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_diagonal : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : Ring 𝔸]
  [inst_3 : TopologicalSpace 𝔸] [inst_4 : IsTopologicalRing 𝔸] [T2Space 𝔸] [Algebra ℚ 𝔸] (v : m → 𝔸),
  NormedSpace.exp (Matrix.diagonal v) = Matrix.diagonal (NormedSpace.exp v)
-- Init.Data.Fin.Lemmas
Fin.instAssociativeHMul : ∀ {n : ℕ}, Std.Associative fun x1 x2 => x1 * x2
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.toGlued.eq_1 : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) (i : ι),
  AlgebraicGeometry.Scheme.LocalRepresentability.toGlued hf i =
    (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).ι i
-- Mathlib.Algebra.Group.Pi.Basic
Pi.divInvMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → DivInvMonoid (f i)],
  Pi.divInvMonoid =
    { toMonoid := Pi.monoid, toInv := Pi.instInv, toDiv := Pi.instDiv, zpow := fun z x i => x i ^ z,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯ }
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_insertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced),
  l.Ordered →
    (Std.DTreeMap.Internal.Impl.insertIfNew k v l hlb).impl.toListModel.Perm
      (Std.Internal.List.insertEntryIfNew k v l.toListModel)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.subsingleton_of_empty_right : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [IsEmpty n], Subsingleton (Matrix m n α)
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.Arrow 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 X₃.left)]
  [inst_4 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorRight X₃.right)]
  [inst_5 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft X₁.left)]
  [inst_6 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft X₁.right)],
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator X₁ X₂ X₃).inv.right =
    (CategoryTheory.MonoidalCategoryStruct.associator X₁.right X₂.right X₃.right).inv
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom : ∀ {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)
  (X_1 : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)),
  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso F U).hom.app X_1).hom =
    CategoryTheory.CategoryStruct.id X_1.pt
-- Mathlib.MeasureTheory.PiSystem
generatePiSystem_mono : ∀ {α : Type u_1} {S T : Set (Set α)}, S ⊆ T → generatePiSystem S ⊆ generatePiSystem T
-- Mathlib.Data.Fin.Tuple.Sort
Tuple.sort.eq_1 : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] (f : Fin n → α),
  Tuple.sort f = (Tuple.graphEquiv₂ f).trans (Tuple.graphEquiv₁ f).symm
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addZ_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation Q → Q 2 = 0 → W'.addZ P Q = -(Q 1 ^ 2 * P 2) * P 2
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiFunctorExtension : ∀ (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.IsIdempotentComplete D],
  (CategoryTheory.Idempotents.functorExtension C D).IsEquivalence
-- Mathlib.Control.Functor.Multivariate
MvFunctor.LiftP_PredLast_iff : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u_1} [inst : MvFunctor F] [LawfulMvFunctor F] {α : TypeVec.{u} n} {β : Type u}
  (P : β → Prop) (x : F (α ::: β)), MvFunctor.LiftP' (α.PredLast' P) x ↔ MvFunctor.LiftP (α.PredLast P) x
-- Mathlib.Data.Multiset.Find
Multiset.find?.congr_simp : ∀ {α : Type u_1} (p p_1 : α → Prop) (e_p : p = p_1) {inst : DecidablePred p} [inst_1 : DecidablePred p_1]
  (s s_1 : Multiset α) (e_s : s = s_1) (a : {x | x ∈ s ∧ p x}.Subsingleton),
  Multiset.find? p s a = Multiset.find? p_1 s_1 ⋯
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
/-- The condition that a Mayer-Vietoris square becomes a pullback square
when we evaluate a presheaf on it.  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] →
        J.MayerVietorisSquare →
          {A : Type u'} → [inst_2 : CategoryTheory.Category.{v', u'} A] → CategoryTheory.Functor Cᵒᵖ A → Prop
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.toLinearEquiv : {R : Type u_2} →
  {M₁ : Type u_5} →
    {M₂ : Type u_6} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] →
                      {Q₁ : QuadraticMap R M₁ N} → {Q₂ : QuadraticMap R M₂ N} → Q₁.IsometryEquiv Q₂ → M₁ ≃ₗ[R] M₂
-- Mathlib.CategoryTheory.Category.PartialFun
partialFunEquivPointed_functor_obj_X : ∀ (X : PartialFun), (partialFunEquivPointed.functor.obj X).X = Option X
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- `a` is less than or equal to `b` if and only if `b` is either `a` or a transitive successor
of `a`.
 -/
Std.PRange.LawfulUpwardEnumerableLE.le_iff : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : LE α} [self : Std.PRange.LawfulUpwardEnumerableLE α]
  (a b : α), a ≤ b ↔ Std.PRange.UpwardEnumerable.LE a b
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_eq_iff_eq_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x : R} {y : ↥M} {z : S},
  IsLocalization.mk' S x y = z ↔ (algebraMap R S) x = z * (algebraMap R S) ↑y
-- Std.Data.HashSet.Lemmas
Std.HashSet.isSome_get?_iff_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a : α},
  (m.get? a).isSome = true ↔ a ∈ m
-- Mathlib.NumberTheory.Zsqrtd.Basic
instDecidableEqZsqrtd : {d : ℤ} → DecidableEq (ℤ√d)
-- Mathlib.Data.NNReal.Defs
Real.natCast_lt_toNNReal : ∀ {r : ℝ} {n : ℕ}, ↑n < r.toNNReal ↔ ↑n < r
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.Functor.commShiftOfLocalization.iso_inv_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W] {A : Type w} [inst_4 : AddMonoid A]
  [inst_5 : CategoryTheory.HasShift C A] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E)
  [inst_6 : CategoryTheory.Localization.Lifting L W F F'] [inst_7 : CategoryTheory.HasShift D A]
  [inst_8 : CategoryTheory.HasShift E A] [inst_9 : L.CommShift A] [inst_10 : F.CommShift A] (a : A) (X : C),
  (CategoryTheory.Functor.commShiftOfLocalization.iso L W F F' a).inv.app (L.obj X) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor E a).map ((CategoryTheory.Localization.Lifting.iso L W F F').hom.app X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app X)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Localization.Lifting.iso L W F F').inv.app ((CategoryTheory.shiftFunctor C a).obj X))
          (F'.map ((CategoryTheory.Functor.commShiftIso L a).hom.app X))))
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.Prepartition.mem_biUnionTagged : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J}, J ∈ π.biUnionTagged πi ↔ ∃ J' ∈ π, J ∈ πi J'
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- A family is affinely independent if and only if any affine
combinations (with sum of weights 1) that evaluate to the same point
have equal `Set.indicator`.  -/
affineIndependent_iff_indicator_eq_of_affineCombination_eq : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P),
  AffineIndependent k p ↔
    ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      ∑ i ∈ s1, w1 i = 1 →
        ∑ i ∈ s2, w2 i = 1 →
          (Finset.affineCombination k s1 p) w1 = (Finset.affineCombination k s2 p) w2 →
            (↑s1).indicator w1 = (↑s2).indicator w2
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.BifibrantObject.homMk_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] (X : C) [inst_5 : HomotopicalAlgebra.IsCofibrant X]
  [inst_6 : HomotopicalAlgebra.IsFibrant X],
  HomotopicalAlgebra.BifibrantObject.homMk (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id (HomotopicalAlgebra.BifibrantObject.mk X)
-- Mathlib.CategoryTheory.Action.Basic
Action.resComp_inv_app_hom : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} {K : Type u_5}
  [inst_1 : Monoid G] [inst_2 : Monoid H] [inst_3 : Monoid K] (f : G →* H) (g : H →* K) (X : Action V K),
  ((Action.resComp V f g).inv.app X).hom = CategoryTheory.CategoryStruct.id X.V
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atTop_add_left_of_le : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  (∀ (x : α), C ≤ f x) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- The `n`th group homology of a `k`-linear `G`-representation `A` is isomorphic to
`Torₙ(A, k)` (taken in `Rep k G`), where `k` is a trivial `k`-linear `G`-representation.  -/
groupHomologyIsoTor : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        [DecidableEq G] → (n : ℕ) → groupHomology A n ≅ ((Rep.Tor k G n).obj A).obj (Rep.trivial k G k)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.commAlgEquiv.eq_1 : ∀ (R : Type u_1) {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N],
  MonoidAlgebra.commAlgEquiv R =
    (MonoidAlgebra.curryAlgEquiv R).symm.trans
      ((MonoidAlgebra.domCongr R A MulEquiv.prodComm).trans (MonoidAlgebra.curryAlgEquiv R))
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.map_inr : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ →* N₂) (fg : G₁ →* G₂)
  (h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn) (g : G₁),
  (SemidirectProduct.map fn fg h) (SemidirectProduct.inr g) = SemidirectProduct.inr (fg g)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.nhdsWithin_bot : nhdsWithin ⊥ {⊥}ᶜ = Filter.map Real.toEReal Filter.atBot
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.pairingIn_le_zero_iff : ∀ {ι : 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) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : LinearOrder S] [IsStrictOrderedRing S] [inst_8 : Algebra S R] [FaithfulSMul S R]
  [inst_10 : Module S M] [IsScalarTower S R M] [inst_12 : P.IsValuedIn S] {i j : ι} [Finite ι] [NeZero 2] [IsDomain R]
  [Module.IsTorsionFree R M], P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instToMessageDataCodeLiveness : Lean.ToMessageData Lean.Elab.Do.CodeLiveness
-- Mathlib.GroupTheory.Submonoid.Center
Subsemigroup.centerToMulOpposite.eq_1 : ∀ {M : Type u_2} [inst : Mul M],
  Subsemigroup.centerToMulOpposite =
    { toFun := fun r => ⟨MulOpposite.op ↑r, ⋯⟩, invFun := fun r => ⟨MulOpposite.unop ↑r, ⋯⟩, left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯ }
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_add : ∀ (a b : UInt16), (a + b).toUInt8 = a.toUInt8 + b.toUInt8
-- Mathlib.Data.Finset.Lattice.Basic
Finset.subset_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ u : Finset α}, s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatch.isMatch : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos → String.Slice.Pattern.Model.IsMatch pat pos
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: the sum of (the `r`-powers of) the product of two functions is bounded by
the product of their `L^p` and `L^q` norms when `p`, `q` and `r` form a `Real.HolderTriple`.
Version for sums over finite sets, with real-valued functions.  -/
Real.Lr_rpow_le_Lp_mul_Lq : ∀ {ι : Type u} (s : Finset ι) (f g : ι → ℝ) {p q r : ℝ},
  p.HolderTriple q r → ∑ i ∈ s, |f i * g i| ^ r ≤ (∑ i ∈ s, |f i| ^ p) ^ (r / p) * (∑ i ∈ s, |g i| ^ q) ^ (r / q)
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.integral_add_const : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [OpensMeasurableSpace X]
  {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X ℝ) (c : ℝ),
  ∫ (x : X), (f + BoundedContinuousFunction.const X c) x ∂μ = ∫ (x : X), f x ∂μ + μ.real Set.univ • c
-- Mathlib.Data.EReal.Basic
instLinearOrderEReal : LinearOrder EReal
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.center_toAddSubmonoid : ∀ (G : Type u_1) [inst : AddGroup G], (AddSubgroup.center G).toAddSubmonoid = AddSubmonoid.center G
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A],
  CanLift (Set A) (NonUnitalSubalgebra R A) SetLike.coe fun s =>
    0 ∈ s ∧
      (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
        (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R) {x : A}, x ∈ s → r • x ∈ s
-- Mathlib.RingTheory.Localization.Defs
Localization.mk_eq_mk'_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (x : R) (y : ↥M),
  Localization.mk x y = IsLocalization.mk' (Localization M) x y
-- Mathlib.Data.List.OffDiag
List.mem_offDiag_iff_getElem : ∀ {α : Type u_1} {l : List α} {x : α × α},
  x ∈ l.offDiag ↔ ∃ i, ∃ (x_1 : i < l.length), ∃ j, ∃ (x_2 : j < l.length), i ≠ j ∧ l[i] = x.1 ∧ l[j] = x.2
-- Mathlib.Algebra.Group.Equiv.Defs
instCoeTCAddEquivOfAddEquivClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : Add α] [inst_2 : Add β]
  [inst_3 : AddEquivClass F α β], instCoeTCAddEquivOfAddEquivClass = { coe := AddEquivClass.toAddEquiv }
-- Lean.Meta.Basic
Lean.Meta.Cache.whnf : Lean.Meta.Cache → Lean.Meta.WhnfCache
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.even_card_aut_of_not_isUnramifiedIn : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K]
  {w : NumberField.InfinitePlace k}, ¬NumberField.InfinitePlace.IsUnramifiedIn K w → Even (Nat.card Gal(K/k))
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mem_normalizer_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {g : G},
  g ∈ Subgroup.normalizer ↑H ↔ ∀ (h : G), h ∈ H ↔ g * h * g⁻¹ ∈ H
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.notMem_of_indep : ∀ {α : Type u_1} {M : Matroid α} {e : α} {I : Set α}, M.IsLoop e → M.Indep I → e ∉ I
-- Mathlib.Data.ZMod.Basic
ZMod.isUnit_prime_of_not_dvd : ∀ {n p : ℕ}, Nat.Prime p → ¬p ∣ n → IsUnit ↑p
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_compl : ∀ {α : Type u_1} {M : Matroid α} {R : Set α},
  autoParam (R ⊆ M.E) Matroid.delete_compl._auto_1 → M.delete (M.E \ R) = M.restrict R
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.natCast : ℕ → Lean.Grind.CommRing.Expr