mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.mk : {F : Type u → Type v} →
  [inst : Applicative F] →
    {G : Type u → Type w} →
      [inst_1 : Applicative G] →
        (app : (α : Type u) → F α → G α) →
          (∀ {α : Type u} (x : α), app α (pure x) = pure x) →
            (∀ {α β : Type u} (x : F (α → β)) (y : F α), app β (x <*> y) = app (α → β) x <*> app α y) →
              ApplicativeTransformation F G
-- Init.Data.String.Lemmas.Order
String.Pos.ofSliceTo_ne_endPos : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos}, p ≠ (s.sliceTo p₀).endPos → String.Pos.ofSliceTo p ≠ s.endPos
-- Mathlib.Analysis.Convex.Cone.Dual
ProperCone.dual_zero : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : ClosedIciTopology R] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : TopologicalSpace M] [inst_8 : AddCommGroup N] [inst_9 : Module R N] [inst_10 : TopologicalSpace N]
  {p : M →ₗ[R] N →ₗ[R] R} [inst_11 : p.IsContPerfPair], ProperCone.dual p 0 = ⊤
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelDesc.congr_simp : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y} {g g_1 : Y ⟶ Z} (e_g : g = g_1) (w : CategoryTheory.CategoryStruct.comp f g = 0),
  SemiNormedGrp.explicitCokernelDesc w = SemiNormedGrp.explicitCokernelDesc ⋯
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_le_sub_iff_le_add : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, -b ≤ a - c ↔ c ≤ a + b
-- Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
/-- If `f` is analytic on the ball of convergence of its Taylor series, then the series converges
to `f` on this ball. This is a stronger version of `AnalyticAt.hasFPowerSeriesAt` that requires
the assumption `RCLike 𝕜`.

For example, over the `p`-adic numbers, the indicator function of the unit ball is
analytic everywhere, but it agrees with the sum of its Taylor series only on this unit ball.  -/
AnalyticOn.hasFPowerSeriesOnBall : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜},
  0 < (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial).radius →
    AnalyticOn 𝕜 f
        (Metric.eball x (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial).radius) →
      HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x
        (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial).radius
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- If the product comparison morphism is an iso, its inverse is natural in both argument.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {A B A' B' : C}
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)] (f : A ⟶ A')
  (g : B ⟶ B') [inst_5 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A' B')],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B))
      (F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A' B'))
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_union : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (s t : Set α),
  Metric.cthickening δ (s ∪ t) = Metric.cthickening δ s ∪ Metric.cthickening δ t
-- Mathlib.NumberTheory.MulChar.Duality
MulChar.exists_apply_ne_one_iff_exists_monoidHom : ∀ {M : Type u_1} {R : Type u_2} [inst : CommMonoid M] [inst_1 : CommRing R] (a : Mˣ), (∃ χ, χ ↑a ≠ 1) ↔ ∃ φ, φ a ≠ 1
-- Batteries.Classes.Order
Std.LawfulCmp.mk : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] {cmp : α → α → Ordering} [toTransCmp : Std.TransCmp cmp]
  [toLawfulEqCmp : Std.LawfulEqCmp cmp],
  (∀ {x y : α}, cmp x y = Ordering.lt ↔ x < y) → (∀ {x y : α}, (cmp x y).isLE = true ↔ x ≤ y) → Std.LawfulCmp cmp
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.CoPolarizationIn_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M] [IsScalarTower S R M]
  [inst_10 : Module S N] [inst_11 : IsScalarTower S R N] [inst_12 : P.IsValuedIn S] [inst_13 : Fintype ι]
  (x : ↥(P.corootSpan S)), (P.CoPolarizationIn S) x = P.CoPolarization ↑x
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.div_mem_comm_iff : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {a b : G}, a / b ∈ H ↔ b / a ∈ H
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.MLListImpl.thunk : {m : Type u → Type u} → {α : Type u} → Thunk (MLList.MLListImpl✝ m α) → MLList.MLListImpl✝ m α
-- Lean.Meta.Basic
/-- When `univApprox` is set to true,
we use approximations when solving postponed universe constraints.
Examples:
- `max u ?v =?= u` is solved with `?v := u` and ignoring the solution `?v := 0`.
- `max u w =?= max u ?v` is solved with `?v := w` ignoring the solution `?v := max u w`
 -/
Lean.Meta.Config.univApprox : Lean.Meta.Config → Bool
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend.eq_1 : ∀ {α : Type u_2} {P : α → Prop} (m : (s : α) → P s → ENNReal) (s : α), MeasureTheory.extend m s = ⨅ (h : P s), m s h
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.eLpNorm_lt_top : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  [inst_1 : TopologicalSpace ε] {f : α → ε}, MeasureTheory.MemLp f p μ → MeasureTheory.eLpNorm f p μ < ⊤
-- Mathlib.Algebra.Group.Prod
/-- The equivalence between `M × N` and `N × M` given by swapping the
components is additive.  -/
AddEquiv.prodComm : {M : Type u_3} → {N : Type u_4} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M × N ≃+ N × M
-- Std.Data.Internal.List.Associative
Std.Internal.List.perm_cons_getEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α}
  (h : Std.Internal.List.containsKey a l = true), ∃ l', l.Perm (Std.Internal.List.getEntry a l h :: l')
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMap_sum : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : ContinuousAdd M₂] {ι : Type u_9}
  (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂), ↑(∑ d ∈ t, f d) = ∑ d ∈ t, ↑(f d)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofCommandInfo.sizeOf_spec : ∀ (i : Lean.Elab.CommandInfo), sizeOf (Lean.Elab.Info.ofCommandInfo i) = 1 + sizeOf i
-- Mathlib.Logic.IsEmpty.Basic
biTotal_iff_isEmpty_right : ∀ {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α], Relator.BiTotal R ↔ IsEmpty β
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- A function is integrable for the counting measure iff its norm is summable.  -/
MeasureTheory.integrable_count_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup β] [MeasurableSingletonClass α]
  {f : α → β}, MeasureTheory.Integrable f MeasureTheory.Measure.count ↔ Summable fun x => ‖f x‖
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.angle_eq_iff_two_pi_dvd_sub : ∀ {ψ θ : ℝ}, ↑θ = ↑ψ ↔ ∃ k, θ - ψ = 2 * Real.pi * ↑k
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.merge.match_1.eq_1 : ∀ {α : Type u_1} (motive : α × Batteries.BinomialHeap.Imp.HeapNode α → Sort u_2) (a : α)
  (n : Batteries.BinomialHeap.Imp.HeapNode α)
  (h_1 : (a : α) → (n : Batteries.BinomialHeap.Imp.HeapNode α) → motive (a, n)),
  (match (a, n) with
    | (a, n) => h_1 a n) =
    h_1 a n
-- Std.Data.ExtTreeSet.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtTreeSet.get? : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → Option α
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.inaccessible.inj : ∀ {e e_1 : Lean.Expr}, Lean.Meta.Match.Pattern.inaccessible e = Lean.Meta.Match.Pattern.inaccessible e_1 → e = e_1
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_one : ∀ {R : Type u} [inst : CommRing R] (A : AlgCat R), CategoryTheory.MonObj.one = ModuleCat.ofHom (Algebra.linearMap R ↑A)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.coe_mk : ∀ {P : Type u_2} [inst : MetricSpace P] (c : P) (r : ℝ),
  Metric.sphere { center := c, radius := r }.center { center := c, radius := r }.radius = Metric.sphere c r
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.essSurj_of_hasRightResolutions : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₂]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂]
  [Φ.HasRightResolutions], (Φ.functor.comp L₂).EssSurj
-- Mathlib.GroupTheory.OreLocalization.Cardinality
AddOreLocalization.oreSub_zero_surjective_of_finite_right : ∀ {R : Type u} [inst : AddMonoid R] (S : AddSubmonoid R) [inst_1 : AddOreLocalization.AddOreSet S] (X : Type v)
  [inst_2 : AddAction R X] [Finite X], Function.Surjective fun x => x -ₒ 0
-- Mathlib.Order.WithBot
WithBot.map_toDual : ∀ {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : WithBot α),
  WithBot.map f (WithBot.toDual a) = WithBot.map (⇑OrderDual.toDual ∘ f) a
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.tendsto_sigmoid_atTop : Filter.Tendsto Real.sigmoid Filter.atTop (nhds 1)
-- Mathlib.Analysis.Convex.Strict
strictConvex_Ioi : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace β]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r : β), StrictConvex 𝕜 (Set.Ioi r)
-- Mathlib.SetTheory.Ordinal.Univ
/-- Principal segment version of the lift operation on ordinals, embedding `Ordinal.{u}` in
`Ordinal.{v}` as a principal segment when `u < v`.  -/
Ordinal.liftPrincipalSeg : Ordinal.{u} <i Ordinal.{max (u + 1) v}
-- Batteries.Data.Vector.Basic
/-- Auxiliary tail-recursive function for scanlM  -/
Vector.scanlM.loop : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    {α : Type u_3} →
      {n : ℕ} → [Monad m] → (β → α → m β) → Vector α n → β → (i : ℕ) → i ≤ n → Vector β i → m (Vector β (n + 1))
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.union_div_inter_subset_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s₁ s₂ t₁ t₂ : Finset α},
  (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂
-- Std.Do.Triple.Basic
/-- A Hoare triple for reasoning about monadic programs. A Hoare triple `Triple x P Q` is a
*specification* for `x`: if assertion `P` holds before `x`, then postcondition `Q` holds after
running `x`.

`⦃P⦄ x ⦃Q⦄` is convenient syntax for `Triple x P Q`.
 -/
Std.Do.triple : Lean.ParserDescr
-- Mathlib.Order.Interval.Finset.Defs
WithBot.insertBot.eq_1 : ∀ {α : Type u_1},
  WithBot.insertBot =
    OrderEmbedding.ofMapLEIff (fun s => Finset.cons ⊥ (Finset.map Function.Embedding.coeWithBot s) ⋯) ⋯
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.map_add_left_Icc : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  [ExistsAddOfLE α] [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Finset.map (addLeftEmbedding c) (Finset.Icc a b) = Finset.Icc (c + a) (c + b)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α} {fallback : β}, m.contains a = false → m.getD a fallback = fallback
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
_private.Mathlib.RingTheory.Bialgebra.MonoidAlgebra.0.MonoidAlgebra.mapDomainOfBialgHomFun.congr_simp : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G]
  [inst_3 : Group H] (f f_1 : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H),
  f = f_1 →
    ∀ (g g_1 : G), g = g_1 → MonoidAlgebra.mapDomainOfBialgHomFun✝ f g = MonoidAlgebra.mapDomainOfBialgHomFun✝ f_1 g_1
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_inv_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : AddCommGroup Γ] [inst_2 : IsOrderedAddMonoid Γ]
  [inst_3 : Field R] (x : HahnSeries Γ R), x⁻¹.cardSupp ≤ max Cardinal.aleph0 x.cardSupp
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
/-- For nonzero `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b`  -/
factorization_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : NormalizationMonoid α]
  [inst_3 : DecidableEq α] {a b : α}, a ≠ 0 → b ≠ 0 → factorization (a * b) = factorization a + factorization b
-- Mathlib.Algebra.Group.Pi.Basic
Sum.elim_mul_mul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a a' : α → γ) (b b' : β → γ) [inst : Mul γ],
  Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'
-- Mathlib.GroupTheory.Index
AddSubgroup.index_antitone : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H ≤ K → ∀ [H.FiniteIndex], K.index ≤ H.index
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_single : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} (b : β),
  (∀ (b' : β), b' ≠ b → f b' = 1) →
    ∀ (L : optParam (SummationFilter β) (SummationFilter.unconditional β)) [L.LeAtTop], HasProd f (f b) L
-- Mathlib.CategoryTheory.Limits.SmallComplete
/-- A small category with products is a thin category.

in Lean, a preorder category is one where the morphisms are in Prop, which is weaker than the usual
notion of a preorder/thin category which says that each homset is subsingleton; we show the latter
rather than providing a `Preorder C` instance.
 -/
CategoryTheory.instIsThin : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasProducts C], Quiver.IsThin C
-- Mathlib.Order.RelClasses
IsOrderConnected.mk : ∀ {α : Type u} {lt : α → α → Prop}, (∀ (a b c : α), lt a c → lt a b ∨ lt b c) → IsOrderConnected α lt
-- Mathlib.Data.Set.Lattice
Set.subset_sUnion_of_mem : ∀ {α : Type u_1} {S : Set (Set α)} {t : Set α}, t ∈ S → t ⊆ ⋃₀ S
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.triangle_assoc : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c}
  (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g) h
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instLTPosition : LT Lean.Lsp.Position
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.instSmallCategorySmallFilteredIntermediate : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          (F : CategoryTheory.Functor D C) →
            CategoryTheory.SmallCategory (CategoryTheory.IsFiltered.SmallFilteredIntermediate F)
-- Mathlib.Tactic.Linter.TextBased
/-- The path to the file which was linted  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ErrorContext.path : Mathlib.Linter.TextBased.ErrorContext✝ → System.FilePath
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.mk_def : ∀ {K : Type u_1} [inst : CommRing K] [inst_1 : IsDomain K] (p q : Polynomial K),
  RatFunc.mk p q =
    {
      toFractionRing :=
        (algebraMap (Polynomial K) (FractionRing (Polynomial K))) p /
          (algebraMap (Polynomial K) (FractionRing (Polynomial K))) q }
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.stalkMap_injective_of_isAffine : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine Y] (x : ↥X),
  (∀ (g : ↑(Y.presheaf.obj (Opposite.op ⊤))),
      (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
            ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.Γgerm (f x))) g) =
          0 →
        (CategoryTheory.ConcreteCategory.hom (Y.presheaf.Γgerm (f x))) g = 0) →
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
tangentMapWithin_prodSnd : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set (M × M')}
  {p : TangentBundle (I.prod I') (M × M')},
  UniqueMDiffAt[s] p.proj → tangentMapWithin (I.prod I') I' Prod.snd s p = ⟨p.proj.2, p.snd.2⟩
-- Lean.Setup
/-- A module's setup information as described by a JSON file.  -/
Lean.ModuleSetup : Type
-- Mathlib.Combinatorics.SimpleGraph.UniversalVerts
SimpleGraph.deleteUniversalVerts_adj : ∀ {V : Type u_1} (G : SimpleGraph V) (u v : V),
  G.deleteUniversalVerts.Adj u v = (u ∉ G.universalVerts ∧ v ∉ G.universalVerts ∧ G.Adj u v)
-- Mathlib.LinearAlgebra.Finsupp.SumProd
Finsupp.sumFinsuppLEquivProdFinsupp_apply : ∀ {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_7}
  {β : Type u_8} (a : α ⊕ β →₀ M),
  (Finsupp.sumFinsuppLEquivProdFinsupp R) a = Finsupp.sumFinsuppAddEquivProdFinsupp.toFun a
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite : AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.LocallyQuasiFinite fun {R S} [CommRing R] [CommRing S] =>
  RingHom.QuasiFinite
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec_smul' : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Semigroup α] (w : m → α) (r : α) (v : n → α),
  Matrix.vecMulVec w (r • v) = Matrix.vecMulVec (MulOpposite.op r • w) v
-- Mathlib.Topology.MetricSpace.Thickening
IsClosed.cthickening_eq_biUnion_closedBall : ∀ {δ : ℝ} {α : Type u_2} [inst : PseudoMetricSpace α] [ProperSpace α] {E : Set α},
  IsClosed E → 0 ≤ δ → Metric.cthickening δ E = ⋃ x ∈ E, Metric.closedBall x δ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_alter!_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).isEmpty = false →
        ((Std.DTreeMap.Internal.Impl.alter! k f t).minKey! = k ↔
          (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Map an `Arrow.Relation` along a refinement `S ⟶ T`.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {S T : J.Cover X} → {I₁ I₂ : S.Arrow} → I₁.Relation I₂ → (f : S ⟶ T) → (I₁.map f).Relation (I₂.map f)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.pow_apply : ∀ {A : Type u_2} {E : Type u_6} [inst : Monoid A] [inst_1 : TopologicalSpace A] [inst_2 : CommMonoid E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousMul E] (f : A →ₜ* E) (n : ℕ) (a : A), (f ^ n) a = f a ^ n
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.homMk'_mk_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T),
  (CategoryTheory.CostructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯
-- Mathlib.Data.Quot
/-- Induction on two `Quotient` arguments `a` and `b`, result type depends on `⟦a⟧` and `⟦b⟧`.  -/
Quotient.hrecOn₂ : {α : Sort u_1} →
  {β : Sort u_2} →
    {sa : Setoid α} →
      {sb : Setoid β} →
        {φ : Quotient sa → Quotient sb → Sort u_3} →
          (qa : Quotient sa) →
            (qb : Quotient sb) →
              (f : (a : α) → (b : β) → φ ⟦a⟧ ⟦b⟧) →
                (∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ ≍ f a₂ b₂) → φ qa qb
-- Mathlib.Order.SuccPred.Basic
Order.lt_succ_iff_not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α}, a < Order.succ a ↔ ¬IsMax a
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
/-- If `G` acts naturally on `F.obj X` for each `X : C`, this is the canonical
group homomorphism into the automorphism group of `F`.  -/
CategoryTheory.PreGaloisCategory.toAut : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      (G : Type u_1) →
        [inst_1 : Group G] →
          [inst_2 : (X : C) → MulAction G (F.obj X).obj] →
            [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] → G →* CategoryTheory.Aut F
-- Init.Tactics
/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.
```
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"
```

This command can also be used in `simp_all` and `dsimp`.
 -/
Lean.Parser.Tactic.tacticSimp_all?!_ : Lean.ParserDescr
-- Mathlib.Algebra.Order.Ring.Basic
IsSquare.nonneg : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] {x : R},
  IsSquare x → 0 ≤ x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : β k → β k},
      (t.modify k f).getKey? k' = if cmp k k' = Ordering.eq then if k ∈ t then some k else none else t.getKey? k'
-- Mathlib.Order.Atoms
IsSimpleOrder.mk : ∀ {α : Type u_4} [inst : LE α] [inst_1 : BoundedOrder α] [toNontrivial : Nontrivial α],
  (∀ (a : α), a = ⊥ ∨ a = ⊤) → IsSimpleOrder α
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.addUnit'.eq_1 : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a),
  h.addUnit' = { val := a, neg := -a, val_neg := ⋯, neg_val := ⋯ }
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.nsmul_piAntidiag_univ : ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] (m : ℕ) {n : ℕ},
  n ≠ 0 → n • Finset.univ.piAntidiag m = {f ∈ Finset.univ.piAntidiag (n * m) | ∀ (i : ι), n ∣ f i}