mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getValueCast! : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [LawfulBEq α] → (a : α) → [Inhabited (β a)] → List ((a : α) × β a) → β a
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} {inst : NontriviallyNormedField 𝕜} {EB : Type u_7}
  {inst_1 : NormedAddCommGroup EB} {inst_2 : NormedSpace 𝕜 EB} {HB : Type u_8} {inst_3 : TopologicalSpace HB}
  {IB : ModelWithCorners 𝕜 EB HB} {inst_4 : TopologicalSpace B} {inst_5 : ChartedSpace HB B}
  {inst_6 : (x : B) → AddCommMonoid (E x)} {inst_7 : (x : B) → Module 𝕜 (E x)} {inst_8 : NormedAddCommGroup F}
  {inst_9 : NormedSpace 𝕜 F} {inst_10 : (x : B) → TopologicalSpace (E x)} {a : VectorPrebundle 𝕜 F E} {n : WithTop ℕ∞}
  [self : VectorPrebundle.IsContMDiff IB a n],
  ∀ e ∈ a.pretrivializationAtlas,
    ∀ e' ∈ a.pretrivializationAtlas,
      ∃ f,
        ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n f (e.baseSet ∩ e'.baseSet) ∧
          ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' ⟨b, e.symm b v⟩).2
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.polar_toQuadraticMap : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {B : LinearMap.BilinMap R M N} (x y : M),
  QuadraticMap.polar (⇑B.toQuadraticMap) x y = (B x) y + (B y) x
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vadd_finset_subset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {s t : Finset β}
  {a : α}, a +ᵥ s ⊆ t ↔ s ⊆ -a +ᵥ t
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- A variant of `Projectivization.mk` in terms of a subtype. `mk` is preferred.  -/
Projectivization.mk' : (K : Type u_1) →
  {V : Type u_2} →
    [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → { v // v ≠ 0 } → Projectivization K V
-- Lean.Meta.Transform
Lean.TransformStep.visit.injEq : ∀ (e e_1 : Lean.Expr), (Lean.TransformStep.visit e = Lean.TransformStep.visit e_1) = (e = e_1)
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- The standard basis for an additive monoid algebra.  -/
AddMonoidAlgebra.basis : (R : Type u_7) → (k : Type u_8) → [inst : Semiring k] → Module.Basis R k (AddMonoidAlgebra k R)
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- Given an additive Freiman isomorphism `f` from `A` to `B`, if `g` maps `B` into `A`, and is a
right inverse to `f` on `B`, then `g` is an additive Freiman isomorphism from `B` to `A`.
 -/
IsAddFreimanIso.symm : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β}
  {n : ℕ} {g : β → α}, Set.MapsTo g B A → Set.RightInvOn g f B → IsAddFreimanIso n A B f → IsAddFreimanIso n B A g
-- Mathlib.Geometry.Euclidean.Simplex
/-- In a triangle, the distance from a vertex to the `centroid` equals twice the distance from the
`centroid` to the `faceOppositeCentroid`.  -/
Affine.Triangle.dist_point_centroid : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) (i : Fin 3),
  dist (t.points i) (Affine.Simplex.centroid t) =
    2 * dist (Affine.Simplex.centroid t) (Affine.Simplex.faceOppositeCentroid t i)
-- Mathlib.Data.Fin.Basic
Fin.cast_eq_self : ∀ {n : ℕ} (a : Fin n), Fin.cast ⋯ a = a
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.cancel_iso_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Y ≅ Z) (f f' : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp g.inv f = CategoryTheory.CategoryStruct.comp g.inv f' ↔ f = f'
-- Mathlib.Data.Bool.Set
Bool.range_eq : ∀ {α : Type u_1} (f : Bool → α), Set.range f = {f false, f true}
-- Mathlib.SetTheory.Cardinal.Defs
/-- `ℵ₀` is the smallest infinite cardinal. 

Conventions for notations in identifiers:

 * The recommended spelling of `ℵ₀` in identifiers is `aleph0`. -/
Cardinal.termℵ₀ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.biproduct_ι_comp_rightDistributor_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (f : J → C) (X : C) (j : J),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j)
      (CategoryTheory.rightDistributor f X).inv =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G),
  CategoryTheory.Presheaf.IsLocallySurjective J f ↔
    CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.Functor.whiskerRight f (CategoryTheory.forget A))
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.trans_smul : ∀ {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} {G : Type u_18} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : Module S V]
  [inst_5 : AddCommMonoid W] [inst_6 : Module R W] [inst_7 : Module S W] [inst_8 : AddCommMonoid G]
  [inst_9 : Module R G] [inst_10 : Module S G] [inst_11 : SMulCommClass R S W] [inst_12 : SMul S R]
  [inst_13 : IsScalarTower S R V] [inst_14 : IsScalarTower S R W] [inst_15 : IsScalarTower S R G] (α : Sˣ)
  (e : G ≃ₗ[R] V) (f : V ≃ₗ[R] W), e ≪≫ₗ (α • f) = α • e ≪≫ₗ f
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanLocationLink : Lean.ToJson Lean.Lsp.LeanLocationLink
-- Mathlib.Order.Interval.Finset.Fin
Fin.Iio_add_one_eq_Iic : ∀ {n : ℕ} {b : Fin n}, ↑b + 1 < n → Finset.Iio (b + 1) = Finset.Iic b
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₁₂_comp_d₂₃ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.d₁₂ A) (groupCohomology.d₂₃ A) = 0
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.instZPow : {M : Type uM} → {N : Type uN} → [inst : MulOneClass M] → [inst_1 : CommGroup N] → Pow (M →* N) ℤ
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_monotone : ∀ {K : Type u_1} [inst : RCLike K], Monotone ⇑RCLike.re
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.mono_lie_left : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  {I J : LieIdeal R L}, I ≤ J → ⁅I, N⁆ ≤ ⁅J, N⁆
-- Mathlib.Order.Hom.Basic
StrictMono.orderIsoOfRightInverse_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Preorder β] (f : α → β) (h_mono : StrictMono f)
  (g : β → α) (hg : Function.RightInverse g f), ⇑(RelIso.symm (StrictMono.orderIsoOfRightInverse f h_mono g hg)) = g
-- Mathlib.Algebra.Order.Sub.Basic
AddLECancellable.tsub_lt_tsub_iff_right : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b c : α}, AddLECancellable c → c ≤ a → (a - c < b - c ↔ a < b)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_le_card_div_right : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] {s t : Finset α}, t.Nonempty → s.card ≤ (s / t).card
-- Mathlib.MeasureTheory.Measure.AEMeasurable
MeasureTheory.Measure.map_sum : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {ι : Type u_7}
  {m : ι → MeasureTheory.Measure α} {f : α → β},
  AEMeasurable f (MeasureTheory.Measure.sum m) →
    MeasureTheory.Measure.map f (MeasureTheory.Measure.sum m) =
      MeasureTheory.Measure.sum fun i => MeasureTheory.Measure.map f (m i)
-- Mathlib.Analysis.Normed.Module.FiniteDimension
LinearIndependent.eventually : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] {f : ι → E},
  LinearIndependent 𝕜 f → ∀ᶠ (g : ι → E) in nhds f, LinearIndependent 𝕜 g
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instZero.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α], LowerSet.instZero = { zero := LowerSet.Iic 0 }
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.comp_iff_of_bijective_left : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  {f : R →+* S} {g : S →+* T}, Function.Bijective ⇑g → ((g.comp f).Flat ↔ f.Flat)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_eq : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.mixedEmbedding.fundamentalCone.completeBasis K) NumberField.Units.dirichletUnitTheorem.w₀ = fun w =>
    ↑w.mult
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarCoord_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (p : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)),
  ↑(NumberField.mixedEmbedding.polarCoord K) p = (p.1, Pi.map (fun i => ↑Complex.polarCoord) p.2)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.GenerateMeasurable.brecOn : ∀ {α : Type u_1} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.GenerateMeasurable s a → Prop} {a : Set α}
  (t : MeasurableSpace.GenerateMeasurable s a),
  (∀ (a : Set α) (t : MeasurableSpace.GenerateMeasurable s a),
      MeasurableSpace.GenerateMeasurable.below t → motive a t) →
    motive a t
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.vandermonde_succ : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v : Fin n.succ → R),
  Matrix.vandermonde v =
    Matrix.of Fin.cons (fun j => v 0 ^ ↑j) fun i => Fin.cons 1 fun j => v i.succ * Matrix.vandermonde (Fin.tail v) i j
-- Mathlib.Topology.Algebra.Module.Complement
/-- **Alias** of the reverse direction of `Submodule.projectionOntoL_apply_eq_zero_iff`. -/
Submodule.projectionOntoL_apply_eq_zero_of_mem_right : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q) {x : M},
  x ∈ q → (p.projectionOntoL q h) x = 0
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_map_term : ∀ {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') (i : ι),
  (CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv ι' e).functor.map
      (CategoryTheory.Limits.WidePullbackShape.Hom.term i) =
    CategoryTheory.Limits.WidePullbackShape.Hom.term (e i)
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_max : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ), ↑(max p q) = max ↑p ↑q
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.Measure.conv_smul_right : ∀ {M : Type u_2} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] (μ ν : MeasureTheory.Measure M)
  [MeasureTheory.SFinite ν] (s : ENNReal), μ.conv (s • ν) = s • μ.conv ν
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (idx : ℕ) (hidx : idx ≤ len)
  (s : aig.RefVec idx) (lhs rhs : aig.RefVec len)
  (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α f],
  aig.decls.size ≤ (Std.Sat.AIG.RefVec.zip.go aig idx s hidx lhs rhs f).aig.decls.size
-- Std.Time.Format.Modifier
/-- `G`: Era (e.g., AD, Anno Domini, A).
 -/
Std.Time.Modifier.G : Std.Time.Text → Std.Time.Modifier
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.ofPermHomFun_commute_zpow_apply : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)) (x : α) (j : ℤ),
  a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).minKey! =
        t.minKey?.elim k fun k' => if (compare k k').isLE = true then k else k'
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.res_const : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : M) (g : R)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : U ≤ PrimeSpectrum.basicOpen g)
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hv : V ≤ PrimeSpectrum.basicOpen g)
  (i : Opposite.op U ⟶ Opposite.op V),
  (CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.structureSheafInType R M).obj.map i))
      (AlgebraicGeometry.StructureSheaf.const f g U hu) =
    AlgebraicGeometry.StructureSheaf.const f g V hv
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_lt_type : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] (a : α), (Ordinal.typein r).toRelEmbedding a < Ordinal.type r
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.neg_one_le_mulExpNegMulSq_one : ∀ (x : ℝ), -1 ≤ Real.mulExpNegMulSq 1 x
-- Mathlib.Order.Filter.EventuallyConst
/-- **Alias** of the forward direction of `Filter.eventuallyConst_iff_exists_eventuallyEq`. -/
Filter.EventuallyConst.eventuallyEq_const : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Nonempty β],
  Filter.EventuallyConst f l → ∃ c, f =ᶠ[l] fun x => c
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.instEnoughProjectivesOppositeOfEnoughInjectives : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.EnoughInjectives C],
  CategoryTheory.EnoughProjectives Cᵒᵖ
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- **Binet's formula** for integer values.  -/
Real.coe_intFib_eq : ∀ (n : ℤ), ↑(Int.fib n) = (Real.goldenRatio ^ n - Real.goldenConj ^ n) / √5
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.instCommGroupSubtypeMemSubmonoid : {M : Type u_1} → [inst : CommMonoid M] → CommGroup ↥(IsUnit.submonoid M)
-- Init.PropLemmas
dite_then_false : ∀ {p : Prop} [inst : Decidable p] {x : ¬p → Prop}, (if h : p then False else x h) ↔ ∃ (h : ¬p), x h
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_eq_iff_eq_untrop : ∀ {R : Type u} {x : R} {y : Tropical R}, Tropical.trop x = y ↔ x = Tropical.untrop y
-- Init.Data.List.Lemmas
List.getLast_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} (h : List.map f l ≠ []),
  (List.map f l).getLast h = f (l.getLast ⋯)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyMapIso'_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  (CategoryTheory.ShortComplex.leftHomologyMapIso' e h₁ h₂).hom =
    CategoryTheory.ShortComplex.leftHomologyMap' e.hom h₁ h₂
-- Mathlib.LinearAlgebra.CrossProduct
/-- The triple product of `u`, `v`, and `w` is equal to the determinant of the matrix
with those vectors as its rows.  -/
triple_product_eq_det : ∀ {R : Type u_1} [inst : CommRing R] (u v w : Fin 3 → R), u ⬝ᵥ (crossProduct v) w = Matrix.det ![u, v, w]
-- Mathlib.Order.OrderDual
OrderDual.toDual_comp_ofDual : ∀ {α : Type u_1}, ⇑OrderDual.toDual ∘ ⇑OrderDual.ofDual = id
-- Mathlib.SetTheory.Ordinal.Notation
instDecidableEqONote : DecidableEq ONote
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.invRev_injective : ∀ {α : Type u}, Function.Injective FreeGroup.invRev
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.context.sizeOf_spec : ∀ (i : Lean.Elab.PartialContextInfo) (t : Lean.Elab.InfoTree),
  sizeOf (Lean.Elab.InfoTree.context i t) = 1 + sizeOf i + sizeOf t
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.isFractionRing : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], IsFractionRing ℤ_[p] ℚ_[p]
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instUniqueOfSubsingleton : {M : Type u_1} → [inst : Monoid M] → [Subsingleton M] → Unique (Associates M)
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.getD_rightInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ),
  (cs.rightInvSeq ω).getD j 1 =
    (cs.wordProd (List.drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (List.drop (j + 1) ω)
-- Mathlib.RepresentationTheory.Homological.Resolution
classifyingSpaceUniversalCover.compForgetAugmented.eq_1 : ∀ (G : Type u) [inst : Monoid G],
  classifyingSpaceUniversalCover.compForgetAugmented G =
    CategoryTheory.SimplicialObject.augment
      (CategoryTheory.Functor.comp (classifyingSpaceUniversalCover G) (CategoryTheory.forget (Action (Type u) G)))
      (⊤_ Type u)
      (CategoryTheory.Limits.terminal.from
        ((CategoryTheory.Functor.comp (classifyingSpaceUniversalCover G)
              (CategoryTheory.forget (Action (Type u) G))).obj
          (Opposite.op { len := 0 })))
      ⋯
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittNeg_zero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.wittNeg p 0 = -MvPolynomial.X (0, 0)
-- Mathlib.Algebra.Order.Module.Defs
/-- **Alias** of `le_of_smul_le_smul_left`. -/
le_of_smul_le_smul_of_pos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [PosSMulReflectLE α β], a • b₁ ≤ a • b₂ → 0 < a → b₁ ≤ b₂
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsLocallyFiniteMeasure μ], MeasureTheory.IsFiniteMeasureOnCompacts μ
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.mk.inj : ∀ {R : Type u_1} {inst : CommRing R} {asIdeal : Ideal R} {isPrime : asIdeal.IsPrime} {ne_bot : asIdeal ≠ ⊥}
  {asIdeal_1 : Ideal R} {isPrime_1 : asIdeal_1.IsPrime} {ne_bot_1 : asIdeal_1 ≠ ⊥},
  { asIdeal := asIdeal, isPrime := isPrime, ne_bot := ne_bot } =
      { asIdeal := asIdeal_1, isPrime := isPrime_1, ne_bot := ne_bot_1 } →
    asIdeal = asIdeal_1
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.toSearcher_eq : ∀ {c : Char} {s : String.Slice},
  String.Slice.Pattern.ToForwardSearcher.toSearcher c s =
    String.Slice.Pattern.ToForwardSearcher.toSearcher (fun x => x == c) s
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The sum of two `C^n` functions is `C^n`.  -/
ContDiff.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {f g : E → F}, ContDiff 𝕜 n f → ContDiff 𝕜 n g → ContDiff 𝕜 n fun x => f x + g x
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.eLpNorm_exponent_top : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] {μ : MeasureTheory.Measure α} {f : α → ε},
  MeasureTheory.eLpNorm f ⊤ μ = MeasureTheory.eLpNormEssSup f μ
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.surjective : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), Function.Surjective ⇑e
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_inv_lt_iff : ∀ {x y : ENNReal} {z : ℝ}, 0 < z → (x ^ z⁻¹ < y ↔ x < y ^ z)
-- Mathlib.Analysis.InnerProductSpace.Reproducing
_private.Mathlib.Analysis.InnerProductSpace.Reproducing.0.RKHS.inner_H₀_def : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : CompleteSpace V] {K : Matrix X X (V →L[𝕜] V)} [inst_4 : Fact K.PosSemidef]
  (f g : RKHS.H₀ K),
  inner 𝕜 f g =
    Finsupp.sum f fun x z =>
      match x with
      | (y, u) =>
        Finsupp.sum g fun x w =>
          match x with
          | (x, v) => star z * w * inner 𝕜 ((K x y) u) v
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperPresheaf_obj : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{w, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C] (A : C)
  (U : (TopologicalSpace.Opens ↑X)ᵒᵖ), (skyscraperPresheaf p₀ A).obj U = if p₀ ∈ Opposite.unop U then A else ⊤_ C
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_psigma_congrRight : ∀ {ι : Type u} {f g : ι → Type v},
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g i)) → Cardinal.mk ((i : ι) ×' f i) = Cardinal.mk ((i : ι) ×' g i)
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
/-- A function is `C^(n + 1)` if and only if it is differentiable,
and its derivative (formulated in terms of `deriv`) is `C^n`.  -/
contDiff_succ_iff_deriv : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F},
  ContDiff 𝕜 (n + 1) f ↔ Differentiable 𝕜 f ∧ (n = ⊤ → AnalyticOn 𝕜 f Set.univ) ∧ ContDiff 𝕜 n (deriv f)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.intCast_apply : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : PseudoMetricSpace β] [inst_2 : IntCast β] (m : ℤ)
  (x : α), ↑m x = ↑m
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_mono_fun : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f g : β → α},
  (∀ b ∈ s, g b ≤ f b) → s.inf g ≤ s.inf f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ \ t₂).getKey? k = none
-- Mathlib.Order.Grade
IsMax.grade : ∀ (𝕆 : Type u_1) {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : Preorder α] [inst_2 : GradeMaxOrder 𝕆 α] {a : α},
  IsMax a → IsMax (grade 𝕆 a)
-- Mathlib.Combinatorics.Additive.CauchyDavenport
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.wellFoundedOn_devosMulRel : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α], {x | x.1.Nonempty ∧ x.2.Nonempty}.WellFoundedOn DevosMulRel✝
-- Init.ShareCommon
ShareCommon.mkStateImpl : (σ : ShareCommon.StateFactory) → ShareCommon.State σ
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- Linear equivalence between `S : Submodule R A` and `S`. Though these types are equal,
we define it as a `LinearEquiv` to avoid type equalities.  -/
NonUnitalSubalgebra.toSubmoduleEquiv : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → (S : NonUnitalSubalgebra R A) → ↥S.toSubmodule ≃ₗ[R] ↥S
-- Mathlib.Data.Option.NAry
Option.map_map₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} (f : α → β → γ) (g : γ → δ),
  Option.map g (Option.map₂ f a b) = Option.map₂ (fun a b => g (f a b)) a b