mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.toIsometryEquiv_refl : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P],
  (AffineIsometryEquiv.refl 𝕜 P).toIsometryEquiv = IsometryEquiv.refl P
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerived_fac_app : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W] (G : CategoryTheory.Functor D H) (β : F ⟶ L.comp G) (X : C),
  CategoryTheory.CategoryStruct.comp (α.app X) ((RF.rightDerivedDesc α W G β).app (L.obj X)) = β.app X
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.smul_def : ∀ {F : Type u_1} [inst : CommRing F] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  (m : Matrix.SpecialLinearGroup ι F) (v : ι → F), m • v = ↑m • v
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapTrifunctorMapMap_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [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₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃ → J) {X₁ Y₁ : CategoryTheory.GradedObject I₁ C₁}
  (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : CategoryTheory.GradedObject I₂ C₂} (f₂ : X₂ ⟶ Y₂) {X₃ Y₃ : CategoryTheory.GradedObject I₃ C₃}
  (f₃ : X₃ ⟶ Y₃) [inst_4 : ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
  [inst_5 : ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p] (i₁ : I₁)
  (i₂ : I₂) (i₃ : I₃) (j : J) (h : p (i₁, i₂, i₃) = j) {Z : C₄}
  (h_1 : CategoryTheory.GradedObject.mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapTrifunctorMapMap F p f₁ f₂ f₃ j) h_1) =
    CategoryTheory.CategoryStruct.comp (((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃))
      (CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃))
        (CategoryTheory.CategoryStruct.comp (((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h) h_1)))
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- The saturation of a subalgebra `s` with respect to a submonoid `M` is the smallest
subalgebra closed under division by `s`.  -/
Subalgebra.saturation : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] → (s : Subalgebra R S) → (M : Submonoid S) → M ≤ s.toSubmonoid → Subalgebra R S
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.unique_iff : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R} [inst_1 : Fintype I] [inst_2 : Unique I],
  CompleteOrthogonalIdempotents e ↔ e default = 1
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.toLin'_one : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α],
  Matrix.UnitaryGroup.toLin' 1 = LinearMap.id
-- Std.Do.Internal.Ensures.Def
Std.Do.Internal.ErasesTo.mk : ∀ {α : Type u} {m : Type u → Type v} [inst : Bind m] {P : α → Prop} {x : m { b // P b }} {y : m α},
  (∀ {β : Type u} (k : α → m β),
      (do
          let a ← x
          k ↑a) =
        y >>= k) →
    Std.Do.Internal.ErasesTo x y
-- Mathlib.Order.InitialSeg
/-- A `PrincipalSeg` between the `<` relations of two types.  -/
«term_<i_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.lift.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f f_1 : A ⟶ X} (e_f : f = f_1)
  {i i_1 : A ⟶ B} (e_i : i = i_1) {p p_1 : X ⟶ Y} (e_p : p = p_1) {g g_1 : B ⟶ Y} (e_g : g = g_1)
  (sq : CategoryTheory.CommSq f i p g) [hsq : sq.HasLift], sq.lift = ⋯.lift
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.join.congr_simp : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R]
  (f f_1 : Convexity.StdSimplex R (Convexity.StdSimplex R M)), f = f_1 → f.join = f_1.join
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.subset_le_of_restrict_le_restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v w : MeasureTheory.VectorMeasure α M) {i : Set α},
  MeasurableSet i → v.restrict i ≤ w.restrict i → ∀ {j : Set α}, j ⊆ i → v j ≤ w j
-- Init.Data.SInt.Lemmas
Int8.ofNat_mul : ∀ (a b : ℕ), Int8.ofNat (a * b) = Int8.ofNat a * Int8.ofNat b
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
/-- Build a `CuspForm 𝒮ℒ k` from a `ModularForm 𝒮ℒ k` whose q-expansion has vanishing
constant term. The resulting cusp form has the same underlying function.  -/
ModularForm.toCuspForm : {k : ℤ} →
  (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
    (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0 → CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.ext : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  {inst : CategoryTheory.Category.{v₁, u₁} A} {inst_1 : CategoryTheory.Category.{v₂, u₂} B}
  {inst_2 : CategoryTheory.Category.{v₃, u₃} C} {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {inst_3 : CategoryTheory.Category.{v₄, u₄} A'} {inst_4 : CategoryTheory.Category.{v₅, u₅} B'}
  {inst_5 : CategoryTheory.Category.{v₆, u₆} C'} {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {x y : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ'},
  x.left = y.left → x.right = y.right → x.base = y.base → x = y
-- Mathlib.LinearAlgebra.Trace
/-- When `M` is finite free, the trace of a linear map corresponds to the contraction pairing under
the isomorphism `End(M) ≃ M* ⊗ M`.  -/
LinearMap.trace_eq_contract' : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M],
  LinearMap.trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquiv R M M).symm
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.π_descTruncGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [inst_6 : t.IsGE Y n],
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) (t.descTruncGE f n) = f
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instLeftDistribClass : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Mul R] [inst_2 : Add R] [LeftDistribClass R]
  [inst_4 : ContinuousMul R] [inst_5 : ContinuousAdd R], LeftDistribClass (SeparationQuotient R)
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.instAddGroup : (R : Type u) → (X : Type v) → [inst : CommRing R] → AddGroup (FreeLieAlgebra R X)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- Auxiliary definition for `extend.rightHomologyData`.  -/
HomologicalComplex.extend.rightHomologyData.kernelFork : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {i j k : ι} →
                      {i' j' k' : ι'} →
                        (hj' : e.f j = j') →
                          (hi : c.prev j = i) →
                            (hi' : c'.prev j' = i') →
                              c.next j = k →
                                c'.next j' = k' →
                                  (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) →
                                    (hcocone : CategoryTheory.Limits.IsColimit cocone) →
                                      CategoryTheory.Limits.KernelFork
                                          (hcocone.desc (CategoryTheory.Limits.CokernelCofork.ofπ (K.d j k) ⋯)) →
                                        CategoryTheory.Limits.KernelFork
                                          ((HomologicalComplex.extend.rightHomologyData.isColimitCokernelCofork K e hj'
                                                hi hi' cocone hcocone).desc
                                            (CategoryTheory.Limits.CokernelCofork.ofπ ((K.extend e).d j' k') ⋯))
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_eq_some_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.minKey? = some (t.minKeyD fallback)
-- Mathlib.GroupTheory.ArchimedeanDensely
Int.addEquiv_eq_refl_or_neg : ∀ (e : ℤ ≃+ ℤ), e = AddEquiv.refl ℤ ∨ e = AddEquiv.neg ℤ
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExSumNat.add.injEq : ∀ {a b : Q(ℕ)} (a_1 : Mathlib.Tactic.Ring.Common.ExProdNat a) (a_2 : Mathlib.Tactic.Ring.Common.ExSumNat b)
  (a_3 : Mathlib.Tactic.Ring.Common.ExProdNat a) (a_4 : Mathlib.Tactic.Ring.Common.ExSumNat b),
  (Mathlib.Tactic.Ring.Common.ExSumNat.add a_1 a_2 = Mathlib.Tactic.Ring.Common.ExSumNat.add a_3 a_4) =
    (a_1 = a_3 ∧ a_2 = a_4)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {P Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) {Z : C}
  (h : Q.X.X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.p.f n) (CategoryTheory.CategoryStruct.comp (f.f.f n) h) =
    CategoryTheory.CategoryStruct.comp (f.f.f n) h
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_natCast_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (n : ℕ) (a : R),
  ⌈↑n + a⌉ = ↑n + ⌈a⌉
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_sSup : ∀ {α : Type u_1} [inst : LE α] (S : Set (UpperSet α)), ↑(sSup S) = ⋂ s ∈ S, ↑s
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.mk.congr_simp : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N}
  (toLinearEquiv toLinearEquiv_1 : M₁ ≃ₗ[R] M₂) (e_toLinearEquiv : toLinearEquiv = toLinearEquiv_1)
  (map_app' : ∀ (m : M₁), Q₂ ((↑toLinearEquiv).toFun m) = Q₁ m),
  { toLinearEquiv := toLinearEquiv, map_app' := map_app' } = { toLinearEquiv := toLinearEquiv_1, map_app' := ⋯ }
-- Lean.Data.NameMap.Basic
Lean.NameSet.instSingletonName : Singleton Lean.Name Lean.NameSet
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.toMon_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Grp C), A.toMon.X = A.X
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
/-- A `NormalMonoCategory` category with finite products and kernels has all equalizers.  -/
CategoryTheory.NormalMonoCategory.hasEqualizers : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C]
  [CategoryTheory.IsNormalMonoCategory C], CategoryTheory.Limits.HasEqualizers C
-- Mathlib.Data.List.MinMax
List.argmin_cons : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] (f : α → β) (a : α) (l : List α),
  List.argmin f (a :: l) = Option.casesOn (List.argmin f l) (some a) fun c => if f c < f a then some c else some a
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.comp_tensor_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) (g : X ⟶ Y),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g)
      (CategoryTheory.CategoryStruct.id Z) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id Z))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id Z))
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) {n₁ : ℕ}
  (x₃ : CategoryTheory.Abelian.Ext S.X₃ Y n₁),
  (CategoryTheory.Abelian.Ext.mk₀ S.g).comp x₃ ⋯ = 0 →
    ∀ {n₀ : ℕ} (hn₀ : 1 + n₀ = n₁), ∃ x₁, hS.extClass.comp x₁ hn₀ = x₃
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.comp_neg_X_comp_neg_X : ∀ {R : Type u_3} [inst : CommRing R] (p : Polynomial R), (p.comp (-Polynomial.X)).comp (-Polynomial.X) = p
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.type.sizeOf_spec : ∀ (next : Mathlib.Tactic.Conv.Path), sizeOf next.type = 1 + sizeOf next
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- We say that `R` has the invariant basis number property if `(Fin n → R) ≃ₗ[R] (Fin m → R)`
implies `n = m`. This gives rise to a well-defined notion of rank of a finitely generated free
module.  -/
InvariantBasisNumber : (R : Type u) → [Semiring R] → Prop
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.opFunctor_map_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : (CategoryTheory.Square C)ᵒᵖ} (φ : X ⟶ Y),
  (CategoryTheory.Square.opFunctor.map φ).τ₁ = φ.unop.τ₄.op
-- Mathlib.Tactic.Core
/-- Make a PreDefinition taking some metadata from declaration `nm`.
You can provide a new type, value and (optional) docstring, but the remaining information is taken
from `nm`.
Currently only implemented for definitions and theorems. Also see docstring of `toModifiers`
 -/
Lean.toPreDefinition : Lean.Name →
  Lean.Name →
    Lean.Expr →
      Lean.Expr →
        optParam (Option (Lean.TSyntax `Lean.Parser.Command.docComment)) none → Lean.CoreM Lean.Elab.PreDefinition
-- Mathlib.Analysis.SpecialFunctions.Sqrt
HasDerivAt.sqrt : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasDerivAt f f' x → f x ≠ 0 → HasDerivAt (fun y => √(f y)) (f' / (2 * √(f x))) x
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.instHasIdealSupportOfFactIsUnitOfNat : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R} [h : Fact (IsUnit 2)], P.HasIdealSupport
-- Mathlib.Algebra.Order.Kleene
kstar_eq_one : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α}, KStar.kstar a = 1 ↔ a ≤ 1
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.instQuiverComonad : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → Quiver (CategoryTheory.Comonad C)
-- Mathlib.Algebra.Order.Monovary
monovary_inv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : CommGroup β] [inst_4 : PartialOrder β] [IsOrderedMonoid β] {f : ι → α} {g : ι → β},
  Monovary f⁻¹ g⁻¹ ↔ Monovary f g
-- Mathlib.Order.Concept
Order.IsExtent.univ : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, Order.IsExtent r Set.univ
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.normalizedDerivOfComplex_const : ∀ (c : ℂ), (Derivative.normalizedDerivOfComplex fun x => c) = 0
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.instCommutativeHAdd_1 : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α], Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.stdSymm : ∀ {α : Type u_1}, Std.Symm Equiv.Perm.Disjoint
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.sheafification_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D),
  (J.sheafification D).obj P = J.sheafify P
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.Std.Slice.toArray.eq_1 : ∀ {γ : Type u_1} {α β : Type u_2} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  (s : Std.Slice γ), s.toArray = (Std.Slice.Internal.iter s).toArray
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mem_map : ∀ {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N] {f : M →ₗ[R] N} {C : ConvexCone R M} {y : N},
  y ∈ ConvexCone.map f C ↔ ∃ x ∈ C, f x = y
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearMap.codRestrictOfInjective.eq_1 : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M₁ →ₗ[R] M₂) (i : M₃ →ₗ[R] M₂) (hi : Function.Injective ⇑i)
  (hf : ∀ (x : M₁), f x ∈ i.range),
  f.codRestrictOfInjective i hi hf = ↑(LinearEquiv.ofInjective i hi).symm ∘ₗ LinearMap.codRestrict i.range f hf
-- Init.Data.List.Perm
List.instTransPerm : {α : Type u_1} → Trans List.Perm List.Perm List.Perm
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.induce_connected_of_patches : ∀ {V : Type u} {G : SimpleGraph V} {s : Set V},
  ∀ u ∈ s,
    (∀ {v : V},
        v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (SimpleGraph.induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩) →
      (SimpleGraph.induce s G).Connected
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The category of augmented simplicial objects, defined as a comma category.  -/
CategoryTheory.SimplicialObject.Augmented : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- The obvious free presheaf of modules of rank `1`.  -/
PresheafOfModules.unit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (R : CategoryTheory.Functor Cᵒᵖ RingCat) → PresheafOfModules R
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- `lpMeasSubgroup F m p μ` is the subspace of `Lp F p μ` containing functions `f` verifying
`AEStronglyMeasurable[m] f μ`, i.e. functions which are `μ`-a.e. equal to
an `m`-strongly measurable function.  -/
MeasureTheory.lpMeasSubgroup : {α : Type u_1} →
  (F : Type u_2) →
    [inst : NormedAddCommGroup F] →
      MeasurableSpace α →
        [inst_1 : MeasurableSpace α] →
          (p : ENNReal) → (μ : MeasureTheory.Measure α) → AddSubgroup ↥(MeasureTheory.Lp F p μ)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.map.eq_1 : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] (f : β → γ) (it : Std.Iter β),
  Std.Iter.map f it = (Std.IterM.map f it.toIterM).toIter
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
/-- If a zero morphism is a cokernel of `f`, then `f` is an epimorphism.  -/
CategoryTheory.NormalMonoCategory.epi_of_zero_cokernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C]
  [CategoryTheory.IsNormalMonoCategory C] {X Y : C} (f : X ⟶ Y) (Z : C)
  (l : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ 0 ⋯)), CategoryTheory.Epi f
-- Mathlib.Analysis.Calculus.FDeriv.Pow
differentiableOn_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  (n : ℕ) {s : Set 𝔸}, DifferentiableOn 𝕜 (fun x => x ^ n) s
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- Given functions `f`, `g` and a real number `R`, the following convenience structure packs the
information relevant in the canonical decomposition.  The condition "`g` is without zeros or poles"
is formulated by saying that `g` is meromorphic in normal form and `g ≠ 0`.
 -/
Complex.CanonicalDecomp : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (ℂ → E) → (ℂ → E) → ℝ → Prop
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
CategoryTheory.Functor.isIso_of_isRightDerivedFunctor_of_inverts : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {L : CategoryTheory.Functor C D} {W : CategoryTheory.MorphismProperty C} [inst_3 : L.IsLocalization W]
  {F : CategoryTheory.Functor C H} (RF : CategoryTheory.Functor D H) (α : F ⟶ L.comp RF),
  W.IsInvertedBy F → ∀ [RF.IsRightDerivedFunctor α W], CategoryTheory.IsIso α
-- Mathlib.Topology.Algebra.AsymptoticCone
Filter.Tendsto.const_vadd_asymptoticNhds : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] {α : Type u_4} {l : Filter α} {f : α → P}
  {v : V} (u : V),
  Filter.Tendsto f l (AffineSpace.asymptoticNhds k P v) →
    Filter.Tendsto (fun x => u +ᵥ f x) l (AffineSpace.asymptoticNhds k P v)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.transFiberHomeomorph_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] {F' : Type u_5} [inst_3 : TopologicalSpace F'] (e : Bundle.Trivialization F proj)
  (h : F ≃ₜ F') (x : Z), ↑(e.transFiberHomeomorph h) x = ((↑e x).1, h (↑e x).2)
-- Batteries.Data.MLList.Basic
/-- Construct a singleton monadic lazy list from a single value.  -/
MLList.singleton : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → α → MLList m α
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.setLIntegral_eq : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ →
    MeasureTheory.IsFundamentalDomain G t μ →
      ∀ (f : α → ENNReal), (∀ (g : G) (x : α), f (g • x) = f x) → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- An additive subsemigroup is isomorphic to its image under an injective function  -/
AddSubsemigroup.equivMapOfInjective : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Add M] →
      [inst_1 : Add N] →
        (S : AddSubsemigroup M) → (f : M →ₙ+ N) → Function.Injective ⇑f → ↥S ≃+ ↥(AddSubsemigroup.map f S)