mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
/-- Bowen-Dinaburg's definition of topological entropy using nets is
`⨆ U ∈ 𝓤 X, netEntropyEntourage T F U`. This quantity is the same as the topological entropy using
covers, so there is no need to define a new notion of topological entropy. This version of the
theorem relates the `limsup` versions of topological entropy.  -/
Dynamics.coverEntropy_eq_iSup_netEntropyEntourage : ∀ {X : Type u_1} [inst : UniformSpace X] (T : X → X) (F : Set X),
  Dynamics.coverEntropy T F = ⨆ U ∈ uniformity X, Dynamics.netEntropyEntourage T F U
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.pullbackObjFreeIso_hom_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_5 : CategoryTheory.HasWeakSheafify K AddCommGrpCat] [inst_6 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_7 : K.WEqualsLocallyBijective AddCommGrpCat] [inst_8 : F.Final] {I J_1 : Type u} (f : I → J_1),
  CategoryTheory.CategoryStruct.comp ((SheafOfModules.pullback φ).map (SheafOfModules.freeMap f))
      (SheafOfModules.pullbackObjFreeIso φ J_1).hom =
    CategoryTheory.CategoryStruct.comp (SheafOfModules.pullbackObjFreeIso φ I).hom (SheafOfModules.freeMap f)
-- Mathlib.Analysis.Convex.Independent
/-- The range of an injective indexed family of points is convex independent iff that family is.  -/
Function.Injective.convexIndependent_iff_set : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {p : ι → E}, Function.Injective p → (ConvexIndependent 𝕜 Subtype.val ↔ ConvexIndependent 𝕜 p)
-- Mathlib.Algebra.Order.Group.Abs
abs_le : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G},
  |a| ≤ b ↔ -b ≤ a ∧ a ≤ b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyLTD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.Equiv t₂ → t₁.getKeyLTD k fallback = t₂.getKeyLTD k fallback
-- Mathlib.Tactic.DeriveCountable
/-- Assuming all of the auxiliary definitions exist, create all the `instance` commands
for the `ToExpr` instances for the (mutual) inductive type(s).  -/
_private.Mathlib.Tactic.DeriveCountable.0.Mathlib.Deriving.Countable.mkCountableInstanceCmds : Lean.Elab.Deriving.Context → Array Lean.Name → Lean.Elab.TermElabM (Array Lean.Command)
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- The action `Gᵐᵒᵖ ↷ G` by right translations is proper.  -/
instProperSMulMulOppositeOfIsTopologicalGroup : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G], ProperSMul Gᵐᵒᵖ G
-- Mathlib.Data.Set.Opposite
Set.unop_op : ∀ {α : Type u_1} (s : Set αᵒᵖ), s.unop.op = s
-- Init.Data.Range.Polymorphic.BitVec
BitVec.succ?_eq_none : ∀ {n : ℕ} {x : BitVec n}, Std.PRange.succ? x = none ↔ x.toNat = 2 ^ n - 1
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.ε_add : ∀ {I : Type u_7} [inst : AddMonoid I] (c : ComplexShape I) [inst_1 : c.TensorSigns] (p q : I),
  c.ε (p + q) = c.ε p * c.ε q
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_union_eq_left_of_forall₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {s t : Set X} {μ : MeasureTheory.Measure X} {f : X → E},
  MeasureTheory.NullMeasurableSet t μ → (∀ x ∈ t, f x = 0) → ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles._auto_1),
  (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).g = X.pOpcycles f g n₁
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
isStationary_iUnion_iff_of_orderTop : ∀ {α : Type v} [inst : LinearOrder α] [OrderTop α] {ι : Sort u_1} {f : ι → Set α},
  IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- If a category has wide pullbacks on a higher universe level it also has wide pullbacks
on a lower universe level.  -/
CategoryTheory.Limits.hasWidePullbacks_shrink : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWidePullbacks C],
  CategoryTheory.Limits.HasWidePullbacks C
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instLawfulSingleton : LawfulSingleton ZFSet.{u_1} ZFSet.{u_1}
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k},
  t.WF → (Std.DTreeMap.Raw.map f t).getD k fallback = (Option.map (f k) (t.get? k)).getD fallback
-- Mathlib.Order.Hom.WithTopBot
InfHom.withTop'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] [inst_2 : OrderTop β]
  (f : InfHom α β), f.withTop' = { toFun := fun a => Option.elim a ⊤ ⇑f, map_inf' := ⋯, map_top' := ⋯ }
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr.inverse_map_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  {X Y : CategoryTheory.Sheaf K A} (f : X ⟶ Y) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongr.inverse J K e A).map f).hom.app X_1 =
    f.hom.app (Opposite.op (e.functor.obj (Opposite.unop X_1)))
-- Init.Data.Array.Lemmas
Array.getElem_of_getElem? : ∀ {α : Type u_1} {i : ℕ} {a : α} {xs : Array α}, xs[i]? = some a → ∃ (h : i < xs.size), xs[i] = a
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.exteriorPower.iso₁_hom_naturality : ∀ {R : Type u} [inst : CommRing R] {M N : ModuleCat R} (f : M ⟶ N),
  CategoryTheory.CategoryStruct.comp (ModuleCat.exteriorPower.map f 1) (ModuleCat.exteriorPower.iso₁ N).hom =
    CategoryTheory.CategoryStruct.comp (ModuleCat.exteriorPower.iso₁ M).hom f
-- Mathlib.Data.ENat.Basic
ENat.recTopCoe_ofNat : ∀ {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a) (x : ℕ) [inst : x.AtLeastTwo],
  ENat.recTopCoe d f (OfNat.ofNat x) = f (OfNat.ofNat x)
-- Mathlib.Algebra.Category.ModuleCat.Basic
_private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk.inj : ∀ {R : Type u} {inst : Ring R} {M N : ModuleCat R} {hom' hom'_1 : ↑M →ₗ[R] ↑N},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Data.Fintype.Basic
PSigma.fintypePropProp : {α : Prop} → {β : α → Prop} → [Decidable α] → [(a : α) → Decidable (β a)] → Fintype ((a : α) ×' β a)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.standardσ.eq_1 : ∀ {m₁ m₂ : ℕ} (h_2 : m₂ + [].length = m₁), SimplexCategoryGenRel.standardσ [] h_2 = CategoryTheory.eqToHom ⋯
-- Mathlib.Analysis.Calculus.Deriv.Linear
LinearMap.hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →ₗ[𝕜] F), HasDerivAt (⇑e) (e 1) x
-- Mathlib.LinearAlgebra.Finsupp.Defs
Module.End.ringHomEndFinsupp_surjective : ∀ (ι : Type u_4) (R : Type u_5) (M : Type u_6) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.Surjective ⇑(Module.End.ringHomEndFinsupp ι)
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.degree_smul_le_of_le : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : SMulZeroClass S R] {n : ℕ} {a : S} {f : Polynomial R},
  f.degree ≤ ↑n → (a • f).degree ≤ ↑n
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_ofNatLT : ∀ {n : ℕ} (hn : n < UInt64.size), (UInt64.ofNatLT n hn).toBitVec = n#'hn
-- Mathlib.RingTheory.Finiteness.Cardinality
AddSubgroup.fg_iff_exists_fin_addMonoidHom : ∀ {M : Type u_3} [inst : AddCommGroup M] {H : AddSubgroup M}, H.FG ↔ ∃ n f, f.range = H
-- Mathlib.Order.Birkhoff
/-- **Birkhoff's Representation Theorem**. Any finite distributive lattice can be embedded in a
powerset lattice.  -/
OrderEmbedding.birkhoffSet : {α : Type u_1} → [inst : DistribLattice α] → [Fintype α] → [DecidablePred SupIrred] → α ↪o Set { a // SupIrred a }
-- Std.Internal.Do.Order.Basic
/-- Pointwise characterization of binary meet on function lattices.  -/
Lean.Order.meet_apply : ∀ {σ : Type v} {β : σ → Type w} [inst : (s : σ) → Lean.Order.CompleteLattice (β s)] (a b : (s : σ) → β s) (s : σ),
  Lean.Order.meet a b s = Lean.Order.meet (a s) (b s)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- The conjugate of a complex embedding as a complex embedding.  -/
NumberField.ComplexEmbedding.conjugate : {K : Type u_1} → [inst : Field K] → (K →+* ℂ) → K →+* ℂ
-- Mathlib.Data.Multiset.Sections
/-- The sections of a multiset of multisets `s` consists of all those multisets
which can be put in bijection with `s`, so each element is a member of the corresponding multiset.
 -/
Multiset.Sections : {α : Type u_1} → Multiset (Multiset α) → Multiset (Multiset α)
-- Mathlib.Geometry.Euclidean.Inversion.Basic
Filter.Tendsto.inversion : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {α : Type u_3} {x c : P} {R : ℝ} {l : Filter α} {fc fx : α → P} {fR : α → ℝ},
  Filter.Tendsto fc l (nhds c) →
    Filter.Tendsto fR l (nhds R) →
      Filter.Tendsto fx l (nhds x) →
        x ≠ c →
          Filter.Tendsto (fun a => EuclideanGeometry.inversion (fc a) (fR a) (fx a)) l
            (nhds (EuclideanGeometry.inversion c R x))
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.map_apply_dp : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_4)
  [inst_3 : CommSemiring S] {N : Type u_5} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : Module S N]
  (f : M →ₗ[R] N) [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S N] {n : ℕ} {a : M},
  (DividedPowerAlgebra.map S f) (DividedPowerAlgebra.dp R n a) = DividedPowerAlgebra.dp S n (f a)
-- Init.Data.BitVec.Lemmas
BitVec.usubOverflow.eq_1 : ∀ {w : ℕ} (x y : BitVec w), x.usubOverflow y = decide (x.toNat < y.toNat)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerYield_flatMap_pure : ∀ {α β α₂ γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] {f : β → Std.Iter γ}
  {it₁ : Std.Iter β} {it₂ it₂' : Std.Iter γ} {b : γ},
  it₂.IsPlausibleStep (Std.IterStep.yield it₂' b) →
    (Std.Iter.flatMapAfter f it₁ (some it₂)).IsPlausibleStep
      (Std.IterStep.yield (Std.Iter.flatMapAfter f it₁ (some it₂')) b)
-- Mathlib.Order.Filter.Pointwise
Filter.le_vsub_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f g : Filter β} {h : Filter α},
  h ≤ f -ᵥ g ↔ ∀ ⦃s : Set β⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s -ᵥ t ∈ h
-- Init.Data.SInt.Basic
/-- The largest number that `ISize` can represent: `2^(System.Platform.numBits - 1) - 1`.  -/
ISize.maxValue : ISize
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.v₀₁.τ₁ (CategoryTheory.CategoryStruct.comp S.v₁₂.τ₁ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
/-- A proper pairing is regular when the ancestrality relation
is well founded.  -/
SSet.Subcomplex.Pairing.IsRegular : {X : SSet} → {A : X.Subcomplex} → A.Pairing → Prop
-- Mathlib.Analysis.Convolution
MeasureTheory.Integrable.ae_convolution_exists : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ ν : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] [MeasureTheory.SFinite ν],
  MeasureTheory.Integrable f ν →
    MeasureTheory.Integrable g μ → ∀ᵐ (x : G) ∂μ, MeasureTheory.ConvolutionExistsAt f g x L ν
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasKernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).inv
      (F.map (CategoryTheory.Abelian.factorThruCoimage f)) =
    CategoryTheory.Abelian.factorThruCoimage (F.map f)
-- Mathlib.Analysis.Meromorphic.Basic
AnalyticOnNhd.meromorphicOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, AnalyticOnNhd 𝕜 f U → MeromorphicOn f U
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_unitOfList_le : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α}, (Std.TreeMap.unitOfList l cmp).size ≤ l.length
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.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.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.isLocalHom_singleZeroRingHom : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddMonoid M],
  IsLocalHom AddMonoidAlgebra.singleZeroRingHom
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.IsMaximal.mem_or_not_mem : ∀ {L : FirstOrder.Language} {T : L.Theory},
  T.IsMaximal → ∀ (φ : L.Sentence), φ ∈ T ∨ FirstOrder.Language.Formula.not φ ∈ T
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.rightKanExtensionUnique_hom : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] (F'' : CategoryTheory.Functor D H) (α' : L.comp F'' ⟶ F)
  [inst_4 : F''.IsRightKanExtension α'],
  (F'.rightKanExtensionUnique α F'' α').hom = F''.liftOfIsRightKanExtension α' F' α
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.canonicalEquiv_self : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P], FractionalIdeal.canonicalEquiv S P P = RingEquiv.refl (FractionalIdeal S P)
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `fallback` if no such pair exists.
 -/
Std.ExtTreeMap.getEntryGTD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → α × β → α × β
-- Mathlib.Order.Cover
WCovBy.wcovBy_iff_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⩿ b → (b ⩿ a ↔ b ≤ a)
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.visitLevel : Lean.Level → Lean.MetavarContext.LevelMVarToParam.M Lean.Level
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Init.Data.List.Range
List.getLast_range : ∀ {n : ℕ} (h : List.range n ≠ []), (List.range n).getLast h = n - 1
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.mapTermRel_id_id_id : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n),
  FirstOrder.Language.BoundedFormula.mapTermRel (fun x => id) (fun x => id) (fun x => id) φ = φ
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.ker_mk' : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal], (QuotientAddGroup.mk' N).ker = N
-- Mathlib.ModelTheory.LanguageMap
/-- A language homomorphism is injective when all the maps between symbol types are.  -/
FirstOrder.Language.LHom.Injective : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → (L →ᴸ L') → Prop
-- Mathlib.RingTheory.AdicCompletion.Topology
RingSubgroupsBasis.toRingFilterBasis.eq_1 : ∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] [inst_1 : Nonempty ι] {B : ι → AddSubgroup A}
  (hB : RingSubgroupsBasis B),
  hB.toRingFilterBasis =
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := ⋯, inter_sets := ⋯, zero' := ⋯, add' := ⋯, neg' := ⋯, conj' := ⋯,
      mul' := ⋯, mul_left' := ⋯, mul_right' := ⋯ }
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.Grpd.free_map : ∀ {C D : CategoryTheory.Cat} (F : C ⟶ D), CategoryTheory.Grpd.free.map F = CategoryTheory.FreeGroupoid.map F.toFunctor
-- Lean.Compiler.LCNF.PublicDeclsExt
Lean.Compiler.LCNF.isDeclPublic : Lean.Environment → Lean.Name → Bool
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.coeff_zero_apply : ∀ (b e : Ordinal.{u_1}), (Ordinal.CNF.coeff b 0) e = 0
-- Mathlib.MeasureTheory.Function.Floor
measurable_fract : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [inst_3 : TopologicalSpace R]
  [OrderTopology R] [inst_5 : MeasurableSpace R] [IsStrictOrderedRing R] [BorelSpace R], Measurable Int.fract
-- Mathlib.Algebra.Order.Module.Defs
/-- **Alias** of `le_of_smul_le_smul_right`. -/
le_of_smul_le_smul_of_pos_right : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero β] [SMulPosReflectLE α β], a₁ • b ≤ a₂ • b → 0 < b → a₁ ≤ a₂
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.π_comp_cokernelIsoOfEq_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasCokernel g]
  (h : f = g) {Z : C} (h_1 : CategoryTheory.Limits.cokernel g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelIsoOfEq h).hom h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g) h_1
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_biSup : ∀ {α : Type u_1} (u : α → ℕ → EReal) {s : Set α},
  s.Finite → LinearGrowth.linearGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, LinearGrowth.linearGrowthSup (u x)
-- Mathlib.GroupTheory.Frattini
/-- The Frattini subgroup is characteristic.  -/
frattini_characteristic : ∀ {G : Type u_1} [inst : Group G], (frattini G).Characteristic
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is a commutative division monoid under pointwise operations if `α` is.  -/
Finset.divisionCommMonoid : {α : Type u_2} → [DecidableEq α] → [DivisionCommMonoid α] → DivisionCommMonoid (Finset α)
-- Mathlib.Algebra.Order.Interval.Basic
instNegInterval.eq_1 : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α],
  instNegInterval = { neg := WithBot.map Neg.neg }
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.drop.hcongr_6 : ∀ (V V' : Type u),
  V = V' →
    ∀ (G : SimpleGraph V) (G' : SimpleGraph V'),
      G ≍ G' →
        ∀ (u : V) (u' : V'),
          u ≍ u' →
            ∀ (v : V) (v' : V'),
              v ≍ v' → ∀ (p : G.Walk u v) (p' : G'.Walk u' v'), p ≍ p' → ∀ (n n' : ℕ), n = n' → p.drop n ≍ p'.drop n'
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- The property that links the quotient and remainder functions.
This allows us to compute GCDs and LCMs.  -/
EuclideanDomain.quotient_mul_add_remainder_eq : ∀ {R : Type u} [self : EuclideanDomain R] (a b : R),
  b * EuclideanDomain.quotient a b + EuclideanDomain.remainder a b = a
-- Mathlib.RingTheory.Ideal.Quotient.Index
Ideal.index_pow_le : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} (s : Finset R),
  Ideal.span ↑s = I →
    ∀ [Finite (R ⧸ I)] (n : ℕ),
      (Submodule.toAddSubgroup (I ^ n)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i
-- Mathlib.Algebra.Module.BigOperators
Multiset.sum_smul : ∀ {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {l : Multiset R}
  {x : M}, l.sum • x = (Multiset.map (fun r => r • x) l).sum
-- Mathlib.Order.Max
IsMax.snd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMax x → IsMax x.2
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Finset.mulIndicator_biUnion : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [inst : CommMonoid β] (s : Finset ι) (t : ι → Set κ) {f : κ → β},
  (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a => ∏ i ∈ s, (t i).mulIndicator f a
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comap_mono : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), Monotone fun x => x.comap f
-- Mathlib.FieldTheory.ChevalleyWarning
/-- The **Chevalley–Warning theorem**, `Fintype` version.
Let `(f i)` be a finite family of multivariate polynomials
in finitely many variables (`X s`, `s : σ`) over a finite field of characteristic `p`.
Assume that the sum of the total degrees of the `f i` is less than the cardinality of `σ`.
Then the number of common solutions of the `f i` is divisible by `p`.  -/
char_dvd_card_solutions_of_fintype_sum_lt : ∀ {K : Type u_1} {σ : Type u_2} {ι : Type u_3} [inst : Fintype K] [inst_1 : Field K] [inst_2 : Fintype σ]
  [inst_3 : DecidableEq σ] [inst_4 : DecidableEq K] (p : ℕ) [CharP K p] [inst_6 : Fintype ι] {f : ι → MvPolynomial σ K},
  ∑ i, (f i).totalDegree < Fintype.card σ → p ∣ Fintype.card { x // ∀ (i : ι), (MvPolynomial.eval x) (f i) = 0 }
-- Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Complex.digamma_def : Complex.digamma = logDeriv Complex.Gamma
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.zeroRootSubalgebra_normalizer_eq_self : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H],
  (LieAlgebra.zeroRootSubalgebra R L H).normalizer = LieAlgebra.zeroRootSubalgebra R L H