mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_sdiff_eq_div : ∀ {ι : Type u_1} {G : Type u_3} {s₁ s₂ : Finset ι} [inst : CommGroup G] [inst_1 : DecidableEq ι] {f : ι → G},
  s₁ ⊆ s₂ → ∏ x ∈ s₂ \ s₁, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.algebraTensorAlgEquiv.eq_1 : ∀ (R : Type u) [inst : CommSemiring R] {σ : Type u_1} (A : Type u_4) [inst_1 : CommSemiring A] [inst_2 : Algebra R A],
  MvPolynomial.algebraTensorAlgEquiv R A = AddMonoidAlgebra.scalarTensorEquiv R A
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Get the discrimination tree matches with theorems from imported files.  -/
Mathlib.Tactic.ClickSuggestions.getImportMatches : {α : Type} →
  IO.Ref (Option (Lean.Meta.RefinedDiscrTree α)) → Lean.Expr → Lean.MetaM (Lean.Meta.RefinedDiscrTree.MatchResult α)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.colimitCoconeOfUnique_cocone_ι : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C),
  (CategoryTheory.Limits.colimitCoconeOfUnique f).cocone.ι =
    CategoryTheory.Discrete.natTrans fun x =>
      match x with
      | { as := j } => CategoryTheory.eqToHom ⋯
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.addNamespaceCompletionItem : Lean.Name → Lean.Server.Completion.M✝ Unit
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Poly.combine.match_1.splitter : (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Sort u_1) →
  (p₁ p₂ : Lean.Grind.Linarith.Poly) →
    ((p₂ : Lean.Grind.Linarith.Poly) → motive Lean.Grind.Linarith.Poly.nil p₂) →
      ((p₁ : Lean.Grind.Linarith.Poly) →
          (p₁ = Lean.Grind.Linarith.Poly.nil → False) → motive p₁ Lean.Grind.Linarith.Poly.nil) →
        ((a₁ : ℤ) →
            (x₁ : Lean.Grind.Linarith.Var) →
              (p₁ : Lean.Grind.Linarith.Poly) →
                (a₂ : ℤ) →
                  (x₂ : Lean.Grind.Linarith.Var) →
                    (p₂ : Lean.Grind.Linarith.Poly) →
                      motive (Lean.Grind.Linarith.Poly.add a₁ x₁ p₁) (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂)) →
          motive p₁ p₂
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.ediam_range : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂),
  Metric.ediam (Set.range ⇑f) = Metric.ediam Set.univ
-- Mathlib.Data.Set.Prod
Set.union_pi_inter : ∀ {ι : Type u_1} {α : ι → Type u_2} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)},
  (∀ i ∉ s₁, t₁ i = Set.univ) → (∀ i ∉ s₂, t₂ i = Set.univ) → ((s₁ ∪ s₂).pi fun i => t₁ i ∩ t₂ i) = s₁.pi t₁ ∩ s₂.pi t₂
-- Mathlib.CategoryTheory.Functor.TypeValuedFlat
/-- Given a functor `F : C ⥤ Type w`, an object `X : C` and `x : F.obj X`,
this is the functor `Over X ⥤ Type w` which sends an object of `Over X`
corresponding to a morphism `f : Y ⟶ X` to the subtype of `F.obj Y`
consisting of those elements `y : F.obj Y` such that `F.map f y = x`.  -/
CategoryTheory.FunctorToTypes.fromOverFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type w)) →
      {X : C} → F.obj X → CategoryTheory.Functor (CategoryTheory.Over X) (Type w)
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.uniformBell_eq_div : ∀ (m : ℕ) {n : ℕ}, n ≠ 0 → m.uniformBell n = (m * n).factorial / (n.factorial ^ m * m.factorial)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- The cofan `cofan₃MapBifunctorBifunctor₂₃MapObj` is a colimit, see the induced isomorphism
`mapBifunctorComp₁₂MapObjIso`.  -/
CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₂₃ : Type u_6} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] →
                    (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) →
                      (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) →
                        {I₁ : Type u_7} →
                          {I₂ : Type u_8} →
                            {I₃ : Type u_9} →
                              {J : Type u_10} →
                                {r : I₁ × I₂ × I₃ → J} →
                                  (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) →
                                    (X₁ : CategoryTheory.GradedObject I₁ C₁) →
                                      (X₂ : CategoryTheory.GradedObject I₂ C₂) →
                                        (X₃ : CategoryTheory.GradedObject I₃ C₃) →
                                          [inst_5 :
                                              (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj
                                                    X₃).HasMap
                                                ρ₂₃.p] →
                                            [inst_6 :
                                                (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
                                                      (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂
                                                        X₃)).HasMap
                                                  ρ₂₃.q] →
                                              [H :
                                                  CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂
                                                    X₃] →
                                                (j : J) →
                                                  CategoryTheory.Limits.IsColimit
                                                    (CategoryTheory.GradedObject.cofan₃MapBifunctorBifunctor₂₃MapObj F
                                                      G₂₃ ρ₂₃ X₁ X₂ X₃ j)
-- Mathlib.CategoryTheory.CommSq
/-- A `LiftStruct` for a commutative square gives a `LiftStruct` for the
corresponding square in the opposite category.  -/
CategoryTheory.CommSq.LiftStruct.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A B X Y : C} →
      {f : A ⟶ X} →
        {i : A ⟶ B} → {p : X ⟶ Y} → {g : B ⟶ Y} → {sq : CategoryTheory.CommSq f i p g} → sq.LiftStruct → ⋯.LiftStruct
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
/-- An object `X` in a category `C` is Artinian if `Subobject X`
satisfies the descending chain condition. This definition is a
term in `ObjectProperty C` which allows to study the stability
properties of Artinian objects. For statements regarding
specific objects, it is advisable to use the type class
`IsArtinianObject` instead.  -/
CategoryTheory.isArtinianObject : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.Hom.id_single.sizeOf_spec : ∀ {ι : Type v} [inst : SizeOf ι] (i : ι), sizeOf (CategoryTheory.Pairwise.Hom.id_single i) = 1 + sizeOf i
-- Mathlib.CategoryTheory.Limits.Filtered
CategoryTheory.Limits.hasCofilteredLimitsOfSize_of_hasLimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfSize.{w', w, v, u} C],
  CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v, u} C
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
CategoryTheory.Functor.instCommShiftPlusMapHomotopyCategoryPlusInt : {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] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] →
            (F : CategoryTheory.Functor C D) → [inst_4 : F.Additive] → F.mapHomotopyCategoryPlus.CommShift ℤ
-- Lean.Parser.Types
Lean.Parser.FirstTokens.optTokens.injEq : ∀ (a a_1 : List Lean.Parser.Token),
  (Lean.Parser.FirstTokens.optTokens a = Lean.Parser.FirstTokens.optTokens a_1) = (a = a_1)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.toWeightBasis.eq_1 : ∀ {ι : 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] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsRootSystem], b.toWeightBasis = Module.Basis.mk ⋯ ⋯
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.map.eq_1 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → γ a),
  Std.DHashMap.Internal.AssocList.map f = Std.DHashMap.Internal.AssocList.map.go✝ f Std.DHashMap.Internal.AssocList.nil
-- Init.Sym.Lemmas
Lean.Sym.Int.lt_eq_false : ∀ (a b : ℤ), decide (a < b) = false → (a < b) = False
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.le_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {k fallback : α}, (cmp k (t.minKeyD fallback)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.GroupTheory.ClassEquation
/-- Conjugacy classes form a partition of G, stated in terms of cardinality.  -/
sum_conjClasses_card_eq_card : ∀ (G : Type u_1) [inst : Group G] [inst_1 : Fintype (ConjClasses G)] [inst_2 : Fintype G]
  [inst_3 : (x : ConjClasses G) → Fintype ↑x.carrier], ∑ x, x.carrier.toFinset.card = Fintype.card G
-- Mathlib.Data.Set.Basic
Set.sep_ext_iff : ∀ {α : Type u} {s : Set α} {p q : α → Prop}, {x | x ∈ s ∧ p x} = {x | x ∈ s ∧ q x} ↔ ∀ x ∈ s, p x ↔ q x
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.compQuadraticMap'_apply : ∀ {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : CommSemiring S] [inst_7 : Algebra S R] [inst_8 : Module S N]
  [inst_9 : Module S M] [inst_10 : IsScalarTower S R N] [inst_11 : IsScalarTower S R M] [inst_12 : Module S P]
  (f : N →ₗ[S] P) (Q : QuadraticMap R M N) (x : M), (f.compQuadraticMap' Q) x = f (Q x)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- The base case of equation (1): `S₀(α) = {ε}`, the singleton of the empty
word `ε`.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.S_zero : ∀ {n : ℕ} (i : Fin n), BirdDet.S✝ 0 i = {![]}
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_sInf : ∀ {s : Set NNReal}, s.Nonempty → ↑(sInf s) = ⨅ a ∈ s, ↑a
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteSAsRing.eq_4 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (a b : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteSAsRing ctx (a.add b) =
    Lean.Grind.CommRing.Expr.denoteSAsRing ctx a + Lean.Grind.CommRing.Expr.denoteSAsRing ctx b
-- Mathlib.Order.Grade
/-- Maximal elements have maximal grades.  -/
GradeBoundedOrder.isMax_grade : ∀ {𝕆 : Type u_5} {α : Type u_6} {inst : Preorder 𝕆} {inst_1 : Preorder α} [self : GradeBoundedOrder 𝕆 α] ⦃a : α⦄,
  IsMax a → IsMax (GradeOrder.grade a)
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIoi : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderTop α] → (a : α) → Fintype ↑(Set.Ioi a)
-- 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₀} {f f' : E ⟶ E'},
  (∀ (r : ℤ) (hr : r₀ ≤ r), f.hom r ⋯ = f'.hom r ⋯) → f = f'
-- Mathlib.Topology.Compactness.Lindelof
/-- `X` is a non-Lindelöf topological space if it is not a Lindelöf space.  -/
NonLindelofSpace : (X : Type u_2) → [TopologicalSpace X] → Prop
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRight_obj_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (r : R₂ ⟶ R₁) (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRight L r).obj X).left = X.left
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.alterₘ.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} (a : α) (motive : Option (β a) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (b : β a) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Init.Data.String.Slice
/-- Creates a `String` from a `String.Slice` by copying the bytes.  -/
String.Slice.toString : String.Slice → String
-- ProofWidgets.Component.Basic
ProofWidgets.MarkdownDisplay.Props.mk.injEq : ∀ (contents contents_1 : String), ({ contents := contents } = { contents := contents_1 }) = (contents = contents_1)
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.intSpanEquivQuotAddOrderOf_apply : ∀ {A : Type uA} [inst : AddCommGroup A] (a : A) (x : ↥(ℤ ∙ a)),
  (CharacterModule.intSpanEquivQuotAddOrderOf a) x =
    ((LinearMap.toSpanSingleton ℤ A a).ker.quotEquivOfEq (Ideal.span {↑(addOrderOf a)}) ⋯)
      ((LinearMap.toSpanSingleton ℤ A a).quotKerEquivRange.symm
        ((LinearEquiv.ofEq (ℤ ∙ a) (LinearMap.toSpanSingleton ℤ A a).range ⋯) x))
-- Init.Data.Order.Lemmas
Std.instAntisymmLeOfLawfulOrderLTOfTrichotomousLt : ∀ {α : Type u} {x : LE α} [inst : LT α] [Std.LawfulOrderLT α] [Std.Trichotomous fun x1 x2 => x1 < x2],
  Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Mathlib.Logic.Basic
and_forall_ne : ∀ {α : Sort u_1} {p : α → Prop} (a : α), (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b
-- Init.Data.String.Basic
String.Slice.str_slice : ∀ {s : String.Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd}, (s.slice newStart newEnd h).str = s.str
-- Mathlib.LinearAlgebra.BilinearMap
/-- A version of `Function.Injective.comp` for composition of a bilinear map with a linear map.  -/
LinearMap.injective_compr₂_of_injective : ∀ {R : Type u_2} [inst : CommSemiring R] {M : Type u_5} {Nₗ : Type u_8} {Pₗ : Type u_9} {Qₗ : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid Nₗ] [inst_3 : AddCommMonoid Pₗ] [inst_4 : AddCommMonoid Qₗ]
  [inst_5 : Module R M] [inst_6 : Module R Nₗ] [inst_7 : Module R Pₗ] [inst_8 : Module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ)
  (g : Pₗ →ₗ[R] Qₗ), Function.Injective ⇑f → Function.Injective ⇑g → Function.Injective ⇑(f.compr₂ g)
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.IsBasis.cardinalMk_eq_cRk : ∀ {α : Type u} {M : Matroid α} {I X : Set α} [M.InvariantCardinalRank], M.IsBasis I X → Cardinal.mk ↑I = M.cRk X
-- Mathlib.Combinatorics.SimpleGraph.Prod
_private.Mathlib.Combinatorics.SimpleGraph.Prod.0.SimpleGraph.sum.match_1.splitter : {V : Type u_1} →
  {W : Type u_2} →
    (motive : V ⊕ W → V ⊕ W → Sort u_3) →
      (x x_1 : V ⊕ W) →
        ((u v : V) → motive (Sum.inl u) (Sum.inl v)) →
          ((u v : W) → motive (Sum.inr u) (Sum.inr v)) →
            ((x x_2 : V ⊕ W) →
                (∀ (u v : V), x = Sum.inl u → x_2 = Sum.inl v → False) →
                  (∀ (u v : W), x = Sum.inr u → x_2 = Sum.inr v → False) → motive x x_2) →
              motive x x_1
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.hasMFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x → HasMFDerivAt[s] f x (mfderiv[s] f x)
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- A triangle `(X,Y,Z,f,g,h)` in `C` is defined by the morphisms `f : X ⟶ Y`, `g : Y ⟶ Z`
and `h : Z ⟶ X⟦1⟧`.
 -/
CategoryTheory.Pretriangulated.Triangle.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {X Y Z : C} →
        (X ⟶ Y) → (Y ⟶ Z) → (Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) → CategoryTheory.Pretriangulated.Triangle C
-- Lean.Elab.Tactic.Config
Lean.Elab.Tactic.ConfigItemView.mk.injEq : ∀ (ref : Lean.Syntax) (option : Lean.Ident) (value : Lean.Term) (bool : Bool) (ref_1 : Lean.Syntax)
  (option_1 : Lean.Ident) (value_1 : Lean.Term) (bool_1 : Bool),
  ({ ref := ref, option := option, value := value, bool := bool } =
      { ref := ref_1, option := option_1, value := value_1, bool := bool_1 }) =
    (ref = ref_1 ∧ option = option_1 ∧ value = value_1 ∧ bool = bool_1)
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.mk.injEq : ∀ {n : ℕ} (A : Type u) (B : A → TypeVec.{u} n) (A_1 : Type u) (B_1 : A_1 → TypeVec.{u} n),
  ({ A := A, B := B } = { A := A_1, B := B_1 }) = (A = A_1 ∧ B ≍ B_1)
-- Mathlib.RingTheory.Depth.Rees
/-- **The Rees theorem**
For any `n : ℕ`, Noetherian ring `R`, `I : Ideal R`, and finitely generated and nontrivial
`R`-module `M` satisfying `IM < M`, the following are equivalent:
* for any `N : ModuleCat R` finitely generated and nontrivial with support contained in the
  zero locus of `I`, `∀ i < n, Ext N M i = 0`
* `∀ i < n, Ext (R ⧸ I) M i = 0`
* there exists a `N : ModuleCat R` finitely generated and nontrivial with support equal to the
  zero locus of `I`, `∀ i < n, Ext N M i = 0`
* there exists a `M`-regular sequence of length `n` with every element in `I`
 -/
ModuleCat.exists_isRegular_tfae : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (n : ℕ)
  (M : ModuleCat R) [Module.Finite R ↑M],
  I • ⊤ < ⊤ →
    [∀ (N : ModuleCat R),
          Nontrivial ↑N →
            Module.Finite R ↑N →
              Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I →
                ∀ i < n, Subsingleton (CategoryTheory.Abelian.Ext N M i),
        ∀ i < n, Subsingleton (CategoryTheory.Abelian.Ext (ModuleCat.of R (Shrink.{v, u} (R ⧸ I))) M i),
        ∃ N,
          Nontrivial ↑N ∧
            Module.Finite R ↑N ∧
              Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧
                ∀ i < n, Subsingleton (CategoryTheory.Abelian.Ext N M i),
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs].TFAE
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.mk_pow : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : Preorder α] [inst_2 : ZeroLEOneClass α] [inst_3 : PosMulMono α]
  {x : α} (hx : 0 ≤ x) (n : ℕ), ⟨x, hx⟩ ^ n = ⟨x ^ n, ⋯⟩
-- Mathlib.Data.ENNReal.Basic
ENNReal.lt_iff_exists_add_pos_lt : ∀ {a b : ENNReal}, a < b ↔ ∃ r, 0 < r ∧ a + ↑r < b
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- `mulForbidden F` is the set of configurations that avoid every pattern in `F`.

Formally: `x ∈ mulForbidden F` if and only if for every pattern `p ∈ F` and every
monoid element `g : G`, the pattern `p` does not occur in `x` at position `g`.

Intuitively, `mulForbidden F` is the shift space defined by declaring the finite set
(or family) of patterns `F` to be *forbidden*. A configuration belongs to the subshift if and only
it avoids all the forbidden patterns.  -/
SymbolicDynamics.FullShift.mulForbidden : {A : Type u_1} →
  {G : Type u_2} → [inst : Inhabited A] → [Monoid G] → Set (SymbolicDynamics.FullShift.Pattern A G) → Set (G → A)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- The bialgebra equivalence between `AddMonoidAlgebra` and `MonoidAlgebra` in terms of
`Multiplicative`.  -/
AddMonoidAlgebra.toMultiplicativeBialgEquiv : (R : Type u_1) →
  (A : Type u_3) →
    (M : Type u_8) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Bialgebra R A] →
            [inst_3 : AddMonoid M] → AddMonoidAlgebra A M ≃ₐc[R] MonoidAlgebra A (Multiplicative M)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.mul_zero : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel.below ⋯
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.of_aeval_smul : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] (f : Polynomial R) (m : M),
  (Module.AEval.of R M a) ((Polynomial.aeval a) f • m) = f • (Module.AEval.of R M a) m
-- Mathlib.Algebra.Group.Basic
leftInverse_add_right_neg_add : ∀ {G : Type u_3} [inst : AddGroup G] (c : G), Function.LeftInverse (fun x => c + x) fun x => -c + x
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.pentagonIso_assoc : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} E]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D)
  (K : CategoryTheory.Functor D E) {Z : CategoryTheory.Functor A E} (h : F.comp (G.comp (H.comp K)) ≅ Z),
  CategoryTheory.Functor.isoWhiskerRight (F.associator G H) K ≪≫
      F.associator (G.comp H) K ≪≫ F.isoWhiskerLeft (G.associator H K) ≪≫ h =
    (F.comp G).associator H K ≪≫ F.associator G (H.comp K) ≪≫ h
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` with a densely ordered codomain is monotone on a left neighborhood of `a` and
the closure of the image of this neighborhood under `f` is a left neighborhood of `f a`, then `f` is
continuous at `a` from the left  -/
continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α}
  {a : α},
  MonotoneOn f s →
    s ∈ nhdsWithin a (Set.Iic a) →
      closure (f '' s) ∈ nhdsWithin (f a) (Set.Iic (f a)) → ContinuousWithinAt f (Set.Iic a) a
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_neg : ∀ {R : Type u} [inst : Ring R] {a : AddMonoidAlgebra R ℕ}, { toFinsupp := -a } = -{ toFinsupp := a }
-- Mathlib.Data.Quot
Quotient.instSubsingletonQuotient : ∀ {α : Sort u_1} (s : Setoid α) [Subsingleton α], Subsingleton (Quotient s)
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- A monoidal category with binary coproducts is distributive
if it is both left and right distributive.  -/
CategoryTheory.IsMonoidalDistrib : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.MonoidalCategory C] → [CategoryTheory.Limits.HasBinaryCoproducts C] → Prop
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.extendEquiv_apply : ∀ (n : ℕ) (c : (c : OrderedFinpartition n) × Option (Fin c.length)),
  (OrderedFinpartition.extendEquiv n) c = c.fst.extend c.snd
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_sub_sub : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Sub β] [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.IndepFun (f i - f j) (f k - f l) μ