mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.NormNum.Irrational
Mathlib.Meta.NormNum.irrational_sqrt_rat_of_num : ∀ {x : ℝ} {num den num_k : ℕ},
  Mathlib.Meta.NormNum.IsNNRat x num den → num.Coprime den → num_k ^ 2 < num → num < (num_k + 1) ^ 2 → Irrational √x
-- Mathlib.Order.Filter.Pointwise
Filter.smul.instNeBot : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {g : Filter β} [f.NeBot] [g.NeBot], (f • g).NeBot
-- Lean.Server.References
/-- Erases all worker references in `self` for the worker managing `name`.  -/
Lean.Server.References.removeWorkerRefs : Lean.Server.References → Lean.Name → Lean.Server.References
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.add : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β]
  [ContinuousAdd β],
  Asymptotics.SuperpolynomialDecay l k f →
    Asymptotics.SuperpolynomialDecay l k g → Asymptotics.SuperpolynomialDecay l k (f + g)
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instSubtractionMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubtractionMonoid α],
  AddOpposite.instSubtractionMonoid =
    { toSubNegMonoid := AddOpposite.instSubNegMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.comp_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_6 : F.OplaxMonoidal]
  [inst_7 : G.OplaxMonoidal] (X Y : C),
  CategoryTheory.Functor.OplaxMonoidal.δ (F.comp G) X Y =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.OplaxMonoidal.δ F X Y))
      (CategoryTheory.Functor.OplaxMonoidal.δ G (F.obj X) (F.obj Y))
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.iff_finite_primesOver : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S], Algebra.QuasiFinite R S ↔ ∀ (I : Ideal R), I.IsPrime → (I.primesOver S).Finite
-- Mathlib.Analysis.Normed.Group.AddTorsor
dist_vadd_left : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (v : V) (x : P), dist (v +ᵥ x) x = ‖v‖
-- Mathlib.Topology.Sets.Compacts
/-- The image of a compact open under a continuous open map.  -/
TopologicalSpace.CompactOpens.map : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        (f : α → β) → Continuous f → IsOpenMap f → TopologicalSpace.CompactOpens α → TopologicalSpace.CompactOpens β
-- Mathlib.FieldTheory.Galois.Infinite
InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (L : IntermediateField k K)
  [IsGalois k K], IsOpen L.fixingSubgroup.carrier ∧ L.fixingSubgroup.Normal ↔ FiniteDimensional k ↥L ∧ IsGalois k ↥L
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply : ∀ {n : ℕ} {K : Type u} [inst : Field K] {ζ : K} [inst_1 : NeZero n] [inst_2 : CharZero K]
  [inst_3 : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) (a : ↥ℤ[ζ]),
  hζ.adjoinEquivRingOfIntegers a = (IsIntegralClosure.lift ℤ (NumberField.RingOfIntegers K) K) a
-- Std.Time.Format
/-- The leanDateTimeWithIdentifierAndNanos format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS'[z]'`
for representing date, time, and time zone. It uses the default value that can be parsed with the
notation of dates.
 -/
Std.Time.Formats.leanDateTimeWithIdentifierAndNanos : Std.Time.GenericFormat Std.Time.Awareness.any
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.eball_disjoint`. -/
EMetric.ball_disjoint : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε₁ ε₂ : ENNReal},
  ε₁ + ε₂ ≤ edist x y → Disjoint (Metric.eball x ε₁) (Metric.eball y ε₂)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_alter_eq_sub_one : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)},
  m.WF → k ∈ m → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size - 1
-- Mathlib.Logic.Equiv.Pairwise
EquivLike.pairwise_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {F : Sort u_3} [inst : EquivLike F Y X] (f : F) (p : X → X → Prop),
  Pairwise (Function.onFun p ⇑f) ↔ Pairwise p
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_mul_of_one_le_left' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α] [MulRightMono α] {a b : α}, 1 ≤ b → a ≤ b * a
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.pred_le_self : ∀ (o : Ordinal.{u_4}), o.pred ≤ o
-- Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
Squarefree.moebius_eq : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
  Squarefree a → UniqueFactorizationMonoid.moebius a = (-1) ^ (UniqueFactorizationMonoid.factors a).card
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.rotateL_lemma₁ : ∀ {a b c : ℕ}, 3 * a ≤ b + c → c ≤ 3 * b → a ≤ 3 * b
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.eval₂_homogenize_of_eq_one : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] {p : Polynomial R} {n : ℕ},
  p.natDegree ≤ n →
    ∀ (f : R →+* S) (g : Fin 2 → S), g 1 = 1 → MvPolynomial.eval₂ f g (p.homogenize n) = Polynomial.eval₂ f (g 0) p
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H0π_comp_map_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.map f φ 0))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.H0π A)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.H0π B)) ((Rep.Hom.hom φ) x)
-- Mathlib.Combinatorics.Configuration
Configuration.HasPoints.lineCount_eq_pointCount : ∀ {P : Type u_1} {L : Type u_2} [inst : Membership P L] [Configuration.HasPoints P L] [inst_2 : Fintype P]
  [inst_3 : Fintype L],
  Fintype.card P = Fintype.card L →
    ∀ {p : P} {l : L}, p ∉ l → Configuration.lineCount L p = Configuration.pointCount P l
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false →
    (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getKeyD k fallback = fallback
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.induction_on_adjoin : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  (P : IntermediateField F E → Prop),
  P ⊥ →
    (∀ (K : IntermediateField F E) (x : E), P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)) →
      ∀ (K : IntermediateField F E), P K
-- Init.Sym.Lemmas
Lean.Sym.UInt16.lt_eq_true : ∀ (a b : UInt16), decide (a < b) = true → (a < b) = True
-- Mathlib.Algebra.Group.Submonoid.BigOperators
AddSubmonoid.coe_multiset_sum : ∀ {M : Type u_4} [inst : AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset ↥S),
  ↑m.sum = (Multiset.map Subtype.val m).sum
-- Mathlib.CategoryTheory.Presentable.StrongGenerator
CategoryTheory.ObjectProperty.IsStrongGenerator.isDense_colimitsCardinalClosure_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.Small.{w, v, u} P],
  P.IsStrongGenerator → P ≤ CategoryTheory.isCardinalPresentable C κ → (P.colimitsCardinalClosure κ).ι.IsDense
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_eq : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α} (h' : k ∈ m), m.getKey k h' = k
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.basicOpen_restrict : ∀ (X : AlgebraicGeometry.Scheme) {V U : X.Opens} (i : V ⟶ U) (f : ↑(X.presheaf.obj (Opposite.op U))),
  X.basicOpen (TopCat.Presheaf.restrict f i) ≤ X.basicOpen f
-- Mathlib.Algebra.DirectSum.Basic
/-- `toAddMonoid φ` is the natural homomorphism from `⨁ i, β i` to `γ`
induced by a family `φ` of homomorphisms `β i → γ`.  -/
DirectSum.toAddMonoid : {ι : Type v} →
  {β : ι → Type w} →
    [inst : (i : ι) → AddCommMonoid (β i)] →
      [DecidableEq ι] →
        {γ : Type u₁} → [inst_2 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (DirectSum ι fun i => β i) →+ γ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.eq_append_of_dropPrefix?_prop_eq_some : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {res : String.Slice},
  s.dropPrefix? P = some res → ∃ c, s = String.singleton c ++ res.copy ∧ P c
-- Mathlib.Data.Sigma.Order
/-- The lexicographical linear order on a sigma type.  -/
Sigma.Lex.boundedOrder : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : PartialOrder ι] →
      [inst_1 : BoundedOrder ι] →
        [inst_2 : (i : ι) → Preorder (α i)] → [OrderBot (α ⊥)] → [OrderTop (α ⊤)] → BoundedOrder (Σₗ (i : ι), α i)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.instHasFiniteCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  CategoryTheory.Limits.HasFiniteCoproducts C
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.trace_omega : ∀ {R : Type u_2} {a b : R} [inst : CommRing R], QuadraticAlgebra.trace QuadraticAlgebra.omega = b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.DTreeMap.Const.insertMany t l).getKey? k' = some k
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The complex moment-generating function of a Gaussian distribution with mean `μ` and variance `v`
is given by `z ↦ exp (z * μ + v * z ^ 2 / 2)`.  -/
ProbabilityTheory.complexMGF_id_gaussianReal : ∀ {μ : ℝ} {v : NNReal} (z : ℂ),
  ProbabilityTheory.complexMGF id (ProbabilityTheory.gaussianReal μ v) z = Complex.exp (z * ↑μ + ↑↑v * z ^ 2 / 2)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, local version for any measure.

Let filters `l` and `l'` be related by `[intervalIntegral.FTCFilter a l l']`; let `μ` be a locally
finite measure.  If `f` has a finite limit `c` at `l' ⊓ ae μ`, then
`∫ x in u..v, f x ∂μ = μ (Ioc u v) • c + o(μ(Ioc u v))` as both `u` and `v` tend to `l`.

See also `measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le'` for a version that also works,
e.g., for `l = l' = Filter.atTop`.  -/
intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {c : E}
  {l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ]
  [CompleteSpace E] [intervalIntegral.FTCFilter a l l'],
  StronglyMeasurableAtFilter f l' μ →
    Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (nhds c) →
      Filter.Tendsto u lt l →
        Filter.Tendsto v lt l →
          u ≤ᶠ[lt] v →
            (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - μ.real (Set.Ioc (u t) (v t)) • c) =o[lt] fun t =>
              μ.real (Set.Ioc (u t) (v t))
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.inv_functor : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  [inst_2 : Φ.functor.IsEquivalence] [inst_3 : Φ.IsInduced] [inst_4 : W₂.RespectsIso], Φ.inv.functor = Φ.functor.inv
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.freeOn.eq_1 : ∀ {α : Type u_1} (E : Set α), Matroid.freeOn E = (Matroid.loopyOn E)✶
-- Std.Data.DTreeMap.Internal.Cell
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Cell.ofOption : {α : Type u} → {β : α → Type v} → [inst : Ord α] → (k : α) → Option (β k) → Std.DTreeMap.Internal.Cell α β (compare k)
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.I_isPrime : ∀ {P : Type u_1} [inst : Preorder P] (IF : Order.Ideal.PrimePair P), IF.I.IsPrime
-- Mathlib.Data.ENat.Basic
ENat.WithBot.add_le_add_one_left_iff : ∀ {a b : WithBot ℕ∞}, 1 + a ≤ 1 + b ↔ a ≤ b
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.isOrdered_iff' : ∀ {α : Type u_1} {cmp : α → α → Ordering} {L R : Option α} [Std.TransCmp cmp] {t : RBTree.RBNode α},
  RBTree.RBNode.isOrdered cmp t L R = true ↔
    (∀ a ∈ L, RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp a x) t) ∧
      (∀ a ∈ R, RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp x a) t) ∧
        (∀ a ∈ L, ∀ b ∈ R, RBTree.RBNode.cmpLT cmp a b) ∧ RBTree.RBNode.Ordered cmp t
-- Mathlib.Util.LongNames
/-- Lists all declarations with a long name, gathered according to the module they are defined in.
Use as `#long_names` or `#long_names 100` to specify the length.
 -/
«command#long_names_» : Lean.ParserDescr
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
IsStronglyTranscendental.iff_of_isLocalization : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] {M : Submonoid S},
  M ≤ nonZeroDivisors S →
    ∀ [IsLocalization M T] [IsScalarTower R S T] {x : S},
      IsStronglyTranscendental R ((algebraMap S T) x) ↔ IsStronglyTranscendental R x
-- Mathlib.Algebra.Category.CommBialgCat
/-- The type of morphisms in `CommBialgCat R`.  -/
CommBialgCat.Hom : {R : Type u} → [inst : CommRing R] → CommBialgCat R → CommBialgCat R → Type v
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft : ∀ {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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {x y : D} (f : x ≅ y) (z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f.hom z)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f.inv z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x z)
-- Mathlib.RingTheory.Ideal.Maps
RingHom.liftOfRightInverse_comp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Ring A] [inst_1 : Ring B] [inst_2 : Ring C] (f : A →+* B)
  (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : { g // RingHom.ker f ≤ RingHom.ker g }),
  ((f.liftOfRightInverse f_inv hf) g).comp f = ↑g
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extMk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y)
  [inst_3 : HasDerivedCategory C] {n : ℕ} (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m)
  (hf : CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0),
  (R.extMk f m hm hf).hom =
    (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((CategoryTheory.ShiftedHom.map
            (CochainComplex.HomComplex.Cocycle.equivHomShift.symm
              (CochainComplex.HomComplex.Cocycle.fromSingleMk
                (CategoryTheory.CategoryStruct.comp f (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (CategoryTheory.ShiftedHom.mk₀ 0 ⋯
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (DerivedCategory.Q.map R.ι'))
            ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)))
        ⋯)
      ⋯
-- Mathlib.CategoryTheory.Action.Concrete
/-- We have `Fin 1 → G ≅ G` as `G`-sets, with `G` acting by left multiplication.  -/
Action.diagonalOneIsoLeftRegular : (G : Type u_1) → [inst : Monoid G] → Action.diagonal G 1 ≅ Action.leftRegular G
-- Init.Data.Int.Order
Int.le_iff_lt_or_eq : ∀ {a b : ℤ}, a ≤ b ↔ a < b ∨ a = b
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.instIsIsoComp : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.IsIso] [G.IsIso], (F.comp G).IsIso
-- Mathlib.CategoryTheory.Idempotents.SimplicialObject
CategoryTheory.Idempotents.instIsIdempotentCompleteCosimplicialObject : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsIdempotentComplete C],
  CategoryTheory.IsIdempotentComplete (CategoryTheory.CosimplicialObject C)
-- Lean.Elab.AutoBound
Lean.Elab.AutoBoundImplicitContext.mk : Bool → Lean.PArray Lean.Expr → Lean.Elab.AutoBoundImplicitContext
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
/-- A finite Z-group has cyclic commutator subgroup.  -/
IsZGroup.isCyclic_commutator : ∀ (G : Type u_1) [inst : Group G] [Finite G] [IsZGroup G], IsCyclic ↥(commutator G)
-- Mathlib.Combinatorics.Graph.Maps
/-- Map `G : Graph α β` to a `Graph α' β` with the same edge set by applying a function `f : α → α'`
to each vertex. Edges between identified vertices become loops.  -/
Graph.map : {α : Type u_1} → {α' : Type u_2} → {β : Type u_4} → (α → α') → Graph α β → Graph α' β
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- Evidence that the arbitrary choice of cone provided by `limit.cone F` is a limit cone.  -/
CategoryTheory.Limits.limit.isLimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.limit.cone F)
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.compMultilinearMap_add : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃] (g : M₂ →ₗ[R] M₃)
  (f₁ f₂ : MultilinearMap R M₁ M₂), g.compMultilinearMap (f₁ + f₂) = g.compMultilinearMap f₁ + g.compMultilinearMap f₂
-- Init.Data.Vector.Zip
Vector.zipWith_replicate : ∀ {α : Type u_1} {β : Type u_2} {α_1 : Type u_3} {f : α → β → α_1} {a : α} {b : β} {n : ℕ},
  Vector.zipWith f (Vector.replicate n a) (Vector.replicate n b) = Vector.replicate n (f a b)
-- Mathlib.Order.Filter.Basic
Filter.Eventually.ne_of_gt : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {f g : α → β},
  (∀ᶠ (x : α) in l, g x < f x) → ∀ᶠ (x : α) in l, f x ≠ g x
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.conjugate' : ∀ {R : Type u_1} [inst : Semigroup R] [inst_1 : StarMul R] {x : R},
  IsSelfAdjoint x → ∀ (z : R), IsSelfAdjoint (star z * x * z)
-- Init.Data.BitVec.Lemmas
BitVec.ushiftRight_and_distrib : ∀ {w : ℕ} (x y : BitVec w) (n : ℕ), (x &&& y) >>> n = x >>> n &&& y >>> n
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_eq_toReal_iff' : ∀ {x y : ENNReal}, x ≠ ⊤ → y ≠ ⊤ → (x.toReal = y.toReal ↔ x = y)
-- Init.Data.List.Control
List.zipWithM.loop : {m : Type u → Type v} →
  [Monad m] → {α : Type w} → {β : Type x} → {γ : Type u} → (α → β → m γ) → List α → List β → Array γ → m (List γ)
-- Mathlib.RingTheory.GradedAlgebra.Basic
/-- The ring homomorphism `GradedRing.projZeroRingHom' 𝒜` is surjective.  -/
GradedRing.projZeroRingHom'_surjective : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜], Function.Surjective ⇑(GradedRing.projZeroRingHom' 𝒜)
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
factorPowSucc.isUnit_of_isUnit_image : ∀ {R : Type u_3} [inst : CommRing R] {I : Ideal R} {n : ℕ},
  n > 0 → ∀ {a : R ⧸ I ^ (n + 1)}, IsUnit ((Ideal.Quotient.factorPow I ⋯) a) → IsUnit a
-- Mathlib.Order.Filter.Interval
Filter.tendstoIxxClass_principal : ∀ {α : Type u_1} {s t : Set α} {Ixx : α → α → Set α},
  Filter.TendstoIxxClass Ixx (Filter.principal s) (Filter.principal t) ↔ ∀ x ∈ s, ∀ y ∈ s, Ixx x y ⊆ t
-- Init.Prelude
/-- Gadget for optional parameter support.

A binder like `(x : α := default)` in a declaration is syntax sugar for
`x : optParam α default`, and triggers the elaborator to attempt to use
`default` to supply the argument if it is not supplied.
 -/
optParam : (α : Sort u) → α → Sort u
-- Mathlib.Data.Num.Basic
ZNum.decidableLT : DecidableLT ZNum
-- Init.Data.Array.Subarray
/-- The stopping index is no later than the end of the array.

The ending index is exclusive. If it is equal to the size of the array, then the last element of
the array is in the subarray.
 -/
Std.Slice.Internal.SubarrayData.stop_le_array_size : ∀ {α : Type u} (self : Std.Slice.Internal.SubarrayData α), self.stop ≤ self.array.size
-- Mathlib.Analysis.Analytic.Order
/-- An analytic function `f` has finite analytic order `n` at `z₀` if and only if its first
`n` iterated derivatives (including `f` itself) vanish at `z₀` and the `n`-th iterated derivative is
non-zero.  -/
analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CharZero 𝕜] [CompleteSpace E] {z₀ : 𝕜} {f : 𝕜 → E},
  AnalyticAt 𝕜 f z₀ →
    ∀ {n : ℕ}, analyticOrderAt f z₀ = ↑n ↔ (∀ k < n, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv n f z₀ ≠ 0
-- Mathlib.CategoryTheory.Sites.Localization
CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  (A : Type u_2) [inst_1 : CategoryTheory.Category.{v_2, u_2} A] [inst_2 : CategoryTheory.HasWeakSheafify J A],
  J.W =
    (CategoryTheory.MorphismProperty.isomorphisms (CategoryTheory.Sheaf J A)).inverseImage
      (CategoryTheory.presheafToSheaf J A)
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.mul_sum_of_mem : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R},
  OrthogonalIdempotents e → ∀ {i : I} {s : Finset I}, i ∈ s → e i * ∑ j ∈ s, e j = e i
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIso : ∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  {Q : CompHausLike P} {Z : Type (max u w)} (r : LocallyConstant (↑Q.toTop) Z) (a : Function.Fiber ⇑r)
  [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P]
  (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))),
  CategoryTheory.CategoryStruct.comp (X.mapIso (CompHausLike.LocallyConstant.sigmaIso r).op).hom
      (CategoryTheory.CategoryStruct.comp
        (CompHausLike.sigmaComparison X fun a => ↑(CompHausLike.LocallyConstant.fiber r a).toTop)
        (TypeCat.ofHom fun g => g a)) =
    X.map (CompHausLike.LocallyConstant.sigmaIncl r a).op