mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.mk.inj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {inst : CategoryTheory.Category.{v₁, u₁} C₁}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} C₂} {inst_2 : CategoryTheory.Category.{v₃, u₃} C₃}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (Opposite.op X₁)}
  {unit_whiskerRight_map :
    autoParam
      (∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁),
        CategoryTheory.CategoryStruct.comp (adj X₁).unit
            (CategoryTheory.Functor.whiskerRight (F.map f) (G.obj (Opposite.op X₁))) =
          CategoryTheory.CategoryStruct.comp (adj Y₁).unit ((F.obj Y₁).whiskerLeft (G.map f.op)))
      CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map._autoParam}
  {adj_1 : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (Opposite.op X₁)}
  {unit_whiskerRight_map_1 :
    autoParam
      (∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁),
        CategoryTheory.CategoryStruct.comp (adj_1 X₁).unit
            (CategoryTheory.Functor.whiskerRight (F.map f) (G.obj (Opposite.op X₁))) =
          CategoryTheory.CategoryStruct.comp (adj_1 Y₁).unit ((F.obj Y₁).whiskerLeft (G.map f.op)))
      CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map._autoParam},
  { adj := adj, unit_whiskerRight_map := unit_whiskerRight_map } =
      { adj := adj_1, unit_whiskerRight_map := unit_whiskerRight_map_1 } →
    adj = adj_1
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo.declName : Lean.Elab.WF.EqnInfo → Lean.Name
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.multivariateGaussian_zero_one : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι],
  ProbabilityTheory.multivariateGaussian 0 1 = ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.counitForward_val_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)}
  (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (x : F.obj (Opposite.op s)),
  CategoryTheory.OverPresheafAux.YonedaCollection.snd (CategoryTheory.OverPresheafAux.counitForward F s x).val =
    (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯))) x
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- Given a quotient space `G ⧸ Γ` where `Γ` is `Countable`, and the restriction,
`μ_𝓕`, of a right-invariant measure `μ` on `G` to a fundamental domain `𝓕`, a set
in the quotient which has `μ_𝓕`-measure zero, also has measure zero under the
folding of `μ` under the quotient. Note that, if `Γ` is infinite, then the folded map
will take the value `∞` on any open set in the quotient!  -/
MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ →
    ∀ [Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [μ.IsMulRightInvariant],
      (MeasureTheory.Measure.map QuotientGroup.mk μ).AbsolutelyContinuous
        (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕))
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.mem_closure_sdiff_singleton_iff_closure : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e : α},
  e ∈ X →
    autoParam (e ∈ M.E) Matroid.mem_closure_sdiff_singleton_iff_closure._auto_1 →
      (e ∈ M.closure (X \ {e}) ↔ M.closure (X \ {e}) = M.closure X)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.top_prod : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (s : Subring S),
  ⊤.prod s = Subring.comap (RingHom.snd R S) s
-- Mathlib.Order.Filter.Ultrafilter.Basic
Ultrafilter.eq_pure_of_finite : ∀ {α : Type u} [Finite α] (f : Ultrafilter α), ∃ a, f = pure a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mul_nc.go : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.coassoc_symm : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A],
  ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul =
    LinearMap.rTensor A CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul
-- Mathlib.Analysis.Normed.Group.Pointwise
smul_closedBall_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), x • Metric.closedBall 1 δ = Metric.closedBall x δ
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.multipliable_symmetricIco_of_multipliable_symmetricIcc : ∀ {α : Type u_1} {f : ℤ → α} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [ContinuousMul α],
  Multipliable f (SummationFilter.symmetricIcc ℤ) →
    Filter.Tendsto (fun N => (f ↑N)⁻¹) Filter.atTop (nhds 1) → Multipliable f (SummationFilter.symmetricIco ℤ)
-- Mathlib.Analysis.Convex.Deriv
bddBelow_slope_lt_of_mem_interior : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜}
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜],
  ConvexOn 𝕜 s f → x ∈ interior s → BddBelow (slope f x '' {y | y ∈ s ∧ x < y})
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddCommGroup : {α : Type u_1} → [AddCommGroup α] → AddCommGroup αᵒᵈ
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  {F : CategoryTheory.Functor C D} {x y : F.LaxMonoidal},
  x = y ↔
    CategoryTheory.Functor.LaxMonoidal.ε F = CategoryTheory.Functor.LaxMonoidal.ε F ∧
      CategoryTheory.Functor.LaxMonoidal.μ F = CategoryTheory.Functor.LaxMonoidal.μ F
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.exists_mem_germ_eq_of_isBasis : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {B : Set (TopologicalSpace.Opens ↑X)},
  TopologicalSpace.Opens.IsBasis B →
    ∀ (F : TopCat.Presheaf C X) (x : ↑X) (t : CategoryTheory.ToType (F.stalk x)),
      ∃ U, ∃ (m : x ∈ U) (_ : U ∈ B), ∃ s, (CategoryTheory.ConcreteCategory.hom (F.germ U x m)) s = t
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_indicator₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∀ (f : α → ENNReal), ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.finSuccEquiv.eq_1 : ∀ (R : Type u_2) [inst : CommSemiring R] (n : ℕ),
  MvPowerSeries.finSuccEquiv R n =
    (MvPowerSeries.renameEquiv R (finSuccEquiv n)).trans (MvPowerSeries.optionEquivLeft (Fin n) R)
-- Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
BoxIntegral.Box.splitCenterBox_le : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Set ι), I.splitCenterBox s ≤ I
-- Mathlib.Topology.Inseparable
stableUnderSpecialization_sInter : ∀ {X : Type u_1} [inst : TopologicalSpace X] (S : Set (Set X)),
  (∀ s ∈ S, StableUnderSpecialization s) → StableUnderSpecialization (⋂₀ S)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.forM_eq_forM_toArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {m' : Type w → Type w'} [inst : Monad m']
  [LawfulMonad m'] {f : (a : α) → β a → m' PUnit.{w + 1}},
  Std.DHashMap.Raw.forM f ↑m = Array.forM (fun a => f a.fst a.snd) (↑m).toArray
-- Mathlib.Topology.Separation.Hausdorff
/-- A continuous map from a compact space to a Hausdorff space is a closed map.  -/
Continuous.isClosedMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X] [T2Space Y]
  {f : X → Y}, Continuous f → IsClosedMap f
-- Init.Data.BitVec.Lemmas
BitVec.cpop_reverse : ∀ {w : ℕ} (x : BitVec w), x.reverse.cpop = x.cpop
-- Mathlib.Analysis.Normed.Module.FiniteDimension
LinearIsometry.toLinearIsometryEquiv.congr_simp : ∀ {F : Type u_1} {E₁ : Type u_2} [inst : SeminormedAddCommGroup F] [inst_1 : NormedAddCommGroup E₁] {R₁ : Type u_3}
  [inst_2 : Field R₁] [inst_3 : Module R₁ E₁] [inst_4 : Module R₁ F] [inst_5 : FiniteDimensional R₁ E₁]
  [inst_6 : FiniteDimensional R₁ F] (li li_1 : E₁ →ₗᵢ[R₁] F),
  li = li_1 →
    ∀ (h : Module.finrank R₁ E₁ = Module.finrank R₁ F), li.toLinearIsometryEquiv h = li_1.toLinearIsometryEquiv h
-- Mathlib.Topology.MetricSpace.HausdorffDimension
Real.dimH_ball_pi : ∀ {ι : Type u_1} [inst : Fintype ι] (x : ι → ℝ) {r : ℝ}, 0 < r → dimH (Metric.ball x r) = ↑(Fintype.card ι)
-- Mathlib.Control.Bitraversable.Instances
instBitraversableSum : Bitraversable Sum
-- Init.System.IO
/-- Traverses a filesystem starting at the path `p` and exploring directories that satisfy `enter`,
returning the paths visited.

The traversal is a preorder traversal, in which parent directories occur prior to any of their
children. Symbolic links are followed.
 -/
System.FilePath.walkDir : System.FilePath → (optParam (System.FilePath → IO Bool) fun x => pure true) → IO (Array System.FilePath)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.DHashMap.Const.insertMany m l).getKey? k = m.getKey? k
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquiv_inverse_map_hom : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Mon Cᴹᵒᵖ} (f : X ⟶ Y), ((MonObj.mopEquiv C).inverse.map f).hom = f.hom.unmop
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_eq_zero : ∀ {k n : ℕ}, (ArithmeticFunction.sigma k) n = 0 ↔ n = 0
-- Mathlib.Analysis.Real.Sqrt
Real.neg_sqrt_le_of_sq_le : ∀ {x y : ℝ}, x ^ 2 ≤ y → -√y ≤ x
-- Mathlib.NumberTheory.ModularForms.SlashActions
/-- A general version of the slash action of the space of modular forms. This is the same data as a
family of `DistribMulAction Gᵒᵖ α` indexed by `k`.  -/
SlashAction : Type u_1 → (G : Type u_2) → (α : Type u_3) → [Monoid G] → [AddMonoid α] → Type (max (max u_1 u_2) u_3)
-- Init.Control.State
/-- Interpret `σ → m (α × σ)` as an element of `StateT σ m α`.
 -/
StateT.mk : {σ : Type u} → {m : Type u → Type v} → {α : Type u} → (σ → m (α × σ)) → StateT σ m α
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_list : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {ps : Std.Do.PostShape} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] {xs : List α} {init : β} {f : α → β → m (ForInStep β)}
  (inv : Std.Do.Invariant xs β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piConst_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] (X : C)
  (n : Type wᵒᵖ), (CategoryTheory.Limits.piConst.obj X).obj n = ∏ᶜ fun x => X
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_prod_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ι → MvPolynomial σ R},
  (∏ i ∈ s, f i).degrees ≤ ∑ i ∈ s, (f i).degrees
-- Mathlib.RingTheory.Valuation.Basic
Valuation.toAddValuation_symm_eq : ∀ {R : Type u_3} {Γ₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀],
  Valuation.toAddValuation.symm = Valuation.ofAddValuation
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_glue : ∀ {α : Type u} {β : α → Type v} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced} {hr : r.Balanced}
  {hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size},
  (l.glue r hl hr hlr).toListModel = l.toListModel ++ r.toListModel
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.realToRCLike_inj : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] {f g : C(X, ℝ)},
  ContinuousMap.realToRCLike 𝕜 f = ContinuousMap.realToRCLike 𝕜 g ↔ f = g
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by heads: given a function `f`, a
finite sets `s` in its domain, a finite set `t` in its codomain, and a natural number `n` such that
`#s ≤ #t * n`, there exists `y ∈ t` such that its preimage in `s` has no more than `n`
elements. See also `Finset.exists_card_fiber_lt_of_card_lt_mul` for a stronger statement.  -/
Finset.exists_card_fiber_le_of_card_le_mul : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ},
  t.Nonempty → s.card ≤ t.card * n → ∃ y ∈ t, {x ∈ s | f x = y}.card ≤ n
-- Lean.Elab.Tactic.Try
/-- Returns a tactic representing all given suggestions `tacs`.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkTrySuggestions : Array (Lean.TSyntax `tactic) → Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic)
-- Mathlib.Order.RelClasses
IsStrictTotalOrder.swap : ∀ {α : Type u} (r : α → α → Prop) [IsStrictTotalOrder α r], IsStrictTotalOrder α (Function.swap r)
-- Mathlib.Analysis.Meromorphic.NormalForm
toMeromorphicNFOn.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (U : Set 𝕜),
  toMeromorphicNFOn f U =
    if h₁f : MeromorphicOn f U then fun z => if hz : z ∈ U then toMeromorphicNFAt f z z else f z else 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.unique_nonDegenerate_map : ∀ (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })) {m : ℕ} (f₁ : { len := n } ⟶ { len := m })
  [CategoryTheory.Epi f₁] (y₁ : ↑(X.nonDegenerate m)),
  x = (CategoryTheory.ConcreteCategory.hom (X.map f₁.op)) ↑y₁ →
    ∀ (f₂ : { len := n } ⟶ { len := m }) (y₂ : ↑(X.nonDegenerate m)),
      x = (CategoryTheory.ConcreteCategory.hom (X.map f₂.op)) ↑y₂ → f₁ = f₂
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousOn.norm : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {s : Set α},
  ContinuousOn f s → ContinuousOn (fun x => ‖f x‖) s
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.map_mkOfSucc_zero_concat : ∀ {X : SSet} {n : ℕ} (self : X.StrictSegalCore n) (x : X.obj (Opposite.op { len := 1 }))
  (s : X.obj (Opposite.op { len := n }))
  (h :
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
      (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s),
  (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) (self.concat x s h) = x
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_comp_nonneg : ∀ {u : ℕ → ENNReal} {v : ℕ → ℕ},
  Monotone u → u ≠ 0 → Filter.Tendsto v Filter.atTop Filter.atTop → 0 ≤ ExpGrowth.expGrowthSup (u ∘ v)
-- Mathlib.Data.EReal.Basic
EReal.coe_ne_zero : ∀ {x : ℝ}, ↑x ≠ 0 ↔ x ≠ 0
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialLeftAdjointHomEquiv_symm_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) {X : F.PartialLeftAdjointSource} {Y Y' : D} (f : X.obj ⟶ F.obj Y) (g : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (F.partialLeftAdjointHomEquiv.symm f) g =
    F.partialLeftAdjointHomEquiv.symm (CategoryTheory.CategoryStruct.comp f (F.map g))
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesOnBall.iteratedFDeriv_zero_apply_diag : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → iteratedFDeriv 𝕜 0 f x = p 0
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instInhabitedRange : Inhabited Lean.Lsp.Range
-- Std.Data.TreeMap.Lemmas
_private.Std.Data.TreeMap.Lemmas.0.GetElem?.match_1.eq_1 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (e : elem) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match some e with
    | some e => h_1 e
    | none => h_2 ()) =
    h_1 e
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_arrow_factors_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {B : C}
  (X Y : CategoryTheory.Subobject B), Y.Factors (X ⊓ Y).arrow
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.mem_ofSign : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {s : ℤˣ} {σ : Equiv.Perm α},
  σ ∈ Equiv.Perm.ofSign s ↔ Equiv.Perm.sign σ = s
-- Mathlib.Lean.Elab.InfoTree
/-- Collects all suggestions from all `TryThisInfo`s in `trees`.
Does not require context - works with context-free trees.
 -/
Lean.Elab.collectTryThisSuggestions : Lean.PersistentArray Lean.Elab.InfoTree → Array Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.ext : ∀ {R : outParam (Type u_1)} {S : outParam (Type u_2)} [inst : SeminormedCommRing R] [inst_1 : Ring S]
  [inst_2 : Algebra R S] {p q : MulAlgebraNorm R S}, (∀ (x : S), p x = q x) → p = q
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- Any morphism `k : A ⟶ S.X₂` that is a cycle (i.e. `k ≫ S.g = 0`) lifts
to a morphism `A ⟶ K`  -/
CategoryTheory.ShortComplex.LeftHomologyData.liftK : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.LeftHomologyData) → {A : C} → (k : A ⟶ S.X₂) → CategoryTheory.CategoryStruct.comp k S.g = 0 → (A ⟶ h.K)
-- Mathlib.Data.Fin.VecNotation
Matrix.vecAlt1_vecAppend : ∀ {α : Type u} {n : ℕ} (v : Fin (n + 1) → α), Matrix.vecAlt1 ⋯ (Matrix.vecAppend ⋯ v v) = v ∘ fun n_1 => n_1 + n_1 + 1
-- Init.Data.List.ToArray
Array.back!.eq_1 : ∀ {α : Type u} [inst : Inhabited α] (xs : Array α), xs.back! = xs[xs.size - 1]!
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.hasKernel_comp_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] (g : Y ⟶ Z) [CategoryTheory.Mono g],
  CategoryTheory.Limits.HasKernel (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.qaryEntropy_pos : ∀ {q : ℕ} {p : ℝ}, 0 < p → p < 1 → 0 < Real.qaryEntropy q p
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere' : ∀ {P : Type u_2} [inst : MetricSpace P] {p₁ p₂ : P} {s : EuclideanGeometry.Sphere P},
  p₁ ∈ s → p₂ ∈ s → dist s.center p₁ = dist s.center p₂
-- Lean.Elab.ParseImportsFast
Lean.PrintImportResult.errors : Lean.PrintImportResult → Array String
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.coe_vadd : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : VAdd M X] [UniformContinuousConstVAdd M X] (c : M)
  (x : X), ↑(c +ᵥ x) = c +ᵥ ↑x
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.mk.sizeOf_spec : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Semiring R] [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {E : Type u_11} {E₂ : Type u_12}
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  [inst_8 : SizeOf R] [inst_9 : SizeOf R₂] [inst_10 : SizeOf E] [inst_11 : SizeOf E₂] (toLinearEquiv : E ≃ₛₗ[σ₁₂] E₂)
  (norm_map' : ∀ (x : E), ‖toLinearEquiv x‖ = ‖x‖),
  sizeOf { toLinearEquiv := toLinearEquiv, norm_map' := norm_map' } = 1 + sizeOf toLinearEquiv
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
/-- Constructor for 2-isomorphisms in the induced bicategory.  -/
CategoryTheory.Bicategory.InducedBicategory.isoMk : {B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory C] →
      {F : B → C} → {X Y : CategoryTheory.Bicategory.InducedBicategory C F} → {f g : X ⟶ Y} → (f.hom ≅ g.hom) → (f ≅ g)
-- Mathlib.Data.EReal.Operations
EReal.coe_mul_top_of_neg : ∀ {x : ℝ}, x < 0 → ↑x * ⊤ = ⊥
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.ofArray_apply : ∀ {R : Type u_7} {m n : ℕ} (A : Array R) (hA : A.size = m * n) (i : Fin m) (j : Fin n),
  Matrix.ofArray A hA i j = A[i.mkDivMod j]
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme),
  AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
    P ≤ @AlgebraicGeometry.IsAffineHom
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.ofLex_degree_fst : ∀ {R : Type u_2} [inst : CommRing R] {n : ℕ} {e : ChevalleyThm.PolynomialC.InductionObj✝ R n} (i : Fin n),
  (ofLex (ChevalleyThm.PolynomialC.InductionObj.degree✝ e)).1 i =
    (ChevalleyThm.PolynomialC.InductionObj.val✝ e i).degree
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.forIn'_eq_if_roc : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α] [inst_3 : Std.PRange.Least? α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_8 : Std.Rxc.IsAlwaysFinite α] [inst_9 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w}
  [inst_10 : Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f =
    if hu : Std.PRange.UpwardEnumerable.least ≤ r.upper then do
      let __do_lift ← f Std.PRange.UpwardEnumerable.least hu init
      match __do_lift with
        | ForInStep.yield c => forIn' (Std.PRange.UpwardEnumerable.least<...=r.upper) c fun a ha acc => f a ⋯ acc
        | ForInStep.done c => pure c
    else pure init
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
CategoryTheory.Limits.instHasIterationOfShapeFunctor : ∀ (J : Type w) [inst : LinearOrder J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] (K : Type u')
  [inst_2 : CategoryTheory.Category.{v', u'} K] [CategoryTheory.Limits.HasIterationOfShape J C],
  CategoryTheory.Limits.HasIterationOfShape J (CategoryTheory.Functor K C)
-- Mathlib.Tactic.FunProp.Types
/-- current transition depth  -/
Mathlib.Meta.FunProp.Context.transitionDepth : Mathlib.Meta.FunProp.Context → ℕ