mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Endowing the space `WithLp p (α × β)` with the `L^p` pseudometric structure. This definition is
not satisfactory, as it does not register the fact that the topology, the uniform structure, and the
bornology coincide with the product ones. Therefore, we do not register it as an instance. Using
this as a temporary pseudoemetric space instance, we will show that the uniform structure is equal
(but not defeq) to the product one, and then register an instance in which we replace the uniform
structure and the bornology by the product ones using this pseudometric space,
`PseudoMetricSpace.replaceUniformity`, and `PseudoMetricSpace.replaceBornology`.

See note [reducible non-instances]  -/
WithLp.prodPseudoMetricAux : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) →
      [hp : Fact (1 ≤ p)] → [PseudoMetricSpace α] → [PseudoMetricSpace β] → PseudoMetricSpace (WithLp p (α × β))
-- Mathlib.Tactic.Module
/-- Augment a `Module.NF R M` object `l`, i.e. a list of pairs in `R × M`, by prepending another
pair `p : R × M`.  -/
Mathlib.Tactic.Module.NF.cons : {R : Type u_2} → {M : Type u_3} → R × M → Mathlib.Tactic.Module.NF R M → Mathlib.Tactic.Module.NF R M
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
WfDvdMonoid.wellFoundedLT_associates : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [WfDvdMonoid α], WellFoundedLT (Associates α)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.uniqueDiffOn_preimage : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  (h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n),
  n ≠ 0 → ∀ {s : Set F}, UniqueDiffOn 𝕜 (⇑h ⁻¹' s) ↔ UniqueDiffOn 𝕜 s
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.invOneSubPow_inv_eq_one_sub_pow : ∀ (S : Type u_1) [inst : CommRing S] (d : ℕ), (PowerSeries.invOneSubPow S d).inv = (1 - PowerSeries.X) ^ d
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuous_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β},
  UpperSemicontinuous f ↔ ∀ (x : α), UpperSemicontinuousAt f x
-- Std.Http.Server.Connection
/-- Processes a single async I/O event and updates the connection state.
Returns the updated state and `true` if the connection should be closed immediately.
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.handleRecvEvent : {σ β : Type} →
  [Std.Http.Server.Handler σ] →
    [Std.Http.Body β] →
      σ →
        Std.Http.Config →
          Std.Http.Server.Connection.Recv✝ β →
            Std.Http.Server.Connection.ConnectionState✝ β →
              Std.Async.Async (Std.Http.Server.Connection.ConnectionState✝ β × Bool)
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₁ : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleRotateIso.inv.app X).hom₁ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biUnion_biUnion : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq α] (s : Finset γ) (t : γ → Finset α) (f : α → Set β),
  ⋃ y ∈ s.biUnion t, f y = ⋃ x ∈ s, ⋃ y ∈ t x, f y
-- Mathlib.LinearAlgebra.Isomorphisms
/-- **Noether's third isomorphism theorem** for modules: `(M / S) / (T / S) ≃ M / T`.  -/
Submodule.quotientQuotientEquivQuotient : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (S T : Submodule R M) → S ≤ T → ((M ⧸ S) ⧸ Submodule.map S.mkQ T) ≃ₗ[R] M ⧸ T
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.const_max : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : LinearOrder β] (x y : β), ↑(max x y) = max ↑x ↑y
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_sub_intCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (z : ℤ),
  ⌊a - ↑z⌋ = ⌊a⌋ - z
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.postcompose₃_obj_obj_obj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [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₃] {E : Type u_7}
  [inst_3 : CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [inst_4 : CategoryTheory.Category.{v_8, u_8} E']
  (X : CategoryTheory.Functor E E')
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (X_1 : C₁) {X_2 Y : C₂}
  (f : X_2 ⟶ Y) (X_3 : C₃),
  ((((CategoryTheory.Functor.postcompose₃.obj X).obj F).obj X_1).map f).app X_3 = X.map (((F.obj X_1).map f).app X_3)
-- Aesop.Util.Basic
Aesop.forEachExprInGoalCore : {ω : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] →
      [MonadLiftT (ST ω) m] →
        [Monad m] →
          [MonadControlT Lean.MetaM m] →
            [MonadLiftT Lean.MetaM m] → Lean.MVarId → (Lean.Expr → m Bool) → Lean.MonadCacheT Lean.Expr Unit m Unit
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.mk.sizeOf_spec : ∀ {M : Type u_10} {N : Type u_11} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : SizeOf M] [inst_3 : SizeOf N]
  (toZeroHom : ZeroHom M N) (map_add' : ∀ (x y : M), toZeroHom.toFun (x + y) = toZeroHom.toFun x + toZeroHom.toFun y),
  sizeOf { toZeroHom := toZeroHom, map_add' := map_add' } = 1 + sizeOf toZeroHom
-- Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
MeasureTheory.AEFinStronglyMeasurable.exists_measurableSet_measure_pos_lt_top : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → E}, MeasureTheory.AEFinStronglyMeasurable f μ → ¬f =ᵐ[μ] 0 → ∃ s, MeasurableSet s ∧ 0 < μ s ∧ μ s < ⊤
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.opEquiv_inverse_map_inclLeft_op : ∀ (C : Type u₁) {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {d d' : D} (f : d ⟶ d'),
  (CategoryTheory.Join.opEquiv C D).inverse.map ((CategoryTheory.Join.inclLeft Dᵒᵖ Cᵒᵖ).map f.op) =
    Opposite.op ((CategoryTheory.Join.inclRight C D).map f)
-- Init.Data.Array.MapIdx
Array.mapIdx_eq_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : ℕ → α → β} {b : β},
  Array.mapIdx f xs = #[b] ↔ ∃ a, xs = #[a] ∧ f 0 a = b
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainBotCoeff_zero_right : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) [inst_8 : Nontrivial L],
  α.IsNonZero → LieModule.chainBotCoeff (⇑α) 0 = 1
-- Mathlib.CategoryTheory.Limits.EpiMono
CategoryTheory.epi_iff_isIso_inl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : X ⟶ Y}
  {c : CategoryTheory.Limits.PushoutCocone f f} (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.Epi f ↔ CategoryTheory.IsIso c.inl
-- Mathlib.Topology.Closure
/-- **Alias** of the forward direction of `closure_nonempty_iff`. -/
Set.Nonempty.of_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, (closure s).Nonempty → s.Nonempty
-- Lean.Declaration
Lean.instInhabitedConstantInfo.default : Lean.ConstantInfo
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.cosimplicialSimplicialEquiv_functor_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : (CategoryTheory.Functor SimplexCategory C)ᵒᵖ}
  (α : X ⟶ Y) (X_1 : SimplexCategoryᵒᵖ),
  ((CategoryTheory.cosimplicialSimplicialEquiv C).functor.map α).app X_1 = (α.unop.app (Opposite.unop X_1)).op
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.ordinaryHypergeometric_div_Gamma_eq : ∀ {a b c z : ℂ}, (∀ (k : ℕ), c ≠ -↑k) → ₂F₁ a b c z / Complex.Gamma c = a.regularizedGaussHGFun b c z
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_iso_inv_app : ∀ {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) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X_1 : X),
  ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).functor.obj J).iso.inv.app X_1 = (J.obj X_1).iso.inv
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- See `Scheme.exists_π_app_comp_eq_of_locallyOfFinitePresentation` for the general case.  -/
_private.Mathlib.AlgebraicGeometry.AffineTransitionLimit.0.AlgebraicGeometry.Scheme.exists_π_app_comp_eq_of_locallyOfFinitePresentation_of_isAffine : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (t : D ⟶ (CategoryTheory.Functor.const I).obj S) (f : X ⟶ S)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [AlgebraicGeometry.LocallyOfFinitePresentation f] [AlgebraicGeometry.IsAffine S] [AlgebraicGeometry.IsAffine X]
  [∀ (i : I), AlgebraicGeometry.IsAffine (D.obj i)] (a : c.pt ⟶ X),
  CategoryTheory.CategoryStruct.comp c.π t =
      (CategoryTheory.Functor.const I).map (CategoryTheory.CategoryStruct.comp a f) →
    ∃ i g, CategoryTheory.CategoryStruct.comp (c.π.app i) g = a ∧ CategoryTheory.CategoryStruct.comp g f = t.app i
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.ω₁_mem_lattice : ∀ (L : PeriodPair), L.ω₁ ∈ L.lattice
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.range_toUniformOnFun : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : DecidableEq ι]
  [inst_7 : TopologicalSpace F],
  Set.range ContinuousMultilinearMap.toUniformOnFun =
    {f |
      Continuous ((UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f) ∧
        (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
            (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i (x + y)) =
              (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i x) +
                (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i y)) ∧
          ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
            (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i (c • x)) =
              c • (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i x)}
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly.congr_simp : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ φ_1 : L →ₗ[R] Module.End R M),
  φ = φ_1 →
    ∀ [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
      (b b_1 : Module.Basis ι R L), b = b_1 → φ.polyCharpoly b = φ_1.polyCharpoly b_1
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.isLE_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ),
  X.IsLE n ↔ ∀ (i : ℤ), n < i → CategoryTheory.Limits.IsZero ((DerivedCategory.homologyFunctor C i).obj X)
-- Mathlib.Order.Filter.Pointwise
Filter.sub_le_sub : ∀ {α : Type u_2} [inst : Sub α] {f₁ f₂ g₁ g₂ : Filter α}, f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ - g₁ ≤ f₂ - g₂
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.isOpen_compl_support : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X},
  IsOpen μ.supportᶜ
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
ExteriorAlgebra.basis_eq_coe_basis : ∀ {R : Type u_1} {M : Type u_2} {m : ℕ} {I : Type u_3} [inst : LinearOrder I] [inst_1 : CommRing R]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I m)),
  b.ExteriorAlgebra ↑s = ↑((Module.Basis.exteriorPower m b) s)
-- Mathlib.GroupTheory.Index
/-- An additive subgroup `H` has index two if and only if there exists `a ∉ H` such
that for all `b`, one of `b + a` and `b` belongs to `H`.  -/
AddSubgroup.index_eq_two_iff_exists_notMem_and : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index = 2 ↔ ∃ a ∉ H, ∀ (b : G), b + a ∈ H ∨ b ∈ H
-- Lean.Environment
Lean.ConstantInfo.instantiateValueLevelParams! : Lean.ConstantInfo → List Lean.Level → optParam Bool false → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- A chosen pullback of `h₁₂.pullback` and `h₂₃.pullback` over `X₂`.  -/
CategoryTheory.Limits.ChosenPullback₃.chosenPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {f₃ : X₃ ⟶ S} →
            {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
              {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃} →
                {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} →
                  CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃ → CategoryTheory.Limits.ChosenPullback h₁₂.p₂ h₂₃.p₁
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.comp_hom₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {X Y Z : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : C} (h : Z.obj₂ ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom₂ h =
    CategoryTheory.CategoryStruct.comp f.hom₂ (CategoryTheory.CategoryStruct.comp g.hom₂ h)
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] [inst_3 : MeasurableSpace δ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  {f : α → γ} {g : β → γ} {ρ : MeasureTheory.Measure δ} {h : δ → γ},
  ProbabilityTheory.IdentDistrib f g μ ν →
    ProbabilityTheory.IdentDistrib g h ν ρ → ProbabilityTheory.IdentDistrib f h μ ρ
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.out : ∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it →
    it = { s := String.ofList (l.reverseAux r), i := { byteIdx := String.utf8Len l } }
-- ProofWidgets.Presentation.Expr
ProofWidgets.GetExprPresentationParams.mk : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx → Lean.Name → ProofWidgets.GetExprPresentationParams
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max!_erase_le_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  (t.erase k).isEmpty = false → (cmp (t.erase k).max! t.max!).isLE = true
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_21 : HAdd Std.Time.Minute.Offset Std.Time.Hour.Offset Std.Time.Minute.Offset
-- Init.Data.UInt.Lemmas
USize.le_iff_lt_or_eq : ∀ {a b : USize}, a ≤ b ↔ a < b ∨ a = b
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- `AffineMap.linear` on endomorphisms is a `MonoidHom`.  -/
AffineMap.linearHom : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V1] → [inst_2 : Module k V1] → [inst_3 : AddTorsor V1 P1] → (P1 →ᵃ[k] P1) →* V1 →ₗ[k] V1
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.coe_bot : ∀ {M : Type u_1} [inst : AddZeroClass M], ↑⊥ = {0}
-- Mathlib.Topology.MetricSpace.HausdorffDimension
Isometry.dimH_image : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {f : X → Y},
  Isometry f → ∀ (s : Set X), dimH (f '' s) = dimH s
-- Mathlib.Data.NNRat.Floor
NNRat.intFloor_cast : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorRing K] (x : ℚ≥0),
  ⌊↑x⌋ = ⌊↑x⌋
-- Mathlib.CategoryTheory.ObjectProperty.Extensions
CategoryTheory.ObjectProperty.prop_biprod : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X₁ X₂ : C},
  P X₁ →
    P X₂ →
      ∀ [inst_1 : CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [P.IsClosedUnderExtensions]
        [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂], P (X₁ ⊞ X₂)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) {Z : D} (h : (F.rightDerived 0).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X)
      (CategoryTheory.CategoryStruct.comp (F.toRightDerivedZero.app X) h) =
    h
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
/-- If `p` is prime and `ζ` is a `p`-th primitive root of unity, then `ζ - 1` divides `η₁ - η₂`
for all `p`-th roots of unity `η₁` and `η₂`.  -/
IsPrimitiveRoot.sub_one_dvd_sub : ∀ {p : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [inst_1 : IsDomain A],
  IsPrimitiveRoot ζ p →
    Nat.Prime p →
      ∀ {η₁ : A}, η₁ ∈ Polynomial.nthRootsFinset p 1 → ∀ {η₂ : A}, η₂ ∈ Polynomial.nthRootsFinset p 1 → ζ - 1 ∣ η₁ - η₂
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.outsidePart_zero : DyckWord.outsidePart 0 = 0
-- Init.Data.List.Nat.TakeDrop
/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
length `> i`. Version designed to rewrite from the big list to the small list.  -/
List.getElem_take' : ∀ {α : Type u_1} {xs : List α} {i j : ℕ} (hi : i < xs.length) (hj : i < j), xs[i] = (List.take j xs)[i]
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.unitIso_hom_app_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Idempotents.Karoubi C),
  ((CategoryTheory.Idempotents.KaroubiKaroubi.unitIso C).hom.app X).f = X.p
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasStrictFDerivAt.rpow_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {p : ℝ},
  HasStrictFDerivAt f f' x → f x ≠ 0 ∨ 1 ≤ p → HasStrictFDerivAt (fun x => f x ^ p) ((p * f x ^ (p - 1)) • f') x
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_presheafFiberMapObjIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C)
  (x : Φ.fiber.obj X) {Z : A} (h : Φ.presheafFiber.obj (F.op.comp P) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x)
      (CategoryTheory.CategoryStruct.comp (Φ.presheafFiberMapObjIso F K P).hom h) =
    CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (F.op.comp P)) h
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.rawStx.parenthesizer : Lean.PrettyPrinter.CategoryParenthesizer
-- Mathlib.Data.Set.Insert
Set.singleton_nonempty : ∀ {α : Type u_1} (a : α), {a}.Nonempty
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Left.nsmul_nonneg : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] {a : M}, 0 ≤ a → ∀ (n : ℕ), 0 ≤ n • a
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- **Alias** of `isOpen_setOfPred_linearIndependent`. -/
isOpen_setOf_linearIndependent : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι], IsOpen {f | LinearIndependent 𝕜 f}
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.ofRepr.injEq : ∀ {ι : Type u_1} {G : Type u_2} [inst : Group G] (repr repr_1 : G ≃* FreeGroup ι),
  ({ repr := repr } = { repr := repr_1 }) = (repr = repr_1)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.norm_setToL1S_le : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F) {C : ℝ},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * μ.real s) →
    ∀ (f : ↥(α →₁ₛ[μ] E)), ‖MeasureTheory.L1.SimpleFunc.setToL1S T f‖ ≤ C * ‖f‖
-- Aesop.Search.Queue
Aesop.FIFOQueue : Type
-- Mathlib.FieldTheory.RatFunc.IntermediateField
Polynomial.aevalAevalEquiv.eq_1 : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A],
  Polynomial.aevalAevalEquiv R A =
    {
      toFun := fun xy =>
        (AlgHom.restrictScalars R (Polynomial.aeval xy.1)).comp
          (let this := Polynomial.algebra;
          AlgHom.restrictScalars R (Polynomial.aeval (Polynomial.C xy.2))),
      invFun := fun f => (f (Polynomial.C Polynomial.X), f Polynomial.X), left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.Iterators.Combinators.Monadic.Zip
Option.SomeLtNone.lt.eq_3 : ∀ {β : Type u_1} {α : Type u_2} (r : α → β → Prop) (x_2 : α) (y : β),
  Option.SomeLtNone.lt r (some x_2) (some y) = r x_2 y
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.coindResAdjunction.eq_1 : ∀ (k : Type u) {G : Type v} [inst : CommRing k] [inst_1 : Group G] (S : Subgroup G)
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex],
  Rep.coindResAdjunction k S = (Rep.indResAdjunction k S.subtype).ofNatIsoLeft (Rep.indCoindNatIso k S)
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkspaceEdit.mk.sizeOf_spec : ∀ (changes? : Option (Std.TreeMap Lean.Lsp.DocumentUri Lean.Lsp.TextEditBatch compare))
  (documentChanges? : Option (Array Lean.Lsp.DocumentChange))
  (changeAnnotations? : Option (Std.TreeMap String Lean.Lsp.ChangeAnnotation compare)),
  sizeOf { changes? := changes?, documentChanges? := documentChanges?, changeAnnotations? := changeAnnotations? } =
    1 + sizeOf changes? + sizeOf documentChanges? + sizeOf changeAnnotations?
-- Mathlib.Data.Option.Basic
Option.none_eq_map_iff : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → β}, none = Option.map f x ↔ x = none
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- This structure contains the data of two left fractions for
`W : MorphismProperty C` that have the same "denominator".  -/
CategoryTheory.MorphismProperty.LeftFraction₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.MorphismProperty C → C → C → Type (max u_1 v_1)
-- Mathlib.Algebra.Group.AddChar
AddChar.mulShift_mulShift : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M) (r s : R),
  (ψ.mulShift r).mulShift s = ψ.mulShift (r * s)