mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_sub_Ioo : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a - x) ⁻¹' Set.Ioo b c = Set.Ioo (a - c) (a - b)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inj_sigmaOfIsColimit_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (i : E.I₀) (r : PUnit.{w + 1}),
  CategoryTheory.CategoryStruct.comp (c.inj i) ((E.sigmaOfIsColimit hc).f r) = E.f i
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.IsHenstock.disjUnion : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I},
  π₁.IsHenstock → π₂.IsHenstock → ∀ (h : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂ h).IsHenstock
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.IsClique.card_le_of_colorable : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ} {s : Finset V}, G.IsClique ↑s → G.Colorable n → s.card ≤ n
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.braiding_naturality_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C) {Y Z : CategoryTheory.Dial C} (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) f) (X.braiding Z).hom =
    CategoryTheory.CategoryStruct.comp (X.braiding Y).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id X))
-- Mathlib.Tactic.PNatToNat
Mathlib.Tactic.PNatToNat.coe_le_coe : ∀ (m n : ℕ+), m ≤ n ↔ ↑m ≤ ↑n
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_C : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (c : R) [inst_1 : Decidable (c = 0)],
  m.withBotDegree (MvPolynomial.C c) = if c = 0 then ⊥ else 0
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
ConditionallyCompletePartialOrderSup.toSupSet : {α : Type u_3} → [self : ConditionallyCompletePartialOrderSup α] → SupSet α
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.IsLocallyInjective.equalizerSieve_mem : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {D : Type u'} {inst_1 : CategoryTheory.Category.{v', u'} D}
  {FD : D → D → Type u_1} {CD : D → Type w} {inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)}
  {inst_3 : CategoryTheory.ConcreteCategory D FD} {J : CategoryTheory.GrothendieckTopology C}
  {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D} {φ : F₁ ⟶ F₂} [self : CategoryTheory.Presheaf.IsLocallyInjective J φ] {X : Cᵒᵖ}
  (x y : CategoryTheory.ToType (F₁.obj X)),
  (CategoryTheory.ConcreteCategory.hom (φ.app X)) x = (CategoryTheory.ConcreteCategory.hom (φ.app X)) y →
    CategoryTheory.Presheaf.equalizerSieve x y ∈ J (Opposite.unop X)
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.instInhabited : {n : ℕ} → Inhabited n.Partition
-- Mathlib.LinearAlgebra.Matrix.RowCol
/-- `v ᵥ* M` is the vector whose entries are those of `replicateRow ι v * M`.  -/
Matrix.replicateRow_vecMul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring α]
  (M : Matrix m n α) (v : m → α), Matrix.replicateRow ι (Matrix.vecMul v M) = Matrix.replicateRow ι v * M
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff_of_mem : ∀ {C : Type u₁} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₃, u₃} H]
  (F : CategoryTheory.Functor C H) (W : CategoryTheory.MorphismProperty C) {X Y : C} (w : X ⟶ Y),
  W w → (F.HasPointwiseRightDerivedFunctorAt W X ↔ F.HasPointwiseRightDerivedFunctorAt W Y)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomCongrEquiv_apply : ∀ {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2}
  (σ : ι₁ ≃ ι₂) (m : MultilinearMap R (fun x => M₂) M₃),
  (MultilinearMap.domDomCongrEquiv σ) m = MultilinearMap.domDomCongr σ m
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- The minimum degree in the graph is at most the degree of any particular vertex.  -/
SimpleGraph.minDegree_le_degree : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (v : V), G.minDegree ≤ G.degree v
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_div : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Div M] (a b : M), ↑(a / b) = ↑a / ↑b
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.fibres_closed : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} [inst : TopologicalSpace S] [inst_1 : TopologicalSpace T]
  [inst_2 : TopologicalSpace X] [DiscreteTopology X] [T2Space T] [CompactSpace S] (π : T → S × OnePoint X),
  Continuous π →
    ∀ (σ : Option X → S → T),
      (∀ (x : Option X), Continuous (σ x)) →
        (∀ (x : Option X) (s : S), (π (σ x s)).2 = x) → IsClosed (InternalProjectivityProof.fibres✝ π σ)
-- Mathlib.Topology.Spectral.Hom
SpectralMap.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] (f : SpectralMap γ δ) (g : SpectralMap β γ)
  (h : SpectralMap α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.isSheaf_of_isSheaf_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  (P : CategoryTheory.Functor Cᵒᵖ A) (s : CategoryTheory.Functor A B)
  [CategoryTheory.Limits.ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s],
  CategoryTheory.Presheaf.IsSheaf J (P.comp s) → CategoryTheory.Presheaf.IsSheaf J P
-- Mathlib.RingTheory.WittVector.Defs
WittVector.constantCoeff_wittZSMul : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (z : ℤ) (n : ℕ), MvPolynomial.constantCoeff (WittVector.wittZSMul p z n) = 0
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_sub_of_le : ∀ {a b : Int8}, 0 ≤ b → b ≤ a → (a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg
-- Mathlib.Computability.Primrec.Basic
PrimrecPred.primrecRel : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α × β → Prop},
  PrimrecPred p → PrimrecRel fun a b => p (a, b)
-- Mathlib.Data.Set.Basic
Set.ofPred_subset_ofPred : ∀ {α : Type u} {p q : α → Prop}, {a | p a} ⊆ {a | q a} ↔ ∀ (a : α), p a → q a
-- Mathlib.Algebra.Homology.BifunctorShift
CategoryTheory.CommShift₂Setup.int.congr_simp : ∀ {D : Type u_5} [inst : CategoryTheory.Category.{v_5, u_5} D] [inst_1 : CategoryTheory.Preadditive D]
  [inst_2 : CategoryTheory.HasShift D ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive],
  CategoryTheory.CommShift₂Setup.int = CategoryTheory.CommShift₂Setup.int
-- Mathlib.Analysis.Complex.ReImTopology
IsOpen.reProdIm : ∀ {s t : Set ℝ}, IsOpen s → IsOpen t → IsOpen (s ×ℂ t)
-- Mathlib.Topology.Inseparable
Specializes.fst : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {a b : X × Y},
  a ⤳ b → a.1 ⤳ b.1
-- Mathlib.Topology.ContinuousMap.Compact
BoundedContinuousFunction.mkOfCompact_star : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  [inst_2 : StarAddMonoid β] [inst_3 : NormedStarGroup β] [inst_4 : CompactSpace α] (f : C(α, β)),
  BoundedContinuousFunction.mkOfCompact (star f) = star (BoundedContinuousFunction.mkOfCompact f)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mk_eq_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  {f g : α → β} {hf : MeasureTheory.AEStronglyMeasurable f μ} {hg : MeasureTheory.AEStronglyMeasurable g μ},
  MeasureTheory.AEEqFun.mk f hf = MeasureTheory.AEEqFun.mk g hg ↔ f =ᵐ[μ] g
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_a_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a ≠ 0 → P.toPoly.degree = 3
-- Mathlib.GroupTheory.Coset.Card
AddSubgroup.card_comap_dvd_of_injective : ∀ {α : Type u_1} [inst : AddGroup α] {H : Type u_2} [inst_1 : AddGroup H] (K : AddSubgroup H) (f : α →+ H),
  Function.Injective ⇑f → Nat.card ↥(AddSubgroup.comap f K) ∣ Nat.card ↥K
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The proposed colimit cocone is a colimit in `CommSemiRingCat`.  -/
CommSemiRingCat.FilteredColimits.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J CommSemiRingCat) →
        CategoryTheory.Limits.IsColimit (CommSemiRingCat.FilteredColimits.colimitCocone F)
-- Mathlib.CategoryTheory.Enriched.Basic
/-- Enriched functors form a category with the morphisms between functors `F` and `G` being
enriched natural transformations, i.e. natural transformations `F.forget ⟶ G.forget`.  -/
CategoryTheory.EnrichedFunctor.category : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              CategoryTheory.Category.{max u₁ w, max (max u₂ u₁) w} (CategoryTheory.EnrichedFunctor V C D)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
CategoryTheory.Limits.PreservesWellOrderContinuousOfShape.mk : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type w} [inst_2 : LinearOrder J] {G : CategoryTheory.Functor C D},
  autoParam (∀ (j : J), Order.IsSuccLimit j → CategoryTheory.Limits.PreservesColimitsOfShape (↑(Set.Iio j)) G)
      CategoryTheory.Limits.PreservesWellOrderContinuousOfShape.preservesColimitsOfShape._autoParam →
    CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J G
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_sInf : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜]
  (ℐ : Set (HomogeneousIdeal 𝒜)), (sInf ℐ).toIdeal = ⨅ s ∈ ℐ, s.toIdeal
-- Mathlib.Topology.Path
Path.coe_mk_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (f : ↑unitInterval → X) (h₁ : Continuous f) (h₂ : f 0 = x)
  (h₃ : f 1 = y), ⇑{ toFun := f, continuous_toFun := h₁, source' := h₂, target' := h₃ } = f
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- The indexing set of a root pairing carries an involutive negation, corresponding to the negation
of a root / coroot.  -/
RootPairing.indexNeg : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → InvolutiveNeg ι
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.get?_eq_getValue? : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α},
      Std.DHashMap.Internal.Raw₀.Const.get? m a =
        Std.Internal.List.getValue? a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.Algebra.Ring.SumsOfSquares
Subsemiring.coe_sumSq : ∀ {T : Type u_2} [inst : CommSemiring T], ↑(Subsemiring.sumSq T) = {s | IsSumSq s}
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.EditableDocument.mk.sizeOf_spec : ∀ (toEditableDocumentCore : Lean.Server.FileWorker.EditableDocumentCore) (reporter : Lean.Server.ServerTask Unit),
  sizeOf { toEditableDocumentCore := toEditableDocumentCore, reporter := reporter } =
    1 + sizeOf toEditableDocumentCore + sizeOf reporter
-- Mathlib.Order.RelClasses
/-- Set notation form of `ne_of_not_ge` -/
ne_of_not_superset : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, ¬b ⊆ a → a ≠ b
-- Mathlib.InformationTheory.Coding.KraftMcMillan
/-- Auxiliary bound for Kraft–McMillan.

If `S` is a finite uniquely decodable code and `1 ≤ r`, then the `r`-th power of its Kraft sum
is bounded by `r * sup length`:

`(∑ w ∈ S, (1 / D) ^ w.length) ^ r ≤ r * (S.sup List.length)`.  -/
_private.Mathlib.InformationTheory.Coding.KraftMcMillan.0.InformationTheory.kraft_mcmillan_inequality_aux : ∀ {α : Type u_1} {S : Finset (List α)} [inst : Fintype α] [Nonempty α],
  InformationTheory.UniquelyDecodable ↑S →
    ∀ r ≥ 1, (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r ≤ ↑r * ↑(S.sup List.length)
-- Init.Data.List.BasicAux
List.append_cancel_left_eq : ∀ {α : Type u_1} (as bs cs : List α), (as ++ bs = as ++ cs) = (bs = cs)
-- Mathlib.Combinatorics.Configuration
Configuration.instFiniteDual : ∀ (P : Type u_1) [Finite P], Finite (Configuration.Dual P)
-- Mathlib.Data.Countable.Basic
Sum.uncountable_inl : ∀ {α : Type u} {β : Type v} [Uncountable α], Uncountable (α ⊕ β)
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.Stained.goal : Mathlib.Linter.Flexible.Stained✝
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.coe_id : ∀ (P : TopCat → Prop) (X : CompHausLike P),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Analysis.Meromorphic.Basic
/-- Iterated derivatives of meromorphic functions are meromorphic.  -/
MeromorphicOn.iterated_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → ∀ [CompleteSpace E] {n : ℕ}, MeromorphicOn (deriv^[n] f) U
-- Mathlib.Topology.Connected.Clopen
Sum.isPreconnected_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set (α ⊕ β)},
  IsPreconnected s ↔ (∃ t, IsPreconnected t ∧ s = Sum.inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = Sum.inr '' t
-- Mathlib.Algebra.Group.Hom.Basic
/-- The `n`-th power map (for an integer `n`) on a commutative group, considered as a group
homomorphism.  -/
zpowGroupHom : {α : Type u_1} → [inst : DivisionCommMonoid α] → ℤ → α →* α
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.card_smul_finset₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β] {a : α},
  a ≠ 0 → ∀ (s : Finset β), (a • s).card = s.card
-- Init.Data.Sum.Basic
Sum.getRight.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (ab ab_1 : α ⊕ β) (e_ab : ab = ab_1) (a : ab.isRight = true),
  ab.getRight a = ab_1.getRight ⋯
-- Mathlib.Topology.Separation.Regular
T4Space.toT1Space : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T4Space X], T1Space X
-- Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
/-- Any finite-dimensional irreducible representation of a commutative algebra over an algebraically
closed field is one-dimensional.  -/
IsSimpleModule.finrank_eq_one_of_isMulCommutative : ∀ (A : Type u_1) (V : Type u_2) (k : Type u_3) [inst : Field k] [inst_1 : Ring A] [inst_2 : Algebra k A]
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : Module A V] [IsScalarTower k A V] [IsSimpleModule A V]
  [FiniteDimensional k V] [IsAlgClosed k] [IsMulCommutative A], Module.finrank k V = 1
-- Mathlib.Order.Category.HeytAlg
HeytAlg.Iso.mk_hom : ∀ {α β : HeytAlg} (e : ↑α ≃o ↑β),
  (HeytAlg.Iso.mk e).hom = HeytAlg.ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }
-- Init.Control.Do
/-- Exit a loop body via `break`.  -/
BreakT.break : {α : Type w} → {m : Type w → Type x} → [Monad m] → BreakT m α
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDeriv_add_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} {i : ℕ}
  {f g : E → F},
  ContDiffAt 𝕜 (↑i) f x →
    ContDiffAt 𝕜 (↑i) g x → iteratedFDeriv 𝕜 i (f + g) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularCompactLTTop.mk : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α},
  (μ.InnerRegularWRT IsCompact fun s => MeasurableSet s ∧ μ s ≠ ⊤) → μ.InnerRegularCompactLTTop
-- Mathlib.Dynamics.Ergodic.Conservative
MeasureTheory.Conservative.mk : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Measure.QuasiMeasurePreserving f μ μ →
    (∀ ⦃s : Set α⦄, MeasurableSet s → μ s ≠ 0 → ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s) → MeasureTheory.Conservative f μ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_eq_getLast!_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.maxKey! = t.keys.getLast!
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_zero_cochain_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n)
  (z₂ : CochainComplex.HomComplex.Cochain G K 0) (p q : ℤ) (hpq : p + n = q),
  (z₁.comp z₂ ⋯).v p q hpq = CategoryTheory.CategoryStruct.comp (z₁.v p q hpq) (z₂.v q q ⋯)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.max_one : ∀ {α : Type u_2} [inst : One α] [inst_1 : LinearOrder α], Finset.max 1 = 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {newWidth : ℕ} →
        (aig : Std.Sat.AIG α) →
          (motive : Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig newWidth → Sort u_1) →
            (target : Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig newWidth) →
              ((lw rw : ℕ) →
                  (lhs : aig.RefVec lw) →
                    (rhs : aig.RefVec rw) →
                      (h : newWidth = rw + lw) → motive { lw := lw, rw := rw, lhs := lhs, rhs := rhs, h := h }) →
                motive target
-- Std.Http.Protocol.H1.Config
/-- Maximum length of reason phrase (default: 512 bytes).
 -/
Std.Http.Protocol.H1.Config.maxReasonPhraseLength : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCoreAux_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E],
  balancedCoreAux 𝕜 ∅ = ∅
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F]
  [CompleteSpace F] (f : E →L[𝕜] F) (G : Submodule 𝕜 F),
  IsCompl (↑f).range G → IsClosed ↑G → (↑f).ker = ⊥ → IsClosed ↑(↑f).range
-- Mathlib.GroupTheory.Congruence.Defs
/-- The binary function on the quotient by a congruence relation `c`
induced by a binary function that is constant on `c`'s equivalence classes.  -/
AddCon.liftOn₂ : {M : Type u_1} →
  [inst : Add M] →
    {β : Sort u_4} →
      {c : AddCon M} →
        c.Quotient → c.Quotient → (f : M → M → β) → (∀ (a₁ a₂ b₁ b₂ : M), c a₁ b₁ → c a₂ b₂ → f a₁ a₂ = f b₁ b₂) → β
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokensOptions.fromJson : Lean.Json → Except String Lean.Lsp.SemanticTokensOptions
-- Init.Data.Option.Basic
/-- Implementation of `OrElse`'s `<|>` syntax for `Option`. If the first argument is `some a`, returns
`some a`, otherwise evaluates and returns the second argument.

See also `or` for a version that is strict in the second argument.
 -/
Option.orElse : {α : Type u_1} → Option α → (Unit → Option α) → Option α
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.smul_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {A : Type u_8} [inst_1 : SMulZeroClass A R] (a : A) (m : M) (r : R),
  a • MonoidAlgebra.single m r = MonoidAlgebra.single m (a • r)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.Eval.instInhabitedResult.default : Mathlib.Tactic.BicategoryLike.Eval.Result
-- Init.Data.SInt.Lemmas
Int64.toNat_toInt : ∀ (x : Int64), x.toInt.toNat = x.toNatClampNeg
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The isomorphism `truncGE'.X K e i ≅ K.opcycles (e.f i)` when `e.BoundaryGE i` holds.  -/
HomologicalComplex.truncGE'.XIsoOpcycles : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : ∀ (i' : ι'), K.HasHomology i'] →
                    {i : ι} → e.BoundaryGE i → (HomologicalComplex.truncGE'.X K e i ≅ K.opcycles (e.f i))
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- If `F : C ⥤ D` is a fully faithful monoidal functor, then `F.mapMon : Mon C ⥤ Mon D` is fully
faithful too.  -/
CategoryTheory.Functor.FullyFaithful.mapMon : {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.Monoidal] → F.FullyFaithful → F.mapMon.FullyFaithful
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin_last_snd : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α),
  (F.intervalGapsWithin h a b (Fin.last k)).2 = b
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpace_le_genWeightSpaceChain : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [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] (χ₁ χ₂ : L → R) (p q : ℤ) {k : ℤ},
  k ∈ Set.Ioo p q → LieModule.genWeightSpace M (k • χ₁ + χ₂) ≤ LieModule.genWeightSpaceChain M χ₁ χ₂ p q
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.prevn.eq_def : ∀ (x : Substring.Raw) (x_1 : ℕ) (x_2 : String.Pos.Raw),
  x.prevn x_1 x_2 =
    match x, x_1, x_2 with
    | x, 0, p => p
    | ss, i.succ, p => ss.prevn i (ss.prev p)
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_rci_eq_toList_mkSlice_rco : ∀ {α : Type u_1} {xs : List α} {lo : ℕ},
  Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) =
    Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...xs.length)
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
/-- The `limsup` relationship for the spectral radius used to prove `spectrum.gelfand_formula`.  -/
spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] (a : A),
  Filter.limsup (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop ≤ spectralRadius ℂ a
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.SpecOfPoint.eq_1 : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↥(CategoryTheory.Limits.pullback f g)),
  AlgebraicGeometry.Scheme.Pullback.SpecOfPoint t =
    (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor t)) ⊥