mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Nat.Dist
Nat.dist_mul_left : ∀ (k n m : ℕ), (k * n).dist (k * m) = k * n.dist m
-- Mathlib.AlgebraicGeometry.Scheme
/-- `Spec R` with the specialization order is order isomorphic to the dual of the prime
spectrum of `R`.  -/
AlgebraicGeometry.specOrderIsoPrimeSpectrum : (R : CommRingCat) → ↥(AlgebraicGeometry.Spec R) ≃o (PrimeSpectrum ↑R)ᵒᵈ
-- Mathlib.Algebra.Order.Archimedean.Class
/-- `ArchimedeanClass M` is the quotient of the additive group `M` by additive archimedean
equivalence, where two elements `a` and `b` are in the same class iff
`(∃ m : ℕ, |b| ≤ m • |a|) ∧ (∃ n : ℕ, |a| ≤ n • |b|)`.  -/
ArchimedeanClass : (M : Type u_1) → [inst : AddCommGroup M] → [inst_1 : LinearOrder M] → [IsOrderedAddMonoid M] → Type u_1
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
/-- The permutation representation of the Weyl group induced by `reflectionPerm`.  -/
RootPairing.weylGroupToPerm : {ι : 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) → ↥P.weylGroup →* ι ≃ ι
-- Batteries.Data.Random.MersenneTwister
Batteries.Random.MersenneTwister.State.mk.sizeOf_spec : ∀ {cfg : Batteries.Random.MersenneTwister.Config} (data : Vector (BitVec cfg.wordSize) cfg.stateSize)
  (index : Fin cfg.stateSize), sizeOf { data := data, index := index } = 1 + sizeOf data + sizeOf index
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_comp_to_continuous_fun : ∀ {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ]
  [inst_2 : TopologicalSpace δ] [inst_3 : Zero δ] (f : CompactlySupportedContinuousMap γ δ) (g : CocompactMap β γ),
  ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.all_ae_of : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {ι : Sort u_4} {p : α → ι → Prop}, (∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) → ∀ (i : ι), ∀ᵐ (a : α) ∂μ, p a i
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.α.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.α✝ f n =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.cokernel f).πTruncGE n)
        (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.p✝ f n))
-- Mathlib.Data.Finset.Basic
Finset.Nontrivial.exists_cons_eq : ∀ {α : Type u_1} {s : Finset α},
  s.Nontrivial → ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), Finset.cons a (Finset.cons b t hb) ⋯ = s
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.π_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] [inst_2 : CategoryTheory.Limits.HasColimits C],
  CategoryTheory.Epi D.π
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- A projection from the product of a family of triangles.  -/
CategoryTheory.Pretriangulated.productTriangle.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {J : Type u_1} →
        (T : J → CategoryTheory.Pretriangulated.Triangle C) →
          [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] →
            [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] →
              [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] →
                [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] →
                  (j : J) → CategoryTheory.Pretriangulated.productTriangle T ⟶ T j
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.cells_bot : ⊥.cells = ∅
-- Mathlib.Topology.Algebra.Monoid.Defs
/-- Eta-expanded form of `Continuous.mul` -/
Continuous.fun_mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M}, Continuous f → Continuous g → Continuous fun i => f i * g i
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `L/K` is finite and normal, and `f` is a power-multiplicative `K`-algebra norm on `L`
extending the norm on `K`, then `f = spectralNorm K L`.  -/
spectralNorm_unique_of_finiteDimensional_normal : ∀ (K : Type u_2) [inst : NormedField K] (L : Type u_3) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hn : Normal K L] {f : AlgebraNorm K L},
  IsPowMul ⇑f →
    IsNonarchimedean ⇑f →
      (∀ (x : K), f ((algebraMap K L) x) = ↑‖x‖₊) →
        (∀ (σ : Gal(L/K)) (x : L), f x = f (σ x)) → ∀ (x : L), f x = spectralNorm K L x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.distinct_keys_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp],
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) (Std.ExtDTreeMap.Const.toList t)
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.mk_eq_bot_iff_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [inst_3 : CategoryTheory.Mono f],
  CategoryTheory.Subobject.mk f = ⊥ ↔ f = 0
-- Mathlib.Analysis.Normed.Operator.Basic
/-- If a continuous linear map is constructed from a linear map via the constructor `mkContinuous`,
then its norm is bounded by the bound or zero if bound is negative.  -/
LinearMap.mkContinuous_norm_le' : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ₁₂] F) {C : ℝ}
  (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖), ‖f.mkContinuous C h‖ ≤ max C 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.I.eq_1 : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore), h.I = Set.range h.type₁
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.TensorSigns.rel_add : ∀ {I : Type u_7} {inst : AddMonoid I} {c : ComplexShape I} [self : c.TensorSigns] (p q r : I),
  c.Rel p q → c.Rel (p + r) (q + r)
-- Mathlib.Order.Compare
Eq.cmp_eq_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α}, x = y → cmp x y = Ordering.eq
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.out_mul' : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] (a b : Associates α),
  Associated (a * b).out (a.out * b.out)
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {s : LowerSet α} (g : β ≃o γ) (f : α ≃o β), (LowerSet.map g) ((LowerSet.map f) s) = (LowerSet.map (f.trans g)) s
-- Mathlib.Order.Bounds.Defs
/-- A set is cofinal when for every `x : α` there exists `y ∈ s` with `x ≤ y`.  -/
IsCofinal : {α : Type u_1} → [LE α] → Set α → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_strictMono : StrictMono Real.arctan
-- Mathlib.Topology.UniformSpace.Defs
mem_nhds_left : ∀ {α : Type ua} [inst : UniformSpace α] (x : α) {s : SetRel α α}, s ∈ uniformity α → {y | (x, y) ∈ s} ∈ nhds x
-- Mathlib.Data.Nat.Squarefree
Nat.minSqFac_le_of_dvd : ∀ {n d : ℕ}, n.minSqFac = some d → ∀ {m : ℕ}, 2 ≤ m → m * m ∣ n → d ≤ m
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.one_le_y : ∀ {s : SelbergSieve}, 1 ≤ s.level
-- Lean.Environment
Lean.ImportM.Context.opts : Lean.ImportM.Context → Lean.Options
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.List.foldlM_filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.foldM_map : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps : Std.Do.PostShape} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad m] [LawfulMonad n]
  [inst_6 : Std.Do.WPMonad n ps] [inst_7 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_9 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : Std.IterM m β}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄ Std.IterM.foldM (fun d b => g d (f b)) init it ⦃Q⦄ → ⦃P⦄ Std.IterM.foldM g init (Std.IterM.map f it) ⦃Q⦄
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.mkIso'_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Comon C} (f : M.X ≅ N.X) [inst_2 : CategoryTheory.IsComonHom f.hom],
  (CategoryTheory.Comon.mkIso' f).hom.hom = f.hom
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)},
  k' ∈ (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl ↔
    if compare k k' = Ordering.eq then (f (t.get? k)).isSome = true else k' ∈ t
-- Mathlib.Data.List.Iterate
List.range_map_iterate : ∀ {α : Type u_1} (n : ℕ) (f : α → α) (a : α), List.map (fun x => f^[x] a) (List.range n) = List.iterate f a n
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.Small.limitCone_pt_ext : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : Small.{u, max u v} ↑F.sections] {x y : (CategoryTheory.Limits.Types.Small.limitCone F).pt},
  (equivShrink ↑F.sections).symm x = (equivShrink ↑F.sections).symm y → x = y
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.coe_injective : ∀ (α : Type u_1) [inst : UniformSpace α] [T0Space α], Function.Injective UniformSpace.Completion.coe'
-- Mathlib.MeasureTheory.VectorMeasure.Integral
_private.Mathlib.MeasureTheory.VectorMeasure.Integral.0.MeasureTheory.VectorMeasure.integral.eq_1 : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (f : X → E) (B : E →L[ℝ] F →L[ℝ] G),
  μ.integral f B = MeasureTheory.setToFun μ.variation ⇑(μ.transpose B) ⋯ f
-- Mathlib.FieldTheory.Fixed
/-- A typeclass for subrings invariant under a `MulSemiringAction`.  -/
IsInvariantSubfield : (M : Type u) → [inst : Monoid M] → {F : Type v} → [inst_1 : Field F] → [MulSemiringAction M F] → Subfield F → Prop
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- A set `s : Set (TaggedPrepartition I)` belongs to `l.toFilteriUnion I π₀` if for any `c : ℝ≥0`
there exists a function `r : ℝⁿ → (0, ∞)` (or a constant `r` if `l.bRiemann = true`) such that `s`
contains each prepartition `π` such that `l.MemBaseSet I c r π` and `π.iUnion = π₀.iUnion`.  -/
BoxIntegral.IntegrationParams.toFilteriUnion : {ι : Type u_1} →
  [Fintype ι] →
    {l : BoxIntegral.IntegrationParams} →
      (I : BoxIntegral.Box ι) → BoxIntegral.Prepartition I → Filter (BoxIntegral.TaggedPrepartition I)
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {V : (x : M') → TangentSpace I' x} {g : M' → 𝕜},
  VectorField.mpullback I I' f (g • V) = g ∘ f • VectorField.mpullback I I' f V
-- Mathlib.Analysis.Normed.Operator.Basic
/-- The operator norm of a continuous linear map is the inf of all its bounds.  -/
ContinuousLinearMap.opNorm : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_4} →
      {F : Type u_5} →
        [inst : SeminormedAddCommGroup E] →
          [inst_1 : SeminormedAddCommGroup F] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NontriviallyNormedField 𝕜₂] →
                [inst_4 : NormedSpace 𝕜 E] → [inst_5 : NormedSpace 𝕜₂ F] → {σ₁₂ : 𝕜 →+* 𝕜₂} → (E →SL[σ₁₂] F) → ℝ
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- Pushforwards of finite-dimensional submodules are finite-dimensional.  -/
FiniteDimensional.instSubtypeMemSubmoduleMap : ∀ (K : Type u) {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V) [FiniteDimensional K ↥p],
  FiniteDimensional K ↥(Submodule.map f p)
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
_private.Mathlib.Combinatorics.Extremal.RuzsaSzemeredi.0.locallyLinear : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : CommRing α] {s : Finset α} [Fact (IsUnit 2)],
  ThreeAPFree ↑s → (SimpleGraph.TripartiteFromTriangles.graph (triangleIndices✝ s)).LocallyLinear
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instMonoidWithZero : MonoidWithZero Complex.UnitClosedDisc
-- Mathlib.Data.Set.NAry
Set.image2_subset_iff_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {u : Set γ},
  Set.image2 f s t ⊆ u ↔ ∀ b ∈ t, (fun a => f a b) '' s ⊆ u
-- Batteries.Data.List.Lemmas
List.pairwise_idxsOf : ∀ {α : Type u_1} {xs : List α} {x : α} {s : ℕ} [inst : BEq α], List.Pairwise (fun x1 x2 => x1 < x2) (List.idxsOf x xs s)
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.restrictTarget_target : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (U : Y.Opens) (hU : Dense ↑U) (hU' : U ≤ f.target),
  (f.restrictTarget U hU hU').target = (f.symm.restrictSource U hU hU').source
-- Lean.Compiler.ExternAttr
Lean.instInhabitedExternAttrData : Inhabited Lean.ExternAttrData
-- Mathlib.GroupTheory.Congruence.Basic
/-- If e : M →* N is surjective then (c.comap e).Quotient ≃* c.Quotient with c :
AddCon N  -/
AddCon.comapQuotientEquivOfSurj : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        (c : AddCon M) → (f : N →+ M) → Function.Surjective ⇑f → (AddCon.comap ⇑f ⋯ c).Quotient ≃+ c.Quotient
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Context : Type
-- Mathlib.NumberTheory.PowModTotient
Nat.pow_add_mul_totient_mod_eq : ∀ {x k l n : ℕ}, 1 < n → x.Coprime n → x ^ (k + l * n.totient) % n = x ^ k % n
-- Mathlib.Algebra.Star.Module
StarModule.selfAdjointPart_add_skewAdjointPart : ∀ (R : Type u_1) {A : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] (x : A), ↑((selfAdjointPart R) x) + ↑((skewAdjointPart R) x) = x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- The pullback of a monomorphism is a monomorphism  -/
CategoryTheory.Limits.pullback.fst_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Mono g],
  CategoryTheory.Mono (CategoryTheory.Limits.pullback.fst f g)
-- Lean.Meta.Tactic.Util
/-- Get the user name of the given metavariable.  -/
Lean.MVarId.getTag : Lean.MVarId → Lean.MetaM Lean.Name
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.Equiv.congr_simp : ∀ {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] {β α₁ α₂ : Type w} [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] (ita ita_1 : Std.IterM m β),
  ita = ita_1 → ∀ (itb itb_1 : Std.IterM m β), itb = itb_1 → ita.Equiv itb = ita_1.Equiv itb_1
-- Lean.Data.NameMap.Basic
Lean.NameMap.instInhabited : (α : Type) → Inhabited (Lean.NameMap α)
-- Lean.Util.MonadCache
Lean.MonadCacheT.instMonadExceptOf : {ω α β : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] →
      [inst_1 : BEq α] →
        [inst_2 : Hashable α] → (ε : Type u_1) → [MonadExceptOf ε m] → MonadExceptOf ε (Lean.MonadCacheT α β m)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatMk_X₃_carrier : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ X₃ : Type v} [inst_1 : AddCommGroup X₁] [inst_2 : AddCommGroup X₂]
  [inst_3 : AddCommGroup X₃] [inst_4 : Module R X₁] [inst_5 : Module R X₂] [inst_6 : Module R X₃] (f : X₁ →ₗ[R] X₂)
  (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0), ↑(CategoryTheory.ShortComplex.moduleCatMk f g hfg).X₃ = X₃
-- Mathlib.RingTheory.Coalgebra.Basic
/-- The counit satisfies the left counitality law  -/
Coalgebra.rTensor_counit_comp_comul : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  [self : Coalgebra R A],
  LinearMap.rTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul = (TensorProduct.mk R R A) 1
-- Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
/-- Pull back a left rigid structure along an equivalence.  -/
CategoryTheory.leftRigidCategoryOfEquivalence : {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 D] →
            {F : CategoryTheory.Functor C D} →
              [F.Monoidal] →
                {G : CategoryTheory.Functor D C} →
                  (F ⊣ G) →
                    [F.IsEquivalence] → [CategoryTheory.LeftRigidCategory D] → CategoryTheory.LeftRigidCategory C
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
BoundedContinuousFunction.range_toLp : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_3}
  [inst_5 : Fact (1 ≤ p)] [inst_6 : NormedRing 𝕜] [inst_7 : Module 𝕜 E] [inst_8 : IsBoundedSMul 𝕜 E],
  (↑(BoundedContinuousFunction.toLp p μ 𝕜)).range.toAddSubgroup = MeasureTheory.Lp.boundedContinuousFunction E p μ
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAt_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (c : F) (x : E), HasFDerivAt (fun x => c) 0 x
-- Mathlib.LinearAlgebra.Pi
/-- Construct a linear map between two (dependent) function spaces
by applying index-dependent linear maps to the coordinates.
A bundled version of `Pi.map`.

If the index type is finite, then this map can be seen as a “block diagonal” map
between indexed products of modules.  -/
LinearMap.piMap : {R : Type u} →
  {ι : Type x} →
    [inst : Semiring R] →
      {φ : ι → Type i} →
        [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
          [inst_2 : (i : ι) → Module R (φ i)] →
            {ψ : ι → Type u_1} →
              [inst_3 : (i : ι) → AddCommMonoid (ψ i)] →
                [inst_4 : (i : ι) → Module R (ψ i)] → ((i : ι) → φ i →ₗ[R] ψ i) → ((i : ι) → φ i) →ₗ[R] (i : ι) → ψ i
-- Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
ContinuousLinearMap.measurable_apply' : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : MeasurableSpace E] [OpensMeasurableSpace E] [inst_7 : MeasurableSpace F] [BorelSpace F],
  Measurable fun x f => f x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_filterMap!_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] [inst : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.filterMap! f t) k =
        ((Std.DTreeMap.Internal.Impl.Const.get? t k).bind fun x => f k' x).get!
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.dense_domain : ∀ {X Y : AlgebraicGeometry.Scheme} (self : X.PartialMap Y), Dense ↑self.domain
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.sum_Prop : ∀ {M : Type u_4} [inst : AddCommMonoid M] (f : Prop → M), ∑ p, f p = f True + f False
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
/-- `condExpL2` commutes with taking inner products with constants. See the lemma
`condExpL2_comp_continuousLinearMap` for a more general result about commuting with continuous
linear maps.  -/
MeasureTheory.condExpL2_const_inner : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E 2 μ)) (c : E),
  ↑↑↑((MeasureTheory.condExpL2 𝕜 𝕜 hm) (MeasureTheory.MemLp.toLp (fun a => inner 𝕜 c (↑↑f a)) ⋯)) =ᵐ[μ] fun a =>
    inner 𝕜 c (↑↑↑((MeasureTheory.condExpL2 E 𝕜 hm) f) a)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- The functor sending a topological space `X` to its fundamental groupoid.  -/
FundamentalGroupoid.fundamentalGroupoidFunctor : CategoryTheory.Functor TopCat CategoryTheory.Grpd
-- Mathlib.Algebra.Ring.Commute
neg_sq : ∀ {R : Type u} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R), (-a) ^ 2 = a ^ 2
-- Mathlib.Data.Set.Functor
Set.mem_coe_of_mem : ∀ {α : Type u} {β : Set α} {γ : Set ↑β} {a : α} (ha : a ∈ β),
  ⟨a, ha⟩ ∈ γ →
    a ∈ do
      let a ← γ
      pure ↑a
-- Mathlib.Topology.SmallInductiveDimension
HasSmallInductiveDimensionLT.zero : ∀ {X : Type u} [inst : TopologicalSpace X] [IsEmpty X], HasSmallInductiveDimensionLT X 0
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.repr_support_subset_of_mem_span : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (s : Set ι) {m : M}, m ∈ Submodule.span R (⇑b '' s) → ↑(b.repr m).support ⊆ s
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.fst_comp_prodComm : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂],
  LinearMap.fst R M₂ M ∘ₗ ↑(LinearEquiv.prodComm R M M₂) = LinearMap.snd R M M₂
-- Init.Control.StateRef
/-- Retrieves the current value of the monad's mutable state.

This increments the reference count of the state, which may inhibit in-place updates.
 -/
StateRefT'.get : {ω σ : Type} → {m : Type → Type} → [MonadLiftT (ST ω) m] → StateRefT' ω σ m σ
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.add_mul_left_left : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → ∀ (z : R), IsRelPrime (x + y * z) y