mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The isomorphism between the fibred product of two schemes `Spec S` and `Spec T`
over a scheme `Spec R` and the `Spec` of the tensor product `S ⊗[R] T`.  -/
AlgebraicGeometry.pullbackSpecIso : (R S T : Type u) →
  [inst : CommRing R] →
    [inst_1 : CommRing S] →
      [inst_2 : CommRing T] →
        [inst_3 : Algebra R S] →
          [inst_4 : Algebra R T] →
            CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
                (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))) ≅
              AlgebraicGeometry.Spec (CommRingCat.of (TensorProduct R S T))
-- Mathlib.MeasureTheory.Measure.Prod
/-- If `Prod.snd ⁻¹' t` is a null measurable set and `μ ≠ 0`, then `t` is a null measurable set.  -/
MeasureTheory.NullMeasurableSet.of_preimage_snd : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [NeZero μ] {t : Set β},
  MeasureTheory.NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν) → MeasureTheory.NullMeasurableSet t ν
-- Mathlib.LinearAlgebra.Finsupp.Span
Submodule.smul_top_eq_range_lsum : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  s • ⊤ = ((Finsupp.lsum R) fun i => ↑i • LinearMap.id).range
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- `of` is the canonical injection from the type to the free group over that type
by sending each element to the equivalence class of the letter that is the element.  -/
FreeAddGroup.of : {α : Type u} → α → FreeAddGroup α
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f f_1 : X ⟶ Y)
  (e_f : f = f_1) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f =
    AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f_1
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_right_unitor_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)),
  (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).hom.toNatTrans.app X)
      ((self.mapId b).hom.toNatTrans.app ((self.map f).toFunctor.obj X))
-- Init.Data.UInt.Lemmas
UInt64.ofNatTruncate_eq_ofNat : ∀ n < UInt64.size, UInt64.ofNatClamp n = UInt64.ofNat n
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- The isomorphism between `Multiplicative ℤ` and the infinite cyclic group `G` sending
`Multiplicative.ofAdd 1` to the generator `g : G`.  -/
intEquivOfZPowersEqTop : {G : Type u_2} → [Infinite G] → [inst : Group G] → (g : G) → Subgroup.zpowers g = ⊤ → Multiplicative ℤ ≃* G
-- Mathlib.GroupTheory.OrderOfElement
finEquivZMultiples_apply : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} (hx : IsOfFinAddOrder x) {n : Fin (addOrderOf x)},
  (finEquivZMultiples hx) n = ⟨↑n • x, ⋯⟩
-- Mathlib.NumberTheory.ModularForms.Basic
CuspFormClass.toSlashInvariantFormClass : ∀ {F : Type u_2} {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} {inst : FunLike F UpperHalfPlane ℂ}
  [self : CuspFormClass F Γ k], SlashInvariantFormClass F Γ k
-- Init.Data.String.Basic
String.append_empty : ∀ {s : String}, s ++ "" = s
-- Lean.Meta.Tactic.Grind.Theorems
/-- Returns theorems associated with the given origin.
 -/
Lean.Meta.Grind.Theorems.find : {α : Type} → Lean.Meta.Grind.Theorems α → Lean.Meta.Grind.Origin → List α
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- **Alias** of `CategoryTheory.Limits.kernelIsoOfEq`.

---

If two morphisms are known to be equal, then their kernels are isomorphic.  -/
CategoryTheory.Limits.kernel.congr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            [inst_3 : CategoryTheory.Limits.HasKernel g] →
              f = g → (CategoryTheory.Limits.kernel f ≅ CategoryTheory.Limits.kernel g)
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_degree : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R},
  f ≠ 0 ↔ ∃ n d, (MvPowerSeries.coeff d) f ≠ 0 ∧ Finsupp.degree d = n
-- Mathlib.Data.Finset.Basic
Finset.sdiff_singleton_eq_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), s \ {a} = s.erase a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : (a : α) → β a → γ a} {k : α} (h : (↑m).WF)
  {h' : (Std.DHashMap.Internal.Raw₀.map f m).contains k = true},
  (Std.DHashMap.Internal.Raw₀.map f m).getKey k h' = m.getKey k ⋯
-- Mathlib.Order.Monotone.Basic
strictAnti_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ StrictAnti f
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_sphere_of_ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ},
  r ≠ 0 → μ (Metric.sphere x r) = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The universal property of categorical pullbacks, stated as an equivalence
of categories between functors `X ⥤ (F ⊡ G)` and categorical commutative squares
over X.  -/
CategoryTheory.Limits.CategoricalPullback.functorEquiv : {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] →
                    CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G) ≌
                      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
CategoryTheory.Limits.inv_piComparison_comp_map_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [inst_2 : CategoryTheory.Limits.HasProduct f]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => G.obj (f j)]
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)] (j : J) {Z : D} (h : G.obj (f j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.piComparison G f))
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.π f j)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => G.obj (f x)) j) h
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.sub_eq_sub_iff : ∀ {α : Type u} [inst : SubtractionCommMonoid α] {a b c d : α},
  IsAddUnit b → IsAddUnit d → (a - b = c - d ↔ a + d = c + b)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A cocone is a colimit cocone exactly if
there is a unique cocone morphism from any other cocone.
 -/
CategoryTheory.Limits.IsColimit.isoUniqueCoconeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit t ≅ (s : CategoryTheory.Limits.Cocone F) → Unique (t ⟶ s)
-- Mathlib.Order.Interval.Set.InitialSeg
Set.principalSegIioIicOfLE_top : ∀ {α : Type u_1} [inst : Preorder α] {i j : α} (h : i ≤ j), (Set.principalSegIioIicOfLE h).top = ⟨i, h⟩
-- Mathlib.Topology.UniformSpace.Path
/-- The function sending a path `γ` to its extension `γ.extend : ℝ → X`
is uniformly continuous in `γ`.  -/
Path.uniformContinuous_extend_left : ∀ {X : Type u_1} [inst : UniformSpace X] {x y : X}, UniformContinuous Path.extend
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.contains.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_3 ()
-- Mathlib.FieldTheory.PrimitiveElement
Field.primitive_element_iff_algHom_eq_of_eval : ∀ (F : Type u_3) {E : Type u_4} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  [Algebra.IsSeparable F E] (A : Type u_5) [inst_5 : Field A] [inst_6 : Algebra F A],
  (∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits) →
    ∀ (α : E) (φ : E →ₐ[F] A), F⟮α⟯ = ⊤ ↔ ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.id_s₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i j : E.I₀}
  (a : E.I₁ i j), (CategoryTheory.CategoryStruct.id E).s₁ a = a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
HasDerivWithinAt.arctan : ∀ {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ},
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => Real.arctan (f x)) (1 / (1 + f x ^ 2) * f') s x
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
restrict₂_comp_IicProdIoc : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] (a b : ι), Finset.restrict₂ ⋯ ∘ IicProdIoc a b = Prod.snd
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C]
  (K : HomologicalComplex C c), (HomologicalComplex.cyclesFunctor C c i).obj K = K.cycles i
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- This is a slightly more convenient method to verify that a fork is a limit cone. It
only asks for a proof of facts that carry any mathematical content  -/
CategoryTheory.Limits.Fork.IsLimit.mk : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        (t : CategoryTheory.Limits.Fork f g) →
          (lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt) →
            (∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι) →
              (∀ (s : CategoryTheory.Limits.Fork f g) (m : s.pt ⟶ t.pt),
                  CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = lift s) →
                CategoryTheory.Limits.IsLimit t
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_of_left_mem : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x : P} (y : P), x ∈ s → s.WOppSide x y
-- Mathlib.Analysis.Meromorphic.Basic
/-- `Meromorphic` is invariant under translation.  -/
Meromorphic.meromorphic_fun_comp_add_const_iff_meromorphic : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜}, (Meromorphic fun z => f (z + c)) ↔ Meromorphic f
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The space of affine maps between two modules is linearly equivalent to the product of the
domain with the space of linear maps, by taking the value of the affine map at `(0 : V1)` and the
linear part.

See note [bundled maps over different rings]  -/
AffineMap.toConstProdLinearMap : (R : Type u_1) →
  {k : Type u_2} →
    {V1 : Type u_3} →
      {V2 : Type u_5} →
        [inst : Ring k] →
          [inst_1 : AddCommGroup V1] →
            [inst_2 : AddCommGroup V2] →
              [inst_3 : Module k V1] →
                [inst_4 : Module k V2] →
                  [inst_5 : Semiring R] →
                    [inst_6 : Module R V2] → [inst_7 : SMulCommClass k R V2] → (V1 →ᵃ[k] V2) ≃ₗ[R] V2 × (V1 →ₗ[k] V2)
-- Init.Data.Option.Lemmas
Option.none_lt : ∀ {α : Type u_1} [inst : LT α] {a : Option α}, none < a ↔ a.isSome = true
-- Mathlib.RingTheory.Algebraic.Basic
Transcendental.pow : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : A},
  Transcendental R r → ∀ {n : ℕ}, 0 < n → Transcendental R (r ^ n)
-- Batteries.Control.Nondet.Basic
/-- Convert a non-deterministic value into a lazy list, by discarding the backtrackable state.
 -/
Nondet.toMLList' : {σ : Type} → {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → Nondet m α → MLList m α
-- Mathlib.Data.List.Permutation
List.nodup_permutations'Aux_iff : ∀ {α : Type u_1} {s : List α} {x : α}, (List.permutations'Aux x s).Nodup ↔ x ∉ s
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.denote_projected_entry : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {entry : Std.Sat.AIG.Entrypoint α},
  ⟦assign, { aig := entry.aig, ref := entry.ref }⟧ = ⟦assign, entry⟧
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.instIsIsoπMap : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [inst_3 : CategoryTheory.Category.{v₁, u₁} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v',
        max (max (u + 1) u₁) v₁}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) [CategoryTheory.IsIso G.π],
  CategoryTheory.IsIso (G.map F η).π
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Change of variables, most common version. If `f` has continuous derivative `f'` on `[a, b]`,
and `g` is continuous, then we can substitute `u = f x` to get
`∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`.
 -/
intervalIntegral.integral_comp_mul_deriv : ∀ {a b : ℝ} {f f' g : ℝ → ℝ},
  (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
    ContinuousOn f' (Set.uIcc a b) → Continuous g → ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (x : ℝ) in f a..f b, g x
-- Mathlib.Order.Circular
sbtw_irrefl_left_right : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b : α}, ¬sbtw a b a
-- Init.Data.List.Perm
List.perm_append_comm : ∀ {α : Type u_1} {l₁ l₂ : List α}, (l₁ ++ l₂).Perm (l₂ ++ l₁)
-- Mathlib.Topology.ClusterPt
mapClusterPt_iff_frequently : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X},
  MapClusterPt x F u ↔ ∀ s ∈ nhds x, ∃ᶠ (a : α) in F, u a ∈ s
-- Mathlib.Order.CompleteLattice.SetLike
Sublattice.setLike_mem_sup : ∀ {X : Type u_1} {L : Sublattice (Set X)} {S T : ↥L} {x : X}, x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- This homology map data expresses compatibilities of the homology data
constructed by `HomologyData.ofEpiOfIsIsoOfMono`  -/
CategoryTheory.ShortComplex.HomologyMapData.ofEpiOfIsIsoOfMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h : S₁.HomologyData) →
            [inst_2 : CategoryTheory.Epi φ.τ₁] →
              [inst_3 : CategoryTheory.IsIso φ.τ₂] →
                [inst_4 : CategoryTheory.Mono φ.τ₃] →
                  CategoryTheory.ShortComplex.HomologyMapData φ h
                    (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono φ h)
-- Mathlib.Algebra.Star.Unitary
/-- In a star monoid, the product `a * b⁻¹` of units is unitary if `star a * a = star b * b`.  -/
Units.mul_inv_mem_unitary : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (a b : Rˣ), ↑a * ↑b⁻¹ ∈ unitary R ↔ star a * a = star b * b
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Run an `OmegaM` computation, restoring the state afterwards.
 -/
Lean.Elab.Tactic.Omega.withoutModifyingState : {α : Type} → Lean.Elab.Tactic.Omega.OmegaM α → Lean.Elab.Tactic.Omega.OmegaM α
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
DirectedOn.le_ciSup_set : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderSup α] {f : β → α} {s : Set β},
  DirectedOn (fun x1 x2 => x1 ≤ x2) (f '' s) → BddAbove (f '' s) → ∀ {c : β}, c ∈ s → f c ≤ ⨆ i, f ↑i
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.tensorObj₄_ext : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C}
  [inst_3 : X₃.HasTensor X₄] [inst_4 : X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_5 :
    X₁.HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))]
  {j : I} {A : C}
  (f g :
    CategoryTheory.GradedObject.Monoidal.tensorObj X₁
        (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)) j ⟶
      A)
  [X₂.HasGoodTensorTensor₂₃ X₃ X₄] [H : X₁.HasTensor₄ObjExt X₂ X₃ X₄],
  (∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h)
          f =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.GradedObject.Monoidal.ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h) g) →
    f = g
-- Mathlib.Order.Interval.Finset.Floor
Int.cast_mem_Ioo_iff : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a b : α} {n : ℤ},
  ↑n ∈ Set.Ioo a b ↔ n ∈ Finset.Ioo ⌊a⌋ ⌈b⌉
-- Mathlib.NumberTheory.Height.NumberField
/-- **Alias** of `NumberField.finite_setOfPred_logHeight₁_le`.

---

A number field `K` satisfies the **Northcott property**:
The set of elements of bounded logarithmic height is finite.  -/
NumberField.finite_setOf_logHeight₁_le : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (B : ℝ), {x | Height.logHeight₁ x ≤ B}.Finite
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.core_map_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : CategoryTheory.Core C} (f : X ⟶ Y), (F.core.map f).iso.hom = F.map f.iso.hom
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_apply_app : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] {F₁ F₂ : CategoryTheory.Functor J C}
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] (a : F₁ ⟶ F₂) (X : J),
  ((CategoryTheory.Enriched.FunctorCategory.functorHomEquiv V) a).app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Enriched.FunctorCategory.homEquiv V) a)
      (CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom V F₁ F₂ (CategoryTheory.Under.forget X))
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- A term of `FormalMultilinearSeries.changeOriginSeries`.

Given a formal multilinear series `p` and a point `x` in its ball of convergence,
`p.changeOrigin x` is a formal multilinear series such that
`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense. Each term of `p.changeOrigin x`
is itself an analytic function of `x` given by the series `p.changeOriginSeries`. Each term in
`changeOriginSeries` is the sum of `changeOriginSeriesTerm`'s over all `s` of cardinality `l`.
The definition is such that `p.changeOriginSeriesTerm k l s hs (fun _ ↦ x) (fun _ ↦ y) =
p (k + l) (s.piecewise (fun _ ↦ x) (fun _ ↦ y))`
 -/
FormalMultilinearSeries.changeOriginSeriesTerm : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                FormalMultilinearSeries 𝕜 E F →
                  (k l : ℕ) → (s : Finset (Fin (k + l))) → s.card = l → E [×l]→L[𝕜] E [×k]→L[𝕜] F
-- Mathlib.CategoryTheory.Subfunctor.Sieves
/-- Given a subpresheaf `G` of `F`, an `F`-section `s` on `U`, we may define a sieve of `U`
consisting of all `f : V ⟶ U` such that the restriction of `s` along `f` is in `G`.  -/
CategoryTheory.Subfunctor.sieveOfSection : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      CategoryTheory.Subfunctor F → {U : Cᵒᵖ} → F.obj U → CategoryTheory.Sieve (Opposite.unop U)
-- Mathlib.Data.Set.Function
Equiv.image_eq_iff_bijOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : α ≃ β), ⇑e '' s = t ↔ Set.BijOn (⇑e) s t
-- Mathlib.Data.Set.Lattice
Set.biUnion_const : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Nonempty → ∀ (t : Set β), ⋃ a ∈ s, t = t
-- Mathlib.Order.RelClasses
instIsStrictTotalOrderLt : ∀ {α : Type u} [inst : LinearOrder α], IsStrictTotalOrder α fun x1 x2 => x1 < x2
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_eq_singleton_append : ∀ {m n : ℤ}, m < n → (m<...=n).toArray = #[m + 1] ++ ((m + 1)<...=n).toArray
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_self_pos : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] {s : Finset α}, s.Nonempty → 0 < s.addEnergy s
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.lift_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type w} {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) (b : β) {Z : C} (h : f b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) h) =
    CategoryTheory.CategoryStruct.comp (p b) h
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
/-- All objects that are binary coproducts of objects in `P`.  -/
CategoryTheory.ObjectProperty.binaryCoproductsClosure : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C
-- Init.Data.UInt.Lemmas
USize.mul_add : ∀ {a b c : USize}, a * (b + c) = a * b + a * c
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem_toList_rio : ∀ {n i : ℕ} (_h : i < (*...n).toList.length), (*...n).toList[i] = i
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.isBasis_basicOpen : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X], TopologicalSpace.Opens.IsBasis (Set.range X.basicOpen)
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.inv_mem_iff : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x : G}, x⁻¹ ∈ H ↔ x ∈ H