mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Finiteness
/-- A monoid if finitely generated if and only if there exists a surjective homomorphism from a
`FreeMonoid` on an arbitrary finite type `α` to the monoid.  -/
Monoid.fg_iff_exists_freeGroup_hom_surjective_finite : ∀ {M : Type u_1} [inst : Monoid M], Monoid.FG M ↔ ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ
-- Mathlib.Analysis.Normed.Algebra.Spectrum
NNReal.spectralRadius_mem_spectrum : ∀ {A : Type u_4} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] {a : A},
  (spectrum ℝ a).Nonempty →
    SpectrumRestricts a ⇑ContinuousMap.realToNNReal → (spectralRadius ℝ a).toNNReal ∈ spectrum NNReal a
-- Init.Data.SInt.Lemmas
ISize.left_eq_add : ∀ {a b : ISize}, a = a + b ↔ b = 0
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.next_eq : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁.Hom C₂) {i j : ι} (w : c.Rel i j),
  f.next i =
    CategoryTheory.CategoryStruct.comp (C₁.xNextIso w).hom
      (CategoryTheory.CategoryStruct.comp (f.f j) (C₂.xNextIso w).inv)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_iff_meet_eq_left : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l},
  Lean.Order.PartialOrder.rel P Q ↔ Lean.Order.meet P Q = P
-- Mathlib.Computability.Language
Language.reverse_involutive : ∀ {α : Type u_1}, Function.Involutive Language.reverse
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.differentiableAt_arctan : ∀ (x : ℝ), DifferentiableAt ℝ Real.arctan x
-- Lean.Data.Lsp.Workspace
Lean.Lsp.WorkspaceFolder.uri : Lean.Lsp.WorkspaceFolder → Lean.Lsp.DocumentUri
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.colimitAdjunction_homEquiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.InitiallySmall C]
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R}
  (hcR : CategoryTheory.Limits.IsColimit cR) (F : PresheafOfModules R) (G : ModuleCat ↑cR.pt),
  (PresheafOfModules.colimitAdjunction hcR).homEquiv F G =
    ↑(PresheafOfModules.ModuleColimit.homEquiv hcR (CategoryTheory.Limits.colimit.isColimit F.presheaf))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.instTrans : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Trans Std.DHashMap.Equiv Std.DHashMap.Equiv Std.DHashMap.Equiv
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.ofDual_eq_bot : ∀ (α : Type u) [inst : Bot α] {a : αᵒᵈ}, OrderDual.ofDual a = ⊥ ↔ a = ⊤
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- See also `map_yonedaEquiv'` for a more general version.  -/
CategoryTheory.GrothendieckTopology.map_yonedaEquiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : C} {F : CategoryTheory.Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F) (g : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (F.obj.map g.op)) (J.yonedaEquiv f) =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op Y))) g
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
exists_le_isAssociatedPrime_of_isNoetherianRing : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [H : IsNoetherianRing R] (x : M), x ≠ 0 → ∃ P, IsAssociatedPrime P M ∧ ⊥.colon {x} ≤ P
-- Mathlib.Data.EReal.Operations
EReal.sub_lt_sub_of_le_of_gt : ∀ {x y z t : EReal}, x ≤ y → z < t → x ≠ ⊤ → y ≠ ⊥ → x - t < y - z
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_pow : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (ψ : AddChar A M) (n : ℕ),
  ⇑(ψ ^ n) = ⇑ψ ^ n
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp₂.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ] (g g_1 : β → γ → δ)
  (e_g : g = g_1) (hg : Continuous (Function.uncurry g)) (f₁ f₁_1 : α →ₘ[μ] β),
  f₁ = f₁_1 →
    ∀ (f₂ f₂_1 : α →ₘ[μ] γ),
      f₂ = f₂_1 → MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂ = MeasureTheory.AEEqFun.comp₂ g_1 ⋯ f₁_1 f₂_1
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.Prefunctor.mapPath_comp' : ∀ (V : Type u₁) [inst : Quiver V] (W : Type u₂) [inst_1 : Quiver W] (F : V ⥤q W) {X Y Z : CategoryTheory.Paths V}
  (f : X ⟶ Y) (g : Y ⟶ Z), F.mapPath (CategoryTheory.CategoryStruct.comp f g) = (F.mapPath f).comp (F.mapPath g)
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f g : N →ₗ[R] P) [inst_11 : Module.Flat R M]
  (x :
    ↥(((TensorProduct.AlgebraTensorModule.lTensor S M) f).eqLocus ((TensorProduct.AlgebraTensorModule.lTensor S M) g))),
  (LinearMap.lTensor M (f.eqLocus g).subtype) ((LinearMap.tensorEqLocusEquiv S M f g).symm x) = ↑x
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.run : {α : Type} → Lean.Meta.Sym.Pattern → Bool → Bool → Lean.Meta.Sym.UnifyM✝ α → Lean.Meta.Sym.SymM α
-- Init.Core
Decidable.of_not_not : ∀ {p : Prop} [Decidable p], ¬¬p → p
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_pos_of_root : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.IsRoot a → 0 < p.degree
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.facePairComplIso_hom_ι' : ∀ {n : ℕ} (i j : Fin (n + 3)) (h : i < j),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.facePairComplIso i j h).hom (SSet.stdSimplex.face {i, j}ᶜ).ι =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ (j.pred ⋯)) (SSet.stdSimplex.δ i)
-- Mathlib.Topology.LocallyFinite
LocallyFinite.on_range : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X}, LocallyFinite f → LocallyFinite Subtype.val
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.toWord.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α], FreeGroup.toWord = Quot.lift FreeGroup.reduce ⋯
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Var.denote.eq_1 : ∀ {α : Type u_1} (ctx : Lean.Grind.CommRing.Context α) (v : Lean.Grind.CommRing.Var),
  Lean.Grind.CommRing.Var.denote ctx v = Lean.RArray.get ctx v
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.comap_normalizer_eq_of_le_range : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {N : Type u_5} [inst_1 : Group N] {f : N →* G},
  H ≤ f.range → Subgroup.comap f (Subgroup.normalizer ↑H) = Subgroup.normalizer ↑(Subgroup.comap f H)
-- Mathlib.Data.PNat.Interval
PNat.card_fintype_Icc : ∀ (a b : ℕ+), Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- Subsingletons are (trivial) blocks.  -/
MulAction.IsBlock.of_subsingleton : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X}, B.Subsingleton → MulAction.IsBlock G B
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Circle integrals are invariant when functions change along discrete sets.  -/
circleIntegral.circleIntegral_congr_codiscreteWithin : ∀ {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → ℂ},
  f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂ →
    R ≠ 0 → ∮ (z : ℂ) in C(c, R), f₁ z = ∮ (z : ℂ) in C(c, R), f₂ z
-- Mathlib.Algebra.Ring.CentroidHom
/-- The canonical homomorphism from the center into the centroid  -/
CentroidHom.centerToCentroid : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → ↥(NonUnitalSubsemiring.center α) →ₙ+* CentroidHom α
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.prop_pi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u_3}
  [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete J)] (X : J → C) [inst_2 : CategoryTheory.Limits.HasProduct X],
  (∀ (j : J), P (X j)) → P (∏ᶜ X)
-- Mathlib.Algebra.Free
/-- Length of an element of a free magma.  -/
FreeMagma.length : {α : Type u} → FreeMagma α → ℕ
-- Std.Data.String.ToNat
String.Slice.toNat?_copy : ∀ {s : String.Slice}, s.copy.toNat? = s.toNat?
-- Std.Time.DateTime.Timestamp
/-- Subtracts a `Minute.Offset` from the given `Timestamp`.
 -/
Std.Time.Timestamp.subMinutes : Std.Time.Timestamp → Std.Time.Minute.Offset → Std.Time.Timestamp
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.withDensity_rnDeriv_le : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [inst : ProbabilityTheory.IsFiniteKernel η] (a : α),
  (η.withDensity (κ.rnDeriv η)) a ≤ κ a
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.whiskerRight_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f g : a ⟶ b) (h : b ⟶ c)
  [inst_1 : CategoryTheory.BicategoricalCoherence f g],
  CategoryTheory.BicategoricalCoherence.iso =
    CategoryTheory.Bicategory.whiskerRightIso CategoryTheory.BicategoricalCoherence.iso h
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_uint16 : ∀ (x : UInt16), ↑x = ↑x.toNat
-- Init.System.IO
IO.FS.instLESystemTime : LE IO.FS.SystemTime
-- Mathlib.Topology.Algebra.Support
isCompact_range_of_support_subset_isCompact : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β} {K : Set α}
  [inst_2 : TopologicalSpace β], Continuous f → IsCompact K → Function.support f ⊆ K → IsCompact (Set.range f)
-- Mathlib.Order.Hom.CompleteLattice
instCoeTCFrameHomOfFrameHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : CompleteLattice α] → [inst_2 : CompleteLattice β] → [FrameHomClass F α β] → CoeTC F (FrameHom α β)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.val_symm_eq : ∀ {M : Type u_1}, MulArchimedeanOrder.val.symm = MulArchimedeanOrder.of
-- Init.System.Uri
System.Uri.UriEscape.uriEscapeAsciiChar : Char → String
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.snd_epi : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.IsSplitEpi CategoryTheory.Limits.biprod.snd
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Given any distinguished triangle
```
      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
```
the composition `f ≫ g = 0`.  -/
CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, CategoryTheory.CategoryStruct.comp T.mor₁ T.mor₂ = 0
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformSpace_comap_precomp' : ∀ {ι : Type u_1} {ι' : Type u_2} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (φ : ι' → ι),
  UniformSpace.comap (fun g i' => g (φ i')) (Pi.uniformSpace fun i' => α (φ i')) =
    ⨅ i', UniformSpace.comap (Function.eval (φ i')) (U (φ i'))
-- Mathlib.Topology.EMetricSpace.Basic
EMetric.secondCountable_of_almost_dense_set : ∀ {α : Type u} [inst : PseudoEMetricSpace α],
  (∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, Metric.closedEBall x ε = Set.univ) → SecondCountableTopology α
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- The `Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self`
for commutative rings.  -/
Submodule.LinearDisjoint.rank_le_one_of_flat_of_self : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Submodule R S},
  M.LinearDisjoint M → ∀ [Module.Flat R ↥M], Module.rank R ↥M ≤ 1
-- Init.Data.List.MinMaxOn
List.maxOn_singleton : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {x : α} {f : α → β}, List.maxOn f [x] ⋯ = x
-- Mathlib.RingTheory.DualNumber
DualNumber.exists_mul_left_or_mul_right : ∀ {K : Type u_2} [inst : DivisionRing K] (a b : DualNumber K), ∃ c, a * c = b ∨ b * c = a
-- Mathlib.Data.Finset.SymmDiff
Finset.symmDiff_eq_union_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), symmDiff s t = s ∪ t ↔ Disjoint s t
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Relation.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {fst snd : S.Arrow} (r : fst.Relation snd) (fst_1 snd_1 : S.Arrow) (r_1 : fst_1.Relation snd_1),
  ({ fst := fst, snd := snd, r := r } = { fst := fst_1, snd := snd_1, r := r_1 }) =
    (fst = fst_1 ∧ snd = snd_1 ∧ r ≍ r_1)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.symm : ∀ {V : Type u} (self : SimpleGraph V), Std.Symm self.Adj
-- Init.Prelude
/-- The unexpander monad, essentially `Syntax → Option α`. The `Syntax` is the `ref`,
and it has the possibility of failure without an error message.
 -/
Lean.PrettyPrinter.UnexpandM : Type → Type
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.range_ofSpan : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  (hs : ⊤ ≤ Submodule.span K s), Set.range ⇑(Module.Basis.ofSpan hs) = ⋯.extend ⋯
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.mem_of_isSumSq : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R} {x : R}, IsSumSq x → x ∈ P
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.leftUnshift_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ : CochainComplex.HomComplex.Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ)
  (hn : n + a = n'), ↑(γ.leftUnshift n hn) = (↑γ).leftUnshift n hn
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpContext.isRetrigger : Lean.Lsp.SignatureHelpContext → Bool
-- Mathlib.MeasureTheory.Function.EssSup
essSup_le_iSup : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : CompleteLattice β]
  {f : α → β}, essSup f μ ≤ ⨆ i, f i
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHomRight : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : D) {y z : C} (f : y ⟶ z)
  [CategoryTheory.IsIso f],
  CategoryTheory.IsIso (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k fallback : α},
  (Std.ExtDTreeMap.filter f t).getKeyD k fallback = ((t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)).getD fallback
-- Mathlib.GroupTheory.Perm.Sign
Equiv.swapCore.eq_1 : ∀ {α : Sort u_1} [inst : DecidableEq α] (a b r : α), Equiv.swapCore a b r = if r = a then b else if r = b then a else r
-- Mathlib.Algebra.BigOperators.Intervals
/-- Telescopic product over `Fin`.  -/
Fin.prod_Icc_div : ∀ {M : Type u_3} [inst : CommGroup M] {n : ℕ} {a b : Fin n},
  a ≤ b → ∀ (f : Fin (n + 1) → M), ∏ i ∈ Finset.Icc a b, f i.succ / f i.castSucc = f b.succ / f a.castSucc
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_zero : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  ∫ (x : ℝ) in a..b, 0 ∂μ = 0
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.isLink_iff_eq : ∀ {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β}, G.IsLink e x y → (G.IsLink e x z ↔ z = y)
-- Std.Data.ExtTreeSet.Basic
/-- Carries out a monadic action on each element in the tree set in ascending order.  -/
Std.ExtTreeSet.forM : {α : Type u} →
  {cmp : α → α → Ordering} →
    {m : Type w → Type w₂} →
      [inst : Monad m] →
        [LawfulMonad m] → [Std.TransCmp cmp] → (α → m PUnit.{w + 1}) → Std.ExtTreeSet α cmp → m PUnit.{w + 1}
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `Div` across an `Equiv`  -/
Equiv.div : {α : Type u_2} → {β : Type u_3} → α ≃ β → [Div β] → Div α
-- Lean.Elab.Parallel
/-- Runs a list of TacticM computations in parallel and collects results in the original order,
discarding state information.

Unlike `par`, this doesn't return state information from tasks.

The final TacticM state is restored to the initial state (before tasks ran).
 -/
Lean.Elab.Tactic.TacticM.par' : {α : Type} → List (Lean.Elab.Tactic.TacticM α) → Lean.Elab.Tactic.TacticM (List (Except Lean.Exception α))
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
conj_circleMap_zero : ∀ (r θ : ℝ), (starRingEnd ℂ) (circleMap 0 r θ) = circleMap 0 r (-θ)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  {k : α} {f : β → β} {hc : k ∈ Std.DTreeMap.Const.modify t k f},
  Std.DTreeMap.Const.get (Std.DTreeMap.Const.modify t k f) k hc = f (Std.DTreeMap.Const.get t k ⋯)
-- Std.Internal.Parsec.Basic
/-- Try `p`, and if it fails without consuming input, run `q ()` instead.
 -/
Std.Internal.Parsec.orElse : {α ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] →
      [Std.Internal.Parsec.Input ι elem idx] →
        Std.Internal.Parsec ι α → (Unit → Std.Internal.Parsec ι α) → Std.Internal.Parsec ι α
-- Mathlib.Order.Heyting.Basic
/-- Pullback a `CoheytingAlgebra` along an injection.  -/
Function.Injective.coheytingAlgebra : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Min α] →
      [inst_1 : Max α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : Bot α] →
              [inst_5 : Top α] →
                [inst_6 : HNot α] →
                  [inst_7 : SDiff α] →
                    [inst_8 : CoheytingAlgebra β] →
                      (f : α → β) →
                        Function.Injective f →
                          (∀ {y x : α}, f y ≤ f x ↔ y ≤ x) →
                            (∀ {y x : α}, f y < f x ↔ y < x) →
                              (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                                (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                                  f ⊤ = ⊤ →
                                    f ⊥ = ⊥ →
                                      (∀ (a : α), f (￢a) = ￢f a) →
                                        (∀ (b a : α), f (b \ a) = f b \ f a) → CoheytingAlgebra α
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.mem_of_mem_nsmul : ∀ {α : Type u_1} {a : α} {s : Multiset α} {n : ℕ}, a ∈ n • s → a ∈ s
-- Mathlib.Order.ConditionallyCompleteLattice.Group
mul_ciSup_le : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : Group α] [MulLeftMono α]
  {a g : α} {h : ι → α}, (∀ (j : ι), g * h j ≤ a) → g * iSup h ≤ a
-- Aesop.Stats.Basic
Aesop.Stats.configParsing : Aesop.Stats → Aesop.Nanos
-- Lean.Declaration
Lean.Constructor.mk : Lean.Name → Lean.Expr → Lean.Constructor
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- Over affine schemes, ideal sheaves are in bijection with ideals of the global sections.  -/
AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine : {X : AlgebraicGeometry.Scheme} →
  [AlgebraicGeometry.IsAffine X] → X.IdealSheafData ≃+*o Ideal ↑(X.presheaf.obj (Opposite.op ⊤))
-- Mathlib.CategoryTheory.EffectiveEpi.Extensive
CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C]
  {α : Type} [inst_2 : Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B),
  CategoryTheory.EffectiveEpi (CategoryTheory.Limits.Sigma.desc π) ↔ CategoryTheory.EffectiveEpiFamily X π
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.Context.compFields : Lean.Elab.ComputedFields.Context → Array Lean.Name
-- Mathlib.Algebra.Order.SuccPred
Order.lt_two_iff : ∀ {α : Type u_1} {x : α} [inst : LinearOrder α] [inst_1 : AddMonoidWithOne α] [SuccAddOrder α] [NoMaxOrder α],
  x < 2 ↔ x ≤ 1
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.comp_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {X Y Z : CategoryTheory.PreZeroHypercover S}
  (f : X.Hom Y) (g : Y.Hom Z) (a : X.I₀), (CategoryTheory.CategoryStruct.comp f g).s₀ a = g.s₀ (f.s₀ a)
-- Mathlib.Condensed.Light.Module
LightCondMod.hom_naturality_apply : ∀ (R : Type u) [inst : Ring R] {X Y : LightCondMod R} (f : X ⟶ Y) {S T : LightProfiniteᵒᵖ} (g : S ⟶ T)
  (x : ↑(X.obj.obj S)),
  (CategoryTheory.ConcreteCategory.hom (f.hom.app T)) ((CategoryTheory.ConcreteCategory.hom (X.obj.map g)) x) =
    (CategoryTheory.ConcreteCategory.hom (Y.obj.map g)) ((CategoryTheory.ConcreteCategory.hom (f.hom.app S)) x)
-- Mathlib.Data.List.OfFn
/-- A special case of `List.ofFn_inj` for when the two functions are indexed by defeq `n`.  -/
List.ofFn_inj : ∀ {α : Type u} {n : ℕ} {f g : Fin n → α}, List.ofFn f = List.ofFn g ↔ f = g
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- The standard error bound for trapezoidal integration on the general interval `[[a, b]]`.  -/
trapezoidal_error_le : ∀ {f : ℝ → ℝ} {a b : ℝ},
  DifferentiableOn ℝ f (Set.uIcc a b) →
    DifferentiableOn ℝ (derivWithin f (Set.uIcc a b)) (Set.uIcc a b) →
      ∀ {ζ : ℝ},
        (∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.uIcc a b) x| ≤ ζ) →
          ∀ {N : ℕ}, 0 < N → |trapezoidal_error f N a b| ≤ |b - a| ^ 3 * ζ / (12 * ↑N ^ 2)
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.AState.mk.sizeOf_spec : ∀ (generalizations : Array (Lean.Expr × Lean.Expr)) (propToProof : Lean.ExprMap Lean.Expr),
  sizeOf { generalizations := generalizations, propToProof := propToProof } =
    1 + sizeOf generalizations + sizeOf propToProof
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.injectiveDimension_eq_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (e : X ≅ Y),
  CategoryTheory.injectiveDimension X = CategoryTheory.injectiveDimension Y
-- Lean.Structure
/-- The name of the field. This is a single-component name.  -/
Lean.StructureFieldInfo.fieldName : Lean.StructureFieldInfo → Lean.Name
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.erase.match_1.eq_2 : ∀ {α : Type u_1} (as : Array α) (motive : Option (Fin as.size) → Sort u_2) (i : Fin as.size) (h_1 : Unit → motive none)
  (h_2 : (i : Fin as.size) → motive (some i)),
  (match some i with
    | none => h_1 ()
    | some i => h_2 i) =
    h_2 i
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.C0_projOrd : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Profinite.NobelingProof.contained C (Order.succ o) →
    ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2) {x : I → Bool},
      x ∈ Profinite.NobelingProof.C0 C ho →
        Profinite.NobelingProof.Proj (fun x => Profinite.NobelingProof.ord I x < o) x = x