mathlib-initiative/mathlib-types huggingface dataset:
-- Init.MetaTypes
Lean.Meta.Simp.NormCastConfig.toConfig : Lean.Meta.Simp.NormCastConfig → Lean.Meta.Simp.Config
-- Mathlib.Combinatorics.SimpleGraph.Prod
/-- The box product is associative up to isomorphism. `Equiv.prodAssoc` as a graph isomorphism.  -/
SimpleGraph.boxProdAssoc : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → (G : SimpleGraph α) → (H : SimpleGraph β) → (I : SimpleGraph γ) → G □ H □ I ≃g G □ (H □ I)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instMul : {α : Type u_1} → [Mul α] → Mul (Colex α)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_ext_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {f : J → C} {X Y : C}
  {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X ⟶ Y},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) g =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) h) →
    g = h
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_compl_eq_mk_compl_finite : ∀ {α β : Type u} [Finite α] {s : Set α} {t : Set β},
  Cardinal.mk α = Cardinal.mk β → Cardinal.mk ↑s = Cardinal.mk ↑t → Cardinal.mk ↑sᶜ = Cardinal.mk ↑tᶜ
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.instCommShiftDerivedCategoryMapDerivedCategoryInt : {C₁ : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    [inst_1 : CategoryTheory.Abelian C₁] →
      [inst_2 : HasDerivedCategory C₁] →
        {C₂ : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_4 : CategoryTheory.Abelian C₂] →
              [inst_5 : HasDerivedCategory C₂] →
                (F : CategoryTheory.Functor C₁ C₂) →
                  [inst_6 : F.Additive] →
                    [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F] →
                      [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] → F.mapDerivedCategory.CommShift ℤ
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isSyntheticTacticCompletion.isEmptyTacticBlock : Lean.Syntax → Bool
-- Mathlib.Algebra.Lie.Killing
/-- We say a Lie algebra is Killing if its Killing form is non-singular.  -/
LieAlgebra.IsKilling.killingCompl_top_eq_bot : ∀ {R : Type u_1} {L : Type u_3} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  [self : LieAlgebra.IsKilling R L], LieIdeal.killingCompl R L ⊤ = ⊥
-- Mathlib.Order.Interval.Finset.Defs
instLocallyFiniteOrderTopSubtypeLtOfDecidableLTOfLocallyFiniteOrder : {α : Type u_1} →
  [inst : Preorder α] → {y : α} → [DecidableLT α] → [LocallyFiniteOrder α] → LocallyFiniteOrderTop { x // x < y }
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- Over a noetherian ring, if `S` and `T` are disjoint and `T` is CoFG, then `S` is FG.  -/
Submodule.CoFG.fg_of_disjoint : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherianRing R]
  {S T : Submodule R M}, Disjoint S T → T.CoFG → S.FG
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.isLUB_mem : ∀ {α : Type v} {s t : Set α} {x : α} [inst : LinearOrder α], IsClub s → t ⊆ s → t.Nonempty → IsLUB t x → x ∈ s
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.inv_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.GrpObj.inv = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.continuousOn_extend_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H}, ContinuousOn (↑(f.extend I).symm) (f.extend I).target
-- Mathlib.GroupTheory.HNNExtension
/-- To put a word in the HNN Extension into a normal form, we must choose an element of each right
coset of both `A` and `B`, such that the chosen element of the subgroup itself is `1`.  -/
HNNExtension.NormalWord.TransversalPair : (G : Type u_1) → [inst : Group G] → Subgroup G → Subgroup G → Type u_1
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.concat.match_1.splitter : {α : Type u_1} →
  (motive : List α → α → Sort u_2) →
    (x : List α) →
      (x_1 : α) → ((b : α) → motive [] b) → ((a : α) → (as : List α) → (b : α) → motive (a :: as) b) → motive x x_1
-- Std.Internal.Do.PredTrans
/-- Lift a predicate transformer to one with an additional exception layer (high priority).  -/
Std.Internal.Do.instMonadLiftPredTransConsForall : {ε Pred EPred : Type u} →
  MonadLift (Std.Internal.Do.PredTrans Pred EPred) (Std.Internal.Do.PredTrans Pred (EPost.Cons✝ (ε → Pred) EPred))
-- Mathlib.Topology.Sheaves.Presheaf
/-- restriction of a section along an inclusion  -/
AlgebraicGeometry.«term_|_ₕ_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The product topology on the Cartesian product of two semitopological semirings
makes the product into a semitopological semiring.  -/
instIsSemitopologicalSemiringProd : ∀ {R : Type u_1} {S : Type u_2} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace S]
  [inst_2 : NonUnitalNonAssocSemiring R] [inst_3 : NonUnitalNonAssocSemiring S] [IsSemitopologicalSemiring R]
  [IsSemitopologicalSemiring S], IsSemitopologicalSemiring (R × S)
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.trans_isBigO : ∀ {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [inst : Norm E] [inst_1 : Norm G]
  [inst_2 : SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G},
  f =Θ[l] g → g =O[l] k → f =O[l] k
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.IsHomotopyInvariant.map_eq_of_homotopy : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {ι : Type u_2} {c : ComplexShape ι} (HP : TopPair.HomologyPretheory C c) [self : HP.IsHomotopyInvariant]
  {X Y : TopPair} {f g : X ⟶ Y} (F : TopPair.Homotopy f g) (i : ι), (HP.Hₚ i).map f = (HP.Hₚ i).map g
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.match_4.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (k : ℕ),
  x = Lean.Grind.CommRing.Expr.natCast k →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.natCast k => h_2 k
      | Lean.Grind.CommRing.Expr.intCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_2 k
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_prod_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β × γ} {s : Set α} {x : α},
  ContinuousWithinAt f s x ↔ ContinuousWithinAt (Prod.fst ∘ f) s x ∧ ContinuousWithinAt (Prod.snd ∘ f) s x
-- Mathlib.SetTheory.Ordinal.Basic
/-- `ω` is the first infinite ordinal, defined as the order type of `ℕ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `ω` in identifiers is `omega0`. -/
Ordinal.omega0 : Ordinal.{u}
-- Mathlib.Algebra.Group.Equiv.Defs
/-- A multiplicative equivalence of groups preserves division.  -/
MulEquiv.map_div : ∀ {G : Type u_7} {H : Type u_8} [inst : Group G] [inst_1 : DivisionMonoid H] (h : G ≃* H) (x y : G),
  h (x / y) = h x / h y
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableWithinAt.const_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a : E → 𝔸}, DifferentiableWithinAt 𝕜 a s x → ∀ (b : 𝔸), DifferentiableWithinAt 𝕜 (fun y => b * a y) s x
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftCoyonedaEquiv_uliftCoyoneda_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.uliftCoyonedaEquiv (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.map f) = { down := f.unop }
-- Mathlib.Algebra.Homology.Localization
CategoryTheory.Functor.instLiftingHomotopyCategoryHomologicalComplexUpToQuasiIsoQhQuasiIsoCompMapHomotopyCategoryMapHomologicalComplexUpToQuasiIso : {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) →
          {ι : Type u_3} →
            (c : ComplexShape ι) →
              [inst_2 : CategoryTheory.Preadditive C] →
                [inst_3 : CategoryTheory.Preadditive D] →
                  [inst_4 : CategoryTheory.CategoryWithHomology C] →
                    [inst_5 : CategoryTheory.CategoryWithHomology D] →
                      [inst_6 : (HomologicalComplex.quasiIso D c).HasLocalization] →
                        [inst_7 : F.Additive] →
                          [inst_8 : F.PreservesHomology] →
                            [inst_9 : (HomologicalComplex.quasiIso C c).HasLocalization] →
                              [inst_10 : c.QFactorsThroughHomotopy C] →
                                [inst_11 : c.QFactorsThroughHomotopy D] →
                                  [(HomotopyCategory.quotient C c).IsLocalization
                                        (HomologicalComplex.homotopyEquivalences C c)] →
                                    CategoryTheory.Localization.Lifting HomologicalComplexUpToQuasiIso.Qh
                                      (HomotopyCategory.quasiIso C c)
                                      ((F.mapHomotopyCategory c).comp HomologicalComplexUpToQuasiIso.Qh)
                                      (F.mapHomologicalComplexUpToQuasiIso c)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.coversTop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (self : M.QuasicoherentData), J.CoversTop self.X
-- Init.System.FilePath
System.FilePath.mk.injEq : ∀ (toString toString_1 : String), ({ toString := toString } = { toString := toString_1 }) = (toString = toString_1)
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- Two refinement morphisms of `1`-hypercovers are homotopic if there exists a homotopy between
them.
Note: This is not an equivalence relation, it is not even reflexive!
 -/
CategoryTheory.GrothendieckTopology.OneHypercover.homotopicRel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) → (S : C) → HomRel (J.OneHypercover S)
-- Std.Http.Protocol.H1
/-- Appends one event to the machine's event queue for later retrieval by `step`.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.addEvent : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Event dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentable.iff_exists_isRepresentedBy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)},
  F.IsRepresentable ↔ ∃ X x, F.IsRepresentedBy x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpContext.mk.inj : ∀ {triggerKind : Lean.Lsp.SignatureHelpTriggerKind} {triggerCharacter? : Option String} {isRetrigger : Bool}
  {activeSignatureHelp? : Option Lean.Lsp.SignatureHelp} {triggerKind_1 : Lean.Lsp.SignatureHelpTriggerKind}
  {triggerCharacter?_1 : Option String} {isRetrigger_1 : Bool} {activeSignatureHelp?_1 : Option Lean.Lsp.SignatureHelp},
  { triggerKind := triggerKind, triggerCharacter? := triggerCharacter?, isRetrigger := isRetrigger,
        activeSignatureHelp? := activeSignatureHelp? } =
      { triggerKind := triggerKind_1, triggerCharacter? := triggerCharacter?_1, isRetrigger := isRetrigger_1,
        activeSignatureHelp? := activeSignatureHelp?_1 } →
    triggerKind = triggerKind_1 ∧
      triggerCharacter? = triggerCharacter?_1 ∧
        isRetrigger = isRetrigger_1 ∧ activeSignatureHelp? = activeSignatureHelp?_1
-- Mathlib.Analysis.InnerProductSpace.MulOpposite
MulOpposite.instInnerProductSpace : {𝕜 : Type u_1} →
  {H : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup H] → [InnerProductSpace 𝕜 H] → InnerProductSpace 𝕜 Hᵐᵒᵖ
-- Init.Control.Lawful.MonadLift.Lemmas
liftM_pure : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  [LawfulMonadLiftT m n] {α : Type u} (a : α), liftM (pure a) = pure a
-- Mathlib.Topology.Order
DiscreteTopology.of_finite_of_isClosed_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] [Finite α], (∀ (a : α), IsClosed {a}) → DiscreteTopology α
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S), Function.Surjective (WithAbs.toAbs v)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.prod_source : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type w} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {E' : Type v'}
  [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {H' : Type w'} [inst_6 : TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H'), (I.prod I').source = {x | x.1 ∈ I.source ∧ x.2 ∈ I'.source}
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.mk : (carrier : Type u) → [str : Add carrier] → AddMagmaCat
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiable_of_differentiableOn_union_of_isOpen : ∀ {𝕜 : 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] {f : E → F} {s t : Set E},
  DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 f t → s ∪ t = Set.univ → IsOpen s → IsOpen t → Differentiable 𝕜 f
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.exact_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ),
  { X₁ := P.complex.X (n + 2), X₂ := P.complex.X (n + 1), X₃ := P.complex.X n, f := P.complex.d (n + 2) (n + 1),
      g := P.complex.d (n + 1) n, zero := ⋯ }.Exact
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.IsSFiniteKernel.restrict : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β}
  (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (hs : MeasurableSet s),
  ProbabilityTheory.IsSFiniteKernel (κ.restrict hs)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.ιMapObjOrZero_mapMap : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (p : I → J) [inst_1 : X.HasMap p] [inst_2 : Y.HasMap p]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : DecidableEq J] (i : I) (j : J),
  CategoryTheory.CategoryStruct.comp (X.ιMapObjOrZero p i j) (CategoryTheory.GradedObject.mapMap φ p j) =
    CategoryTheory.CategoryStruct.comp (φ i) (Y.ιMapObjOrZero p i j)
-- Mathlib.Order.Partition.Finpartition
Finpartition.extendOfLE.eq_1 : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableEq α] {a b : α} (P : Finpartition a)
  (hab : a ≤ b), P.extendOfLE hab = if hr : b \ a = ⊥ then ⋯ ▸ P else P.extend hr ⋯ ⋯
-- Init.Prelude
/-- Is this syntax a null `node`?  -/
Lean.Syntax.matchesNull : Lean.Syntax → ℕ → Bool
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
/-- Shows that `IntFractPair.stream` has the sequence property, that is once we return `none` at
position `n`, we also return `none` at `n + 1`.
 -/
GenContFract.IntFractPair.stream_isSeq : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K),
  (GenContFract.IntFractPair.stream v).IsSeq
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.ordFrac_le_smul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsNoetherianRing R] [inst_3 : Ring.KrullDimLE 1 R]
  {K : Type u_2} [inst_4 : Field K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K] {S : Type u_3}
  [inst_7 : CommRing S] [inst_8 : Algebra S R] [inst_9 : Algebra S K] [IsScalarTower S R K] (a : S),
  (algebraMap S R) a ≠ 0 → ∀ (f : K), (Ring.ordFrac R) f ≤ (Ring.ordFrac R) (a • f)
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanAuxM.go.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (a : β) (a_1 : List β),
  List.scanAuxM.go✝ f [] a a_1 = pure (a :: a_1)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTransposeLinearEquiv_symm : ∀ (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : AddCommMonoid α] [inst_3 : StarAddMonoid α] [inst_4 : Module R α] [inst_5 : StarModule R α],
  (Matrix.conjTransposeLinearEquiv m n R α).symm = Matrix.conjTransposeLinearEquiv n m R α
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ D` creates finite coproducts, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates finite
products.  -/
CategoryTheory.Limits.createsFiniteProductsOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.CreatesFiniteCoproducts F] → CategoryTheory.Limits.CreatesFiniteProducts F.op
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxKeyD.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) (fallback : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      (fallback : α) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback) =
    h_1 fallback
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
/-- The members of `l.ranges` have no duplicates  -/
List.ranges_nodup : ∀ {l s : List ℕ}, s ∈ l.ranges → s.Nodup
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_sub_of_nonempty : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [IsTopologicalAddGroup E] {s t : Set E},
  s.Nonempty →
    t.Nonempty → (Bornology.IsVonNBounded 𝕜 (s - t) ↔ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientMapₐ.congr_simp : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Ring B] [inst_4 : Algebra R₁ B] {I : Ideal A} (J : Ideal B) [inst_5 : I.IsTwoSided] [inst_6 : J.IsTwoSided]
  (f f_1 : A →ₐ[R₁] B) (e_f : f = f_1) (hIJ : I ≤ Ideal.comap f J),
  Ideal.quotientMapₐ J f hIJ = Ideal.quotientMapₐ J f_1 ⋯
-- Lean.Meta.Tactic.Simp.Rewrite
/-- Discharge procedure for the ground/symbolic evaluator.
 -/
Lean.Meta.Simp.dischargeGround : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)
-- Mathlib.RingTheory.Lasker
/-- **Alias** of `Submodule.IsLasker.exists_isMinimalPrimaryDecomposition`. -/
Ideal.IsLasker.minimal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsLasker R M → ∀ (N : Submodule R M), ∃ t, N.IsMinimalPrimaryDecomposition t
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The edist to a set is bounded above by the edist to any of its points  -/
Metric.infEDist_le_edist_of_mem : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {s : Set α}, y ∈ s → Metric.infEDist x s ≤ edist x y
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_add_def : ∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R),
  x + y = Tropical.trop (min (Tropical.untrop x) (Tropical.untrop y))
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
/-- Any intersection of translates of two sets `s` and `t` can be covered by a single translate of
`(-s + s) ∩ (-t + t)`.

This is useful to show that the intersection of approximate subgroups is an approximate subgroup.
 -/
Set.exists_vadd_inter_vadd_subset_vadd_neg_add_inter_neg_add : ∀ {α : Type u_2} [inst : AddGroup α] (s t : Set α) (a b : α), ∃ z, (a +ᵥ s) ∩ (b +ᵥ t) ⊆ z +ᵥ (-s + s) ∩ (-t + t)
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.Locally.left : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : LinearOrder ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p q : (ι → Ω → E) → Prop}
  [inst_1 : OrderBot ι] [inst_2 : TopologicalSpace ι] [inst_3 : OrderTopology ι] [inst_4 : Zero E],
  ProbabilityTheory.Locally (fun Y => p Y ∧ q Y) 𝓕 X P → ProbabilityTheory.Locally p 𝓕 X P
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] {P : Ideal R} [inst_5 : P.IsPrime] [inst_6 : FaithfulSMul R S]
  [Algebra.IsSeparable (FractionRing R) (FractionRing S)],
  Algebra.IsSeparable (FractionRing (Localization.AtPrime P))
    (FractionRing (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)))