mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.map_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q} (x : M), (f.map hy k) (f x) = k (g x)
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- A synonym for `M.obj.carrier`, which we can mark with `@[coe]`.  -/
FGModuleCat.carrier : {R : Type u} → [inst : Ring R] → FGModuleCat R → Type v
-- Init.Data.Range.Polymorphic.Fin
Fin.instLawfulHasSize_2 : ∀ {n : ℕ}, Std.Rxi.LawfulHasSize (Fin n)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If every finite diagram in `C` admits a cocone, then `C` is filtered. It is sufficient to verify
this for diagrams whose shape lives in any one fixed universe.  -/
CategoryTheory.IsFiltered.of_cocone_nonempty : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (∀ {J : Type w} [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
      (F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cocone F)) →
    CategoryTheory.IsFiltered C
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.neg_mul : ∀ {R : Type u_2} [inst : CommRing R] (a₁ : R) (a₂ : ℕ) {a₃ b : R}, -a₃ = b → -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b
-- Std.Tactic.BVDecide.Syntax
/-- The SAT solver configuration to use. Defaults to `.proof` as that is the most relevant use case
for `bv_decide`.
 -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.solverMode : Lean.Elab.Tactic.BVDecide.BVDecideConfig → Lean.Elab.Tactic.BVDecide.SolverMode
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.addEquiv_symm : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (e : M ≃+ N),
  (Finsupp.mapRange.addEquiv e).symm = Finsupp.mapRange.addEquiv e.symm
-- Mathlib.CategoryTheory.Limits.Opposites
/-- If `C` has colimits of shape `Jᵒᵖ`, we can construct limits in `Cᵒᵖ` of shape `J`.
 -/
CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C], CategoryTheory.Limits.HasColimitsOfShape J Cᵒᵖ
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_div' : ∀ (x : ℝ) {y : ℝ}, 0 ≤ y → √(x / y) = √x / √y
-- Mathlib.GroupTheory.OrderOfElement
infinite_powers : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] {a : G}, (↑(Submonoid.powers a)).Infinite ↔ ¬IsOfFinOrder a
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- A matrix algebra is isomorphic to the opposite of an endomorphism algebra.  -/
matrixAlgEquivEndVecMulOpposite : {ι : Type u_1} →
  [inst : Fintype ι] →
    [inst_1 : DecidableEq ι] →
      (R : Type u_2) →
        [inst_2 : CommSemiring R] →
          {A : Type u_3} → [inst_3 : Semiring A] → [inst_4 : Algebra R A] → Matrix ι ι A ≃ₐ[R] (Module.End A (ι → A))ᵐᵒᵖ
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instSub : {α : Type u_1} → [inst : AddCommGroup α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → Sub (LowerSet α)
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- If `f` and `g` are homotopic relative to a path object `P`, then `g` and `f`
are homotopic relative to `P.symm`.  -/
HomotopicalAlgebra.PathObject.RightHomotopy.symm : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        {P : HomotopicalAlgebra.PathObject Y} → {f g : X ⟶ Y} → P.RightHomotopy f g → P.symm.RightHomotopy g f
-- Mathlib.Topology.Sets.VietorisTopology
/-- Given a basis `B` on the underlying topological space, the Vietoris topology has a basis
consisting of sets of the form `{s | s ⊆ V, s ∩ U₁ ≠ ∅, …, s ∩ Uₙ ≠ ∅}`, where `U₁, …, Uₙ ∈ B` are
subsets of some open set `V`.  -/
TopologicalSpace.IsTopologicalBasis.vietoris : ∀ {α : Type u_1} [inst : TopologicalSpace α] {B : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis B →
    TopologicalSpace.IsTopologicalBasis
      ((fun p => {s | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
        {p | IsOpen p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
-- Mathlib.Topology.SmallInductiveDimension
hasSmallInductiveDimensionLT_one_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  HasSmallInductiveDimensionLT X 1 ↔ TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.instZero : {E : Type u_3} → [inst : AddGroup E] → Zero (NonarchAddGroupSeminorm E)
-- Std.Data.DTreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.DTreeMap.getKey? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Option α
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.IsPrestackFor.isSheafFor' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {S₀ : C}
  (S : CategoryTheory.Over S₀) {R : CategoryTheory.Sieve S},
  F.IsPrestackFor ((CategoryTheory.Sieve.overEquiv S) R).arrows →
    ∀ (M N : ↑(F.obj { as := Opposite.op S₀ })), CategoryTheory.Presieve.IsSheafFor (F.presheafHom M N) R.arrows
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.mk : {α : Type u_4} →
  (vertexSet : Set α) → (edgeSet : Set (Set α)) → (∀ ⦃e : Set α⦄, e ∈ edgeSet → e ⊆ vertexSet) → Hypergraph α
-- Lean.PrivateName
/-- Return `true` if `n` is of the form `_private.<module_name>.0`
See comment above.
 -/
Lean.isPrivatePrefix : Lean.Name → Bool
-- Mathlib.RingTheory.Etale.StandardEtale
/-- Mapping `StandardEtalePresentation` under `AlgEquiv`s.  -/
StandardEtalePresentation.mapEquiv : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R T] → StandardEtalePresentation R S → (S ≃ₐ[R] T) → StandardEtalePresentation R T
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `lowerHemicontinuousWithinAt_iff_frequently`. -/
LowerHemicontinuousWithinAt.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  {s : Set α},
  (∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ t) → f x ⊆ t) → LowerHemicontinuousWithinAt f s x
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationDesc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {T : AlgebraicGeometry.Scheme} (f₁ : X ⟶ T) (f₂ : T ⟶ Y)
  [inst_2 : AlgebraicGeometry.IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f)
      (AlgebraicGeometry.Scheme.Hom.normalizationDesc f f₁ f₂ H) =
    f₁
-- Mathlib.Data.Finset.Grade
Finset.empty_covBy_singleton : ∀ {α : Type u_1} (a : α), ∅ ⋖ {a}
-- Init.Data.List.Erase
List.erase_append : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {l₁ l₂ : List α},
  (l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a
-- Lean.CompactedRegion
/-- A compacted region holds multiple Lean objects in a contiguous memory region, which can be
read/written to/from disk. Objects inside the region do not have reference counters and cannot be
freed individually. The contents of `.olean` files are compacted regions.
 -/
Lean.CompactedRegion : Type
-- Lean.Meta.Tactic.Simp.Arith
Lean.Meta.Simp.Arith.parentIsTarget : Option Lean.Expr → Bool
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_sdiff_distrib : ∀ {α : Type u_1} {s t u : Set α}, (s ∪ t) \ u = s \ u ∪ t \ u
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fstHom_apply : ∀ (S : Type u_1) (R : Type u) (M : Type v) [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M]
  (x : TrivSqZeroExt R M), (TrivSqZeroExt.fstHom S R M) x = x.fst
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
MaximalSpectrum.mapPiLocalization_id : ∀ {R : Type u_1} [inst : CommSemiring R],
  MaximalSpectrum.mapPiLocalization (RingHom.id R) ⋯ = RingHom.id (MaximalSpectrum.PiLocalization R)
-- Mathlib.Analysis.Normed.Operator.Basic
/-- For a normed space `E`, continuous linear endomorphisms form a normed algebra with
respect to the operator norm.  -/
ContinuousLinearMap.toNormedAlgebra : {𝕜 : Type u_1} →
  {E : Type u_4} →
    [inst : SeminormedAddCommGroup E] →
      [inst_1 : NontriviallyNormedField 𝕜] → [inst_2 : NormedSpace 𝕜 E] → NormedAlgebra 𝕜 (E →L[𝕜] E)
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.WP.wp_econs_bot_le : ∀ {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] (x : Prog)
  (post : Value → Pred) (epost : EPred) {pre : Pred},
  Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x post Lean.Order.bot) →
    Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x post epost)
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extMk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X)
  [inst_3 : HasDerivedCategory C] {n : ℕ} (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m)
  (hf : CategoryTheory.CategoryStruct.comp (R.complex.d m n) f = 0),
  (R.extMk f m hm hf).hom =
    (CategoryTheory.ShiftedHom.mk₀ 0 ⋯
          (CategoryTheory.CategoryStruct.comp ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)
            (CategoryTheory.inv (DerivedCategory.Q.map R.π')))).comp
      ((CategoryTheory.ShiftedHom.map
            (CochainComplex.HomComplex.Cocycle.equivHomShift.symm
              (CochainComplex.HomComplex.Cocycle.toSingleMk
                (CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso (-↑n) n ⋯).hom f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q).comp
        (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯
-- Mathlib.Analysis.Normed.Affine.Ceva
/-- **Ceva's theorem** for a triangle, expressed in terms of multiplying distances.  -/
Affine.Triangle.prod_dist_eq_prod_dist_of_mem_line_of_mem_line : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : NormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {t : Affine.Triangle 𝕜 P}
  {p : Fin 3 → P} {p' : P},
  (∀ (i : Fin 3), p i ∈ line[𝕜, t.points (i + 1), t.points (i + 2)]) →
    (∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, p i]) →
      ∏ i, dist (t.points (i + 1)) (p i) = ∏ i, dist (p i) (t.points (i + 2))
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.coe_tsum : ∀ {α : Type u_2} {L : SummationFilter α} {f : α → NNReal}, ↑(∑'[L] (a : α), f a) = ∑'[L] (a : α), ↑(f a)
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkItem.f : Std.Format.WorkItem✝ → Std.Format
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (m.alter k f).contains k' = if (k == k') = true then (f m[k]?).isSome else m.contains k'
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isLongestMatchAtChain_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAtChain p pos pos' ↔
    pos ≤ pos' ∧ ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h : pos'' < pos'), p (pos''.get ⋯) = true
-- Mathlib.Algebra.Group.Pi.Basic
Pi.instIsLeftCancelAdd : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → Add (f i)] [∀ (i : I), IsLeftCancelAdd (f i)],
  IsLeftCancelAdd ((i : I) → f i)
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Icc_succ_top : ∀ {M : Type u_3} [inst : AddCommMonoid M] {a b : ℕ},
  a ≤ b + 1 → ∀ (f : ℕ → M), ∑ k ∈ Finset.Icc a (b + 1), f k = ∑ k ∈ Finset.Icc a b, f k + f (b + 1)
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.sum_prob_mem_Ioc_le : ∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  {X : Ω → ℝ},
  MeasureTheory.Integrable X MeasureTheory.volume →
    0 ≤ X →
      ∀ {K N : ℕ},
        K ≤ N →
          ∑ j ∈ Finset.range K, MeasureTheory.volume {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.w₀_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} (self : E.Hom F) (i : E.I₀) {Z : C} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.h₀ i) (CategoryTheory.CategoryStruct.comp (F.f (self.s₀ i)) h) =
    CategoryTheory.CategoryStruct.comp (E.f i) h
-- Mathlib.Order.Hom.Basic
OrderEmbedding.ofStrictMono.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : LinearOrder α] [inst_1 : Preorder β] (f f_1 : α → β) (e_f : f = f_1)
  (h : StrictMono f), OrderEmbedding.ofStrictMono f h = OrderEmbedding.ofStrictMono f_1 ⋯
-- Mathlib.Analysis.Convex.Between
Set.InjOn.wbtw_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] {x y z : P} {f : P →ᵃ[R] P'} {s : AffineSubspace R P},
  Set.InjOn ⇑f ↑s → x ∈ s → y ∈ s → z ∈ s → (Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z)
-- Mathlib.Algebra.Group.ConjFinite
instDecidableRelIsConjOfDecidableEqOfFintype : {α : Type u_1} → [inst : Monoid α] → [DecidableEq α] → [Fintype α] → DecidableRel IsConj
-- Mathlib.Algebra.GroupWithZero.Divisibility
eq_zero_of_zero_dvd : ∀ {α : Type u_1} [inst : SemigroupWithZero α] {a : α}, 0 ∣ a → a = 0
-- Lean.Data.KVMap
Lean.instBEqDataValue.beq : Lean.DataValue → Lean.DataValue → Bool
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.IsRightAdjoint.mk : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (adj : CategoryTheory.Bicategory.Adjunction f g), CategoryTheory.Bicategory.IsRightAdjoint g
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.reverse_coe : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v), ↑p.reverse = (↑p).reverse
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_insert_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback v : β k}, (m.insert k v).getD k fallback = v
-- Mathlib.Data.ZMod.Basic
ZMod.val_mul : ∀ {n : ℕ} (a b : ZMod n), (a * b).val = a.val * b.val % n
-- Mathlib.Data.Set.Insert
/-- Inserting an element to a set is equivalent to the option type.  -/
Set.subtypeInsertEquivOption : {α : Type u_1} → [DecidableEq α] → {t : Set α} → {x : α} → x ∉ t → { i // i ∈ insert x t } ≃ Option { i // i ∈ t }
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_neg_one_one : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R],
  Matrix.detp (-1) 1 = 0
-- Mathlib.Data.Finset.Preimage
Equiv.image_eq_preimage_symm_of_finset : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] (e : α ≃ β) (s : Finset α),
  Finset.image (⇑e) s = s.preimage ⇑e.symm ⋯
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.insert.eq_def : ∀ (k : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.insert k v p =
    match p with
    | Int.Internal.Linear.Poly.num k' => Int.Internal.Linear.Poly.add k v (Int.Internal.Linear.Poly.num k')
    | Int.Internal.Linear.Poly.add k' v' p =>
      bif Nat.blt v' v then Int.Internal.Linear.Poly.add k v (Int.Internal.Linear.Poly.add k' v' p)
      else
        bif Nat.beq v v' then if (k.add k' == 0) = true then p else Int.Internal.Linear.Poly.add (k.add k') v' p
        else Int.Internal.Linear.Poly.add k' v' (Int.Internal.Linear.Poly.insert k v p)
-- Mathlib.RingTheory.Localization.Algebra
IsLocalization.mapₐ.congr_simp : ∀ {R : Type u_5} [inst : CommSemiring R] (M M_1 : Submonoid R) (e_M : M = M_1) {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 f_1 : A →ₐ[R] B),
  f = f_1 → IsLocalization.mapₐ M Rₚ Aₚ Bₚ f = IsLocalization.mapₐ M_1 Rₚ Aₚ Bₚ f_1
-- Mathlib.SetTheory.Cardinal.Finite
Set.card_singleton_prod : ∀ {α : Type u_1} {β : Type u_2} (a : α) (t : Set β), Nat.card ↑({a} ×ˢ t) = Nat.card ↑t
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.instEntails : {α : Type u_1} →
  {β : Type u_2} → [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] → Std.Tactic.BVDecide.LRAT.Internal.Entails α β
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.monomorphisms.infer_property : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.Mono f],
  CategoryTheory.MorphismProperty.monomorphisms C f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- A function is `AEStronglyMeasurable` with respect to a measure `μ` if it is almost everywhere
equal to the limit of a sequence of simple functions.

One can specify the sigma-algebra according to which simple functions are taken using the
`AEStronglyMeasurable[m]` notation in the `MeasureTheory` scope.  -/
MeasureTheory.AEStronglyMeasurable : {α : Type u_1} →
  {β : Type u_2} →
    [TopologicalSpace β] →
      [m : MeasurableSpace α] →
        {m₀ : MeasurableSpace α} →
          (α → β) → autoParam (MeasureTheory.Measure α) MeasureTheory.AEStronglyMeasurable._auto_1 → Prop
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithTerminal.id.match_1.eq_2 : ∀ {C : Type u_1} (motive : CategoryTheory.WithTerminal C → Sort u_2)
  (h_1 : (a : C) → motive (CategoryTheory.WithTerminal.of a)) (h_2 : Unit → motive CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of a => h_1 a
    | CategoryTheory.WithTerminal.star => h_2 ()) =
    h_2 ()
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.insertMany_cons : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {l : List ((a : α) × β a)}
  {k : α} {v : β k}, t.insertMany (⟨k, v⟩ :: l) = (t.insert k v).insertMany l
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.leftAdjointCommShift_commShiftIso : ∀ {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 : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : G.CommShift A] (a : A),
  CategoryTheory.Functor.commShiftIso F a = CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a
-- Std.Async.Basic
/-- Construct an `ETask` that is already resolved with value `x`.
 -/
Std.Async.ETask.pure : {α ε : Type} → α → Std.Async.ETask ε α
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.quotient_eq_of_quotient_addSubgroup_eq' : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : AddSubgroup G} {a b : α},
  Quotient.mk'' a = Quotient.mk'' b → Quotient.mk'' a = Quotient.mk'' b
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- This is often the more useful lemma to rewrite the norm as opposed to `Unitization.norm_def`.  -/
Unitization.norm_eq_sup : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A] (x : Unitization 𝕜 A),
  ‖x‖ = max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (ContinuousLinearMap.mul 𝕜 A) x.toProd.2‖
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.opEquiv.eq_1 : ∀ {M : Type u_2} [inst : MulOneClass M],
  Submonoid.opEquiv =
    { toFun := Submonoid.op, invFun := Submonoid.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Algebra.Group.Fin.Tuple
Fin.insertNth_zero_right : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (j : Fin (n + 1)) → Zero (α j)] (i : Fin (n + 1)) (x : α i),
  i.insertNth x 0 = Pi.single i x
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_id_f_map_mono : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (φ : A ⟶ B) [CategoryTheory.Mono φ]
  (i : ℕ), CategoryTheory.Mono ((groupHomology.chainsMap (MonoidHom.id G) φ).f i)
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.map_retraction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} {f : Y ⟶ X} (se : CategoryTheory.SplitMono f) (F : CategoryTheory.Functor C D),
  (se.map F).retraction = F.map se.retraction
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGTD_eq_getD_getEntryGT? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α} {fallback : (a : α) × β a},
  Std.DTreeMap.Internal.Impl.getEntryGTD k t fallback = (Std.DTreeMap.Internal.Impl.getEntryGT? k t).getD fallback
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.const : ∀ (n : ℕ), Nat.Primrec fun x => n
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.lt_top : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) (K : TopologicalSpace.Compacts G), μ K < ⊤
-- Init.Prelude
Trans.mk : {α : Sort u_1} →
  {β : Sort u_2} →
    {γ : Sort u_3} →
      {r : α → β → Sort u} →
        {s : β → γ → Sort v} →
          {t : outParam (α → γ → Sort w)} → ({a : α} → {b : β} → {c : γ} → r a b → s b c → t a c) → Trans r s t
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.isLeftRegular_iff_isRightRegular : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] {A : Matrix n n R} [IsCancelAdd R],
  IsLeftRegular A ↔ IsRightRegular A
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.get?_eq_get?ₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α),
  Std.DHashMap.Internal.Raw₀.Const.get? m a = Std.DHashMap.Internal.Raw₀.Const.get?ₘ m a
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.multicospanIndex_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.Functor Cᵒᵖ A) (j : E.multicospanShape.R),
  (E.multicospanIndex F).snd j = F.map (E.p₂ j.snd).op