mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonRenameOptions.toJson : Lean.Lsp.RenameOptions → Lean.Json
-- Mathlib.Analysis.SpecialFunctions.Sqrt
HasFDerivWithinAt.sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E}
  {f' : StrongDual ℝ E},
  HasFDerivWithinAt f f' s x → f x ≠ 0 → HasFDerivWithinAt (fun y => √(f y)) ((1 / (2 * √(f x))) • f') s x
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  (c : ComplexShape ι),
  (CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C c).functor =
    CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
MeasureTheory.memLp_prodLp_iff : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p q : ENNReal} [inst : Fact (1 ≤ q)]
  {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  {f : X → WithLp q (E × F)},
  MeasureTheory.MemLp f p μ ↔
    MeasureTheory.MemLp (fun x => (f x).fst) p μ ∧ MeasureTheory.MemLp (fun x => (f x).snd) p μ
-- Mathlib.MeasureTheory.Integral.Lebesgue.Sub
MeasureTheory.lintegral_sub_le' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (f g : α → ENNReal),
  AEMeasurable f μ → ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.transPartialEquiv_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f' : PartialEquiv β γ) (a : γ),
  ↑(e.transPartialEquiv f').symm a = e.symm (↑f'.symm a)
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRelO.eq_1 : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (C : Stream'.WSeq α → Stream'.WSeq β → Prop),
  Stream'.WSeq.LiftRelO R C none none = True
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange_def : ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β₁ i)]
  [inst_2 : (i : ι) → Zero (β₂ i)] [inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)] {f : (i : ι) → β₁ i → β₂ i}
  {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i},
  DFinsupp.mapRange f hf g = DFinsupp.mk g.support fun i => f (↑i) (g ↑i)
-- Mathlib.Data.Finsupp.Defs
Finsupp.coe_equivFunOnFinite_symm : ∀ {M : Type u_4} [inst : Zero M] {α : Type u_9} [inst_1 : Finite α] (f : α → M), ⇑(Finsupp.equivFunOnFinite.symm f) = f
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E / F` is a separable field extension of exponential characteristic `q`, then
`F(S) = F(S ^ q)` for any subset `S` of `E`.  -/
IntermediateField.adjoin_eq_adjoin_pow_expChar_of_isSeparable' : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E]
  (S : Set E) (q : ℕ) [ExpChar F q], IntermediateField.adjoin F S = IntermediateField.adjoin F ((fun x => x ^ q) '' S)
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_range_left : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {f : G ⧸ H → G},
  (∀ (q : G ⧸ H), ↑(f q) = q) → Subgroup.IsComplement (Set.range f) ↑H
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_intCast_mul : ∀ (x : NNReal) (n : ℤ) (z : ℝ), x ^ (↑n * z) = (x ^ n) ^ z
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.encard_smul_set : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (a : G) (s : Set α), (a • s).encard = s.encard
-- Mathlib.Order.Fin.Tuple
finSuccAboveOrderIso_apply : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), (finSuccAboveOrderIso p) i = ⟨p.succAbove i, ⋯⟩
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoAdd'_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {a b c : A} (h : a + b = c)
  (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) (X : C),
  (CategoryTheory.Functor.CommShift.isoAdd' h e₁ e₂).hom.app X =
    CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd' C a b c h).hom.app X))
      (CategoryTheory.CategoryStruct.comp (e₂.hom.app ((CategoryTheory.shiftFunctor C a).obj X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.hom.app X))
          ((CategoryTheory.shiftFunctorAdd' D a b c h).inv.app (F.obj X))))
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instNonUnitalSemiringOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : NonUnitalSemiring Mᵃᵒᵖ], DomAddAct.instNonUnitalSemiringOfAddOpposite = inst
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors_zero : ArithmeticFunction.cardFactors 0 = 0
-- Mathlib.Analysis.Calculus.Implicit
/-- Implicit function `g` defined by `f (g z y) = z`.  -/
HasStrictFDerivAt.implicitFunctionOfComplemented : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [CompleteSpace F] →
                    (f : E → F) →
                      (f' : E →L[𝕜] F) →
                        {a : E} →
                          HasStrictFDerivAt f f' a → (↑f').range = ⊤ → (↑f').ker.ClosedComplemented → F → ↥(↑f').ker → E
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_mul_X_eq_monomial : ∀ {R : Type u} {a : R} [inst : Semiring R], Polynomial.C a * Polynomial.X = (Polynomial.monomial 1) a
-- Init.Data.String.Defs
String.exists_eq_ofList : ∀ (s : String), ∃ l, s = String.ofList l
-- Mathlib.Algebra.Lie.Basic
/-- A morphism of Lie algebra modules (denoted as `M →ₗ⁅R,L⁆ N`) is a linear map
which commutes with the action of the Lie algebra.  -/
LieModuleHom : (R : Type u) →
  (L : Type v) →
    (M : Type w) →
      (N : Type w₁) →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [Module R M] → [Module R N] → [LieRingModule L M] → [LieRingModule L N] → Type (max w w₁)
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- In a compactly generated space `X`, a set `s` is open when `s ∩ K` is
open for every open set `K`.  -/
CompactlyGeneratedSpace.isOpen : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactlyGeneratedSpace X] {s : Set X},
  (∀ ⦃K : Set X⦄, IsCompact K → IsOpen (s ∩ K)) → IsOpen s
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_top : ∀ {M : Type u_2} [inst : Add M], ⊤.op = ⊤
-- Mathlib.Algebra.Ring.Semireal.Defs
/-- **Alias** of the reverse direction of `isSemireal_iff_not_isSumSq_neg_one`. -/
IsSemireal.of_not_isSumSq_neg_one : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : One R] [inst_2 : Mul R], ¬IsSumSq (-1) → IsSemireal R
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.mk : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β},
  Set.MapsTo f A B →
    (∀ ⦃s t : Multiset α⦄,
        (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
          (∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
            s.card = n → t.card = n → s.sum = t.sum → (Multiset.map f s).sum = (Multiset.map f t).sum) →
      IsAddFreimanHom n A B f
-- Mathlib.Data.List.Basic
List.infix_flatMap_of_mem : ∀ {α : Type u} {a : α} {as : List α}, a ∈ as → ∀ (f : α → List α), f a <:+: List.flatMap f as
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The morphism of `posSubmonoid`s associated to an algebra map.
This is used in constructing `ValuativeExtension.mapValueGroupWithZero`.  -/
ValuativeExtension.mapPosSubmonoid : (A : Type u_1) →
  (B : Type u_2) →
    [inst : CommSemiring A] →
      [inst_1 : Semiring B] →
        [inst_2 : ValuativeRel A] →
          [inst_3 : ValuativeRel B] →
            [inst_4 : Algebra A B] →
              [ValuativeExtension A B] → ↥(ValuativeRel.posSubmonoid A) →* ↥(ValuativeRel.posSubmonoid B)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
Dense.uniformContinuous_extend : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {s : Set α} {f : ↑s → β}
  [CompleteSpace β] (hs : Dense s), UniformContinuous f → UniformContinuous (hs.extend f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isSome_minKey?_modify_eq_isSome : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Raw.Const.modify t k f).minKey?.isSome = t.minKey?.isSome
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPParens : Lean.Options → Bool
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_iff_isIso_descOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂),
  S₁.g = 0 →
    ∀ (hf₂ : S₂.f = 0),
      S₂.g = 0 → (CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (S₁.descOpcycles φ.τ₂ ⋯))
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelMonoid.toIsCancelMul : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelMonoid α], IsCancelMul α
-- Init.Data.Slice.List.Lemmas
List.mkSlice_roi_eq_mkSlice_rci : ∀ {α : Type u_1} {xs : List α} {lo : ℕ},
  Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rci.Sliceable.mkSlice xs (lo + 1)...*
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_sub_toENNReal : ∀ (r : ENNReal) (n : ℕ∞), ⌊r - ↑n⌋ₑ = ⌊r⌋ₑ - n
-- Mathlib.Probability.BrownianMotion.Basic
/-- A stochastic process is called **Brownian** if its finite-dimensional laws are those
of the Brownian motion, see `IsPreBrownianReal`, and if it has almost-surely continuous paths.  -/
ProbabilityTheory.IsBrownianReal : {Ω : Type u_1} →
  {mΩ : MeasurableSpace Ω} →
    (NNReal → Ω → ℝ) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsBrownianReal._auto_1 → Prop
-- Init.Data.Array.Lemmas
Array.reverse_empty : ∀ {α : Type u_1}, #[].reverse = #[]
-- Mathlib.Topology.Separation.Hausdorff
t2Space_iff_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X], T2Space X ↔ Pairwise fun x y => ∃ U ∈ nhds x, ∃ V ∈ nhds y, Disjoint U V
-- Mathlib.Algebra.Order.Monoid.WithTop
WithTop.isOrderedAddMonoid : ∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α], IsOrderedAddMonoid (WithTop α)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.integrable_exp_mul_of_mem_Icc : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ}
  {a b t : ℝ},
  AEMeasurable X μ → (∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) → MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ
-- Mathlib.Order.SymmDiff
symmDiff_assoc : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b c : α), symmDiff (symmDiff a b) c = symmDiff a (symmDiff b c)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_comp_rev : ∀ {n : ℕ} {α : Sort u_3} (i : Fin (n + 1)) (x : α) (p : Fin n → α),
  i.insertNth x p ∘ Fin.rev = i.rev.insertNth x (p ∘ Fin.rev)
-- Init.Data.SInt.Lemmas
Int8.toInt_div_of_ne_right : ∀ (a b : Int8), b ≠ -1 → (a / b).toInt = a.toInt.tdiv b.toInt
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfSizeFunctorOppositePresheafFiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w, max u v', v', max (max (max u u') v) v', u'} Φ.presheafFiber
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.denoteN.eq_def : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.Poly.denoteN ctx p =
    match p with
    | Lean.Grind.Linarith.Poly.nil => 0
    | Lean.Grind.Linarith.Poly.add k v p =>
      bif decide (k < 0) then 0
      else k.natAbs • Lean.Grind.Linarith.Var.denote ctx v + Lean.Grind.Linarith.Poly.denoteN ctx p
-- Mathlib.CategoryTheory.Limits.Yoneda
/-- The colimit cocone over `coyoneda.obj X`, with cocone point `PUnit`.
 -/
CategoryTheory.Coyoneda.colimitCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (X : Cᵒᵖ) → CategoryTheory.Limits.Cocone (CategoryTheory.coyoneda.obj X)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.binderDefault.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Notation
/-- `a ^^^ b` computes the bitwise XOR of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^^^` in identifiers is `xor`. -/
«term_^^^_» : Lean.TrailingParserDescr
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.instFinitenessRelation : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.Iterators.FinitenessRelation (Std.DTreeMap.Internal.RxoIterator α β) Id
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.hom_id : ∀ {R : Type u} [inst : CommRing R] {A : CommHopfAlgCat R},
  ↑(CommHopfAlgCat.Hom.hom (CategoryTheory.CategoryStruct.id A)) = AlgHom.id R ↑A
-- Mathlib.Algebra.Group.TypeTags.Pointwise
Multiplicative.ofAdd_image_nsmul : ∀ {M : Type u_1} [inst : AddMonoid M] (n : ℕ) (s : Set M),
  ⇑Multiplicative.ofAdd '' (n • s) = (⇑Multiplicative.ofAdd '' s) ^ n
-- Init.Data.String.Pattern.String
String.Slice.Pattern.BackwardSliceSearcher.instBackwardPattern_1 : {pat : String} → String.Slice.Pattern.BackwardPattern pat
-- Mathlib.Data.Multiset.Sum
Multiset.mem_disjSum : ∀ {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} {x : α ⊕ β},
  x ∈ s.disjSum t ↔ (∃ a ∈ s, Sum.inl a = x) ∨ ∃ b ∈ t, Sum.inr b = x
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given a `k`-linear `G`-representation `(A, ρ₁)`, this is the 'internal Hom' functor sending
`(B, ρ₂)` to the representation `Homₖ(A, B)` that maps `g : G` and `f : A →ₗ[k] B` to
`(ρ₂ g) ∘ₗ f ∘ₗ (ρ₁ g⁻¹)`.  -/
Rep.ihom : {k : Type u} →
  [inst : CommRing k] →
    {G : Type v} →
      [inst_1 : Group G] → Rep.{w, u, v} k G → CategoryTheory.Functor (Rep.{u_1, u, v} k G) (Rep.{max w u_1, u, v} k G)
-- Mathlib.Algebra.Order.Group.PosPart
/-- **Alias** of the reverse direction of `negPart_eq_neg`. -/
negPart_of_nonpos : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], a ≤ 0 → a⁻ = -a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.degree_norm_ne_one : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [IsDomain R] (x : W'.CoordinateRing),
  ((Algebra.norm (Polynomial R)) x).degree ≠ 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.tan_add : ∀ {x y : ℂ},
  (((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑Real.pi / 2) ∨
      (∃ k, x = (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑Real.pi / 2) →
    Complex.tan (x + y) = (Complex.tan x + Complex.tan y) / (1 - Complex.tan x * Complex.tan y)
-- Mathlib.Data.Finset.Preimage
Finset.monotone_preimage : ∀ {α : Type u} {β : Type v} {f : α → β} (h : Function.Injective f), Monotone fun s => s.preimage f ⋯
-- Mathlib.Topology.Order.WithTop
WithBot.nhds_coe : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] {r : ι},
  nhds ↑r = Filter.map WithBot.some (nhds r)
-- Mathlib.Data.Set.Lattice
Set.iUnion_sigma' : ∀ {α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (s : (i : α) → γ i → Set β), ⋃ i, ⋃ a, s i a = ⋃ ia, s ia.fst ia.snd
-- Mathlib.Data.Stream.Init
Stream'.interchange : ∀ {α : Type u} {β : Type v} (fs : Stream' (α → β)) (a : α), fs ⊛ Stream'.pure a = (Stream'.pure fun f => f a) ⊛ fs
-- Mathlib.Analysis.Analytic.Uniqueness
/-- If a function `f : 𝕜 → E` has two power series representations at `x`, then the given radii in
which convergence is guaranteed may be interchanged. This can be useful when the formal multilinear
series in one representation has a particularly nice form, but the other has a larger radius.  -/
HasFPowerSeriesOnBall.exchange_radius : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {r₁ r₂ : ENNReal} {x : 𝕜},
  HasFPowerSeriesOnBall f p₁ x r₁ → HasFPowerSeriesOnBall f p₂ x r₂ → HasFPowerSeriesOnBall f p₁ x r₂
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toList_roc : ∀ {m n k : ℤ}, List.map (fun x => x + k) (m<...=n).toList = ((m + k)<...=n + k).toList
-- Mathlib.Algebra.Field.Subfield.Defs
/-- Copy of a subfield with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
Subfield.copy : {K : Type u} → [inst : DivisionRing K] → (S : Subfield K) → (s : Set K) → s = ↑S → Subfield K
-- Mathlib.Topology.Homotopy.HomotopyGroup
Equiv.sumArrowEquivProdArrow.eq_1 : ∀ (α : Type u_9) (β : Type u_10) (γ : Type u_11),
  Equiv.sumArrowEquivProdArrow α β γ =
    { toFun := fun f => (f ∘ Sum.inl, f ∘ Sum.inr), invFun := fun p => Sum.elim p.1 p.2, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- A path of length `m` in an `n + 1`-truncated simplicial set `X` is given by
the data of a `Path₁` structure on the further 1-truncation of `X`.  -/
SSet.Truncated.Path : {n : ℕ} → SSet.Truncated (n + 1) → ℕ → Type u
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
_private.Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace.0.volumePreservingSymmMeasurableEquivToLpProdAux.eq_1 : ∀ (U : Type u_4) (V : Type u_5) [inst : NormedAddCommGroup U] [inst_1 : InnerProductSpace ℝ U]
  [inst_2 : MeasurableSpace U] [inst_3 : BorelSpace U] [inst_4 : FiniteDimensional ℝ U] [inst_5 : NormedAddCommGroup V]
  [inst_6 : InnerProductSpace ℝ V] [inst_7 : MeasurableSpace V] [inst_8 : BorelSpace V]
  [inst_9 : FiniteDimensional ℝ V],
  volumePreservingSymmMeasurableEquivToLpProdAux✝ U V =
    ((LinearIsometryEquiv.withLpProdCongr 2 (stdOrthonormalBasis ℝ U).repr (stdOrthonormalBasis ℝ V).repr).trans
            (PiLp.sumPiLpEquivProdLpPiLp 2 fun x => ℝ).symm).toMeasurableEquiv.trans
      ((MeasurableEquiv.toLp 2 (Fin (Module.finrank ℝ U) ⊕ Fin (Module.finrank ℝ V) → ℝ)).symm.trans
        ((MeasurableEquiv.sumPiEquivProdPi fun x => ℝ).trans
          (((MeasurableEquiv.toLp 2 (Fin (Module.finrank ℝ U) → ℝ)).trans
                (stdOrthonormalBasis ℝ U).repr.symm.toMeasurableEquiv).prodCongr
            ((MeasurableEquiv.toLp 2 (Fin (Module.finrank ℝ V) → ℝ)).trans
              (stdOrthonormalBasis ℝ V).repr.symm.toMeasurableEquiv))))
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.Const.modify.match_3.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DHashMap.Internal.Raw₀ α fun x => β) → Sort u_3) →
      (m : Std.DHashMap.Internal.Raw₀ α fun x => β) →
        ((size : ℕ) →
            (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β)) →
              (hm : 0 < { size := size, buckets := buckets }.buckets.size) →
                motive ⟨{ size := size, buckets := buckets }, hm⟩) →
          motive m
-- Mathlib.Algebra.Order.Module.Defs
OrderDual.instSMulPosMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Monoid α] [inst_2 : AddCommGroup β]
  [inst_3 : PartialOrder β] [IsOrderedAddMonoid β] [inst_5 : DistribMulAction α β] [SMulPosMono α β], SMulPosMono α βᵒᵈ
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_intCast : ∀ {R : Type u} [inst : Ring R] {S : Type u_1} [inst_1 : Ring S] (f : R →+* S) (n : ℤ), Polynomial.map f ↑n = ↑n
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.integral_comap_eq_mulEquivHaarChar_smul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure]
  [μ.Regular] {f : G → ℝ} (φ : G ≃ₜ* G),
  ∫ (a : G), f a ∂MeasureTheory.Measure.comap (⇑φ) μ = MeasureTheory.mulEquivHaarChar φ • ∫ (a : G), f a ∂μ
-- Mathlib.Algebra.DirectSum.Ring
/-- The `CommRing` derived from `GCommSemiring A`.  -/
DirectSum.instCommRingOfNat : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : (i : ι) → AddCommGroup (A i)] → [inst_1 : AddCommMonoid ι] → [DirectSum.GCommRing A] → CommRing (A 0)
-- Mathlib.GroupTheory.DivisibleHull
/-- Create an element `m / s`.  -/
DivisibleHull.mk : {M : Type u_1} → [inst : AddCommMonoid M] → M → ℕ+ → DivisibleHull M
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} {l : List α} {k : α},
  (m.insertManyIfNewUnit l)[k]! = ()
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
instPosMulStrictMonoIdeal : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A], PosMulStrictMono (Ideal A)
-- Mathlib.Algebra.Group.Even
isSquare_iff_exists_sq : ∀ {α : Type u_2} [inst : Monoid α] (a : α), IsSquare a ↔ ∃ r, a = r ^ 2
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colim_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] {X Y : CategoryTheory.Functor J C} (α : X ⟶ Y),
  CategoryTheory.Limits.colim.map α = CategoryTheory.Limits.colimMap α
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
_private.Mathlib.Algebra.ContinuedFractions.Computation.Basic.0.GenContFract.IntFractPair.stream.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Data.Part
Part.instSub : {α : Type u_1} → [Sub α] → Sub (Part α)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_sdiff_right : ∀ {α : Type u_7} {β : Type u_8} [inst : GeneralizedBooleanAlgebra α] (s : Finset β) (f : β → α) (a : α),
  (s.sup fun b => f b \ a) = s.sup f \ a
-- Mathlib.Data.Fintype.EquivFin
/-- If `s : Set α` is a proper subset of `α` and `f : α → s` is injective, then `α` is infinite.  -/
Infinite.of_injective_to_set : ∀ {α : Type u_1} {s : Set α}, s ≠ Set.univ → ∀ {f : α → ↑s}, Function.Injective f → Infinite α
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The structure sheaf of a locally ringed space.  -/
AlgebraicGeometry.LocallyRingedSpace.𝒪 : (X : AlgebraicGeometry.LocallyRingedSpace) → TopCat.Sheaf CommRingCat X.toTopCat
-- Init.Data.Array.Attach
Array.size_attachWith : ∀ {α : Type u_1} {p : α → Prop} {xs : Array α} {H : ∀ x ∈ xs, p x}, (xs.attachWith p H).size = xs.size
-- Mathlib.Algebra.Order.Group.DenselyOrdered
le_mul_of_forall_lt : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a b c : α},
  (∀ a' > a, ∀ b' > b, c ≤ a' * b') → c ≤ a * b
-- Mathlib.Algebra.Group.Invertible.Basic
Invertible.mulLeft_apply : ∀ {α : Type u} [inst : Monoid α] {a : α} (x : Invertible a) (b : α) (x_1 : Invertible b),
  (x.mulLeft b) x_1 = invertibleMul a b
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankOne.exists_val_lt : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [inst_1 : DivisionRing K]
  (v : Valuation K Γ₀) [inst_2 : v.RankOne] {γ : NNReal},
  γ ≠ 0 → ∃ x, x ≠ 0 ∧ (Valuation.RankOne.hom v) (v.restrict x) < γ
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_eq_nil_iff : ∀ {m n : ℤ}, (m...n).toList = [] ↔ n ≤ m
-- Mathlib.Algebra.Order.Field.Basic
Mathlib.Meta.Positivity.div_ne_zero_of_pos_of_ne_zero : ∀ {α : Type u_4} [inst : GroupWithZero α] [inst_1 : PartialOrder α] {a b : α}, 0 < a → b ≠ 0 → a / b ≠ 0