mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series on a ball, then the partial sums
`p.partialSum n z` converges to `f (x + y)` as `n → ∞` and `z → y`.  -/
HasFPowerSeriesOnBall.tendsto_partialSum_prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {y : E},
  HasFPowerSeriesOnBall f p x r →
    y ∈ Metric.eball 0 r → Filter.Tendsto (fun z => p.partialSum z.1 z.2) (Filter.atTop ×ˢ nhds y) (nhds (f (x + y)))
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- A `Subalgebra` is `FiniteDimensional` iff it is `FiniteDimensional` as a submodule.  -/
Subalgebra.finiteDimensional_toSubmodule : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E] {S : Subalgebra F E},
  FiniteDimensional F ↥(Subalgebra.toSubmodule S) ↔ FiniteDimensional F ↥S
-- Mathlib.Dynamics.BirkhoffSum.NormedSpace
dist_birkhoffAverage_birkhoffAverage : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] (𝕜 : Type u_3) [inst_1 : RCLike 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (f : α → α) (g : α → E) (n : ℕ) (x y : α),
  dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) = dist (birkhoffSum f g n x) (birkhoffSum f g n y) / ↑n
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- When the derivative of a function is nonnegative, then it is automatically integrable,
interval version.  -/
intervalIntegral.intervalIntegrable_deriv_of_nonneg : ∀ {g' g : ℝ → ℝ} {a b : ℝ},
  ContinuousOn g (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt g (g' x) x) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), 0 ≤ g' x) → IntervalIntegrable g' MeasureTheory.volume a b
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.haarScalarFactor.congr_simp : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ'_1 : MeasureTheory.Measure G) (e_μ' : μ' = μ'_1)
  (μ μ_1 : MeasureTheory.Measure G) (e_μ : μ = μ_1) [inst_5 : μ.IsHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsMulLeftInvariant],
  μ'.haarScalarFactor μ = μ'_1.haarScalarFactor μ_1
-- Mathlib.CategoryTheory.DifferentialObject
/-- The differential of a differential object.  -/
CategoryTheory.DifferentialObject.d : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            (self : CategoryTheory.DifferentialObject S C) → self.obj ⟶ (CategoryTheory.shiftFunctor C 1).obj self.obj
-- Mathlib.GroupTheory.FreeGroup.Orbit
/-- The neutral element is not contained in one of the startsWith sets.
 -/
FreeGroup.startsWith.ne_one : ∀ {α : Type u_1} [inst : DecidableEq α] {w : α × Bool}, ∀ g ∈ FreeGroup.startsWith w, g ≠ 1
-- Mathlib.Algebra.Opposites
MulOpposite.unop_neg : ∀ {α : Type u_1} [inst : Neg α] (x : αᵐᵒᵖ), MulOpposite.unop (-x) = -MulOpposite.unop x
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousOn.div_const : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : DivInvMonoid G₀] [inst_1 : TopologicalSpace G₀] [SeparatelyContinuousMul G₀]
  {f : α → G₀} {s : Set α} [inst_3 : TopologicalSpace α],
  ContinuousOn f s → ∀ (y : G₀), ContinuousOn (fun x => f x / y) s
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.ofNat_succ : ∀ {n : ℕ} [inst : NeZero n] (a : ℕ), OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- For `f : α → ℝ≥0∞`, define `∫ [f]` to be `∫ f`  -/
MeasureTheory.AEEqFun.lintegral : {α : Type u_1} → [inst : MeasurableSpace α] → {μ : MeasureTheory.Measure α} → (α →ₘ[μ] ENNReal) → ENNReal
-- Mathlib.CategoryTheory.Sites.PreservesLimits
instPreservesColimitsOfShapeSheafTypeUliftYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : J.Subcanonical] {K : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} K]
  [∀ (X : CategoryTheory.Sheaf J (Type (max v v'))), CategoryTheory.Limits.PreservesLimitsOfShape Kᵒᵖ X.obj],
  CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α}, (t.erase k).getKey! k = default
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₀MonoidHom.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → MulOneClass (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)],
  DirectLimit.map₀MonoidHom f = { toFun := fun x => DirectLimit.map₀ f x, map_one' := ⋯, map_mul' := ⋯ }
-- Init.Core
/-- Like `Quot.liftOn q f h` but allows `f a` to "know" that `q = Quot.mk r a`.
 -/
Quot.pliftOn : {β : Sort u_1} →
  {α : Sort u} →
    {r : α → α → Prop} →
      (q : Quot r) →
        (f : (a : α) → q = Quot.mk r a → β) →
          (∀ (a b : α) (h : q = Quot.mk r a) (h' : q = Quot.mk r b), r a b → f a h = f b h') → β
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.Minpoly.coe_toAdjoin : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  ⇑(AdjoinRoot.Minpoly.toAdjoin R x) = ⇑(AdjoinRoot.liftAlgHom (minpoly R x) (Algebra.ofId R ↥R[x]) ⟨x, ⋯⟩ ⋯)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- `AddMonoidAlgebra.map` of an surjective function is surjective.  -/
AddMonoidAlgebra.map_surjective : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S),
  Function.Surjective ⇑f → Function.Surjective (AddMonoidAlgebra.map f)
-- Mathlib.Data.Finset.Union
Finset.biUnion_empty : ∀ {α : Type u_1} {β : Type u_2} {t : α → Finset β} [inst : DecidableEq β], ∅.biUnion t = ∅
-- Mathlib.Topology.NhdsWithin
principal_inter_le_nhdsSetWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α}, Filter.principal (s ∩ t) ≤ nhdsSetWithin s t
-- Mathlib.CategoryTheory.InducedCategory
/-- The type of morphisms in `InducedCategory D F` between `X` and `Y`
is a 1-field structure which identifies to `F X ⟶ F Y`.  -/
CategoryTheory.InducedCategory.Hom : {C : Type u₁} →
  {D : Type u₂} →
    [CategoryTheory.Category.{v, u₂} D] →
      {F : C → D} → CategoryTheory.InducedCategory D F → CategoryTheory.InducedCategory D F → Type v
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.zsmul : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S) (z : ℤ) (x : WittVector p R), WittVector.mapFun (⇑f) (z • x) = z • WittVector.mapFun (⇑f) x
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_inv_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  (U : X.Opens) (r : ↑(Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U))))
  (x : ↑(M.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv) (r • x) =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).hom) r •
      (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv) x
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `+` is an additive commutative semigroup,if it admits
an injective map that preserves `+` to an additive commutative semigroup.  -/
Function.Injective.addCommSemigroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : AddCommSemigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x + y) = f x + f y) → AddCommSemigroup M₁
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.soIndefiniteEquiv_apply : ∀ (p : Type u_2) (q : Type u_3) (R : Type u₂) [inst : DecidableEq p] [inst_1 : DecidableEq q] [inst_2 : CommRing R]
  [inst_3 : Fintype p] [inst_4 : Fintype q] {i : R} (hi : i * i = -1) (A : ↥(LieAlgebra.Orthogonal.so' p q R)),
  ↑((LieAlgebra.Orthogonal.soIndefiniteEquiv p q R hi) A) =
    (LieAlgebra.Orthogonal.Pso p q R i)⁻¹ * ↑A * LieAlgebra.Orthogonal.Pso p q R i
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.const.sizeOf_spec : ∀ {w : ℕ} (val : BitVec w), sizeOf (Std.Tactic.BVDecide.BVExpr.const val) = 1 + sizeOf w + sizeOf val
-- Mathlib.Algebra.Algebra.Hom
AlgHom.linearMapMk_toAddHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), { toAddHom := ↑f, map_smul' := ⋯ } = f.toLinearMap
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.exists_gt : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (f : CauSeq α abs),
  ∃ a, f < CauSeq.const abs a
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredPrelimit_iff_pred_eq : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : PredOrder α],
  ¬Order.IsPredPrelimit a ↔ ∃ b, ¬IsMin b ∧ Order.pred b = a
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.isRoot_gcd_iff_isRoot_left_right : ∀ {R : Type u} [inst : Field R] [inst_1 : DecidableEq R] {f g : Polynomial R} {α : R},
  (EuclideanDomain.gcd f g).IsRoot α ↔ f.IsRoot α ∧ g.IsRoot α
-- Lean.Meta.Sorry
/-- Records the origin module name, logical source position, and LSP range for the `sorry`.
The logical source position is used when displaying the sorry when the `pp.sorrySource` option is true,
and the LSP range is used for "go to definition" in the Infoview.
 -/
Lean.Meta.SorryLabelView.module? : Lean.Meta.SorryLabelView → Option Lean.DeclarationLocation
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Given a map `f : R →+ S`, return the corresponding map `R[M] → S[M]` obtained by mapping
each coefficient along `f`.  -/
AddMonoidAlgebra.map : {R : Type u_3} →
  {S : Type u_4} →
    {M : Type u_6} →
      [inst : Semiring R] → [inst_1 : Semiring S] → (R →+ S) → AddMonoidAlgebra R M → AddMonoidAlgebra S M
-- Mathlib.MeasureTheory.Group.Arithmetic
AddOpposite.instMeasurableMul₂ : ∀ {M : Type u_2} [inst : Add M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M], MeasurableAdd₂ Mᵃᵒᵖ
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
sup_sub_inf_eq_abs_sub : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b : α), a ⊔ b - a ⊓ b = |b - a|
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.val_inf : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : ↥L), ↑(a ⊓ b) = ↑a ⊓ ↑b
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesLeftKanExtension F L] [inst_5 : L.HasLeftKanExtension F],
  G.leftKanExtensionCompIsoOfPreserves F L =
    ((L.leftKanExtension F).comp G).leftKanExtensionUnique
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.leftKanExtensionUnit F) G)
        (L.associator (L.leftKanExtension F) G).hom)
      (L.leftKanExtension (F.comp G)) (L.leftKanExtensionUnit (F.comp G))
-- Mathlib.Data.Bool.Basic
Bool.lt_iff : ∀ {x y : Bool}, x < y ↔ x = false ∧ y = true
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.instHashableCall.hash : Lean.Meta.FunInd.Call → UInt64
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∪ m₂).getKey? k = m₂.getKey? k
-- Init.Data.Range.Polymorphic.SInt
Int64.instRxcHasSize : Std.Rxc.HasSize Int64
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.IsAlternating.sup_edge : ∀ {V : Type u_1} {G G' : SimpleGraph V} {u x : V},
  G.IsAlternating G' →
    ¬G'.Adj u x →
      (∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u') →
        (∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u) → (G ⊔ SimpleGraph.edge u x).IsAlternating G'
-- Init.Data.SInt.Lemmas
Int32.mul_zero : ∀ {a : Int32}, a * 0 = 0
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.ofFactorizationData_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
      (CategoryTheory.Limits.diag A)),
  (HomotopicalAlgebra.PathObject.ofFactorizationData h).p₁ =
    CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.snd
-- Mathlib.Topology.Defs.Filter
NoncompactSpace.mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], ¬IsCompact Set.univ → NoncompactSpace X
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.toMvPowerSeries_symm_apply_coeff : ∀ {R : Type u_2} [inst : Semiring R] {σ : Type u_3} [inst_1 : Finite σ] (f : MvPowerSeries σ R),
  (HahnSeries.toMvPowerSeries.symm f).coeff = f
-- Mathlib.AlgebraicGeometry.Morphisms.Descent
/-- Let `P` be the morphism property associated to the ring hom property `Q`. Suppose

- `P'` implies `Q'` on global sections for affine schemes,
- `P'` is satisfied for all surjective, local isomorphisms, and
- `Q` codescend along `Q'`.

Then `P` descends along quasi-compact morphisms satisfying `P'`.

Note: The second condition is in particular satisfied for faithfully flat morphisms.
 -/
AlgebraicGeometry.HasRingHomProperty.descendsAlong : ∀ (P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  (Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) [P'.IsStableUnderBaseChange]
  [P'.IsStableUnderComposition] [P.IsStableUnderBaseChange],
  @AlgebraicGeometry.IsLocalIso ⊓ @AlgebraicGeometry.Surjective ≤ P' →
    (∀ {R S : CommRingCat} {f : R ⟶ S}, P' (AlgebraicGeometry.Spec.map f) → Q' (CommRingCat.Hom.hom f)) →
      ∀ [AlgebraicGeometry.HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] => Q],
        (RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] => Q') →
          P.DescendsAlong (P' ⊓ @AlgebraicGeometry.QuasiCompact)
-- Mathlib.Data.Set.NAry
Set.image2_right_comm : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {s : Set α} {t : Set β}
  {u : Set γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε},
  (∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b) →
    Set.image2 f (Set.image2 g s t) u = Set.image2 g' (Set.image2 f' s u) t
-- Mathlib.Analysis.Matrix.Spectrum
Fintype.equivOfCardEq.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (h : Fintype.card α = Fintype.card β),
  Fintype.equivOfCardEq h = Fintype.equivOfCardEq h
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.coe_id : ∀ {X : TopCat} {x : ↑X} {U : TopologicalSpace.OpenNhds x} (f : U ⟶ U), ⇑f = id
-- Mathlib.Data.Finite.Sigma
Finite.instSigma : ∀ {α : Type u_1} {β : α → Type u_2} [Finite α] [∀ (a : α), Finite (β a)], Finite ((a : α) × β a)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_sup : ∀ {α : Type u_1} [inst : LE α] (s t : UpperSet α), (s ⊔ t).compl = s.compl ⊔ t.compl
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.mem_support_iff : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, n ∈ p.support ↔ p.coeff n ≠ 0
-- Mathlib.Data.Set.Basic
Set.eq_empty_of_subset_empty : ∀ {α : Type u} {s : Set α}, s ⊆ ∅ → s = ∅
-- Mathlib.LinearAlgebra.Prod
LinearMap.inr_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (x : M₂), (LinearMap.inr R M M₂) x = (0, x)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_zero : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α], |0| = 0
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.neg_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Neg Y] (f : LocallyConstant X Y) (x : X),
  (-f) x = -f x
-- Std.Http.Protocol.H1
/-- Validates the required `Host` header for HTTP/1.1 requests:
exactly one value that is either empty or parseable as a valid host.

As defined in RFC 9112 Section 3.2:

"A client MUST send a Host header field (Section 7.2 of [HTTP]) in all HTTP/1.1 request messages.
If the target URI includes an authority component, then a client MUST send a field value for Host that
is identical to that authority component, excluding any userinfo subcomponent and its "@"
delimiter (Section 4.2 of [HTTP]). If the authority component is missing or undefined for the target
URI, then a client MUST send a Host header field with an empty field value."

Reference: https://www.rfc-editor.org/rfc/rfc9112.html#name-request-target
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.hasSingleAcceptedHostHeader : Std.Http.Protocol.H1.Message.Head Std.Http.Protocol.H1.Direction.receiving → Bool
-- Mathlib.Order.Interval.Finset.Defs
Finset.Iic_product_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : LocallyFiniteOrderBot β] [inst_4 : DecidableLE (α × β)] (a : α) (b : β),
  Finset.Iic a ×ˢ Finset.Iic b = Finset.Iic (a, b)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
/-- If a valuation `v` is trivial on constants and `1 < v RatFunc.X` then for every polynomial `p`,
`v p = v RatFunc.X ^ p.natDegree`.

Note: The condition `1 < v RatFunc.X` is typically satisfied by the valuation at infinity.  -/
Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X : ∀ (K : Type u_1) [inst : Field K] {Γ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [hv : Valuation.IsTrivialOn K v],
  1 < v RatFunc.X → ∀ {p : Polynomial K}, p ≠ 0 → v ↑p = v RatFunc.X ^ p.natDegree
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Inhabited α]
  [inst_1 : Std.TransCmp cmp] {k : α}, k ∈ t₂ → (t₁ ∩ t₂).getKey! k = t₁.getKey! k
-- Mathlib.GroupTheory.Congruence.Defs
/-- Definition of `≤` for additive congruence relations.  -/
AddCon.le_def : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, c ≤ d ↔ ∀ {x y : M}, c x y → d x y
-- Mathlib.Topology.Algebra.Group.Pointwise
closure_subset_mul_right_of_mem_nhds_one_of_inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] (s : Set G) {s' : Set G},
  s' ∈ nhds 1 → (∀ x ∈ s', x⁻¹ ∈ s') → closure s ⊆ s * s'
-- Mathlib.SetTheory.ZFC.PSet
PSet.toSet.eq_1 : ∀ (u : PSet.{u}), u.toSet = {x | x ∈ u}
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.inter.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t₁ t₁_1 : Std.ExtTreeMap α β cmp),
  t₁ = t₁_1 → ∀ (t₂ t₂_1 : Std.ExtTreeMap α β cmp), t₂ = t₂_1 → t₁.inter t₂ = t₁_1.inter t₂_1
-- Mathlib.Topology.FiberBundle.Basic
/-- Make a `FiberBundle` from a `FiberPrebundle`.  Concretely this means
that, given a `FiberPrebundle` structure for a sigma-type `E` -- which consists of a
number of "pretrivializations" identifying parts of `E` with product spaces `U × F` -- one
establishes that for the topology constructed on the sigma-type using
`FiberPrebundle.totalSpaceTopology`, these "pretrivializations" are actually
"trivializations" (i.e., homeomorphisms with respect to the constructed topology).  -/
FiberPrebundle.toFiberBundle : {B : Type u_2} →
  {F : Type u_3} →
    {E : B → Type u_5} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : (x : B) → TopologicalSpace (E x)] → (a : FiberPrebundle F E) → FiberBundle F E
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instCommRingQuotient : {R : Type u_1} → [inst : CommRing R] → (c : RingCon R) → CommRing c.Quotient
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.localGeneratorsData_I : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.QuasicoherentData), q.localGeneratorsData.I = q.I
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- **Alias** of the forward direction of `Convexity.StdSimplex.weights_inj`. -/
Convexity.StdSimplex.ext : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} {f g : Convexity.StdSimplex R M},
  f.weights = g.weights → f = g
-- Mathlib.Algebra.Order.Group.Abs
le_mabs' : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G}, a ≤ |b|ₘ ↔ b ≤ a⁻¹ ∨ a ≤ b
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.cases.injEq : ∀ (declName : Lean.Name) (eager : Bool) (declName_1 : Lean.Name) (eager_1 : Bool),
  (Lean.Meta.Grind.Entry.cases declName eager = Lean.Meta.Grind.Entry.cases declName_1 eager_1) =
    (declName = declName_1 ∧ eager = eager_1)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.toSL2R_smul_I : ∀ (z : UpperHalfPlane), z.toSL2R • UpperHalfPlane.I = z
-- Mathlib.Order.Hom.BoundedLattice
/-- Copy of an `InfTopHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
InfTopHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Min α] →
      [inst_1 : Top α] →
        [inst_2 : Min β] → [inst_3 : Top β] → (f : InfTopHom α β) → (f' : α → β) → f' = ⇑f → InfTopHom α β
-- Mathlib.Data.Finset.Max
Finset.max'_lt_iff : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α}, s.max' H < x ↔ ∀ y ∈ s, y < x
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc : ∀ (R : CommRingCat) [inst : IsLocalRing ↑R] {Z : CommRingCat} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ (IsLocalRing.closedPoint ↑R) trivial)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.stalkClosedPointIso R).hom h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).hom h