mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Composing two formal multilinear series `q` and `p` along an ordered partition extended by a
new atom to the left corresponds to applying `p 1` on the first coordinates, and the initial
ordered partition on the other coordinates.
This is one of the terms that appears when differentiating in the Faa di Bruno
formula, going from step `m` to step `m + 1`.  -/
_private.Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno.0.faaDiBruno_aux1 : ∀ {𝕜 : 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] {m : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
  (p : FormalMultilinearSeries 𝕜 E F) (c : OrderedFinpartition m),
  (q.compAlongOrderedFinpartition p (c.extend none)).curryLeft =
    ((OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c).flipMultilinear fun i => p (c.partSize i)) ∘SL
      (q (c.length + 1)).curryLeft ∘SL (continuousMultilinearCurryFin1 𝕜 E F) (p 1)
-- Init.MetaTypes
/-- Disable eta for structures and classes.  -/
Lean.Meta.EtaStructMode.none : Lean.Meta.EtaStructMode
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point.0.WeierstrassCurve.Projective.Point.toAffine_add_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Nonsingular P →
    W.Nonsingular Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          ¬(P 0 * Q 2 = Q 0 * P 2 ∧ P 1 * Q 2 = W.negY Q * P 2) →
            WeierstrassCurve.Projective.Point.toAffine W
                ![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2)
                    (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                  W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2)
                    (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                  1] =
              WeierstrassCurve.Projective.Point.toAffine W P + WeierstrassCurve.Projective.Point.toAffine W Q
-- Batteries.Data.Char.Basic
/-- Maximum character code point.
(See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).)
 -/
Char.max : ℕ
-- Mathlib.Order.WithBot
WithTop.coe_ne_top : ∀ {α : Type u_1} {a : α}, ↑a ≠ ⊤
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
LaurentPolynomial.comul_T : ∀ {R : Type u_11} [inst : CommSemiring R] {A : Type u_12} [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (n : ℤ),
  CoalgebraStruct.comul (LaurentPolynomial.T n) = LaurentPolynomial.T n ⊗ₜ[R] LaurentPolynomial.T n
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalenceFunctor_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G)
  (g : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G)),
  ((CategoryTheory.StructuredArrow.preEquivalenceFunctor F f).obj g).hom =
    CategoryTheory.StructuredArrow.Hom.right g.hom
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
/-- Cokernel in `TopModuleCat R` is the cokernel of the linear map with the quotient topology.  -/
TopModuleCat.coker : {R : Type u} → [inst : Ring R] → [inst_1 : TopologicalSpace R] → {M N : TopModuleCat R} → (M ⟶ N) → TopModuleCat R
-- Mathlib.Order.Heyting.Hom
BiheytingHom.instBiheytingHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β],
  BiheytingHomClass (BiheytingHom α β) α β
-- Mathlib.Algebra.NeZero
zero_ne_one' : ∀ (α : Type u_2) [inst : Zero α] [inst_1 : One α] [NeZero 1], 0 ≠ 1
-- Init.Tactics
/-- Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
the given tactic.
Like `optParam`, this gadget only affects elaboration.
For example, the tactic will *not* be invoked during type class resolution.  -/
autoParam : Sort u → Lean.Syntax → Sort u
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd : ∀ {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : CategoryTheory.Limits.PullbackCone f g}
  (hc : CategoryTheory.Limits.IsLimit c) (x : CategoryTheory.Limits.Types.PullbackObj f g),
  (CategoryTheory.ConcreteCategory.hom c.snd)
      ((CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj hc).symm x) =
    (↑x).2
-- Init.Data.Range.Polymorphic.NatLemmas
/-- Induction principle for proving properties of `Nat`-based ranges of the form `a<...b` by
varying the lower bound.

In the `base` case, one proves that for any `a : Nat` and `b : Nat` with
`b ≤ a + 1`, the statement holds for the empty range `a<...b`.

In the `step` case, one proves that for any `a : Nat` and `b : Nat`, the
statement holds for nonempty ranges `a<...b` if it holds for the smaller range
`(a + 1)<...b`.

The following is an example reproving `length_toList_roo`.

```
example (a b : Nat) : (a<...b).toList.length = b - a - 1 := by
  induction a, b using Nat.induct_roo_left
  case base =>
    simp only [Nat.toList_roo_eq_nil, List.length_nil, *]; omega
  case step =>
    simp only [Nat.toList_roo_eq_cons, List.length_cons, *]; omega
``` -/
Nat.induct_roo_left : ∀ (motive : ℕ → ℕ → Prop),
  (∀ (a b : ℕ), b ≤ a + 1 → motive a b) →
    (∀ (a b : ℕ), a + 1 < b → motive (a + 1) b → motive a b) → ∀ (a b : ℕ), motive a b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∈ t₂ → (t₁ ∩ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.Data.NNReal.Basic
NNReal.le_iInf_mul : ∀ {ι : Sort u_3} [Nonempty ι] {a : NNReal} {g : ι → NNReal} {h : NNReal}, (∀ (i : ι), a ≤ g i * h) → a ≤ iInf g * h
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.CreatesFiniteProducts.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          autoParam ((J : Type) → [Fintype J] → CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete J) F)
              CategoryTheory.Limits.CreatesFiniteProducts.creates._autoParam →
            CategoryTheory.Limits.CreatesFiniteProducts F
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `f ≫ g = 0` implies `g = 0` for all `g`, then `0 : Y ⟶ 0` is a cokernel of `f`.  -/
CategoryTheory.Limits.zeroCokernelOfZeroCancel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X Y : C} →
          (f : X ⟶ Y) →
            (∀ (Z : C) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0) →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ 0 ⋯)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_zero_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →L[𝕜] F), TensorProduct.mapL f 0 = 0
-- Mathlib.Order.Filter.Extr
IsMaxOn.isExtr : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α}, IsMaxOn f s a → IsExtrOn f s a
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mem_localTrivAsPartialEquiv_target : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι) (p : B × F), p ∈ (Z.localTrivAsPartialEquiv i).target ↔ p.1 ∈ Z.baseSet i
-- Std.Time.DateTime.PlainDateTime
/-- Creates a new `PlainDateTime` by adjusting the `second` component of its `time` to the given value.
 -/
Std.Time.PlainDateTime.withSeconds : Std.Time.PlainDateTime → Std.Time.Second.Ordinal true → Std.Time.PlainDateTime
-- Mathlib.Topology.Category.CompHaus.Basic
CompHaus.instCompactSpaceCarrierToTopTrue : ∀ {X : CompHaus}, CompactSpace ↑X.toTop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → ∀ {h' : k' ∈ Std.TreeMap.unitOfList l cmp}, (Std.TreeMap.unitOfList l cmp).getKey k' h' = k
-- Init.Data.Int.Gcd
Int.gcd_dvd_gcd_of_dvd_left : ∀ {a b : ℤ} (c : ℤ), a ∣ b → a.gcd c ∣ b.gcd c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'] {Z_1 : C} (h : W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso f g g').hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd f (CategoryTheory.CategoryStruct.comp g' g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f g) g')
      h
-- Mathlib.Order.Cover
Prod.wcovBy_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {x y : α × β},
  x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.mulMap_bot_right_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (A : Subalgebra R S), A.mulMap ⊥ = A.val.comp ↑A.rTensorBot
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_left : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan f g)
    AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Finite
Set.infinite_vadd_set : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} {s : Set α},
  (a +ᵥ s).Infinite ↔ s.Infinite
-- Mathlib.CategoryTheory.Action.Basic
Action.comp_hom_assoc : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N K : Action V G}
  (f : M ⟶ N) (g : N ⟶ K) {Z : V} (h : K.V ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
-- Lean.PrettyPrinter.Parenthesizer
/-- Adds necessary parentheses in `stx` parsed by `parser`.
 -/
Lean.PrettyPrinter.parenthesize : Lean.PrettyPrinter.Parenthesizer → Lean.Syntax → Lean.CoreM Lean.Syntax
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `AddMonoidHom.pi_injective`. -/
Pi.addMonoidHom_injective : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → AddZeroClass (f i)] {γ : Type w} [Nonempty I]
  [inst_2 : AddZeroClass γ] (g : (i : I) → γ →+ f i),
  (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(AddMonoidHom.pi g)
-- Lean.Environment
Lean.Environment.instBEqVisibility.beq : Lean.Environment.Visibility → Lean.Environment.Visibility → Bool
-- Mathlib.LinearAlgebra.Dimension.RankNullity
/-- The **rank-nullity theorem**  -/
LinearMap.rank_range_add_rank_ker : ∀ {R : Type u_1} {M M₁ : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₁]
  [inst_3 : Module R M] [inst_4 : Module R M₁] [HasRankNullity.{u, u_1} R] (f : M →ₗ[R] M₁),
  Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R M
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.epi_of_epi_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f : A ⟶ B)
  [h : CategoryTheory.Epi (CategoryTheory.StructuredArrow.Hom.right f)], CategoryTheory.Epi f
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsTree.of_subsingleton : ∀ {V : Type u_1} [Nonempty V] [Subsingleton V] {G : SimpleGraph V}, G.IsTree
-- Mathlib.Algebra.Free
instDecidableEqFreeAddMagma : {α : Type u_1} → [DecidableEq α] → DecidableEq (FreeAddMagma α)
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] {g₁ g₂ : BoundedLatticeHom β γ}
  {f : BoundedLatticeHom α β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Icc_castSucc : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∏ i ∈ Finset.Icc a.castSucc b.castSucc, f i = ∏ i ∈ Finset.Icc a b, f i.castSucc
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.instMetricSpace : {𝕜 : Type u_1} →
  {V : Type u_3} →
    {W : Type u_4} →
      {Q : Type u_6} →
        [inst : NormedAddCommGroup V] →
          [inst_1 : NormedAddCommGroup W] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NormedSpace 𝕜 V] →
                [inst_4 : NormedSpace 𝕜 W] →
                  [inst_5 : MetricSpace Q] → [inst_6 : NormedAddTorsor W Q] → MetricSpace (V →ᴬ[𝕜] Q)
-- Mathlib.Algebra.Star.Module
/-- **Alias** of the reverse direction of `IsIdempotentElem.star_iff`. -/
IsIdempotentElem.star : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] {a : R}, IsIdempotentElem a → IsIdempotentElem (star a)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- We say that `t : Set Y` is an image of `s : Set X` under an open partial homeomorphism `e`
if any of the following equivalent conditions hold:

* `e '' (e.source ∩ s) = e.target ∩ t`;
* `e.source ∩ e ⁻¹ t = e.source ∩ s`;
* `∀ x ∈ e.source, e x ∈ t ↔ x ∈ s` (this one is used in the definition).
 -/
OpenPartialHomeomorph.IsImage : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → OpenPartialHomeomorph X Y → Set X → Set Y → Prop
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- Second projection from the intersection of two pre-`1`-hypercovers.  -/
CategoryTheory.PreOneHypercover.interSnd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreOneHypercover S) →
        (F : CategoryTheory.PreOneHypercover S) →
          [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] →
            [inst_2 :
                ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
                  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
                    (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] →
              (E.inter F).Hom F
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.algebraMap_norm_eq_pow : ∀ {K : Type u_1} {K' : Type u_2} [inst : Field K] [inst_1 : Field K'] [inst_2 : Algebra K K'] [Finite K'] {x : K'},
  (algebraMap K K') ((Algebra.norm K) x) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.IsIPCOfShape.congr_simp : ∀ (ι ι_1 : Type u_3) (e_ι : ι = ι_1) (C : Type u_4) [inst : CategoryTheory.Category.{v_2, u_4} C]
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape ι C],
  CategoryTheory.Limits.IsIPCOfShape.{w, u_3, v_2, u_4} ι C =
    CategoryTheory.Limits.IsIPCOfShape.{w, u_3, v_2, u_4} ι_1 C
-- Std.Data.HashSet.Raw
/-- Returns the number of buckets in the internal representation of the hash set. This function may
be useful for things like monitoring system health, but it should be considered an internal
implementation detail.
 -/
Std.HashSet.Raw.Internal.numBuckets : {α : Type u} → Std.HashSet.Raw α → ℕ
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.ker_inf_lt_ker_inf_of_map_eq_of_lt : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Ring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {p p' : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂},
  p < p' → Submodule.map f p = Submodule.map f p' → f.ker ⊓ p < f.ker ⊓ p'
-- Mathlib.Topology.Algebra.Group.Basic
/-- Given a compact set `K` inside an open set `U`, there is an open neighborhood `V` of
`0` such that `K + V ⊆ U`.  -/
compact_open_separated_add_right : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddZeroClass G] [ContinuousAdd G] {K U : Set G},
  IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ nhds 0, K + V ⊆ U
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_fintype : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] [inst_2 : Fintype α]
  (f : α →₀ M) (g : α → M → N), (∀ (i : α), g i 0 = 0) → f.sum g = ∑ i, g i (f i)
-- Init.Grind.ToInt
Lean.Grind.IntInterval.isFinite.eq_1 : ∀ (lo hi : ℤ), (Lean.Grind.IntInterval.co lo hi).isFinite = true
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- (Implementation) Show the cone constructed in `buildLimit` is limiting, provided the cones used in
its construction are.
 -/
CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        {F : CategoryTheory.Functor J C} →
          {c₁ : CategoryTheory.Limits.Fan F.obj} →
            {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} →
              (s t : c₁.pt ⟶ c₂.pt) →
                (hs :
                    ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
                      CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) =
                        CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) →
                  (ht :
                      ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
                        CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) →
                    {i : CategoryTheory.Limits.Fork s t} →
                      CategoryTheory.Limits.IsLimit c₁ →
                        CategoryTheory.Limits.IsLimit c₂ →
                          CategoryTheory.Limits.IsLimit i →
                            CategoryTheory.Limits.IsLimit
                              (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i)
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
HasStrictFDerivAt.clog : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E},
  HasStrictFDerivAt f f' x → f x ∈ Complex.slitPlane → HasStrictFDerivAt (fun t => Complex.log (f t)) ((f x)⁻¹ • f') x
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.maxInsts.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
/-- The free presheaf of modules functor is left adjoint to the forget functor
`PresheafOfModules.{u} R ⥤ Cᵒᵖ ⥤ Type u`.  -/
PresheafOfModules.freeAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (R : CategoryTheory.Functor Cᵒᵖ RingCat) →
      PresheafOfModules.free R ⊣
        (PresheafOfModules.toPresheaf R).comp
          ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (CategoryTheory.forget Ab))
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nontrivial.mul_left : ∀ {α : Type u_2} [inst : Mul α] [IsLeftCancelMul α] [inst_2 : DecidableEq α] {s t : Finset α},
  t.Nontrivial → s.Nonempty → (s * t).Nontrivial
-- Mathlib.NumberTheory.NumberField.DirichletDensity
/-- If `S` has no Dirichlet density, then `dirichletDensity S = 0`.  -/
NumberField.Set.dirichletDensity_eq_zero_of_not_hasDirichletDensity : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))},
  (∀ (δ : ℝ), ¬NumberField.Set.HasDirichletDensity S δ) → NumberField.Set.dirichletDensity S = 0
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Functor.mapHomologicalComplexCompIso_inv_app_f : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W] [inst_3 : CategoryTheory.Preadditive W] {W' : Type u_5}
  [inst_4 : CategoryTheory.Category.{u_6, u_5} W'] [inst_5 : CategoryTheory.Preadditive W']
  {F : CategoryTheory.Functor V W} {G : CategoryTheory.Functor W W'} {H : CategoryTheory.Functor V W'}
  (e : F.comp G ≅ H) [inst_6 : F.Additive] [inst_7 : G.Additive] [inst_8 : H.Additive] (c : ComplexShape ι)
  (C : HomologicalComplex V c) (x : ι),
  ((CategoryTheory.Functor.mapHomologicalComplexCompIso e c).inv.app C).f x = e.inv.app (C.X x)
-- Mathlib.Data.Nat.Cast.Defs
Nat.binCast_eq : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] (n : ℕ), n.binCast = ↑n
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PartialMatch.mk : Array Lean.Expr → ℕ → Lean.Meta.LazyDiscrTree.TrieIndex → Lean.Meta.LazyDiscrTree.PartialMatch
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
nhds_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] (a : α),
  (nhds a).IsMeasurablyGenerated
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- This is not an instance as it conflicts with `SkewMonoidAlgebra.distribMulAction`
when `G = kˣ`.  -/
SkewMonoidAlgebra.comapDistribMulActionSelf : {k : Type u_1} →
  {G : Type u_2} → [inst : Monoid G] → [inst_1 : AddCommMonoid k] → DistribMulAction G (SkewMonoidAlgebra k G)
-- Init.Data.Array.Lemmas
Array.getElem_append_left : ∀ {α : Type u_1} {i : ℕ} {xs ys : Array α} {h : i < (xs ++ ys).size} (hlt : i < xs.size), (xs ++ ys)[i] = xs[i]
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.eq_of_prod_take_eq : ∀ {M : Type u_4} [inst : LeftCancelMonoid M] {L L' : List M},
  L.length = L'.length → (∀ i ≤ L.length, (List.take i L).prod = (List.take i L').prod) → L = L'
-- Lean.Data.Position
Lean.instInhabitedPosition : Inhabited Lean.Position
-- Mathlib.Algebra.Star.Subalgebra
/-- The centralizer, or commutant, of the star-closure of a set as a star subalgebra.  -/
StarSubalgebra.centralizer : (R : Type u_2) →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : StarRing A] → [inst_4 : Algebra R A] → [inst_5 : StarModule R A] → Set A → StarSubalgebra R A
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁)
      (CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₁ n₁' h₁).hom h) =
    CategoryTheory.CategoryStruct.comp
      (x.negOnePow •
        CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁'))
      h
-- Init.Data.Nat.Basic
Nat.sub_mul : ∀ (n m k : ℕ), (n - m) * k = n * k - m * k