mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.PreservesEqualizer.iso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasEqualizer f g]
  [inst_3 : CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G],
  CategoryTheory.Limits.PreservesEqualizer.iso G f g = CategoryTheory.Limits.PreservesEqualizer.iso G f g
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.coyonedaEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)}
  (f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F),
  CategoryTheory.coyonedaEquiv f = (CategoryTheory.ConcreteCategory.hom (f.app X)) (CategoryTheory.CategoryStruct.id X)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.disjoint_nhdsWithin_cofinite_of_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y]
  (f : Function.locallyFinsuppWithin U Y), ∀ p ∈ U, Disjoint (nhdsWithin p f.support) Filter.cofinite
-- Init.Data.UInt.Lemmas
instCommutativeUInt16HAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- **Alias** of `MonoidAlgebra.mapAlgHom`.

---

The algebra homomorphism of monoid algebras induced by a homomorphism of the base algebras.  -/
MonoidAlgebra.mapRangeAlgHom : {R : Type u_1} →
  {A : Type u_4} →
    {B : Type u_5} →
      (M : Type u_7) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] → [inst_5 : Monoid M] → (A →ₐ[R] B) → MonoidAlgebra A M →ₐ[R] MonoidAlgebra B M
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- The image under an onto linear map of a finite-dimensional space is also finite-dimensional.  -/
LinearMap.finiteDimensional_of_surjective : ∀ {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₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂),
  f.range = ⊤ → FiniteDimensional K V₂
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isEmpty_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub_nsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIocDiv hp a (b - m • p) = toIocDiv hp a b - ↑m
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valuation.norm_def : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀)
  [hv : v.RankOne] {x : L}, v.norm x = ↑((Valuation.RankOne.hom v) (v.restrict x))
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.ofIso_commShiftIso_hom_app : ∀ {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] {F G : CategoryTheory.Functor C D} (e : F ≅ G) (A : Type u_4)
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F.CommShift A] (a : A) (X : C),
  (CategoryTheory.Functor.commShiftIso G a).hom.app X =
    CategoryTheory.CategoryStruct.comp (e.inv.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).hom.app X)
        ((CategoryTheory.shiftFunctor D a).map (e.hom.app X)))
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.mk.injEq : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (simplex : Y.obj (Opposite.op { len := d }))
  (nonDegenerate : simplex ∈ Y.nonDegenerate d)
  (notMem : simplex ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d }))))
  (simplex_1 : Y.obj (Opposite.op { len := d })) (nonDegenerate_1 : simplex_1 ∈ Y.nonDegenerate d)
  (notMem_1 : simplex_1 ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d })))),
  ({ simplex := simplex, nonDegenerate := nonDegenerate, notMem := notMem } =
      { simplex := simplex_1, nonDegenerate := nonDegenerate_1, notMem := notMem_1 }) =
    (simplex = simplex_1)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsCocircuit.isNonloop_of_mem : ∀ {α : Type u_1} {M : Matroid α} {e : α} {K : Set α}, M.IsCocircuit K → e ∈ K → M.IsNonloop e
-- Mathlib.CategoryTheory.Functor.Functorial
CategoryTheory.Functorial.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : C → D} →
          (map : {X Y : C} → (X ⟶ Y) → (F X ⟶ F Y)) →
            autoParam (∀ {X : C}, map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (F X))
                CategoryTheory.Functorial.map_id._autoParam →
              autoParam
                  (∀ {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z},
                    map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map f) (map g))
                  CategoryTheory.Functorial.map_comp._autoParam →
                CategoryTheory.Functorial F
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- The trivial square-zero extension is nontrivial if it is over a nontrivial ring.  -/
TrivSqZeroExt.instNontrivial_of_left : ∀ {R : Type u_3} {M : Type u_4} [Nontrivial R] [Nonempty M], Nontrivial (TrivSqZeroExt R M)
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore minuend of a difference.  -/
AddOreLocalization.oreMin : {R : Type u_1} → [inst : AddMonoid R] → {S : AddSubmonoid R} → [AddOreLocalization.AddOreSet S] → R → ↥S → R
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_iff_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C)
  [inst_1 : ∀ (A : C), CategoryTheory.Limits.HasProduct fun x => G],
  CategoryTheory.IsCoseparator G ↔ ∀ (A : C), CategoryTheory.Mono (CategoryTheory.Limits.Pi.lift fun f => f)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.smul_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) {U V : Cᵒᵖ} (f : U ⟶ V) (r : ↑(R.obj U)),
  CategoryTheory.CategoryStruct.comp ((M.obj U).smul r) (M.presheaf.map f) =
    CategoryTheory.CategoryStruct.comp (M.presheaf.map f)
      ((M.obj V).smul ((CategoryTheory.ConcreteCategory.hom (R.map f)) r))
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- **Alias** of the forward direction of `tendstoUniformlyOn_iff_tendstoUniformlyOnFilter`. -/
TendstoUniformlyOn.tendstoUniformlyOnFilter : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι}, TendstoUniformlyOn F f p s → TendstoUniformlyOnFilter F f p (Filter.principal s)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A subgroup containing the stabilizer of `a`
is the stabilizer of the orbit of `a` under that subgroup  -/
AddAction.stabilizer_orbit_eq : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {a : X} {H : AddSubgroup G},
  AddAction.stabilizer G a ≤ H → AddAction.stabilizer G (AddAction.orbit (↥H) a) = H
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.P : {n : ℕ} → (F : TypeVec.{u} n → Type u_1) → [self : MvQPF F] → MvPFunctor.{u} n
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.SMulInvariantMeasure.smul : ∀ {M : Type v} {α : Type w} [inst : SMul M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.SMulInvariantMeasure M α μ] (c : ENNReal), MeasureTheory.SMulInvariantMeasure M α (c • μ)
-- Mathlib.Tactic.ClickSuggestions.Util
/-- If `motiveTypeCorrect := true`, we suggest `rw!` instead of `rw`.
If `occ := some n`, we suggest `nth_rw n` instead of `rw`.  -/
Mathlib.Tactic.ClickSuggestions.RwKind.valid : Bool → Option ℕ → Mathlib.Tactic.ClickSuggestions.RwKind
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- The adjunction between pushforward along `Over.map` and pushforward along `Over.pullback`.  -/
SheafOfModules.overMapPushforwardAdj : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) →
        [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
          {X Y : C} → (f : X ⟶ Y) → SheafOfModules.overMap R f ⊣ SheafOfModules.overPullback R f
-- Init.Data.Float.Model.Float
Float.Model.mk.sizeOf_spec : ∀ (toBits : UInt64) (valid : Float.Model.Format.binary64.Valid toBits.toBitVec),
  sizeOf { toBits := toBits, valid := valid } = 1 + sizeOf toBits + sizeOf valid
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.hG : Primrec Nat.Partrec.Code.G✝
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false →
    ∀ {km fallback : α}, t.minKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_zero_measure : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}, AEMeasurable f 0
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.ofGradedObject_toGradedObject : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂)
  (X : CategoryTheory.GradedObject (I₁ × I₂) C) (d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂))
  (d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂'))
  (shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0)
  (shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0)
  (d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₁ i₁' i₁'' i₂) = 0)
  (d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₂ i₁ i₂' i₂'') = 0)
  (comm :
    ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂),
      CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₂ i₁' i₂ i₂') =
        CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₁ i₁ i₁' i₂')),
  (HomologicalComplex₂.ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).toGradedObject = X
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coeToMvPowerSeries.algHom_apply : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (φ : MvPolynomial σ R) (A : Type u_3) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A], (MvPolynomial.coeToMvPowerSeries.algHom A) φ = (MvPowerSeries.map (algebraMap R A)) ↑φ
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.fst_comp_inl : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0],
  (MonoidWithZeroHom.fst G₀ H₀).comp (MonoidWithZeroHom.inl G₀ H₀) = MonoidWithZeroHom.id G₀
-- Aesop.Tree.Data
Aesop.Iteration.instLT : LT Aesop.Iteration
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
/-- The functor `HomologicalComplex (Karoubi C) c ⥤ Karoubi (HomologicalComplex C c)`,
on morphisms  -/
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {K L : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c} →
            (K ⟶ L) →
              (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K ⟶
                CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj L)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] {l : List α} {k : α}
  {h' : k ∈ Std.DTreeMap.Const.insertManyIfNewUnit t l} (contains : k ∈ t),
  (Std.DTreeMap.Const.insertManyIfNewUnit t l).getKey k h' = t.getKey k contains
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {f : (a : α) → β a → Bool} {k : α} {h' : k ∈ Std.DHashMap.Raw.filter f m} (h : m.WF),
  (Std.DHashMap.Raw.filter f m).getKey k h' = m.getKey k ⋯
-- Mathlib.NumberTheory.Bernoulli
bernoulli_two : bernoulli 2 = 6⁻¹
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p p_1 : S' ⟶ S} (e_p : p = p_1) {ι' : Type t'} {X' : ι' → C}
  {f' f'_1 : (j : ι') → X' j ⟶ S'} (e_f' : f' = f'_1) {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  (D : F.DescentData f) ⦃Y : C⦄ (q q_1 : Y ⟶ S') (e_q : q = q_1) ⦃j₁ j₂ : ι'⦄ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂)
  (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f' j₁) = q) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f' j₂) = q),
  CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom w D q f₁ f₂ hf₁ hf₂ =
    CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom ⋯ D q_1 f₁ f₂ ⋯ ⋯
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- The set of row stochastic matrices is convex.  -/
Matrix.convex_rowStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R], Convex R ↑(Matrix.rowStochastic R n)
-- Mathlib.Algebra.Lie.Basic
LieHom.mk.injEq : ∀ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (toLinearMap : L →ₗ[R] L')
  (map_lie' : ∀ {x y : L}, toLinearMap.toFun ⁅x, y⁆ = ⁅toLinearMap.toFun x, toLinearMap.toFun y⁆)
  (toLinearMap_1 : L →ₗ[R] L')
  (map_lie'_1 : ∀ {x y : L}, toLinearMap_1.toFun ⁅x, y⁆ = ⁅toLinearMap_1.toFun x, toLinearMap_1.toFun y⁆),
  ({ toLinearMap := toLinearMap, map_lie' := map_lie' } = { toLinearMap := toLinearMap_1, map_lie' := map_lie'_1 }) =
    (toLinearMap = toLinearMap_1)
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
/-- `expNegInvGlue` is the real function given by `x ↦ exp (-1/x)` for `x > 0` and `0`
for `x ≤ 0`. It is a basic building block to construct smooth partitions of unity. Its main property
is that it vanishes for `x ≤ 0`, it is positive for `x > 0`, and the junction between the two
behaviors is flat enough to retain smoothness. The fact that this function is `C^∞` is proved in
`expNegInvGlue.contDiff`.  -/
expNegInvGlue : ℝ → ℝ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.ofList_cons : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {k : α} {v : β k} {tl : List ((a : α) × β a)},
  Std.DTreeMap.Raw.ofList (⟨k, v⟩ :: tl) cmp = (∅.insert k v).insertMany tl
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k fallback : α}, l.contains k = false → (Std.DTreeMap.Raw.Const.unitOfList l cmp).getKeyD k fallback = fallback
-- Mathlib.Data.Set.Lattice.Image
Set.image2_iInter_subset_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (f : α → β → γ) (s : ι → Set α) (t : Set β),
  Set.image2 f (⋂ i, s i) t ⊆ ⋂ i, Set.image2 f (s i) t
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.get : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      (a : α) →
        (l : Std.DHashMap.Internal.AssocList α fun x => β) → Std.DHashMap.Internal.AssocList.contains a l = true → β
-- Lean.Meta.Sym.Canon
/-- Canonicalize `e` and apply post reductions.  -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonAppAndPost : Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.RingTheory.Ideal.IsPrincipal
/-- The non-zero-divisors principal ideals of `R` form a submonoid of `(Ideal R)⁰`.  -/
Ideal.isPrincipalNonZeroDivisorsSubmonoid : (R : Type u_1) → [inst : CommRing R] → Submonoid ↥(nonZeroDivisors (Ideal R))
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd_assoc_inv_app_assoc : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a₁ a₂ a₃ : A) (X : C) {Z : C}
  (h : (CategoryTheory.shiftFunctor C (a₁ + a₂ + a₃)).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).inv.app X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctorAdd C a₂ a₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).inv.app X)
        h)
-- Mathlib.Data.Finset.Union
Finset.image_biUnion : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq β] [inst_1 : DecidableEq γ] {f : α → β}
  {s : Finset α} {t : β → Finset γ}, (Finset.image f s).biUnion t = s.biUnion fun a => t (f a)
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_lt_left : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ y < x ↔ ¬Disjoint y x
-- Init.Data.List.Control
List.findSome?_eq_findSomeM? : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {as : List α},
  List.findSome? f as = (List.findSomeM? (fun x => pure (f x)) as).run
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyGTD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.Equiv t₂ → t₁.getKeyGTD k fallback = t₂.getKeyGTD k fallback
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.instPowNat : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → Pow (SpecialLinearGroup R V) ℕ
-- Batteries.Tactic.PrintPrefix
/-- Exclude declarations whose types are not propositions.  -/
Batteries.Tactic.PrintPrefixConfig.propositionsOnly : Batteries.Tactic.PrintPrefixConfig → Bool
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instReduced : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p],
  IsReduced (PerfectClosure K p)
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
catalan.eq_2 : ∀ (n : ℕ), catalan n.succ = ∑ i, catalan ↑i * catalan (n - ↑i)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsMarkovKernel.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsMarkovKernel κ],
  ProbabilityTheory.IsMarkovKernel κ.fst
-- Init.Grind.Attr
Lean.Parser.Attr.grindMod : Lean.ParserDescr
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodComm_symm_apply : ∀ (M : Type u_1) (N : Type u_2) [inst : MulOneClass M] [inst_1 : MulOneClass N],
  ⇑(MulEquiv.coprodComm M N).symm = ⇑(Monoid.Coprod.swap N M)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_bdEqual : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M}
  (t₁ t₂ : L.Term (α ⊕ Fin l)),
  (t₁.bdEqual t₂).Realize v xs ↔
    FirstOrder.Language.Term.realize (Sum.elim v xs) t₁ = FirstOrder.Language.Term.realize (Sum.elim v xs) t₂
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.drain_eq_fold : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] {it : Std.IterM m β},
  it.drain = Std.IterM.fold (fun x x_1 => PUnit.unit) PUnit.unit it
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.cast_add_one_pos : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [NeZero 1]
  (n : ℕ), 0 < ↑n + 1
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_eq_tmod : ∀ {a b : ℤ},
  a.fmod b =
    a.tmod b + if b ∣ a then 0 else if 0 ≤ a then if 0 ≤ b then 0 else b else if 0 ≤ b then ↑b.natAbs else 2 * ↑b.toNat
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.op_symm_apply_symm_apply : ∀ {α : Type u_7} {β : Type u_8} [inst : Add α] [inst_1 : Mul α] [inst_2 : Add β] [inst_3 : Mul β] (f : αᵐᵒᵖ ≃+* βᵐᵒᵖ)
  (a : β), (RingEquiv.op.symm f).symm a = MulOpposite.unop (f.symm (MulOpposite.op a))
-- Mathlib.Order.Closure
ClosureOperator.mk₂_apply : ∀ {α : Type u_1} [inst : PartialOrder α] (f : α → α) (hf : ∀ (x : α), x ≤ f x) (hmin : ∀ ⦃x y : α⦄, x ≤ f y → f x ≤ f y)
  (a : α), (ClosureOperator.mk₂ f hf hmin) a = f a
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.Context.val : Lean.Elab.ComputedFields.Context → Lean.Expr
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.mod_add_div : ∀ {R : Type u} [inst : EuclideanDomain R] (a b : R), a % b + b * (a / b) = a
-- Mathlib.CategoryTheory.Sites.Over
/-- The Grothendieck topology on `Over X`, obtained from localizing the topology generated
by the precoverage `K`, is generated by the preimage of `K`.  -/
CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (K : CategoryTheory.Precoverage C) [K.HasPullbacks]
  [K.IsStableUnderBaseChange] (X : C),
  K.toGrothendieck.over X = (CategoryTheory.Precoverage.comap (CategoryTheory.Over.forget X) K).toGrothendieck
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.isCoboundedUnder_le : ∀ {α : Type u_1} {γ : Type u_3} {u : γ → α} {l : Filter γ} [inst : Preorder α] [l.NeBot],
  Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l u → Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) l u
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.denoteS.match_1.splitter : (motive : Lean.Grind.CommRing.Expr → Sort u_1) →
  (x : Lean.Grind.CommRing.Expr) →
    ((k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k)) →
      ((k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k)) →
        ((v : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var v)) →
          ((a b : Lean.Grind.CommRing.Expr) → motive (a.add b)) →
            ((a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) →
              ((a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) →
                ((a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) →
                  ((a : Lean.Grind.CommRing.Expr) → motive a.neg) →
                    ((k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) → motive x
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C) [S.HasHomology] [inst_3 : CategoryTheory.Limits.HasKernel S.g],
  S.Exact ↔ CategoryTheory.Epi (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.hausdorffMeasure_zero_singleton : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (x : X),
  (MeasureTheory.Measure.hausdorffMeasure 0) {x} = 1