mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.TemperedDistribution
MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : CompleteSpace F] [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E]
  {μ : MeasureTheory.Measure E} [hμ : μ.HasTemperateGrowth] [FiniteDimensional ℝ E]
  [MeasureTheory.IsLocallyFiniteMeasure μ] {p : ENNReal} [hp : Fact (1 ≤ p)],
  (↑(MeasureTheory.Lp.toTemperedDistributionCLM F μ p)).ker = ⊥
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_eq_some_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α}, t.contains k = true → t.getKey? k = some k
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insertC.go.eq_def : ∀ (m : Lean.Grind.CommRing.Mon) (c : ℕ) (k : ℤ) (a : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.insertC.go m c k a =
    match a with
    | Lean.Grind.CommRing.Poly.num k' => Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.num k')
    | Lean.Grind.CommRing.Poly.add k' m' p =>
      match m.grevlex m' with
      | Ordering.eq =>
        have k'' := (k + k') % ↑c;
        bif k'' == 0 then p else Lean.Grind.CommRing.Poly.add k'' m p
      | Ordering.gt => Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.add k' m' p)
      | Ordering.lt => Lean.Grind.CommRing.Poly.add k' m' (Lean.Grind.CommRing.Poly.insertC.go m c k p)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.id' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Grp C), (CategoryTheory.CategoryStruct.id A).hom = CategoryTheory.CategoryStruct.id A.toMon
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.edges_takeUntil_prefix_edges : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.takeUntil u h).edges <+: p.edges
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y}
  {c : C} (i i_1 : F.obj c ⟶ X) (e_i : i = i_1) (h h_1 : c ⟶ a) (e_h : h = h_1)
  (hi : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp (F.map h) g) [inst_2 : F.Full],
  hf.lift i h hi = hf.lift i_1 h_1 ⋯
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.app_bijective_of_stalkFunctor_map_bijective : ∀ {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)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  {F G : TopCat.Sheaf C X} (f : F ⟶ G) (U : TopologicalSpace.Opens ↑X),
  (∀ x ∈ U, Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f.hom))) →
    Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op U)))
-- Init.NotationExtra
unexpandProdMk : Lean.PrettyPrinter.Unexpander
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldr'_algebraMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N)
  (hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx)
  (n : N) (r : R), (CliffordAlgebra.foldr' Q f hf n) ((algebraMap R (CliffordAlgebra Q)) r) = r • n
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsSemilinearSet.empty : ∀ {M : Type u_1} [inst : AddCommMonoid M], IsSemilinearSet ∅
-- Mathlib.Analysis.Calculus.Taylor
/-- The `k`th coefficient of the Taylor polynomial.  -/
taylorCoeffWithin : {E : Type u_2} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℝ → E) → ℕ → Set ℝ → ℝ → E
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedCallHierarchyItem.default : Lean.Lsp.CallHierarchyItem
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.mk_as : ∀ {α : Type u₁} (X : CategoryTheory.Discrete α), { as := X.as } = X
-- Mathlib.Data.Vector3
instInhabitedVector3 : {α : Type u_1} → {n : ℕ} → [Inhabited α] → Inhabited (Vector3 α n)
-- Std.Internal.Do.ExceptPost
/-- Pretty-print `EPost.Cons.mk` as `epost⟨v₁, v₂, ...⟩`.  -/
Std.Internal.Do.unexpandEPostConsMk : Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.isIdempotentElem : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Star R] {p : R}, IsStarProjection p → IsIdempotentElem p
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsSFiniteKernel.map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (f : β → γ),
  ProbabilityTheory.IsSFiniteKernel (κ.map f)
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion_sub : ∀ {h : ℝ} {f g : UpperHalfPlane → ℂ},
  AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0 →
    AnalyticAt ℂ (UpperHalfPlane.cuspFunction h g) 0 →
      UpperHalfPlane.qExpansion h (f - g) = UpperHalfPlane.qExpansion h f - UpperHalfPlane.qExpansion h g
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.isPWO_support' : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] (self : HahnSeries Γ R),
  (Function.support self.coeff).IsPWO
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgEquiv_symm_apply : ∀ {σ : Type u_1} (R : Type u_3) {n : ℕ} [inst : Fintype σ] [inst_1 : CommRing R] (hn : Fintype.card σ = n) (i : Fin n),
  (MvPolynomial.esymmAlgEquiv σ R hn).symm ⟨MvPolynomial.esymm σ R (↑i + 1), ⋯⟩ = MvPolynomial.X i
-- Init.Data.List.MinMaxOn
List.maxOn_replicate : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {n : ℕ} {a : α}
  {f : α → β} (h : List.replicate n a ≠ []), List.maxOn f (List.replicate n a) h = a
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Ideal.ResidueField.exists_smul_eq_tmul_one : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (x : TensorProduct R S p.ResidueField), ∃ r ∉ p, ∃ s, r • x = s ⊗ₜ[R] 1
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.Valid.validFor : ∀ {it : String.Legacy.Iterator}, it.Valid → ∃ l r, String.Legacy.Iterator.ValidFor l r it
-- Init.Data.SInt.Lemmas
Int64.ofIntLE.eq_1 : ∀ (i : ℤ) (_hl : Int64.minValue.toInt ≤ i) (_hr : i ≤ Int64.maxValue.toInt), Int64.ofIntLE i _hl _hr = Int64.ofInt i
-- Mathlib.Algebra.Algebra.Unitization
Unitization.mk.injEq : ∀ {R : Type u_1} {A : Type u_2} (toProd toProd_1 : R × A),
  (Unitization.mk toProd = Unitization.mk toProd_1) = (toProd = toProd_1)
-- Mathlib.Data.List.Basic
List.surjective_head? : ∀ {α : Type u}, Function.Surjective List.head?
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.instIsClosedUnderIsomorphismsHeart : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), t.heart.IsClosedUnderIsomorphisms
-- Mathlib.AlgebraicGeometry.Cover.Directed
/-- If `𝒰` is a directed open cover of `X`, to glue morphisms `{gᵢ : 𝒰ᵢ ⟶ Y}` it suffices
to check compatibility with the transition maps.
See `OpenCover.isColimitCoconeOfLocallyDirected` for this result stated in the language of
colimits.
 -/
AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirected : {X : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    [inst : CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] →
      [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
        {Y : AlgebraicGeometry.Scheme} →
          (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y) →
            (∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
                CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i) →
              (X ⟶ Y)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.posPart : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : AddGroup β] [inst_2 : Lattice β] [ContinuousSup β],
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => (f x)⁺) μ
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If a function is `C^n` with `n ≠ 0` around a point, and its derivative at that point is given to
us as `f'`, then `f'` is also a strict derivative.  -/
ContDiffAt.hasStrictFDerivAt' : ∀ {n : WithTop ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E']
  [inst_2 : NormedSpace 𝕂 E'] {F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F'] {f : E' → F'}
  {f' : E' →L[𝕂] F'} {x : E'}, ContDiffAt 𝕂 n f x → HasFDerivAt f f' x → n ≠ 0 → HasStrictFDerivAt f f' x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.add_neg_rev_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : C) [inst_3 : CategoryTheory.AddGrpObj G] {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg)
      (CategoryTheory.CategoryStruct.comp (β_ G G).hom
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h))
-- Init.Data.ByteArray.Basic
ByteArray.findIdx?.loop.eq_def : ∀ (a : ByteArray) (p : UInt8 → Bool) (i : ℕ),
  ByteArray.findIdx?.loop a p i =
    if h : i < a.size then if p a[i] = true then some i else ByteArray.findIdx?.loop a p (i + 1) else none
-- Init.Meta.Defs
Lean.Meta.ApplyNewGoals.nonDependentFirst : Lean.Meta.ApplyNewGoals
-- Mathlib.Algebra.GroupWithZero.Hom
/-- Given two monoid with zero morphisms `f`, `g` to a commutative monoid with zero, `f * g` is the
monoid with zero morphism sending `x` to `f x * g x`.  -/
MonoidWithZeroHom.instMul : {α : Type u_2} → [inst : MulZeroOneClass α] → {β : Type u_7} → [inst_1 : CommMonoidWithZero β] → Mul (α →*₀ β)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.isEmpty_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.Equiv t₂ → t₁.isEmpty = t₂.isEmpty
-- Mathlib.RepresentationTheory.Action
Representation.linearize_apply : ∀ (k : Type u) (G : Type v) [inst : Monoid G] [inst_1 : Semiring k] (X : Action (Type w) G) (g : G),
  (Representation.linearize k G X) g =
    MonoidAlgebra.mapDomainLinearMap k k ⇑(CategoryTheory.ConcreteCategory.hom (X.ρ g))
-- Init.Omega.Constraint
Lean.Omega.Constraint.isImpossible.eq_1 : ∀ (x_1 y : ℤ), { lowerBound := some x_1, upperBound := some y }.isImpossible = decide (y < x_1)
-- Batteries.Control.Lemmas
ReaderT.run_throwThe : ∀ {ε : Type u_1} {m : Type u_2 → Type u_3} {ρ α : Type u_2} [inst : MonadExceptOf ε m] (e : ε) (ctx : ρ),
  (throwThe ε e).run ctx = throwThe ε e
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkCoinductiveAux₁.eq_3 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0) (one : P.X 2 ⟶ Q.X 1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X (n + 1) ⟶ Q.X n) ×'
            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'')
  (n : ℕ),
  Homotopy.mkCoinductiveAux₁ e zero one comm_one succ n.succ.succ =
    ⟨(Homotopy.mkCoinductiveAux₁ e zero one comm_one succ (n + 1)).snd.fst,
      ⟨(succ (n + 1) (Homotopy.mkCoinductiveAux₁ e zero one comm_one succ (n + 1))).fst, ⋯⟩⟩
-- Mathlib.Order.Partition.Finpartition
Finpartition.parts_bot : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), ⊥.parts = Finset.map { toFun := singleton, inj' := ⋯ } s
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.exact₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ComposableArrows C 0), S.Exact
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.image_le_opensRange : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
DifferentiableAt.comp_mdifferentiableAt : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {F' : Type u_11} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F'] {g : F → F'}
  {f : M → F} {x : M}, DifferentiableAt 𝕜 g (f x) → MDiffAt f x → MDiffAt (g ∘ f) x
-- Mathlib.AlgebraicGeometry.Modules.Presheaf
/-- The category of presheaves of modules over a scheme.  -/
AlgebraicGeometry.Scheme.PresheafOfModules : AlgebraicGeometry.Scheme → Type (u + 1)
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- A conditionally complete linear order with `Bot` is a linear order with least element, in which
every nonempty subset which is bounded above has a supremum, and every nonempty subset (necessarily
bounded below) has an infimum.  A typical example is the natural numbers.

To differentiate the statements from the corresponding statements in (unconditional)
complete linear orders, we prefix `sInf` and `sSup` by a `c` everywhere. The same statements should
hold in both worlds, sometimes with additional assumptions of nonemptiness or
boundedness.  -/
ConditionallyCompleteLinearOrderBot : Type u_5 → Type u_5
-- Mathlib.Topology.Sets.BaseChangeNhds
TopologicalSpace.Compacts.instInitialElemOpensOpenRcNhdsCompactNhdsFunctorOfT2Space : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K : TopologicalSpace.Compacts α} [T2Space α], ⋯.functor.Initial
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.AndKind.and : Mathlib.Tactic.ITauto.AndKind
-- Init.Data.List.Basic
List.intersperse_cons₂ : ∀ {α : Type u} {x y : α} {zs : List α} {sep : α},
  List.intersperse sep (x :: y :: zs) = x :: sep :: List.intersperse sep (y :: zs)
-- Mathlib.Order.CompleteBooleanAlgebra
iInf_sup_iInf : ∀ {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α},
  (⨅ i, f i) ⊔ ⨅ j, g j = ⨅ i, f i.1 ⊔ g i.2
-- Mathlib.Condensed.Limits
instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology : ∀ {A : Type u_1} {J : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J] [CategoryTheory.Limits.HasColimitsOfShape J A]
  [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) A],
  CategoryTheory.Limits.HasColimitsOfShape J (Condensed A)
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- An arbitrary choice of a finite presentation of a finitely presented algebra.  -/
Algebra.Presentation.ofFinitePresentation : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          [inst_3 : Algebra.FinitePresentation R S] →
            Algebra.Presentation R S (Fin (Algebra.Presentation.ofFinitePresentationVars R S))
              (Fin (Algebra.Presentation.ofFinitePresentationRels R S))
-- Std.Sync.RecursiveMutex
_private.Std.Sync.RecursiveMutex.0.Std.RecursiveMutexImpl : NonemptyType
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.invOfUnit_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] (φ : MvPowerSeries σ R) (u : Rˣ),
  MvPowerSeries.constantCoeff φ = ↑u → φ.invOfUnit u * φ = 1
-- Init.Data.SInt.Lemmas
Int8.toInt64_ofInt : ∀ {n : ℤ}, Int8.minValue.toInt ≤ n → n ≤ Int8.maxValue.toInt → (Int8.ofInt n).toInt64 = Int64.ofInt n
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The `Functor.Monoidal` structure given by a lax monoidal functor such
that `ε` and `μ` are isomorphisms.  -/
CategoryTheory.Functor.Monoidal.ofLaxMonoidal : {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) →
              [inst_4 : F.LaxMonoidal] →
                [CategoryTheory.IsIso (CategoryTheory.Functor.LaxMonoidal.ε F)] →
                  [∀ (X Y : C), CategoryTheory.IsIso (CategoryTheory.Functor.LaxMonoidal.μ F X Y)] → F.Monoidal
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
SSet.StrictSegal.isRightKanExtension : ∀ {X : SSet} (sx : X.StrictSegal),
  CategoryTheory.Functor.IsRightKanExtension X
    (CategoryTheory.CategoryStruct.id ((SimplexCategory.Truncated.inclusion 2).op.comp X))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_of_contains_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α}, (Std.ExtTreeMap.filter f t).contains k = true → t.contains k = true
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.im_smul : ∀ {R : Type u_1} {S : Type u_2} {a b : R} [inst : SMul S R] (s : S) (z : QuadraticAlgebra R a b), (s • z).im = s • z.im
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The equivariant map on `SubMulAction.ofFixingSubgroup` given a set inclusion.  -/
SubMulAction.ofFixingSubgroup_of_inclusion : (M : Type u_1) →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        {s t : Set α} →
          (hst : t ⊆ s) →
            ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[⇑(Subgroup.inclusion ⋯)] ↥(SubMulAction.ofFixingSubgroup M t)
-- Init.Data.Array.Attach
Array.find?_subtype : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Option.map Subtype.val (Array.find? f xs) = Array.find? g xs.unattach
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_of_isOpen : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, IsOpen s → x ∈ s → derivWithin f s x = deriv f x
-- Mathlib.Order.Sublattice
Sublattice.map_le_iff_le_comap : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} {f : LatticeHom α β}
  {M : Sublattice β}, Sublattice.map f L ≤ M ↔ L ≤ Sublattice.comap f M
-- Mathlib.Topology.Semicontinuity.Basic
LowerSemicontinuous.sup : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β},
  LowerSemicontinuous f → LowerSemicontinuous g → LowerSemicontinuous fun x => max (f x) (g x)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.isZero_zero : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : Nontrivial ↥(LieModule.genWeightSpace M 0)], LieModule.Weight.IsZero 0
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
/-- When `f₁`, `f₂` and `f₃` are composable morphisms, this is the exact sequence
`Z^n(f₁ ≫ f₂, f₃) ⟶ Z^n(f₂, f₃) ⟶ opZ^{n+1}(f₁, f₂) ⟶ opZ^{n+1}(f₁, f₂ ≫ f₃)`.  -/
CategoryTheory.Abelian.SpectralObject.sequenceΨ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (f₁₂ : i ⟶ k) →
                      CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂ →
                        (f₂₃ : j ⟶ l) →
                          CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃ →
                            (n₀ n₁ : ℤ) →
                              autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sequenceΨ._auto_1 →
                                CategoryTheory.ComposableArrows C 3
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.instIsTwoSidedTop : ∀ {α : Type u} [inst : Semiring α], ⊤.IsTwoSided
-- Mathlib.Algebra.PresentedMonoid.Basic
_private.Mathlib.Algebra.PresentedMonoid.Basic.0.PresentedMonoid.termP₁ : Lean.ParserDescr
-- Init.Data.BitVec.Lemmas
BitVec.length_pos_of_ne : ∀ {w : ℕ} {x y : BitVec w}, x ≠ y → 0 < w
-- Mathlib.Data.List.Count
List.countP_diff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ : List α},
  l₂.Subperm l₁ → ∀ (p : α → Bool), List.countP p (l₁.diff l₂) = List.countP p l₁ - List.countP p l₂
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.keys.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.Internal.List.keys [] = []
-- Mathlib.Order.Filter.AtTopBot.Finset
/-- Every finset is eventually a subset of `s` along `atTop`.  -/
Filter.eventually_finset_atTop_subset : ∀ {α : Type u_3} (i : Finset α), ∀ᶠ (s : Finset α) in Filter.atTop, i ⊆ s
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.card_biUnion_le_card_mul : ∀ {ι : Type u_1} {β : Type u_3} [inst : DecidableEq β] (s : Finset ι) (f : ι → Finset β) (n : ℕ),
  (∀ a ∈ s, (f a).card ≤ n) → (s.biUnion f).card ≤ s.card * n
-- ImportGraph.Tools.MinImports
/-- Try to compute a minimal set of imports for this file,
by analyzing the declarations.

This must be run at the end of the file,
and is not aware of syntax and tactics,
so the results will likely need to be adjusted by hand.
 -/
«command#min_imports» : Lean.ParserDescr
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.List.getElem?_zipWithAll.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          (Unit → motive none none) →
            ((a? : Option α) → (b? : Option β) → (a? = none → b? = none → False) → motive a? b?) → motive x x_1
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.isPlausibleIndirectOutput_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] {it : Std.Iter α} {out : α},
  it.IsPlausibleIndirectOutput out ↔
    ∃ n, (it.internalState.next.bind fun x => Std.PRange.succMany? n x) = some out ∧ out ≤ it.internalState.upperBound