mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] (f : NumberField.mixedEmbedding.mixedSpace K → E),
  ∫ (x : NumberField.mixedEmbedding.polarSpace K) in (NumberField.mixedEmbedding.polarSpaceCoord K).target,
      (∏ w, x.1 ↑w) • f (↑(NumberField.mixedEmbedding.polarSpaceCoord K).symm x) =
    ∫ (x : NumberField.mixedEmbedding.mixedSpace K), f x
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The unique map to the terminal object.  -/
CategoryTheory.SubobjectRepresentableBy.χ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} →
        (h : CategoryTheory.SubobjectRepresentableBy Ω) → (U : C) → U ⟶ CategoryTheory.Subobject.underlying.obj h.Ω₀
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.edgeSet_fromEdgeSet_incidenceSet : ∀ {V : Type u_1} (G : SimpleGraph V) (x : V), (SimpleGraph.fromEdgeSet (G.incidenceSet x)).edgeSet = G.incidenceSet x
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_mkSlice_rcc : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  Std.Slice.toList (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = List.drop lo (List.take (hi + 1) (Std.Slice.toList xs))
-- Mathlib.Data.Multiset.Bind
Multiset.bind_zero : ∀ {α : Type u_1} {β : Type v} (s : Multiset α), (s.bind fun x => 0) = 0
-- Mathlib.Order.Filter.Ultrafilter.Basic
Filter.atTop_eq_pure_of_isTop : ∀ {α : Type u} [inst : PartialOrder α] {x : α}, IsTop x → Filter.atTop = pure x
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Auxiliary function appearing in the functional equation for the odd Hurwitz zeta kernel, equal
to `∑ (n : ℕ), 2 * n * sin (2 * π * n * a) * exp (-π * n ^ 2 * x)`. See `hasSum_nat_sinKernel`
for the defining sum.  -/
HurwitzZeta.sinKernel : UnitAddCircle → ℝ → ℝ
-- Init.Data.Vector.Lemmas
Array.vector_mk_replicate : ∀ {α : Type u_1} {a : α} {n : ℕ}, Vector.mk (Array.replicate n a) ⋯ = Vector.replicate n a
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `LT` instance if available  -/
Lean.Meta.Grind.Arith.Linear.NatStruct.ltInst? : Lean.Meta.Grind.Arith.Linear.NatStruct → Option Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.zero_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f : Y ⟶ Z}, CategoryTheory.CategoryStruct.comp 0 f = 0
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.toStream.eq_def : ∀ {α : Type u_1} (x : RBTree.RBNode α) (x_1 : RBTree.RBNode.Stream α),
  x.toStream x_1 =
    match x, x_1 with
    | RBTree.RBNode.nil, acc => acc
    | RBTree.RBNode.node c l v r, acc => l.toStream (RBTree.RBNode.Stream.cons v r acc)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.lintegral_eq_top_of_measure_eq_top_ne_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → μ {x | f x = ⊤} ≠ 0 → ∫⁻ (x : α), f x ∂μ = ⊤
-- Mathlib.Data.Nat.Digits.Div
Nat.eleven_dvd_of_palindrome : ∀ {n : ℕ}, (Nat.digits 10 n).Palindrome → Even (Nat.digits 10 n).length → 11 ∣ n
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
/-- The value of the quadratic character at `-2`  -/
quadraticChar_neg_two : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 → (quadraticChar F) (-2) = ZMod.χ₈' ↑(Fintype.card F)
-- Init.Data.Range.Polymorphic.PRange
/-- The upper bound of the range. `upper` is included in the range.
   -/
Std.Ric.upper : {α : Type u} → Std.Ric α → α
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.isTopologicalAddGroup : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] (self : TopModuleCat R),
  IsTopologicalAddGroup ↑self.toModuleCat
-- Aesop.Nanos
Aesop.Nanos.instLE : LE Aesop.Nanos
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgHom_zero : ∀ {σ : Type u_1} {R : Type u_3} {n : ℕ} [inst : CommSemiring R] [inst_1 : Fintype σ] {r : R},
  MvPolynomial.esymmAlgHomMonomial σ 0 r = MvPolynomial.C r
-- Lean.Meta.Tactic.Grind.ProveEq
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.State.mk.inj : ∀ {cache : Std.HashMap (Lean.Expr × Lean.Expr) Lean.Expr} {varTypes lhss rhss : Array Lean.Expr}
  {cache_1 : Std.HashMap (Lean.Expr × Lean.Expr) Lean.Expr} {varTypes_1 lhss_1 rhss_1 : Array Lean.Expr},
  { cache := cache, varTypes := varTypes, lhss := lhss, rhss := rhss } =
      { cache := cache_1, varTypes := varTypes_1, lhss := lhss_1, rhss := rhss_1 } →
    cache = cache_1 ∧ varTypes = varTypes_1 ∧ lhss = lhss_1 ∧ rhss = rhss_1
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_norm_le_norm_inv_mul : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), ‖a‖ - ‖b‖ ≤ ‖a⁻¹ * b‖
-- Init.Grind.Module.OfNatModule
Lean.Grind.IntModule.OfNatModule.of_not_lt : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [inst_5 : Lean.Grind.OrderedAdd α] {a b : α}
  {a' b' : Lean.Grind.IntModule.OfNatModule.Q α},
  Lean.Grind.IntModule.OfNatModule.toQ a = a' → Lean.Grind.IntModule.OfNatModule.toQ b = b' → ¬a < b → ¬a' < b'
-- Std.Tactic.BVDecide.LRAT.Internal.Actions
/-- Since `IntAction` is a convenient parsing target and `DefaultClauseAction` is a useful Action type
for working with default clauses, an expected workflow pattern is to parse an external LRAT proof
into a list of `IntAction`s, and then use this function to convert that list of `IntAction`s to
`DefaultClauseAction`s.

This function returns an `Option` type so that `none` can be returned if converting from the
`IntAction` to `DefaultClauseAction` fails. This can occur if any of the literals in the `IntAction`
are 0 or ≥ n.
 -/
Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction : (n : ℕ) → Std.Tactic.BVDecide.LRAT.IntAction → Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n)
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_inj : ∀ {α : Type u_1} [inst : Encodable α] {a b : α}, Encodable.encode a = Encodable.encode b ↔ a = b
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.Script.TacticBuilder.extN.mkPat : Lean.FVarId → Lean.MetaM (Lean.TSyntax `rintroPat)
-- Mathlib.Algebra.Group.Defs
NSMul.ofSMul.eq_1 : ∀ {M : Type u_2} [inst : SMul ℕ M], NSMul.ofSMul = { nsmul := fun n x => SMul.smul n x }
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionsResult.subgoal.inj : ∀ {mvarId : Lean.MVarId} {remainingNames : List Lean.Name} {forbidden : Lean.FVarIdSet} {mvarId_1 : Lean.MVarId}
  {remainingNames_1 : List Lean.Name} {forbidden_1 : Lean.FVarIdSet},
  Lean.Meta.InjectionsResult.subgoal mvarId remainingNames forbidden =
      Lean.Meta.InjectionsResult.subgoal mvarId_1 remainingNames_1 forbidden_1 →
    mvarId = mvarId_1 ∧ remainingNames = remainingNames_1 ∧ forbidden = forbidden_1
-- Mathlib.Algebra.Polynomial.Div
Polynomial.X_sub_C_dvd_sub_C_eval : ∀ {R : Type u} {a : R} [inst : CommRing R] {p : Polynomial R},
  Polynomial.X - Polynomial.C a ∣ p - Polynomial.C (Polynomial.eval a p)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.SymmStruct.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C}
  (iso : (i j : ι) → I.left (i, j) ≅ I.left (j, i))
  (iso_hom_fst : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso i j).hom (I.fst (j, i)) = I.snd (i, j))
  (iso_hom_snd : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso i j).hom (I.snd (j, i)) = I.fst (i, j))
  (fst_eq_snd : ∀ (i : ι), I.fst (i, i) = I.snd (i, i)) (iso_1 : (i j : ι) → I.left (i, j) ≅ I.left (j, i))
  (iso_hom_fst_1 : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso_1 i j).hom (I.fst (j, i)) = I.snd (i, j))
  (iso_hom_snd_1 : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso_1 i j).hom (I.snd (j, i)) = I.fst (i, j))
  (fst_eq_snd_1 : ∀ (i : ι), I.fst (i, i) = I.snd (i, i)),
  ({ iso := iso, iso_hom_fst := iso_hom_fst, iso_hom_snd := iso_hom_snd, fst_eq_snd := fst_eq_snd } =
      { iso := iso_1, iso_hom_fst := iso_hom_fst_1, iso_hom_snd := iso_hom_snd_1, fst_eq_snd := fst_eq_snd_1 }) =
    (iso = iso_1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_eq_get_getKey? : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : a ∈ m}, m.getKey a h = (m.getKey? a).get ⋯
-- Mathlib.Algebra.Algebra.Prod
Prod.algebraMap_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (r : R),
  (algebraMap R (A × B)) r = ((algebraMap R A) r, (algebraMap R B) r)
-- Aesop.Tree.ExtractScript
Aesop.ExtractScriptM.State.mk.sizeOf_spec : ∀ (script : Aesop.Script.UScript) (proofHasMVar : Bool),
  sizeOf { script := script, proofHasMVar := proofHasMVar } = 1 + sizeOf script + sizeOf proofHasMVar
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapBilipschitz_packingRadius : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ Y) (K₁ K₂ : NNReal)
  (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hf₁ : AntilipschitzWith K₁ ⇑f) (hf₂ : LipschitzWith K₂ ⇑f) (D : Delone.DeloneSet X),
  (Delone.DeloneSet.mapBilipschitz f K₁ K₂ hK₁ hK₂ hf₁ hf₂ D).packingRadius = D.packingRadius / K₁
-- Lean.Meta.RecursorInfo
Lean.Meta.mkRecursorInfo : Lean.Name → optParam (Option ℕ) none → Lean.MetaM Lean.Meta.RecursorInfo
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.Suggestion.mk : Lean.Meta.Tactic.TryThis.SuggestionText →
  Option String →
    Option String →
      Option Lean.Meta.Tactic.TryThis.SuggestionStyle →
        Option Lean.MessageData → Option (String → String) → Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix_injective : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : DecidableEq n] [inst_1 : MulZeroOneClass α] [Nontrivial α],
  Function.Injective PEquiv.toMatrix
-- Init.Data.Vector.MapIdx
Vector.mapIdx_eq_replicate_iff : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : ℕ → α → β} {b : β},
  Vector.mapIdx f xs = Vector.replicate n b ↔ ∀ (i : ℕ) (h : i < n), f i xs[i] = b
-- Lean.Meta.Order
/-- An n-ary version of `mkInstPiOfInstForall`. Takes an array of arguments instead.
- -/
Lean.Meta.mkInstPiOfInstsForall : Array Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.sort_roots_charpoly_eq_eigenvalues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n),
  ((Multiset.map (⇑RCLike.re) T.charpoly.roots).sort fun x1 x2 => x1 ≥ x2) = List.ofFn (hT.eigenvalues hn)
-- Mathlib.LinearAlgebra.Matrix.Adjugate
/-- The adjugate matrix is the transpose of the cofactor matrix.

Typically, the cofactor matrix is defined by taking minors,
i.e. the determinant of the matrix with a row and column removed.
However, the proof of `mul_adjugate` becomes a lot easier if we use the
matrix replacing a column with a basis vector, since it allows us to use
facts about the `cramer` map.
 -/
Matrix.adjugate : {n : Type v} → {α : Type w} → [DecidableEq n] → [Fintype n] → [CommRing α] → Matrix n n α → Matrix n n α
-- Mathlib.Algebra.Group.Submonoid.Units
IsAddUnit.coe : ∀ {M : Type u_1} [inst : AddMonoid M] {S : Type u_2} [inst_1 : SetLike S M] [inst_2 : AddSubmonoidClass S M] {N : S}
  {a : ↥N}, IsAddUnit a → IsAddUnit ↑a
-- Mathlib.Algebra.Group.Commute.Defs
Commute.instRefl : ∀ {S : Type u_3} [inst : Mul S], Std.Refl Commute
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Given a functor `F : C₀ ⥤ C`, Grothendieck topologies `J₀` on `C₀` and `J`
on `C`, an object `S. : C`, this structure roughly contains the data of a `1`-hypercover
of `S` consisting of objects in `C₀`.  -/
CategoryTheory.Functor.OneHypercoverDenseData : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        CategoryTheory.Functor C₀ C →
          CategoryTheory.GrothendieckTopology C₀ →
            CategoryTheory.GrothendieckTopology C → C → Type (max (max (max u₀ v) v₀) (w + 1))
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
/-- Any continuous linear map from a locally compact space is a compact operator.  -/
isCompactOperator_of_locallyCompactSpace_rng : ∀ {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₂] [inst_1 : Semiring R₃] {σ₂₃ : R₂ →+* R₃} {M₂ : Type u_5}
  {M₃ : Type u_6} [inst_2 : TopologicalSpace M₂] [inst_3 : TopologicalSpace M₃] [inst_4 : AddCommGroup M₂]
  [inst_5 : Module R₂ M₂] [IsTopologicalAddGroup M₂] [LocallyCompactSpace M₂] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R₃ M₃] (T : M₂ →SL[σ₂₃] M₃), IsCompactOperator ⇑T
-- Mathlib.GroupTheory.Coprod.Basic
/-- Map `M ∗ N` to `M' ∗ N'` by applying `Sum.map f g` to each element of the underlying list.  -/
Monoid.Coprod.map : {M : Type u_1} →
  {N : Type u_2} →
    {M' : Type u_3} →
      {N' : Type u_4} →
        [inst : MulOneClass M] →
          [inst_1 : MulOneClass N] →
            [inst_2 : MulOneClass M'] →
              [inst_3 : MulOneClass N'] → (M →* M') → (N →* N') → Monoid.Coprod M N →* Monoid.Coprod M' N'
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.comp_codRestrict : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.Structure P] (f : L.Hom M N) (g : L.Hom N P) (p : L.Substructure P) (h : ∀ (b : N), g b ∈ p),
  (FirstOrder.Language.Hom.codRestrict p g h).comp f = FirstOrder.Language.Hom.codRestrict p (g.comp f) ⋯
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The deduplication of a pre-`0`-hypercover `E` in universe `w` to a pre-`0`-hypercover in
universe `max u v`. This is indexed by the morphisms of `E`.  -/
CategoryTheory.PreZeroHypercover.shrink : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → CategoryTheory.PreZeroHypercover S → CategoryTheory.PreZeroHypercover S
-- Init.Meta.Defs
/-- Creates an identifier from a name. The resulting identifier has no source position.
 -/
Lean.mkIdent : Lean.Name → Lean.Ident
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instOrdRange : Ord Lean.Lsp.Range
-- Init.Data.SInt.Lemmas
Int16.toInt_mod : ∀ (a b : Int16), (a % b).toInt = a.toInt.tmod b.toInt
-- Mathlib.LinearAlgebra.Dimension.Basic
Module.rank_top_le_rank_of_isScalarTower : ∀ (R : Type u) (R' : Type u') (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring R'] [inst_4 : Module R' M] [inst_5 : SMulWithZero R R'] [IsScalarTower R R' M] [FaithfulSMul R R']
  [IsScalarTower R R' R'], Module.rank R' M ≤ Module.rank R M
-- Mathlib.AlgebraicTopology.DoldKan.Faces
AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Y : C} {n q : ℕ} {φ : Y ⟶ X.obj (Opposite.op { len := n + 1 })},
  AlgebraicTopology.DoldKan.HigherFacesVanish q φ →
    ∀ (j : Fin (n + 2)), j ≠ 0 → n + 2 ≤ ↑j + q → CategoryTheory.CategoryStruct.comp φ (X.δ j) = 0
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.one_right_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {ζ : M}, IsPrimitiveRoot ζ 1 ↔ ζ = 1
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_intCast : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : IntCast α] (n : ℤ),
  Measurable ↑n
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_whiskerLeft_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z Z' : C} (f : Z ⟶ Z'),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) f)
        (CategoryTheory.MonoidalCategoryStruct.associator X Y Z').hom)
-- Init.Prelude
monadFunctorRefl : (m : Type u_1 → Type u_2) → MonadFunctorT m m
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.decodeBinLitAux : String → String.Pos.Raw → ℕ → Option ℕ
-- Init.MetaTypes
/-- Syntax objects for a Lean module.  -/
Lean.Module : Type
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply' : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K),
  ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x =
    Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀) • fun w =>
      ∏ i,
        w
            ((algebraMap (NumberField.RingOfIntegers K) K)
              ↑(NumberField.Units.fundSystem K (NumberField.mixedEmbedding.fundamentalCone.equivFinRank.symm i))) ^
          x ↑i
-- Mathlib.Analysis.Analytic.IteratedFDeriv
FormalMultilinearSeries.iteratedFDerivSeries.eq_2 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (k_2 : ℕ),
  p.iteratedFDerivSeries k_2.succ =
    (↑↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm).compFormalMultilinearSeries
      (p.iteratedFDerivSeries k_2).derivSeries
-- Std.Data.DTreeMap.Internal.Balancing
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.tacticTree_tac : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.comp_continuous_iff : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {α : Type u_14}
  [inst_9 : TopologicalSpace α] {f : α → P}, Continuous (⇑e ∘ f) ↔ Continuous f
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Turn an element of a type `F` satisfying `RingHomClass F α β` into an actual
`RingHom`. This is declared as the default coercion from `F` to `α →+* β`.  -/
RingHomClass.toRingHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → [RingHomClass F α β] → F → α →+* β
-- Mathlib.Data.Finset.Pi
Finset.restrict₂_preimage : ∀ {ι : Type u_2} {π : ι → Type u_3} {s t : Finset ι} [inst : DecidablePred fun x => x ∈ s] (hst : s ⊆ t)
  (u : (i : ↥s) → Set (π ↑i)),
  Finset.restrict₂ hst ⁻¹' Set.univ.pi u = Set.univ.pi fun j => if h : ↑j ∈ s then u ⟨↑j, h⟩ else Set.univ
-- Init.Grind.Ring.Field
Lean.Grind.Field.toInv : {α : Type u} → [self : Lean.Grind.Field α] → Inv α
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_key : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k (List.filter (fun p => f p.fst) l) = Option.filter f (Std.Internal.List.getKey? k l)
-- Mathlib.Topology.Order.Hom.Esakia
/-- `id` as a `PseudoEpimorphism`.  -/
PseudoEpimorphism.id : (α : Type u_2) → [inst : Preorder α] → PseudoEpimorphism α α
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.unop_epi_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.Epi f.unop ↔ CategoryTheory.Mono f
-- Mathlib.NumberTheory.ModularForms.LevelOne.Basic
one_mem_strictPeriods_SL : 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.cons.inj : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w} {v_1 : V} {h_1 : G.Adj u v_1}
  {p_1 : G.Walk v_1 w}, SimpleGraph.Walk.cons h p = SimpleGraph.Walk.cons h_1 p_1 → v = v_1 ∧ p ≍ p_1
-- Mathlib.Analysis.SumOverResidueClass
/-- If `f : ℕ → ℝ` is decreasing and has a negative term, then `f` is not summable.  -/
not_summable_of_antitone_of_neg : ∀ {f : ℕ → ℝ}, Antitone f → ∀ {n : ℕ}, f n < 0 → ¬Summable f
-- Mathlib.Data.List.Sort
List.sortedGE_iff_getElem_ge_getElem_of_le : ∀ {α : Type u_1} {l : List α} [inst : Preorder α],
  l.SortedGE ↔ ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, j ≤ i → l[i] ≤ l[j]
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.ext : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  {f f' : ContinuousMultilinearMap R M₁ M₂}, (∀ (x : (i : ι) → M₁ i), f x = f' x) → f = f'
-- Mathlib.Order.Interval.Finset.Defs
/-- `x ∈ finsetIoo a b ↔ a < x ∧ x < b`  -/
LocallyFiniteOrder.finset_mem_Ioo : ∀ {α : Type u_1} {inst : Preorder α} [self : LocallyFiniteOrder α] (a b x : α),
  x ∈ LocallyFiniteOrder.finsetIoo a b ↔ a < x ∧ x < b
-- Init.Data.Array.MapIdx
Array.mapFinIdx_append : ∀ {α : Type u_1} {β : Type u_2} {xs ys : Array α} {f : (i : ℕ) → α → i < (xs ++ ys).size → β},
  (xs ++ ys).mapFinIdx f = (xs.mapFinIdx fun i a h => f i a ⋯) ++ ys.mapFinIdx fun i a h => f (i + xs.size) a ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.paste_vert_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
  CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁ →
    CategoryTheory.CategoryStruct.comp h₂₁ v₂₂ = CategoryTheory.CategoryStruct.comp v₂₁ h₃₁ →
      (CategoryTheory.IsPushout h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁)
          (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁ ↔
        CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  hU.fromSpec = CategoryTheory.CategoryStruct.comp hU.isoSpec.inv U.ι
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.toFilteriUnion.eq_1 : ∀ {ι : Type u_1} [inst : Fintype ι] {l : BoxIntegral.IntegrationParams} (I : BoxIntegral.Box ι)
  (π₀ : BoxIntegral.Prepartition I),
  BoxIntegral.IntegrationParams.toFilteriUnion I π₀ = ⨆ c, l.toFilterDistortioniUnion I c π₀
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddCommGroup.toMetricSpace : {E : Type u_8} → [self : NormedAddCommGroup E] → MetricSpace E
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjoint : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ι → Set (Set Ω)} {S T : Set ι},
  ProbabilityTheory.Kernel.iIndepSets s κ μ →
    Disjoint S T → ProbabilityTheory.Kernel.IndepSets (piiUnionInter s S) (piiUnionInter s T) κ μ
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.limitConeIsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections],
  AddGrpCat.limitConeIsLimit F =
    CategoryTheory.liftedLimitIsLimit
      (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat)))