mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_insertIfNewₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {b : β a},
      (Std.DHashMap.Internal.toListModel (↑(m.insertIfNewₘ a b)).buckets).Perm
        (Std.Internal.List.insertEntryIfNew a b (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Real.neg_one_le_sinc : ∀ (x : ℝ), -1 ≤ Real.sinc x
-- Mathlib.NumberTheory.Padics.RingHoms
/-- A ring hom from `ℤ_[p]` to `ZMod (p^n)`, with underlying function `PadicInt.appr n`.  -/
PadicInt.toZModPow : {p : ℕ} → [hp_prime : Fact (Nat.Prime p)] → (n : ℕ) → ℤ_[p] →+* ZMod (p ^ n)
-- Lean.Elab.AssertExists
/-- Defines the `assertExistsExt` extension for adding a `HashSet` of `AssertExists` entries
to the environment.  -/
Lean.Elab.Command.assertExistsExt : Lean.SimplePersistentEnvExtension Lean.Elab.Command.AssertExists (Std.HashSet Lean.Elab.Command.AssertExists)
-- Init.Data.UInt.Bitwise
UInt32.toUInt8_and : ∀ (a b : UInt32), (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
AbsoluteValue.sum_le : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  [IsOrderedRing S] (abv : AbsoluteValue R S) (s : Finset ι) (f : ι → R), abv (∑ i ∈ s, f i) ≤ ∑ i ∈ s, abv (f i)
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.three_le_nValue : ∀ {N : ℕ}, 64 ≤ N → 3 ≤ Behrend.nValue N
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
OrderIso.map_ciInf_of_directed : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α]
  [inst_1 : ConditionallyCompletePartialOrderInf β] [Nonempty ι] (e : α ≃o β) {f : ι → α},
  Directed (fun x1 x2 => x2 ≤ x1) f → BddBelow (Set.range f) → e (⨅ i, f i) = ⨅ i, e (f i)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- The affine equivalence given by reflection about the point `x`.
This is `Equiv.pointReflection` as an `AffineEquiv`.  -/
AffineEquiv.pointReflection : (k : Type u_1) →
  {P₁ : Type u_2} →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] → [inst_2 : Module k V₁] → [inst_3 : AddTorsor V₁ P₁] → P₁ → P₁ ≃ᵃ[k] P₁
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `hasFiniteSupport_of_finsum_eq_one`. -/
finite_support_of_finsum_eq_one : ∀ {α : Type u_1} {R : Type u_7} [inst : NonAssocSemiring R] {f : α → R},
  ∑ᶠ (i : α), f i = 1 → Function.HasFiniteSupport f
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind : Repr Lean.Meta.Grind.NormalizePattern.PatternArgKind
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.functorProdToProdFunctor_obj : ∀ (A : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (C : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A (B × C)),
  (CategoryTheory.functorProdToProdFunctor A B C).obj F =
    (F.comp (CategoryTheory.Prod.fst B C), F.comp (CategoryTheory.Prod.snd B C))
-- Mathlib.Topology.Connected.TotallyDisconnected
Topology.IsCoinducing.connectedComponentsMap_bijective : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Topology.IsCoinducing f), (∀ (y : β), IsConnected (f ⁻¹' {y})) → Function.Bijective ⋯.connectedComponentsMap
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
/-- A continuous function with compact support on a product space is measurable for the product
sigma-algebra. The subtlety is that we do not assume that the spaces are separable, so the
product of the Borel sigma algebras might not contain all open sets, but still it contains enough
of them to approximate compactly supported continuous functions.  -/
HasCompactSupport.measurable_of_prod : ∀ {X : Type u_3} {Y : Type u_4} {α : Type u_5} [inst : Zero α] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : MeasurableSpace X] [inst_4 : MeasurableSpace Y] [OpensMeasurableSpace X]
  [OpensMeasurableSpace Y] [inst_7 : TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
  [inst_9 : MeasurableSpace α] [BorelSpace α] {f : X × Y → α}, Continuous f → HasCompactSupport f → Measurable f
-- Init.Data.Vector.Range
Vector.range'_zero : ∀ {s step : ℕ}, Vector.range' s 0 step = #v[]
-- Mathlib.NumberTheory.Transcendental.Liouville.Basic
/-- **Liouville's Theorem**  -/
Liouville.transcendental : ∀ {x : ℝ}, Liouville x → Transcendental ℤ x
-- Mathlib.Algebra.GroupWithZero.Units.Basic
inv_mul_eq_inv_mul_iff : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a b c d : G₀}, b ≠ 0 → d ≠ 0 → (b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionIdentifier.const : Lean.Name → Lean.Lsp.CompletionIdentifier
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
/-- Radius such that distinct points of `carrier` are separated by more than `r`.  -/
Delone.DeloneSet.packingRadius : {X : Type u_3} → [inst : MetricSpace X] → Delone.DeloneSet X → NNReal
-- Aesop.Frontend.Attribute
Aesop.Frontend.Parser.Aesop.attr_rules.quot : Lean.ParserDescr
-- Mathlib.Data.EReal.Operations
EReal.sub_top : ∀ (x : EReal), x - ⊤ = ⊥
-- Mathlib.Analysis.Complex.Poisson
/-- The Herglotz-Riesz kernel of integration.
 -/
herglotzRieszKernel : ℂ → ℂ → ℂ → ℂ
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.of_zpow : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, (f ^ n).SameCycle x y → f.SameCycle x y
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_diff_eq_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (∀ a ∈ m₁, a ∉ m₂) → (m₁ \ m₂).size = m₁.size
-- Mathlib.Data.List.Perm.Basic
_private.Mathlib.Data.List.Perm.Basic.0.List.«term_∘r_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.instVAdd.eq_1 : ∀ {α : Type u_4} {M : Type u_5} [inst : AddZeroClass M] [inst_1 : VAdd α M] [inst_2 : VAddAssocClass α M M]
  (c : AddCon M), c.instVAdd = { vadd := fun a => Quotient.map' (fun x => a +ᵥ x) ⋯ }
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.const.injEq : ∀ (declName : Lean.Name) (nargs : ℕ) (declName_1 : Lean.Name) (nargs_1 : ℕ),
  (Lean.Meta.RefinedDiscrTree.Key.const declName nargs = Lean.Meta.RefinedDiscrTree.Key.const declName_1 nargs_1) =
    (declName = declName_1 ∧ nargs = nargs_1)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- In the setting of `MeromorphicOn.extract_zeros_poles`, the function `log ‖f‖` is equivalent, modulo
equality on codiscrete subsets, to `∑ᶠ u, (divisor f U u * log ‖· - u‖) + log ‖g ·‖`.
 -/
MeromorphicOn.extract_zeros_poles_log : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f g : 𝕜 → E} {D : Function.locallyFinsuppWithin U ℤ},
  (∀ (u : ↑U), g ↑u ≠ 0) →
    f =ᶠ[Filter.codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x => x - u) ^ D u) • g →
      (fun x => Real.log ‖f x‖) =ᶠ[Filter.codiscreteWithin U]
        (∑ᶠ (u : 𝕜), fun x => ↑(D u) * Real.log ‖x - u‖) + fun x => Real.log ‖g x‖
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst_sum : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ι : Type u_4}
  (μ : ι → MeasureTheory.Measure (α × β)),
  (MeasureTheory.Measure.sum μ).fst = MeasureTheory.Measure.sum fun n => (μ n).fst
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
ContinuousMapZero.aeStronglyMeasurable_mkD_restrict_of_uncurry : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] {t : Set Y} [CompactSpace ↑t] [inst_4 : Zero ↑t]
  [inst_5 : TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(↑t, E)] (f : X → Y → E)
  (g : ContinuousMapZero (↑t) E),
  ContinuousOn (Function.uncurry f) (Set.univ ×ˢ t) →
    (∀ᵐ (x : X) ∂μ, f x ↑0 = 0) →
      MeasureTheory.AEStronglyMeasurable (fun x => ContinuousMapZero.mkD (t.domRestrict (f x)) g) μ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k k' : α}, t.WF → t.getKey? k = some k' → (Std.TreeMap.Raw.map f t)[k]? = Option.map (f k') t[k]?
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_id_eq_sInf : ∀ {α : Type u_2} [inst : CompleteLattice α] (s : Finset α), s.inf id = sInf ↑s
-- Mathlib.ModelTheory.Order
FirstOrder.Language.dlo.eq_1 : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered],
  L.dlo = L.linearOrderTheory ∪ {L.noTopOrderSentence, L.noBotOrderSentence, L.denselyOrderedSentence}
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_pos_iff_ne_zero : ∀ {x : ENNReal}, 0 < ↑x ↔ x ≠ 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.one_lt_coe : ∀ {α : Type u} [inst : One α] [inst_1 : LT α] {a : α}, 1 < ↑a ↔ 1 < a
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.homEquiv_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.ComposableArrows C 0),
  CategoryTheory.nerve.homEquiv (SSet.Edge.id x) = CategoryTheory.CategoryStruct.id (CategoryTheory.nerveEquiv x)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.ε₁_ε₂ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] {i₁ i₁' : I₁} {i₂ i₂' : I₂},
  c₁.Rel i₁ i₁' →
    c₂.Rel i₂ i₂' → c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁, i₂) = -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_preimage_of_injective : ∀ {α β : Type u} (f : α → β) (s : Set β), Function.Injective f → Cardinal.mk ↑(f ⁻¹' s) ≤ Cardinal.mk ↑s
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
/-- `Complex.arg ∘ (↑)` and `Circle.exp` define a partial equivalence between `Circle` and `ℝ`
with `source = Set.univ` and `target = Set.Ioc (-π) π`.  -/
Circle.argPartialEquiv : PartialEquiv Circle ℝ
-- Mathlib.Order.DirSupClosed
/-- **Alias** of the forward direction of `dirSupInaccOn_compl`. -/
DirSupClosedOn.of_compl : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α], DirSupInaccOn D sᶜ → DirSupClosedOn D s
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
lowerHemicontinuous_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  (LowerHemicontinuous fun x => {f x}) ↔ Continuous f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.maxKey!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.Equiv t₂ → t₁.maxKey! = t₂.maxKey!
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.decidableEq : (J : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {j k : CategoryTheory.Bicone J} → DecidableEq (CategoryTheory.BiconeHom J j k)
-- Mathlib.Algebra.Module.Submodule.EqLocus
LinearMap.eqLocus_eq_ker_sub : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f g : M →ₛₗ[τ₁₂] M₂), f.eqLocus g = (f - g).ker
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_setWidth' : ∀ {w v : ℕ} (x : BitVec w) (i : ℕ) (h : w ≤ v), (BitVec.setWidth' h x)[i]? = if i < v then some (x.getLsbD i) else none
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
_private.Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord.0.NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral_aux : ∀ {K : Type u_1} [inst : Field K] {A : Set (NumberField.mixedEmbedding.mixedSpace K)},
  NumberField.mixedEmbedding.normAtAllPlaces ⁻¹' NumberField.mixedEmbedding.normAtAllPlaces '' A = A →
    NumberField.mixedEmbedding.normAtAllPlaces '' A ∩ ⋂ w, {x | x ↑w ≠ 0} =
      NumberField.mixedEmbedding.normAtComplexPlaces '' NumberField.mixedEmbedding.plusPart A
-- Init.Data.Array.Attach
/-- “Attaches” the proof that the elements of `xs` are in fact elements of `xs`, producing a new array with
the same elements but in the subtype `{ x // x ∈ xs }`.

`O(1)`.

This function is primarily used to allow definitions by [well-founded
recursion](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=well-founded-recursion) that use higher-order functions (such as
`Array.map`) to prove that an value taken from a list is smaller than the list. This allows the
well-founded recursion mechanism to prove that the function terminates.
 -/
Array.attach : {α : Type u_1} → (xs : Array α) → Array { x // x ∈ xs }
-- Mathlib.Order.CompactlyGenerated.Basic
/-- See [Lemma 5.1][calugareanu].  -/
isAtomistic_of_complementedLattice : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] [ComplementedLattice α],
  IsAtomistic α
-- Batteries.Data.List.Interleave
_private.Batteries.Data.List.Interleave.0.List.interleave.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (l₂ : List α) (h_1 : (l₂ : List α) → motive [] l₂)
  (h_2 : (a : α) → (l₁ l₂ : List α) → motive (a :: l₁) l₂),
  (match [], l₂ with
    | [], l₂ => h_1 l₂
    | a :: l₁, l₂ => h_2 a l₁ l₂) =
    h_1 l₂
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.prod_one : ∀ {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Finset α}, (∀ x ∈ s, f x ≡ 1 [MOD n]) → ∏ x ∈ s, f x ≡ 1 [MOD n]
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_biprod_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  P (X ⊞ Y) → P X
-- Std.Data.Internal.List.Associative
Std.Internal.List.guard_eq_map : ∀ {α : Type u} {β : α → Type v} (p : (a : α) × β a → Prop) [inst : DecidablePred p],
  (Option.guard fun b => decide (p b)) = fun x => Option.map (fun y => ⟨x.fst, y⟩) (if p x then some x.snd else none)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Commutativity of the `L^p` product as a linear isometric equivalence.  -/
LinearIsometryEquiv.withLpProdComm : (p : ENNReal) →
  (𝕜 : Type u_1) →
    (α : Type u_2) →
      (β : Type u_3) →
        [hp : Fact (1 ≤ p)] →
          [inst : Semiring 𝕜] →
            [inst_1 : SeminormedAddCommGroup α] →
              [inst_2 : Module 𝕜 α] →
                [inst_3 : SeminormedAddCommGroup β] → [inst_4 : Module 𝕜 β] → WithLp p (α × β) ≃ₗᵢ[𝕜] WithLp p (β × α)
-- Std.Time.DateTime.Timestamp
_private.Std.Time.DateTime.Timestamp.0.Std.Time.Timestamp.mk : Std.Time.Duration → Std.Time.Timestamp
-- Lean.Meta.Sym.ReplaceS
Lean.Meta.Sym.replaceS : Lean.Expr →
  (Lean.Expr → ℕ → Lean.Meta.Sym.Internal.AlphaShareBuilderM (Option Lean.Expr)) → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- An alternative statement of the Stone-Weierstrass theorem,
for those who like their epsilons.

If `A` is a subalgebra of `C(X, ℝ)` which separates points (and `X` is compact),
every real-valued continuous function on `X` is within any `ε > 0` of some element of `A`.
 -/
ContinuousMap.exists_mem_subalgebra_near_continuousMap_of_separatesPoints : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)),
  A.SeparatesPoints → ∀ (f : C(X, ℝ)) (ε : ℝ), 0 < ε → ∃ g, ‖↑g - f‖ < ε
-- Init.Data.SInt.Basic
instToStringInt16 : ToString Int16
-- Init.Data.List.Nat.TakeDrop
List.getElem_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l : List α} {l' : List β} {i : ℕ}
  {h : i < (List.zipWith f l l').length}, (List.zipWith f l l')[i] = f l[i] l'[i]
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.toConstProdLinearMap_apply : ∀ (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddCommGroup V2] [inst_3 : Module k V1] [inst_4 : Module k V2] [inst_5 : Semiring R] [inst_6 : Module R V2]
  [inst_7 : SMulCommClass k R V2] (f : V1 →ᵃ[k] V2), (AffineMap.toConstProdLinearMap R) f = (f 0, f.linear)
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d._auto_5),
  CategoryTheory.CategoryStruct.comp
      (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)
      (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) =
    0
-- Mathlib.CategoryTheory.Pi.Monoidal
/-- The internal hom functor `X ⟶[∀ i, C i] -`  -/
CategoryTheory.Pi.ihom : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [(i : I) → CategoryTheory.MonoidalClosed (C i)] →
          ((i : I) → C i) → CategoryTheory.Functor ((i : I) → C i) ((i : I) → C i)
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDeriv_comp_three : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {g f : 𝕜 → 𝕜} {x : 𝕜},
  ContDiffAt 𝕜 3 g (f x) →
    ContDiffAt 𝕜 3 f x →
      iteratedDeriv 3 (g ∘ f) x =
        iteratedDeriv 3 g (f x) * deriv f x ^ 3 + 3 * iteratedDeriv 2 g (f x) * iteratedDeriv 2 f x * deriv f x +
          deriv g (f x) * iteratedDeriv 3 f x
-- Mathlib.LinearAlgebra.LinearPMap
/-- The (semi)linear map as just a function.  -/
LinearPMap.toFun' : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → (f : E →ₛₗ.[σ] F) → ↥f.domain → F
-- Batteries.Lean.HashSet
Std.HashSet.instBEq_batteries : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → BEq (Std.HashSet α)
-- Mathlib.RingTheory.LocalProperties.Submodule
/-- Let `N₁ N₂ : Submodule R M`. If the localization of `N₁` at each maximal ideal `P` is
included in the localization of `N₂` at `P`, then `N₁ ≤ N₂`.  -/
Submodule.le_of_localization_maximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_5 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_5 : ∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] {N₁ N₂ : Submodule R M},
  (∀ (P : Ideal R) [inst_6 : P.IsMaximal],
      Submodule.localized₀ P.primeCompl (f P) N₁ ≤ Submodule.localized₀ P.primeCompl (f P) N₂) →
    N₁ ≤ N₂
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.NatTrans.sum_app_inr : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {F G : CategoryTheory.Functor A B} {H I : CategoryTheory.Functor C D}
  (α : F ⟶ G) (β : H ⟶ I) (c : C),
  (CategoryTheory.NatTrans.sum α β).app (Sum.inr c) = (CategoryTheory.Sum.inr_ B D).map (β.app c)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom.id.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] (a : B),
  sizeOf (CategoryTheory.FreeBicategory.Hom.id a) = 1 + sizeOf a
-- Mathlib.Tactic.Ring.Basic
/-- Raise a rational number expression to the power of a natural number.

Fails if the exponent is not a literal.  -/
Mathlib.Tactic.Ring.RingCompute.pow : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {a : Q(«$α»)} →
        {b : Q(ℕ)} →
          Mathlib.Tactic.Ring.RatCoeff a →
            Mathlib.Tactic.Ring.Common.ExProdNat q(«$b») →
              OptionT Lean.MetaM (Mathlib.Tactic.Ring.Common.Result Mathlib.Tactic.Ring.RatCoeff q(«$a» ^ «$b»))
-- Lean.Parser.Command
Lean.Parser.Command.instance : Lean.Parser.Parser
-- Mathlib.Algebra.Module.LocalizedModule.Basic
_private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.example_oreLocalizationInstAlgebra_eq_localizedModuleAlgebra' : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R}, OreLocalization.instAlgebra = LocalizedModule.algebra'
-- Mathlib.Data.Set.Card
Set.encard_preimage_val_le_encard_left : ∀ {α : Type u_1} (P Q : Set α), (Subtype.val ⁻¹' Q).encard ≤ P.encard
-- Lean.Server.Rpc.RequestHandling
Lean.Server.handleRpcCall : Lean.Lsp.RpcCallParams → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Json)
-- Init.Tactics
/-- Rotate the goals to the right by `n`. That is, take the goal at the back
and push it to the front `n` times. If `n` is omitted, it defaults to `1`.
 -/
Lean.Parser.Tactic.rotateRight : Lean.ParserDescr
-- Mathlib.Data.Finsupp.Weight
Finsupp.weight_eq_sum : ∀ {σ : Type u_1} {M : Type u_2} {R : Type u_3} [inst : Semiring R] (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Fintype σ] (f : σ →₀ R), (Finsupp.weight w) f = ∑ i, f i • w i
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.monomial_comp : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R} (n : ℕ),
  ((Polynomial.monomial n) a).comp p = Polynomial.C a * p ^ n
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.mk.injEq : ∀ {R : Type u_5} [inst : CommSemiring R] {A : Type u_6} {B : Type u_7} [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (toCoalgHom : A →ₗc[R] B) (invFun : B → A)
  (left_inv : autoParam (Function.LeftInverse invFun toCoalgHom.toFun) Equiv.left_inv._autoParam)
  (right_inv : autoParam (Function.RightInverse invFun toCoalgHom.toFun) Equiv.right_inv._autoParam)
  (toCoalgHom_1 : A →ₗc[R] B) (invFun_1 : B → A)
  (left_inv_1 : autoParam (Function.LeftInverse invFun_1 toCoalgHom_1.toFun) Equiv.left_inv._autoParam)
  (right_inv_1 : autoParam (Function.RightInverse invFun_1 toCoalgHom_1.toFun) Equiv.right_inv._autoParam),
  ({ toCoalgHom := toCoalgHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toCoalgHom := toCoalgHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }) =
    (toCoalgHom = toCoalgHom_1 ∧ invFun = invFun_1)
-- Mathlib.Tactic.Tauto
/-- `tauto` proves tautologies in classical propositional logic.
It breaks down assumptions of the form `_ ∧ _`, `_ ∨ _`, `_ ↔ _` and `∃ _, _`
and splits a goal of the form `_ ∧ _`, `_ ↔ _` or `∃ _, _` until it can be discharged
using `rfl`, `contradiction` or `solve_by_elim`.
This is a finishing tactic: it either closes the goal or raises an error.

This tactic makes no attempt to avoid classical reasoning. The `itauto` tactic
is designed for that purpose.
 -/
Mathlib.Tactic.Tauto.tauto : Lean.ParserDescr