mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.instIsStableUnderCompositionSchemeTopologicallyIsOpenMap : (AlgebraicGeometry.topologically @IsOpenMap).IsStableUnderComposition
-- Mathlib.RingTheory.AdjoinRoot
Polynomial.Monic.free_adjoinRoot : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R}, g.Monic → Module.Free R (AdjoinRoot g)
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallCache.decrTactic? : Lean.Elab.WF.GuessLex.RecCallCache → Option Lean.Elab.DecreasingBy
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The identity morphism on a comonoid object.  -/
CategoryTheory.Comon.id : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (M : CategoryTheory.Comon C) → M.Hom M
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_add_left' : ∀ {α : 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 T' T'' : Set α → E →L[ℝ] F),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s) →
    ∀ {f : MeasureTheory.SimpleFunc α E},
      MeasureTheory.Integrable (⇑f) μ →
        MeasureTheory.SimpleFunc.setToSimpleFunc T'' f =
          MeasureTheory.SimpleFunc.setToSimpleFunc T f + MeasureTheory.SimpleFunc.setToSimpleFunc T' f
-- Mathlib.Lean.Expr.Basic
/-- Tests is if an expression matches either `x ≠ y` or `¬ (x = y)`.
If it matches, returns `some (type, x, y)`.  -/
Lean.Expr.ne?' : Lean.Expr → Option (Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_inverse_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma S' (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).inverse.obj X).right = X.right
-- Mathlib.Topology.DiscreteQuotient
Setoid.classes.eq_1 : ∀ {α : Type u_1} (r : Setoid α), r.classes = {s | ∃ y, s = {x | r x y}}
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- **Alias** of `ModelWithCorners.contDiffWithinAt_extendCoordChange`. -/
OpenPartialHomeomorph.contDiffWithinAt_extend_coord_change : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {n : WithTop ℕ∞} {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} [inst_5 : ChartedSpace H M],
  e ∈ IsManifold.maximalAtlas I n M →
    e' ∈ IsManifold.maximalAtlas I n M →
      ∀ {x : E},
        x ∈ (ModelWithCorners.extendCoordChange e e').source →
          ContDiffWithinAt 𝕜 n (↑(ModelWithCorners.extendCoordChange e e')) (Set.range ↑I) x
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.insert.eq_def : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.insert k m p =
    bif k == 0 then p
    else bif m == Lean.Grind.CommRing.Mon.unit then p.addConst k else Lean.Grind.CommRing.Poly.insert.go k m p
-- Std.Http.Data.Body.Full
/-- Selector that immediately resolves to the remaining chunk (or EOF).
 -/
Std.Http.Body.Full.recvSelector : Std.Http.Body.Full → Std.Async.Selector (Option Std.Http.Chunk)
-- Mathlib.Order.SuccPred.WithBot
/-- The predecessor of `a : WithTop α` as an element of `α`.  -/
WithTop.pred : {α : Type u_1} → [inst : Preorder α] → [OrderTop α] → [PredOrder α] → WithTop α → α
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.plusMap_plusLift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R),
  CategoryTheory.CategoryStruct.comp (J.plusMap η) (J.plusLift γ hR) =
    J.plusLift (CategoryTheory.CategoryStruct.comp η γ) hR
-- Mathlib.ModelTheory.Basic
/-- Any element of a bijective `StrongHomClass` can be realized as a first order isomorphism.  -/
FirstOrder.Language.StrongHomClass.toEquiv : {L : FirstOrder.Language} →
  {F : Type u_3} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : L.Structure M] →
          [inst_1 : L.Structure N] → [inst_2 : EquivLike F M N] → [L.StrongHomClass F M N] → F → L.Equiv M N
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonChangeAnnotation.fromJson : Lean.Json → Except String Lean.Lsp.ChangeAnnotation
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
/-- The type of morphisms between spectral objects in pretriangulated categories.  -/
CategoryTheory.Triangulated.SpectralObject.Hom : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [inst_6 : CategoryTheory.Pretriangulated C] →
                  CategoryTheory.Triangulated.SpectralObject C ι →
                    CategoryTheory.Triangulated.SpectralObject C ι → Type (max (max u_2 v_1) v_2)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : LawfulBEq α] {k : α} {f : Option β → Option β},
  m.WF →
    (Std.DHashMap.Raw.Const.alter m k f).size =
      if k ∈ m ∧ (f (Std.DHashMap.Raw.Const.get? m k)).isNone = true then m.size - 1
      else if k ∉ m ∧ (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true then m.size + 1 else m.size
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.card_relations_sum : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (i : ℕ),
  Cardinal.mk ((L.sum L').Relations i) =
    Cardinal.lift.{v', v} (Cardinal.mk (L.Relations i)) + Cardinal.lift.{v, v'} (Cardinal.mk (L'.Relations i))
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castSuccEmb_Ici : ∀ {n : ℕ} (i : Fin n), Finset.map Fin.castSuccEmb (Finset.Ici i) = Finset.Ico i.castSucc (Fin.last n)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The oriented angle are equal or opposite if the unoriented angles are equal.  -/
EuclideanGeometry.oangle_eq_or_eq_neg_of_angle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₅ p₆ →
    p₂ ≠ p₁ →
      p₂ ≠ p₃ →
        p₅ ≠ p₄ →
          p₅ ≠ p₆ →
            EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₄ p₅ p₆ ∨
              EuclideanGeometry.oangle p₁ p₂ p₃ = -EuclideanGeometry.oangle p₄ p₅ p₆
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority.elab : Lean.Syntax → Aesop.ElabM Aesop.Frontend.Priority
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int16.intCast_neg : ∀ (i : ℤ), ↑(-i) = -↑i
-- Mathlib.Analysis.Convex.Between
/-- The interior of a 1-simplex is a segment between its vertices.  -/
Affine.Simplex.interior_eq_image_Ioo : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] (s : Affine.Simplex R P 1),
  s.interior = ⇑(AffineMap.lineMap (s.points 0) (s.points 1)) '' Set.Ioo 0 1
-- Std.Data.DTreeMap.Internal.Def
/-- (Implementation detail)  -/
Std.DTreeMap.Internal.Impl.leaf : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.logHomeomorph_apply : ∀ (x : ENNReal), ENNReal.logHomeomorph x = x.log
-- Mathlib.Tactic.Sat.FromLRAT
/-- Swap the polarity of a literal.  -/
Sat.Literal.negate : Sat.Literal → Sat.Literal
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- Cancellation of a telescoping sum.  -/
List.sum_range_sub : ∀ {G : Type u_7} [inst : AddCommGroup G] (n : ℕ) (f : ℕ → G),
  (List.map (fun k => f (k + 1) - f k) (List.range n)).sum = f n - f 0
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintKind.type.sizeOf_spec : sizeOf Lean.Elab.InlayHintKind.type = 1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  [inst_4 : (G.sheafPushforwardContinuous A J K).IsEquivalence] [inst_5 : CategoryTheory.HasWeakSheafify J A]
  {P : CategoryTheory.Functor Dᵒᵖ A} {Q₁ Q₂ : CategoryTheory.Sheaf K A}
  (f : (CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).obj P ⟶ Q₁) (g : Q₁ ⟶ Q₂)
  {Z : CategoryTheory.Functor Dᵒᵖ A} (h : Q₂.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G)
        (CategoryTheory.CategoryStruct.comp f g))
      h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G) f)
      (CategoryTheory.CategoryStruct.comp g.hom h)
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts
/-- An abbreviation for `HasConicalLimit V (Discrete.functor f)`.  -/
CategoryTheory.Enriched.HasConicalProduct : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [CategoryTheory.EnrichedOrdinaryCategory V C] → {I : Type w} → (I → C) → Prop
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.comp_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {a_1 b_1 c : a ⟶ b}
  (x : CategoryTheory.Bicategory.Adj.Hom₂ a_1 b_1) (y : CategoryTheory.Bicategory.Adj.Hom₂ b_1 c),
  (CategoryTheory.CategoryStruct.comp x y).τr = CategoryTheory.CategoryStruct.comp y.τr x.τr
-- Mathlib.Geometry.Manifold.Notation
/-- `TangentSpace% x` elaborates to `TangentSpace I x`,
trying to determine `I` from the local context.  -/
Manifold.«termTangentSpace%__» : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.Bounded
/-- **Alias** of the forward direction of `isBounded_iff_forall_norm_le`. -/
Bornology.IsBounded.exists_norm_le : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] {s : Set E}, Bornology.IsBounded s → ∃ C, ∀ x ∈ s, ‖x‖ ≤ C
-- Mathlib.Tactic.Ring.Common
/-- `ExProdNat e` stores the structure of a normalized monomial expression `e : Q(ℕ)`.
A monomial here is a product of powers of `ExBaseNat` expressions, terminated by a (nonzero)
constant coefficient.

Used to represent normalized natural number expressions in exponents.

`ExProdNat q($e)` is equivalent to `ExProd btℕ sℕ q($e)`, and one can cast between the two.
 -/
Mathlib.Tactic.Ring.Common.ExProdNat : Q(ℕ) → Type
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- `PolynomialModule.coeff` as an `AddEquiv`.  -/
PolynomialModule.coeffAddEquiv : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → PolynomialModule R M ≃+ (ℕ →₀ M)
-- Mathlib.Topology.Germ
restrictGermPredicate_congr : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f g : X → Y} {A : Set X} {x : X}
  {P : (x : X) → (nhds x).Germ Y → Prop},
  RestrictGermPredicate P A x ↑f → (∀ᶠ (z : X) in nhdsSet A, g z = f z) → RestrictGermPredicate P A x ↑g
-- Init.Data.BitVec.Bitblast
BitVec.intMin_udiv_ne_zero_of_ne_zero : ∀ {w : ℕ} {b : BitVec w}, b.msb = false → b ≠ 0#w → BitVec.intMin w / b ≠ 0#w
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getNegThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.number.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.number = 1
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.le_def : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f g : L.PartialEquiv M N),
  f ≤ g ↔
    ∃ (h : f.dom ≤ g.dom),
      g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion h)) =
        f.cod.subtype.comp f.toEquiv.toEmbedding
-- Mathlib.Algebra.Order.Hom.Monoid
AddMonoidHomClass.ext_iff_le : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddMonoid β] {F : Type u_6} [inst_2 : FunLike F α β]
  [AddMonoidHomClass F α β] [inst : PartialOrder β] [AddRightMono β] [AddLeftMono β] {f g : F},
  f = g ↔ ∀ (x : α), f x ≤ g x
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- By definition, if we have `ZeroMemClass S M`, we have `0 ∈ s` for all `s : S`.  -/
ZeroMemClass.zero_mem : ∀ {S : Type u_3} {M : outParam (Type u_4)} {inst : Zero M} {inst_1 : SetLike S M} [self : ZeroMemClass S M] (s : S),
  0 ∈ s
-- Init.Data.BitVec.Bitblast
Bool.atLeastTwo_false_right : ∀ {a b : Bool}, a.atLeastTwo b false = (a && b)
-- Mathlib.Data.Nat.Log
Nat.log_eq_one_iff' : ∀ {b n : ℕ}, Nat.log b n = 1 ↔ b ≤ n ∧ n < b * b
-- Mathlib.Topology.Order.ScottTopology
Topology.WithScott.toScott_ofScott : ∀ {α : Type u_1} (a : Topology.WithScott α), Topology.WithScott.toScott (Topology.WithScott.ofScott a) = a
-- Mathlib.Algebra.Ring.Units
/-- Representing an element of a ring's unit group as an element of the ring commutes with
mapping this element to its additive inverse.  -/
Units.val_neg : ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] (u : αˣ), ↑(-u) = -↑u
-- Mathlib.Tactic.FBinop
FBinopElab.SRec.mk.inj : ∀ {name : Lean.Name} {args : Array Lean.Expr} {name_1 : Lean.Name} {args_1 : Array Lean.Expr},
  { name := name, args := args } = { name := name_1, args := args_1 } → name = name_1 ∧ args = args_1
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} (kf : CategoryTheory.Limits.KernelFork f)
  {kf' : CategoryTheory.Limits.KernelFork f'} (hf' : CategoryTheory.Limits.IsLimit kf')
  (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'),
  CategoryTheory.CategoryStruct.comp (kf.mapOfIsLimit hf' φ) (CategoryTheory.Limits.Fork.ι kf') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Arrow.Hom.left φ)
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.restrictionLEIso_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (i : ℕ),
  h.restrictionLEIso.hom.f i =
    (HomologicalComplex.restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.mk.injEq : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (toFun : ι → ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)
  (locallyFinite' : LocallyFinite fun i => Function.support ⇑(toFun i)) (nonneg' : ∀ (i : ι) (x : M), 0 ≤ (toFun i) x)
  (sum_eq_one' : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun i) x = 1) (sum_le_one' : ∀ (x : M), ∑ᶠ (i : ι), (toFun i) x ≤ 1)
  (toFun_1 : ι → ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)
  (locallyFinite'_1 : LocallyFinite fun i => Function.support ⇑(toFun_1 i))
  (nonneg'_1 : ∀ (i : ι) (x : M), 0 ≤ (toFun_1 i) x) (sum_eq_one'_1 : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun_1 i) x = 1)
  (sum_le_one'_1 : ∀ (x : M), ∑ᶠ (i : ι), (toFun_1 i) x ≤ 1),
  ({ toFun := toFun, locallyFinite' := locallyFinite', nonneg' := nonneg', sum_eq_one' := sum_eq_one',
        sum_le_one' := sum_le_one' } =
      { toFun := toFun_1, locallyFinite' := locallyFinite'_1, nonneg' := nonneg'_1, sum_eq_one' := sum_eq_one'_1,
        sum_le_one' := sum_le_one'_1 }) =
    (toFun = toFun_1)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorPreCore.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : SizeOf B] [inst_3 : SizeOf C] (toPrelaxFunctor : CategoryTheory.PrelaxFunctor B C)
  (map_id :
    autoParam
      (∀ (X : B),
        toPrelaxFunctor.map (CategoryTheory.CategoryStruct.id X) =
          CategoryTheory.CategoryStruct.id (toPrelaxFunctor.obj X))
      CategoryTheory.StrictPseudofunctorPreCore.map_id._autoParam)
  (map_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        toPrelaxFunctor.map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (toPrelaxFunctor.map f) (toPrelaxFunctor.map g))
      CategoryTheory.StrictPseudofunctorPreCore.map_comp._autoParam)
  (map₂_whisker_left :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'),
        toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.whiskerLeft f η) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor.map f) (toPrelaxFunctor.map₂ η))
              (CategoryTheory.eqToHom ⋯)))
      CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_left._autoParam)
  (map₂_whisker_right :
    autoParam
      (∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
        toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.whiskerRight η g) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerRight (toPrelaxFunctor.map₂ η) (toPrelaxFunctor.map g))
              (CategoryTheory.eqToHom ⋯)))
      CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_right._autoParam),
  sizeOf
      { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := map_comp,
        map₂_whisker_left := map₂_whisker_left, map₂_whisker_right := map₂_whisker_right } =
    1 + sizeOf toPrelaxFunctor
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_X : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R] [MulSemiringAction (Multiplicative ℕ) R],
  SkewPolynomial.X.support = {1}
-- Aesop.Forward.State
Aesop.Hyp.mk.sizeOf_spec : ∀ (fvarId? : Option Lean.FVarId) (subst : Aesop.Substitution),
  sizeOf { fvarId? := fvarId?, subst := subst } = 1 + sizeOf fvarId? + sizeOf subst
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.Z_eq_zero_of_equiv : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P ≈ Q → (P 2 = 0 ↔ Q 2 = 0)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.initial_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} [F.Initial] (i : F ≅ F'), F'.Initial
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceInverse_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  {Y Z :
    CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
      (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))}
  (f : Y ⟶ Z),
  (CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X).map f =
    CategoryTheory.StructuredArrow.homMk
      { left := CategoryTheory.StructuredArrow.Hom.right f.left,
        right := CategoryTheory.StructuredArrow.Hom.right f.right, w := ⋯ }
      ⋯
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofSubmodules_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂)
  {p : Submodule R M} {q : Submodule R₂ M₂} (h : Submodule.map (↑e) p = q) (x : ↥p), ↑((e.ofSubmodules p q h) x) = e ↑x
-- Mathlib.Analysis.LocallyConvex.WeakDual
/-- When `B` is left-separating, `E` is linearly equivalent to the strong dual of `F` with the
weak topology.  -/
LinearMap.leftDualEquiv : {𝕜 : Type u_5} →
  {E : Type u_6} →
    {F : Type u_7} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : AddCommGroup F] →
              [inst_4 : Module 𝕜 F] →
                (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → B.SeparatingLeft → E ≃ₗ[𝕜] StrongDual 𝕜 (WeakBilin B.flip)
-- Mathlib.Algebra.Homology.LocalCohomology
/-- Local cohomology agrees along precomposition with a cofinal diagram.  -/
localCohomology.isoOfFinal : {R : Type (max u v v')} →
  [inst : CommRing R] →
    {D : Type v} →
      [inst_1 : CategoryTheory.SmallCategory D] →
        {E : Type v'} →
          [inst_2 : CategoryTheory.SmallCategory E] →
            (I' : CategoryTheory.Functor E D) →
              (I : CategoryTheory.Functor D (Ideal R)) →
                [I'.Initial] → (i : ℕ) → localCohomology.ofDiagram (I'.comp I) i ≅ localCohomology.ofDiagram I i
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.flip_bijective_iff₂ : ∀ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂],
  Function.Bijective ⇑B.flip ↔ Function.Bijective ⇑B
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow.oadd : ∀ {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}}, e.NF → a.NFBelow e.repr → e.repr < b → (e.oadd n a).NFBelow b
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalarsSum_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜), FormalMultilinearSeries.ofScalarsSum c 0 = c 0 • 1
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.coe_unop : ∀ {M : Type u_2} [inst : AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ), ↑x.unop = AddOpposite.op ⁻¹' ↑x