mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.LiminfLimsup
/-- Let `u : ℕ → α → β` be a sequence of antitone functions `α → β` indexed by `ℕ`. Suppose that for
all `n : ℕ`, `u n` tends to `c` at infinity, and that furthermore the limsup of `n ↦ u n r`
tends to the same `c` as `r` tends to infinity.
Then the supremum function `r ↦ ⨆ n, u n r` also tends to `c` at infinity.  -/
Nat.tendsto_iSup_of_tendsto_limsup : ∀ {α : Type u_7} {β : Type u_8} [inst : ConditionallyCompleteLattice α] [inst_1 : CompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {u : ℕ → α → β} {c : β},
  (∀ (n : ℕ), Filter.Tendsto (u n) Filter.atTop (nhds c)) →
    Filter.Tendsto (fun r => Filter.limsup (fun n => u n r) Filter.atTop) Filter.atTop (nhds c) →
      (∀ (n : ℕ), Antitone (u n)) → Filter.Tendsto (fun r => ⨆ n, u n r) Filter.atTop (nhds c)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.instMulActionUnitsRingOfIntegersMixedSpace : (K : Type u_1) → [inst : Field K] → MulAction (NumberField.RingOfIntegers K)ˣ (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd.instIsZeroOrProbabilityMeasure : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)} [MeasureTheory.IsZeroOrProbabilityMeasure ρ],
  MeasureTheory.IsZeroOrProbabilityMeasure ρ.snd
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.BlockMem.coe_bot : ∀ (G : Type u_1) [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] (a : X), ↑⊥ = {a}
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.map_mk : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (N : AddSubgroup G) [nN : N.Normal]
  (M : AddSubgroup H) [inst_2 : M.Normal] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) (x : G),
  (QuotientAddGroup.map N M f h) ↑x = ↑(f x)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.map_fst : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape}
  (d : CategoryTheory.Limits.MulticospanIndex J C) (F : CategoryTheory.Functor C D) (i : J.R),
  (d.map F).fst i = F.map (d.fst i)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.piLE_eq_comap_frestrictLe : ∀ {ι : Type u_2} [inst : Preorder ι] {X : ι → Type u_4} [inst_1 : (i : ι) → MeasurableSpace (X i)]
  [inst_2 : LocallyFiniteOrderBot ι] (i : ι),
  ↑MeasureTheory.Filtration.piLE i = MeasurableSpace.comap (Preorder.frestrictLe i) MeasurableSpace.pi
-- Mathlib.RingTheory.Flat.Equalizer
/-- (Implementation): Use `AlgHom.tensorEqualizer` instead.  -/
AlgHom.tensorEqualizerAux : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (T : Type u_3) →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  [inst_6 : IsScalarTower R S T] →
                    {A : Type u_4} →
                      {B : Type u_5} →
                        [inst_7 : CommRing A] →
                          [inst_8 : CommRing B] →
                            [inst_9 : Algebra R A] →
                              [inst_10 : Algebra R B] →
                                (f g : A →ₐ[R] B) →
                                  TensorProduct R T ↥(f.equalizer g) →ₗ[S]
                                    ↥((Algebra.TensorProduct.map (AlgHom.id S T) f).equalizer
                                        (Algebra.TensorProduct.map (AlgHom.id S T) g))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.nnnorm_mem_spectrum_of_nonneg : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] [Nontrivial A] {a : A},
  autoParam (0 ≤ a) CStarAlgebra.nnnorm_mem_spectrum_of_nonneg._auto_1 → ‖a‖₊ ∈ spectrum NNReal a
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Tensor product of elements along a base change.

This notation is necessary because we need to reason about `s ⊗ₜ m` where `s : S` and `m : M`;
without this notation, one needs to work with `s : (restrictScalars f).obj ⟨S⟩`.  -/
ChangeOfRings.«term_⊗ₜ[_,_]_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.InjSurj
/-- A type has an involutive negation if it admits a surjective map that
preserves `-` to a type which has an involutive negation.  -/
Function.Surjective.involutiveNeg : {M₁ : Type u_1} →
  {M₂ : Type u_3} →
    [inst : Neg M₂] →
      [inst_1 : InvolutiveNeg M₁] →
        (f : M₁ → M₂) → Function.Surjective f → (∀ (x : M₁), f (-x) = -f x) → InvolutiveNeg M₂
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.instFintypeOfSubtypeHomInjectiveCoe : {V : Type u_1} →
  {W : Type u_2} →
    {G : SimpleGraph V} → {H : SimpleGraph W} → [Fintype { f // Function.Injective ⇑f }] → Fintype (G.Copy H)
-- Mathlib.Data.Setoid.Basic
/-- The underlying binary operation of the infimum of a set of equivalence relations
is the infimum of the set's image under the map to the underlying binary operation.  -/
Setoid.sInf_def : ∀ {α : Type u_1} {s : Set (Setoid α)}, ⇑(sInf s) = sInf (@Setoid.r α '' s)
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.IsOpenPosMeasure.comap : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} [BorelSpace X] {Z : Type u_3}
  [inst_2 : TopologicalSpace Z] {mZ : MeasurableSpace Z} [BorelSpace Z] (μ : MeasureTheory.Measure Z)
  [μ.IsOpenPosMeasure] {f : X → Z}, Topology.IsOpenEmbedding f → (MeasureTheory.Measure.comap f μ).IsOpenPosMeasure
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.categoryStruct : (B : Type u₁) →
  [CategoryTheory.Bicategory B] → CategoryTheory.CategoryStruct.{v₁, u₁} (CategoryTheory.Bicategory.Pith B)
-- Mathlib.Algebra.GroupWithZero.Invertible
mul_div_cancel_of_invertible : ∀ {α : Type u} [inst : GroupWithZero α] (a b : α) [Invertible b], a * b / b = a
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.LawfulOperator.denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → Type}
  {f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α} [inst_2 : Std.Sat.AIG.LawfulOperator α β f]
  {assign : α → Bool} {start : ℕ} {invert : Bool} {aig : Std.Sat.AIG α} {input : β aig} (h : start < aig.decls.size),
  ⟦assign, { aig := (f aig input).aig, ref := { gate := start, invert := invert, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := h } }⟧
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.hasNPowNat : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → Pow (CentroidHom α) ℕ
-- Mathlib.Data.EReal.Basic
EReal.bot_ne_coe : ∀ (x : ℝ), ⊥ ≠ ↑x
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_iSup_of_antitone : ∀ {α : Type u_1} {ι : Type u_3} {_mα : MeasurableSpace α} [inst : SemilatticeInf ι] {Ω : Type u_4}
  {m : ι → MeasurableSpace Ω} {m' m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  (∀ (i : ι), ProbabilityTheory.Kernel.Indep (m i) m' κ μ) →
    (∀ (i : ι), m i ≤ m0) → m' ≤ m0 → Antitone m → ProbabilityTheory.Kernel.Indep (⨆ i, m i) m' κ μ
-- Lean.Meta.Tactic.Simp.Arith.Util
Lean.Meta.Simp.Arith.isLinearTerm : Lean.Expr → Bool
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.isDomain_iff_prime : ∀ {R : Type u_3} [inst : Ring R] (I : Ideal R) [inst_1 : I.IsTwoSided], IsDomain (R ⧸ I) ↔ I.IsPrime
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  [inst_3 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)]
  (X : CategoryTheory.Grothendieck F),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G X)
      (CategoryTheory.Limits.colimitFiberwiseColimitIso G).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X.base).comp G) X.fiber)
      (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.fiberwiseColimit G) X.base)
-- Std.Async.Basic
Std.Async.BaseAsync.instMonadAwaitTask : Std.Async.MonadAwait Task Std.Async.BaseAsync
-- Mathlib.Data.Real.Basic
Real.ofCauchy_mul : ∀ (a b : CauSeq.Completion.Cauchy abs), { cauchy := a * b } = { cauchy := a } * { cauchy := b }
-- Mathlib.CategoryTheory.Presentable.Directed
/-- Auxiliary definition for `functor`.  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      {D₁ D₂ : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ} →
        D₁ ≤ D₂ → (D₁.top ⟶ D₂.top)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.coe_pointwise_smul : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α M] (a : α)
  (S : Submonoid M), ↑(a • S) = a • ↑S
-- Mathlib.MeasureTheory.Measure.Restrict
Set.EqOn.aeEq_restrict : ∀ {α : Type u_7} {β : Type u_8} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → β},
  Set.EqOn f g s → MeasurableSet s → f =ᵐ[μ.restrict s] g
-- Mathlib.CategoryTheory.Yoneda
/-- Two morphisms of presheaves of types `P ⟶ Q` coincide if the precompositions
with morphisms `uliftCoyoneda.obj X ⟶ P` agree.  -/
CategoryTheory.hom_ext_uliftCoyoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor C (Type (max w v₁))}
  {f g : P ⟶ Q},
  (∀ (X : Cᵒᵖ) (p : CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ P),
      CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp p g) →
    f = g
-- Mathlib.Combinatorics.Hindman
Ultrafilter.add.eq_1 : ∀ {M : Type u_1} [inst : Add M], Ultrafilter.add = { add := fun U V => (fun x1 x2 => x1 + x2) <$> U <*> V }
-- Mathlib.Computability.Language
Language.kstar_def_nonempty : ∀ {α : Type u_1} (l : Language α), KStar.kstar l = {x | ∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}
-- Mathlib.ModelTheory.Arithmetic.Presburger.Definability
/-- A set is Presburger definable in `ℕ` if and only if it is semilinear.  -/
FirstOrder.Language.presburger.definable_iff_isSemilinearSet : ∀ {α : Type u_1} {A : Set ℕ} [Finite α] {s : Set (α → ℕ)},
  A.Definable FirstOrder.Language.presburger s ↔ IsSemilinearSet s
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_congr : ∀ {u v : ℕ → ENNReal}, u =ᶠ[Filter.atTop] v → ExpGrowth.expGrowthSup u = ExpGrowth.expGrowthSup v
-- Mathlib.Control.Traversable.Instances
_private.Mathlib.Control.Traversable.Instances.0.List.next?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match [] with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_1 ()
-- Mathlib.RingTheory.Polynomial.Hermite.Gaussian
Polynomial.hermite_eq_deriv_gaussian' : ∀ (n : ℕ) (x : ℝ),
  (Polynomial.aeval x) (Polynomial.hermite n) =
    (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
subset_lowerBounds_mul : ∀ {M : Type u_3} [inst : Mul M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] (s t : Set M),
  lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t)
-- Mathlib.Algebra.Group.Prod
AddHom.prod_comp_prodMap : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} [inst : Add M] [inst_1 : Add N]
  [inst_2 : Add M'] [inst_3 : Add N'] [inst_4 : Add P] (f : P →ₙ+ M) (g : P →ₙ+ N) (f' : M →ₙ+ M') (g' : N →ₙ+ N'),
  (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
-- Mathlib.LinearAlgebra.Ray
/-- `SameRay` is symmetric.  -/
SameRay.symm : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {x y : M}, SameRay R x y → SameRay R y x
-- Mathlib.Tactic.NormNum.Inv
/-- Helper function to synthesize a typed `CharZero α` expression given `DivisionRing α`, if it
exists.  -/
Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing? : {u : Lean.Level} →
  {α : Q(Type u)} →
    (_i : autoParam Q(DivisionRing «$α») Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing?._auto_1) →
      Lean.MetaM (Option Q(CharZero «$α»))
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.union_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ m₃ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₂.Equiv m₃ → (m₁ ∪ m₂).Equiv (m₁ ∪ m₃)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.hₚFunctor_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (i : ι) (HP : TopPair.HomologyPretheory C c),
  (TopPair.HomologyPretheory.hₚFunctor i).obj HP = HP.Hₚ i
-- Mathlib.Topology.MetricSpace.Defs
instDistOrderDual : {X : Type u_1} → [Dist X] → Dist Xᵒᵈ
-- Mathlib.Logic.Encodable.Basic
Nat.encodable : Encodable ℕ
-- Mathlib.CategoryTheory.EffectiveEpi.Comp
/-- An effective epi family followed by an iso is an effective epi family.  -/
CategoryTheory.effectiveEpiFamilyStructCompIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {B B' : C} →
      {α : Type u_2} →
        (X : α → C) →
          (π : (a : α) → X a ⟶ B) →
            (i : B ⟶ B') →
              [CategoryTheory.EffectiveEpiFamily X π] →
                [CategoryTheory.IsIso i] →
                  CategoryTheory.EffectiveEpiFamilyStruct X fun a => CategoryTheory.CategoryStruct.comp (π a) i
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_neg : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] ⦃f : ↥(lp E p)⦄,
  ‖-f‖ = ‖f‖
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {he : t ≠ ∅}, t.getKey! (t.minKey he) = t.minKey he
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.LeanClientCapabilities.mk.injEq : ∀ (incrementalDiagnosticSupport? silentDiagnosticSupport? : Option Bool)
  (rpcWireFormat? : Option Lean.Lsp.RpcWireFormat)
  (incrementalDiagnosticSupport?_1 silentDiagnosticSupport?_1 : Option Bool)
  (rpcWireFormat?_1 : Option Lean.Lsp.RpcWireFormat),
  ({ incrementalDiagnosticSupport? := incrementalDiagnosticSupport?,
        silentDiagnosticSupport? := silentDiagnosticSupport?, rpcWireFormat? := rpcWireFormat? } =
      { incrementalDiagnosticSupport? := incrementalDiagnosticSupport?_1,
        silentDiagnosticSupport? := silentDiagnosticSupport?_1, rpcWireFormat? := rpcWireFormat?_1 }) =
    (incrementalDiagnosticSupport? = incrementalDiagnosticSupport?_1 ∧
      silentDiagnosticSupport? = silentDiagnosticSupport?_1 ∧ rpcWireFormat? = rpcWireFormat?_1)
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_three : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ : C₁} {X₂ : C₂} {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃) (g : X₂ ⟶ (G.obj (Opposite.op X₁)).obj X₃),
  adj₂.homEquiv.symm (CategoryTheory.CategoryStruct.comp g ((G.obj (Opposite.op X₁)).map f₃)) =
    CategoryTheory.CategoryStruct.comp (adj₂.homEquiv.symm g) f₃
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.det_eq_zero_of_mulVec_eq_zero_of_mem_nonZeroDivisors : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] {M : Matrix n n α}
  {v : n → α}, M.mulVec v = 0 → ∀ {i : n}, v i ∈ nonZeroDivisors α → M.det = 0
-- Init.Data.Range.Polymorphic.PRange
/-- Every element of the intersection is an element of both original ranges.
   -/
Std.Rio.LawfulRcoIntersection.mem_intersection_iff : ∀ {α : Type w} {inst : LT α} {inst_1 : LE α} {inst_2 : Std.Rio.HasRcoIntersection α}
  [self : Std.Rio.LawfulRcoIntersection α] {a : α} {r : Std.Rio α} {s : Std.Rco α},
  a ∈ Std.Rio.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
-- Mathlib.Order.Filter.Bases.Basic
/-- If `B` is a filter basis on `α`, and `U` a subset of `α` then we can write `U ∈ B` as
on paper.  -/
instMembershipSetFilterBasis : {α : Type u_6} → Membership (Set α) (FilterBasis α)
-- Lean.Meta.Tactic.Grind.Action
/-- Runs action `a` on the given `goal`.
 -/
Lean.Meta.Grind.Action.run : Lean.Meta.Grind.Goal → Lean.Meta.Grind.Action → Lean.Meta.Grind.GrindM Lean.Meta.Grind.ActionResult
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- When `A : Rep k G` is a trivial representation of `G`, `Z¹(G, A)` is isomorphic to the
group homs `G → A`.  -/
groupCohomology.cocycles₁IsoOfIsTrivial : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u_1, u, u} k G) →
        [hA : A.IsTrivial] → ModuleCat.of k ↥(groupCohomology.cocycles₁ A) ≅ ModuleCat.of k (Additive G →+ ↑A)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀' : ∀ {Ω : Type u_7} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {M : Type u_10} [inst : AddMonoid M]
  [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] {f g : Ω → M},
  AEMeasurable f μ →
    AEMeasurable g μ →
      MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ) →
        MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g μ) →
          ProbabilityTheory.IndepFun f g μ →
            MeasureTheory.Measure.map (f + g) μ = (MeasureTheory.Measure.map f μ).conv (MeasureTheory.Measure.map g μ)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.cosimplicialSimplicialEquiv_unitIso_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor SimplexCategory C)ᵒᵖ),
  (CategoryTheory.cosimplicialSimplicialEquiv C).unitIso.hom.app X = (Opposite.unop X).opUnopIso.hom.op
-- Init.Data.Iterators.Basic
Std.IterM.Step.toPure_skip : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it it' : Std.IterM Id β}
  {h : it.IsPlausibleStep (Std.IterStep.skip it')},
  Std.IterM.Step.toPure ⟨Std.IterStep.skip it', h⟩ = Std.PlausibleIterStep.skip it'.toIter h
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.nnnorm_sqrt : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  (a : A), autoParam (0 ≤ a) CFC.nnnorm_sqrt._auto_1 → ‖CFC.sqrt a‖₊ = NNReal.sqrt ‖a‖₊
-- Mathlib.CategoryTheory.Grothendieck
/-- `Grothendieck.ι F c` composed with `Grothendieck.functorFrom` is isomorphic a functor on a fiber
on `F` supplied as the first argument to `Grothendieck.functorFrom`.  -/
CategoryTheory.Grothendieck.ιCompFunctorFrom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {E : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} E] →
          (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) →
            (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) →
              (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) →
                (hom_comp :
                    ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
                      hom (CategoryTheory.CategoryStruct.comp f g) =
                        CategoryTheory.CategoryStruct.comp (hom f)
                          (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g))
                            (CategoryTheory.eqToHom ⋯))) →
                  (c : C) →
                    (CategoryTheory.Grothendieck.ι F c).comp
                        (CategoryTheory.Grothendieck.functorFrom fib (fun {c c'} => hom) hom_id hom_comp) ≅
                      fib c
-- Init.Data.List.Count
_private.Init.Data.List.Count.0.List.findIdx.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (n : ℕ) (h_1 : (n : ℕ) → motive [] n)
  (h_2 : (a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n),
  (match [], n with
    | [], n => h_1 n
    | a :: l, n => h_2 a l n) =
    h_1 n
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.IsCompleteMultipartite.colorable_of_cliqueFree : ∀ {α : Type u} {G : SimpleGraph α} {n : ℕ}, G.IsCompleteMultipartite → G.CliqueFree n → G.Colorable (n - 1)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
/-- The bijection `A.op.N ≃ A.N` for a subcomplex `A` of a simplicial set..  -/
SSet.Subcomplex.N.opEquiv : {X : SSet} → {A : X.Subcomplex} → A.op.N ≃o A.N
-- Lean.Parser.Types
Lean.Parser.Error.mk.inj : ∀ {unexpectedTk : Lean.Syntax} {unexpected : String} {expected : List String} {unexpectedTk_1 : Lean.Syntax}
  {unexpected_1 : String} {expected_1 : List String},
  { unexpectedTk := unexpectedTk, unexpected := unexpected, expected := expected } =
      { unexpectedTk := unexpectedTk_1, unexpected := unexpected_1, expected := expected_1 } →
    unexpectedTk = unexpectedTk_1 ∧ unexpected = unexpected_1 ∧ expected = expected_1
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.IsEquipartition.sum_nonUniforms_lt : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [inst_4 : DecidableRel G.Adj]
  {ε : 𝕜},
  A.Nonempty →
    0 < ε →
      P.IsEquipartition →
        P.IsUniform G ε →
          ↑((P.nonUniforms G ε).biUnion fun x =>
                  match x with
                  | (U, V) => U ×ˢ V).card <
            4 * ε * ↑A.card ^ 2
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsFunctorPreservesFiniteLimits : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_3, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_5, u_3} C],
  CategoryTheory.ObjectProperty.preservesFiniteLimits.IsClosedUnderIsomorphisms
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- If `f : X ⟶ Y`, this is the pushforward of sheaves of modules along `Over.pullback f`.  -/
SheafOfModules.overPullback : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {K : CategoryTheory.GrothendieckTopology D} →
      (R : CategoryTheory.Sheaf K RingCat) →
        [CategoryTheory.Limits.HasPullbacks D] →
          {X Y : D} → (X ⟶ Y) → CategoryTheory.Functor (SheafOfModules (R.over X)) (SheafOfModules (R.over Y))
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_ne_zero_of_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b : α}, a ≠ 0 → gcd a b ≠ 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {km : α}, t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.CategoryTheory.Category.PartialFun
/-- The category of types equipped with partial functions.  -/
PartialFun : Type (u + 1)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.realSize_toHeap : ∀ {α : Type u_1} (s : Batteries.BinomialHeap.Imp.HeapNode α), s.toHeap.realSize = s.realSize