mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instInhabited : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → Inhabited (QuadraticMap R M N)
-- Init.Data.List.Nat.Range
List.take_range'_of_length_le : ∀ {n k start step : ℕ}, n ≤ k → List.take k (List.range' start n step) = List.range' start n step
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_C : ∀ {R : Type u} {a : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a).trailingDegree = 0
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.mk : (carrier : Type u) → [str : AddMonoid carrier] → AddMonCat
-- Lean.Data.Trie
Lean.Data.Trie.node1.inj : ∀ {α : Type} {a : Option α} {a_1 : UInt8} {a_2 : Lean.Data.Trie α} {a_3 : Option α} {a_4 : UInt8}
  {a_5 : Lean.Data.Trie α},
  Lean.Data.Trie.node1 a a_1 a_2 = Lean.Data.Trie.node1 a_3 a_4 a_5 → a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_mod : ∀ (a b : UInt64), a < 4294967296 → b < 4294967296 → (a % b).toUInt32 = a.toUInt32 % b.toUInt32
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_inverse_obj_of : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) (X : CategoryTheory.Core D), (E.core.inverse.obj X).of = E.inverse.obj X.of
-- Mathlib.Algebra.Notation.Prod
Prod.swap_inv : ∀ {G : Type u_8} {H : Type u_9} [inst : Inv G] [inst_1 : Inv H] (p : G × H), p⁻¹.swap = p.swap⁻¹
-- Mathlib.Order.Filter.AtTopBot.Tendsto
StrictMono.tendsto_atTop : ∀ {φ : ℕ → ℕ}, StrictMono φ → Filter.Tendsto φ Filter.atTop Filter.atTop
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportFailure.mk : Lean.Name → Lean.Name → Lean.Exception → Lean.Meta.RefinedDiscrTree.ImportFailure✝
-- Batteries.Data.Fin.Lemmas
Fin.findSome?_zero : ∀ {α : Type u_1} {f : Fin 0 → Option α}, Fin.findSome? f = none
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasDetector.hasCodetector_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.HasDetector C],
  CategoryTheory.HasCodetector Cᵒᵖ
-- Lean.LocalContext
Lean.LocalContext.foldrM : {m : Type u_1 → Type u_2} → {β : Type u_1} → [Monad m] → Lean.LocalContext → (Lean.LocalDecl → β → m β) → β → m β
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
CategoryTheory.ObjectProperty.instIsEquivalenceFullSubcategoryIsoClosureιOfLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  (CategoryTheory.ObjectProperty.ιOfLE ⋯).IsEquivalence
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.idCompletionCore : Lean.Elab.ContextInfo →
  Lean.Syntax → Lean.Name → Lean.Server.Completion.HoverInfo → Bool → Lean.Server.Completion.M✝ Unit
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupKind.noConfusionType : Sort v✝ → Lean.Lsp.MarkupKind → Lean.Lsp.MarkupKind → Sort v✝
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Const.maxEntry.eq_def : ∀ {α : Type u} {β : Type v} (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.isEmpty = false),
  Std.DTreeMap.Internal.Impl.Const.maxEntry x x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => (k, v)
    | Std.DTreeMap.Internal.Impl.inner size k v l l_1@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r), h_1 =>
      Std.DTreeMap.Internal.Impl.Const.maxEntry l_1 ⋯
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.disjoint_map : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F},
  Function.Injective ⇑f → ∀ {H K : Submonoid M}, Disjoint H K → Disjoint (Submonoid.map f H) (Submonoid.map f K)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_pos_iff_mem_support : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)], 0 < G.degree v ↔ v ∈ G.support
-- Mathlib.CategoryTheory.Join.Opposites
_private.Mathlib.CategoryTheory.Join.Opposites.0.CategoryTheory.Join.opEquiv.match_1.splitter : (C : Type u_2) →
  (D : Type u_1) →
    [inst : CategoryTheory.Category.{u_3, u_2} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_1} D] →
        (motive : (CategoryTheory.Join C D)ᵒᵖ → Sort u_5) →
          (x : (CategoryTheory.Join C D)ᵒᵖ) →
            ((a : C) → motive (Opposite.op (CategoryTheory.Join.left a))) →
              ((a : D) → motive (Opposite.op (CategoryTheory.Join.right a))) → motive x
-- Mathlib.Probability.Kernel.Composition.Lemmas
/-- The composition of two product kernels `(ξ ×ₖ η') ∘ₖ (κ ×ₖ ζ)` is the product of the
compositions `(ξ ∘ₖ (κ ×ₖ ζ)) ×ₖ (η' ∘ₖ (κ ×ₖ ζ))`, if `ζ` is deterministic (of the form
`.deterministic f hf`) and `η'` does not depend on the output of `κ`.
That is, `η'` has the form `η.prodMkLeft β` for a kernel `η`.

If `κ` was deterministic, this would be true even if `η.prodMkLeft β` was a more general
kernel since `κ ×ₖ Kernel.deterministic f hf` would be deterministic and commute with copying.
Here `κ` is not deterministic, but it is discarded in one branch of the copy.  -/
ProbabilityTheory.Kernel.prod_prodMkLeft_comp_prod_deterministic : ∀ {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ} {β' : Type u_5} {ε : Type u_6} {mβ' : MeasurableSpace β'} {mε : MeasurableSpace ε}
  (κ : ProbabilityTheory.Kernel γ β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel ε β')
  [ProbabilityTheory.IsSFiniteKernel η] (ξ : ProbabilityTheory.Kernel (β × ε) δ) [ProbabilityTheory.IsSFiniteKernel ξ]
  {f : γ → ε} (hf : Measurable f),
  (ξ.prod (ProbabilityTheory.Kernel.prodMkLeft β η)).comp (κ.prod (ProbabilityTheory.Kernel.deterministic f hf)) =
    (ξ.comp (κ.prod (ProbabilityTheory.Kernel.deterministic f hf))).prod
      (η.comp (ProbabilityTheory.Kernel.deterministic f hf))
-- Lean.Meta.AbstractNestedProofs
Lean.Meta.AbstractNestedProofs.M : Type → Type
-- Mathlib.Topology.Category.Profinite.Extend
Profinite.Extend.functorOp_obj : ∀ {I : Type u} [inst : CategoryTheory.SmallCategory I] {F : CategoryTheory.Functor I FintypeCat}
  (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (X : Iᵒᵖ),
  (Profinite.Extend.functorOp c).obj X = CategoryTheory.CostructuredArrow.mk (c.π.app (Opposite.unop X)).op
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The projection to the opcycles of a homological complex.  -/
HomologicalComplex.pOpcycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) → (i : ι) → [inst_2 : K.HasHomology i] → K.X i ⟶ K.opcycles i
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.hasFPowerSeriesAt : ∀ {𝕜 : 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}, HasFPowerSeriesOnBall f p x r → HasFPowerSeriesAt f p x
-- Lean.Level
Lean.LevelMVarId.mk.sizeOf_spec : ∀ (name : Lean.Name), sizeOf { name := name } = 1 + sizeOf name
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.DTreeMap.Raw.entryAtIdx? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → ℕ → Option ((a : α) × β a)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
/-- The prime spectrum of the zero ring is empty.  -/
PrimeSpectrum.instIsEmptyOfSubsingleton : ∀ {R : Type u} [inst : CommSemiring R] [Subsingleton R], IsEmpty (PrimeSpectrum R)
-- Init.Data.AC
Lean.Data.AC.removeNeutrals : {α : Sort u_1} → [info : Lean.Data.AC.ContextInformation α] → α → List ℕ → List ℕ
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.adjp_transpose : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  (A : Matrix n n R), Matrix.adjp s A.transpose = (Matrix.adjp s A).transpose
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Subtype.boundedOrder : {X : Type u_1} →
  [inst : NormedAddCommGroup X] →
    {M : Type u_2} →
      [inst_1 : Ring M] → [inst_2 : Module M X] → [inst_3 : FaithfulSMul M X] → BoundedOrder { P // IsLprojection X P }
-- Mathlib.Data.Set.Function
Subtype.coind_surjective : ∀ {α : Type u_7} {β : Type u_8} {f : α → β} {p : Set β} (h : ∀ (a : α), f a ∈ p),
  Set.SurjOn f Set.univ p → Function.Surjective (Subtype.coind f h)
-- Mathlib.Topology.UniformSpace.Cauchy
/-- The union of two totally bounded sets is totally bounded.  -/
TotallyBounded.union : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s t : Set α},
  TotallyBounded s → TotallyBounded t → TotallyBounded (s ∪ t)
-- Mathlib.Data.Countable.Small
Uncountable.of_not_small : ∀ {α : Type v}, ¬Small.{w, v} α → Uncountable α
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.congr_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s s₁ : Set α}
  {x : α}, ContinuousWithinAt f s x → Set.EqOn g f s₁ → s₁ ⊆ s → g x = f x → ContinuousWithinAt g s₁ x
-- Init.Data.Format.Basic
/-- `nest indent f` increases the current indentation level by `indent` while rendering `f`.

Example:
```lean example
open Std Format in
def fmtList (l : List Format) : Format :=
  let f := joinSep l  ("," ++ Format.line)
  group (nest 1 <| "[" ++ f ++ "]")
```

This will be written all on one line, but if the text is too large, the formatter will put in
linebreaks after the commas and indent later lines by 1.
 -/
Std.Format.nest : ℤ → Std.Format → Std.Format
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.linear_isTheta_right_add : ∀ (c e : ℤ) (z : ℂ), (fun d => ↑c * z + ↑d + ↑e) =Θ[Filter.cofinite] fun n => ↑n
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.compCreatesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Initial] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  {B : Type u₄} →
                    [inst_4 : CategoryTheory.Category.{v₄, u₄} B] →
                      {H : CategoryTheory.Functor E B} →
                        [CategoryTheory.CreatesLimit G H] → CategoryTheory.CreatesLimit (F.comp G) H
-- Mathlib.MeasureTheory.Constructions.Pi
/-- The product measure on an encodable finite type, defined by mapping `Measure.tprod` along the
equivalence `MeasurableEquiv.piMeasurableEquivTProd`.
The definition `MeasureTheory.Measure.pi` should be used instead of this one.  -/
MeasureTheory.Measure.pi' : {ι : Type u_1} →
  {α : ι → Type u_3} →
    [Fintype ι] →
      [inst : (i : ι) → MeasurableSpace (α i)] →
        ((i : ι) → MeasureTheory.Measure (α i)) → [Encodable ι] → MeasureTheory.Measure ((i : ι) → α i)
-- Mathlib.NumberTheory.MulChar.Basic
/-- The inverse of a multiplicative character `χ`, applied to `a`, is the inverse of `χ a`.  -/
MulChar.inv_apply_eq_inv : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R') (a : R),
  χ⁻¹ a = Ring.inverse (χ a)
-- Mathlib.Algebra.GroupWithZero.Associated
prime_pow_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p : M} {n : ℕ}, Prime (p ^ n) ↔ Prime p ∧ n = 1
-- Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
HomotopicalAlgebra.CofibrantObject.instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.CofibrantObject.localizerMorphism C).arrow.HasLeftResolutions
-- Mathlib.Data.Real.Basic
Real.mk_near_of_forall_near : ∀ {f : CauSeq ℚ abs} {x ε : ℝ}, (∃ i, ∀ j ≥ i, |↑(↑f j) - x| ≤ ε) → |Real.mk f - x| ≤ ε
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.below.add : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  {motive : (a : E) → IsSolvableByRad F a → Prop} (α β : E) (a : IsSolvableByRad F α) (a_1 : IsSolvableByRad F β),
  IsSolvableByRad.below a → motive α a → IsSolvableByRad.below a_1 → motive β a_1 → IsSolvableByRad.below ⋯
-- Mathlib.Order.ScottContinuity.Complete
ScottContinuous.inf₂ : ∀ {β : Type u_2} [inst : CompleteLinearOrder β],
  ScottContinuous fun x =>
    match x with
    | (a, b) => min a b
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₃ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ)
  (h : a + b = n) (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).inv.app X).hom₃ =
    (CategoryTheory.shiftFunctorAdd' C a b n h).inv.app X.obj₃
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.addConvolution_zero : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : AddMonoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F]
  (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E), DiscreteConvolution.addConvolution L f 0 = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.compare_minKeyD_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β}
  {fallback : α}, cmp ((t.modify k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Mathlib.Data.Fin.Basic
Fin.coe_natCast_eq_mod : ∀ (m n : ℕ) [inst : NeZero m], ↑↑n = n % m
-- Mathlib.Topology.Algebra.Monoid
instContinuousAddAdditiveOfContinuousMul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M], ContinuousAdd (Additive M)
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
ModuleCat.Derivation.desc_d : ∀ {A B : CommRingCat} {f : A ⟶ B} {M : ModuleCat ↑B} (D : M.Derivation f) (b : ↑B),
  (CategoryTheory.ConcreteCategory.hom D.desc) (CommRingCat.KaehlerDifferential.d b) = D.d b
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.eq_of_xn_modEq_lem2 : ∀ {a : ℕ} (a1 : 1 < a) {n : ℕ}, 2 * Pell.xn a1 n = Pell.xn a1 (n + 1) → a = 2 ∧ n = 0
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopCoeff.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] (i j : ι),
  RootPairing.chainTopCoeff i j = if h : LinearIndependent R ![P.root i, P.root j] then ⋯.choose.toNat else 0
-- Mathlib.CategoryTheory.Galois.Examples
/-- A nonempty `G`-set with transitive `G`-action is connected.  -/
CategoryTheory.FintypeCat.Action.isConnected_of_transitive : ∀ (G : Type u) [inst : Group G] (X : FintypeCat) [inst_1 : MulAction G X.obj] [MulAction.IsPretransitive G X.obj]
  [h : Nonempty X.obj], CategoryTheory.PreGaloisCategory.IsConnected (Action.FintypeCat.ofMulAction G X)
-- Mathlib.Algebra.Homology.ShortComplex.Limits
/-- `limitCone F` becomes limit after the application of `π₁ : ShortComplex C ⥤ C`.  -/
CategoryTheory.ShortComplex.isLimitπ₁MapConeLimitCone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) →
            [inst_3 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] →
              [inst_4 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] →
                [inst_5 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] →
                  CategoryTheory.Limits.IsLimit
                    (CategoryTheory.ShortComplex.π₁.mapCone (CategoryTheory.ShortComplex.limitCone F))
-- Mathlib.Algebra.Group.Hom.Defs
/-- `0` is the additive homomorphism sending all elements to `0`  -/
instZeroAddHom : {M : Type u_4} → {N : Type u_5} → [inst : Add M] → [inst_1 : AddZeroClass N] → Zero (M →ₙ+ N)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.exists_pow_eq' : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} [Finite α], f.SameCycle x y → ∃ i < orderOf f, (f ^ i) x = y
-- Mathlib.Order.Filter.Prod
Filter.tendsto_prod_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {x : Filter α} {y : Filter β} {z : Filter γ},
  Filter.Tendsto f (x ×ˢ y) z ↔ ∀ W ∈ z, ∃ U ∈ x, ∃ V ∈ y, ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderiv_const_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {x : E} (c : F), fderiv 𝕜 (fun x => c) x = 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqResolvableCompletionItemData.beq : Lean.Lsp.ResolvableCompletionItemData → Lean.Lsp.ResolvableCompletionItemData → Bool
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
CFC.conjSqrt_one : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : SeparatelyContinuousMul A] [IsSemitopologicalRing A] [T2Space A] (c : A),
  autoParam (0 ≤ c) CFC.conjSqrt_one._auto_1 → (CFC.conjSqrt c) 1 = c
-- Mathlib.Data.Rat.Floor
Nat.coprime_sub_mul_floor_rat_div_of_coprime : ∀ {n d : ℕ}, n.Coprime d → (↑n - ↑d * ⌊↑n / ↑d⌋).natAbs.Coprime d
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
/-- `legendreSym p (-2)` is given by `χ₈' p`.  -/
legendreSym.at_neg_two : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], p ≠ 2 → legendreSym p (-2) = ZMod.χ₈' ↑p
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.piCongrRight_apply : ∀ {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [inst : (j : η) → Add (Ms j)]
  [inst_1 : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (j : η),
  (AddEquiv.piCongrRight es) x j = (es j) (x j)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_filterMap_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)},
  (Std.DTreeMap.filterMap f t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f k (t.get k h) = none
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
/-- `Real.tan` as an `OpenPartialHomeomorph` between `(-(π / 2), π / 2)` and the whole line.  -/
Real.tanPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.lfpApprox_eq_all_of_fixedPoint : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α},
  x ≤ f x → ((∀ (o : Ordinal.{u}), OrdinalApprox.lfpApprox f x o = x) ↔ f x = x)
-- Mathlib.Order.ULift
ULift.instMax_mathlib : {α : Type u} → [Max α] → Max (ULift.{v, u} α)
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.norm_def : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A] (x : Unitization 𝕜 A), ‖x‖ = ‖(Unitization.splitMul 𝕜 A) x‖
-- Mathlib.NumberTheory.Dioph
/-- Extensionality for `Poly α`  -/
Poly.ext : ∀ {α : Type u_1} {f g : Poly α}, (∀ (x : α → ℕ), f x = g x) → f = g
-- Mathlib.Data.Complex.Basic
Complex.ofReal.eq_1 : ∀ (r : ℝ), ↑r = { re := r, im := 0 }
-- Mathlib.Control.Traversable.Instances
Sum.id_traverse : ∀ {σ α : Type u_1} (x : σ ⊕ α), Sum.traverse pure x = x
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.minEntry? : {α : Type u} → {β : Type v} → (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_smul_pointwise_iff_exists : ∀ {K : Type u} [inst : Field K] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G K] (g : G) (x : K)
  (S : ValuationSubring K), x ∈ g • S ↔ ∃ s ∈ S, g • s = x
-- Mathlib.Algebra.Lie.Basic
LieEquiv.ofBijective_invFun : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Bijective ⇑f) (a : L₂),
  (LieEquiv.ofBijective f h).invFun a = (LinearEquiv.ofBijective (↑f) h).symm a
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.instEpiModuleCatH2π : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.Epi (groupHomology.H2π A)
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.charFun_map_add_prod_eq_mul : ∀ {E : Type u_2} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E]
  [inst_3 : InnerProductSpace ℝ E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν],
  MeasureTheory.charFun (MeasureTheory.Measure.map (fun p => p.1 + p.2) (μ.prod ν)) =
    MeasureTheory.charFun μ * MeasureTheory.charFun ν
-- Mathlib.Algebra.FiveLemma
/-- A special case of the five lemma in terms of groups. For a diagram explaining the
variables, see the module docstring.  -/
MonoidHom.bijective_of_surjective_of_bijective_of_right_exact : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} [inst : Group M₁]
  [inst_1 : Group M₂] [inst_2 : Group M₃] [inst_3 : Group N₁] [inst_4 : Group N₂] [inst_5 : Group N₃] (f₁ : M₁ →* M₂)
  (f₂ : M₂ →* M₃) (g₁ : N₁ →* N₂) (g₂ : N₂ →* N₃) (i₁ : M₁ →* N₁) (i₂ : M₂ →* N₂) (i₃ : M₃ →* N₃),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      Function.MulExact ⇑f₁ ⇑f₂ →
        Function.MulExact ⇑g₁ ⇑g₂ →
          Function.Surjective ⇑i₁ →
            Function.Bijective ⇑i₂ → Function.Surjective ⇑f₂ → Function.Surjective ⇑g₂ → Function.Bijective ⇑i₃
-- Mathlib.Order.Filter.Lift
Filter.eventually_lift'_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β},
  Monotone h → ∀ {p : β → Prop}, (∀ᶠ (y : β) in f.lift' h, p y) ↔ ∃ t ∈ f, ∀ y ∈ h t, p y
-- Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
HomotopyCategory.spectralObjectMappingCone_ω₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproducts C],
  (HomotopyCategory.spectralObjectMappingCone C).ω₁ =
    (HomotopyCategory.composableArrowsFunctor C).comp (HomotopyCategory.quotient C (ComplexShape.up ℤ))
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
IsLUB.neg : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G},
  IsLUB s a → IsGLB (-s) (-a)