mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Fubini
/-- The limit of `F.flip ⋙ lim` is isomorphic to the limit of `F ⋙ lim`.  -/
CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] →
                [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K C] →
                  CategoryTheory.Limits.limit (F.flip.comp CategoryTheory.Limits.lim) ≅
                    CategoryTheory.Limits.limit (F.comp CategoryTheory.Limits.lim)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonModuleHierarchyOptions.fromJson : Lean.Json → Except String Lean.Lsp.ModuleHierarchyOptions
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_neg : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [inst_4 : DistribMulAction 𝕜 E] {s : Set E},
  Bornology.IsVonNBounded 𝕜 (-s) ↔ Bornology.IsVonNBounded 𝕜 s
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- The isomorphism `AddCircle T ≃ Ico a (a + T)` whose inverse is the natural quotient map,
as an equivalence of measurable spaces.  -/
AddCircle.measurableEquivIco : (T : ℝ) → [hT : Fact (0 < T)] → (a : ℝ) → AddCircle T ≃ᵐ ↑(Set.Ico a (a + T))
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.mk : {ι : 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} →
                    [toIsValuedIn : P.IsValuedIn ℤ] →
                      [toIsReduced : P.IsReduced] → (long short : ι) → P.pairingIn ℤ long short = -3 → P.EmbeddedG2
-- Mathlib.LinearAlgebra.Matrix.ToLin
Algebra.toMatrix_lmul_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {m : Type u_3}
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (b : Module.Basis m R S) (x : S),
  (LinearMap.toMatrix b b) (LinearMap.mulLeft R x) = (Algebra.leftMulMatrix b) x
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.beq.match_1.eq_4 : ∀ (motive : Lean.Name → Lean.Name → Sort u_1) (x x_1 : Lean.Name)
  (h_1 : Unit → motive Lean.Name.anonymous Lean.Name.anonymous)
  (h_2 : (p₁ : Lean.Name) → (s₁ : String) → (p₂ : Lean.Name) → (s₂ : String) → motive (p₁.str s₁) (p₂.str s₂))
  (h_3 : (p₁ : Lean.Name) → (n₁ : ℕ) → (p₂ : Lean.Name) → (n₂ : ℕ) → motive (p₁.num n₁) (p₂.num n₂))
  (h_4 : (x x_2 : Lean.Name) → motive x x_2),
  (x = Lean.Name.anonymous → x_1 = Lean.Name.anonymous → False) →
    (∀ (p₁ : Lean.Name) (s₁ : String) (p₂ : Lean.Name) (s₂ : String), x = p₁.str s₁ → x_1 = p₂.str s₂ → False) →
      (∀ (p₁ : Lean.Name) (n₁ : ℕ) (p₂ : Lean.Name) (n₂ : ℕ), x = p₁.num n₁ → x_1 = p₂.num n₂ → False) →
        (match x, x_1 with
          | Lean.Name.anonymous, Lean.Name.anonymous => h_1 ()
          | p₁.str s₁, p₂.str s₂ => h_2 p₁ s₁ p₂ s₂
          | p₁.num n₁, p₂.num n₂ => h_3 p₁ n₁ p₂ n₂
          | x, x_5 => h_4 x x_5) =
          h_4 x x_1
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- Key lemma for Mahler's theorem: for `f` a continuous function on `ℤ_[p]`, the sequence
`n ↦ Δ^[n] f 0` tends to 0. See `PadicInt.fwdDiff_iter_le_of_forall_le` for an explicit
estimate of the decay rate.  -/
PadicInt.fwdDiff_tendsto_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] (f : C(ℤ_[p], E)),
  Filter.Tendsto (fun x => (fwdDiff 1)^[x] (⇑f) 0) Filter.atTop (nhds 0)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.comap_map_hom : ∀ {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.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.AddMonObj A] [inst_5 : CategoryTheory.AddMonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsAddMonHom f] {M N : CategoryTheory.AddMod D B} (g : M ⟶ N),
  ((CategoryTheory.AddMod.comap f).map g).hom = g.hom
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.mkCommaMorphism_left_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D} (η : F ⟶ G) (X : C),
  (CategoryTheory.WithTerminal.mkCommaMorphism η).left.app X = η.app (CategoryTheory.WithTerminal.incl.obj X)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_pi_add_coe_pi : ↑Real.pi + ↑Real.pi = 0
-- Mathlib.Order.KrullDimension
Order.coheight_le_krullDim : ∀ {α : Type u_1} [inst : Preorder α] (a : α), ↑(Order.coheight a) ≤ Order.krullDim α
-- Mathlib.Analysis.Normed.Group.Continuity
controlled_sum_of_mem_closure : ∀ {E : Type u_4} [inst : SeminormedAddCommGroup E] {a : E} {s : AddSubgroup E},
  a ∈ closure ↑s →
    ∀ {b : ℕ → ℝ},
      (∀ (n : ℕ), 0 < b n) →
        ∃ v,
          Filter.Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), v i) Filter.atTop (nhds a) ∧
            (∀ (n : ℕ), v n ∈ s) ∧ ‖-v 0 + a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
-- Init.Data.Float.Model.Unpacked.Operations.Compare
/-- Computes the ordering between the two floats as specificed by IEEE. Returns an
`Option Ordering` to account for the fact that `NaN` is incomparable with everything.
Also, positive and negative zero are equal.

Important: this operation only works correctly if the two inputs are in
canonical form for a common format (see the docstring for `UnpackedFloat` for details.)
 -/
Float.Model.UnpackedFloat.compare : Float.Model.UnpackedFloat → Float.Model.UnpackedFloat → Option Ordering
-- Lean.Meta.Coe
/-- Expands coercions occurring in `e` and return the result together with a list of applied
`Coe` instances.
 -/
Lean.Meta.expandCoe : Lean.Expr → Lean.MetaM (Lean.Expr × List Lean.Name)
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereographic'.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (n : ℕ)
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)] (v v_1 : ↑(Metric.sphere 0 1)),
  v = v_1 → stereographic' n v = stereographic' n v_1
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instOrdOrdinal : Ord Std.Time.Minute.Ordinal
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.getD_eq_getDₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α)
  (fallback : β),
  Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = Std.DHashMap.Internal.Raw₀.Const.getDₘ m a fallback
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallCache.cache : Lean.Elab.WF.GuessLex.RecCallCache → IO.Ref (Array (Array (Option Lean.Elab.WF.GuessLex.GuessLexRel)))
-- Init.Data.String.Defs
String.Pos.Raw.IsValid.le_endPos : ∀ {s : String} {off : String.Pos.Raw}, String.Pos.Raw.IsValid s off → off ≤ s.rawEndPos
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- Some approximation of the least fixed point starting from `⊤` is the greatest fixed point.  -/
OrdinalApprox.gfp_mem_range_gfpApprox : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), OrderHom.gfp f ∈ Set.range (OrdinalApprox.gfpApprox f ⊤)
-- Batteries.Data.List.Matcher
/-- Accumulator loop for `List.Matcher.findAll`  -/
List.Matcher.findAll.loop : {α : Type u_1} → [BEq α] → List.Matcher α → List α × ℕ → Array.Matcher α → Array (ℕ × ℕ) → Array (ℕ × ℕ)
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.image_Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (a b : α),
  ⇑e '' Set.Icc a b = Set.Icc (e a) (e b)
-- Init.Data.List.Nat.Basic
List.min?_get_le_of_mem : ∀ {l : List ℕ} {a : ℕ} (h : a ∈ l), l.min?.get ⋯ ≤ a
-- Mathlib.Algebra.Quandle
/-- Associative racks are uninteresting.
 -/
Rack.assoc_iff_id : ∀ {R : Type u_2} [inst : Rack R] {x y z : R},
  Shelf.act x (Shelf.act y z) = Shelf.act (Shelf.act x y) z ↔ Shelf.act x z = z
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Div β]
  [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.Kernel.IndepFun (f i / f j) (f k) κ μ
-- Mathlib.Analysis.Normed.Group.Basic
exists_norm_ne_zero' : ∀ (E : Type u_5) [inst : SeminormedGroup E] [NontrivialTopology E], ∃ x, ‖x‖ ≠ 0
-- Mathlib.Order.Filter.Ultrafilter.Basic
Ultrafilter.le_cofinite_or_eq_pure : ∀ {α : Type u} (f : Ultrafilter α), ↑f ≤ Filter.cofinite ∨ ∃ a, f = pure a
-- Init.Data.String.Subslice
String.Slice.toSlice_subslice : ∀ {s : String.Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd},
  (s.subslice newStart newEnd h).toSlice = s.slice newStart newEnd h
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.transitionMap.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {m n : ℕ} (hmn : m ≤ n), AdicCompletion.transitionMap I M hmn = Submodule.factorPow I M hmn
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_le_self : ∀ {α : Type u_2} {M : Type u_3} [inst : AddMonoid M] [inst_1 : PartialOrder M] [CanonicallyOrderedAdd M] (s : Set α)
  (f : α → M), s.indicator f ≤ f
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_zsmul : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (r : ℤ)
  (f : NormedAddGroupHom V₁ V₂), ⇑(r • f) = r • ⇑f
-- Mathlib.Data.List.Permutation
List.permutations_nil : ∀ {α : Type u_1}, [].permutations = [[]]
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyUnramified.propertyIsLocal : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.Q_f_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (q n : ℕ)
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj Y).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n }))
      (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) h) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n)
      (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n })) h)
-- Mathlib.Logic.Basic
xor_not_left : ∀ {a b : Prop}, Xor (¬a) b ↔ (a ↔ b)
-- Std.Data.ByteSlice
/-- Creates a sub-slice of the byte slice with the given bounds.

If `start` or `stop` are not valid bounds for a sub-slice, then they are clamped to the slice's size.
Additionally, the starting index is clamped to the ending index.

The indices are relative to the current slice, not the underlying byte array.
 -/
ByteSlice.slice : (s : ByteSlice) → optParam ℕ 0 → optParam ℕ s.size → ByteSlice
-- Mathlib.Algebra.Category.Grp.FilteredColimits
CommGrpCat.FilteredColimits.G.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J CommGrpCat),
  CommGrpCat.FilteredColimits.G F = GrpCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat))
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If `p ^ k` is a prime power, then
`cyclotomic (p ^ (n + 1)) R = ∑ i ∈ range p, (X ^ (p ^ n)) ^ i`.  -/
Polynomial.cyclotomic_prime_pow_eq_geom_sum : ∀ {R : Type u_1} [inst : CommRing R] {p n : ℕ},
  Nat.Prime p → Polynomial.cyclotomic (p ^ (n + 1)) R = ∑ i ∈ Finset.range p, (Polynomial.X ^ p ^ n) ^ i
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_mul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {c : E → 𝔸'}, DifferentiableAt 𝕜 c x → ∀ (d : 𝔸'), fderiv 𝕜 (fun y => c y * d) x = d • fderiv 𝕜 c x
-- Lean.Parser.Syntax
Lean.Parser.Command.elab_rules.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.contDiffAt : ∀ {x : ℝ} {n : ℕ∞}, ContDiffAt ℝ (↑n) Real.smoothTransition x
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.continuous_rng_of_compactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {f : X → CompactCoherentification Y} [CompactSpace X],
  Continuous f ↔ Continuous (⇑(CompactCoherentification.mk Y).symm ∘ f)
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.support_one : ∀ {ι : Type u_1} (R : Type u_5) [inst : Zero R] [inst_1 : One R] [NeZero 1], Function.support 1 = Set.univ
-- Mathlib.Algebra.Ring.Periodic
Finset.periodic_prod : ∀ {α : Type u_1} {β : Type u_2} {c : α} [inst : Add α] [inst_1 : CommMonoid β] {ι : Type u_4} {f : ι → α → β}
  (s : Finset ι), (∀ i ∈ s, Function.Periodic (f i) c) → Function.Periodic (∏ i ∈ s, f i) c
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplexHomeomorphUnitInterval_apply_coe : ∀ (f : ↑(stdSimplex ℝ (Fin 2))), ↑(stdSimplexHomeomorphUnitInterval f) = ↑f 1
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- Construct an element of the projectivization from a nonzero vector.  -/
Projectivization.mk : (K : Type u_1) →
  {V : Type u_2} →
    [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → (v : V) → v ≠ 0 → Projectivization K V
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
          (CategoryTheory.CategoryStruct.id Y))
        h)
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.mul_add_mul : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : α), a * b + b * a = 0
-- Mathlib.Analysis.Convex.StdSimplex
/-- The standard simplex in the zero-dimensional space is empty.  -/
stdSimplex_of_isEmpty_index : ∀ (𝕜 : Type u_2) (ι : Type u_1) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Fintype ι] [IsEmpty ι]
  [Nontrivial 𝕜], stdSimplex 𝕜 ι = ∅
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.instNontrivialOfNonempty : ∀ {M : Type u_1} [inst : Add M] [hn : Nonempty M], Nontrivial (AddSubsemigroup M)
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsRat.to_isNNRat : ∀ {α : Type u_1} [inst : Ring α] {a : α} {n d : ℕ},
  Mathlib.Meta.NormNum.IsRat a (Int.ofNat n) d → Mathlib.Meta.NormNum.IsNNRat a n d
-- Mathlib.Analysis.Analytic.Constructions
/-- The alternating geometric series `1 - x + x ^ 2 - ...` as a `FormalMultilinearSeries`.  -/
alternatingGeometricSeries : (𝕜 : Type u_2) →
  [inst : NontriviallyNormedField 𝕜] →
    (A : Type u_7) → [inst_1 : NormedRing A] → [inst_2 : NormedAlgebra 𝕜 A] → FormalMultilinearSeries 𝕜 A A
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trCont.eq_1 : Turing.PartrecToTM2.trCont Turing.ToPartrec.Cont.halt = Turing.PartrecToTM2.Cont'.halt
-- Mathlib.Algebra.Group.Conj
ConjClasses.instInhabited.eq_1 : ∀ {α : Type u} [inst : Monoid α], ConjClasses.instInhabited = { default := ⟦1⟧ }
-- Mathlib.RingTheory.Localization.Algebra
/-- The canonical linear map from the kernel of an algebra homomorphism to its localization
is localizing.  -/
AlgHom.toKerIsLocalization_isLocalizedModule : ∀ {R : Type u_5} [inst : CommSemiring R] (M : Submonoid R) {A : Type u_6} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] {B : Type u_7} [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (Rₚ : Type u_8)
  [inst_5 : CommSemiring Rₚ] [inst_6 : Algebra R Rₚ] [inst_7 : IsLocalization M Rₚ] (Aₚ : Type u_9)
  [inst_8 : CommSemiring Aₚ] [inst_9 : Algebra R Aₚ] [inst_10 : Algebra A Aₚ] [inst_11 : IsScalarTower R A Aₚ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type u_10) [inst_13 : CommSemiring Bₚ]
  [inst_14 : Algebra R Bₚ] [inst_15 : Algebra B Bₚ] [inst_16 : IsScalarTower R B Bₚ]
  [inst_17 : IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ] [inst_18 : Algebra Rₚ Aₚ] [inst_19 : Algebra Rₚ Bₚ]
  [inst_20 : IsScalarTower R Rₚ Aₚ] [inst_21 : IsScalarTower R Rₚ Bₚ] (f : A →ₐ[R] B),
  IsLocalizedModule (Algebra.algebraMapSubmonoid A M) (AlgHom.toKerIsLocalization M Rₚ Aₚ Bₚ f)
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_Iio : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] {a x : α}, x ∈ Finset.Iio a ↔ x < a
-- Mathlib.RingTheory.PowerSeries.Log
/-- `logOf f` is `log(1+X)` substituted at `f - 1`, i.e., `(f-1) - (f-1)²/2 + (f-1)³/3 - ⋯`.  -/
PowerSeries.logOf : {A : Type u_1} → [inst : CommRing A] → [Algebra ℚ A] → PowerSeries A → PowerSeries A
-- Mathlib.Order.Bounds.Basic
bddAbove_empty : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], BddAbove ∅
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The 2-morphism filling the triangle diagram.  -/
CategoryTheory.Bicategory.RightExtension.counit : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          (t : CategoryTheory.Bicategory.RightExtension f g) → CategoryTheory.CategoryStruct.comp f t.extension ⟶ g
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- The forgetful functor from commutative group objects to commutative monoid objects.  -/
CategoryTheory.CommGrp.forget₂CommMon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.CommGrp C) (CategoryTheory.CommMon C)
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.Arrow.Hom.zero_right : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [inst_1 : CategoryTheory.Preadditive T]
  {u v : CategoryTheory.Arrow T}, CategoryTheory.Arrow.Hom.right 0 = 0
-- Mathlib.GroupTheory.GroupAction.ConjAct
/-- A recursor for `ConjAct`, for use as `induction x` when `x : ConjAct G`.  -/
ConjAct.rec : {G : Type u_3} →
  [inst : DivInvMonoid G] → {C : ConjAct G → Sort u_4} → ((g : G) → C (ConjAct.toConjAct g)) → (g : ConjAct G) → C g
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.sum_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} {ι : Type u_9} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂} (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) (b : M),
  (∑ d ∈ t, f d) b = ∑ d ∈ t, (f d) b
-- Mathlib.Algebra.Quaternion
/-- The cardinality of a quaternion algebra, as a type.  -/
Cardinal.mk_quaternionAlgebra : ∀ {R : Type u_1} (c₁ c₂ c₃ : R), Cardinal.mk (QuaternionAlgebra R c₁ c₂ c₃) = Cardinal.mk R ^ 4
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.toCompacts : {α : Type u_4} → [inst : TopologicalSpace α] → TopologicalSpace.PositiveCompacts α → TopologicalSpace.Compacts α
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_add_neg_iff_le : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, 0 ≤ a + -b ↔ b ≤ a
-- Mathlib.CategoryTheory.Limits.Unit
/-- A trivial cone for a functor into `PUnit`. `punitConeIsLimit` shows it is a limit.  -/
CategoryTheory.Limits.punitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{v', v} J] →
    {F : CategoryTheory.Functor J (CategoryTheory.Discrete PUnit.{u_1 + 1})} → CategoryTheory.Limits.Cone F
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.instIsFiniteMeasure : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)],
  MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.pi μ)
-- Init.Data.UInt.Lemmas
UInt16.toUSize_lt : ∀ {a b : UInt16}, a.toUSize < b.toUSize ↔ a < b
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
WithIdeal.instUniformSpace : (R : Type u_1) → [inst : CommRing R] → [WithIdeal R] → UniformSpace R
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The functor taking a cone over `F` to a cone over `Over.post F : Over i ⥤ Over (F.obj i)`
preserves limit cones  -/
CategoryTheory.Over.isLimitConePost : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [CategoryTheory.IsCofilteredOrEmpty J] →
          {F : CategoryTheory.Functor J C} →
            {c : CategoryTheory.Limits.Cone F} →
              (i : J) →
                CategoryTheory.Limits.IsLimit c →
                  CategoryTheory.Limits.IsLimit ((CategoryTheory.Over.conePost F i).obj c)
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Does `r` contain any entries with key `n`?  -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.DirectoryDependency.NamePrefixRel.containsKey : Mathlib.Linter.DirectoryDependency.NamePrefixRel✝ → Lean.Name → Bool
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.instFullCompPostOfFaithful : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T)
  (F : CategoryTheory.Functor T C) [F.Faithful], (CategoryTheory.Comma.post L R F).Full
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- A smooth compactly supported function is a Schwartz function.  -/
HasCompactSupport.toSchwartzMap : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] → {f : E → F} → HasCompactSupport f → ContDiff ℝ (↑⊤) f → SchwartzMap E F
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.Hom.w_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i j : ι) (X : TopPair),
  CategoryTheory.CategoryStruct.comp ((HP.δ i j).app X) ((f.hom j).app X.left) =
    CategoryTheory.CategoryStruct.comp ((f.homₚ i).app X) ((HP'.δ i j).app X)
-- Mathlib.Data.Num.Basic
/-- `ofNatSucc n` is the `PosNum` corresponding to `n + 1`.  -/
PosNum.ofNatSucc : ℕ → PosNum
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_iUnion_apply : ∀ {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [inst : CompleteLattice M] [inst_1 : One M],
  ⊥ = 1 → ∀ (s : ι → Set α) (f : α → M) (x : α), (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.closure_insert_sdiff_eq_of_mem_closure : ∀ {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α},
  M.Indep I → f ∈ M.closure I → e ∈ M.closure (insert f I \ {e}) → M.closure (insert f I \ {e}) = M.closure I
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_empty' : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] (f : α → M), ∅.indicator f = 0