mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv : ∀ (n : Type u) (S : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine S],
  (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).inv =
    AlgebraicGeometry.AffineSpace.homOfVector
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom MvPolynomial.C)) S.isoSpec.inv)
      (⇑(CategoryTheory.ConcreteCategory.hom
            (AlgebraicGeometry.Scheme.ΓSpecIso
                (CommRingCat.of (MvPolynomial n ↑(S.presheaf.obj (Opposite.op ⊤))))).inv) ∘
        MvPolynomial.X)
-- Mathlib.Algebra.GroupWithZero.Semiconj
Commute.zpow_zpow₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a b : G₀}, Commute a b → ∀ (m n : ℤ), Commute (a ^ m) (b ^ n)
-- Mathlib.Analysis.Normed.Group.Real
Real.norm_natCast : ∀ (n : ℕ), ‖↑n‖ = ↑n
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_list_eq_sum_pow : ∀ (α : Type u), Cardinal.mk (List α) = Cardinal.sum fun n => Cardinal.mk α ^ n
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
/-- The morphism `snakeInput hS₁ i j hij ⟶ snakeInput hS₂ i j hij` induced by
a morphism `φ : S₁ ⟶ S₂` of short complexes of homological complexes, that
are short exact (`hS₁ : S₁.ShortExact` and `hS₂ : S₁.ShortExact`).  -/
HomologicalComplex.HomologySequence.mapSnakeInput : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        {c : ComplexShape ι} →
          {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} →
            (S₁ ⟶ S₂) →
              (hS₁ : S₁.ShortExact) →
                (hS₂ : S₂.ShortExact) →
                  (i j : ι) →
                    (hij : c.Rel i j) →
                      HomologicalComplex.HomologySequence.snakeInput hS₁ i j hij ⟶
                        HomologicalComplex.HomologySequence.snakeInput hS₂ i j hij
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.generatorsOfIsCokernelFree_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {ι σ : Type u} {M : SheafOfModules R}
  (f : SheafOfModules.free ι ⟶ SheafOfModules.free σ) (g : SheafOfModules.free σ ⟶ M)
  (H : CategoryTheory.CategoryStruct.comp f g = 0)
  (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)),
  (SheafOfModules.generatorsOfIsCokernelFree f g H H').π = g
-- Std.Data.HashMap.Lemmas
Std.HashMap.insert_eq_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {p : α × β},
  insert p m = m.insert p.1 p.2
-- Mathlib.AlgebraicGeometry.Stalk
/-- A variant of `Spec.fromSpecStalk_eq` that breaks abstraction boundaries.  -/
AlgebraicGeometry.Spec.fromSpecStalk_eq' : ∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)),
  (AlgebraicGeometry.Spec R).fromSpecStalk x =
    AlgebraicGeometry.Spec.map (AlgebraicGeometry.StructureSheaf.toStalk (↑R) x)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeMapCone_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₅, u₅} E] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D}
  {H' : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Functor.mapConeMapCone c).hom.hom = CategoryTheory.CategoryStruct.id (H'.obj (H.obj c.pt))
-- Mathlib.Analysis.Normed.Lp.lpSpace
memℓp_gen_iff : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
  0 < p.toReal → ∀ {f : (i : α) → E i}, Memℓp f p ↔ Summable fun i => ‖f i‖ ^ p.toReal
-- Batteries.Util.ProofWanted
/-- Check that `nm` is a `theorem_wanted` or `def_wanted` declaration, and return both
which kind it is and the parameter-binder type to use when referencing it. The binder type is
Π-quantified over `nm`'s user binders, so parametrised wanted declarations can be referenced as
`❰foo❱ x y` (which desugars to applying the generated parameter to `x y`).

`nm`'s own auto-generated binders (chained `❰…❱` dependencies and ambient `instance_wanted`
includes — the trailing ones, counted by `wantedArityExt`) are handled specially. Instance-valued
ones stay quantified inside the reference's binder, so instance synth still discharges them at the
use site.
Non-class ones (a `def_wanted`/`theorem_wanted` `nm` referenced in its own body) would become
*unsolvable* implicits if quantified — nothing constrains them, since the `.Val`/`.Stmt` accessor
discards its argument — so instead they are returned as `deps`: the caller adds a matching binder
to the enclosing declaration and threads it into `nm`'s application.

We build the binder type by combining explicit syntactic construction for the Π body (so that
`@foo` is applied to each binder's argument) with `PrettyPrinter.delab` for each binder's TYPE
(under options that force a round-trip-safe form). The arguments use fresh names rather than
those from `forallTelescope` to avoid hygiene collisions with the outer signature, and `@` is
prepended to each argument to suppress Lean's implicit-lambda / auto-application machinery —
otherwise functional arguments (e.g. a chained `d_Jacobian` binder) get η-expanded during
elaboration, leaving lambdas in the stored env type that don't round-trip back through delab.  -/
_private.Batteries.Util.ProofWanted.0.classifyWantedRef : Lean.Name → Lean.Syntax → Lean.Elab.Command.CommandElabM WantedRefInfo✝
-- Mathlib.Algebra.Order.AddTorsor
instIsOrderedCancelSMulOfIsOrderedCancelMonoid : ∀ {G : Type u_1} [inst : CommMonoid G] [inst_1 : Preorder G] [IsOrderedCancelMonoid G], IsOrderedCancelSMul G G
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_limit : ∀ {o : Ordinal.{u_1}}, Order.IsSuccPrelimit o → Cardinal.preBeth o = ⨆ a, Cardinal.preBeth ↑a
-- Init.PropLemmas
dite_iff_left_iff : ∀ {p : Prop} [inst : Decidable p] {x : Prop} {y : ¬p → Prop}, ((if h : p then x else y h) ↔ x) ↔ ∀ (h : ¬p), y h ↔ x
-- Mathlib.Computability.Ackermann
ack_succ_zero : ∀ (m : ℕ), ack (m + 1) 0 = ack m 1
-- Mathlib.Tactic.GRewrite.Core
/-- The information about the given rewrite lemma.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.GRewriteLemma : Type
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- If an additive group satisfies the universal property of an additive free group with respect to
a given type, then it is free. Here the universal property is expressed as in
`IsFreeAddGroup.unique_lift`.  -/
IsFreeAddGroup.ofUniqueLift : ∀ {G : Type u} [inst : AddGroup G] (X : Type u) (of : X → G),
  (∀ {H : Type u} [inst_1 : AddGroup H] (f : X → H), ∃! F, ∀ (a : X), F (of a) = f a) → IsFreeAddGroup G
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- When `f` is an epimorphism, the cokernel of `f ≫ g` is isomorphic to the cokernel of `g`.
 -/
CategoryTheory.Limits.cokernelEpiComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y Z : C} →
        (f : X ⟶ Y) →
          (g : Y ⟶ Z) →
            [inst_2 : CategoryTheory.Epi f] →
              [inst_3 : CategoryTheory.Limits.HasCokernel g] →
                CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp f g) ≅
                  CategoryTheory.Limits.cokernel g
-- Lean.Message
Lean.BaseMessage.mk.injEq : ∀ {α : Type u} (fileName : String) (pos : Lean.Position) (endPos : Option Lean.Position) (keepFullRange : Bool)
  (severity : Lean.MessageSeverity) (isSilent : Bool) (caption : String) (data : α) (fileName_1 : String)
  (pos_1 : Lean.Position) (endPos_1 : Option Lean.Position) (keepFullRange_1 : Bool) (severity_1 : Lean.MessageSeverity)
  (isSilent_1 : Bool) (caption_1 : String) (data_1 : α),
  ({ fileName := fileName, pos := pos, endPos := endPos, keepFullRange := keepFullRange, severity := severity,
        isSilent := isSilent, caption := caption, data := data } =
      { fileName := fileName_1, pos := pos_1, endPos := endPos_1, keepFullRange := keepFullRange_1,
        severity := severity_1, isSilent := isSilent_1, caption := caption_1, data := data_1 }) =
    (fileName = fileName_1 ∧
      pos = pos_1 ∧
        endPos = endPos_1 ∧
          keepFullRange = keepFullRange_1 ∧
            severity = severity_1 ∧ isSilent = isSilent_1 ∧ caption = caption_1 ∧ data = data_1)
-- Init.Data.SInt.Basic
Int16.instOfNat : {n : ℕ} → OfNat Int16 n
-- Mathlib.Order.Category.Lat
_private.Mathlib.Order.Category.Lat.0.Lat.Hom.mk.inj : ∀ {X Y : Lat} {hom' hom'_1 : LatticeHom ↑X ↑Y}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Analysis.InnerProductSpace.PiL2
Complex.isometryOfOrthonormal.eq_1 : ∀ {F : Type u_5} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (v : OrthonormalBasis (Fin 2) ℝ F),
  Complex.isometryOfOrthonormal v = Complex.orthonormalBasisOneI.repr.trans v.repr.symm
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.prodComonad_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (Y : C), (CategoryTheory.prodComonad X).obj Y = (X ⨯ Y)
-- Mathlib.Data.Finsupp.Single
Finsupp.uniqueEquiv.congr_simp : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a a_1 : α),
  a = a_1 → ∀ [inst_1 : Subsingleton α], Finsupp.uniqueEquiv a = Finsupp.uniqueEquiv a_1
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- Given `E` and `F` two topological vector spaces and `𝔖 : Set (Set E)`, then
`UniformConvergenceCLM σ F 𝔖` (denoted `E →SLᵤ[σ, 𝔖] F`) is a type synonym of `E →SL[σ] F` equipped
with the "topology of uniform convergence on the elements of `𝔖`".

If the continuous linear image of any element of `𝔖` is bounded, this makes `E →SL[σ] F` a
topological vector space.  -/
UniformConvergenceCLM.«term_→SLᵤ[_,_]_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.mk' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  Function.Injective f → (∀ (x : X), Filter.comap f (nhds (f x)) = nhds x) → Topology.IsEmbedding f
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instCategoryWithWeakEquivalencesHoCat : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      HomotopicalAlgebra.CategoryWithWeakEquivalences (HomotopicalAlgebra.FibrantObject.HoCat C)
-- Init.Data.Float.Model.Float32
/-- Converts an `Int64` to a `Float32.Model`, returning positive zero on zero.  -/
Float32.Model.ofInt64 : Int64 → Float32.Model
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_union : ∀ {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] {s t : Set P},
  asymptoticCone k (s ∪ t) = asymptoticCone k s ∪ asymptoticCone k t
-- Mathlib.Algebra.Order.Group.Abs
apply_abs_le_mul_of_one_le : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2}
  [inst_3 : MulOneClass H] [inst_4 : LE H] [MulLeftMono H] [MulRightMono H] {f : G → H},
  (∀ (x : G), 1 ≤ f x) → ∀ (a : G), f |a| ≤ f a * f (-a)
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.Slice.Pos.find?_eq_find?_sliceFrom : ∀ {ρ : Type} {pat : ρ} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id] [inst_2 : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice} {p : s.Pos}, p.find? pat = Option.map String.Slice.Pos.ofSliceFrom ((s.sliceFrom p).find? pat)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instIsTorsionFree' : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [IsDomain A]
  (S : Subalgebra R A), Module.IsTorsionFree (↥S) A
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {h' : a ∈ t.erase k}, (t.erase k).getKey a h' = t.getKey a ⋯
-- Std.Http.Internal.ChunkedBuffer
Std.Http.Internal.ChunkedBuffer.mk : Array ByteArray → ℕ → Std.Http.Internal.ChunkedBuffer
-- Mathlib.RingTheory.TensorProduct.Basic
TensorProduct.Algebra.mul'_comp_tensorTensorTensorComm : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : SMulCommClass R A A]
  [inst_6 : SMulCommClass R B B] [inst_7 : IsScalarTower R A A] [inst_8 : IsScalarTower R B B],
  LinearMap.mul' R (TensorProduct R A B) ∘ₗ ↑(TensorProduct.tensorTensorTensorComm R A A B B) =
    TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R B)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.pushouts_ofLE_le_largerSubobject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  (hG : CategoryTheory.IsSeparator G) {X : C} (A : CategoryTheory.Subobject X),
  (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms G).pushouts
    (A.ofLE (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG A) ⋯)
-- Lean.Data.PersistentArray
Lean.PersistentArray.mkEmptyArray : {α : Type u} → Array α
-- Lean.Meta.Tactic.Grind.Theorems
/-- Retrieves theorems from `s` associated with the given symbol. See `Theorems.insert`.
The theorems are removed from `s`.
 -/
Lean.Meta.Grind.Theorems.retrieve? : {α : Type} → Lean.Meta.Grind.Theorems α → Lean.Name → Option (List α × Lean.Meta.Grind.Theorems α)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- The empty list lifts the element `0` of `⨂[R] i, s i`.
 -/
PiTensorProduct.lifts_zero : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)], 0 ∈ PiTensorProduct.lifts 0
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.measurableSet_fiber : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (x : β),
  MeasurableSet (⇑f ⁻¹' {x})
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.val_step_filterMap.match_1.eq_2 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (out' : γ) (h_1 : Unit → motive none)
  (h_2 : (out' : γ) → motive (some out')),
  (match some out' with
    | none => h_1 ()
    | some out' => h_2 out') =
    h_2 out'
-- Batteries.Data.Float.Lemmas
Float32.toBits.eq_1 : ∀ (a : Float32), a.toBits = a.toModel.toBits
-- Init.Data.Fin.Lemmas
Fin.pred_add_one : ∀ {n : ℕ} (i : Fin (n + 2)) (h : ↑i < n + 1), (i + 1).pred ⋯ = i.castLT h
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.diagSub.match_1.eq_1 : ∀ (motive : (n : ℕ) → (α : TypeVec.{u_1} n) → (x : Fin2 n) → α x → Sort u_2) (n : ℕ) (α : TypeVec.{u_1} (n + 1))
  (a : Fin2 n) (x : α a.fs)
  (h_1 : (n : ℕ) → (α : TypeVec.{u_1} (n + 1)) → (a : Fin2 n) → (x : α a.fs) → motive (n + 1) α a.fs x)
  (h_2 : (n : ℕ) → (α : TypeVec.{u_1} (n + 1)) → (x : α Fin2.fz) → motive (n + 1) α Fin2.fz x),
  (match n + 1, α, a.fs, x with
    | .(n + 1), α, a.fs, x => h_1 n α a x
    | .(n + 1), α, Fin2.fz, x => h_2 n α x) =
    h_1 n α a x
-- Init.Omega.Constraint
/-- A lower bound at `x` is satisfied at `t` if `x ≤ t`.  -/
Lean.Omega.LowerBound.sat : Lean.Omega.LowerBound → ℤ → Bool
-- Mathlib.Algebra.Group.Finsupp
Finsupp.single_add_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (a : ι) (m₁ m₂ : M) (b : ι),
  (fun₀ | a => m₁ + m₂) b = (fun₀ | a => m₁) b + (fun₀ | a => m₂) b
-- Mathlib.Data.Nat.Choose.Basic
Nat.ascFactorial_eq_factorial_mul_choose' : ∀ (n k : ℕ), n.ascFactorial k = k.factorial * (n + k - 1).choose k
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_interior : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : Set α), ↑(TopologicalSpace.Opens.interior s) = interior s
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ_δ₀Iter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (j : Fin (m + 1)) (hi : autoParam (n + (i + 1) = m + 1) CategoryTheory.SimplicialObject.σ_δ₀Iter._auto_1),
  autoParam (↑j ≤ i) CategoryTheory.SimplicialObject.σ_δ₀Iter._auto_3 →
    CategoryTheory.CategoryStruct.comp (X.σ j) (X.δ₀Iter (i + 1) hi) = X.δ₀Iter i ⋯
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous
MeasureTheory.Lp.instContinuousSMulDomMulAct : ∀ {X : Type u_1} {M : Type u_2} {E : Type u_3} [inst : TopologicalSpace X] [R1Space X] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : TopologicalSpace M] [inst_5 : MeasurableSpace M] [inst_6 : OpensMeasurableSpace M]
  [inst_7 : SMul M X] [inst_8 : ContinuousSMul M X] [inst_9 : NormedAddCommGroup E] {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.InnerRegularCompactLTTop]
  [inst_12 : MeasureTheory.SMulInvariantMeasure M X μ] {p : ENNReal} [inst_13 : Fact (1 ≤ p)] [hp : Fact (p ≠ ⊤)],
  ContinuousSMul Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)
-- Mathlib.CategoryTheory.Extensive
/-- If `C` has pullbacks and is finitary (pre-)extensive, pullbacks distribute over finite
coproducts, i.e., `∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ)`.
For an `IsPullback` version, see `FinitaryPreExtensive.isPullback_sigmaDesc`.  -/
CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  [inst_2 : CategoryTheory.FinitaryPreExtensive C] {ι : Type u_1} {ι' : Type u_2} [inst_3 : Finite ι]
  [inst_4 : Finite ι'] {S : C} {X : ι → C} {Y : ι' → C} (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S),
  CategoryTheory.IsIso
    (CategoryTheory.Limits.Sigma.desc fun p =>
      CategoryTheory.Limits.pullback.map (f p.1) (g p.2) (CategoryTheory.Limits.Sigma.desc f)
        (CategoryTheory.Limits.Sigma.desc g) (CategoryTheory.Limits.Sigma.ι X p.1) (CategoryTheory.Limits.Sigma.ι Y p.2)
        (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
-- Std.Data.HashMap.Lemmas
Std.HashMap.equiv_emptyWithCapacity_iff_isEmpty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {c : ℕ}, m.Equiv (Std.HashMap.emptyWithCapacity c) ↔ m.isEmpty = true
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inl_isoPushout_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp inl h.isoPushout.hom = CategoryTheory.Limits.pushout.inl f g
-- Lean.Parser.Command
Lean.Parser.Command.partial.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Rat.Cast.CharZero
NNRat.cast_divNat : ∀ {α : Type u_3} [inst : DivisionSemiring α] [CharZero α] (a b : ℕ), ↑(NNRat.divNat a b) = ↑a / ↑b
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `FunLike.coe_add`. -/
GroupNorm.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.MeasureTheory.Measure.Lebesgue.Integral
integral_comp_abs : ∀ {f : ℝ → ℝ}, ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Set.Ioi 0, f x
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A set is homeomorphic to its image under any embedding.  -/
Topology.IsEmbedding.homeomorphImage : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f : X → Y} → Topology.IsEmbedding f → (s : Set X) → ↑s ≃ₜ ↑(f '' s)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.normAtAllPlaces '' NumberField.mixedEmbedding.fundamentalCone.normLeOne K =
    ⇑NumberField.mixedEmbedding.mixedSpaceOfRealSpace ⁻¹'
            NumberField.mixedEmbedding.logMap ⁻¹'
              ZSpan.fundamentalDomain
                (Module.Basis.ofZLatticeBasis ℝ (NumberField.Units.unitLattice K)
                  (NumberField.Units.basisUnitLattice K)) ∩
          {x | ∀ (w : NumberField.InfinitePlace K), 0 ≤ x w} ∩
        {x | NumberField.mixedEmbedding.norm (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) ≠ 0} ∩
      {x | NumberField.mixedEmbedding.norm (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) ≤ 1}
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub.eq_1 : ∀ {α : Type u_2} [inst : Sub α], Set.sub = { sub := Set.image2 fun x1 x2 => x1 - x2 }
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.sk.full : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (n : ℕ)
  [inst_1 :
    ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F]
  [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F],
  (CategoryTheory.SimplicialObject.Truncated.sk n).Full
-- Init.Data.SInt.Lemmas
Int32.toInt_maxValue_add_one : Int32.maxValue.toInt + 1 = 2 ^ 31
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- Mapping with respect to a semilinear map over an isomorphism of fields yields
an injective map on projective spaces.  -/
Projectivization.map_injective : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {L : Type u_3}
  {W : Type u_4} [inst_3 : DivisionRing L] [inst_4 : AddCommGroup W] [inst_5 : Module L W] {σ : K →+* L} {τ : L →+* K}
  [RingHomInvPair σ τ] (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f), Function.Injective (Projectivization.map f hf)
-- Lean.Elab.DocString
Lean.Doc.DocArg.str.injEq : ∀ (val val_1 : Lean.StrLit), (Lean.Doc.DocArg.str val = Lean.Doc.DocArg.str val_1) = (val = val_1)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.toList_rcoIter : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β}
  {t_ord : t.Ordered} {lowerBound upperBound : α},
  (Std.DTreeMap.Internal.rcoIterator t lowerBound upperBound).toList =
    List.filter (fun e => decide ((compare e.fst lowerBound).isGE = true ∧ (compare e.fst upperBound).isLT = true))
      t.toList
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.tan_sub : ∀ {x y : ℂ},
  (((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑Real.pi / 2) ∨
      (∃ k, x = (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑Real.pi / 2) →
    Complex.tan (x - y) = (Complex.tan x - Complex.tan y) / (1 + Complex.tan x * Complex.tan y)
-- Mathlib.CategoryTheory.Category.Bipointed
/-- `BipointedToPointed_snd` is inverse to `PointedToBipointed`.  -/
pointedToBipointedCompBipointedToPointedSnd : pointedToBipointed.comp bipointedToPointedSnd ≅ CategoryTheory.Functor.id Pointed
-- Mathlib.Algebra.MvPolynomial.Monad
/-- `join₂` is the monadic join operation corresponding to `MvPolynomial.bind₂`. Given a polynomial `p`
with variables in `σ` whose coefficients are polynomials in `σ` with coefficients in `R`,
`join₂ p` collapses `p` to a polynomial with variables in `σ` and coefficients in `R`.
This operation is a ring hom.
 -/
MvPolynomial.join₂ : {σ : Type u_1} → {R : Type u_3} → [inst : CommSemiring R] → MvPolynomial σ (MvPolynomial σ R) →+* MvPolynomial σ R
-- Init.Data.Nat.Lcm
Nat.lcm_one_right : ∀ (m : ℕ), m.lcm 1 = m
-- Mathlib.Analysis.RCLike.Basic
RCLike.star_def : ∀ {K : Type u_1} [inst : RCLike K], star = ⇑(starRingEnd K)