mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Extension
/-- Converts the syntax of a value from a `set_option` to a `DataValue`, matching the forms accepted by
the `optionValue` parser. Returns `none` for an unrecognized value, in which case the option is left
unchanged during parsing and the error is reported during elaboration.
 -/
_private.Lean.Parser.Extension.0.Lean.Parser.optionValueToDataValue? : Lean.Syntax → Option Lean.DataValue
-- Mathlib.Algebra.Divisibility.Basic
RightDvd.of_mul_left : ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, b * a ∣ᵣ c → a ∣ᵣ c
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.instLECastMode : LE Mathlib.Tactic.DepRewrite.CastMode
-- Std.Do.WP.SimpLemmas
Std.Do.WP.throw_EStateM : ∀ {ε σ α : Type u_1} {e : ε}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))},
  (Std.Do.wp (MonadExceptOf.throw e)).apply Q = Q.2.1 e
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.induction_on_adjoin_finset : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Finset E)
  (P : IntermediateField F E → Prop),
  P ⊥ →
    (∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)) →
      P (IntermediateField.adjoin F ↑S)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_norm_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ} {g : α → F}
  {f' : α → E'} {l : Filter α}, Asymptotics.IsBigOWith c l (fun x => ‖f' x‖) g ↔ Asymptotics.IsBigOWith c l f' g
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.monotone_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C},
  P ≤ Q → P.isoClosure ≤ Q.isoClosure
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.sum_comm : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β},
  ∑ x ∈ s, ∑ y ∈ t, f x y = ∑ y ∈ t, ∑ x ∈ s, f x y
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω), μ.toFiniteMeasure.mass = 1
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableWithinAt.cle_arrowCongr : ∀ {𝕜 : 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] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_17}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} {s : Set M}
  {x : M},
  (MDiffAt[s] fun x => ↑(f x).symm) x →
    (MDiffAt[s] fun x => ↑(g x)) x → (MDiffAt[s] fun y => ↑((f y).arrowCongr (g y))) x
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.compHom.eq_1 : ∀ {M : Type uM} {N : Type uN} {P : Type uP} [inst : MulOneClass M] [inst_1 : CommMonoid N] [inst_2 : CommMonoid P],
  MonoidHom.compHom =
    { toFun := fun g => { toFun := g.comp, map_one' := ⋯, map_mul' := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_arrow : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C)
  (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ) (i : ℕ)
  (hi : autoParam (i < n) CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_arrow._auto_1),
  (CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc).arrow i hi =
    CategoryTheory.ComposableArrows.mk₁ (mapSucc ⟨i, hi⟩)
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Node.measure.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (es : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))),
  (Lean.PersistentHashMap.Node.entries es).measure = Lean.PersistentHashMap.Node.measure.measureEntries✝ es 0
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.coe_sub : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β] (f g : ZeroAtInftyContinuousMap α β), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Data.ZMod.Basic
ZMod.cast_one : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] {m : ℕ} [CharP R m], m ∣ n → ZMod.cast 1 = 1
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.lift_symm_apply_coe : ∀ {R : Type u_1} [inst : CommRing R] {d : ℤ} (f : ℤ√d →+* R), ↑(Zsqrtd.lift.symm f) = f Zsqrtd.sqrtd
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Transport an adjunction along a natural isomorphism on the right.  -/
CategoryTheory.Adjunction.ofNatIsoRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} → {H : CategoryTheory.Functor D C} → (H ⊣ F) → (F ≅ G) → (H ⊣ G)
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.instIsStrictlyLECochainComplexOfNatInt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.ProjectiveResolution X),
  R.cochainComplex.IsStrictlyLE 0
-- Mathlib.Topology.LocallyFinite
LocallyFinite.subset : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f g : ι → Set X},
  LocallyFinite f → (∀ (i : ι), g i ⊆ f i) → LocallyFinite g
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
/-- `AddSubmonoid.neg` distributes over multiplication.

This is available as an instance in the `Pointwise` locale.  -/
AddSubmonoid.hasDistribNeg : {R : Type u_2} → [inst : NonUnitalNonAssocRing R] → HasDistribNeg (AddSubmonoid R)
-- Mathlib.Topology.EMetricSpace.Lipschitz
LocallyLipschitz.mul_end : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f g : Function.End α},
  LocallyLipschitz f → LocallyLipschitz g → LocallyLipschitz (f * g)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.foldlM_toArray : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'}
  [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m]
  {f : γ → β → m γ} {init : γ} {it : Std.Iter β}, Array.foldlM f init it.toArray = Std.Iter.foldM f init it
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.coe_inf : ∀ {ι : Type u_1} (I J : WithBot (BoxIntegral.Box ι)), ↑(I ⊓ J) = ↑I ∩ ↑J
-- Std.Internal.Do.Triple.Basic
/-- Hoare triple notation with a binder for the return value.  -/
Std.Internal.Do.tripleBinderNotation : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic.0.termY_1 : Lean.ParserDescr
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SymExtension.modifyState : {σ : Type} → Lean.Meta.Sym.SymExtension σ → (σ → σ) → Lean.Meta.Sym.SymM Unit
-- Std.Http.Data.URI.Encoding
List.toByteArray.loop.eq_2 : ∀ (x : ByteArray) (b : UInt8) (bs : List UInt8), List.toByteArray.loop (b :: bs) x = List.toByteArray.loop bs (x.push b)
-- Std.Data.DTreeMap.Internal.Queries
/-- Support for the `for` construct in `do` blocks.  -/
Std.DTreeMap.Internal.Impl.forIn : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      {m : Type w → Type u_1} →
        [Monad m] → ((a : α) → β a → δ → m (ForInStep δ)) → δ → Std.DTreeMap.Internal.Impl α β → m δ
-- Mathlib.MeasureTheory.PiSystem
IsPiSystem.singleton : ∀ {α : Type u_1} (S : Set α), IsPiSystem {S}
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mk'.congr_simp : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s s_1 : Set R) (e_s : s = s_1) (sg sg_1 : Subsemigroup R)
  (e_sg : sg = sg_1) (hg : ↑sg = s) (sa sa_1 : AddSubmonoid R) (e_sa : sa = sa_1) (ha : ↑sa = s),
  NonUnitalSubsemiring.mk' s sg hg sa ha = NonUnitalSubsemiring.mk' s_1 sg_1 ⋯ sa_1 ⋯
-- Std.Data.HashMap.Lemmas
Std.HashMap.forall_mem_keysArray_iff_forall_mem_getKey : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {p : α → Prop}, (∀ k ∈ m.keysArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.getKey k h)
-- Mathlib.LinearAlgebra.Matrix.DotProduct
dotProduct_le_dotProduct_of_nonneg_right : ∀ {n : Type u_2} {R : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [inst_3 : Fintype n]
  {u v w : n → R}, u ≤ v → 0 ≤ w → u ⬝ᵥ w ≤ v ⬝ᵥ w
-- Mathlib.Algebra.Group.Prod
Prod.instRightCancelMonoid : {M : Type u_3} → {N : Type u_4} → [RightCancelMonoid M] → [RightCancelMonoid N] → RightCancelMonoid (M × N)
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.«term_~_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.adjp_some_none : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ) (i : n)
  (A : Matrix (Option n) (Option n) R),
  Matrix.adjp s A (some i) none = Matrix.detp (-s) (A.submatrix some (Function.update some i none))
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.diff_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (p q : ℤ) (hpq : p + 1 = q), (CochainComplex.HomComplex.Cochain.diff K).v p q hpq = K.d p q
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- For any ideal `I` in a commutative ring `R`, the quotient map `specObj R ⟶ specObj (R ⧸ I)`
is a closed immersion.  -/
AlgebraicGeometry.IsClosedImmersion.spec_of_quotient_mk : ∀ {R : CommRingCat} (I : Ideal ↑R),
  AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
-- Init.Data.Vector.Algebra
Vector.mul_zero : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] [inst_1 : Mul α], (∀ (x : α), x * 0 = 0) → ∀ (xs : Vector α n), xs * 0 = 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_Ioi_sub_Ioi' : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  MeasureTheory.IntegrableOn f (Set.Ioi a) μ →
    MeasureTheory.IntegrableOn f (Set.Ioi b) μ →
      ∫ (x : ℝ) in Set.Ioi a, f x ∂μ - ∫ (x : ℝ) in Set.Ioi b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
-- Mathlib.Tactic.DeprecateTo
/-- Returns the array of names that are in `new` but not in `old`.  -/
Mathlib.Tactic.DeprecateTo.newNames : Lean.Environment → Lean.Environment → Array Lean.Name
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.isSome_maxKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β}, (Std.ExtDTreeMap.Const.modify t k f).maxKey?.isSome = !t.isEmpty
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AccLevelState.mk.inj : ∀ {levels levels_1 : Lean.LevelMap ℤ}, { levels := levels } = { levels := levels_1 } → levels = levels_1
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearEquiv.mfderiv_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E ≃L[𝕜] E') {x : E}, mfderiv% ⇑f x = ↑f
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.instCompleteSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F] [ContinuousSMul 𝕜 E] [ContinuousConstSMul 𝕜 F]
  [CompleteSpace F] [IsTopologicalAddGroup E] [SequentialSpace (ι → E)], CompleteSpace (E [⋀^ι]→L[𝕜] F)
-- Mathlib.Algebra.Order.AddTorsor
/-- An ordered scalar multiplication is a bi-monotone scalar multiplication. Note that this is
different from `IsOrderedModule` whose defining conditions are restricted to nonnegative elements.
 -/
IsOrderedSMul : (G : Type u_3) → (P : Type u_4) → [LE G] → [LE P] → [SMul G P] → Prop
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.mono_left : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t s' : Set X},
  Metric.AreSeparated s' t → s ⊆ s' → Metric.AreSeparated s t
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The Hom types for the categorical commutative squares over X are given by pairs of natural
transformations compatible with the structural isomorphisms.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                (X : Type u₄) →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X →
                      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X → Type (max (max u₄ v₁) v₃)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of Haar measures**:
Two Haar measures on a compact group coincide up to a multiplicative factor.  -/
MeasureTheory.Measure.isMulInvariant_eq_smul_of_compactSpace : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [CompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : μ'.IsMulLeftInvariant] [inst_8 : MeasureTheory.IsFiniteMeasureOnCompacts μ'],
  μ' = μ'.haarScalarFactor μ • μ
-- Mathlib.NumberTheory.ModularForms.NormTrace
SlashInvariantForm.coe_trace : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ]
  {k : ℤ} [inst_1 : SlashInvariantFormClass F 𝒢 k] [inst_2 : 𝒢.IsFiniteRelIndex ℋ],
  ⇑(SlashInvariantForm.trace ℋ f) = ∑ q, SlashInvariantForm.quotientFunc f q
-- Init.Data.List.Attach
List.pmap_eq_attachWith : ∀ {α : Type u_1} {p q : α → Prop} {f : ∀ (a : α), p a → q a} {l : List α} (H : ∀ a ∈ l, p a),
  List.pmap (fun a h => ⟨a, ⋯⟩) l H = l.attachWith q ⋯
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.isometryEquivOnRange_toEquiv : ∀ {α : Type u} {β : Type v} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} (h : Isometry f),
  h.isometryEquivOnRange.toEquiv = Equiv.ofInjective f ⋯
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.vaddInvariantMeasure_iff : ∀ (M : Type u_1) (α : Type u_2) [inst : VAdd M α] {x : MeasurableSpace α} (μ : MeasureTheory.Measure α),
  MeasureTheory.VAddInvariantMeasure M α μ ↔ ∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s
-- Mathlib.Order.SuccPred.Basic
Order.isMax_iterate_succ_of_eq_of_ne : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α} {n m : ℕ},
  Order.succ^[n] a = Order.succ^[m] a → n ≠ m → IsMax (Order.succ^[n] a)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
/-- The projection map to the cokernel in `TopModuleCat R`.  -/
TopModuleCat.cokerπ : {R : Type u} →
  [inst : Ring R] → [inst_1 : TopologicalSpace R] → {M N : TopModuleCat R} → (φ : M ⟶ N) → N ⟶ TopModuleCat.coker φ
-- Lean.Parser.Do
Lean.Parser.Term.doSeqIndent.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- In a category with pullbacks, a morphism `f : X ⟶ Y` induces a functor `Over Y ⥤ Over X`,
by pulling back a morphism along `f`.  -/
CategoryTheory.Over.pullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [CategoryTheory.Limits.HasPullbacksAlong f] →
          CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)
-- Mathlib.Topology.Separation.Basic
ker_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] (x : X), (nhds x).ker = {x}
-- Mathlib.GroupTheory.Commensurable
/-- For `H` a subgroup of `G`, this is the subgroup of all elements `g : conjAut G`
such that `Commensurable (g • H) H`  -/
Subgroup.Commensurable.commensurator' : {G : Type u_1} → [inst : Group G] → Subgroup G → Subgroup (ConjAct G)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- A finite-dimensional manifold modelled on a locally compact field
(such as ℝ, ℂ or the `p`-adic numbers) is locally compact.  -/
Manifold.locallyCompact_of_finiteDimensional : ∀ {E : Type u_8} {𝕜 : Type u_9} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_10} [inst_3 : TopologicalSpace H] {M : Type u_11} [inst_4 : TopologicalSpace M]
  [ChartedSpace H M] (I : ModelWithCorners 𝕜 E H) [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E], LocallyCompactSpace M
-- Init.Data.SInt.Lemmas
Int64.le_of_lt : ∀ {a b : Int64}, a < b → a ≤ b
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
/-- Show the equalizing cone is a limit  -/
CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerConeIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) →
          CategoryTheory.Limits.IsLimit
            (CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerCone F)
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev?_startPos : ∀ {s : String}, s.startPos.prev? = none
-- Mathlib.Order.Hom.WithTopBot
InfHom.withBot'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] [inst_2 : OrderBot β]
  (f : InfHom α β), f.withBot' = { toFun := fun a => Option.elim a ⊥ ⇑f, map_inf' := ⋯ }
-- Lean.Parser.Syntax
/-- Parses a literal symbol. The `&` prefix prevents it from being included in the set of reserved tokens ("keywords").
This means that the symbol can still be recognized as an identifier by other parsers.

Some syntax categories, such as `tactic`, automatically apply `&` to the first symbol.

Whitespace before or after the atom is used as a pretty printing hint.
For example, `" + "` parses `+` and pretty prints it with whitespace on both sides.
The whitespace has no effect on parsing behavior.

(Not exposed by parser description syntax:
If the `includeIdent` argument is true, lets `ident` be reinterpreted as `atom` if it matches.)
 -/
Lean.Parser.Syntax.nonReserved : Lean.Parser.Parser
-- Init.Data.Nat.Basic
/-- Returns the greater of two natural numbers. Usually accessed via `Max.max`.

Returns `m` if `n ≤ m`, or `n` if `m ≤ n`.

Examples:
* `max 0 5 = 5`
* `max 4 5 = 5`
* `max 4 3 = 4`
* `max 8 8 = 8`
 -/
Nat.max : ℕ → ℕ → ℕ
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
/-- Key lemma for Sylvester's law of inertia: the sum of `sigPos Q` and the dimension of any
negative-semidefinite subspace is bounded above by the dimension of the whole space.  -/
QuadraticForm.sigPos_add_finrank_le_of_nonpos : ∀ {M : Type u_2} [inst : AddCommGroup M] {𝕜 : Type u_4} [inst_1 : Field 𝕜] [inst_2 : LinearOrder 𝕜]
  [inst_3 : Module 𝕜 M] {Q : QuadraticForm 𝕜 M} [FiniteDimensional 𝕜 M] {V : Subspace 𝕜 M},
  (∀ x ∈ V, Q x ≤ 0) → sigPos Q + Module.finrank 𝕜 ↥V ≤ Module.finrank 𝕜 M
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_negPart : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : NormedAddCommGroup β] [inst_2 : Lattice β]
  [inst_3 : HasSolidNorm β] [inst_4 : IsOrderedAddMonoid β] (f : BoundedContinuousFunction α β), ⇑f⁻ = (⇑f)⁻
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- Given `S`-schemes `X` and `Y` such that `Y` is locally of finite type and `X` is integral,
`S`-morphisms `Spec K(X) ⟶ Y` correspond bijectively to `S`-rational maps from `X` to `Y`.
 -/
AlgebraicGeometry.Scheme.RationalMap.equivFunctionField : {X Y S : AlgebraicGeometry.Scheme} →
  (sX : X ⟶ S) →
    (sY : Y ⟶ S) →
      [inst : AlgebraicGeometry.IsIntegral X] →
        [AlgebraicGeometry.LocallyOfFiniteType sY] →
          { f //
              CategoryTheory.CategoryStruct.comp f sY =
                CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) sX } ≃
            { f // f.compHom sY = AlgebraicGeometry.Scheme.Hom.toRationalMap sX }
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
/-- The strict AM–GM inequality for two `NNReal`s, with means in canonical form.  -/
NNReal.sqrt_mul_lt_half_add_of_ne : ∀ {x y : NNReal}, x ≠ y → NNReal.sqrt (x * y) < (x + y) / 2
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_nsmul_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s t : Finset α} {n : ℕ}, n • (s ∩ t) ⊆ n • s ∩ n • t
-- Mathlib.Topology.Order.Monotone
IsClosed.csSup_mem : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {s : Set α}, IsClosed s → s.Nonempty → BddAbove s → sSup s ∈ s
-- Mathlib.Algebra.Group.Defs
pow_succ' : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.normedCommGroup.eq_1 : ∀ {E : Type u_2} [inst : NormedCommGroup E],
  OrderDual.normedCommGroup =
    { toNorm := OrderDual.toNorm, toCommGroup := OrderDual.instCommGroup, toMetricSpace := instMetricSpaceOrderDual,
      dist_eq := ⋯ }
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
/-- `(d/dx) lim_{n → ∞} f n x = lim_{n → ∞} f' n x` when the `f' n` converge
_uniformly_ to their limit at `x`.

In words the assumptions mean the following:
  * `hf'`: The `f'` converge "uniformly at" `x` to `g'`. This does not mean that the `f' n` even
    converge away from `x`!
  * `hf`: For all `(y, n)` with `y` sufficiently close to `x` and `n` sufficiently large, `f' n` is
    the derivative of `f n`
  * `hfg`: The `f n` converge pointwise to `g` on a neighborhood of `x`  -/
hasFDerivAt_of_tendstoUniformlyOnFilter : ∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3}
  [inst_1 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] {G : Type u_4}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] {f : ι → E → G} {g : E → G} {f' : ι → E → E →L[𝕜] G}
  {g' : E → E →L[𝕜] G} {x : E} [l.NeBot],
  TendstoUniformlyOnFilter f' g' l (nhds x) →
    (∀ᶠ (n : ι × E) in l ×ˢ nhds x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2) →
      (∀ᶠ (y : E) in nhds x, Filter.Tendsto (fun n => f n y) l (nhds (g y))) → HasFDerivAt g (g' x) x
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryOfSet.comp_id : ∀ {Ω : Type w} (self : CategoryTheory.SmallCategoryOfSet Ω) {X Y : ↑self.obj} (f : ↑(self.hom X Y)),
  self.comp f (self.id Y) = f
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_self' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (y : ↥S), f.mk' (↑y) y = 1
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.add_right : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s t : Set α},
  IsOpen s → IsOpen (s + t)
-- Mathlib.Algebra.Group.Units.Defs
/-- A unit can be interpreted as a term in the base `Monoid`.  -/
Units.instCoeHead : {α : Type u} → [inst : Monoid α] → CoeHead αˣ α