mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecificLimits.Normed
summable_of_ratio_norm_eventually_le : ∀ {α : Type u_4} [inst : SeminormedAddCommGroup α] [CompleteSpace α] {f : ℕ → α} {r : ℝ},
  r < 1 → (∀ᶠ (n : ℕ) in Filter.atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖) → Summable f
-- Init.Data.Int.Lemmas
Int.negSucc_add_one_eq_neg_ofNat_iff : ∀ {a b : ℕ}, Int.negSucc a + 1 = -↑b ↔ a = b
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.instHaveLebesgueDecompositionSingularPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, (μ.singularPart ν).HaveLebesgueDecomposition ν
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_neg_of_pos_of_neg : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [PosMulStrictMono α], 0 < a → b < 0 → a * b < 0
-- Mathlib.Analysis.Normed.Order.Lattice
lipschitzWith_posPart : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α],
  LipschitzWith 1 posPart
-- Lean.Meta.DiscrTree.Util
/-- Check for the presence of a value satisfying a predicate.
 -/
Lean.Meta.DiscrTree.containsValueP : {α : Type} → Lean.Meta.DiscrTree α → (α → Bool) → Bool
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_left_le_size_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.size ≤ (m₁ ∪ m₂).size
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C),
  AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso.hom.app X =
    CategoryTheory.CategoryStruct.id (X.obj (Opposite.op CategoryTheory.WithInitial.star))
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension₁_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] (F : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)),
  (CategoryTheory.Idempotents.functorExtension₁ C D).obj F = CategoryTheory.Idempotents.FunctorExtension₁.obj F
-- Init.Data.Vector.Perm
/-- `Perm as bs` asserts that `as` and `bs` are permutations of each other.

This is a wrapper around `List.Perm`, and for now has much less API.
For more complicated verification, use `perm_iff_toList_perm` and the `List` API.
 -/
Vector.«term_~_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.continuous_inr : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A],
  Continuous Unitization.inr
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
/-- `exp` as a homeomorphism.  -/
EReal.expHomeomorph : EReal ≃ₜ ENNReal
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.startsWith_prop_eq_startsWith_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.startsWith p = s.startsWith fun x => decide (p x)
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
/-- The source-local closure of `P` along a precoverage `K` is the weakest property
containing `P` that is local on the source.  -/
CategoryTheory.MorphismProperty.sourceLocalClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Precoverage C → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.discreteTopology : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {N : Subgroup G},
  IsOpen ↑N → DiscreteTopology (G ⧸ N)
-- Mathlib.CategoryTheory.Sites.Types
/-- `yoneda'` induces an equivalence of categories between `Type u` and
`Sheaf typesGrothendieckTopology (Type u)`.  -/
CategoryTheory.typeEquiv : Type u ≌ CategoryTheory.Sheaf CategoryTheory.typesGrothendieckTopology (Type u)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.t3Space_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], T3Space (TopologicalSpace.NonemptyCompacts α) ↔ T3Space α
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.inv : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Inv β] [ContinuousInv β],
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable f⁻¹ μ
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_biUnion_le : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] {m : MeasureTheory.AddContent G C}
  [inst_1 : PartialOrder G] [CanonicallyOrderedAdd G] {ι : Type u_3},
  MeasureTheory.IsSetRing C → ∀ {s : ι → Set α} {S : Finset ι}, (∀ n ∈ S, s n ∈ C) → m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.autMapHom.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] {A B : C}
  [inst_2 : CategoryTheory.PreGaloisCategory.IsConnected A] [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois B]
  (f f_1 : A ⟶ B),
  f = f_1 → CategoryTheory.PreGaloisCategory.autMapHom f = CategoryTheory.PreGaloisCategory.autMapHom f_1
-- Mathlib.Data.Nat.Choose.Sum
/-- The sum of entries in a row of Pascal's triangle  -/
Nat.sum_range_choose : ∀ (n : ℕ), ∑ m ∈ Finset.range (n + 1), n.choose m = 2 ^ n
-- Mathlib.LinearAlgebra.Dimension.OrzechProperty
/-- A finite family of vectors is linearly independent if and only if
its cardinality equals the dimension of its span.  -/
linearIndependent_iff_card_eq_finrank_span : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [OrzechProperty R] [inst_2 : AddCommMonoid M] [inst_3 : Module R M]
  [Nontrivial R] {ι : Type u_3} [inst_5 : Fintype ι] {b : ι → M},
  LinearIndependent R b ↔ Fintype.card ι = Set.finrank R (Set.range b)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropOn_congr_iff : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g g' : M → M'} {s : Set M},
  G.LocalInvariantProp G' P → (∀ y ∈ s, g' y = g y) → (ChartedSpace.LiftPropOn P g' s ↔ ChartedSpace.LiftPropOn P g s)
-- Mathlib.Logic.Equiv.Set
Equiv.ofLeftInverse'.congr_simp : ∀ {α : Sort u_3} {β : Type u_4} (f : α → β) (f_inv f_inv_1 : β → α) (e_f_inv : f_inv = f_inv_1)
  (hf : Function.LeftInverse f_inv f), Equiv.ofLeftInverse' f f_inv hf = Equiv.ofLeftInverse' f f_inv_1 ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α}, t.contains a = true → t.getKey? a = some (t.getKeyD a fallback)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.add_kroneckerTMul : ∀ (R : Type u_1) {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid α] [inst_2 : Module R α] (A₁ A₂ : Matrix l m α) (B : Matrix n p α),
  Matrix.kroneckerMap (TensorProduct.tmul R) (A₁ + A₂) B =
    Matrix.kroneckerMap (TensorProduct.tmul R) A₁ B + Matrix.kroneckerMap (TensorProduct.tmul R) A₂ B
-- Mathlib.Order.Heyting.Basic
Prod.instHeytingAlgebra : {α : Type u_2} → {β : Type u_3} → [HeytingAlgebra α] → [HeytingAlgebra β] → HeytingAlgebra (α × β)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.two_lt_edist_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, 2 < G.edist u v ↔ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
-- Init.Core
Std.Associative.mk : ∀ {α : Sort u} {op : α → α → α}, (∀ (a b c : α), op (op a b) c = op a (op b c)) → Std.Associative op
-- Lean.LocalContext
/-- Class used to denote that `m` has a local context.  -/
Lean.MonadLCtx : (Type → Type) → Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {a : α}, ∅.getKey? a = none
-- Init.Data.List.MinMaxOn
List.minOn_cons_cons_nil : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {a b : α} {f : α → β},
  List.minOn f [a, b] ⋯ = minOn f a b
-- Mathlib.Geometry.Diffeology.Basic
/-- The predicate determining which maps `u → X` with `u : Set (EuclideanSpace ℝ (Fin n))` open
are plots.  -/
DiffeologicalSpace.CorePlotsOn.isPlotOn : {X : Type u_1} →
  DiffeologicalSpace.CorePlotsOn X →
    {n : ℕ} → {u : Set (EuclideanSpace ℝ (Fin n))} → IsOpen u → (EuclideanSpace ℝ (Fin n) → X) → Prop
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₃ : ∀ {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) (i : EInt) {X Y : C} (φ : X ⟶ Y),
  ((t.eTriangleLTGE.obj i).map φ).hom₃ = (t.eTruncGE.obj i).map φ
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.commMon_forget₂_obj_coe : ∀ (M : CommRingCat), ↑(CategoryTheory.HasForget₂.forget₂.obj M) = ↑M
-- Mathlib.Algebra.Group.Basic
sub_add_eq_sub_add_zero_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - (b + c) = a - b + (0 - c)
-- Mathlib.Order.Concept
Concept.intent_iInf : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Concept α β r),
  (⨅ i, f i).intent = upperPolar r (⋂ i, (f i).extent)
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_eq_zero : ∀ {n : ℕ} [inst : NeZero n] {i : Fin (n + 1)} (h : i ≠ Fin.last n), i.castPred h = 0 ↔ i = 0
-- Mathlib.Algebra.Group.WithOne.Defs
/-- The canonical map from `α` into `WithZero α`  -/
WithZero.coe : {α : Type u} → α → WithZero α
-- Aesop.Util.EqualUpToIds
_private.Aesop.Util.EqualUpToIds.0.Aesop.EqualUpToIds.Unsafe.namesEqualUpToMacroScopes : Lean.Name → Lean.Name → Bool
-- Mathlib.Topology.Constructions
Continuous.subtype_val : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop}
  {f : Y → Subtype p}, Continuous f → Continuous fun x => ↑(f x)
-- Mathlib.Order.Sublocale
Sublocale.coe_himp : ∀ {X : Type u_1} [inst : Order.Frame X] {S : Sublocale X} (a b : ↥S), ↑(a ⇨ b) = ↑a ⇨ ↑b
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.getKey?.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a k : α) (v : β k) (l : List ((a : α) × β a)),
  Std.Internal.List.getKey? a (⟨k, v⟩ :: l) = bif k == a then some k else Std.Internal.List.getKey? a l
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.cone_pt : ∀ (P : ProfiniteGrp.{u}), P.cone.pt = P
-- Init.Data.List.MapIdx
_private.Init.Data.List.MapIdx.0.List.mapFinIdx.go.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (as : List α) →
      (motive : (x : List α) → (x_1 : Array β) → x.length + x_1.size = as.length → Sort u_3) →
        (x : List α) →
          (x_1 : Array β) →
            (x_2 : x.length + x_1.size = as.length) →
              ((acc : Array β) → (h : [].length + acc.size = as.length) → motive [] acc h) →
                ((a : α) →
                    (as_1 : List α) →
                      (acc : Array β) → (h : (a :: as_1).length + acc.size = as.length) → motive (a :: as_1) acc h) →
                  motive x x_1 x_2
-- Mathlib.Probability.Distributions.Uniform
PMF.support_uniformOfFinset : ∀ {α : Type u_1} {s : Finset α} (hs : s.Nonempty), (PMF.uniformOfFinset s hs).support = ↑s
-- Mathlib.Dynamics.Ergodic.Ergodic
MeasureTheory.MeasurePreserving.ergodic_conjugate_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : MeasureTheory.Measure α} {β : Type u_2}
  {m' : MeasurableSpace β} {μ' : MeasureTheory.Measure β} {e : α ≃ᵐ β},
  MeasureTheory.MeasurePreserving (⇑e) μ μ' → (Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_eq_zero : ∀ {o : Ordinal.{u_1}}, o.cof = 0 ↔ o = 0
-- Mathlib.Control.LawfulFix
Pi.lawfulFix : {α : Type u_1} → {β : Type u_3} → LawfulFix (α → Part β)
-- Mathlib.Order.Category.CompleteLat
CompleteLat.coe_of : ∀ (α : Type u_1) [inst : CompleteLattice α], ↑{ carrier := α, str := inst } = α
-- Mathlib.Data.Finsupp.Basic
/-- Given `f : α ≃ β`, the finitely supported function spaces are also in bijection:
`(α →₀ M) ≃ (β →₀ M)`.

This is the finitely-supported version of `Equiv.piCongrLeft`.  -/
Finsupp.equivCongrLeft : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [inst : Zero M] → α ≃ β → (α →₀ M) ≃ (β →₀ M)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is unchanged by replacing the third point with the midpoint of the segment
between it and the second point.  -/
EuclideanGeometry.oangle_midpoint_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ p₃ : P), EuclideanGeometry.oangle p₁ p₂ (midpoint ℝ p₃ p₂) = EuclideanGeometry.oangle p₁ p₂ p₃
-- Init.Data.UInt.Lemmas
UInt64.zero_lt_one : 0 < 1
-- Mathlib.Tactic.Simproc.Factors
Mathlib.Meta.Simproc.FactorsHelper.cons : ∀ {n m a : ℕ} (b : ℕ) {l : List ℕ},
  Mathlib.Meta.NormNum.IsNat (b * m) n →
    a.blt b = true →
      Mathlib.Meta.NormNum.IsNat b.minFac b →
        Mathlib.Meta.Simproc.FactorsHelper m b l → Mathlib.Meta.Simproc.FactorsHelper n a (b :: l)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen : ∀ (X : AlgebraicGeometry.Scheme) (r : ↑(X.presheaf.obj (Opposite.op ⊤))),
  (TopologicalSpace.Opens.map X.toSpecΓ.base).obj (PrimeSpectrum.basicOpen r) = X.basicOpen r
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_equiv_top : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {F : Type u_7} [inst_2 : EquivLike F G N]
  [inst_3 : AddEquivClass F G N] (f : F), AddSubgroup.map ↑f ⊤ = ⊤
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.frequently_ae_ne_zero_of_setIntegral_ne_zero : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {t : Set X} {μ : MeasureTheory.Measure X}, ∫ (x : X) in t, f x ∂μ ≠ 0 → ∃ᵐ (x : X) ∂μ.restrict t, f x ≠ 0
-- Mathlib.Order.Hom.Basic
OrderHom.coeFnHom_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β], ⇑OrderHom.coeFnHom = fun f => ⇑f
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- Factorized rational functions are non-zero wherever the exponent is zero.
 -/
Function.FactorizedRational.ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ} {x : 𝕜},
  d x = 0 → (∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u) x ≠ 0
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_top : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F), AddSubmonoid.comap f ⊤ = ⊤
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.hom_ext : ∀ {n : Type u} {S X : AlgebraicGeometry.Scheme} {f g : X ⟶ AlgebraicGeometry.AffineSpace n S},
  CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.AffineSpace n S ↘ S) =
      CategoryTheory.CategoryStruct.comp g (AlgebraicGeometry.AffineSpace n S ↘ S) →
    (∀ (i : n),
        (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f))
            (AlgebraicGeometry.AffineSpace.coord S i) =
          (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop g))
            (AlgebraicGeometry.AffineSpace.coord S i)) →
      f = g
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.antidiagonalTuple_one : ∀ (n : ℕ), List.Nat.antidiagonalTuple 1 n = [![n]]
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the number of elements contained in the given closed range.
 -/
Std.Ric.size : {α : Type u} → [Std.Rxc.HasSize α] → [Std.PRange.Least? α] → Std.Ric α → ℕ
-- Mathlib.Topology.Bases
/-- For every point `x`, the set of `t ∈ s` such that `x ∈ t` is directed downwards.  -/
TopologicalSpace.IsTopologicalBasis.exists_subset_inter : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis s → ∀ t₁ ∈ s, ∀ t₂ ∈ s, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkRegisterSimpAttr : Lean.Linter.MissingDocs.SimpleHandler
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_le_pow_iff_right' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftStrictMono M] {a : M} {m n : ℕ},
  1 < a → (a ^ m ≤ a ^ n ↔ m ≤ n)
-- ProofWidgets.Component.MakeEditLink
/-- The `title` property, if any, to set on the displayed `<a>` link.  -/
ProofWidgets.MakeEditLinkProps.title? : ProofWidgets.MakeEditLinkProps → Option String
-- Mathlib.LinearAlgebra.Dual.Defs
LinearMap.dualCoannihilator_range_eq_ker_flip : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (B : M →ₗ[R] M' →ₗ[R] R), B.range.dualCoannihilator = B.flip.ker
-- Mathlib.RingTheory.Jacobson.Artinian
/-- If `A` is a finite type algebra over an Artinian ring `R`,
then `A` is finite over `R` if and only if `A` is an Artinian ring.  -/
Module.finite_iff_isArtinianRing : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FiniteType R A] [IsArtinianRing R], Module.Finite R A ↔ IsArtinianRing A
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzOnWith.edist_le_mul_of_le : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β},
  LipschitzOnWith K f s → ∀ {x y : α}, x ∈ s → y ∈ s → ∀ {r : ENNReal}, edist x y ≤ r → edist (f x) (f y) ≤ ↑K * r
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.comp : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] (g : Z ⟶ Y)
  [AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion g],
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerivedNatTrans_comp : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF RF' RF'' : CategoryTheory.Functor D H) {F F' F'' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (α'' : F'' ⟶ L.comp RF'') (W : CategoryTheory.MorphismProperty C)
  [inst_3 : L.IsLocalization W] [inst_4 : RF.IsRightDerivedFunctor α W] [inst_5 : RF'.IsRightDerivedFunctor α' W]
  (τ : F ⟶ F') (τ' : F' ⟶ F''),
  CategoryTheory.CategoryStruct.comp (RF.rightDerivedNatTrans RF' α α' W τ)
      (RF'.rightDerivedNatTrans RF'' α' α'' W τ') =
    RF.rightDerivedNatTrans RF'' α α'' W (CategoryTheory.CategoryStruct.comp τ τ')
-- Mathlib.Topology.Connected.PathConnected
pathComponent_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ∈ pathComponent y ↔ y ∈ pathComponent x
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.toIntertwiningMap_refl : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] {ρ : Representation A G V}, ↑(Representation.Equiv.refl ρ) = Representation.IntertwiningMap.id ρ
-- Mathlib.Algebra.Group.Translate
/-- Translation of a function in a group by an element of that group.
`τ a f` is defined as `x ↦ f (x - a)`.  -/
translate.termτ : Lean.ParserDescr
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddZeroClassOfAddMonoidHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → AddZeroClass (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] → AddZeroClass (DirectLimit G f)
-- Mathlib.Topology.Order.NhdsSet
Ioo_mem_nhdsSet_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c d : α},
  a < b → c < d → Set.Ioo a d ∈ nhdsSet (Set.Icc b c)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseMarkerShort : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.HourMarker
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.bipartiteDoubleCover.match_1.congr_eq_3 : ∀ {V : Type u_1} (motive : V ⊕ V → V ⊕ V → Sort u_2) (x x_1 : V ⊕ V)
  (h_1 : (v' w' : V) → motive (Sum.inl v') (Sum.inr w')) (h_2 : (v' w' : V) → motive (Sum.inr v') (Sum.inl w'))
  (h_3 : (x x_2 : V ⊕ V) → motive x x_2) (x_2 x_3 : V ⊕ V),
  x = x_2 →
    x_1 = x_3 →
      (∀ (v' w' : V), x_2 = Sum.inl v' → x_3 = Sum.inr w' → False) →
        (∀ (v' w' : V), x_2 = Sum.inr v' → x_3 = Sum.inl w' → False) →
          (match x, x_1 with
            | Sum.inl v', Sum.inr w' => h_1 v' w'
            | Sum.inr v', Sum.inl w' => h_2 v' w'
            | x, x_6 => h_3 x x_6) ≍
            h_3 x_2 x_3
-- Mathlib.Order.Filter.Cofinite
Filter.hasBasis_cofinite : ∀ {α : Type u_2}, Filter.cofinite.HasBasis (fun s => s.Finite) compl
-- Mathlib.CategoryTheory.Filtered.Basic
/-- A category `IsFiltered` if
1. for every pair of objects there exists another object "to the right",
2. for every pair of parallel morphisms there exists a morphism to the right so the compositions
   are equal, and
3. there exists some object.  -/
CategoryTheory.IsFiltered : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Std.Http.Data.URI.Encoding
Std.Http.URI.EncodedString.instHashable : {r : UInt8 → Bool} → Hashable (Std.Http.URI.EncodedString r)
-- Mathlib.Order.UpperLower.Prod
UpperSet.prod_top : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s : UpperSet α), s ×ˢ ⊤ = ⊤
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs.congr_simp : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] (a a_1 : A), a = a_1 → CFC.abs a = CFC.abs a_1
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
Matrix.gram_eq_conjTranspose_mul : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_5} [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (v : n → E),
  Matrix.gram 𝕜 v =
    (Matrix.of fun i j => (b.repr (v j)).ofLp i).conjTranspose * Matrix.of fun i j => (b.repr (v j)).ofLp i
-- Lean.Meta.Basic
Lean.Meta.mkLetFVars : Array Lean.Expr →
  Lean.Expr →
    optParam Bool true → optParam Bool true → optParam Lean.BinderInfo Lean.BinderInfo.implicit → Lean.MetaM Lean.Expr
-- Init.Data.Array.Lemmas
Array.filter_size_eq_size : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, (Array.filter p xs).size = xs.size ↔ ∀ a ∈ xs, p a = true