mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
summableLocallyUniformly_of_of_forall_exists_nhds : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β], (∀ (x : β), ∃ t ∈ nhds x, SummableUniformlyOn f t) → SummableLocallyUniformly f
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_pi' : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {ι : Type u_4} {φ : ι → Type u_5} [inst_4 : (i : ι) → TopologicalSpace (φ i)]
  [inst_5 : (i : ι) → AddCommMonoid (φ i)] [inst_6 : (i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i),
  ⇑(ContinuousLinearMap.pi f) = fun c i => (f i) c
-- Mathlib.Algebra.Group.Semiconj.Defs
SemiconjBy.conj_iff : ∀ {G : Type u_3} [inst : Group G] {a x y b : G}, SemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) ↔ SemiconjBy a x y
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tprod_of_nat_of_neg_add_one : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] [T2Space M] {f : ℤ → M},
  (Multipliable fun n => f ↑n) →
    (Multipliable fun n => f (-(↑n + 1))) → ∏' (n : ℤ), f n = (∏' (n : ℕ), f ↑n) * ∏' (n : ℕ), f (-(↑n + 1))
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {n : ℕ}
  {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n)
  (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc)
  (hkf : CategoryTheory.Limits.IsLimit kf),
  (S.sc hS k ⋯).Exact → CategoryTheory.Mono (hS.cokerToKer' k hk cc kf hcc hkf)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.structurePresheafInModuleCat_obj_carrier : ∀ (R M : Type u) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ),
  ↑((AlgebraicGeometry.structurePresheafInModuleCat R M).obj U) = (AlgebraicGeometry.structureSheafInType R M).obj.obj U
-- Mathlib.Topology.Instances.Matrix
Topology.IsClosedEmbedding.matrix_map : ∀ {m : Type u_11} {n : Type u_12} {R : Type u_13} {S : Type u_14} [inst : TopologicalSpace R]
  [inst_1 : TopologicalSpace S] {f : R → S}, Topology.IsClosedEmbedding f → Topology.IsClosedEmbedding fun x => x.map f
-- Mathlib.Algebra.Order.Ring.StandardPart
/-- The standard part of a `FiniteElement` is the unique real number with an infinitesimal
difference.

For any infinite inputs, this function outputs a junk value of 0.  -/
ArchimedeanClass.stdPart : {K : Type u_1} → [inst : LinearOrder K] → [inst_1 : Field K] → [IsOrderedRing K] → K → ℝ
-- Mathlib.Analysis.Analytic.Order
/-- On a connected set, there exists a point where a meromorphic function `f` has finite order iff
`f` has finite order at every point.  -/
AnalyticOnNhd.exists_analyticOrderAt_ne_top_iff_forall : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E},
  AnalyticOnNhd 𝕜 f U → IsConnected U → ((∃ u, analyticOrderAt f ↑u ≠ ⊤) ↔ ∀ (u : ↑U), analyticOrderAt f ↑u ≠ ⊤)
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_8.eq : ∀ {i : Type u} {b : Type v} {motive_1 : Lean.Doc.Block i b → Sort u_1}
  {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1}
  {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1}
  {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1}
  (t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))
  (F_1 : (t : Lean.Doc.Block i b) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_4 t → motive_5 t)
  (F_6 :
    (t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t)
  (F_8 : (t : Lean.Doc.ListItem (Lean.Doc.Block i b)) → Lean.Doc.Block.below_7 t → motive_8 t)
  (F_9 : (t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Lean.Doc.Block.below_8 t → motive_9 t),
  Lean.Doc.Block.brecOn_8 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 =
    F_9 t (Lean.Doc.Block.brecOn_8.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9).2
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- The backwards edge  -/
SSet.Edge.InvStruct.inv : {X : SSet} → {x₀ x₁ : X.obj (Opposite.op { len := 0 })} → {hom : SSet.Edge x₀ x₁} → hom.InvStruct → SSet.Edge x₁ x₀
-- Mathlib.Algebra.Category.ModuleCat.Kernels
/-- The kernel of a linear map is a kernel in the categorical sense.  -/
ModuleCat.kernelIsLimit : {R : Type u} →
  [inst : Ring R] → {M N : ModuleCat R} → (f : M ⟶ N) → CategoryTheory.Limits.IsLimit (ModuleCat.kernelCone f)
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Implementation of `SheafConditionPairwiseIntersections.coneEquiv`.  -/
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F) →
                CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)
-- Mathlib.SetTheory.Lists
/-- Membership of ZFA list. A ZFA list belongs to a proper ZFA list if it belongs to the latter as a
proper ZFA prelist. An atom has no members.  -/
Lists.mem : {α : Type u_1} → Lists α → Lists α → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.instInhabitedHom : {J : CategoryTheory.Limits.MulticospanShape} → {a : CategoryTheory.Limits.WalkingMulticospan J} → Inhabited (a.Hom a)
-- Init.Data.SInt.Lemmas
instCommutativeInt8HAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_alter_eq_sub_one : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  k ∈ t → (f (t.get? k)).isNone = true → (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.size = t.size - 1
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorZero'.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ) (h : n = 0),
  CochainComplex.shiftFunctorZero' C n h = CochainComplex.shiftFunctorZero' C n h
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- The unit sphere in an `n + 1`-dimensional inner product space `E` is a charted space
modelled on the Euclidean space of dimension `n`.  -/
EuclideanSpace.instChartedSpaceSphere : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      {n : ℕ} → [Fact (Module.finrank ℝ E = n + 1)] → ChartedSpace (EuclideanSpace ℝ (Fin n)) ↑(Metric.sphere 0 1)
-- Init.Grind.ToInt
/-- The embedding function.  -/
Lean.Grind.ToInt.toInt : {α : Type u} → {range : outParam Lean.Grind.IntInterval} → [self : Lean.Grind.ToInt α range] → α → ℤ
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.instSProdProd : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        SProd (TopologicalSpace.Clopens α) (TopologicalSpace.Clopens β) (TopologicalSpace.Clopens (α × β))
-- Mathlib.Algebra.Group.Even
isSquare_unop_iff : ∀ {α : Type u_2} [inst : Mul α] {a : αᵐᵒᵖ}, IsSquare (MulOpposite.unop a) ↔ IsSquare a
-- Init.GrindInstances.ToInt
Lean.Grind.instLTInt64SintOfNatNat : Lean.Grind.ToInt.LT Int64 (Lean.Grind.IntInterval.sint 64)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toArray_toList_ensureTermination : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterators.Finite α m] {it : Std.IterM m β}, List.toArray <$> it.ensureTermination.toList = it.toArray
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.associator_neg_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H I : CategoryTheory.AddGrp C),
  (CategoryTheory.MonoidalCategoryStruct.associator G H I).inv.hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.associator G.X H.X I.X).inv
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.instNoncompactSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NoncompactSpace α], NoncompactSpace (TopologicalSpace.Compacts α)
-- Init.Data.Rat.Lemmas
Rat.normalize_eq : ∀ {num : ℤ} {den : ℕ} (den_nz : den ≠ 0),
  Rat.normalize num den den_nz =
    { num := num / ↑(num.natAbs.gcd den), den := den / num.natAbs.gcd den, den_nz := ⋯, reduced := ⋯ }
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.carrier_neg : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (c : ConjRootClass K L),
  (-c).carrier = -c.carrier
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.image_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {x : H}
  {s : Set H}, s ∈ nhds x → ↑I '' s ∈ nhdsWithin (↑I x) (Set.range ↑I)
-- Mathlib.RingTheory.TensorProduct.Maps
/-- Given a subalgebra `C` of an `R`-algebra `A`, and an `R`-algebra `B`, the base change of `C` to
a subalgebra of `B ⊗[R] A`  -/
Subalgebra.baseChange : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          (B : Type u_3) →
            [inst_3 : CommSemiring B] → [inst_4 : Algebra R B] → Subalgebra R A → Subalgebra B (TensorProduct R B A)
-- Lean.Elab.AutoBound
/-- Tracks extra context needed within the scope of `Lean.Elab.Term.withAutoBoundImplicit`
 -/
Lean.Elab.AutoBoundImplicitContext : Type
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β} [inst : Inhabited β],
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (Std.TreeMap.ofList l cmp)[k']! = v
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  [inst_2 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] (c : C)
  (X : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H),
  (CategoryTheory.Limits.fiberwiseColimCompEvaluationIso c).hom.app X =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit ((CategoryTheory.Grothendieck.ι F c).comp X))
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
Unitary.conjStarAlgAut_trans_conjStarAlgAut : ∀ {S : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : SMul S R]
  [inst_3 : IsScalarTower S R R] [inst_4 : SMulCommClass S R R] (u₁ u₂ : ↥(unitary R)),
  ((Unitary.conjStarAlgAut S R) u₁).trans ((Unitary.conjStarAlgAut S R) u₂) = (Unitary.conjStarAlgAut S R) (u₂ * u₁)
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_nat_floor_div_atTop : ∀ {R : Type u_4} [inst : TopologicalSpace R] [inst_1 : Field R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R]
  [OrderTopology R] [inst_5 : FloorRing R], Filter.Tendsto (fun x => ↑⌊x⌋₊ / x) Filter.atTop (nhds 1)
-- Mathlib.GroupTheory.Subgroup.Center
AddCommGroup.center_eq_top : ∀ {G : Type u_2} [inst : AddCommGroup G], AddSubgroup.center G = ⊤
-- Mathlib.Dynamics.Ergodic.Ergodic
/-- For a quasi-ergodic map, sets that are almost invariant (rather than strictly invariant) are
still either almost empty or full.  -/
QuasiErgodic.ae_empty_or_univ₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α},
  QuasiErgodic f μ → MeasureTheory.NullMeasurableSet s μ → f ⁻¹' s =ᵐ[μ] s → s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
-- Mathlib.Probability.Distributions.Gaussian.CharFun
/-- If the characteristic function of `μ` takes the form of a gaussian characteristic function,
then the parameters have to be the expectation and the covariance bilinear form.  -/
ProbabilityTheory.gaussian_charFun_congr : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_5 : InnerProductSpace ℝ E]
  [MeasureTheory.IsFiniteMeasure μ] (m : E) (f : E →L[ℝ] E →L[ℝ] ℝ),
  f.toBilinForm.IsPosSemidef →
    (∀ (t : E), MeasureTheory.charFun μ t = Complex.exp (↑(inner ℝ t m) * Complex.I - ↑((f t) t) / 2)) →
      m = ∫ (x : E), x ∂μ ∧ f = ProbabilityTheory.covarianceBilin μ
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Associating a `Composition n` to a `CompositionAsSet n`, by registering the sizes of the
blocks as a list of positive integers.  -/
CompositionAsSet.toComposition : {n : ℕ} → CompositionAsSet n → Composition n
-- Std.Time.Format.Modifier
/-- `z`: Time zone name (e.g., Pacific Standard Time, PST).
 -/
Std.Time.Modifier.z : Std.Time.ZoneName → Std.Time.Modifier
-- Mathlib.Data.Rel
SetRel.rfl : ∀ {α : Type u_1} (R : SetRel α α) {a : α} [R.IsRefl], (a, a) ∈ R
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.BiconeMorphism.ext_iff : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F}
  {f g : c ⟶ c'}, f = g ↔ f.hom = g.hom
-- Init.Grind.Module.Basic
Lean.Grind.NatModule.nsmul_add : ∀ {M : Type u} [inst : Lean.Grind.NatModule M] (n : ℕ) (a b : M), n • (a + b) = n • a + n • b
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- A functor reflecting larger filtered colimits also reflects smaller filtered colimits.  -/
CategoryTheory.Limits.reflectsFilteredColimitsOfSize_of_univLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
  [CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
-- Mathlib.Data.Matrix.Basis
Matrix.col_eq_zero_of_commute_single : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Semiring α] {i j k : n}
  {M : Matrix n n α}, Commute (Matrix.single i j 1) M → k ≠ i → M k i = 0
-- Mathlib.Tactic.Order.CollectFacts
/-- Adds `fact` to the state. Assumes that `type` is already added by `addType`.  -/
Mathlib.Tactic.Order.addFact : Lean.Expr → Mathlib.Tactic.Order.AtomicFact → Mathlib.Tactic.Order.CollectFactsM Unit
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteVerts_deleteVerts : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s s' : Set V),
  (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s')
-- Mathlib.Analysis.Complex.Exponential
_private.Mathlib.Analysis.Complex.Exponential.0.Nat.factorial.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Init.Data.Rat.Lemmas
Rat.divInt_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ Rat.divInt a b
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.instIsStrictlySupportedOfNat : ∀ {ι : 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] (e : c.Embedding c')
  [inst_2 : CategoryTheory.Limits.HasZeroObject C], HomologicalComplex.IsStrictlySupported 0 e
-- Mathlib.RingTheory.PowerSeries.Derivative
/-- **Alias** of `PowerSeries.derivative_coe`. -/
PowerSeries.derivativeFun_coe : ∀ {R : Type u_1} [inst : CommSemiring R] (f : Polynomial R), (PowerSeries.derivative R) ↑f = ↑(Polynomial.derivative f)
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of the forward direction of `Order.isPredPrelimit_iff_isPredLimit`. -/
Order.IsPredPrelimit.isPredLimit : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [NoMaxOrder α], Order.IsPredPrelimit a → Order.IsPredLimit a
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_right_fderivWithin : ∀ {𝕜 : 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 ≃L[𝕜] F) {f : F → G} {s : Set F} {x : E},
  UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' s) x → fderivWithin 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x = fderivWithin 𝕜 f s (iso x) ∘SL ↑iso
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.inter_orthRadius_eq_singleton_of_dist_eq_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P},
  dist p s.center = s.radius → Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {p}
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.skipSuffixWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.toSlice.skipSuffixWhile pat = (s.skipSuffixWhile pat).toSlice
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.fromGlued.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover),
  AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰 =
    CategoryTheory.Limits.Multicoequalizer.desc (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).diagram X (fun x => 𝒰.f x)
      ⋯
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs_add : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) (x y : R), WithAbs.toAbs v (x + y) = WithAbs.toAbs v x + WithAbs.toAbs v y
-- Std.Sync.CancellationContext
_private.Std.Sync.CancellationContext.0.Std.CancellationContext.countAliveTokensRec : Std.CancellationContext.State → UInt64 → ℕ
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.factors_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {x : α} (n : ℕ),
  Multiset.Rel Associated (UniqueFactorizationMonoid.factors (x ^ n)) (n • UniqueFactorizationMonoid.factors x)
-- Aesop.Tree.Tracing
_private.Aesop.Tree.Tracing.0.Aesop.Goal.withHeadlineTraceNode.fmt : Aesop.Goal → (Lean.MessageData → Lean.MetaM Lean.MessageData) → Lean.MetaM Lean.MessageData
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
_private.Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme.0.AlgebraicGeometry.«termA⁰__» : Lean.ParserDescr
-- Mathlib.Algebra.Opposites
MulOpposite.instSMul : {α : Type u_1} → {β : Type u_2} → [SMul α β] → SMul α βᵐᵒᵖ
-- Aesop.RuleSet
Aesop.GlobalRuleSet.modifyBase : (Aesop.BaseRuleSet → Aesop.BaseRuleSet) → Aesop.GlobalRuleSet → Aesop.GlobalRuleSet
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.mem_carrier : ∀ {K : Type u} [inst : DivisionRing K] {s : Subfield K} {x : K}, x ∈ s.carrier ↔ x ∈ s
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.join.match_1.splitter : {α : Type u_1} →
  (motive : Option (Stream'.WSeq α) → Sort u_2) →
    (o : Option (Stream'.WSeq α)) → (Unit → motive none) → ((s : Stream'.WSeq α) → motive (some s)) → motive o
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Run a `MetaM` action in the saved state.  -/
Lean.Elab.WF.GuessLex.SavedLocalContext.run : {α : Type} → Lean.Elab.WF.GuessLex.SavedLocalContext → Lean.MetaM α → Lean.MetaM α
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.mul_const : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f : α → M}
  {μ : MeasureTheory.Measure α} [MeasurableMul M], AEMeasurable f μ → ∀ (c : M), AEMeasurable (fun x => f x * c) μ
-- Mathlib.Algebra.Lie.Sl2
_private.Mathlib.Algebra.Lie.Sl2.0.IsSl2Triple.termφ_ : Lean.ParserDescr
-- Lean.Elab.Parallel
_private.Lean.Elab.Parallel.0.Std.Iterators.Types.Internal.TaskIterator.mk.sizeOf_spec : ∀ {α : Type w} [inst : SizeOf α] (tasks : List (Task α)), sizeOf { tasks := tasks } = 1 + sizeOf tasks
-- Mathlib.Order.Filter.Pi
Filter.coprodᵢ.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → Filter (α i)),
  Filter.coprodᵢ f = ⨆ i, Filter.comap (Function.eval i) (f i)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- Version of `skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier` using `skeleton`.  -/
Topology.RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] {n : ℕ∞}
  {m : ℕ} {j : Topology.RelCWComplex.cell C m},
  n < ↑m →
    ↑(Topology.RelCWComplex.skeleton C n) ∩ Topology.RelCWComplex.closedCell m j =
      ↑(Topology.RelCWComplex.skeleton C n) ∩ Topology.RelCWComplex.cellFrontier m j
-- Mathlib.CategoryTheory.Category.Cat
/-- `Cat` is a strict bicategory.  -/
CategoryTheory.Cat.bicategory.strict : CategoryTheory.Bicategory.Strict CategoryTheory.Cat
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_zero_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C], (CategoryTheory.Limits.imageSubobject 0).arrow = 0
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.tr_eval : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] {σ : Type u_3} [inst_1 : Inhabited σ]
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) [inst_2 : Inhabited Γ] (l : List Γ),
  Turing.TM0.eval (Turing.TM1to0.tr M) l = Turing.TM1.eval M l
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_nsmul_ne_zero_iff : ∀ {θ : Real.Angle}, 2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_add_filter_not : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (p : ι → Prop)
  [inst_1 : DecidablePred p], DFinsupp.filter p f + DFinsupp.filter (fun i => ¬p i) f = f
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsAdjunction_homEquiv_symm_apply_hom : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] {X : Rep.{w, u, v} k G} {Y : ModuleCat k}
  (f : X ⟶ (Rep.trivialFunctor k G).obj Y), ((Rep.coinvariantsAdjunction k G).homEquiv X Y).symm f = Rep.desc f
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- Given `h : v.FineSubfamilyOn f s`, then `h.covering p` is a set in the family,
for `p ∈ h.index`, such that these sets form a disjoint covering of almost every `s`.  -/
VitaliFamily.FineSubfamilyOn.covering : {X : Type u_1} →
  [inst : PseudoMetricSpace X] →
    {m0 : MeasurableSpace X} →
      {μ : MeasureTheory.Measure X} →
        {v : VitaliFamily μ} → {f : X → Set (Set X)} → {s : Set X} → v.FineSubfamilyOn f s → X × Set X → Set X