mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.extensionEmbedding_coe : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x : WithAbs ↑v),
  (NumberField.InfinitePlace.Completion.extensionEmbedding v) { toCompletion := ↑x } =
    v.embedding ((WithAbs.equiv ↑v) x)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LevelMVarErrorInfo.ref : Lean.Elab.Term.LevelMVarErrorInfo → Lean.Syntax
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- In a normed space, the von Neumann bornology (`Bornology.vonNBornology`) is equal to the
metric bornology.  -/
NormedSpace.vonNBornology_eq : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E], Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_mkSlice_roo : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...hi) = List.drop (lo + 1) (List.take hi (Std.Slice.toList xs))
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
/-- The jump of `variationOnFromTo` on the left of a point is given by the distance between the
left limit and the value of the function.  -/
variationOnFromTo.tendsto_left : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {E : Type u_3} [inst_1 : PseudoMetricSpace E]
  [inst_2 : TopologicalSpace α] [OrderTopology α] {f : α → E} {l : E} {a b : α},
  a ∈ s →
    b ∈ s →
      LocallyBoundedVariationOn f s →
        Filter.Tendsto f (nhdsWithin b (s ∩ Set.Iio b)) (nhds l) →
          Filter.Tendsto (variationOnFromTo f s a) (nhdsWithin b (s ∩ Set.Iio b))
            (nhds (variationOnFromTo f s a b - dist (f b) l))
-- Mathlib.Topology.Metrizable.Uniformity
/-- The maximal pseudometric space structure on `X` such that `dist x y ≤ d x y` for all `x y`,
where `d : X → X → ℝ≥0` is a function such that `d x x = 0` and `d x y = d y x` for all `x`, `y`.  -/
PseudoMetricSpace.ofPreNNDist : {X : Type u_1} → (d : X → X → NNReal) → (∀ (x : X), d x x = 0) → (∀ (x y : X), d x y = d y x) → PseudoMetricSpace X
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.codisjoint_coe : ∀ {α : Type u_1} [inst : LE α] {s t : UpperSet α}, Codisjoint ↑s ↑t ↔ Disjoint s t
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioc_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Ioc a b)), Subtype.val '' Set.Ici c = Set.Icc (↑c) b
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.le_iff_of_unique : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : LinearOrder α] [inst_2 : Unique α] [inst_3 : PartialOrder N]
  {x y : Colex (α →₀ N)}, x ≤ y ↔ (ofColex x) default ≤ (ofColex y) default
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsId'App_inv_apply : ∀ {R : Type u₁} [inst : Ring R] (f : R →+* R) (hf : f = RingHom.id R) (M : ModuleCat R) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.restrictScalarsId'App f hf M).inv) x = x
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.rightInvOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  Set.RightInvOn (↑I.symm) (↑I) (Set.range ↑I)
-- Mathlib.Data.Set.Semiring
instInhabitedSetSemiring : (α : Type u_1) → Inhabited (SetSemiring α)
-- Mathlib.CategoryTheory.Sums.Basic
/-- The double swap on `C ⊕ D` is naturally isomorphic to the identity functor.  -/
CategoryTheory.Sum.Swap.symmetry : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (CategoryTheory.Sum.swap C D).comp (CategoryTheory.Sum.swap D C) ≅ CategoryTheory.Functor.id (C ⊕ D)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : C} (h : CategoryTheory.Limits.pushout f g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutSymmetry f g).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) h
-- Mathlib.Data.Real.Basic
Real.cauchy_sub : ∀ (a b : ℝ), (a - b).cauchy = a.cauchy - b.cauchy
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.ShiftMkCore.mk : {C : Type u} →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        (F : A → CategoryTheory.Functor C C) →
          (zero : F 0 ≅ CategoryTheory.Functor.id C) →
            (add : (n m : A) → F (n + m) ≅ (F n).comp (F m)) →
              autoParam
                  (∀ (m₁ m₂ m₃ : A) (X : C),
                    CategoryTheory.CategoryStruct.comp ((add (m₁ + m₂) m₃).hom.app X)
                        ((F m₃).map ((add m₁ m₂).hom.app X)) =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
                        (CategoryTheory.CategoryStruct.comp ((add m₁ (m₂ + m₃)).hom.app X)
                          ((add m₂ m₃).hom.app ((F m₁).obj X))))
                  CategoryTheory.ShiftMkCore.assoc_hom_app._autoParam →
                autoParam
                    (∀ (n : A) (X : C),
                      (add 0 n).hom.app X =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((F n).map (zero.inv.app X)))
                    CategoryTheory.ShiftMkCore.zero_add_hom_app._autoParam →
                  autoParam
                      (∀ (n : A) (X : C),
                        (add n 0).hom.app X =
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (zero.inv.app ((F n).obj X)))
                      CategoryTheory.ShiftMkCore.add_zero_hom_app._autoParam →
                    CategoryTheory.ShiftMkCore C A
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.biprodIsoProd_inv_comp_fst_apply : ∀ {R : Type u} [inst : Ring R] (M N : ModuleCat R) (x : ↑M × ↑N),
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.biprod.fst)
      ((CategoryTheory.ConcreteCategory.hom (M.biprodIsoProd N).inv) x) =
    x.1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- `Cofork.ofπ f pullback.condition` is a colimit cocone if and only if
`Fork.ofι f.op pushout.condition` in the opposite category is a limit cone.  -/
CategoryTheory.Limits.Cofork.isColimitCoforkPushoutEquivIsColimitForkOpPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasPullback f f] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯) ≃
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f.op ⋯)
-- Std.Time.Notation
/-- Defines a syntax for zoned datetime values. It expects a string representing a datetime with
timezone information.

Example:
`zoned("2024-10-13T15:00:00-03:00")`
 -/
Std.Time.«termZoned(_)» : Lean.ParserDescr
-- Mathlib.Data.PEquiv
PEquiv.ofSet_eq_some_self_iff : ∀ {α : Type u} {s : Set α} {x : DecidablePred fun x => x ∈ s} {a : α}, (PEquiv.ofSet s) a = some a ↔ a ∈ s
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] (b : J.R),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (J.fst b)) (I.fst b) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (J.snd b)) (I.snd b)
-- Mathlib.Order.Filter.EventuallyConst
Filter.eventuallyConst_iff_tendsto : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Nonempty β],
  Filter.EventuallyConst f l ↔ ∃ x, Filter.Tendsto f l (pure x)
-- Lean.Meta.Match.CaseValues
Lean.Meta.CaseValuesSubgoal.mk : Lean.MVarId → Array Lean.FVarId → Lean.Meta.FVarSubst → Lean.Meta.CaseValuesSubgoal
-- Init.Data.Bool
Bool.false_bne : ∀ (b : Bool), (false != b) = b
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.isClosedImmersion_of_comp_eq_id : ∀ {X Y : AlgebraicGeometry.Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id Y → AlgebraicGeometry.IsClosedImmersion g
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- The First Derivative test with a hypothesis on the sign of the derivative, minimum version.  -/
isLocalMin_of_sign_deriv : ∀ {f : ℝ → ℝ} {x₀ : ℝ},
  ContinuousAt f x₀ →
    (∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x - x₀)) → IsLocalMin f x₀
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
CategoryTheory.Presieve.isSheaf_of_nat_equiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P₁ : CategoryTheory.Functor Cᵒᵖ (Type w)} {P₂ : CategoryTheory.Functor Cᵒᵖ (Type w')}
  (e : ⦃X : C⦄ → P₁.obj (Opposite.op X) ≃ P₂.obj (Opposite.op X)),
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (Opposite.op Y)),
      e ((CategoryTheory.ConcreteCategory.hom (P₁.map f.op)) x) =
        (CategoryTheory.ConcreteCategory.hom (P₂.map f.op)) (e x)) →
    CategoryTheory.Presieve.IsSheaf J P₁ → CategoryTheory.Presieve.IsSheaf J P₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} [inst_1 : Inhabited (β k)],
  Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.union m₂ ⋯ ⋯).get! k = m₂.get! k
-- Mathlib.Data.Finset.Union
/-- Rewrite a `biUnion` over `s.attach` as a `biUnion` over `s`, in the case where the indexing
function on `s.attach` happens to factor through `α`. See `Finset.attach_biUnion'` for the version
without that hypothesis.  -/
Finset.attach_biUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} [inst : DecidableEq β] {f : α → Finset β},
  (s.attach.biUnion fun x => f ↑x) = s.biUnion f
-- Init.Data.Int.Order
Int.mul_nonpos_of_nonpos_of_nonneg : ∀ {a b : ℤ}, a ≤ 0 → 0 ≤ b → a * b ≤ 0
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- One can replace `f` in `Approximates` with the function that eventually equals `f`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.replaceFun : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)} {f : ℝ → ℝ},
  ms.toFun =ᶠ[Filter.atTop] f → ms.Approximates → (ms.replaceFun f).Approximates
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A/R` is integral, such that `A'` and `B` are linearly disjoint for all subalgebras `A'`
of `A` which are finitely generated `R`-modules, then `A` and `B` are linearly disjoint.  -/
Subalgebra.LinearDisjoint.of_linearDisjoint_finite_left : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  [Algebra.IsIntegral R ↥A], (∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B) → A.LinearDisjoint B
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.isClosed_iff_zeroLocus : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (Z : Set (ProjectiveSpectrum 𝒜)), IsClosed Z ↔ ∃ s, Z = ProjectiveSpectrum.zeroLocus 𝒜 s
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.tr.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ)
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) (l : Λ),
  Turing.TM1to1.tr enc dec M (Turing.TM1to1.Λ'.normal l) = Turing.TM1to1.trNormal dec (M l)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddCommGroup : {G : Type u_1} →
  [inst : TopologicalSpace G] →
    [inst_1 : AddCommGroup G] → [IsTopologicalAddGroup G] → AddCommGroup (SeparationQuotient G)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opId_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ),
  (CategoryTheory.Functor.opId C).inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- A singleton is a measurable set.  -/
MeasurableSingletonClass.measurableSet_singleton : ∀ {α : Type u_7} {inst : MeasurableSpace α} [self : MeasurableSingletonClass α] (x : α), MeasurableSet {x}
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.forM_eq_forM : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m']
  {f : α → β → m' PUnit.{w + 1}}, Std.HashMap.Raw.forM f m = forM m fun a => f a.1 a.2
-- Init.Data.Int.DivMod.Lemmas
Int.eq_mul_of_ediv_eq_left : ∀ {a b c : ℤ}, b ∣ a → a / b = c → a = c * b
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAt.hasFDerivWithinAt : ∀ {𝕜 : 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} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivAt f f' x → HasFDerivWithinAt f f' s x
-- Init.Data.Iterators.Basic
/-- Match pattern for the `yield` case. See also `IterStep.yield`.
 -/
Std.PlausibleIterStep.yield : {α : Type u} →
  {β : Type w} →
    {IsPlausibleStep : Std.IterStep α β → Prop} →
      (it' : α) → (out : β) → IsPlausibleStep (Std.IterStep.yield it' out) → Std.PlausibleIterStep IsPlausibleStep
-- Mathlib.Data.Vector.Basic
List.Vector.instInhabited : {α : Type u_1} → {n : ℕ} → [Inhabited α] → Inhabited (List.Vector α n)
-- Lean.Parser.Basic
Lean.Parser.many1Fn : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_eq_sub : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b c : α), toIocMod hp a (b - c) = toIocMod hp (a + c) b - c
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'.eq_5 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS' b c d 4 = d
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.add_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.AddMonObj M]
  [inst_4 : CategoryTheory.AddMonObj N],
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)
-- Mathlib.Logic.Encodable.Basic
ULower.down_up : ∀ {α : Type u_1} [inst : Encodable α] {a : ULower α}, ULower.down a.up = a
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivAt.mul_const' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a : E → 𝔸}
  {a' : E →L[𝕜] 𝔸}, HasFDerivAt a a' x → ∀ (b : 𝔸), HasFDerivAt (fun y => a y * b) (MulOpposite.op b • a') x
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {I : C}
  [CategoryTheory.Injective I] {L : CochainComplex C ℤ} {i : ℤ} (ι : (CochainComplex.singleFunctor C i).obj I ⟶ L)
  [L.IsStrictlyGE i] [QuasiIsoAt ι i], CategoryTheory.IsSplitMono ι
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.nonsingular_of_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  P ≈ Q → (W'.Nonsingular P ↔ W'.Nonsingular Q)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WindowClientCapabilities.mk.sizeOf_spec : ∀ (showDocument? : Option Lean.Lsp.ShowDocumentClientCapabilities),
  sizeOf { showDocument? := showDocument? } = 1 + sizeOf showDocument?
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.isLocalizationMap_nat_int : ∀ (S : AddSubmonoid ℕ), S ≠ ⊥ → S.IsLocalizationMap Nat.cast
-- Lean.Elab.Tactic.Config
/-- Whether this was using `+`/`-`, to be able to give a better error message on type mismatch.  -/
Lean.Elab.Tactic.ConfigItemView.bool : Lean.Elab.Tactic.ConfigItemView → Bool
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.coordinate_eval_8 : ∀ {a0 a1 a2 a3 a4 a5 a6 a7 a8 : ℤ} {t : List ℤ},
  (Lean.Omega.LinearCombo.coordinate 8).eval
      (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: t)) =
    a8
-- Mathlib.Data.ENNReal.Inv
ENNReal.exists_nnreal_pos_mul_lt : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ 0 → ∃ n > 0, ↑n * a < b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {fallback : β}, k ∉ t₁ → Std.ExtDTreeMap.Const.getD (t₁ ∩ t₂) k fallback = fallback
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_rcc_ne_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m...=n).toArray[i]! ≠ 0 ↔ i < (n + 1 - m).toNat ∧ m + ↑i ≠ 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionOptions.mk.injEq : ∀ (triggerCharacters? allCommitCharacters? : Option (Array String)) (resolveProvider : Bool)
  (triggerCharacters?_1 allCommitCharacters?_1 : Option (Array String)) (resolveProvider_1 : Bool),
  ({ triggerCharacters? := triggerCharacters?, allCommitCharacters? := allCommitCharacters?,
        resolveProvider := resolveProvider } =
      { triggerCharacters? := triggerCharacters?_1, allCommitCharacters? := allCommitCharacters?_1,
        resolveProvider := resolveProvider_1 }) =
    (triggerCharacters? = triggerCharacters?_1 ∧
      allCommitCharacters? = allCommitCharacters?_1 ∧ resolveProvider = resolveProvider_1)
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.ZariskisMainProperty.eq_1 : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S),
  Algebra.ZariskisMainProperty R p =
    ∃ r, ↑r ∉ p ∧ Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom r)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.lift.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F : IntermediateField K L}
  (E : IntermediateField K ↥F), IntermediateField.lift E = IntermediateField.map F.val E
-- Aesop.RuleTac.Forward.Basic
Aesop.getForwardHypData : Lean.MetaM Aesop.ForwardHypData
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instCommRing : {p : ℕ} → [hp : Fact (Nat.Prime p)] → CommRing ℤ_[p]
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α} {h' : k ∈ Std.ExtHashMap.filterMap f m},
  (Std.ExtHashMap.filterMap f m).getKey k h' = m.getKey k ⋯
-- Mathlib.Topology.Order.Basic
induced_orderTopology' : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [ta : TopologicalSpace β] [inst_1 : Preorder β] [OrderTopology β]
  (f : α → β),
  (∀ {x y : α}, f x < f y ↔ x < y) →
    (∀ {a : α} {x : β}, x < f a → ∃ b < a, x ≤ f b) → (∀ {a : α} {x : β}, f a < x → ∃ b > a, f b ≤ x) → OrderTopology α
-- Init.Data.UInt.Lemmas
USize.toNat_toUInt64 : ∀ (x : USize), x.toUInt64.toNat = x.toNat
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.instIsMonHomInvOfHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (f : M ≅ N) [CategoryTheory.IsMonHom f.hom],
  CategoryTheory.IsMonHom f.inv
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Interpret an affine isometry as a continuous affine map.  -/
AffineIsometry.toContinuousAffineMap : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] → [inst_8 : NormedAddTorsor V₂ P₂] → (P →ᵃⁱ[𝕜] P₂) → P →ᴬ[𝕜] P₂
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.subsingleton_H_of_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {F : CategoryTheory.Sheaf J AddCommGrpCat},
  CategoryTheory.Limits.IsZero F → ∀ (n : ℕ), Subsingleton (F.H n)
-- Mathlib.Analysis.Convex.Topology
/-- **Alias** of `Convex.nhdsWithin_sdiff_eq_nhdsGT`. -/
Convex.nhdsWithin_diff_eq_nhdsGT : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜},
  Convex 𝕜 s →
    ∀ {a : 𝕜},
      a ∈ closure s → s ∩ Set.Iio a = ∅ → (s ∩ Set.Ioi a).Nonempty → nhdsWithin a (s \ {a}) = nhdsWithin a (Set.Ioi a)
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.instCategory : (R : Type u) → [inst : CommRing R] → CategoryTheory.Category.{v, max (v + 1) u} (AlgCat R)
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Trie.brecOn_3.go : {α : Type} →
  {motive_1 : Lean.Meta.DiscrTree.Trie α → Sort u} →
    {motive_2 : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u} →
      {motive_3 : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u} →
        {motive_4 : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α → Sort u} →
          (t : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) →
            ((t : Lean.Meta.DiscrTree.Trie α) → t.below → motive_1 t) →
              ((t : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
                  Lean.Meta.DiscrTree.Trie.below_1 t → motive_2 t) →
                ((t : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
                    Lean.Meta.DiscrTree.Trie.below_2 t → motive_3 t) →
                  ((t : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) →
                      Lean.Meta.DiscrTree.Trie.below_3 t → motive_4 t) →
                    motive_4 t ×' Lean.Meta.DiscrTree.Trie.below_3 t
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationSpanTarget`
if `P` holds for `R →+* S` whenever there exists a set `{ r }` that spans `S` such that
`P` holds for `R →+* Sᵣ`.

Note that this is equivalent to `RingHom.OfLocalizationFiniteSpanTarget` via
`RingHom.ofLocalizationSpanTarget_iff_finite`, but this has less restrictions when applying.  -/
RingHom.OfLocalizationSpanTarget : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.Data.Prod.Basic
Prod.map_def : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ},
  Prod.map f g = fun p => (f p.1, g p.2)
-- Mathlib.Algebra.Algebra.Pi
AlgEquiv.sumArrowEquivProdArrow_symm_apply_inr : ∀ {α : Type u_1} {β : Type u_2} {R : Type u_3} [inst : CommSemiring R] (S : Type u_8) [inst_1 : Semiring S]
  [inst_2 : Algebra R S] (x : (α → S) × (β → S)),
  (AlgEquiv.sumArrowEquivProdArrow α β R S).symm x = (Equiv.sumArrowEquivProdArrow α β S).symm x