mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.tsum_prod_uncurry : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousAdd α]
  [T3Space α] {f : β → γ → α},
  Summable (Function.uncurry f) →
    (∀ (b : β), Summable fun c => f b c) → ∑' (p : β × γ), Function.uncurry f p = ∑' (b : β) (c : γ), f b c
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
HomotopyCategory.instShiftSequenceIntUpHomologyFunctorOfNat : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.CategoryWithHomology C] →
        (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).ShiftSequence ℤ
-- Mathlib.Combinatorics.SimpleGraph.Operations
/-- The graph formed by forgetting `t`'s neighbours and instead giving it those of `s`. The `s-t`
edge is removed if present.  -/
SimpleGraph.replaceVertex : {V : Type u_1} → SimpleGraph V → V → V → [DecidableEq V] → SimpleGraph V
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_ofCoeff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (x : M →₀ R), (AddMonoidAlgebra.ofCoeff x).coeff = x
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instIntCastAdicCauchySequence : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → IntCast (AdicCompletion.AdicCauchySequence I R)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_functorPullback_post : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) {X : C} (U : CategoryTheory.Over X)
  (S : CategoryTheory.Sieve ((CategoryTheory.Over.post F).obj U)),
  (CategoryTheory.Sieve.overEquiv U) (CategoryTheory.Sieve.functorPullback (CategoryTheory.Over.post F) S) =
    CategoryTheory.Sieve.functorPullback F ((CategoryTheory.Sieve.overEquiv ((CategoryTheory.Over.post F).obj U)) S)
-- Mathlib.LinearAlgebra.Matrix.Ideal
RingCon.coe_ofMatrix_eq_relationMap : ∀ {R : Type u_1} {n : Type u_2} [inst : NonAssocSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {c : RingCon (Matrix n n R)} (i j : n), ⇑c.ofMatrix = Relation.Map (⇑c) (fun x => x i j) fun x => x i j
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) ⦃x : 𝕜⦄,
  x ∈ quasispectrum 𝕜 a →
    autoParam (p a) NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le._auto_1 → ‖x‖ ≤ ‖a‖
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The (exact) short complex attached to the cokernel cofork `cc`.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            CategoryTheory.Abelian.SpectralObject C ι →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    (r r' : ℤ) →
                      (hrr' : r + 1 = r') →
                        (hr : r₀ ≤ r) →
                          κ →
                            (pq' : κ) →
                              (i₀ i₁ i₂ i₃ i₃' : ι) →
                                i₀ = data.i₀ r pq' ⋯ →
                                  i₁ = data.i₁ pq' →
                                    i₂ = data.i₂ pq' →
                                      i₃ = data.i₃ r pq' ⋯ →
                                        i₃' = data.i₃ r' pq' ⋯ →
                                          (n₀ n₁ n₂ : ℤ) →
                                            n₁ = data.deg pq' →
                                              autoParam (n₀ + 1 = n₁)
                                                  CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc._auto_1 →
                                                autoParam (n₁ + 1 = n₂)
                                                    CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc._auto_3 →
                                                  CategoryTheory.ShortComplex C
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.ι_comp_colimitOpIsoOpLimit_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : Jᵒᵖ) {Z : Cᵒᵖ}
  (h : Opposite.op (CategoryTheory.Limits.limit F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.op j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitOpIsoOpLimit F).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F (Opposite.unop j)).op h
-- Mathlib.Topology.Separation.CompletelyRegular
/-- A T₃.₅ space is a completely regular space that is also T₀.  -/
T35Space : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The type of morphisms in `Rep.{w} k G`.  -/
Rep.Hom : {k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → Rep.{w, u, v} k G → Rep.{w, u, v} k G → Type w
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Returns the denominators `Bₙ` of `g`.  -/
GenContFract.dens : {K : Type u_2} → [DivisionRing K] → GenContFract K → Stream' K
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
Complex.differentiableAt_Gamma_nat_add_one : ∀ (n : ℕ), DifferentiableAt ℂ Complex.Gamma (↑n + 1)
-- Aesop.RuleSet
Aesop.instEmptyCollectionBaseRuleSet : EmptyCollection Aesop.BaseRuleSet
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg_def`. -/
Ideal.inertiaDeg'_def : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S]
  [hq : q.IsPrime] [inst_3 : Algebra (Localization.AtPrime (Ideal.under R q)) (Localization.AtPrime q)]
  [inst_4 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R q) q],
  q.inertiaDeg R = Module.finrank (Ideal.under R q).ResidueField q.ResidueField
-- Mathlib.CategoryTheory.Monad.Limits
/-- If `C` has limits of shape `J` then any coreflective subcategory has limits of shape `J`.  -/
CategoryTheory.hasLimitsOfShape_of_coreflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (R : CategoryTheory.Functor D C)
  [CategoryTheory.Coreflective R] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J D
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.prodMonoidal_whiskerLeft : ∀ (C₁ : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.MonoidalCategory C₁]
  (C₂ : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_3 : CategoryTheory.MonoidalCategory C₂]
  (X x x_1 : C₁ × C₂) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f =
    CategoryTheory.Prod.mkHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.1 f.1)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.2 f.2)
-- Mathlib.Data.Set.Card
Set.nonempty_inter_of_le_ncard_add_ncard : ∀ {α : Type u_1} {s t : Set α} [Finite α], Nat.card α ≤ s.ncard + t.ncard → s ∪ t ≠ Set.univ → (s ∩ t).Nonempty
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.instIsEquivalenceTriangleRotate : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  (CategoryTheory.Pretriangulated.rotate C).IsEquivalence
-- Init.Data.Int.Order
Int.add_nonneg_iff_neg_le : ∀ {a b : ℤ}, 0 ≤ a + b ↔ -b ≤ a
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_natCast : ∀ (n : ℕ), Cardinal.toNat ↑n = n
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- A single point is collinear.  -/
collinear_singleton : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p : P), Collinear k {p}
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.image_horn_lt_subcomplex : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι} {i : ι}
  (c : f.Cell i) [inst_1 : P.IsProper], c.horn.image c.map < (↑(P.p c.s)).subcomplex
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ (f : α → β → Option γ), (Std.TreeMap.Raw.filterMap f t₁).Equiv (Std.TreeMap.Raw.filterMap f t₂)
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.ofHom_hom : ∀ {R S : CommSemiRingCat} (f : R ⟶ S), CommSemiRingCat.ofHom (CommSemiRingCat.Hom.hom f) = f
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
/-- **Alias** of `NumberField.InfinitePlace.IsUnramified.finrank_eq_one`.

---

If `w` is an unramified place over `v` then `w.Completion` has `v.Completion` dimension one.  -/
NumberField.InfinitePlace.Completion.finrank_eq_one_of_isUnramified : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K) {w : NumberField.InfinitePlace L} [inst_3 : w.LiesOver v],
  NumberField.InfinitePlace.IsUnramified K w → Module.finrank v.Completion w.Completion = 1
-- Mathlib.LinearAlgebra.Basis.Prod
/-- `Basis.prod` maps an `ι`-indexed basis for `M` and an `ι'`-indexed basis for `M'`
to an `ι ⊕ ι'`-index basis for `M × M'`.
For the specific case of `R × R`, see also `Basis.finTwoProd`.  -/
Module.Basis.prod : {ι : Type u_1} →
  {ι' : Type u_2} →
    {R : Type u_3} →
      {M : Type u_5} →
        {M' : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : Module R M] →
                [inst_3 : AddCommMonoid M'] →
                  [inst_4 : Module R M'] → Module.Basis ι R M → Module.Basis ι' R M' → Module.Basis (ι ⊕ ι') R (M × M')
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.support_normed_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure],
  Function.support (f.normed μ) = Metric.ball c f.rOut
-- Mathlib.Data.Multiset.Count
Multiset.count_ne_zero : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {a : α}, Multiset.count a s ≠ 0 ↔ a ∈ s
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.Hom.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Abelian C} {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : CategoryTheory.SpectralSequence C c r₀} {x y : E.Hom E'},
  @CategoryTheory.SpectralSequence.Hom.hom C inst inst_1 κ c r₀ E E' x =
      @CategoryTheory.SpectralSequence.Hom.hom C inst inst_1 κ c r₀ E E' y →
    x = y
-- Mathlib.Analysis.Calculus.Deriv.Add
hasStrictDerivAt_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), HasStrictDerivAt Neg.neg (-1) x
-- Mathlib.Order.Ideal
/-- For a preorder `P`, `Cofinal P` is the type of subsets of `P`
containing arbitrarily large elements. They are the dense sets in
the topology whose open sets are terminal segments.  -/
Order.Cofinal : (P : Type u_2) → [Preorder P] → Type u_2
-- Mathlib.LinearAlgebra.Matrix.Gershgorin
/-- If `A` is a row strictly dominant diagonal matrix, then its determinant is nonzero.  -/
det_ne_zero_of_sum_row_lt_diag : ∀ {K : Type u_1} {n : Type u_2} [inst : NormedField K] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n K},
  (∀ (k : n), ∑ j ∈ Finset.univ.erase k, ‖A k j‖ < ‖A k k‖) → A.det ≠ 0
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Ico_left_eq_Ico_pred_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] {a b : α},
  a ≤ b → ¬IsMin a → insert (Order.pred a) (Finset.Ico a b) = Finset.Ico (Order.pred a) b
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
the periodic cochain complex
`0 ⟶ Hom(k[G], A) --(- ∘ (ρ(g) - 𝟙))--> Hom(k[G], A) --(- ∘ N)--> Hom(k[G], A) ⟶ ...`
is isomorphic as a complex in `ModuleCat k` to
`0 ⟶ A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A --N--> A ⟶ ...`.  -/
Rep.FiniteCyclicGroup.homResolutionIso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      [inst_2 : Fintype G] →
        (A : Rep.{u, u, u} k G) →
          (g : G) →
            (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) →
              (Rep.FiniteCyclicGroup.resolution k g hg).complex.linearYonedaObj k A ≅
                Rep.FiniteCyclicGroup.moduleCatCochainComplex A g
-- Lean.Message
Lean.MessageData.ofSyntax : Lean.Syntax → Lean.MessageData
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.uniqueUpToIso_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit),
  (CategoryTheory.Limits.biproduct.uniqueUpToIso f hb).hom = CategoryTheory.Limits.biproduct.lift b.π
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
/-- The (limit) cone for `F : J ⥤ PresheafOfModules.{v} R` that is constructed from the limit
of `F ⋙ evaluation R X` for all `X`.  -/
PresheafOfModules.limitCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {J : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
          (F : CategoryTheory.Functor J (PresheafOfModules R)) →
            [∀ (X : Cᵒᵖ),
                  Small.{v, max u₂ v}
                    ↑((F.comp (PresheafOfModules.evaluation R X)).comp
                          (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] →
              CategoryTheory.Limits.Cone F
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.sheafificationAdjunction_homEquiv_apply : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  {P : PresheafOfModules R₀} {F : SheafOfModules R} (f : (PresheafOfModules.sheafification α).obj P ⟶ F),
  ((PresheafOfModules.sheafificationAdjunction α).homEquiv P F) f = (PresheafOfModules.sheafificationHomEquiv α) f
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If a family is affinely independent, the spans of points indexed
by disjoint subsets of the index type are disjoint, if the underlying
ring is nontrivial.  -/
AffineIndependent.affineSpan_disjoint_of_disjoint : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P},
  AffineIndependent k p →
    ∀ {s1 s2 : Set ι}, Disjoint s1 s2 → Disjoint ↑(affineSpan k (p '' s1)) ↑(affineSpan k (p '' s2))
-- Mathlib.RingTheory.Nilpotent.Basic
IsNilpotent.not_isUnit : ∀ {R : Type u_1} [inst : Ring R] [Nontrivial R] {x : R}, IsNilpotent x → ¬IsUnit x
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- `lift r` is injective if `d` is non-square, and R has characteristic zero (that is, the map from
`ℤ` into `R` is injective).  -/
Zsqrtd.lift_injective : ∀ {R : Type u_1} [inst : CommRing R] [CharZero R] {d : ℤ} (r : { r // r * r = ↑d }),
  (∀ (n : ℤ), d ≠ n * n) → Function.Injective ⇑(Zsqrtd.lift r)
-- Mathlib.Order.SuccPred.Basic
Order.Ico_subset_Ioo_pred_left : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Ico b a ⊆ Set.Ioo (Order.pred b) a
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
isPiSystem_isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α], IsPiSystem {s | IsOpen s}
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If `|r| < 1`, then `n ^ k r ^ n` tends to zero for any natural `k`.  -/
tendsto_pow_const_mul_const_pow_of_abs_lt_one : ∀ (k : ℕ) {r : ℝ}, |r| < 1 → Filter.Tendsto (fun n => ↑n ^ k * r ^ n) Filter.atTop (nhds 0)
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply : ∀ (X : Type u) (S : LightProfinite)
  (s : CategoryTheory.Limits.Cocone (S.diagram.rightOp.comp (LightCondensed.locallyConstantPresheaf X))) (n : ℕ)
  (f : LocallyConstant (↑(S.diagram.obj (Opposite.op n)).toTop) X),
  (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isColimitLocallyConstantPresheafDiagram X S).desc s))
      (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app (Opposite.op n)).hom) f) =
    (CategoryTheory.ConcreteCategory.hom (s.ι.app n)) f
-- Mathlib.GroupTheory.SpecificGroups.Alternating
Equiv.Perm.mem_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {f : Equiv.Perm α},
  f ∈ alternatingGroup α ↔ Equiv.Perm.sign f = 1
-- Mathlib.Combinatorics.SetFamily.HarrisKleitman
IsLowerSet.nonMemberSubfamily : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {a : α},
  IsLowerSet ↑𝒜 → IsLowerSet ↑(Finset.nonMemberSubfamily a 𝒜)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Param.mk : {pu : Lean.Compiler.LCNF.Purity} → Lean.FVarId → Lean.Name → Lean.Expr → Bool → Lean.Compiler.LCNF.Param pu
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.map_add_left_ae : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddLeftInvariant] (x : G), Filter.map (fun h => x + h) (MeasureTheory.ae μ) = MeasureTheory.ae μ
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, a ∈ t.insert k ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.baseSupp.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [inst_4 : Fintype ι] (i : ι),
  b.baseSupp i =
    ∑ j,
      b.A i j •
        ((Module.Basis.span ⋯).map (LinearEquiv.ofEq H.toSubmodule (Submodule.span R (Set.range b.h)) ⋯).symm).coord j
-- Init.Data.Array.Lemmas
/-- Variant of `getElem_append_left` useful for rewriting from the small array to the big array.  -/
Array.getElem_append_left' : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (hi : i < xs.size) (ys : Array α), xs[i] = (xs ++ ys)[i]
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.id_obj : ∀ {C : CategoryTheory.Cat} (X : ↑C), (CategoryTheory.CategoryStruct.id C).toFunctor.obj X = X
-- Mathlib.Algebra.Free
instDecidableEqFreeMagma : {α : Type u_1} → [DecidableEq α] → DecidableEq (FreeMagma α)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapL.eq_1 : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5}
  [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)]
  (f : (i : ι) → E i →L[𝕜] E' i),
  PiTensorProduct.mapL f =
    (PiTensorProduct.liftIsometry 𝕜 E (PiTensorProduct 𝕜 fun i => E' i))
      ((PiTensorProduct.tprodL 𝕜).compContinuousLinearMap f)
-- Init.Data.Fin.Lemmas
/-- An induction principle for `Fin` that considers a given `i : Fin n` as given by a sequence of `i`
applications of `Fin.succ`.

The cases in the induction are:
 * `zero` demonstrates the motive for `(0 : Fin (n + 1))` for all bounds `n`
 * `succ` demonstrates the motive for `Fin.succ` applied to an arbitrary `Fin` for an arbitrary
   bound `n`

Unlike `Fin.induction`, the motive quantifies over the bound, and the bound varies at each inductive
step. `Fin.succRec` is a version of this induction principle that takes the `Fin` argument last.
 -/
Fin.succRecOn : {n : ℕ} →
  (i : Fin n) →
    {motive : (n : ℕ) → Fin n → Sort u_1} →
      ((n : ℕ) → motive (n + 1) 0) → ((n : ℕ) → (i : Fin n) → motive n i → motive n.succ i.succ) → motive n i
-- Mathlib.MeasureTheory.Measure.OpenPos
Metric.measure_closedBall_pos_iff : ∀ {X : Type u_2} [inst : MetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  [MeasureTheory.NullSingletonClass μ] {x : X} {r : ℝ}, 0 < μ (Metric.closedBall x r) ↔ 0 < r
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.link.congr_simp : ∀ {α : Type u} {β : α → Type v} (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (hr : r.Balanced),
      Std.DTreeMap.Internal.Impl.link k v l r hl hr = Std.DTreeMap.Internal.Impl.link k v_1 l r hl hr
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instHasModelBitVecOfNatNat : HasModel✝ Int8 (BitVec 8)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
/-- the index of the cell  -/
HomotopicalAlgebra.RelativeCellComplex.Cells.k : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} →
                      {f : X ⟶ Y} →
                        {c : HomotopicalAlgebra.RelativeCellComplex basicCell f} →
                          (self : c.Cells) → (c.attachCells self.j ⋯).ι
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.pow_nat : ∀ {R : Type u_1} [inst : CommSemiring R] {a : R} {b c k : ℕ} {d e : R}, b = c * k → a ^ c = d → d ^ k = e → a ^ b = e
-- Init.Prelude
HomogeneousPow.mk : {α : Type u} → (α → α → α) → HomogeneousPow α
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the largest key in the tree map, returning `none` if the map is empty.
 -/
Std.DTreeMap.maxKey? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Option α
-- Mathlib.Data.WSeq.Basic
/-- auxiliary definition of tail over weak sequences  -/
Stream'.WSeq.tail.aux : {α : Type u} → Option (α × Stream'.WSeq α) → Computation (Option (α × Stream'.WSeq α))
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}, F.rightAdjointObjIsDefined = ⊤ → F.IsLeftAdjoint
-- Mathlib.Order.CompleteLattice.Basic
iSup_le_iSup_of_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s t : Set β},
  s ⊆ t → ⨆ x ∈ s, f x ≤ ⨆ x ∈ t, f x