mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.OrderClosed
/-- The only order closed topology on a linear order which is a `PredOrder` and a `SuccOrder`
is the discrete topology.

This theorem is not an instance,
because it causes searches for `PredOrder` and `SuccOrder` with their `Preorder` arguments
and very rarely matches.  -/
DiscreteTopology.of_predOrder_succOrder : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] [PredOrder α] [SuccOrder α],
  DiscreteTopology α
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.cast_symm_apply : ∀ {ι : Type u_9} {M : ι → Type u_10} [inst : (i : ι) → Add (M i)] {i j : ι} (h : i = j) (a : M j),
  (AddEquiv.cast h).symm a = cast ⋯ a
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {R₁ R₂ : CategoryTheory.CommRingObjCat C} →
          (hom : R₁.X ⟶ R₂.X) → [isRingHom : CategoryTheory.IsRingHom hom] → R₁.Hom R₂
-- Mathlib.Data.List.OfFn
List.equivSigmaTuple_symm_apply : ∀ {α : Type u} (f : (n : ℕ) × (Fin n → α)), List.equivSigmaTuple.symm f = List.ofFn f.snd
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- If the integral extension `R → S` is injective, and `S` is a field, then `R` is also a field.  -/
isField_of_isIntegral_of_isField : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S], Function.Injective ⇑(algebraMap R S) → IsField S → IsField R
-- Init.Core
Subtype.mk.inj : ∀ {α : Sort u} {p : α → Prop} {val : α} {property : p val} {val_1 : α} {property_1 : p val_1},
  ⟨val, property⟩ = ⟨val_1, property_1⟩ → val = val_1
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete
/-- Auxiliary definition for `functorCategoryMonoidalClosed`  -/
CategoryTheory.Functor.functorCategoryClosed : (I : Type u₂) →
  [inst : CategoryTheory.Category.{v₂, u₂} I] →
    (C : Type u₁) →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalClosed C] →
            [∀ (F : CategoryTheory.Functor (CategoryTheory.Discrete I) C),
                  (CategoryTheory.Discrete.functor id).HasRightKanExtension F] →
              [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair C] →
                (F : CategoryTheory.Functor I C) → CategoryTheory.Closed F
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.map_distinguished_iff : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] [inst_6 : CategoryTheory.Limits.HasZeroObject D]
  [inst_7 : CategoryTheory.Preadditive C] [inst_8 : CategoryTheory.Preadditive D]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_11 : CategoryTheory.Pretriangulated C]
  [inst_12 : CategoryTheory.Pretriangulated D] [F.IsTriangulated] [F.Full] [F.Faithful]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔
    T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Lean.Meta.Tactic.Grind.Types
/-- Sets `nextDeclIdx` to point past the last local declaration in the local context.

This marks all existing local declarations as already processed by `grind`. Use this when
initializing a goal whose hypotheses should not be processed or after internalizing all of them.
 -/
Lean.Meta.Grind.Goal.setNextDeclToEnd : Lean.Meta.Grind.Goal → Lean.MetaM Lean.Meta.Grind.Goal
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_4.eq : ∀ {i : Type u} {b : Type v} {motive_1 : Lean.Doc.Block i b → Sort u_1}
  {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1}
  {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1}
  {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1}
  (t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) (F_1 : (t : Lean.Doc.Block i b) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_4 t → motive_5 t)
  (F_6 :
    (t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t)
  (F_8 : (t : Lean.Doc.ListItem (Lean.Doc.Block i b)) → Lean.Doc.Block.below_7 t → motive_8 t)
  (F_9 : (t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Lean.Doc.Block.below_8 t → motive_9 t),
  Lean.Doc.Block.brecOn_4 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 =
    F_5 t (Lean.Doc.Block.brecOn_4.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9).2
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.corepresentableByUliftFunctorEquiv_symm_apply_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C}
  (R : F.CorepresentableBy X) {Y : C},
  (CategoryTheory.Functor.corepresentableByUliftFunctorEquiv.symm R).homEquiv = R.homEquiv.trans Equiv.ulift.symm
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_comap_map : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  (I : Ideal R) [inst_3 : RingHomClass F R S], Ideal.map f (Ideal.comap f (Ideal.map f I)) = Ideal.map f I
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.hasPrev : ∀ {l r : List Char} {it : String.Legacy.Iterator}, String.Legacy.Iterator.ValidFor l r it → (it.hasPrev = true ↔ l ≠ [])
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.ext_iff : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H = K ↔ ∀ (x : G), x ∈ H ↔ x ∈ K
-- Mathlib.CategoryTheory.Functor.Currying
/-- The functor `curry : (C × D ⥤ E) ⥤ C ⥤ D ⥤ E` is fully faithful.  -/
CategoryTheory.Functor.fullyFaithfulCurry : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        {E : Type u₄} → [inst_2 : CategoryTheory.Category.{v₄, u₄} E] → CategoryTheory.Functor.curry.FullyFaithful
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasDerivAt.cosh : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasDerivAt f f' x → HasDerivAt (fun x => Real.cosh (f x)) (Real.sinh (f x) * f') x
-- Std.Http.Data.Status
Std.Http.Status.upgradeRequired.sizeOf_spec : sizeOf Std.Http.Status.upgradeRequired = 1
-- Mathlib.Condensed.Epi
CondensedMod.epi_iff_surjective_on_stonean : ∀ (R : Type (u + 1)) [inst : Ring R] {X Y : CondensedMod R} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔
    ∀ (S : Stonean), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S.compHaus)))
-- Std.Time.Date.PlainDate
Std.Time.PlainDate.instHAddOffset_1 : HAdd Std.Time.PlainDate Std.Time.Week.Offset Std.Time.PlainDate
-- Lean.MonadEnv
Lean.hasCompileError : Lean.Environment → Lean.Name → Bool
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.tensorProductEquivOfMapIncludeRight.eq_1 : ∀ (R : Type u_7) (S : Type u_8) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {A : Type u_9}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (M : Submonoid A) (B : Type u_10) [inst_5 : CommSemiring B]
  [inst_6 : Algebra R B] [inst_7 : Algebra A B] [inst_8 : IsScalarTower R A B] [inst_9 : IsLocalization M B]
  (C : Type u_11) [inst_10 : CommSemiring C] [inst_11 : Algebra S C] [inst_12 : Algebra (TensorProduct R S A) C]
  [inst_13 : IsScalarTower S (TensorProduct R S A) C]
  [inst_14 : IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) C],
  IsLocalization.tensorProductEquivOfMapIncludeRight R S M B C =
    AlgEquiv.restrictScalars S
      (IsLocalization.algEquiv (Submonoid.map Algebra.TensorProduct.includeRight M) (TensorProduct R S B) C)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ici_ssubset_Ici : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α], Finset.Ici a ⊂ Finset.Ici b ↔ b < a
-- Mathlib.CategoryTheory.Products.Basic
/-- Whiskering by `F` and then evaluating at `a` is the same as evaluating at `F` and then
applying `F`.  -/
CategoryTheory.whiskeringRightCompEvaluation : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor B C) →
              (a : A) →
                ((CategoryTheory.Functor.whiskeringRight A B C).obj F).comp ((CategoryTheory.evaluation A C).obj a) ≅
                  ((CategoryTheory.evaluation A B).obj a).comp F
-- Mathlib.Topology.Algebra.Monoid
tendsto_finsetSum : ∀ {ι : Type u_1} {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] [ContinuousAdd M]
  {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι),
  (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun b => ∑ c ∈ s, f c b) x (nhds (∑ c ∈ s, a c))
-- Lean.Setup
Lean.instFromJsonModuleSetup : Lean.FromJson Lean.ModuleSetup
-- Init.Data.Int.Order
Int.nonneg_of_mul_nonneg_left : ∀ {a b : ℤ}, 0 ≤ a * b → 0 < b → 0 ≤ a
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg : ∀ {𝕜 : Type u_3} {A : Type u_4} {inst : CommSemiring 𝕜} {inst_1 : PartialOrder 𝕜} {inst_2 : NonUnitalRing A}
  {inst_3 : PartialOrder A} {inst_4 : Module 𝕜 A} [self : NonnegSpectrumClass 𝕜 A] (a : A),
  0 ≤ a → ∀ x ∈ quasispectrum 𝕜 a, 0 ≤ x
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubseqResult.prefix.sizeOf_spec : ∀ (s : Lean.Grind.AC.Seq), sizeOf (Lean.Grind.AC.SubseqResult.prefix s) = 1 + sizeOf s
-- Mathlib.RingTheory.Algebraic.Basic
Polynomial.transcendental_X : ∀ (R : Type u) [inst : CommRing R], Transcendental R Polynomial.X
-- Mathlib.Analysis.Calculus.MeanValue
/-- If two functions have equal Fréchet derivatives at every point of a connected open set,
and are equal at one point in that set, then they are equal on that set.  -/
IsOpen.eqOn_of_fderiv_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f g : E → G} {s : Set E} {x : E},
  IsOpen s →
    IsPreconnected s →
      DifferentiableOn 𝕜 f s →
        DifferentiableOn 𝕜 g s → (∀ x ∈ s, fderiv 𝕜 f x = fderiv 𝕜 g x) → x ∈ s → f x = g x → Set.EqOn f g s
-- Init.Data.Array.Zip
Array.map_prod_left_eq_zip : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β}, Array.map (fun x => (x, f x)) xs = xs.zip (Array.map f xs)
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.RanIsSheafOfIsCocontinuous.fac' : ∀ {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] {G : CategoryTheory.Functor C D} {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} [inst_3 : G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A}
  (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F}
  (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X}
  (s : CategoryTheory.Limits.Multifork (S.index R)) (j : CategoryTheory.StructuredArrow (Opposite.op X) G.op),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s)
      (CategoryTheory.CategoryStruct.comp (R.map j.hom) (α.app j.right)) =
    CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s j.hom.unop
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
/-- The arithmetic function corresponding to the Dirichlet series `f(q⁻ˢ)`.
For example, if `f = 1 + X + X² + ...` and `q = p`, then `f(q⁻ˢ) = 1 + p⁻ˢ + p⁻²ˢ + ...`.

If `q ≤ 1` then `k ↦ q ^ k` is not injective, so we use the junk value `f.constantCoeff`.  -/
ArithmeticFunction.ofPowerSeries : {R : Type u_1} → [inst : CommSemiring R] → ℕ → PowerSeries R →ₐ[R] ArithmeticFunction R
-- Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
CategoryTheory.coherentTopology.isLocallySurjective_iff : ∀ {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] {FD : D → D → Type u_3} {CD : D → Type w}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  [inst_4 : CategoryTheory.Preregular C] [inst_5 : CategoryTheory.FinitaryExtensive C]
  {F G : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) D} (f : F ⟶ G)
  [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)],
  CategoryTheory.Sheaf.IsLocallySurjective f ↔
    CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f.hom
-- Mathlib.RingTheory.Derivation.ToSquareZero
/-- Given a tower of algebras `R → A → B`, and a square-zero `I : Ideal B`, each lift `A →ₐ[R] B`
of the canonical map `A →ₐ[R] B ⧸ I` corresponds to an `R`-derivation from `A` to `I`.  -/
derivationToSquareZeroOfLift : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                (I : Ideal B) →
                  [inst_5 : Algebra A B] →
                    [inst_6 : IsScalarTower R A B] →
                      I ^ 2 = ⊥ →
                        (f : A →ₐ[R] B) →
                          (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I) → Derivation R A ↥I
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- If `f` and `g` are continuous on `[a, b]`, `a < b`, `f x ≤ g x` on this interval, and
`f c < g c` at some point `c ∈ [a, b]`, then `∫ x in a..b, f x < ∫ x in a..b, g x`.  -/
intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt : ∀ {f g : ℝ → ℝ} {a b : ℝ},
  a < b →
    ContinuousOn f (Set.Icc a b) →
      ContinuousOn g (Set.Icc a b) →
        (∀ x ∈ Set.Ioc a b, f x ≤ g x) →
          (∃ c ∈ Set.Icc a b, f c < g c) → ∫ (x : ℝ) in a..b, f x < ∫ (x : ℝ) in a..b, g x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get_eq_get? : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α fun x => β)
  {h : Std.DTreeMap.Internal.Impl.contains k l = true},
  some (Std.DTreeMap.Internal.Impl.Const.get l k h) = Std.DTreeMap.Internal.Impl.Const.get? l k
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mk'_toSubsemigroup : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R} {sg : Subsemigroup R} (hg : ↑sg = s)
  {sa : AddSubmonoid R} (ha : ↑sa = s), (NonUnitalSubsemiring.mk' s sg hg sa ha).toSubsemigroup = sg
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₂ → (m₁ ∪ m₂).getKey? k = m₁.getKey? k
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
/-- **Alias** of `CategoryTheory.Functor.mem_restrictedTopology_iff`.

---

If a functor `G : C ⥤ (D, K)` is locally fully faithful and locally dense, `S` is
a covering in the restricted topology on `C` if its image generates a `K`-cover.  -/
CategoryTheory.Functor.mem_inducedTopology_sieves_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D}
  {K : CategoryTheory.GrothendieckTopology D} [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K]
  {X : C} {S : CategoryTheory.Sieve X},
  S ∈ (G.restrictedTopology K) X ↔ CategoryTheory.Sieve.functorPushforward G S ∈ K (G.obj X)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instAdd : (A : Type u_3) → (E : Type u_4) → [Add E] → Add (WithCStarModule A E)
-- Mathlib.Data.Set.Image
/-- Variant of `range_comp` using a lambda instead of function composition.
 -/
Set.range_comp' : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (g : α → β) (f : ι → α), (Set.range fun x => g (f x)) = g '' Set.range f
-- Mathlib.Data.Nat.Choose.Multinomial
Multiset.multinomial_zero : Multiset.multinomial 0 = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_inter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_contains : Std.DTreeMap.Internal.Impl.contains k (m₁.inter m₂ ⋯) = true},
  Std.DTreeMap.Internal.Impl.Const.get (m₁.inter m₂ ⋯) k h_contains = Std.DTreeMap.Internal.Impl.Const.get m₁ k ⋯
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The ring structure is inherited as the pullback under the injective map
`DoubleCentralizer.toProdMulOpposite : 𝓜(𝕜, A) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ`  -/
DoubleCentralizer.instRing : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → Ring (DoubleCentralizer 𝕜 A)
-- Init.Data.Vector.Lemmas
Vector.toArray_swapAt : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α} (h : i < n),
  ((xs.swapAt i x h).1, (xs.swapAt i x h).2.toArray) = ((xs.toArray.swapAt i x ⋯).1, (xs.toArray.swapAt i x ⋯).2)
-- Mathlib.Algebra.Category.MonCat.Yoneda
/-- The `CommMonCat`-valued coyoneda embedding composed with the forgetful functor is the usual
coyoneda embedding.  -/
CommMonCat.coyonedaForget : CommMonCat.coyoneda.comp
    ((CategoryTheory.Functor.whiskeringRight CommMonCat CommMonCat (Type u_1)).obj (CategoryTheory.forget CommMonCat)) ≅
  CategoryTheory.coyoneda
-- Batteries.Data.BinomialHeap.Basic
/-- An empty heap.  -/
Batteries.BinomialHeap.Imp.Heap.nil : {α : Type u} → Batteries.BinomialHeap.Imp.Heap α
-- Lean.Elab.PreDefinition.Structural.Eqns
/-- Searches in the lhs of goal for a `.brecOn` application, possibly with extra arguments
and under `PProd` projections. Returns the `.brecOn` application and the context
`(fun x => (x).1.2.3 extraArgs = rhs)`.
 -/
_private.Lean.Elab.PreDefinition.Structural.Eqns.0.Lean.Elab.Structural.findBRecOnLHS : Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.radius_regularizedGaussHGFunSeries_eq_one : ∀ {a b : ℂ} (c : ℂ), (∀ (k : ℕ), a ≠ -↑k ∧ b ≠ -↑k) → (a.regularizedGaussHGFunSeries b c).radius = 1
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsColimitsOfShapeFintypeCatDiscretePEmpty : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.Limits.ReflectsColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F
-- Mathlib.Data.Finset.Lattice.Basic
Finset.mem_of_mem_inter_left : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finset α}, a ∈ s₁ ∩ s₂ → a ∈ s₁
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) {Z : AlgebraicGeometry.Scheme} (h : ↑U ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict f U).hom
      (CategoryTheory.CategoryStruct.comp (f ∣_ U) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f U.ι) h
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_eventually_congr_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x},
  s =ᶠ[nhds x] t → VectorField.mlieBracketWithin I V W s =ᶠ[nhds x] VectorField.mlieBracketWithin I V W t
-- Aesop.Rule
Aesop.SafeRuleInfo.mk.inj : ∀ {penalty : ℤ} {safety : Aesop.Safety} {penalty_1 : ℤ} {safety_1 : Aesop.Safety},
  { penalty := penalty, safety := safety } = { penalty := penalty_1, safety := safety_1 } →
    penalty = penalty_1 ∧ safety = safety_1
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.subtypeDomain_neg : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] {p : ι → Prop} [inst_1 : DecidablePred p]
  {v : Π₀ (i : ι), β i}, DFinsupp.subtypeDomain p (-v) = -DFinsupp.subtypeDomain p v
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry from an emetric space is injective  -/
Isometry.injective : ∀ {α : Type u} {β : Type v} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → Function.Injective f
-- Mathlib.RingTheory.Idempotents
_private.Mathlib.RingTheory.Idempotents.0.RingHom.prod_bijective_of_isIdempotentElem.match_1_1.eq_2 : ∀ (motive : Fin 2 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_2 ()
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TacticMVarKind.autoParam.inj : ∀ {argName argName_1 : Lean.Name},
  Lean.Elab.Term.TacticMVarKind.autoParam argName = Lean.Elab.Term.TacticMVarKind.autoParam argName_1 →
    argName = argName_1
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.abs_edgeDensity_sub_edgeDensity_le_one_sub_mul : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] {s₁ s₂ : Finset α}
  {t₁ t₂ : Finset β},
  s₂ ⊆ s₁ →
    t₂ ⊆ t₁ →
      s₂.Nonempty →
        t₂.Nonempty →
          |Rel.edgeDensity r s₂ t₂ - Rel.edgeDensity r s₁ t₁| ≤ 1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card)
-- Init.Data.Int.DivMod.Lemmas
Int.negSucc_ediv : ∀ (m : ℕ) {b : ℤ}, 0 < b → Int.negSucc m / b = -((↑m).ediv b + 1)
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.Head.const.inj : ∀ {c c_1 : Lean.Name}, Mathlib.Tactic.Push.Head.const c = Mathlib.Tactic.Push.Head.const c_1 → c = c_1
-- Mathlib.Algebra.Group.Subgroup.Basic
AddGroup.addConjugates_subset_normal : ∀ {G : Type u_1} [inst : AddGroup G] {N : AddSubgroup G} [tn : N.Normal] {a : G}, a ∈ N → addConjugatesOf a ⊆ ↑N
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.take.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive 0 x)
  (h_2 : (n : ℕ) → motive n.succ []) (h_3 : (n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)),
  (match 0, x with
    | 0, x => h_1 x
    | n.succ, [] => h_2 n
    | n.succ, a :: as => h_3 n a as) =
    h_1 x
-- Mathlib.Control.Functor.Multivariate
_private.Mathlib.Control.Functor.Multivariate.0.MvFunctor.g' : {β : Type u} →
  (rr : β → β → Prop) →
    (n : ℕ) →
      (α : TypeVec.{u} n) →
        TypeVec.Arrow (fun i => { p_1 // α.RelLast rr p_1.1 p_1.2 }) fun i =>
          { p_1 // TypeVec.ofRepeat (α.RelLast' rr i (TypeVec.prod.mk i p_1.1 p_1.2)) }
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.nnnorm : {E : Type u_2} → [NNNorm E] → NNNorm (ULift.{u_5, u_2} E)