mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.Pi
/-- Restrict domain of a function `f` to a finite set `s`.  -/
Finset.restrict : {ι : Type u_2} → {π : ι → Type u_3} → (s : Finset ι) → ((i : ι) → π i) → (i : ↥s) → π ↑i
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections],
  Small.{u, max u v} ↑((F.comp (CategoryTheory.forget₂ GrpCat MonCat)).comp (CategoryTheory.forget MonCat)).sections
-- Mathlib.Data.ENat.Lattice
ENat.sSup_eq_zero' : ∀ {s : Set ℕ∞}, sSup s = 0 ↔ s = ∅ ∨ s = {0}
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The seminorms of the Schwartz space given by the best constants in the definition of
`𝓢(E, F)`.  -/
SchwartzMap.seminorm : (𝕜 : Type u_2) →
  {E : Type u_5} →
    {F : Type u_6} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [inst_4 : NormedField 𝕜] →
                [inst_5 : NormedSpace 𝕜 F] → [inst_6 : SMulCommClass ℝ 𝕜 F] → ℕ → ℕ → Seminorm 𝕜 (SchwartzMap E F)
-- Mathlib.Computability.EpsilonNFA
/-- Set of acceptance states.  -/
εNFA.accept : {α : Type u} → {σ : Type v} → εNFA α σ → Set σ
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.im_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasImages C]
  [inst_2 : CategoryTheory.Limits.HasImageMaps C] {X Y : CategoryTheory.Arrow C} (st : X ⟶ Y),
  CategoryTheory.Limits.im.map st = CategoryTheory.Limits.image.map st
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.minKey_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {he : (Std.DTreeMap.Const.modify t k f).isEmpty = false},
  (Std.DTreeMap.Const.modify t k f).minKey he = if cmp (t.minKey ⋯) k = Ordering.eq then k else t.minKey ⋯
-- Init.Data.Vector.InsertIdx
Vector.getElem?_insertIdx_of_lt : ∀ {α : Type u} {n : ℕ} {xs : Vector α n} {x : α} {i k : ℕ} (w : i ≤ n), k < i → (xs.insertIdx i x w)[k]? = xs[k]?
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.exfalsoIfNotProp : Lean.Meta.Grind.Goal → Lean.MetaM Lean.Meta.Grind.Goal
-- Lean.Elab.Command
Lean.Elab.Command.runModuleLinters : Array Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.MeasureTheory.Measure.DiracProba
MeasureTheory.diracProba_toMeasure_apply' : ∀ {X : Type u_1} [inst : MeasurableSpace X] (x : X) {A : Set X},
  MeasurableSet A → ↑(MeasureTheory.diracProba x) A = A.indicator 1 x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_erase_eq_iff_not_compare_eq_maxKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {he : (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKey he = t.maxKey ⋯ ↔ ¬compare k (t.maxKey ⋯) = Ordering.eq
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_fst : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous fun p => p.1
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.ball_infDist_subset_compl : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, Metric.ball x (Metric.infDist x s) ⊆ sᶜ
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- A pullback cone is a limit cone if and only if the corresponding pushout cocone
in the opposite category is a colimit cocone.  -/
CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          (c : CategoryTheory.Limits.PullbackCone f g) →
            CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsColimit c.op
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.mapM_eq_foldlM.aux : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β} {xs : Array α}
  (i : ℕ) (bs : Array β),
  Array.mapM.map✝ f xs i bs = List.foldlM (fun bs a => bs.push <$> f a) bs (List.drop i xs.toList)
-- Lean.Compiler.ImplementedByAttr
Lean.Compiler.getImplementedBy? : Lean.Environment → Lean.Name → Option Lean.Name
-- Lean.DocString.Types
Lean.Doc.instInhabitedListItem : {a : Type u_1} → Inhabited (Lean.Doc.ListItem a)
-- Mathlib.Algebra.Order.Monoid.Units
Units.val_lt_val : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : Preorder α] {a b : αˣ}, ↑a < ↑b ↔ a < b
-- Mathlib.RingTheory.Ideal.CotangentBaseChange
/-- If `T` is a flat `R`-module, the canonical map `tensorCotangentHom R T I` is injective.  -/
Ideal.tensorCotangentHom_injective_of_flat : ∀ (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] (I : Ideal S) [Module.Flat R T],
  Function.Injective ⇑(Ideal.tensorCotangentHom R T I)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_comp_subst_apply : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {υ : Type u_7} {T : Type u_8} [inst_3 : CommRing T]
  [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] {b : τ → MvPowerSeries υ T},
  MvPowerSeries.HasSubst a →
    MvPowerSeries.HasSubst b →
      ∀ (f : MvPowerSeries σ R),
        MvPowerSeries.subst b (MvPowerSeries.subst a f) = MvPowerSeries.subst (fun s => MvPowerSeries.subst b (a s)) f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.divCoeffs : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Lean.Server.Rpc.RequestHandling
_private.Lean.Server.Rpc.RequestHandling.0.Lean.Server.RpcProcedure.mk.injEq : ∀ (wrapper wrapper_1 : UInt64 → Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Json)),
  ({ wrapper := wrapper } = { wrapper := wrapper_1 }) = (wrapper = wrapper_1)
-- Init.Data.String.Lemmas.FindPos
String.posGT_eq_posGE : ∀ {s : String} {p : String.Pos.Raw} {h : p < s.rawEndPos}, s.posGT p h = s.posGE p.inc ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_add_int_mul_two_pi : ∀ (x : ℝ) (n : ℤ), Real.sin (x + ↑n * (2 * Real.pi)) = Real.sin x
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.nontrivial : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (P : Ideal R)
  [hp : P.IsPrime] [IsLocalization.AtPrime S P], Nontrivial S
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Lattice.BicartSq.sup_eq : ∀ {T : Type u} {x₁ x₂ x₃ x₄ : T} [inst : Lattice T], Lattice.BicartSq x₁ x₂ x₃ x₄ → x₂ ⊔ x₃ = x₄
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.congr_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C} {α β : X ⟶ Y}
  (h : α = β) (U : (TopologicalSpace.Opens ↑↑Y)ᵒᵖ),
  α.c.app U = CategoryTheory.CategoryStruct.comp (β.c.app U) (X.presheaf.map (CategoryTheory.eqToHom ⋯))
-- Mathlib.RingTheory.RootsOfUnity.Minpoly
/-- The minimal polynomial of a root of unity `μ` divides `X ^ n - 1`.  -/
IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one : ∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n → ∀ [IsDomain K] [CharZero K], minpoly ℤ μ ∣ Polynomial.X ^ n - 1
-- Mathlib.Order.RelIso.Basic
RelHom.preimage_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : β → β → Prop) (a : α), (RelHom.preimage f s) a = f a
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
UpperHalfPlane.isZeroAtImInfty_iff : ∀ {α : Type u_1} [inst : SeminormedAddGroup α] {f : UpperHalfPlane → α},
  UpperHalfPlane.IsZeroAtImInfty f ↔ ∀ (ε : ℝ), 0 < ε → ∃ A, ∀ (z : UpperHalfPlane), A ≤ z.im → ‖f z‖ ≤ ε
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.continuous : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →A[R] B), Continuous ⇑f
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Subtype.dist_eq : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {p : α → Prop} (x y : Subtype p), dist x y = dist ↑x ↑y
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.coe_rTensorHom : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P], ⇑(LinearMap.rTensorHom M) = LinearMap.rTensor M
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.inclDesc_inv_app : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) (i : I) (X : C i),
  (CategoryTheory.Sigma.inclDesc F i).inv.app X = CategoryTheory.CategoryStruct.id ((F i).obj X)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.asIdeal_injective : ∀ {R : Type u_1} [inst : CommRing R], Function.Injective IsDedekindDomain.HeightOneSpectrum.asIdeal
-- Mathlib.Data.EReal.Operations
EReal.add_lt_add_left_coe : ∀ {x y : EReal}, x < y → ∀ (z : ℝ), ↑z + x < ↑z + y
-- Mathlib.GroupTheory.Perm.List
List.formPerm_pow_apply_head : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α) (l : List α),
  (x :: l).Nodup → ∀ (n : ℕ), ((x :: l).formPerm ^ n) x = (x :: l)[n % (x :: l).length]
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.isZero.eq_2 : ∀ (p : Nat.Internal.Linear.Poly), (p = [] → False) → p.isZero = false
-- Mathlib.Logic.Equiv.Option
Equiv.optionCongr_refl : ∀ {α : Type u_1}, (Equiv.refl α).optionCongr = Equiv.refl (Option α)
-- Init.Data.List.Count
List.count_eq_countP' : ∀ {α : Type u_1} [inst : BEq α] {a : α}, List.count a = List.countP fun x => x == a
-- Aesop.Search.SearchM
Aesop.NormSimpContext.mk : Lean.Meta.Simp.Context → Bool → Bool → Option Lean.Term → Lean.Meta.Simp.SimprocsArray → Aesop.NormSimpContext
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.eval_of : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ) (x : M), (AdicCompletion.eval I M n) ((AdicCompletion.of I M) x) = (I ^ n • ⊤).mkQ x
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- The inclusion of `(F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃))` in
`mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j`
when `r (i₁, i₂, i₃) = j`.  -/
CategoryTheory.GradedObject.ι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] →
                                              (i₁ : I₁) →
                                                (i₂ : I₂) →
                                                  (i₃ : I₃) →
                                                    (j : J) →
                                                      r (i₁, i₂, i₃) = j →
                                                        ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶
                                                          CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
                                                            (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂
                                                              X₃)
                                                            j)
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- Given a linear map into continuous multilinear maps
`B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F`, one cannot always uncurry it as `G` and `E` might
live in a different universe. However, one can always lift it to a continuous multilinear map
on `(G × (Π i, E i)) ^ (1 + n)`, which maps `(v_0, ..., v_n)` to `B (g_0) (u_1, ..., u_n)` where
`g_0` is the `G`-coordinate of `v_0` and `u_i` is the `E_i` coordinate of `v_i`.  -/
ContinuousLinearMap.continuousMultilinearMapOption : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      [Fintype ι] →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → NormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
              {F : Type u_1} →
                {G : Type u_2} →
                  [inst_3 : NormedAddCommGroup F] →
                    [inst_4 : NormedSpace 𝕜 F] →
                      [inst_5 : NormedAddCommGroup G] →
                        [inst_6 : NormedSpace 𝕜 G] →
                          (G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) →
                            ContinuousMultilinearMap 𝕜 (fun x => G × ((i : ι) → E i)) F
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_max?_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t → t.max?.isSome = true
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasWidePushouts_opposite_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Limits.HasWidePushouts Cᵒᵖ ↔ CategoryTheory.Limits.HasWidePullbacks C
-- Init.Data.String.Iterate
String.Internal.ofToSliceWithProof : {s : String} → { p // p ≠ s.toSlice.endPos } → { p // p ≠ s.endPos }
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.ofHom_comp : ∀ {M N P : Type u} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N) (g : N →ₙ* P),
  MagmaCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (MagmaCat.ofHom f) (MagmaCat.ofHom g)
-- Mathlib.Order.ModularLattice
infIooOrderIsoIooSup.congr_simp : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] (a b : α),
  infIooOrderIsoIooSup a b = infIooOrderIsoIooSup a b
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.validateComputedFields : Lean.Elab.ComputedFields.M Unit
-- Lean.Elab.Do.Basic
/-- Backtrackable state for the `TermElabM` monad.
 -/
Lean.Elab.Do.SavedState : Type
-- Mathlib.Tactic.SuppressCompilation
/-- Make sure that notations are compiled, even if `suppress_compilation` is active, by prepending
them with `unsuppress_compilation`.  -/
expandSuppressCompilationNotation : Lean.Macro
-- Mathlib.Algebra.Notation.Defs
dite_add : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Add α] (a : P → α) (b : ¬P → α) (c : α),
  (if h : P then a h else b h) + c = if h : P then a h + c else b h + c
-- Mathlib.Probability.Process.Stopping
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.stronglyAdapted_stoppedProcess`. -/
MeasureTheory.ProgMeasurable.stronglyAdapted_stoppedProcess : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {u : ι → Ω → β}
  {τ : Ω → WithTop ι} [inst_1 : LinearOrder ι] [inst_2 : MeasurableSpace ι] [inst_3 : TopologicalSpace ι]
  [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [inst_7 : TopologicalSpace β]
  {f : MeasureTheory.Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace ι],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStoppingTime f τ → MeasureTheory.StronglyAdapted f (MeasureTheory.stoppedProcess u τ)
-- Batteries.Data.List.Lemmas
List.extractP_eq_find?_eraseP : ∀ {α : Type u_1} {p : α → Bool} (l : List α), List.extractP p l = (List.find? p l, List.eraseP p l)
-- Mathlib.Order.Partition.Finpartition
Finpartition.mk.injEq : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (parts : Finset α) (supIndep : parts.SupIndep id)
  (sup_parts : parts.sup id = a) (bot_notMem : ⊥ ∉ parts) (parts_1 : Finset α) (supIndep_1 : parts_1.SupIndep id)
  (sup_parts_1 : parts_1.sup id = a) (bot_notMem_1 : ⊥ ∉ parts_1),
  ({ parts := parts, supIndep := supIndep, sup_parts := sup_parts, bot_notMem := bot_notMem } =
      { parts := parts_1, supIndep := supIndep_1, sup_parts := sup_parts_1, bot_notMem := bot_notMem_1 }) =
    (parts = parts_1)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.unopMap_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} (φ : S₁ ⟶ S₂), (CategoryTheory.ShortComplex.unopMap φ).τ₃ = φ.τ₁.unop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_modify : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : β k → β k}, (m.modify k f).get? k' = if h : (k == k') = true then cast ⋯ (Option.map f (m.get? k)) else m.get? k'
-- Mathlib.Algebra.Free
Magma.AssocQuotient.map_of : ∀ {α : Type u} [inst : Mul α] {β : Type v} [inst_1 : Mul β] (f : α →ₙ* β) (x : α),
  (Magma.AssocQuotient.map f) (Magma.AssocQuotient.of x) = Magma.AssocQuotient.of (f x)
-- Lean.Declaration
Lean.Declaration.mutualDefnDecl.injEq : ∀ (defns defns_1 : List Lean.DefinitionVal),
  (Lean.Declaration.mutualDefnDecl defns = Lean.Declaration.mutualDefnDecl defns_1) = (defns = defns_1)
-- Mathlib.Data.Set.Operations
/-- **Alias** of `Set.sdiff_eq`. -/
Set.diff_eq : ∀ {α : Type u} (s t : Set α), s \ t = s ∩ tᶜ
-- Aesop.Script.Step
Aesop.Script.mkOnGoal : ℕ → Lean.Syntax.Tactic → Lean.Syntax.Tactic
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.OplaxFunctor.bicategory_leftUnitor_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.leftUnitor η).hom.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtypeNe_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (a_1 : Option { y // y ≠ a }),
  (Equiv.optionSubtypeNe a) a_1 = a_1.casesOn' a Subtype.val
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.skipPrefixWhile_eq_startPos_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String},
  s.skipPrefixWhile pat = s.startPos ↔ s.startsWith pat = false
-- Mathlib.Algebra.Category.CoalgCat.Basic
/-- The category of `R`-coalgebras.  -/
CoalgCat : (R : Type u) → [CommRing R] → Type (max u (v + 1))
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.one_def : ∀ {R A : CommRingCat} [inst : Bialgebra ↑R ↑A],
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (AlgebraicGeometry.algSpec R))
      ((AlgebraicGeometry.algSpec R).map CategoryTheory.MonObj.one)
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
_private.Mathlib.NumberTheory.NumberField.Discriminant.Basic.0.NumberField.rootDiscr.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.rootDiscr K = ↑|NumberField.discr K| ^ (↑(Module.finrank ℚ K))⁻¹
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_of_subset_singleton : ∀ {α : Type u} {a : α} {s : Set α}, s ⊆ {a} → s.Subsingleton
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.eq_of_empty : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β] [IsEmpty α]
  (f g : ZeroAtInftyContinuousMap α β), f = g
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- Either `C.X i`, if there is some `i` with `c.Rel i j`, or `C.X j`.  -/
HomologicalComplex.xPrev : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] → {c : ComplexShape ι} → HomologicalComplex V c → ι → V
-- Mathlib.LinearAlgebra.Projection
Submodule.projectionOnto_projection : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : E), (p.projectionOnto q h) ((p.projection q h) x) = (p.projectionOnto q h) x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (t.insertMany l).getKey? k = t.getKey? k
-- Mathlib.Analysis.Convex.Topology
Convex.nhdsWithin_sdiff_eq_nhdsLT : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜},
  Convex 𝕜 s →
    ∀ {a : 𝕜},
      a ∈ closure s → (s ∩ Set.Iio a).Nonempty → s ∩ Set.Ioi a = ∅ → nhdsWithin a (s \ {a}) = nhdsWithin a (Set.Iio a)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.eq_symm_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₂} {y : M₁}, y = e.symm x ↔ e y = x
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.isHomLift' : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} (self : CategoryTheory.BasedNatTrans F G)
  (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (self.app a)
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Ico_left_eq_Ico_sub_one_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {a b : α}, a ≤ b → ¬IsMin a → insert (a - 1) (Finset.Ico a b) = Finset.Ico (a - 1) b
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instIsDomain : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], IsDomain ℤ_[p]