mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Irreducible
ProbabilityTheory.Kernel.isIrreducible_of_le_measure : ∀ {α : Type u_1} {mα : MeasurableSpace α} {φ₁ φ₂ : MeasureTheory.Measure α},
  φ₁ ≤ φ₂ →
    ∀ {κ : ProbabilityTheory.Kernel α α} [hκ : ProbabilityTheory.Kernel.IsIrreducible φ₂ κ],
      ProbabilityTheory.Kernel.IsIrreducible φ₁ κ
-- Mathlib.Order.Category.FinBoolAlg
/-- Constructs an equivalence between finite Boolean algebras from an order isomorphism between
them.  -/
FinBoolAlg.Iso.mk : {α β : FinBoolAlg} → ↑α.toBoolAlg ≃o ↑β.toBoolAlg → (α ≅ β)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.eta.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F),
  c.eta = CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl c.pt) ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {W W' : CategoryTheory.MorphismProperty C},
  W = W' ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- Given a family of kernels `κ n` from `X 0 × ... × X n` to `X (n + 1)` for all `n`,
construct a kernel from `X 0 × ... × X a` to `X 0 × ... × X b` by iterating `κ`.

The idea is that the input is some trajectory up to time `a`, and the output is the distribution
of the trajectory up to time `b`. In particular if `b ≤ a`, this is just a deterministic kernel
(see `partialTraj_le`). The name `partialTraj` stands for "partial trajectory".

This kernel can be extended into a kernel with codomain `Π n, X n` via the Ionescu-Tulcea theorem.
 -/
ProbabilityTheory.Kernel.partialTraj : {X : ℕ → Type u_1} →
  {mX : (n : ℕ) → MeasurableSpace (X n)} →
    ((n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) →
      (a b : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic a)) → X ↑i) ((i : ↥(Finset.Iic b)) → X ↑i)
-- Mathlib.CategoryTheory.Discrete.Basic
/-- The "Discrete" category on a type, whose morphisms are equalities.

Because we do not allow morphisms in `Prop` (only in `Type`),
somewhat annoyingly we have to define `X ⟶ Y` as `ULift (PLift (X = Y))`.  -/
CategoryTheory.discreteCategory : (α : Type u₁) → CategoryTheory.SmallCategory (CategoryTheory.Discrete α)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_beq : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α} (h' : a ∈ m), (m.getKey a h' == a) = true
-- Mathlib.ModelTheory.Definability
/-- **Alias** of the forward direction of `Set.termDefinable₁_iff_termDefinable`.

---

`TermDefinable₁` is defined as `TermDefinable` on the `Unit` index type.  -/
Set.TermDefinable₁.termDefinable : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] (f : M → M),
  Set.TermDefinable₁ L f → A.TermDefinable L fun v => f (v ())
-- Mathlib.Data.Seq.Computation
Computation.results_thinkN : ∀ {α : Type u} {s : Computation α} {a : α} {m : ℕ} (n : ℕ), s.Results a m → (s.thinkN n).Results a (m + n)
-- Init.Data.List.Nat.Prod
List.prod_eq_zero_iff_exists_zero_nat : ∀ {l : List ℕ}, l.prod = 0 ↔ ∃ x ∈ l, x = 0
-- Init.Data.Nat.MinMax
Nat.min_eq_left : ∀ {a b : ℕ}, a ≤ b → min a b = a
-- Init.Data.SInt.Basic
/-- Computes the absolute value of a word-sized signed integer.

This function is equivalent to `if a < 0 then -a else a`, so in particular `ISize.minValue` will be
mapped to `ISize.minValue`.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.abs : ISize → ISize
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.self_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {kmi : α}, (t.insertIfNew k v).maxKey?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Lean.Data.AssocList
Lean.AssocList.all : {α : Type u} → {β : Type v} → (α → β → Bool) → Lean.AssocList α β → Bool
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (self : F.CoreMonoidal) {X Y : C} (X' : C) (f : X ⟶ Y) {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X' Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f))
      (CategoryTheory.CategoryStruct.comp (self.μIso X' Y).hom h) =
    CategoryTheory.CategoryStruct.comp (self.μIso X' X).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f)) h)
-- Mathlib.Topology.UniformSpace.Cauchy
Cauchy.mono' : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α}, Cauchy f → g.NeBot → g ≤ f → Cauchy g
-- Mathlib.MeasureTheory.Function.EssSup
OrderIso.essInf_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice β] {x : MeasurableSpace α} {γ : Type u_3}
  [inst_1 : ConditionallyCompleteLattice γ] (f : α → β) (μ : MeasureTheory.Measure α) (g : β ≃o γ),
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) f) OrderIso.essInf_apply._auto_1 →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) f) OrderIso.essInf_apply._auto_3 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) fun x => g (f x))
          OrderIso.essInf_apply._auto_5 →
        autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) fun x => g (f x))
            OrderIso.essInf_apply._auto_7 →
          g (essInf f μ) = essInf (fun x => g (f x)) μ
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn_zero : ∀ {a : ℕ} (a1 : 1 < a), Pell.xn a1 0 = 1
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.finite_one : ∀ {α : Type u_2} [inst : One α], Set.Finite 1
-- Mathlib.Algebra.Divisibility.Units
/-- **Alias** of `symm_isRelPrime`. -/
symmetric_isRelPrime : ∀ {α : Type u_1} [inst : CommMonoid α], Std.Symm IsRelPrime
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.coprod_comp_inr : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommMonoid P] (f : M →+ P) (g : N →+ P), (f.coprod g).comp (AddMonoidHom.inr M N) = g
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgHom.mem_range : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (φ : F) {y : B},
  y ∈ NonUnitalStarAlgHom.range φ ↔ ∃ x, φ x = y
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The adjoint is unique: a map `A` is the adjoint of `B` iff it satisfies `⟪A x, y⟫ = ⟪x, B y⟫`
for all `x` and `y`.  -/
ContinuousLinearMap.eq_adjoint_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F) (B : F →L[𝕜] E),
  A = ContinuousLinearMap.adjoint B ↔ ∀ (x : E) (y : F), inner 𝕜 (A x) y = inner 𝕜 x (B y)
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredGenerator : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {κ : Cardinal.{w}} {inst_1 : Fact κ.IsRegular}
  [self : CategoryTheory.IsCardinalAccessibleCategory C κ], CategoryTheory.HasCardinalFilteredGenerator C κ
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.Disjoint.cycleType_noncommProd : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {ι : Type u_2} {k : ι → Equiv.Perm α} {s : Finset ι}
  (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
  (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
  (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
-- Mathlib.Order.Filter.Pointwise
IsAddUnit.vadd_tendsto_vadd_iff : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : AddMonoid γ] [inst_1 : AddAction γ β] {m : α → β} {c : γ}
  {f : Filter α} {g : Filter β}, IsAddUnit c → (Filter.Tendsto (c +ᵥ m) f (c +ᵥ g) ↔ Filter.Tendsto m f g)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- notation for categorical products. We need `ᶜ` to avoid conflict with `Finset.prod`.  -/
CategoryTheory.Limits.«term∏ᶜ_» : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.incl_idealRange : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  I.incl.idealRange = I
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicForallTraj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ),
  ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.traj κ a)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- Making this a global instance would make the typeclass search go in an infinite loop.  -/
CategoryTheory.Limits.hasPushout_symmetry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [CategoryTheory.Limits.HasPushout f g], CategoryTheory.Limits.HasPushout g f
-- Mathlib.Tactic.MinImports
/-- `getIds stx` extracts all identifiers, collecting them in a `NameSet`.  -/
Mathlib.Command.MinImports.getIds : Lean.Syntax → Lean.NameSet
-- Mathlib.Topology.Order.IntermediateValue
isPreconnected_Ioc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, IsPreconnected (Set.Ioc a b)
-- Mathlib.Algebra.Group.Defs
AddRightCancelMonoid.mk : {M : Type u} → [toAddMonoid : AddMonoid M] → [toIsRightCancelAdd : IsRightCancelAdd M] → AddRightCancelMonoid M
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpoint.fixpointType : Lean.Elab.PartialFixpoint → Lean.Elab.PartialFixpointType
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.coeff_modOf_of_not_exists_add : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] (x : AddMonoidAlgebra k G) (g g' : G),
  (¬∃ d, g' = g + d) → (x.modOf g).coeff g' = x.coeff g'
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.d_sndX_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel i j) {Z : C} (h : G.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ j) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ i j hij) (φ.f j) +
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ i) (G.d i j))
      h
-- Mathlib.Topology.Compactness.Lindelof
/-- For every nonempty open cover of a Lindelöf set, there exists a subcover indexed by ℕ.  -/
IsLindelof.indexed_countable_subcover : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v} [Nonempty ι],
  IsLindelof s → ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ f, s ⊆ ⋃ n, U (f n)
-- Mathlib.Order.Interval.Finset.Fin
Fin.instLocallyFiniteOrder : (n : ℕ) → LocallyFiniteOrder (Fin n)
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_comp_of_right : ∀ {𝕜 : 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'] {H'' : Type u_8}
  [inst_11 : TopologicalSpace H''] {E'' : Type u_9} [inst_12 : NormedAddCommGroup E''] [inst_13 : NormedSpace 𝕜 E'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {g : M' → M''} {f : M → M'} {V : (x : M'') → TangentSpace I'' x} {s : Set M} {t : Set M'} {x₀ : M},
  MDiffAt[t] g (f x₀) →
    Set.MapsTo f s t →
      UniqueMDiffAt[s] x₀ →
        (mfderiv[s] f x₀).IsInvertible →
          VectorField.mpullbackWithin I I'' (g ∘ f) V s x₀ =
            VectorField.mpullbackWithin I I' f (VectorField.mpullbackWithin I' I'' g V t) s x₀
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitIsoFlipCompLim_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K),
  (CategoryTheory.Limits.limitIsoFlipCompLim F).hom.app X =
    (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F X).hom
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.tensorUnit_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit P.FullSubcategory).obj =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.CategoryTheory.Yoneda
/-- An isomorphism between a corepresentable `F` and a functor of the form
`C(F.corepr X, -)`. Note the components `F.coreprW.app X`
definitionally have type `F.corepr_X ⟶ X ≅ F.obj X`.
 -/
CategoryTheory.Functor.coreprW : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor C (Type v₁)) →
      [inst_1 : F.IsCorepresentable] → CategoryTheory.coyoneda.obj (Opposite.op F.coreprX) ≅ F
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.range_polarizationIn : ∀ {ι : 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) [inst_5 : Fintype ι],
  Submodule.map P.Polarization (P.rootSpan R) = (P.PolarizationIn R).range
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_map_left : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {M₂ : Type u_5} [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂] (f : M₂ →ₗ[R] N →ₗ[R] P)
  (g : M →ₗ[R] M₂) (p : Submodule R M) (q : Submodule R N),
  Submodule.map₂ f (Submodule.map g p) q = Submodule.map₂ (f ∘ₗ g) p q
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk_homMk : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {x y : V} (e : x ⟶ y),
  CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk V (CategoryTheory.Cat.FreeRefl.homMk e)
-- Mathlib.Algebra.Group.Hom.Defs
instOneMulHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : MulOneClass N],
  instOneMulHom = { one := { toFun := fun x => 1, map_mul' := ⋯ } }
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- Proving equality between reflexive prefunctors. This isn't an extensionality lemma,
because usually you don't really want to do this.  -/
CategoryTheory.ReflPrefunctor.ext : ∀ {V : Type u} [inst : CategoryTheory.ReflQuiver V] {W : Type u₂} [inst_1 : CategoryTheory.ReflQuiver W] {F G : V ⥤rq W}
  (h_obj : ∀ (X : V), F.obj X = G.obj X), (∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))) → F = G
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.mk₂'ₛₗ_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  (f : M → N → P) {H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n}
  {H2 : ∀ (c : R) (m : M) (n : N), f (c • m) n = ρ₁₂ c • f m n}
  {H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂}
  {H4 : ∀ (c : S) (m : M) (n : N), f m (c • n) = σ₁₂ c • f m n} (m : M) (n : N),
  ((LinearMap.mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4) m) n = f m n
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_nonempty : ∀ {α : Type u_1} [inst : LE α] {s : LowerSet α}, (↑s).Nonempty ↔ s ≠ ⊥
-- Mathlib.Data.Rat.NatSqrt.Defs
Nat.ratSqrt_sq_le : ∀ (x : ℕ) {prec : ℕ}, 0 < prec → x.ratSqrt prec ^ 2 ≤ ↑x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
CategoryTheory.yonedaCommRing_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (R : CategoryTheory.CommRingObjCat C),
  CategoryTheory.yonedaCommRing.obj R = CategoryTheory.yonedaCommRingObj R.X
-- Mathlib.Logic.Equiv.Basic
Function.piCongrLeft'_symm_update : ∀ {α : Sort u_1} {β : Sort u_4} [inst : DecidableEq α] [inst_1 : DecidableEq β] (P : α → Sort u_10) (e : α ≃ β)
  (f : (b : β) → P (e.symm b)) (b : β) (x : P (e.symm b)),
  (Equiv.piCongrLeft' P e).symm (Function.update f b x) = Function.update ((Equiv.piCongrLeft' P e).symm f) (e.symm b) x
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isTangent_orthRadius_iff_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P}, s.IsTangent (s.orthRadius p) ↔ p ∈ s
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- Inversion as a measurable automorphism of a group or group with zero.  -/
MeasurableEquiv.inv : (G : Type u_4) → [inst : MeasurableSpace G] → [inst_1 : InvolutiveInv G] → [MeasurableInv G] → G ≃ᵐ G
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
/-- Left whiskering of an oplax natural transformation and a modification.  -/
CategoryTheory.Lax.OplaxTrans.whiskerLeft : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.LaxFunctor B C} →
          (η : F ⟶ G) →
            {θ ι : G ⟶ H} → (θ ⟶ ι) → (CategoryTheory.CategoryStruct.comp η θ ⟶ CategoryTheory.CategoryStruct.comp η ι)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapId_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictlyUnitaryPseudofunctor B C)
  (G : CategoryTheory.StrictlyUnitaryPseudofunctor C D) (a : B),
  ((F.comp G).mapId a).inv = CategoryTheory.CategoryStruct.comp (G.mapId (F.obj a)).inv (G.map₂ (F.mapId a).inv)
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_apply : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  [inst_2 : LinearOrderedAddCommMonoidWithTop Γ'₀] (f : Γ₀ →+ Γ'₀) (ht : f ⊤ = ⊤) (hf : Monotone ⇑f)
  (v : AddValuation R Γ₀) (r : R), (AddValuation.map f ht hf v) r = f (v r)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrp.instMonoidal : {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] →
            [inst_4 : CategoryTheory.BraidedCategory C] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                (F : CategoryTheory.Functor C D) → [inst_6 : F.Braided] → F.mapGrp.Monoidal
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_eq_some_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false}, t.minKey? = some (t.minKey he)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_insertIfNew!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, k ∈ Std.DTreeMap.Internal.Impl.insertIfNew! k v t
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.add.injEq : ∀ (k : ℤ) (v : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly) (k_1 : ℤ) (v_1 : Lean.Grind.Linarith.Var)
  (p_1 : Lean.Grind.Linarith.Poly),
  (Lean.Grind.Linarith.Poly.add k v p = Lean.Grind.Linarith.Poly.add k_1 v_1 p_1) = (k = k_1 ∧ v = v_1 ∧ p = p_1)
-- Mathlib.Analysis.Calculus.Deriv.Prod
hasDerivAtFilter_pi : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {L : Filter (𝕜 × 𝕜)} {ι : Type u_1} {E' : ι → Type u_2}
  [inst_1 : (i : ι) → NormedAddCommGroup (E' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E' i)] {φ : 𝕜 → (i : ι) → E' i}
  {φ' : (i : ι) → E' i}, HasDerivAtFilter φ φ' L ↔ ∀ (i : ι), HasDerivAtFilter (fun x => φ x i) (φ' i) L
-- Init.Data.List.Sort.Lemmas
List.MergeSort.Internal.splitInTwo_snd_pairwise : ∀ {α : Type u_1} {n : ℕ} {le : α → α → Prop} (l : { l // l.length = n }),
  List.Pairwise le ↑l → List.Pairwise le ↑(List.MergeSort.Internal.splitInTwo l).2
-- Mathlib.Algebra.Group.Submonoid.Units
ofUnits_le_iff_le_units : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) (H : Subgroup Mˣ), H.ofUnits ≤ S ↔ H ≤ S.units
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.smul_sum : ∀ {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_5} [inst : Zero β] [inst_1 : AddCommMonoid M]
  [inst_2 : DistribSMul R M] {v : α →₀ β} {c : R} {h : α → β → M}, c • v.sum h = v.sum fun a b => c • h a b
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
/-- The residue map from the stalk to the residue field.  -/
AlgebraicGeometry.LocallyRingedSpace.residue : (X : AlgebraicGeometry.LocallyRingedSpace) → (x : ↑X.toTopCat) → X.presheaf.stalk x ⟶ X.residueField x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (l : List ((a : α) × β a)), (t₁.insertMany l).Equiv (t₂.insertMany l)
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.Hom.mk.inj : ∀ {R : Type u} {inst : CommRing R} {V W : HopfAlgCat R} {toBialgHom' toBialgHom'_1 : V.carrier →ₐc[R] W.carrier},
  { toBialgHom' := toBialgHom' } = { toBialgHom' := toBialgHom'_1 } → toBialgHom' = toBialgHom'_1
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.odd_nsmul_antiperiodic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddMonoid α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → ∀ (n : ℕ), Function.Antiperiodic f ((2 * n + 1) • c)
-- Init.Data.List.Nat.Range
List.map_sub_range' : ∀ {step a s : ℕ}, a ≤ s → ∀ (n : ℕ), List.map (fun x => x - a) (List.range' s n step) = List.range' (s - a) n step
-- Mathlib.GroupTheory.FreeAbelianGroup
/-- Isomorphic types have isomorphic free abelian groups.  -/
FreeAbelianGroup.equivOfEquiv : {α : Type u_2} → {β : Type u_3} → α ≃ β → FreeAbelianGroup α ≃+ FreeAbelianGroup β