mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightParams.mk.inj : ∀ {toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams},
  { toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
setIntegral_withDensity_eq_setIntegral_smul : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {f : X → NNReal},
  Measurable f →
    ∀ (g : X → E) {s : Set X},
      MeasurableSet s → (∫ (x : X) in s, g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousAt.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {x : α} {f : β → Prop}, SemicontinuousAt (fun _x => f) x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
fderivWithin_sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x →
    UniqueDiffWithinAt ℝ s x → fderivWithin ℝ (fun x => Real.sinh (f x)) s x = Real.cosh (f x) • fderivWithin ℝ f s x
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mergeAll? : Array (Lean.TSyntax `tactic) → Lean.Elab.Tactic.Try.TryTacticM (Option (Lean.TSyntax `tactic))
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If ∠ABC = π then dist A B ≠ 0.  -/
EuclideanGeometry.left_dist_ne_zero_of_angle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi → dist p₁ p₂ ≠ 0
-- Init.Data.List.MinMaxOn
List.minOn_append : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []),
  List.minOn f (xs ++ ys) ⋯ = minOn f (List.minOn f xs hxs) (List.minOn f ys hys)
-- Lean.Data.Lsp.Internal
Lean.Lsp.OpenNamespace.renamed.injEq : ∀ («from» «to» from_1 to_1 : Lean.Name),
  (Lean.Lsp.OpenNamespace.renamed «from» «to» = Lean.Lsp.OpenNamespace.renamed from_1 to_1) =
    («from» = from_1 ∧ «to» = to_1)
-- Mathlib.Data.Fintype.Pi
/-- There are finitely many embeddings between finite types.

This instance used to be computable (using `DecidableEq` arguments), but
it makes things a lot harder to work with here.
 -/
Function.Embedding.fintype : {α : Type u_3} → {β : Type u_4} → [Fintype α] → [Fintype β] → Fintype (α ↪ β)
-- Mathlib.Tactic.Translate.Core
/-- Returns a `NameSet` of auxiliary constants in `decl` that might have been generated
when adding `pre` to the environment, and which hence might need to be translated.
Examples include `pre.match_5`, `pre._proof_2`, `someOtherDeclaration._proof_2` and `wrapped✝`.
The reason why we have to include `_proof_i` lemmas from other declarations is that there is a
cache of such proofs, and previous such auxiliary proofs are reused when possible.
These auxiliary declarations may be private or not, independent of whether `pre` is private.
`wrapped✝` is generated by `irreducible_def`, and it has macro scopes.
 -/
Mathlib.Tactic.Translate.findAuxDecls : Lean.ConstantInfo → Lean.Name → Lean.CoreM (Array Lean.Name)
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.def : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x y : M}, x ≡ y [SMOD U] ↔ Submodule.Quotient.mk x = Submodule.Quotient.mk y
-- Mathlib.Data.Finset.Pi
Finset.piDiag.eq_1 : ∀ {α : Type u_1} (s : Finset α) (ι : Type u_3) [inst : DecidableEq (ι → α)],
  s.piDiag ι = Finset.image (Function.const ι) s
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.limitGroup : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J GrpCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections] →
        Group (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget GrpCat))).pt
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.instOrdDatabase : Ord Mathlib.CrossRef.Database
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_ne_top_iff : ∀ {a b : ENNReal}, a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsUpper.isTopologicalBasis : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α],
  TopologicalSpace.IsTopologicalBasis (Topology.IsUpper.upperBasis α)
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgEquiv.toBialgIso_refl : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : Ring X] [inst_2 : Bialgebra R X],
  (BialgEquiv.refl R X).toBialgIso = CategoryTheory.Iso.refl (BialgCat.of R X)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtPlace_apply : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K) (x : K),
  (NumberField.mixedEmbedding.normAtPlace w) ((NumberField.mixedEmbedding K) x) = w x
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instRxcHasSize : {n : ℕ} → Std.Rxc.HasSize (BitVec n)
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.isLowerSet_of_isClosed : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] {s : Set α} [Topology.IsScott α Set.univ],
  IsClosed s → IsLowerSet s
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_evalRingHom_pi : ∀ {ι : Type u_4} {R : ι → Type u_5} [inst : (i : ι) → Semiring (R i)] {I : (i : ι) → Ideal (R i)} (i : ι),
  Ideal.map (Pi.evalRingHom R i) (Ideal.pi I) = I i
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_id : ∀ {K : Type u_1} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing M] (j : K →+* M) (p : ℕ) [inst_2 : ExpChar M p]
  [inst_3 : ExpChar K p] [inst_4 : PerfectRing M p], PerfectRing.lift (RingHom.id K) j p = j
-- Qq.Macro
Qq.Impl.unquoteLevelList : Lean.Expr → Qq.Impl.UnquoteM (List Lean.Level)
-- Init.Data.Array.Range
Array.range'_eq_singleton_iff : ∀ {s n a : ℕ}, Array.range' s n = #[a] ↔ s = a ∧ n = 1
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Multiplicativity of leading coefficients  -/
MonomialOrder.leadingCoeff_mul_of_mul_leadingCoeff_ne_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.leadingCoeff f * m.leadingCoeff g ≠ 0 → m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
-- Init.Data.UInt.Bitwise
UInt32.and_zero : ∀ {a : UInt32}, a &&& 0 = 0
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.IsNormal.generatedNormal_le : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (X : (c d : C) → Set (c ⟶ d)) {S : CategoryTheory.Subgroupoid C},
  S.IsNormal → (CategoryTheory.Subgroupoid.generatedNormal X ≤ S ↔ ∀ (c d : C), X c d ⊆ S.arrows c d)
-- Mathlib.Data.PNat.Basic
PNat.mod_add_div' : ∀ (m k : ℕ+), ↑(m.mod k) + m.div k * ↑k = ↑m
-- Mathlib.Data.TwoPointing
/-- Two-pointing of a type. This is a Type-valued termed `Nontrivial`.  -/
TwoPointing : Type u_3 → Type u_3
-- Std.Do.SPred.SVal
Std.Do.SVal.instInhabitedStateTupleNil : Inhabited (Std.Do.SVal.StateTuple [])
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.sieveExtend.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (x x_1 : CategoryTheory.Presieve.FamilyOfElements P R),
  x = x_1 →
    ∀ ⦃Y : C⦄ (f f_1 : Y ⟶ X) (e_f : f = f_1) (a : (CategoryTheory.Sieve.generate R).arrows f),
      x.sieveExtend f a = x_1.sieveExtend f_1 ⋯
-- Aesop.Forward.State
/-- Map from each rule's name to its `RuleState` -/
Aesop.ForwardState.ruleStates : Aesop.ForwardState → Lean.PHashMap Aesop.RuleName Aesop.RuleState
-- Lean.Meta.Tactic.SolveByElim
Lean.Meta.SolveByElim.ApplyRulesConfig.mk.inj : ∀ {toBacktrackConfig : Lean.Meta.Tactic.Backtrack.BacktrackConfig} {toApplyConfig : Lean.Meta.ApplyConfig}
  {transparency : Lean.Meta.TransparencyMode} {symm exfalso : Bool}
  {toBacktrackConfig_1 : Lean.Meta.Tactic.Backtrack.BacktrackConfig} {toApplyConfig_1 : Lean.Meta.ApplyConfig}
  {transparency_1 : Lean.Meta.TransparencyMode} {symm_1 exfalso_1 : Bool},
  { toBacktrackConfig := toBacktrackConfig, toApplyConfig := toApplyConfig, transparency := transparency, symm := symm,
        exfalso := exfalso } =
      { toBacktrackConfig := toBacktrackConfig_1, toApplyConfig := toApplyConfig_1, transparency := transparency_1,
        symm := symm_1, exfalso := exfalso_1 } →
    toBacktrackConfig = toBacktrackConfig_1 ∧
      toApplyConfig = toApplyConfig_1 ∧ transparency = transparency_1 ∧ symm = symm_1 ∧ exfalso = exfalso_1
-- Mathlib.Analysis.Normed.Group.Basic
edist_zero_left : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), edist 0 a = ↑‖a‖₊
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.uliftFunctor_obj_coe : ∀ (X : AddCommMonCat), ↑(AddCommMonCat.uliftFunctor.obj X) = ULift.{u, v} ↑X
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Ideal.Quotient.eq_factor_of_eq_factor_succ : ∀ {R : Type u_1} [inst : Ring R] {I : ℕ → Ideal R} [inst_1 : ∀ (n : ℕ), (I n).IsTwoSided] (hI : Antitone I)
  (x : (n : ℕ) → R ⧸ I n),
  (∀ (m : ℕ), x m = (Ideal.Quotient.factor ⋯) (x (m + 1))) →
    ∀ {m n : ℕ} (g : m ≤ n), x m = (Ideal.Quotient.factor ⋯) (x n)
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.mk : {R : Type u_1} → R → (n : ℕ) → (Fin n → R) → PrimeSpectrum.BasicConstructibleSetData R
-- Init.Data.UInt.Lemmas
USize.toNat.inj : ∀ {a b : USize}, a.toNat = b.toNat → a = b
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_toUInt8 : ∀ (n : USize) (h : System.Platform.numBits = 64), n.toUInt8.toBitVec = BitVec.setWidth 8 (n.toBitVec64 h)
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.val_map_le_iff : ∀ {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [inst : CommRing R] [inst_1 : Ring A]
  [inst_2 : LinearOrderedCommMonoidWithZero ΓR] [inst_3 : LinearOrderedCommMonoidWithZero ΓA] [inst_4 : Algebra R A]
  (vR : Valuation R ΓR) (vA : Valuation A ΓA) [vR.HasExtension vA] (x y : R),
  vA ((algebraMap R A) x) ≤ vA ((algebraMap R A) y) ↔ vR x ≤ vR y
-- Lean.Data.Json.Basic
Lean.JsonNumber.instInhabited : Inhabited Lean.JsonNumber
-- Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
MeasureTheory.cylinder_mem_closedCompactCylinders : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] (s : Finset ι)
  (S : Set ((i : ↥s) → X ↑i)),
  IsClosed S → IsCompact S → MeasureTheory.cylinder s S ∈ MeasureTheory.closedCompactCylinders X
-- Mathlib.Data.Stream.Init
Stream'.take_prefix : ∀ {α : Type u} (m n : ℕ) (a : Stream' α), Stream'.take m a <+: Stream'.take n a ↔ m ≤ n
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.div_comp : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_7} [inst : Div G] (f g : β → G) (z : α → β), (f / g) ∘ z = f ∘ z / g ∘ z
-- Mathlib.Topology.Algebra.Group.Matrix
Topology.IsClosedEmbedding.generalLinearGroup_map : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : CommRing S] [inst_5 : TopologicalSpace S] {f : R →+* S} [IsTopologicalRing R]
  [T0Space R], Topology.IsClosedEmbedding ⇑f → Topology.IsClosedEmbedding ⇑(Matrix.GeneralLinearGroup.map f)
-- Mathlib.Algebra.Opposites
AddOpposite.instUnique : {α : Type u_1} → [Unique α] → Unique αᵃᵒᵖ
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.instDivisibleByInt : {𝕜 : Type u_1} →
  [inst : Field 𝕜] →
    (p : 𝕜) →
      [inst_1 : LinearOrder 𝕜] →
        [IsStrictOrderedRing 𝕜] → [hp : Fact (0 < p)] → [FloorRing 𝕜] → DivisibleBy (AddCircle p) ℤ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.RankFunction.lt : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} [inst : PartialOrder α] (self : h.RankFunction α)
  {x y : h.ι}, h.AncestralRel x y → self.rank x < self.rank y
-- Mathlib.Order.Filter.Prod
Filter.prod.instNeBot : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} [hf : f.NeBot] [hg : g.NeBot], (f ×ˢ g).NeBot
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_sub_eq_right_of_natDegree_lt : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, p.natDegree < q.natDegree → (p - q).natDegree = q.natDegree
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
quadraticCharFun.congr_simp : ∀ (α : Type u_1) [inst : MonoidWithZero α] {inst_1 : DecidableEq α} [inst_2 : DecidableEq α]
  {inst_3 : DecidablePred IsSquare} [inst_4 : DecidablePred IsSquare] (a a_1 : α),
  a = a_1 → quadraticCharFun α a = quadraticCharFun α a_1
-- Init.Data.Int.Order
/-- Variant of `Int.toNat_sub` taking non-negativity hypotheses,
rather than expecting the arguments to be casts of natural numbers.
 -/
Int.toNat_sub'' : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (a - b).toNat = a.toNat - b.toNat
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.eventually_measurableSet : ∀ {G : Type u_4} {X : Type u_5} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_6} {l : Filter ι} {F : ι → Set X},
  IsAddFoelner G μ l F → ∀ᶠ (i : ι) in l, MeasurableSet (F i)
-- Init.Data.List.Lemmas
List.getLast?_cons_of_ne_nil : ∀ {α : Type u_1} {x : α} {xs : List α}, xs ≠ [] → (x :: xs).getLast? = xs.getLast?
-- Mathlib.Algebra.Quaternion
/-- `QuaternionAlgebra.equivTuple` as a linear equivalence.  -/
QuaternionAlgebra.linearEquivTuple : {R : Type u_3} → (c₁ c₂ c₃ : R) → [inst : CommRing R] → QuaternionAlgebra R c₁ c₂ c₃ ≃ₗ[R] Fin 4 → R
-- Mathlib.Data.Nat.Prime.Basic
Nat.not_prime_of_dvd_of_ne : ∀ {m n : ℕ}, m ∣ n → m ≠ 1 → m ≠ n → ¬Nat.Prime n
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Hom.mk.injEq : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (toHom : X.Hom Y.toPresheafedSpace)
  (prop : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom.stalkMap x)))
  (toHom_1 : X.Hom Y.toPresheafedSpace)
  (prop_1 : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom_1.stalkMap x))),
  ({ toHom := toHom, prop := prop } = { toHom := toHom_1, prop := prop_1 }) = (toHom = toHom_1)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_coe_toAddEquiv : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_5}
  [inst_2 : EquivLike F M N] [inst_3 : AddEquivClass F M N] (f : F) (S : AddSubmonoid M),
  AddSubmonoid.map (↑f) S = AddSubmonoid.map f S
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
/-- `IsMinimalPrime I p` says that `p` is a minimal prime over `I`.  -/
Ideal.IsMinimalPrime : {R : Type u_1} → [inst : CommSemiring R] → Ideal R → Ideal R → Prop
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.mk.congr_simp : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (x x_1 : K) (e_x : x = x_1)
  (h : 0 ≤ ArchimedeanClass.mk x), ArchimedeanClass.FiniteElement.mk x h = ArchimedeanClass.FiniteElement.mk x_1 ⋯
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.exists_isBasis_union_inter_isBasis : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α),
  autoParam (X ⊆ M.E) Matroid.exists_isBasis_union_inter_isBasis._auto_1 →
    autoParam (Y ⊆ M.E) Matroid.exists_isBasis_union_inter_isBasis._auto_3 →
      ∃ I, M.IsBasis I (X ∪ Y) ∧ M.IsBasis (I ∩ Y) Y
-- Mathlib.Topology.DiscreteSubset
IsDiscrete.image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsDiscrete s → Topology.IsInducing f → IsDiscrete (f '' s)
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.sum_lof : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (j : ι)
  (x : AdicCompletion I (M j)),
  (AdicCompletion.sum I M) ((DirectSum.lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) x) =
    (AdicCompletion.map I (DirectSum.lof R ι M j)) x
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.appTop : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  P f →
    ∀ [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y],
      Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f))
-- Mathlib.CategoryTheory.Center.Preadditive
CategoryTheory.CatCenter.app_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (z : CategoryTheory.CatCenter C) (X : C), (-z).app X = -z.app X
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_ofList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  k ∈ Std.ExtDTreeMap.ofList l cmp ↔ (List.map Sigma.fst l).contains k = true
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.le_comap_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β)
  (μ : MeasureTheory.Measure β),
  Function.Injective f →
    (∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ) →
      ∀ (s : Set α), μ (f '' s) ≤ (MeasureTheory.Measure.comap f μ) s
-- Init.Data.String.Subslice
String.Slice.toSlice_subsliceFrom : ∀ {s : String.Slice} {newStart : s.Pos}, (s.subsliceFrom newStart).toSlice = s.sliceFrom newStart
-- Mathlib.Order.BooleanAlgebra.Basic
himp_ne_right : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x ⇨ y ≠ x ↔ x ≠ ⊤ ∨ y ≠ ⊤
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.instTransIsLittleOTVSIsThetaTVS : {α : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : TopologicalSpace E] →
                [inst_3 : Module 𝕜 E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : TopologicalSpace F] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : AddCommGroup G] →
                          [inst_8 : TopologicalSpace G] →
                            [inst_9 : Module 𝕜 G] →
                              {l : Filter α} →
                                Trans (Asymptotics.IsLittleOTVS 𝕜 l) (Asymptotics.IsThetaTVS 𝕜 l)
                                  (Asymptotics.IsLittleOTVS 𝕜 l)
-- Mathlib.GroupTheory.Coxeter.Inversion
/-- The right inversion sequence of `ω`. The right inversion sequence of a word
$s_{i_1} \cdots s_{i_\ell}$ is the sequence
$$s_{i_\ell}\cdots s_{i_1}\cdots s_{i_\ell}, \ldots,
    s_{i_{\ell}}s_{i_{\ell - 1}}s_{i_{\ell - 2}}s_{i_{\ell - 1}}s_{i_\ell}, \ldots,
    s_{i_{\ell}}s_{i_{\ell - 1}}s_{i_\ell}, s_{i_\ell}.$$
 -/
CoxeterSystem.rightInvSeq : {B : Type u_1} → {W : Type u_2} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → List B → List W
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.eq_zero : ∀ {M : Type u_1} [inst : AddMonoid M] [Subsingleton (AddUnits M)] (u : AddUnits M), u = 0
-- Mathlib.Data.Complex.Basic
Complex.one_im : Complex.im 1 = 0
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_monoidHom_injective : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, Function.Injective fun f => ↑f
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.atTop_eq_generate_of_not_bddAbove : ∀ {α : Type u_3} [inst : LinearOrder α] {s : Set α}, ¬BddAbove s → Filter.atTop = Filter.generate (Set.Ici '' s)
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
/-- When `j` is not a maximal element, then
`(Φ.iterationFunctor J).obj (Order.succ j)` is isomorphic to
`Φ.succ ((Φ.iterationFunctor J).obj j)`.  -/
CategoryTheory.SmallObject.SuccStruct.iterationFunctorObjSuccIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Φ : CategoryTheory.SmallObject.SuccStruct C) →
      {J : Type w} →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] →
                [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] →
                  (j : J) →
                    ¬IsMax j → ((Φ.iterationFunctor J).obj (Order.succ j) ≅ Φ.succ ((Φ.iterationFunctor J).obj j))
-- Mathlib.Algebra.Algebra.Hom
MulSemiringAction.toAlgHom_apply : ∀ {M : Type u_1} (R : Type u_3) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] [inst_4 : MulSemiringAction M A] [inst_5 : SMulCommClass M R A] (m : M) (a : A),
  (MulSemiringAction.toAlgHom R A m) a = m • a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.skipSuffixWhile_eq_iff : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  (s : String.Slice) (res : s.Pos),
  s.skipSuffixWhile pat = res ↔
    String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat res s.endPos ∧
      (¬String.Slice.Pattern.Model.RevMatchesAt pat res ∨ String.Slice.Pattern.Model.IsLongestRevMatchAt pat res res)
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
Set.Countable.measure_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α},
  s.Countable → ∀ (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ], μ s = 0
-- Mathlib.Data.Nat.MaxPowDiv
Nat.divMaxPow_base_pow_mul : ∀ {p : ℕ}, p ≠ 0 → ∀ (n k : ℕ), (p ^ k * n).divMaxPow p = n.divMaxPow p
-- Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
/-- Construct a simplicial complex from an abstract simplicial complex on a set of points
over the `𝕜`-module of finitely supported functions on those points.
 -/
Geometry.SimplicialComplex.onFinsupp : {𝕜 : Type u_1} →
  {ι : Type u_2} →
    [DecidableEq ι] →
      [DecidableEq 𝕜] →
        [inst : Field 𝕜] →
          [inst_1 : LinearOrder 𝕜] →
            [IsStrictOrderedRing 𝕜] → PreAbstractSimplicialComplex ι → Geometry.SimplicialComplex 𝕜 (ι →₀ 𝕜)
-- Mathlib.Algebra.Group.NatPowAssoc
neg_npow_assoc : ∀ {R : Type u_2} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [NatPowAssoc R] (a b : R) (k : ℕ),
  (-1) ^ k * a * b = (-1) ^ k * (a * b)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mul : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Lean.Compiler.Specialize
Lean.Compiler.getSpecializationArgs? : Lean.Environment → Lean.Name → Option (Array ℕ)
-- Mathlib.Order.Defs.LinearOrder
LinearOrder.toPartialOrder : {α : Type u_2} → [self : LinearOrder α] → PartialOrder α
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- If `i ≠ j`, the pullback `Xᵢ ×[∐ X] Xⱼ` is initial.  -/
CategoryTheory.Limits.IsInitial.ofCoproductDisjoint : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {X : ι → C} →
        [CategoryTheory.Limits.CoproductDisjoint X] →
          {i j : ι} →
            i ≠ j →
              [inst_2 : CategoryTheory.Limits.HasCoproduct X] →
                [inst_3 :
                    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.Sigma.ι X i)
                      (CategoryTheory.Limits.Sigma.ι X j)] →
                  CategoryTheory.Limits.IsInitial
                    (CategoryTheory.Limits.pullback (CategoryTheory.Limits.Sigma.ι X i)
                      (CategoryTheory.Limits.Sigma.ι X j))
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_neg : ∀ {α : Type u_1} [inst : AddCommGroup α] (a : WithTop α), (-a).untop₀ = -a.untop₀
-- Std.Http.Data.Headers
/-- Retrieves the first `Header.Value` for the given key.
Returns `none` if the header is absent.
 -/
Std.Http.Headers.get? : Std.Http.Headers → Std.Http.Header.Name → Option Std.Http.Header.Value