mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.mk.inj : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} {inst : L.Structure M} {inst_1 : L.Structure N}
  {toFun : M → N}
  {map_formula' :
    autoParam (∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun ∘ x) ↔ φ.Realize x)
      FirstOrder.Language.ElementaryEmbedding.map_formula'._autoParam}
  {toFun_1 : M → N}
  {map_formula'_1 :
    autoParam (∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun_1 ∘ x) ↔ φ.Realize x)
      FirstOrder.Language.ElementaryEmbedding.map_formula'._autoParam},
  { toFun := toFun, map_formula' := map_formula' } = { toFun := toFun_1, map_formula' := map_formula'_1 } →
    toFun = toFun_1
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_map_piCurry : ∀ {ι : Type u_3} {κ : ι → Type u_4} {X : (i : ι) → κ i → Type u_5} {mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)}
  (μ : (i : ι) → (j : κ i) → MeasureTheory.Measure (X i j))
  [hμ : ∀ (i : ι) (j : κ i), MeasureTheory.IsProbabilityMeasure (μ i j)],
  MeasureTheory.Measure.map (⇑(MeasurableEquiv.piCurry X)) (MeasureTheory.Measure.infinitePi fun p => μ p.fst p.snd) =
    MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.infinitePi fun j => μ i j
-- Mathlib.RingTheory.Ideal.GoingDown
Ideal.exists_ideal_le_liesOver_of_le : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.HasGoingDown R S] {p q : Ideal R} [p.IsPrime] [q.IsPrime] (Q : Ideal S) [Q.IsPrime] [Q.LiesOver q],
  p ≤ q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.toIsometry_hom_leftUnitor : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] {M : QuadraticModuleCat R},
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom =
    M.form.tensorLId.toIsometry
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.rightHomologyData_p : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k)
  (hk' : c'.next j' = k') (h : (K.sc' i j k).RightHomologyData),
  (HomologicalComplex.extend.rightHomologyData K e hj' hi hi' hk hk' h).p =
    CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom h.p
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.preimage_symm : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  Set.preimage ⇑h.symm = Set.image ⇑h
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.instIterator.match_3.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        (it : Std.IterM m β) →
          (motive : it.internalState.inner.Step → Sort u_3) →
            (x : it.internalState.inner.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
                      motive ⟨Std.IterStep.yield it' out, h⟩) →
                ((it' : Std.IterM m β) →
                    (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) →
                      motive ⟨Std.IterStep.skip it', h⟩) →
                  ((h : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) →
                    motive x
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If a family is affinely independent, the infimum of the affine spans of points indexed by two
subsets equals the affine span of points indexed by the intersection of those subsets, if the
underlying ring is nontrivial.  -/
AffineIndependent.inf_affineSpan_eq_affineSpan_inter : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P},
  AffineIndependent k p →
    ∀ (s₁ s₂ : Set ι), affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂) = affineSpan k (p '' (s₁ ∩ s₂))
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.ofNat_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ)
  [inst_3 : n.AtLeastTwo] (m : M), (OfNat.ofNat n) m = OfNat.ofNat n • m
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
/-- a bijection from the type (II) simplices to the type (I) simplices  -/
SSet.Subcomplex.Pairing.p : {X : SSet} → {A : X.Subcomplex} → (self : A.Pairing) → ↑self.II ≃ ↑self.I
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.inverseAssociator_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (x x_1 : C × D × E) (f : x ⟶ x_1),
  (CategoryTheory.prod.inverseAssociator C D E).map f =
    CategoryTheory.Prod.mkHom (CategoryTheory.Prod.mkHom f.1 f.2.1) f.2.2
-- Mathlib.Data.Int.ModEq
Int.add_modulus_modEq_iff : ∀ {n a b : ℤ}, a + n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
/-- Any two transcendence bases of a domain `A` have the same cardinality.
May fail if `A` is not a domain; see https://mathoverflow.net/a/144580.  -/
IsTranscendenceBasis.lift_cardinalMk_eq : ∀ {ι : Type u} {ι' : Type u'} {R : Type u_1} {A : Type w} {x : ι → A} {y : ι' → A} [inst : CommRing R]
  [inst_1 : CommRing A] [inst_2 : Algebra R A] [Nontrivial R] [NoZeroDivisors A],
  IsTranscendenceBasis R x →
    IsTranscendenceBasis R y → Cardinal.lift.{u', u} (Cardinal.mk ι) = Cardinal.lift.{u, u'} (Cardinal.mk ι')
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
LinearMap.map_finsupp_linearCombination : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₗ[R] N) {ι : Type u_4} {g : ι → M} (l : ι →₀ R),
  f ((Finsupp.linearCombination R g) l) = (Finsupp.linearCombination R (⇑f ∘ g)) l
-- Mathlib.Data.Nat.Choose.Bounds
Nat.choose_le_two_pow : ∀ (n k : ℕ), n.choose k ≤ 2 ^ n
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftBindFunction.id : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m],
  Std.Internal.LawfulMonadLiftBindFunction fun x x_1 f x_2 => f x_2.run
-- Mathlib.Data.List.Perm.Subperm
List.subperm_cons_self : ∀ {α : Type u_1} {l : List α} {a : α}, l.Subperm (a :: l)
-- Mathlib.RingTheory.Norm.Basic
Algebra.norm_eq_zero_iff_of_basis : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {ι : Type w} [Finite ι]
  [IsDomain R] [IsDomain S] (b : Module.Basis ι R S) {x : S}, (Algebra.norm R) x = 0 ↔ x = 0
-- Mathlib.Algebra.GCDMonoid.Basic
/-- **Alias** of `dvd_lcm_of_dvd_left`. -/
Dvd.dvd.lcm_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ lcm b c
-- Mathlib.Analysis.Analytic.Constructions
/-- Finite sums of analytic functions are analytic  -/
Finset.analyticOn_sum : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {f : α → E → F} {s : Set E} (N : Finset α), (∀ n ∈ N, AnalyticOn 𝕜 (f n) s) → AnalyticOn 𝕜 (∑ n ∈ N, f n) s
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRec_one : ∀ {motive : ℕ → Sort u} (zero : motive 0) (bit : (b : Bool) → (n : ℕ) → motive n → motive (Nat.bit b n)),
  Nat.binaryRec zero bit 1 = bit true 0 zero
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
/-- Given a box `I` in `ℝⁿ`, a function `r : ℝⁿ → (0, ∞)`, and a prepartition `π` of `I`, there
exists a tagged prepartition `π'` of `I` such that

* each box of `π'` is included in some box of `π`;
* `π'` is a Henstock partition;
* `π'` is subordinate to `r`;
* `π'` covers exactly the same part of `I` as `π`;
* the distortion of `π'` is equal to the distortion of `π`.
 -/
BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (r : (ι → ℝ) → ↑(Set.Ioi 0))
  (π : BoxIntegral.Prepartition I),
  ∃ π', π'.toPrepartition ≤ π ∧ π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion
-- Init.Core
Sigma.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)] (fst : α) (snd : β fst),
  sizeOf ⟨fst, snd⟩ = 1 + sizeOf fst + sizeOf snd
-- Mathlib.Topology.Maps.Proper.Basic
/-- A proper map is closed.  -/
IsProperMap.isClosedMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsProperMap f → IsClosedMap f
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.instInhabitedOrdSet : {a : Type} → {a_1 : Hashable a} → {a_2 : BEq a} → Inhabited (Lean.Meta.Try.Collector.OrdSet a)
-- Mathlib.Data.Nat.Nth
Nat.nth_strictMono : ∀ {p : ℕ → Prop}, (Set.ofPred p).Infinite → StrictMono (Nat.nth p)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyι_descOpcycles_eq_zero_of_boundary : ∀ {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] {A : C}
  (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) {i' : ι} (x : K.X i' ⟶ A)
  (hx : k = CategoryTheory.CategoryStruct.comp (K.d i i') x),
  CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.descOpcycles k j hj ⋯) = 0
-- Mathlib.CategoryTheory.Monoidal.End
/-- If `m ⊗ n ≅ 𝟙_M` and `n ⊗ m ≅ 𝟙_M` (subject to some commuting constraints),
then `F.obj m` and `F.obj n` forms a self-equivalence of `C`.  -/
CategoryTheory.equivOfTensorIsoUnit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} M] →
        [inst_2 : CategoryTheory.MonoidalCategory M] →
          (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) →
            (m n : M) →
              (h₁ :
                  CategoryTheory.MonoidalCategoryStruct.tensorObj m n ≅
                    CategoryTheory.MonoidalCategoryStruct.tensorUnit M) →
                (h₂ :
                    CategoryTheory.MonoidalCategoryStruct.tensorObj n m ≅
                      CategoryTheory.MonoidalCategoryStruct.tensorUnit M) →
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight h₁.hom m)
                        (CategoryTheory.MonoidalCategoryStruct.leftUnitor m).hom =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator m n m).hom
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft m h₂.hom)
                          (CategoryTheory.MonoidalCategoryStruct.rightUnitor m).hom) →
                    [F.Monoidal] → C ≌ C
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.instNNRatCast : {α : Type u_1} → [inst : Semifield α] → [inst_1 : LinearOrder α] → [IsStrictOrderedRing α] → NNRatCast { x // 0 ≤ x }
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_nndist_eq_of_L2 : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x y : WithLp 2 (α × β)), nndist x y = NNReal.sqrt (nndist x.fst y.fst ^ 2 + nndist x.snd y.snd ^ 2)
-- Mathlib.Data.Nat.Cast.SetInterval
Nat.image_cast_int_Ioc : ∀ (a b : ℕ), Nat.cast '' Set.Ioc a b = Set.Ioc ↑a ↑b
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.mk.inj : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} {inst : SMul M X} {Y : Type u_6} {inst_1 : SMul N Y}
  {toFun : X → Y} {map_smul' : ∀ (m : M) (x : X), toFun (m • x) = φ m • toFun x} {toFun_1 : X → Y}
  {map_smul'_1 : ∀ (m : M) (x : X), toFun_1 (m • x) = φ m • toFun_1 x},
  { toFun := toFun, map_smul' := map_smul' } = { toFun := toFun_1, map_smul' := map_smul'_1 } → toFun = toFun_1
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.size_nil : ∀ {α : Type u_1}, Ordnode.nil.size = 0
-- Mathlib.Order.WellFoundedSet
/-- `Set.IsWF.min` returns a minimal element of a nonempty well-founded set.  -/
Set.IsWF.min : {α : Type u_2} → [inst : Preorder α] → {s : Set α} → s.IsWF → s.Nonempty → α
-- Mathlib.Algebra.GroupWithZero.Action.Defs
DistribSMul.mk : {M : Type u_12} →
  {A : Type u_13} →
    [inst : AddZeroClass A] →
      [toSMulZeroClass : SMulZeroClass M A] → (∀ (a : M) (x y : A), a • (x + y) = a • x + a • y) → DistribSMul M A
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- The canonical isomorphism `(F.postcomp G).postcomp G' ≅ F.postcomp (G ⋙ G')`.  -/
CategoryTheory.SingleFunctors.postcompPostcompIso : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      {E' : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} E'] →
                {A : Type u_5} →
                  [inst_4 : AddMonoid A] →
                    [inst_5 : CategoryTheory.HasShift D A] →
                      [inst_6 : CategoryTheory.HasShift E A] →
                        [inst_7 : CategoryTheory.HasShift E' A] →
                          (F : CategoryTheory.SingleFunctors C D A) →
                            (G : CategoryTheory.Functor D E) →
                              (G' : CategoryTheory.Functor E E') →
                                [inst_8 : G.CommShift A] →
                                  [inst_9 : G'.CommShift A] → (F.postcomp G).postcomp G' ≅ F.postcomp (G.comp G')
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H1Iso_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.π A 1) (groupHomology.H1Iso A).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ A).hom
      (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.π
-- Mathlib.Algebra.Category.GrpWithZero
/-- Constructs an isomorphism of groups with zero from a group isomorphism between them.  -/
GrpWithZero.Iso.mk : {α β : GrpWithZero} → α.carrier ≃* β.carrier → (α ≅ β)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- Transfer creation of finite limits along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.createsFiniteLimitsOfNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} →
          {h : F ≅ G} → [CategoryTheory.Limits.CreatesFiniteLimits F] → CategoryTheory.Limits.CreatesFiniteLimits G
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneUnopOfCoconeEquiv_functor_map_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} {Y X : (CategoryTheory.Limits.Cocone F)ᵒᵖ} (f : Y ⟶ X),
  (CategoryTheory.Limits.coneUnopOfCoconeEquiv.functor.map f).hom = f.unop.hom.unop
-- Std.Data.HashMap.Raw
/-- Creates a hash map from a list of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofList`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.  -/
Std.HashMap.Raw.unitOfList : {α : Type u} → [BEq α] → [Hashable α] → List α → Std.HashMap.Raw α Unit
-- Mathlib.Order.SuccPred.Limit
WithTop.isSuccPrelimit_iff : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] {x : WithTop α},
  Order.IsSuccPrelimit x ↔ x = ⊤ ∨ ∃ y, x = ↑y ∧ Order.IsSuccPrelimit y
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A fully faithful functor reflects colimits.  -/
CategoryTheory.Limits.fullyFaithful_reflectsColimits : ∀ {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.Full] [F.Faithful],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lt_iSup_add_one_iff : ∀ {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι], a < ⨆ i, f i + 1 ↔ ∃ i, a ≤ f i
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.mul_toMatrix'_mul : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} {o : Type u_6} [inst_1 : Fintype n] [inst_2 : Fintype o]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq o] (B : LinearMap.BilinForm R₁ (n → R₁)) (M : Matrix o n R₁)
  (N : Matrix n o R₁),
  M * LinearMap.BilinForm.toMatrix' B * N =
    LinearMap.BilinForm.toMatrix' (B.comp (Matrix.toLin' M.transpose) (Matrix.toLin' N))
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.notValue.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.instFaithfulMonForget₂Mon : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], (CategoryTheory.CommMon.forget₂Mon C).Faithful
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_eraseKey_eq_of_beq_maxKey!_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (k == Std.Internal.List.maxKey! l) = false →
          Std.Internal.List.maxKey! (Std.Internal.List.eraseKey k l) = Std.Internal.List.maxKey! l
-- Init.Data.Ord.Basic
/-- Checks whether the ordering is not `eq`.
 -/
Ordering.isNe : Ordering → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.comp_differentiableAt_iff : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G},
  DifferentiableAt 𝕜 (⇑iso ∘ f) x ↔ DifferentiableAt 𝕜 f x
-- Std.Http.Data.Request
/-- The request line information (`method`, `version`, and request-target `uri`).
 -/
Std.Http.Request.line : {t : Type} → Std.Http.Request t → Std.Http.Request.Head
-- Mathlib.MeasureTheory.Integral.Prod
/-- Symmetric version of **Fubini's Theorem**: For integrable functions on `α × β`,
the Bochner integral of `f` is equal to the iterated Bochner integral.
This version has the integrals on the right-hand side in the other order.  -/
MeasureTheory.integral_prod_symm : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] (f : α × β → E),
  MeasureTheory.Integrable f (μ.prod ν) → ∫ (z : α × β), f z ∂μ.prod ν = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_eq_top_iff : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] {f : G →+ M}, f.ker = ⊤ ↔ f = 0
-- Mathlib.MeasureTheory.Measure.Decomposition.Hahn
MeasureTheory.IsHahnDecomposition.mk : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s →
    μ.restrict s ≤ ν.restrict s → ν.restrict sᶜ ≤ μ.restrict sᶜ → MeasureTheory.IsHahnDecomposition μ ν s
-- Mathlib.NumberTheory.Rayleigh
/-- In the Beatty sequence for real number `r`, the `k`th term is `⌊k * r⌋`.  -/
beattySeq : ℝ → ℤ → ℤ
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- If `P` lies over `p`, then `Localization.AtPrime P` is an algebra over `Localization.AtPrime p`.
This is not an instance for performance reasons and to avoid diamonds in the situation where the top
ring is already an algebra over `Localization.AtPrime p` (e.g., this happens for `Ideal.Fiber`).  -/
Localization.AtPrime.algebraOfLiesOver : {A : Type u_4} →
  {B : Type u_5} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] →
        [inst_2 : Algebra A B] →
          (p : Ideal A) →
            [inst_3 : p.IsPrime] →
              (P : Ideal B) →
                [inst_4 : P.IsPrime] → [P.LiesOver p] → Algebra (Localization.AtPrime p) (Localization.AtPrime P)
-- Lean.Meta.LitValues
/-- Check if an expression is an array literal
(i.e. `List.toArray` applied to a nested chain of `List.cons`, ending at a `List.nil`),
returning the array of `Expr` values.
 -/
Lean.Meta.getArrayLit? : Lean.Expr → Lean.MetaM (Option (Array Lean.Expr))
-- Lean.Parser.Extension
/-- If the parsing stack is of the form `#[.., openCommand]`, we process the open command, and execute `p`  -/
Lean.Parser.withOpenFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffineLift_neg : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} (P : W.Point), (-P).toAffineLift = -P.toAffineLift
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.getD a fallback =
    if h : compare k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.getD a fallback
-- Lean.Parser.Command
Lean.Parser.Command.declValSimple : Lean.Parser.Parser
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryLE : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        (k : α) →
          (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.Ordered → (∃ a ∈ t, (compare a k).isLE = true) → α × β
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.map_iInf_comap : ∀ {α : Type u_1} {ι : Sort u_2} {β : Type u_3} [Nonempty ι] {f : α → β} (m : ι → MeasureTheory.OuterMeasure β),
  (MeasureTheory.OuterMeasure.map f) (⨅ i, (MeasureTheory.OuterMeasure.comap f) (m i)) =
    ⨅ i, (MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) (m i))
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instCompletelyNormalSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [CompletelyNormalSpace M], CompletelyNormalSpace Mᵈᵐᵃ
-- Mathlib.Topology.Closure
Finset.closure_biUnion : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type u_1} (s : Finset ι) (f : ι → Set X),
  closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)
-- Mathlib.Data.Semiquot
Semiquot.instInhabited : {α : Type u_1} → [Inhabited α] → Inhabited (Semiquot α)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.embDomainAlgHom_apply_coeff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommSemiring R] {A : Type u_6} [inst_4 : Semiring A] [inst_5 : Algebra R A] {Γ' : Type u_7}
  [inst_6 : AddCommMonoid Γ'] [inst_7 : PartialOrder Γ'] [inst_8 : IsOrderedCancelAddMonoid Γ'] (f : Γ →+ Γ')
  (hfi : Function.Injective ⇑f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') (a : HahnSeries Γ A) (b : Γ'),
  ((HahnSeries.embDomainAlgHom f hfi hf) a).coeff b =
    if h : b ∈ ⇑f '' a.support then a.coeff (Classical.choose ⋯) else 0