mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.mk.injEq : ∀ {𝕜 : 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] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} (toPartialEquiv : PartialEquiv M N)
  (open_source : IsOpen toPartialEquiv.source) (open_target : IsOpen toPartialEquiv.target)
  (contMDiffOn_toFun : ContMDiffOn I J n (↑toPartialEquiv) toPartialEquiv.source)
  (contMDiffOn_invFun : ContMDiffOn J I n toPartialEquiv.invFun toPartialEquiv.target)
  (toPartialEquiv_1 : PartialEquiv M N) (open_source_1 : IsOpen toPartialEquiv_1.source)
  (open_target_1 : IsOpen toPartialEquiv_1.target)
  (contMDiffOn_toFun_1 : ContMDiffOn I J n (↑toPartialEquiv_1) toPartialEquiv_1.source)
  (contMDiffOn_invFun_1 : ContMDiffOn J I n toPartialEquiv_1.invFun toPartialEquiv_1.target),
  ({ toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
        contMDiffOn_toFun := contMDiffOn_toFun, contMDiffOn_invFun := contMDiffOn_invFun } =
      { toPartialEquiv := toPartialEquiv_1, open_source := open_source_1, open_target := open_target_1,
        contMDiffOn_toFun := contMDiffOn_toFun_1, contMDiffOn_invFun := contMDiffOn_invFun_1 }) =
    (toPartialEquiv = toPartialEquiv_1)
-- Init.Data.Iterators.Basic
Std.IterStep.yield.inj : ∀ {α : Sort u_1} {β : Sort u_2} {it : α} {out : β} {it_1 : α} {out_1 : β},
  Std.IterStep.yield it out = Std.IterStep.yield it_1 out_1 → it = it_1 ∧ out = out_1
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot : ∀ {X : AlgebraicGeometry.Scheme} [hX : AlgebraicGeometry.IsReduced X] {U : X.Opens}
  (s : ↑(X.presheaf.obj (Opposite.op U))), X.basicOpen s = ⊥ → s = 0
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.totalDegree_truncTotal_lt : ∀ {σ : Type u_1} {R : Type u_2} {n : ℕ} [inst : Finite σ] [inst_1 : CommSemiring R] (p : MvPowerSeries σ R),
  n ≠ 0 → ((MvPowerSeries.truncTotal n) p).totalDegree < n
-- Mathlib.Order.Filter.Extr
IsMinOn.neg : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f : α → β} {a : α}
  {s : Set α}, IsMinOn f s a → IsMaxOn (fun x => -f x) s a
-- Init.Data.UInt.Lemmas
UInt16.toUSize_ofNat : ∀ {n : ℕ}, n < 65536 → (OfNat.ofNat n).toUSize = OfNat.ofNat n
-- Init.Data.UInt.Bitwise
UInt16.shiftLeft_add_of_toNat_lt : ∀ {a b c : UInt16}, b.toNat + c.toNat < 16 → a <<< (b + c) = a <<< b <<< c
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.eval.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N],
  AddMonoidHom.eval = (AddMonoidHom.id (M →+ N)).flip
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.map_one : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.MonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal], F.map 1 = 1
-- Mathlib.Order.Interval.Set.Basic
Set.nonempty_Icc_subtype : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → Nonempty ↑(Set.Icc a b)
-- Mathlib.Data.Multiset.Sort
Multiset.instRepr : {α : Type u_1} → [Repr α] → Repr (Multiset α)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.ConvolutionExistsAt.distrib_add : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : Monoid 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] [T2Space F]
  [ContinuousAdd F] {f : M → E} {g g' : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F),
  DiscreteConvolution.ConvolutionExistsAt L f g x →
    DiscreteConvolution.ConvolutionExistsAt L f g' x →
      DiscreteConvolution.convolution L f (g + g') x =
        DiscreteConvolution.convolution L f g x + DiscreteConvolution.convolution L f g' x
-- Init.Data.Vector.Lemmas
Vector.insertIdx_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {h : xs.size = n} {i : ℕ} {x : α} (h' : i ≤ n),
  (Vector.mk xs h).insertIdx i x h' = Vector.mk (xs.insertIdx i x ⋯) ⋯
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.π_comp_colimitUnopIsoOpLimit_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : Jᵒᵖ) {Z : C}
  (h : CategoryTheory.Limits.colimit F.unop ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j).unop
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitUnopIsoOpLimit F).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.unop (Opposite.unop j)) h
-- Init.Data.String.Lemmas.Basic
String.sliceFrom_slice : ∀ {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} {p : (s.slice p₁ p₂ h).Pos},
  (s.slice p₁ p₂ h).sliceFrom p = s.slice (String.Pos.ofSlice p) p₂ ⋯
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.normalizedMooreComplex.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  AlgebraicTopology.normalizedMooreComplex C =
    { obj := AlgebraicTopology.NormalizedMooreComplex.obj,
      map := fun {X Y} f => AlgebraicTopology.NormalizedMooreComplex.map f, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Nonneg.instNonUnitalIsometricContinuousFunctionalCalculus : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : PartialOrder A] [inst_2 : StarRing A] [StarOrderedRing A]
  [inst_4 : NormedSpace ℝ A] [inst_5 : IsScalarTower ℝ A A] [inst_6 : SMulCommClass ℝ A A]
  [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A],
  NonUnitalIsometricContinuousFunctionalCalculus NNReal A fun x => 0 ≤ x
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithTop.decidableLT.match_1.splitter : {α : Type u_1} →
  (motive : WithTop α → WithTop α → Sort u_2) →
    (x x_1 : WithTop α) →
      ((x : WithTop α) → motive x none) →
        ((a : α) → motive none (some a)) → ((a b : α) → motive (some a) (some b)) → motive x x_1
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformly.multipliableLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β], HasProdLocallyUniformly f g → MultipliableLocallyUniformly f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {fallback v : β}, Std.DTreeMap.Raw.Const.getD (t.insert k v) k fallback = v
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.instStarRingId : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → [CompleteSpace E] → StarRing (E →L[𝕜] E)
-- Mathlib.Data.Set.Finite.Lattice
DirectedOn.exists_mem_subset_of_finset_subset_biUnion : ∀ {α : Type u_1} {ι : Type u_2} {f : ι → Set α} {c : Set ι},
  c.Nonempty → DirectedOn (fun i j => f i ⊆ f j) c → ∀ {s : Finset α}, ↑s ⊆ ⋃ i ∈ c, f i → ∃ i ∈ c, ↑s ⊆ f i
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalHorizontalComp_nil_cons : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {f f' g g' h i : C} {α : f ≅ g} {β : f' ≅ g'} {η : g' ⟶ h} {ηs : h ⟶ i}
  {η₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj g g' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj g h}
  {ηs₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj g h ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj g i}
  {η₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj g g' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj g i}
  {η₃ : CategoryTheory.MonoidalCategoryStruct.tensorObj f f' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj g i},
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft g
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl g').hom
          (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl h).hom)) =
      η₁ →
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft g ηs = ηs₁ →
      CategoryTheory.CategoryStruct.comp η₁ ηs₁ = η₂ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorIso α β).hom η₂ = η₃ →
          CategoryTheory.MonoidalCategoryStruct.tensorHom α.hom
              (CategoryTheory.CategoryStruct.comp β.hom (CategoryTheory.CategoryStruct.comp η ηs)) =
            η₃
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.liftFromUnderComp_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {X : C}
  {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {F : CategoryTheory.Functor C D}
  (x : CategoryTheory.WithInitial J),
  CategoryTheory.WithInitial.liftFromUnderComp.inv.app x =
    match x with
    | CategoryTheory.WithInitial.star =>
      CategoryTheory.CategoryStruct.id
        (((CategoryTheory.WithInitial.liftFromUnder.obj K).comp F).obj CategoryTheory.WithInitial.star)
    | CategoryTheory.WithInitial.of a =>
      CategoryTheory.CategoryStruct.id
        (((CategoryTheory.WithInitial.liftFromUnder.obj K).comp F).obj (CategoryTheory.WithInitial.of a))
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.instDecidableEqHom.decEq : {a a_1 : CategoryTheory.Limits.WalkingReflexivePair} → (x x_1 : a.Hom a_1) → Decidable (x = x_1)
-- Mathlib.Logic.Equiv.Defs
Equiv.symm_eq_iff_trans_eq_refl : ∀ {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α}, f.symm = g ↔ f.trans g = Equiv.refl α
-- Mathlib.Data.Set.Function
Set.InjOn.iterate : ∀ {α : Type u_1} {f : α → α} {s : Set α}, Set.InjOn f s → Set.MapsTo f s s → ∀ (n : ℕ), Set.InjOn f^[n] s
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.equiv_mk0 : ∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] [inst_5 : IsDedekindDomain R] (I : ↥(nonZeroDivisors (Ideal R))),
  (ClassGroup.equiv K) (ClassGroup.mk0 I) = (QuotientGroup.mk' (toPrincipalIdeal R K).range) ((FractionalIdeal.mk0 K) I)
-- Lean.Parser.Term
Lean.Parser.Term.suffices.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Quaternion
Quaternion.im_ratCast : ∀ {R : Type u_1} [inst : Field R] (q : ℚ), (↑q).im = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mrangeRestrict.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] {N : Type u_5} [inst_1 : MulOneClass N] (f : M →* N),
  f.mrangeRestrict = f.codRestrict (MonoidHom.mrange f) ⋯
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.liftEquiv.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P],
  AddMonoid.Coprod.liftEquiv =
    { toFun := fun fg => AddMonoid.Coprod.lift fg.1 fg.2,
      invFun := fun f => (f.comp AddMonoid.Coprod.inl, f.comp AddMonoid.Coprod.inr), left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mul_right_coe_nonZeroDivisors_eq_zero_iff : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x : M₀} {c : ↥(nonZeroDivisors M₀)}, x * ↑c = 0 ↔ x = 0
-- Mathlib.Order.Heyting.Basic
himp_inf_distrib : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.length_reverseAux : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk u w),
  (p.reverseAux q).length = p.length + q.length
-- Mathlib.MeasureTheory.Integral.MeanInequalities
ENNReal.lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : ℝ},
  p.HolderConjugate q →
    ∀ {f g : α → ENNReal},
      AEMeasurable f μ →
        AEMeasurable g μ →
          ∫⁻ (a : α), f a * g a ^ (p - 1) ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
ContinuousAlternatingMap.curryLeft_zero : ∀ {𝕜 : 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] {n : ℕ},
  ContinuousAlternatingMap.curryLeft 0 = 0
-- Mathlib.CategoryTheory.Preadditive.Injective.Preserves
/-- See `Functor.injective_obj_of_injective` for a variant taking `Injective X` as an explicit
argument.  -/
CategoryTheory.Functor.injective_obj : ∀ {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.PreservesInjectiveObjects] (X : C) [CategoryTheory.Injective X],
  CategoryTheory.Injective (F.obj X)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.le_graph_of_le : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f g : E →ₗ.[R] F}, f ≤ g → f.graph ≤ g.graph
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.continuous_projRestrict : ∀ {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [inst : (i : I) → Decidable (J i)],
  Continuous (Profinite.NobelingProof.ProjRestrict C J)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.basisFun_repr : ∀ (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [inst : Finite ι] [inst_1 : Ring 𝕜] (x : PiLp p fun x => 𝕜) (i : ι),
  ((PiLp.basisFun p 𝕜 ι).repr x) i = x.ofLp i
-- Mathlib.Algebra.GradedMulAction
GradedMonoid.GSMul.mk : {ιA : Type u_1} →
  {ιM : Type u_3} →
    {A : ιA → Type u_4} →
      {M : ιM → Type u_5} →
        [inst : VAdd ιA ιM] → ({i : ιA} → {j : ιM} → A i → M j → M (i +ᵥ j)) → GradedMonoid.GSMul A M
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.DTreeMap.Raw.Const.entryAtIdxD : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → ℕ → α × β → α × β
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
/-- A variant of `norm_sub_mul_self_le` for non-unital algebras that passes to the unitization.  -/
CStarAlgebra.norm_sub_mul_self_le_of_inr : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {x y : A} (z : A),
  0 ≤ x → x ≤ y → ‖y‖ ≤ 1 → ∀ {c : ℝ}, 0 ≤ c → ‖star ↑z * (1 - ↑x) * ↑z‖ ≤ c ^ 2 → ‖z - y * z‖ ≤ c
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.reassign : Array Lean.Elab.Term.Do.Var → Lean.Syntax → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_union_of_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, k ∈ t₁ → k ∈ t₁ ∪ t₂
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- The two-variable Jacobi theta function is periodic in `τ` with period 2.  -/
jacobiTheta₂_add_right : ∀ (z τ : ℂ), jacobiTheta₂ z (τ + 2) = jacobiTheta₂ z τ
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Algebra.IsIntegral.tensorProduct : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [int : Algebra.IsIntegral R B],
  Algebra.IsIntegral A (TensorProduct R A B)
-- Aesop.Rule.Name
Aesop.DisplayRuleName.ruleName : Aesop.RuleName → Aesop.DisplayRuleName
-- Mathlib.Order.Defs.Prop
le_Prop_eq : (fun x1 x2 => x1 ≤ x2) = fun x1 x2 => x1 → x2
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.analyticAt_uncurry_of_linear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)) {x : ((i : ι) → Em i) × G},
  AnalyticAt 𝕜 (fun p => (f p.1) p.2) x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  k ∈ Std.DTreeMap.Const.unitOfList l cmp ↔ l.contains k = true
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.instNontrivialOfNonempty : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [Nonempty α] [Nontrivial β],
  Nontrivial C(α, β)
-- Mathlib.Topology.Algebra.Group.Basic
Inseparable.zsmul : ∀ {G : Type u_1} [inst : SubNegMonoid G] [inst_1 : TopologicalSpace G] [ContinuousAdd G] [ContinuousNeg G] {x y : G},
  Inseparable x y → ∀ (m : ℤ), Inseparable (m • x) (m • y)
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.beq.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Batteries.AssocList α β → Batteries.AssocList α β → Sort u_3) →
      (x x_1 : Batteries.AssocList α β) →
        (Unit → motive Batteries.AssocList.nil Batteries.AssocList.nil) →
          ((key : α) →
              (value : β) →
                (tail : Batteries.AssocList α β) →
                  motive (Batteries.AssocList.cons key value tail) Batteries.AssocList.nil) →
            ((key : α) →
                (value : β) →
                  (tail : Batteries.AssocList α β) →
                    motive Batteries.AssocList.nil (Batteries.AssocList.cons key value tail)) →
              ((a : α) →
                  (b : β) →
                    (t : Batteries.AssocList α β) →
                      (a' : α) →
                        (b' : β) →
                          (t' : Batteries.AssocList α β) →
                            motive (Batteries.AssocList.cons a b t) (Batteries.AssocList.cons a' b' t')) →
                motive x x_1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.subThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option (Option Lean.Expr)
-- Lean.Elab.DeprecatedArg
Lean.Elab.DeprecatedArgEntry.declName : Lean.Elab.DeprecatedArgEntry → Lean.Name
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- a colimit cofan which gives the coproduct of the object `A (π i)`  -/
HomotopicalAlgebra.AttachCells.cofan₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} →
            {f : X₁ ⟶ X₂} →
              (self : HomotopicalAlgebra.AttachCells g f) → CategoryTheory.Limits.Cofan fun i => A (self.π i)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_pow : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : ContinuousMul M] (x : M) (n : ℕ),
  SeparationQuotient.mk (x ^ n) = SeparationQuotient.mk x ^ n
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.instCoeOutAlgEquiv : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → CoeOut (A ≃ₐc[R] B) (A ≃ₐ[R] B)
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a normed group from a multiplication-invariant pseudodistance.  -/
NormedGroup.ofMulDist' : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : Group E] →
      [inst_2 : MetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 1 x) → (∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y) → NormedGroup E
-- Mathlib.MeasureTheory.VectorMeasure.AddContent
/-- Consider an additive content on a semi-ring of sets whose finite unions are dense. Assume that
it is dominated by a finite positive measure. Then it extends to a countably additive
vector measure.  -/
MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_dense : ∀ {α : Type u_1} {hα : MeasurableSpace α} {E : Type u_2} [inst : NormedAddCommGroup E] [CompleteSpace E]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {C : Set (Set α)} {m : MeasureTheory.AddContent E C},
  MeasureTheory.IsSetSemiring C →
    (∀ s ∈ C, MeasurableSet s) →
      (∀ s ∈ C, ‖m s‖ₑ ≤ μ s) →
        (∀ (t : Set α) (ε : ENNReal), MeasurableSet t → 0 < ε → ∃ s ∈ supClosure C, μ (symmDiff s t) < ε) →
          ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.comp_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} [CategoryTheory.IsIso f]
  [CategoryTheory.IsIso h], CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f h)
-- Lean.Elab.Command
Lean.Elab.Command.instMonadCommandElabM : Monad Lean.Elab.Command.CommandElabM
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.inc.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (n : ℕ) (check persistent : Bool)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_11) (fvarId_1 : Lean.FVarId)
  (n_1 : ℕ) (check_1 persistent_1 : Bool)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_11),
  (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h =
      Lean.Compiler.LCNF.CodeDecl.inc fvarId_1 n_1 check_1 persistent_1 h_1) =
    (fvarId = fvarId_1 ∧ n = n_1 ∧ check = check_1 ∧ persistent = persistent_1)
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.span_singleton_lt_span_singleton : ∀ {α : Type u} [inst : CommSemiring α] [IsDomain α] {x y : α}, Ideal.span {x} < Ideal.span {y} ↔ DvdNotUnit y x
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.instOrdOffset : Ord Std.Time.TimeZone.Offset
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.monodromy_refl : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {x : X}, cov.monodromy (Path.Homotopic.Quotient.refl x) = id
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.has_kernels : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.NonPreadditiveAbelian C],
  CategoryTheory.Limits.HasKernels C
-- Mathlib.Algebra.Order.Ring.Abs
abs_dvd : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] (a b : α), |a| ∣ b ↔ a ∣ b
-- Mathlib.Data.Set.Operations
Set.mem_ofPred_eq : ∀ {α : Type u} {x : α} {p : α → Prop}, (x ∈ {y | p y}) = p x
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- The zeta function of the incidence algebra is the function that assigns 1 to every nonempty
interval, convolution with this function sums functions over intervals.  -/
IncidenceAlgebra.zeta : (𝕜 : Type u_2) → {α : Type u_5} → [inst : Zero 𝕜] → [One 𝕜] → [inst_2 : LE α] → [DecidableLE α] → IncidenceAlgebra 𝕜 α