mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
map_extChartAt_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M),
  Filter.map (↑(extChartAt I x)) (nhds x) = nhdsWithin (↑(extChartAt I x) x) (Set.range ↑I)
-- Mathlib.Order.Category.PartOrd
PartOrd.hom_inv_apply : ∀ {X Y : PartOrd} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.NumberTheory.PellMatiyasevic
_private.Mathlib.NumberTheory.PellMatiyasevic.0.Pell.IsPell.match_1.splitter : {d : ℤ} → (motive : ℤ√d → Sort u_1) → (x : ℤ√d) → ((x y : ℤ) → motive { re := x, im := y }) → motive x
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.quot_mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (x y : RingCat.Colimits.Prequotient F),
  Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) (x.mul y) =
    (have this := Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) x;
      this) *
      have this := Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) y;
      this
-- Lean.Parser.Extension
Lean.Parser.AliasValue.const.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (p : α), sizeOf (Lean.Parser.AliasValue.const p) = 1 + sizeOf p
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.J_le_monomorphisms : SSet.modelCategoryQuillen.J ≤ CategoryTheory.MorphismProperty.monomorphisms SSet
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits_le_ofUnits_iff : ∀ {M : Type u_1} [inst : Monoid M] {S T : Subgroup Mˣ}, S.ofUnits ≤ T.ofUnits ↔ S ≤ T
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∈ m₂ → (m₁ \ m₂).get! k = default
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.comap_le_iff_le_map : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {m' : MeasurableSpace β} {f : α → β},
  MeasurableSpace.comap f m' ≤ m ↔ m' ≤ MeasurableSpace.map f m
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.instLawfulVecOperatorMapTargetMap : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.RefVec.MapTarget fun {len} => Std.Sat.AIG.RefVec.map
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mem_aroots' : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
  {p : Polynomial T} {a : S}, a ∈ p.aroots S ↔ Polynomial.map (algebraMap T S) p ≠ 0 ∧ (Polynomial.aeval a) p = 0
-- Mathlib.Data.Finsupp.Single
Finsupp.uniqueEquiv_symm_apply_apply : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α) [inst_1 : Subsingleton α] (m : M) (b : α),
  ((Finsupp.uniqueEquiv a).symm m) b = m
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b`
is smaller than all elements of `s`, and that this is not the case of any `w>b`.
See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices.  -/
csInf_eq_of_forall_ge_of_forall_gt_exists_lt : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {b : α},
  s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ (w : α), b < w → ∃ a ∈ s, a < w) → sInf s = b
-- Init.Data.List.Nat.Modify
List.tail_modifyHead : ∀ {α : Type u_1} {f : α → α} {l : List α}, (List.modifyHead f l).tail = l.tail
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- For a Lie derivation from a Lie algebra to itself, the usual Leibniz rule holds.  -/
LieDerivation.apply_lie_eq_add : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (D : LieDerivation R L L) (a b : L), D ⁅a, b⁆ = ⁅a, D b⁆ + ⁅D a, b⁆
-- Mathlib.CategoryTheory.Skeletal
/-- The functor from a category to its thin skeleton.  -/
CategoryTheory.toThinSkeleton : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor C (CategoryTheory.ThinSkeleton C)
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Quiver.Hom.toLoc_as : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {a b : C} (f : a ⟶ b), f.toLoc.as = f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.instTrans : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Trans Std.TreeMap.Equiv Std.TreeMap.Equiv Std.TreeMap.Equiv
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.mem_pointwise_smul_iff_inv_smul_mem : ∀ {M : Type u_1} {R : Type u_2} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S : Subsemiring R} {x : R}, x ∈ a • S ↔ a⁻¹ • x ∈ S
-- Mathlib.RingTheory.Artinian.Module
/-- If an element of an Artinian ring is not a zero divisor then it is a unit.  -/
IsArtinianRing.isUnit_of_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : Ring R] [IsArtinianRing R] {a : R}, a ∈ nonZeroDivisors R → IsUnit a
-- Mathlib.Data.Fin.Tuple.Sort
Tuple.graph.proj.eq_1 : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} (p : ↥(Tuple.graph f)), Tuple.graph.proj p = (↑p).1
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.instCoeSortType.eq_1 : AddMagmaCat.instCoeSortType = { coe := AddMagmaCat.carrier }
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.ofIsIso_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N)
  [inst_3 : CategoryTheory.IsIso f] (σ : M.QuasicoherentData) (a : σ.I),
  (SheafOfModules.QuasicoherentData.ofIsIso f σ).X a = σ.X a
-- Lean.SubExpr
Lean.SubExpr.GoalLocation.hypType.sizeOf_spec : ∀ (a : Lean.FVarId) (a_1 : Lean.SubExpr.Pos),
  sizeOf (Lean.SubExpr.GoalLocation.hypType a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.toFun_eq_coe : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Zero 𝕜] [inst_1 : LE α] (f : IncidenceAlgebra 𝕜 α), f.toFun = ⇑f
-- Mathlib.Order.UpperLower.Fibration
Relation.fibration_iff_isUpperSet_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : LE β],
  Relation.Fibration (fun x1 x2 => x1 ≥ x2) (fun x1 x2 => x1 ≥ x2) f ↔ ∀ (s : Set α), IsUpperSet s → IsUpperSet (f '' s)
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- **Alias** of `FourierTransform.fourierInvCLM`. -/
TemperedDistribution.fourierTransformInvCLM : (R : Type u_2) →
  (E : Type u_3) →
    {F : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : AddCommMonoid F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] →
                [inst_5 : FourierTransformInv E F] →
                  [FourierInvAdd E F] →
                    [FourierInvSMul R E F] →
                      [inst_8 : TopologicalSpace E] →
                        [inst_9 : TopologicalSpace F] → [ContinuousFourierInv E F] → E →L[R] F
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.invOf_eq_inv : ∀ {R : Type u} {M : Type v} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M] [inst_2 : Module Rᵐᵒᵖ M]
  [inst_3 : Module R M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) [inst_5 : Invertible x], ⅟x = x⁻¹
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valuation.norm.eq_1 : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀)
  [hv : v.RankOne] (x : L), v.norm x = ↑((Valuation.RankOne.hom v) (v.restrict x))
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a b : α}, cmp a b = Ordering.eq → t[a]! = t[b]!
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nnnorm_toLp_single : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : DecidableEq ι] (i : ι) (b : β i),
  ‖WithLp.toLp p (Pi.single i b)‖₊ = ‖b‖₊
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
ArithmeticFunction.carmichael_two_pow_of_le_two_eq_totient : ∀ {n : ℕ}, n ≤ 2 → ArithmeticFunction.carmichael (2 ^ n) = (2 ^ n).totient
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.isBigO_sub : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x₀ : E} {s : Set E},
  HasFDerivWithinAt f f' s x₀ → (fun x => f x - f x₀) =O[nhdsWithin x₀ s] fun x => x - x₀
-- Mathlib.NumberTheory.LegendreSymbol.Basic
legendreSym.eq_one_iff' : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {a : ℕ}, ↑a ≠ 0 → (legendreSym p ↑a = 1 ↔ IsSquare ↑a)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_denumerable : ∀ (α : Type u) [Denumerable α], Cardinal.mk α = Cardinal.aleph0
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_eq_zero_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α}, s.mulEnergy t = 0 ↔ s = ∅ ∨ t = ∅
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.isMaxOn_T_real : ∀ {n k : ℕ},
  n ≠ 0 →
    k ≤ n →
      Even k →
        IsMaxOn (fun x => Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n)) (Set.Icc (-1) 1)
          (Real.cos (↑k * Real.pi / ↑n))
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_tmul : ∀ {𝕜 : 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) (g : G →L[𝕜] H) (m : E) (n : G),
  (TensorProduct.mapL f g) (m ⊗ₜ[𝕜] n) = f m ⊗ₜ[𝕜] g n
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.quasiIso_truncGEπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ),
  (∀ i < n, QuasiIsoAt f i) →
    ∀ [CategoryTheory.Mono f] [CategoryTheory.Mono (HomologicalComplex.homologyMap f n)],
      QuasiIso ((CategoryTheory.Limits.cokernel f).πTruncGE n)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.map_map_base : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G)
  {a b : F.Grothendieck} (f : a ⟶ b), ((CategoryTheory.Pseudofunctor.Grothendieck.map α).map f).base = f.base
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
CategoryTheory.InducedCategory.hasForget₂ : {C : Type u_1} →
  {D : Type u_3} →
    [inst : CategoryTheory.Category.{v_2, u_3} D] →
      {FD : outParam (D → D → Type u_4)} →
        {CD : outParam (D → Type w)} →
          [inst_1 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] →
            [inst_2 : CategoryTheory.ConcreteCategory D FD] →
              (f : C → D) → CategoryTheory.HasForget₂ (CategoryTheory.InducedCategory D f) D
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHomClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B]
  [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B] [inst_7 : FunLike F A B]
  [toCoalgHomClass : CoalgHomClass F R A B] [toMonoidHomClass : MonoidHomClass F A B], BialgHomClass F R A B
-- Batteries.Data.List.Basic
List.swap.eq_1 : ∀ {α : Type u_1} (x x_1 : ℕ), [].swap x x_1 = []
-- Mathlib.RingTheory.DedekindDomain.Different
/-- The dual of a non-zero fractional ideal is the dual of the submodule under the trace form.  -/
FractionalIdeal.dual : (A : Type u_1) →
  (K : Type u_2) →
    {L : Type u} →
      {B : Type u_3} →
        [inst : CommRing A] →
          [inst_1 : Field K] →
            [inst_2 : CommRing B] →
              [inst_3 : Field L] →
                [inst_4 : Algebra A K] →
                  [inst_5 : Algebra B L] →
                    [inst_6 : Algebra A B] →
                      [inst_7 : Algebra K L] →
                        [inst_8 : Algebra A L] →
                          [IsScalarTower A K L] →
                            [IsScalarTower A B L] →
                              [IsFractionRing A K] →
                                [IsIntegrallyClosed A] →
                                  [FiniteDimensional K L] →
                                    [IsIntegralClosure B A L] →
                                      [Algebra.IsSeparable K L] →
                                        [IsDomain A] →
                                          [IsFractionRing B L] →
                                            [Nontrivial B] →
                                              [NoZeroDivisors B] →
                                                FractionalIdeal (nonZeroDivisors B) L →
                                                  FractionalIdeal (nonZeroDivisors B) L
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.instInhabited : {α : Type u_2} →
  {β : Type u_3} → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → Inhabited (α →ₙ+* β)
-- Mathlib.RingTheory.IsAdjoinRoot
/-- If `α` generates `S` as an algebra and `S` is free and finite,
then `S` is given by adjoining a root of `minpoly R α`.
Does not require that `R` is an integral domain, unlike `mkOfAdjoinEqTop`.  -/
IsAdjoinRootMonic.mkOfAdjoinEqTop' : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          [Module.Finite R S] → [Module.Free R S] → {α : S} → R[α] = ⊤ → IsAdjoinRootMonic S (minpoly R α)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The map `Cochain K L n → Cochain (K⟦a⟧) L n'` when `n + a = n'`.  -/
CochainComplex.HomComplex.Cochain.leftShift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          CochainComplex.HomComplex.Cochain K L n →
            (a n' : ℤ) →
              n + a = n' →
                CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Topology.IsGeneratedBy.coinduced`. -/
DeltaGeneratedSpace.coinduced : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [Topology.IsGeneratedBy X Y] (f : Y → Z), Topology.IsGeneratedBy X Z
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable : ∀ {X : Type u_1} [inst : UniformSpace X] [CompleteSpace X] [(uniformity X).IsCountablyGenerated] [T0Space X],
  TopologicalSpace.IsCompletelyMetrizableSpace X
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instCommSemigroup.eq_1 : ∀ {α : Type u_1} [inst : CommSemigroup α],
  Colex.instCommSemigroup = { toSemigroup := Colex.instSemigroup, mul_comm := ⋯ }
-- Mathlib.Algebra.Module.LinearMap.Basic
DomMulAct.coe_smul_linearMap : ∀ {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [inst : Semiring R] [inst_1 : Semiring R']
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M] [inst_5 : Module R' M'] {σ₁₂ : R →+* R'}
  {S' : Type u_6} [inst_6 : Monoid S'] [inst_7 : DistribMulAction S' M] [inst_8 : SMulCommClass R S' M] (a : S'ᵈᵐᵃ)
  (f : M →ₛₗ[σ₁₂] M'), ⇑(a • f) = a • ⇑f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_alter_of_not_compare_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  ¬cmp k k' = Ordering.eq → (t.alter k f).contains k' = t.contains k'
-- Mathlib.Algebra.MvPolynomial.Counit
MvPolynomial.ACounit_C : ∀ {A : Type u_1} (B : Type u_2) [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Algebra A B] (a : A),
  (MvPolynomial.ACounit A B) (MvPolynomial.C a) = (algebraMap A B) a
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
DirectSum.of.eq_1 : ∀ {ι : Type v} (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] (i : ι),
  DirectSum.of β i = DFinsupp.singleAddHom β i
-- Mathlib.Condensed.Limits
instHasLimitsOfShapeCondensed : ∀ {A : Type u_1} {J : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J] [CategoryTheory.Limits.HasLimitsOfShape J A],
  CategoryTheory.Limits.HasLimitsOfShape J (Condensed A)
-- Mathlib.Topology.Constructions
CofiniteTopology.isOpen_iff' : ∀ {X : Type u} {s : Set (CofiniteTopology X)}, IsOpen s ↔ s = ∅ ∨ sᶜ.Finite
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.mapₐ_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} (R : Type u_7) [inst_1 : CommSemiring R]
  [inst_2 : Semiring Y] [inst_3 : Algebra R Y] [inst_4 : Semiring Z] [inst_5 : Algebra R Z] (f : Y →ₐ[R] Z)
  (g : LocallyConstant X Y) (a : X), ((LocallyConstant.mapₐ R f) g) a = f (g a)
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.coassoc_right : ∀ {R : Type u_1} {M : Type u_3} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] [inst_5 : Coalgebra R M] (f : M →ₗ[R] M'),
  ↑(TensorProduct.assoc R M' M M).symm ∘ₗ TensorProduct.map f CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul =
    TensorProduct.map (TensorProduct.map f LinearMap.id) LinearMap.id ∘ₗ
      TensorProduct.map CoalgebraStruct.comul LinearMap.id ∘ₗ CoalgebraStruct.comul
-- Mathlib.Data.List.SplitLengths
List.flatten_splitLengths : ∀ {α : Type u_1} (l : List α) (sz : List ℕ), l.length ≤ sz.sum → (sz.splitLengths l).flatten = l
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.closedBall_div : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → ∀ (x : E), Metric.closedBall x δ * s = x • Metric.cthickening δ s
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap.congr_simp : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ i₀_1 : J} (e_i₀ : i₀ = i₀_1)
  (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ φ_1 : i ⟶ j),
  φ = φ_1 → ∀ (hφ : Nonempty (i₀ ⟶ i)), h.isoMap φ hφ = ⋯.isoMap φ_1 ⋯
-- Mathlib.Algebra.Group.Basic
right_eq_mul : ∀ {M : Type u_4} [inst : Monoid M] [IsRightCancelMul M] {a b : M}, b = a * b ↔ a = 1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_self : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), dist x x = 0
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.empty_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering}, RBTree.RBSet.empty = ∅
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.  -/
CategoryTheory.Limits.isSplitMono_coprod_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair X Y)],
  CategoryTheory.IsSplitMono CategoryTheory.Limits.coprod.inl
-- Mathlib.Computability.RegularExpressions
RegularExpression.comp : {α : Type u} → RegularExpression α → RegularExpression α → RegularExpression α
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_zero : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G), S.lowerCentralSeries 0 = S
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue!_modifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {k k' : α} [hi : Inhabited β] {f : β → β}
  (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValue! k' (Std.Internal.List.Const.modifyKey k f l) =
      if (k == k') = true then (Option.map f (Std.Internal.List.getValue? k l)).get!
      else Std.Internal.List.getValue! k' l
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.rootSet_monomial : ∀ {R : Type u} {S : Type v} [inst : Field R] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra R S] {n : ℕ},
  n ≠ 0 → ∀ {a : R}, a ≠ 0 → ((Polynomial.monomial n) a).rootSet S = {0}
-- Mathlib.Algebra.Ring.NonZeroDivisors
IsAddRightRegular.nsmul_injective : ∀ {M : Type u_2} [inst : AddMonoid M] [IsAddTorsionFree M] {x : M},
  IsAddRightRegular x → x ≠ 0 → Function.Injective fun n => n • x
-- Init.Data.String.Substring
/-- Folds a function over a substring from the right, accumulating a value starting with `init`. The
accumulated value is combined with each character in reverse order, using `f`.
 -/
Substring.Raw.foldr : {α : Type u} → (Char → α → α) → α → Substring.Raw → α
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.mass_map_le : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] (f : Ω → Ω')
  (μ : MeasureTheory.FiniteMeasure Ω), (μ.map f).mass ≤ μ.mass
-- Mathlib.GroupTheory.Sylow
Sylow.mk.sizeOf_spec : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [inst_1 : SizeOf G] (toSubgroup : Subgroup G)
  (isPGroup' : IsPGroup p ↥toSubgroup)
  (is_maximal' : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup ≤ Q → Q = toSubgroup),
  sizeOf { toSubgroup := toSubgroup, isPGroup' := isPGroup', is_maximal' := is_maximal' } = 1 + sizeOf toSubgroup
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_id_comp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C),
  groupCohomology.cochainsMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap (MonoidHom.id G) φ)
      (groupCohomology.cochainsMap (MonoidHom.id G) ψ)
-- Lean.Meta.Tactic.Grind.Beta
_private.Lean.Meta.Tactic.Grind.Beta.0.Lean.Meta.Grind.isPropagateBetaTarget : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero' : ∀ {α : Type u_1} {E' : Type u_2} (𝕜 : Type u_4) {p : ENNReal} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E']
  [inst : NormedSpace ℝ E'],
  m ≤ m0 →
    ∀ (f : ↥(MeasureTheory.Lp E' p μ)),
      p ≠ 0 →
        p ≠ ⊤ →
          (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑f) s μ) →
            (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0) →
              MeasureTheory.AEStronglyMeasurable (↑↑f) μ → ↑↑f =ᵐ[μ] 0
-- Mathlib.Data.Set.Function
Equiv.bijOn_symm : ∀ {α : Type u_1} {β : Type u_2} {e : α ≃ β} {s : Set α} {t : Set β}, Set.BijOn (⇑e.symm) t s ↔ Set.BijOn (⇑e) s t
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.comap_leq_ker_subToSupQuotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M),
  Submodule.comap p.subtype (p ⊓ p') ≤ (LinearMap.subToSupQuotient p p').ker
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indep_iSup_of_disjoint : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  (∀ (i : ι), m i ≤ _mΩ) →
    ProbabilityTheory.iIndep m μ →
      ∀ {S T : Set ι}, Disjoint S T → ProbabilityTheory.Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) μ