mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toOuterMeasure_apply_singleton : ∀ {α : Type u_1} (p : PMF α) (a : α), p.toOuterMeasure {a} = p a
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `DifferentiableWithinAt.inv` -/
DifferentiableWithinAt.fun_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_5} [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R] {h : E → R}
  {z : E} {S : Set E}, DifferentiableWithinAt 𝕜 h S z → h z ≠ 0 → DifferentiableWithinAt 𝕜 (fun i => (h i)⁻¹) S z
-- Lean.Parser.Command
Lean.Parser.Command.print.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.FiniteAtFilter.prod : ∀ {X : Type u_4} {Y : Type u_5} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {m' : MeasurableSpace Y}
  {ν : MeasureTheory.Measure Y} {l : Filter X} {l' : Filter Y},
  μ.FiniteAtFilter l → ν.FiniteAtFilter l' → (μ.prod ν).FiniteAtFilter (l ×ˢ l')
-- Plausible.Random
/-- A monad transformer to generate random objects using the generator type `StdGen`.
`RandT m α` should be thought of a random value in `m α`.  -/
Plausible.RandT : (Type u_1 → Type u_2) → Type u_1 → Type (max u_1 u_2)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] {g c : Equiv.Perm α} {s : Finset α}
  (hg : ∀ (x : α), g x ∈ s ↔ x ∈ s) (hc : c.support ⊆ s) (n : ℤ),
  c ^ n = Equiv.Perm.ofSubtype (g.subtypePerm hg) ↔ c.subtypePerm ⋯ ^ n = g.subtypePerm hg
-- Init.ShareCommon
ShareCommon.StateFactory : Type
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.mk.injEq : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (toSubmodule : Submodule A L)
  (lie_mem' : ∀ {a b : L}, a ∈ toSubmodule.carrier → b ∈ toSubmodule.carrier → ⁅a, b⁆ ∈ toSubmodule.carrier)
  (toSubmodule_1 : Submodule A L)
  (lie_mem'_1 : ∀ {a b : L}, a ∈ toSubmodule_1.carrier → b ∈ toSubmodule_1.carrier → ⁅a, b⁆ ∈ toSubmodule_1.carrier),
  ({ toSubmodule := toSubmodule, lie_mem' := lie_mem' } = { toSubmodule := toSubmodule_1, lie_mem' := lie_mem'_1 }) =
    (toSubmodule = toSubmodule_1)
-- Mathlib.Data.UInt
UInt8.toBitVec_injective : Function.Injective UInt8.toBitVec
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.DTreeMap.Raw.Const.entryAtIdx? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → ℕ → Option (α × β)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_mul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A) (x y : ↥S), ↑(x * y) = ↑x * ↑y
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Measure.integrable_measure_prodMk_left : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)},
  MeasurableSet s → (μ.prod ν) s ≠ ⊤ → MeasureTheory.Integrable (fun x => ν.real (Prod.mk x ⁻¹' s)) μ
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.isPlausibleOutput_iff : ∀ {α : Type u} {a : α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  {it : Std.Iter α}, it.IsPlausibleOutput a ↔ it.internalState.next = some a ∧ a ≤ it.internalState.upperBound
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.ExactPairing.coevaluation_evaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.ExactPairing X Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (η_ X Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Y).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ X Y) Y)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv
-- Mathlib.Data.ENNReal.Basic
ENNReal.instOrderBot : OrderBot ENNReal
-- Mathlib.Order.Monotone.Monovary
Monovary.monovaryOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  Monovary f g → ∀ (s : Set ι), MonovaryOn f g s
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- **Alias** of `RingEquiv.symm_apply_apply`. -/
MvPolynomial.iterToSum_sumToIter : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S) (x : R),
  e.symm (e x) = x
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K K' : ChainComplex C ℕ} {L L' : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L)
  (h' : CochainComplex.ConnectData K' L') (fK : K ⟶ K') (fL : L ⟶ L')
  (f_comm : CategoryTheory.CategoryStruct.comp (fK.f 0) h'.d₀ = CategoryTheory.CategoryStruct.comp h.d₀ (fL.f 0))
  (x : ℤ),
  (h.map h' fK fL f_comm).f x =
    match x with
    | Int.ofNat n => fL.f n
    | Int.negSucc n => fK.f n
-- Mathlib.CategoryTheory.Galois.Basic
/-- If `A` is connected, the cardinality of `Aut A` is smaller than the cardinality of the
fiber of `A`.  -/
CategoryTheory.PreGaloisCategory.card_aut_le_card_fiber_of_connected : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C)
  [CategoryTheory.PreGaloisCategory.IsConnected A], Nat.card (CategoryTheory.Aut A) ≤ Nat.card (F.obj A).obj
-- Mathlib.Analysis.Convex.Body
ConvexBody.isBounded : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] (K : ConvexBody V), Bornology.IsBounded ↑K
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
/-- The product of two functions that are majorized with exponents `f_exp` and `g_exp` is
majorized with exponent `f_exp + g_exp`.  -/
Tactic.ComputeAsymptotics.Majorized.mul : ∀ {f g b : ℝ → ℝ} {f_exp g_exp : ℝ},
  Tactic.ComputeAsymptotics.Majorized f b f_exp →
    Tactic.ComputeAsymptotics.Majorized g b g_exp →
      (∀ᶠ (t : ℝ) in Filter.atTop, 0 < b t) → Tactic.ComputeAsymptotics.Majorized (f * g) b (f_exp + g_exp)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.homMk'_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T),
  f.homMk' (CategoryTheory.CategoryStruct.id f.left) = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Group.Basic
one_div_one_div : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α), 1 / (1 / a) = a
-- Mathlib.Tactic.Have
/-- A parser for optional binder identifiers  -/
Mathlib.Tactic.optBinderIdent : Lean.Parser.Parser
-- Mathlib.SetTheory.Ordinal.Notation
ONote.split_eq_scale_split' : ∀ {o o' : ONote} {m : ℕ} [o.NF], o.split' = (o', m) → o.split = (ONote.scale 1 o', m)
-- Lean.DocString.Parser
Lean.Doc.Parser.instReprBlockCtxt : Repr Lean.Doc.Parser.BlockCtxt
-- Mathlib.GroupTheory.Perm.ConjAct
/-- `a : α` belongs to the support of `k • g` iff
`k⁻¹ * a` belongs to the support of `g`  -/
Equiv.Perm.mem_conj_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (k : ConjAct (Equiv.Perm α)) (g : Equiv.Perm α) (a : α),
  a ∈ (k • g).support ↔ (ConjAct.ofConjAct k⁻¹) a ∈ g.support
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_one_eq_lift : ∀ {c : Cardinal.{u}}, Cardinal.aleph 1 = Cardinal.lift.{v, u} c ↔ Cardinal.aleph 1 = c
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.orderTop : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → OrderTop (CategoryTheory.Pretopology C)
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftMap_zero : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_6 : CategoryTheory.Limits.HasZeroMorphisms A]
  [F.PreservesZeroMorphisms] [∀ (n : M), (CategoryTheory.shiftFunctor C n).PreservesZeroMorphisms] (X Y : C)
  (n a a' : M) (ha' : n + a = a'), F.shiftMap 0 a a' ha' = 0
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.hasDerivAt_arsinh : ∀ (x : ℝ), HasDerivAt Real.arsinh (√(1 + x ^ 2))⁻¹ x
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.mk₀Inv.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] {X Y : C}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y X] [inst_4 : W.RespectsIso] (m₀ : M)
  (hm₀ : m₀ = 0) (f f_1 : X ⟶ Y) (e_f : f = f_1) (hf : W f),
  CategoryTheory.Localization.SmallShiftedHom.mk₀Inv m₀ hm₀ f hf =
    CategoryTheory.Localization.SmallShiftedHom.mk₀Inv m₀ hm₀ f_1 ⋯
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_eq_empty : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s : TopologicalSpace.Closeds α}, ↑s = ∅ ↔ s = ⊥
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false}, t.minKey he ∈ t
-- Mathlib.Topology.EMetricSpace.Defs
uniformity_basis_edist' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (ε' : ENNReal),
  0 < ε' → (uniformity α).HasBasis (fun ε => ε ∈ Set.Ioo 0 ε') fun ε => {p | edist p.1 p.2 < ε}
-- Std.Data.TreeSet.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the set.
 -/
Std.TreeSet.get! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet α cmp → α → α
-- Mathlib.Data.Sym.Basic
Sym.notMem_nil : ∀ {α : Type u_1} (a : α), a ∉ Sym.nil
-- Mathlib.Data.Set.Function
Set.SurjOn.comp_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β},
  Set.SurjOn f s t → ∀ (g : β → γ), Set.SurjOn (g ∘ f) s (g '' t)
-- Mathlib.Topology.Sheaves.Skyscraper
StalkSkyscraperPresheafAdjunctionAuxs.to_skyscraper_fromStalk : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {c : C} (f : 𝓕 ⟶ skyscraperPresheaf p₀ c),
  StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ (StalkSkyscraperPresheafAdjunctionAuxs.fromStalk p₀ f) =
    f
-- Mathlib.Data.Int.LeastGreatest
Int.leastOfBdd.congr_simp : ∀ {P : ℤ → Prop} [inst : DecidablePred P] (b b_1 : ℤ) (e_b : b = b_1) (Hb : ∀ (z : ℤ), P z → b ≤ z) (Hinh : ∃ z, P z),
  b.leastOfBdd Hb Hinh = b_1.leastOfBdd ⋯ Hinh
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
CompactConvergenceCLM.piEquivL_symm_apply : ∀ {𝕜₁ : Type u_1} [inst : NormedField 𝕜₁] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜₁ E]
  [inst_3 : TopologicalSpace E] {ι : Type u_7} (F : ι → Type u_8) [inst_4 : (i : ι) → AddCommGroup (F i)]
  [inst_5 : (i : ι) → Module 𝕜₁ (F i)] [inst_6 : (i : ι) → TopologicalSpace (F i)]
  [inst_7 : ∀ (i : ι), IsTopologicalAddGroup (F i)] [inst_8 : ∀ (i : ι), ContinuousConstSMul 𝕜₁ (F i)]
  (T : CompactConvergenceCLM (RingHom.id 𝕜₁) E ((i : ι) → F i)) (e : E) (i : ι),
  ((CompactConvergenceCLM.piEquivL 𝕜₁ E F).symm T i) e = T e i
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.ext : ∀ {R : Type u_1} {inst : CommRing R} {I : Ideal R} {M : Type u_3} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  {x y : I.Filtration M}, x.N = y.N → x = y
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProductIter_retractClosure_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) {n : ℕ},
  P.retractClosure.extensionProductIter n ≤ (P.extensionProductIter n).retractClosure
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardCongr_inv_app_val_app : ∀ {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} (e : φ = ψ)
  (M : SheafOfModules R) (U : Cᵒᵖ) (x : ↑(((SheafOfModules.pushforward ψ).obj M).val.obj U)),
  (CategoryTheory.ConcreteCategory.hom (((SheafOfModules.pushforwardCongr e).inv.app M).val.app U)) x = x
-- Mathlib.Topology.Order.ProjIcc
/-- A useful special case of `Continuous.IccExtend`.  -/
Continuous.Icc_extend' : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} {h : a ≤ b} [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : TopologicalSpace β] {f : ↑(Set.Icc a b) → β},
  Continuous f → Continuous (Set.IccExtend h f)
-- Mathlib.Control.Bitraversable.Instances
_private.Mathlib.Control.Bitraversable.Instances.0.Sum.bitraverse.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : α ⊕ β → Sort u_3) →
      (x : α ⊕ β) → ((x : α) → motive (Sum.inl x)) → ((x : β) → motive (Sum.inr x)) → motive x
-- Mathlib.RingTheory.LocalIso
Algebra.isLocalIso_iff : ∀ (R : Type u_1) (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.IsLocalIso R S ↔ ∀ (q : Ideal S) [q.IsPrime], ∃ g ∉ q, Algebra.IsStandardOpenImmersion R (Localization.Away g)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_1.congr_eq_1 : ∀ (motive : Option Bool → Sort u_1) (val? : Option Bool) (h_1 : (val' : Bool) → motive (some val'))
  (h_2 : (x : Option Bool) → motive x) (val' : Bool),
  val? = some val' →
    (match val? with
      | some val' => h_1 val'
      | x => h_2 x) ≍
      h_1 val'
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_mul_monomial_zero : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (d : ℕ) (r : R),
  (p * (Polynomial.monomial 0) r).coeff d = p.coeff d * r
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.FullyFaithful.addGrpObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.AddGrpObj (F.obj X)],
  hF.addGrpObj X =
    { toAddMonObj := hF.addMonObj X, neg := hF.preimage CategoryTheory.AddGrpObj.neg, left_neg := ⋯, right_neg := ⋯ }
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.apply_eq_zero_of_isNilpotent : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] [IsReduced R] (x : L),
  IsNilpotent ((LieModule.toEnd R L M) x) → ∀ (χ : LieModule.Weight R L M), χ x = 0
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial_zero_eq_C_apply : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (a : R), (MvPowerSeries.monomial 0) a = MvPowerSeries.C a
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.instHasCoequalizers : ∀ (R : Type w) [inst : Ring R], CategoryTheory.Limits.HasCoequalizers (ModuleCat R)
-- Mathlib.Order.Filter.CountablyGenerated
Filter.countable_biInf_eq_iInf_seq : ∀ {α : Type u_1} {ι : Type u_4} [inst : CompleteLattice α] {B : Set ι},
  B.Countable → B.Nonempty → ∀ (f : ι → α), ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)
-- Init.Data.Nat.Lemmas
Nat.le_mul_self : ∀ (n : ℕ), n ≤ n * n
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.pairing_eq_zero_of_add_notMem_of_sub_notMem : ∀ {ι : 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) [Finite ι]
  [CharZero R] [P.IsCrystallographic] {i j : ι} [IsDomain R],
  i ≠ j →
    P.root i ≠ -P.root j →
      P.root i + P.root j ∉ Set.range ⇑P.root → P.root i - P.root j ∉ Set.range ⇑P.root → P.pairing i j = 0
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.conjExponent : ∀ {p : ℝ}, 1 < p → p.HolderConjugate p.conjExponent
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_of_le_ge_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Lean.EnvExtension
Lean.mkMapDeclarationExtension : {α : Type} →
  autoParam Lean.Name Lean.mkMapDeclarationExtension._auto_3 →
    optParam Lean.EnvExtension.AsyncMode (Lean.EnvExtension.AsyncMode.async Lean.AsyncBranch.mainEnv) →
      (optParam (Lean.Environment → Lean.NameMap α → Lean.OLeanEntries (Array (Lean.Name × α))) fun env s =>
          have all :=
            Array.filter
              (fun x =>
                match x with
                | (n, snd) => env.contains n false)
              (Std.TreeMap.toArray s);
          Lean.OLeanEntries.uniform all) →
        IO (Lean.MapDeclarationExtension α)
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
/-- The counit of `constantSheafAdj` factors through the isomorphism `constantCommuteCompose`.  -/
CategoryTheory.constantSheafAdj_counit_w : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {B : Type u_3} [inst_3 : CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B)
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [inst_5 : J.PreservesSheafification U] [inst_6 : J.HasSheafCompose U]
  (F : CategoryTheory.Sheaf J D) {T : C} (hT : CategoryTheory.Limits.IsTerminal T),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.constantCommuteCompose J U).hom.app (F.obj.obj (Opposite.op T)))
      ((CategoryTheory.constantSheafAdj J B hT).counit.app ((CategoryTheory.sheafCompose J U).obj F)) =
    (CategoryTheory.sheafCompose J U).map ((CategoryTheory.constantSheafAdj J D hT).counit.app F)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_neg : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x : R), WithVal.toVal v (-x) = -WithVal.toVal v x
-- Mathlib.Order.PrimeIdeal
Order.Ideal.isPrime_iff_mem_or_mem : ∀ {P : Type u_1} [inst : SemilatticeInf P] {I : Order.Ideal P} [I.IsProper],
  I.IsPrime ↔ ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.restrictScalars_rTensor : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] (f : M →ₗ[A] P),
  ↑R ((TensorProduct.AlgebraTensorModule.rTensor R N) f) = LinearMap.rTensor N (↑R f)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.distortion_filter_le : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [inst : Fintype ι]
  (p : BoxIntegral.Box ι → Prop), (π.filter p).distortion ≤ π.distortion
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Characterization of the costructured arrow category on the diagonal functor `T ⥤ T × T`.  -/
CategoryTheory.CostructuredArrow.ofDiagEquivalence : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (X : T × T) →
      CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X ≌
        CategoryTheory.CostructuredArrow (CategoryTheory.Over.forget X.1) X.2
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.trans_assoc : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {R₄ : Type u_5} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10}
  {M₄ : Type u_11} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : Semiring R₄]
  [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid M₃] [inst_7 : AddCommMonoid M₄]
  {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {module_M₄ : Module R₄ M₄}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_8 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_9 : RingHomInvPair σ₃₁ σ₁₃] {σ₁₄ : R₁ →+* R₄} {σ₄₁ : R₄ →+* R₁} [inst_10 : RingHomInvPair σ₁₄ σ₄₁]
  [inst_11 : RingHomInvPair σ₄₁ σ₁₄] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {σ₂₄ : R₂ →+* R₄} {σ₄₂ : R₄ →+* R₂}
  [inst_12 : RingHomInvPair σ₂₄ σ₄₂] [inst_13 : RingHomInvPair σ₄₂ σ₂₄] {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃}
  [inst_14 : RingHomInvPair σ₃₄ σ₄₃] [inst_15 : RingHomInvPair σ₄₃ σ₃₄] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃}
  [inst_16 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_17 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_18 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [inst_19 : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁]
  [inst_20 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [inst_21 : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁]
  [inst_22 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄], ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
CategoryTheory.Limits.HasFiniteProducts.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ (n : ℕ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete (Fin n)) C) →
    CategoryTheory.Limits.HasFiniteProducts C
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- `AddMonoidAlgebra.single` as a `DistribMulActionHom`.  -/
AddMonoidAlgebra.singleDistribMulActionHom : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring S] → [inst_1 : Monoid R] → [inst_2 : DistribMulAction R S] → M → S →+[R] AddMonoidAlgebra S M
-- Std.Http.Data.Body.Full
Std.Http.Body.instNonemptyFull : Nonempty Std.Http.Body.Full
-- Mathlib.Algebra.Lie.Basic
LieHom.toFun_eq_coe : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂), (↑f).toFun = ⇑f
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- If `D` is a divisor, then the divisor of the factorized rational function equals `D`.
 -/
Function.FactorizedRational.divisor : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {D : Function.locallyFinsuppWithin U ℤ},
  D.support.Finite → MeromorphicOn.divisor (∏ᶠ (u : 𝕜), (fun x => x - u) ^ D u) U = D
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp_inj : ∀ {M : Type u_4} {x y : M}, WithZero.exp x = WithZero.exp y ↔ x = y
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.Lean.Loop.forIn.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b' : β) (h_1 : (b' : β) → motive (ForInStep.done b'))
  (h_2 : (b' : β) → motive (ForInStep.yield b')),
  (match ForInStep.done b' with
    | ForInStep.done b' => h_1 b'
    | ForInStep.yield b' => h_2 b') =
    h_1 b'