mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
PresheafOfModules.pullback_comp_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R) [inst_2 : (PresheafOfModules.pushforward φ).IsRightAdjoint],
  PresheafOfModules.pullbackComp φ (CategoryTheory.CategoryStruct.id R) =
    (PresheafOfModules.pullback φ).isoWhiskerLeft (PresheafOfModules.pullbackId R) ≪≫
      (PresheafOfModules.pullback φ).rightUnitor
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The section of `structureSheaf R` on an open `U` sending each `x ∈ U` to the element
`f/g` in the localization of `R` at `x`.  -/
AlgebraicGeometry.StructureSheaf.const : {R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        M →
          (g : R) →
            (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
              U ≤ PrimeSpectrum.basicOpen g → (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op U)
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.bmod.sizeOf_spec : ∀ (m : ℕ) (r : ℤ) (i : ℕ) {x : Lean.Omega.Coeffs}
  (j : Lean.Elab.Tactic.Omega.Justification (Lean.Omega.Constraint.exact r) x),
  sizeOf (Lean.Elab.Tactic.Omega.Justification.bmod m r i j) = 1 + sizeOf m + sizeOf r + sizeOf i + sizeOf x + sizeOf j
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is polynomial on a set `s`, so are its successive derivatives.  -/
CPolynomialOn.iterated_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜}, CPolynomialOn 𝕜 f s → ∀ (n : ℕ), CPolynomialOn 𝕜 (deriv^[n] f) s
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalPi_δ : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : I → Type u₂}
  [inst_2 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)]
  (F : (i : I) → CategoryTheory.Functor (D i) (C i)) [inst_4 : (i : I) → (F i).Monoidal] (X Y : (i : I) → D i) (i : I),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Functor.pi F) X Y i =
    CategoryTheory.Functor.OplaxMonoidal.δ (F i) (X i) (Y i)
-- Mathlib.CategoryTheory.SingleObj
CategoryTheory.SingleObj.natTrans_app : ∀ {M : Type u} [inst : Monoid M] {C : Type v} [inst_1 : CategoryTheory.Category.{w, v} C]
  {F G : CategoryTheory.Functor (CategoryTheory.SingleObj M) C}
  (u : F.obj (CategoryTheory.SingleObj.star M) ⟶ G.obj (CategoryTheory.SingleObj.star M))
  (h : ∀ (a : M), CategoryTheory.CategoryStruct.comp (F.map a) u = CategoryTheory.CategoryStruct.comp u (G.map a))
  (x : CategoryTheory.SingleObj M), (CategoryTheory.SingleObj.natTrans u h).app x = u
-- Init.Data.Array.Attach
Array.attach_congr : ∀ {α : Type u_1} {xs ys : Array α} (h : xs = ys), xs.attach = Array.map (fun x => ⟨↑x, ⋯⟩) ys.attach
-- Init.Data.UInt.Lemmas
UInt32.ofNat_eq_iff_mod_eq_toNat : ∀ (a : ℕ) (b : UInt32), UInt32.ofNat a = b ↔ a % 2 ^ 32 = b.toNat
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
/-- `extendToSucc`, on objects: it coincides with `F.obj` for `i ≤ j`, and
it sends `Order.succ j` to the given object `X`.  -/
CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        [inst_2 : SuccOrder J] → {j : J} → CategoryTheory.Functor (↑(Set.Iic j)) C → C → ↑(Set.Iic (Order.succ j)) → C
-- Mathlib.Algebra.Homology.BifunctorHomotopy
/-- The homotopy between `mapBifunctorMap f₁ f₂ F c` and `mapBifunctorMap f₁' f₂ F c` that
is induced by a homotopy between `f₁` and `f₁'`.  -/
HomologicalComplex.mapBifunctorMapHomotopy₁ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      {I₁ : Type u_4} →
        {I₂ : Type u_5} →
          {J : Type u_6} →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
                  [inst_3 : CategoryTheory.Preadditive C₁] →
                    [inst_4 : CategoryTheory.Preadditive C₂] →
                      [inst_5 : CategoryTheory.Preadditive D] →
                        {c₁ : ComplexShape I₁} →
                          {c₂ : ComplexShape I₂} →
                            {K₁ L₁ : HomologicalComplex C₁ c₁} →
                              {f₁ f₁' : K₁ ⟶ L₁} →
                                Homotopy f₁ f₁' →
                                  {K₂ L₂ : HomologicalComplex C₂ c₂} →
                                    (f₂ : K₂ ⟶ L₂) →
                                      (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                        [inst_6 : F.Additive] →
                                          [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] →
                                            (c : ComplexShape J) →
                                              [inst_8 : DecidableEq J] →
                                                [inst_9 : TotalComplexShape c₁ c₂ c] →
                                                  [inst_10 : K₁.HasMapBifunctor K₂ F c] →
                                                    [inst_11 : L₁.HasMapBifunctor L₂ F c] →
                                                      Homotopy (HomologicalComplex.mapBifunctorMap f₁ f₂ F c)
                                                        (HomologicalComplex.mapBifunctorMap f₁' f₂ F c)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.map_zero_succ_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left) (j : ℕ) (hj : j + 2 < n + 1 + 1),
  CategoryTheory.ComposableArrows.Precomp.map F f 0 ⟨j + 2, hj⟩ ⋯ =
    CategoryTheory.CategoryStruct.comp f (F.map' 0 (j + 1) ⋯ ⋯)
-- Mathlib.Algebra.Polynomial.Sequence
Polynomial.Sequence.mk.injEq : ∀ {R : Type u_1} [inst : Semiring R] (elems' : ℕ → Polynomial R) (degree_eq' : ∀ (i : ℕ), (elems' i).degree = ↑i)
  (elems'_1 : ℕ → Polynomial R) (degree_eq'_1 : ∀ (i : ℕ), (elems'_1 i).degree = ↑i),
  ({ elems' := elems', degree_eq' := degree_eq' } = { elems' := elems'_1, degree_eq' := degree_eq'_1 }) =
    (elems' = elems'_1)
-- Init.Control.Basic
bool : {β : Type u} → {α : Type v} → [ToBool β] → α → α → β → α
-- Mathlib.Order.Filter.CountableInter
Filter.CountableGenerateSets.below.univ : ∀ {α : Type u_2} {g : Set (Set α)} {motive : (a : Set α) → Filter.CountableGenerateSets g a → Prop},
  Filter.CountableGenerateSets.below ⋯
-- Lean.Parser.Basic
Lean.Parser.instReprRecoveryContext : Repr Lean.Parser.RecoveryContext
-- Mathlib.Topology.Sober
Topology.IsClosedEmbedding.quasiSober : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsClosedEmbedding f → ∀ [QuasiSober β], QuasiSober α
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Construct a modification isomorphism between lax natural transformations
by giving object level isomorphisms, and checking naturality only in the forward direction.
 -/
CategoryTheory.Oplax.LaxTrans.isoMk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            (app : (a : B) → η.app a ≅ θ.app a) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))
                        (θ.naturality f) =
                      CategoryTheory.CategoryStruct.comp (η.naturality f)
                        (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom))
                  CategoryTheory.Oplax.LaxTrans.isoMk._auto_1 →
                (η ≅ θ)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instIsScalarTower_closedBall : IsScalarTower Complex.UnitClosedDisc Complex.UnitDisc Complex.UnitDisc
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- A linearly independent family of vectors is also affinely independent.  -/
LinearIndependent.affineIndependent : ∀ (k : Type u_1) {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_4}
  {v : ι → V}, LinearIndependent k v → AffineIndependent k v
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.coconeOfDiagramInitial_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {X : J} (hX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C)
  [inst_2 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)],
  (CategoryTheory.Limits.coconeOfDiagramInitial hX F).pt = F.obj X
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.prop_of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f], P X → P Y
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.allLTTR.loop.congr_simp : ∀ (n : ℕ) (f f_1 : (i : ℕ) → i < n → Bool),
  f = f_1 → ∀ (i i_1 : ℕ) (e_i : i = i_1) (a : i ≤ n), Nat.allLTTR.loop✝ n f i a = Nat.allLTTR.loop✝ n f_1 i_1 ⋯
-- Mathlib.Algebra.Homology.Localization
HomotopyCategory.respectsIso_quasiIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C],
  (HomotopyCategory.quasiIso C c).RespectsIso
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateWithAnchor.mk.sizeOf_spec : ∀ (c : Lean.Meta.Grind.SplitInfo) (numCases : ℕ) (isRec : Bool) (e : Lean.Expr) (anchor : UInt64),
  sizeOf { c := c, numCases := numCases, isRec := isRec, e := e, anchor := anchor } =
    1 + sizeOf c + sizeOf numCases + sizeOf isRec + sizeOf e + sizeOf anchor
-- Lean.Meta.Basic
Lean.Meta.State.mk.injEq : ∀ (mctx : Lean.MetavarContext) (cache : Lean.Meta.Cache) (zetaDeltaFVarIds : Lean.FVarIdSet)
  (postponed : Lean.PersistentArray Lean.Meta.PostponedEntry) (diag : Lean.Meta.Diagnostics)
  (mctx_1 : Lean.MetavarContext) (cache_1 : Lean.Meta.Cache) (zetaDeltaFVarIds_1 : Lean.FVarIdSet)
  (postponed_1 : Lean.PersistentArray Lean.Meta.PostponedEntry) (diag_1 : Lean.Meta.Diagnostics),
  ({ mctx := mctx, cache := cache, zetaDeltaFVarIds := zetaDeltaFVarIds, postponed := postponed, diag := diag } =
      { mctx := mctx_1, cache := cache_1, zetaDeltaFVarIds := zetaDeltaFVarIds_1, postponed := postponed_1,
        diag := diag_1 }) =
    (mctx = mctx_1 ∧ cache = cache_1 ∧ zetaDeltaFVarIds = zetaDeltaFVarIds_1 ∧ postponed = postponed_1 ∧ diag = diag_1)
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instAddGroupQuotient : {S : Type u_2} →
  (M : Type u_3) → [inst : SMul S M] → [inst_1 : AddGroup M] → (c : ModuleCon S M) → AddGroup (ModuleCon.Quotient M c)
-- Mathlib.GroupTheory.Coset.Basic
mem_own_rightCoset : ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ MulOpposite.op a • ↑s
-- Mathlib.CategoryTheory.DinatTrans
/-- The commutativity square for a given morphism.  -/
CategoryTheory.DinatTrans.dinaturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D)} (self : CategoryTheory.DinatTrans F G) {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F.map f.op).app X)
      (CategoryTheory.CategoryStruct.comp (self.app X) ((G.obj (Opposite.op X)).map f)) =
    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op Y)).map f)
      (CategoryTheory.CategoryStruct.comp (self.app Y) ((G.map f.op).app Y))
-- Std.Data.HashSet.Lemmas
Std.HashSet.toList_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α}, ∅.toList = []
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.map_unique : ∀ {f : ZFSet.{u} → ZFSet.{u}} [inst : ZFSet.Definable₁ f] {x z : ZFSet.{u}}, z ∈ x → ∃! w, z.pair w ∈ ZFSet.map f x
-- Init.System.IOError
IO.Error.invalidArgument.sizeOf_spec : ∀ (filename : Option String) (osCode : UInt32) (details : String),
  sizeOf (IO.Error.invalidArgument filename osCode details) = 1 + sizeOf filename + sizeOf osCode + sizeOf details
-- Mathlib.FieldTheory.Finite.Basic
/-- If `R` is a perfect ring and an algebra over a finite field `K`, the Frobenius `K`-algebra
endomorphism of `R` is an automorphism.  -/
FiniteField.frobeniusAlgEquiv : (K : Type u_1) →
  (R : Type u_2) →
    [inst : Field K] →
      [Fintype K] →
        [inst_2 : CommRing R] → [inst_3 : Algebra K R] → (p : ℕ) → [ExpChar R p] → [PerfectRing R p] → R ≃ₐ[K] R
-- Qq.SortLocalDecls
Qq.SortLocalDecls.State.mk.inj : ∀ {visited : Lean.NameSet} {result : Array Lean.LocalDecl} {visited_1 : Lean.NameSet} {result_1 : Array Lean.LocalDecl},
  { visited := visited, result := result } = { visited := visited_1, result := result_1 } →
    visited = visited_1 ∧ result = result_1
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.weierstrassDiv.congr_simp : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f f_1 : PowerSeries A),
  f = f_1 →
    ∀ (g g_1 : PowerSeries A),
      g = g_1 →
        ∀ [inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A] (a a_1 : Unit →₀ ℕ),
          a = a_1 → (f /ʷ g) a = (f_1 /ʷ g_1) a_1
-- Mathlib.Order.Filter.Pointwise
Filter.pure_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {g : Filter β} {a : α}, pure a • g = Filter.map (fun x => a • x) g
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mk_mul_mk : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {a₁ a₂ : A} {s₁ s₂ : ↥S}, LocalizedModule.mk a₁ s₁ * LocalizedModule.mk a₂ s₂ = LocalizedModule.mk (a₁ * a₂) (s₁ * s₂)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.measure_singleton_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {a : α} [MeasureTheory.SigmaFinite μ], μ {a} < ⊤
-- Init.Grind.Util
Lean.Grind.nestedProofUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryMidEquiv_symm_apply : ∀ (𝕜 : Type u) {n : ℕ} (Ei : Fin n.succ → Type wEi) (G : Type wG) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (p : Fin (n + 1))
  (f : Ei p →L[𝕜] Ei (p.succAbove i) [×n]→L[𝕜] G),
  (ContinuousMultilinearMap.curryMidEquiv 𝕜 Ei G p).symm f = ContinuousLinearMap.uncurryMid p f
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nontrivial.mul_left : ∀ {α : Type u_2} [inst : Mul α] [IsLeftCancelMul α] {s t : Set α}, t.Nontrivial → s.Nonempty → (s * t).Nontrivial
-- Mathlib.Topology.Germ
eq_of_germ_isConstant : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y} [i : PreconnectedSpace X],
  (∀ (x : X), (↑f).IsConstant) → ∀ (x x' : X), f x = f x'
-- Mathlib.Algebra.Order.ToIntervalMod
sub_toIocDiv_zsmul_mem_Ioc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), b - toIocDiv hp a b • p ∈ Set.Ioc a (a + p)
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.coe_finsetSup : ∀ {X : Type u_1} {R : Type u_2} [inst : AddCommMonoid R] [inst_1 : LinearOrder R] [inst_2 : AddLeftStrictMono R]
  [inst_3 : IsOrderedAddMonoid R] {Y : Type u_3} {f : Y → PseudoMetric X R} {s : Finset Y} (hs : s.Nonempty),
  ⇑(s.sup f) = ⇑(s.sup' hs fun x => f x)
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_div_sphere : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E), {x} / Metric.sphere y δ = Metric.sphere (x / y) δ
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff`.

---

The natural map from `SkewMonoidAlgebra k G` to `G →₀ k`.  -/
SkewMonoidAlgebra.toFinsupp : {k : Type u_1} → {G : Type u_2} → [inst : Zero k] → SkewMonoidAlgebra k G → G →₀ k
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
/-- The coroot attached to a reflective vector.  -/
LinearMap.IsReflective.coroot : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (B : M →ₗ[R] M →ₗ[R] R) → {x : M} → B.IsReflective x → M →ₗ[R] R
-- Std.Time.Date.Unit.Year
/-- Calculates the number of days in the specified `year`.
 -/
Std.Time.Year.Offset.days : Std.Time.Year.Offset → Std.Time.Internal.Bounded.LE 365 366
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientGroup.instNormedCommGroup.eq_1 : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] (S : Subgroup M) [hS : IsClosed ↑S],
  QuotientGroup.instNormedCommGroup S =
    { toNorm := QuotientGroup.instNorm, toCommGroup := QuotientGroup.Quotient.commGroup S,
      toMetricSpace := MetricSpace.ofT0PseudoMetricSpace (M ⧸ S), dist_eq := ⋯ }
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.Hom.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] {V W : QuadraticModuleCat R} [inst_1 : SizeOf R] (toIsometry' : V.form →qᵢ W.form),
  sizeOf { toIsometry' := toIsometry' } = 1 + sizeOf toIsometry'
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.LetRecClosure.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (localDecls : Array Lean.LocalDecl) (closed : Lean.Expr) (toLift : Lean.Elab.Term.LetRecToLift),
  sizeOf { ref := ref, localDecls := localDecls, closed := closed, toLift := toLift } =
    1 + sizeOf ref + sizeOf localDecls + sizeOf closed + sizeOf toLift
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.isZero_under : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.EnoughInjectives C] (X : C),
  CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsZero (CategoryTheory.Injective.under X)
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticMap.Isometry.tmul_apply : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} {M₄ : Type uM₄} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : AddCommGroup M₄]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] [inst_9 : Invertible 2]
  {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄}
  (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) (x : TensorProduct R M₁ M₃),
  (f.tmul g) x = (TensorProduct.map f.toLinearMap g.toLinearMap) x
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- `c.toOver` is a lift of `c` under the forgetful functor.  -/
CategoryTheory.Limits.Cocone.mapCoconeToOver : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) → (CategoryTheory.Over.forget c.pt).mapCocone c.toOver ≅ c
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure.of_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {X Y : C} (e : X ≅ Y),
  P.colimitsClosure J X → P.colimitsClosure J Y
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_of_isLocalizedEquivalence : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : 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} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₁' : CategoryTheory.MorphismProperty D₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [W₂'.RespectsIso] [L.IsLocalizedEquivalence] [R.IsLocalizedEquivalence]
  [R.functor.EssSurj] [T.IsRightDerivabilityStructure] (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor)
  [CategoryTheory.TwoSquare.GuitartExact iso.hom], B.IsRightDerivabilityStructure
-- Mathlib.Analysis.Complex.Order
/-- **Alias** of the reverse direction of `Complex.ofReal_ne_zero`. -/
Mathlib.Meta.Positivity.ofReal_ne_zero_of_ne_zero : ∀ {z : ℝ}, z ≠ 0 → ↑z ≠ 0
-- Init.Data.BitVec.Lemmas
BitVec.mul_twoPow_eq_shiftLeft : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), x * BitVec.twoPow w i = x <<< i
-- Mathlib.Probability.Independence.Conditional
/-- Two functions are conditionally independent if the two measurable space structures they generate
are conditionally independent. For a function `f` with codomain having measurable space structure
`m`, the generated measurable space structure is `m.comap f`.
See `ProbabilityTheory.condIndepFun_iff`.
We use the notation `X ⟂ᵢ[Z, hZ; μ] Y` to write that `X` and `Y` are conditionally independent
given (the σ-algebra generated by) `Z` (scoped in `ProbabilityTheory`).  -/
ProbabilityTheory.«term_⟂ᵢ[_,_]_» : Lean.TrailingParserDescr
-- Mathlib.Data.Nat.Bits
Nat.bit_cases_on_inj : ∀ {motive : ℕ → Sort u} (H₁ H₂ : (b : Bool) → (n : ℕ) → motive (Nat.bit b n)),
  ((fun n => Nat.bitCasesOn n H₁) = fun n => Nat.bitCasesOn n H₂) ↔ H₁ = H₂
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f = g` on some neighbourhood of `x`,
then `f` is an immersion at `x` if and only if `g` is an immersion at `x`.  -/
Manifold.IsImmersionAt.congr_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M},
  f =ᶠ[nhds x] g → (Manifold.IsImmersionAt I J n f x ↔ Manifold.IsImmersionAt I J n g x)
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Set
_private.Std.Data.Iterators.Lemmas.Consumers.Monadic.Set.0.Std.IterM.toExtHashSet.eq_1 : ∀ {α β : Type w} [inst : BEq β] [inst_1 : Hashable β] [inst_2 : EquivBEq β] [inst_3 : LawfulHashable β]
  {m : Type w → Type w'} [inst_4 : Monad m] [inst_5 : Std.Iterator α m β] [inst_6 : Std.IteratorLoop α m m]
  (it : Std.IterM m β), it.toExtHashSet = Std.IterM.fold (fun acc a => acc.insert a) ∅ it
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- A function is `C^n` within a set at a point iff it is `C^m` within this set at this point, for
any `m ≤ n` which is different from `∞`. This result is useful because, when `m ≠ ∞`, being
`C^m` extends locally to a neighborhood, giving flexibility for local proofs.  -/
contMDiffWithinAt_iff_le_ne_infty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f s x ↔ ∀ m ≤ n, m ≠ ↑⊤ → ContMDiffWithinAt I I' m f s x