mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- If `{Uᵢ}` covers `Y`, this is the `0`-hypercover of `X ×[Z] Y` given by `{X ×[Z] Uᵢ}`.  -/
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      [J.IsStableUnderBaseChange] →
        {Y : C} →
          (E : J.ZeroHypercover Y) →
            {X Z : C} →
              (f : X ⟶ Z) →
                (g : Y ⟶ Z) →
                  [inst_2 : CategoryTheory.Limits.HasPullback f g] →
                    [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.snd f g)] →
                      J.ZeroHypercover (CategoryTheory.Limits.pullback f g)
-- Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderComonoid.comul_mem : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  (P : CategoryTheory.MorphismProperty C) {c : C} {inst_2 : CategoryTheory.ComonObj c}
  [self : P.IsStableUnderComonoid c], P CategoryTheory.ComonObj.comul
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.mulAction_faithful : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α],
  1 ≤ n → ↑n < ENat.card α → ∀ {g : G}, MulAction.toPerm g = 1 ↔ MulAction.toPerm g = 1
-- Mathlib.Algebra.Prime.Lemmas
Prime.left_dvd_or_dvd_right_of_dvd_mul : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p : M},
  Prime p → ∀ {a b : M}, a ∣ p * b → p ∣ a ∨ a ∣ b
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.instIsAddModHomComp : ∀ {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.MonoidalLeftAction C D]
  (A : C) [inst_4 : CategoryTheory.AddMonObj A] {M N O : D} [inst_5 : CategoryTheory.AddModObj A M]
  [inst_6 : CategoryTheory.AddModObj A N] [inst_7 : CategoryTheory.AddModObj A O] (f : M ⟶ N) (g : N ⟶ O)
  [CategoryTheory.IsAddModHom A f] [CategoryTheory.IsAddModHom A g],
  CategoryTheory.IsAddModHom A (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Order.ConditionallyCompleteLattice.Group
ciSup_mul_le : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : Group α] [MulRightMono α]
  {a : α} {g : ι → α} {h : α}, (∀ (i : ι), g i * h ≤ a) → iSup g * h ≤ a
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin'_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  (k : ℕ), Matrix.toLin' (M ^ k) = Matrix.toLin' M ^ k
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousWithinAt_neg_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β],
  LowerSemicontinuousWithinAt (-f) s a ↔ UpperSemicontinuousWithinAt f s a
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Expr.denoteN.match_1.eq_3 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (k : ℤ) (a : Lean.Grind.Linarith.Expr)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a)),
  (match Lean.Grind.Linarith.Expr.intMul k a with
    | a.sub b => h_1 a b
    | a.neg => h_2 a
    | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
    | Lean.Grind.Linarith.Expr.zero => h_4 ()
    | Lean.Grind.Linarith.Expr.var v => h_5 v
    | a.add b => h_6 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) =
    h_3 k a
-- Init.Data.Int.Gcd
Int.coe_lcm_dvd : ∀ {a b c : ℤ}, a ∣ c → b ∣ c → ↑(a.lcm b) ∣ c
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard.eq_1 : ∀ {α : Type u_1} (n : ℕ) (s : Finset α),
  Finset.powersetCard n s = { val := Multiset.pmap Finset.mk (Multiset.powersetCard n s.val) ⋯, nodup := ⋯ }
-- Lean.ToLevel
/-- `ToLevel` for `max u v`. This is not an instance since it causes divergence.  -/
Lean.ToLevel.max : [Lean.ToLevel] → [Lean.ToLevel] → Lean.ToLevel
-- Mathlib.Analysis.Calculus.DSlope
differentiableOn_dslope_of_notMem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} {s : Set 𝕜},
  a ∉ s → (DifferentiableOn 𝕜 (dslope f a) s ↔ DifferentiableOn 𝕜 f s)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.allM_mapM : ∀ {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : MonadLiftT m n] [inst_3 : Monad m] [LawfulMonad m] [inst_5 : Monad n]
  [inst_6 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] {it : Std.IterM m β}
  {f : β → n β'} {p : β' → n (ULift.{w, 0} Bool)},
  Std.IterM.allM p (Std.IterM.mapM f it) =
    Std.IterM.allM
      (fun x => do
        let __do_lift ← f x
        p __do_lift)
      (Std.IterM.mapM pure it)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows.obj_idx : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S}
  {Y : C} {g : Y ⟶ S} (hf : CategoryTheory.Presieve.ofArrows X f g), X hf.idx = Y
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.power_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type t)
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] (i : α → U.I), (U.power α).obj i = ∏ᶜ U.obj ∘ i
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf.eq_1 : ∀ (u : ℕ → ENNReal), ExpGrowth.expGrowthInf u = Filter.liminf (fun n => (u n).log / ↑n) Filter.atTop
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.linearIndepOn_coroot_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic] [P.IsRootSystem] [NeZero 2] {s : Set ι}, LinearIndepOn R (⇑P.coroot) s ↔ LinearIndepOn R (⇑P.root) s
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.exists_pos_of_mem : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) {x : M}, x ∈ s → ∃ i, 0 < (f i) x
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.LocalizerMorphism.equiv_smallHomMap : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁} {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₂ : CategoryTheory.MorphismProperty C₂} {D₁ : Type u₃}
  [inst_2 : CategoryTheory.Category.{v₃, u₃} D₁] {D₂ : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} D₂]
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁]
  (L₂ : CategoryTheory.Functor C₂ D₂) [inst_5 : L₂.IsLocalization W₂] {X Y : C₁}
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)]
  (G : CategoryTheory.Functor D₁ D₂) (e : Φ.functor.comp L₂ ≅ L₁.comp G)
  (f : CategoryTheory.Localization.SmallHom W₁ X Y),
  (CategoryTheory.Localization.SmallHom.equiv W₂ L₂) (Φ.smallHomMap f) =
    CategoryTheory.CategoryStruct.comp (e.hom.app X)
      (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Localization.SmallHom.equiv W₁ L₁) f)) (e.inv.app Y))
-- Batteries.Control.OptionT
OptionT.run_mapConst : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] (x : OptionT m α) (y : β),
  (Functor.mapConst y x).run = Option.map (Function.const α y) <$> x.run
-- Mathlib.Logic.Equiv.Option
Equiv.coe_optionSubtype_apply_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β) (e : { e // e none = x }) (a : α),
  ↑(((Equiv.optionSubtype x) e) a) = ↑e (some a)
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_apply_univ : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsMarkovKernel κ],
  (μ.compProd κ) Set.univ = μ Set.univ
-- Mathlib.ModelTheory.Encoding
/-- Encodes a bounded formula as a list of symbols.  -/
FirstOrder.Language.BoundedFormula.listEncode : {L : FirstOrder.Language} →
  {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.union_isExtendible : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] (c : Set (IntermediateField.Lifts F E K))
  (hc : IsChain (fun x1 x2 => x1 ≤ x2) c) [alg : Algebra.IsAlgebraic F E] [Nonempty ↑c],
  (∀ σ ∈ c, σ.IsExtendible) → (IntermediateField.Lifts.union c hc).IsExtendible
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.instIsDenseSubsiteEtaleTopologySmallEtaleTopologySpec : ∀ {S : AlgebraicGeometry.Scheme},
  CategoryTheory.Functor.IsDenseSubsite (AlgebraicGeometry.Scheme.AffineEtale.topology S) S.smallEtaleTopology
    (AlgebraicGeometry.Scheme.AffineEtale.Spec S)
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Presieve.factorsThruAlong_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} (S T : CategoryTheory.Presieve X),
  S.FactorsThruAlong T (CategoryTheory.CategoryStruct.id X) ↔ S.FactorsThru T
-- Mathlib.NumberTheory.ModularForms.Identities
SlashInvariantForm.slash_S_apply : ∀ (f : UpperHalfPlane → ℂ) (k : ℤ) (z : UpperHalfPlane),
  SlashAction.map k ModularGroup.S f z = f { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * ↑z ^ (-k)
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Lattice α] [inst_1 : Lattice β]
  [inst_2 : Lattice γ] [inst_3 : Lattice δ] [inst_4 : BoundedOrder α] [inst_5 : BoundedOrder β]
  [inst_6 : BoundedOrder γ] [inst_7 : BoundedOrder δ] (f : BoundedLatticeHom γ δ) (g : BoundedLatticeHom β γ)
  (h : BoundedLatticeHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Analysis.Complex.Circle
instTopologicalSpaceCircle : TopologicalSpace Circle
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- Note: this assumes `[IsLeftUniformAddGroup β] [IsRightUniformAddGroup β]`
instead of the more typical (and equivalent) `[IsUniformAddGroup β]` because this is used
in the proof of said equivalence.  -/
Filter.Tendsto.addConj_nhds_zero : ∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : AddGroup β] [IsLeftUniformAddGroup β] [IsRightUniformAddGroup β]
  {ι : Type u_3} {l : Filter ι} {x : ι → β},
  Filter.Tendsto x l (nhds 0) → ∀ (g : ι → β), Filter.Tendsto (g + x + -g) l (nhds 0)
-- Mathlib.Algebra.Order.Antidiag.Finsupp
Finset.finsuppAntidiag_empty_zero : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ], ∅.finsuppAntidiag 0 = {0}
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.range_toLin_eq_top : ∀ {n : Type u_1} [inst : Fintype n] {R : Type u_2} {M : Type u_3} [inst_1 : CommRing R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (b : Module.Basis n R M) [inst_4 : DecidableEq n] (A : Matrix n n R),
  IsUnit A.det → ((Matrix.toLin b b) A).range = ⊤
-- Init.Data.BitVec.Lemmas
BitVec.ofInt_natCast : ∀ (w n : ℕ), BitVec.ofInt w ↑n = BitVec.ofNat w n
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.toFreeGroup_symm_apply : ∀ (G : Type u_1) [inst : Group G] [inst_1 : IsFreeGroup G] (a : FreeGroup (IsFreeGroup.Generators G)),
  (IsFreeGroup.toFreeGroup G).symm a = (IsFreeGroup.mulEquiv G) a
-- Lean.Data.JsonRpc
/-- The server detected that the content of a document got
modified outside normal conditions. A server should
NOT send this error code if it detects a content change
in it unprocessed messages. The result even computed
on an older state might still be useful for the client.

If a client decides that a result is not of any use anymore
the client should cancel the request.  -/
Lean.JsonRpc.ErrorCode.contentModified : Lean.JsonRpc.ErrorCode
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_sdiff : ∀ {α : Type u_1} {s t u : Set α}, (s \ t) \ u = s \ (t ∪ u)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.forget.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMon.forget C = { obj := fun A => A.X, map := fun {X Y} f => f.hom, map_id := ⋯, map_comp := ⋯ }
-- Init.Data.Int.DivMod.Lemmas
Int.zero_fdiv : ∀ (b : ℤ), Int.fdiv 0 b = 0
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofBool.injEq : ∀ (b b_1 : Bool), (Lean.LeanOptionValue.ofBool b = Lean.LeanOptionValue.ofBool b_1) = (b = b_1)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.one_mem_one : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  1 ∈ 1
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Real.Gamma_nat_eq_factorial : ∀ (n : ℕ), Real.Gamma (↑n + 1) = ↑n.factorial
-- Mathlib.Data.Vector.Basic
List.Vector.length_val : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n), (↑v).length = n
-- Mathlib.Analysis.Normed.Module.Bases
GeneralSchauderBasis.ext : ∀ {β : Type u_3} {𝕜 : Type u_4} {X : Type u_5} {inst : NontriviallyNormedField 𝕜} {inst_1 : NormedAddCommGroup X}
  {inst_2 : NormedSpace 𝕜 X} {L : SummationFilter β} {x y : GeneralSchauderBasis β 𝕜 X L},
  ↑x = ↑y → x.coord = y.coord → x = y
-- Mathlib.Order.SuccPred.CompleteLinearOrder
/-- **Alias** of `exists_eq_ciSup_of_not_isSuccPrelimit`.

---

See `exists_eq_ciSup_of_not_isSuccLimit` for the `ConditionallyCompleteLinearOrder` version.  -/
exists_eq_ciSup_of_not_isSuccPrelimit' : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α},
  ¬Order.IsSuccPrelimit (⨆ i, f i) → ∃ i, f i = ⨆ i, f i
-- Mathlib.RingTheory.Spectrum.Prime.Jacobson
/-- If `R` is both Noetherian and Jacobson, then the following are equivalent for `x : Spec R`:
1. `{x}` is open (i.e. `x` is an isolated point)
2. `{x}` is clopen
3. `{x}` is both closed and stable under generalization
  (i.e. `x` is both a minimal prime and a maximal ideal)
 -/
PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [IsJacobsonRing R] (x : PrimeSpectrum R),
  [IsOpen {x}, IsClopen {x}, IsClosed {x} ∧ StableUnderGeneralization {x}].TFAE
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.StrictMono.factorPow_comp_extend : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {a : ℕ → ℕ} (ha : StrictMono a)
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤),
  (∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) →
    ∀ {m n : ℕ} (hle : m ≤ n),
      Submodule.factorPow I N hle ∘ₗ IsAdicComplete.StrictMono.extend ha f n = IsAdicComplete.StrictMono.extend ha f m
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- Two multivariate formal power series are equal if all their coefficients are equal.  -/
MvPowerSeries.ext : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {φ ψ : MvPowerSeries σ R},
  (∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff n) φ = (MvPowerSeries.coeff n) ψ) → φ = ψ
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.append_const_right : ∀ {w1 w2 b w3 c : ℕ} {a : BitVec w1},
  a ++ BitVec.ofNat w2 b ++ BitVec.ofNat w3 c = BitVec.cast ⋯ (a ++ (BitVec.ofNat w2 b ++ BitVec.ofNat w3 c))
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- A sheaf `M` of `R-modules` is localizing if for all `f` in `R`, the restriction map
from `M(⊤)` to `M(D(f))` is localization with respect to `f`.  -/
AlgebraicGeometry.IsLocalizing : {R : CommRingCat} → TopCat.Sheaf (ModuleCat ↑R) ↑(AlgebraicGeometry.Spec R).toPresheafedSpace → Prop
-- Mathlib.Data.Nat.Pairing
Nat.unpair.eq_1 : ∀ (n : ℕ),
  Nat.unpair n =
    if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)
-- Init.Data.Nat.Lemmas
/-- Dependent variant of `exists_lt_succ_right`.  -/
Nat.exists_lt_succ_right' : ∀ {n : ℕ} {p : (m : ℕ) → m < n + 1 → Prop}, (∃ m, ∃ (h : m < n + 1), p m h) ↔ (∃ m, ∃ (h : m < n), p m ⋯) ∨ p n ⋯
-- Mathlib.Order.Birkhoff
/-- The **Birkhoff Embedding** of a finite partial order as sup-irreducible elements in its
lattice of lower sets.  -/
OrderEmbedding.supIrredLowerSet : {α : Type u_1} → [inst : PartialOrder α] → α ↪o { s // SupIrred s }
-- Mathlib.Analysis.ODE.PicardLindelof
/-- Given `IsPicardLindelof` on a symmetric interval `[t₀ - ε, t₀ + ε]`, if we shrink the radius
from `a` to `a'` with `a' ≤ a`, and choose any `r' < a'`, then there exists `ε' > 0` such that
`IsPicardLindelof` holds on `[t₀ - ε', t₀ + ε']` with the new parameters.  -/
IsPicardLindelof.exists_shrink_radius : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E → E} {t₀ ε : ℝ} (hε : 0 < ε) {x₀ : E} {a r L K : NNReal},
  IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a r L K →
    ∀ {a' r' : NNReal}, a' ≤ a → r' < a' → ∃ ε', ∃ (hε' : 0 < ε'), IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a' r' L K
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- `abv` as a `MonoidWithZeroHom`.  -/
IsAbsoluteValue.abvHom : {S : Type u_5} →
  [inst : Ring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_6} →
        [inst_2 : Semiring R] → (abv : R → S) → [IsAbsoluteValue abv] → [IsDomain S] → [Nontrivial R] → R →*₀ S
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : o → Matrix m n α),
  Matrix.blockDiagonal M =
    Matrix.of fun x x_1 =>
      match x with
      | (i, k) =>
        match x_1 with
        | (j, k') => if k = k' then M k i j else 0
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiffTag.delete.sizeOf_spec : sizeOf Lean.Widget.ExprDiffTag.delete✝ = 1
-- Mathlib.Order.Hom.Bounded
TopHom.instMax.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : SemilatticeSup β] [inst_2 : OrderTop β],
  TopHom.instMax = { max := fun f g => { toFun := ⇑f ⊔ ⇑g, map_top' := ⋯ } }
-- Init.Data.List.BasicAux
_private.Init.Data.List.BasicAux.0.List.get.match_1.splitter : {α : Type u_1} →
  (motive : (x : List α) → Fin x.length → Sort u_2) →
    (x : List α) →
      (x_1 : Fin x.length) →
        ((a : α) → (tail : List α) → (isLt : 0 < (a :: tail).length) → motive (a :: tail) ⟨0, isLt⟩) →
          ((head : α) →
              (as : List α) → (i : ℕ) → (h : i.succ < (head :: as).length) → motive (head :: as) ⟨i.succ, h⟩) →
            motive x x_1
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Stream.foldr.match_1.eq_1 : ∀ {α : Type u_1} {σ : Sort u_3} (motive : RBTree.RBNode.Stream α → σ → Sort u_2) (b : σ)
  (h_1 : (b : σ) → motive RBTree.RBNode.Stream.nil b)
  (h_2 :
    (v : α) →
      (r : RBTree.RBNode α) →
        (tail : RBTree.RBNode.Stream α) → (b : σ) → motive (RBTree.RBNode.Stream.cons v r tail) b),
  (match RBTree.RBNode.Stream.nil, b with
    | RBTree.RBNode.Stream.nil, b => h_1 b
    | RBTree.RBNode.Stream.cons v r tail, b => h_2 v r tail b) =
    h_1 b
-- Mathlib.Data.NNReal.Defs
NNReal.coe_le_coe : ∀ {r₁ r₂ : NNReal}, ↑r₁ ≤ ↑r₂ ↔ r₁ ≤ r₂
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toAlgEquiv_trans : ∀ {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Star A] [inst_6 : Star B] {C : Type u_9} [inst_7 : Semiring C]
  [inst_8 : Algebra R C] [inst_9 : Star C] (f : A ≃⋆ₐ[R] B) (g : B ≃⋆ₐ[R] C),
  (f.trans g).toAlgEquiv = f.toAlgEquiv.trans g.toAlgEquiv
-- Mathlib.CategoryTheory.Opposites
/-- Another variant of the opposite of functor, turning a functor `C ⥤ Dᵒᵖ` into a functor `Cᵒᵖ ⥤ D`.
In informal mathematics no distinction is made.
 -/
CategoryTheory.Functor.leftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C Dᵒᵖ → CategoryTheory.Functor Cᵒᵖ D
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.ofSubsingletonₗᵢ_symm_apply : ∀ (𝕜 : Type u) {ι : Type v} (G : Type wG) {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] [inst_3 : SeminormedAddCommGroup G']
  [inst_4 : NormedSpace 𝕜 G'] [inst_5 : Fintype ι] [inst_6 : Subsingleton ι] (i : ι)
  (a : ContinuousMultilinearMap 𝕜 (fun x => G) G'),
  (ContinuousMultilinearMap.ofSubsingletonₗᵢ 𝕜 G i).symm a = (ContinuousMultilinearMap.ofSubsingleton 𝕜 G G' i).invFun a
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
opposite side.  -/
EuclideanGeometry.sin_angle_mul_dist_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 → Real.sin (EuclideanGeometry.angle p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
-- Mathlib.Order.ScottContinuity
ScottContinuousOn.image_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {D : Set (Set α)} {f : α → β} {g : β → γ},
  (∀ (a b : α), a ≤ b → {a, b} ∈ D) →
    ScottContinuousOn ((fun x => f '' x) '' D) g → ScottContinuousOn D f → ScottContinuousOn D (g ∘ f)
-- Init.Data.List.Basic
/-- Counts the number of elements in the list `l` that satisfy the Boolean predicate `p`.

Examples:
* `[1, 2, 3, 4, 5].countP (· % 2 == 0) = 2`
* `[1, 2, 3, 4, 5].countP (· < 5) = 4`
* `[1, 2, 3, 4, 5].countP (· > 5) = 0`
 -/
List.countP : {α : Type u} → (α → Bool) → List α → ℕ
-- Mathlib.Order.Interval.Set.OrderEmbedding
OrderEmbedding.preimage_Ico : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) (x y : α),
  ⇑e ⁻¹' Set.Ico (e x) (e y) = Set.Ico x y
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k k' fallback : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) l →
          k ∈ List.map Prod.fst l → (Std.DHashMap.Raw.Const.insertMany m l).getKeyD k' fallback = k
-- Init.Data.SInt.Lemmas
Int32.neg_zero : -0 = 0
-- Mathlib.Algebra.Category.ModuleCat.Basic
_private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.mk.inj : ∀ {R : Type u} {inst : Ring R} {carrier : Type v} {isAddCommGroup : AddCommGroup carrier} {isModule : Module R carrier}
  {carrier_1 : Type v} {isAddCommGroup_1 : AddCommGroup carrier_1} {isModule_1 : Module R carrier_1},
  { carrier := carrier, isAddCommGroup := isAddCommGroup, isModule := isModule } =
      { carrier := carrier_1, isAddCommGroup := isAddCommGroup_1, isModule := isModule_1 } →
    carrier = carrier_1 ∧ isAddCommGroup ≍ isAddCommGroup_1 ∧ isModule ≍ isModule_1