mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.map_π_preserves_coequalizer_inv_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) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {Z : D}
  (h : CategoryTheory.Limits.coequalizer (G.map f) (G.map g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π (G.map f) (G.map g)) h
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of `C^n` functions at points in domains is `C^n`,
with a weaker condition on `s` and `t`.  -/
ContDiffWithinAt.comp_of_preimage_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : F → G}
  {f : E → F} (x : E),
  ContDiffWithinAt 𝕜 n g t (f x) →
    ContDiffWithinAt 𝕜 n f s x → f ⁻¹' t ∈ nhdsWithin x s → ContDiffWithinAt 𝕜 n (g ∘ f) s x
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.pullback.lift.congr_simp : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g]
  {Z : CompHausLike P} (a a_1 : Z ⟶ X) (e_a : a = a_1) (b b_1 : Z ⟶ Y) (e_b : b = b_1)
  (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g),
  CompHausLike.pullback.lift f g a b w = CompHausLike.pullback.lift f g a_1 b_1 ⋯
-- Mathlib.NumberTheory.Dioph
Poly.const_apply : ∀ {α : Type u_1} (n : ℤ) (x : α → ℕ), (Poly.const n) x = n
-- Lean.Meta.HaveTelescope
/-- The initial expression in `(fun x => b) v` form.
 -/
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.SimpHaveResult.exprInit : Lean.Meta.SimpHaveResult✝ → Lean.Expr
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.self_modEq_zero : ∀ {M : Type u_1} [inst : AddCommMonoid M] {p : M}, p ≡ 0 [PMOD p]
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.sMod_mod : ∀ (p i : ℕ), LucasLehmer.sMod p i % (2 ^ p - 1) = LucasLehmer.sMod p i
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {a fallback : α}, ∅.getKeyD a fallback = fallback
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- Connecting two unreachable vertices by an edge preserves acyclicity.  -/
SimpleGraph.IsAcyclic.sup_edge_of_not_reachable : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, ¬G.Reachable u v → G.IsAcyclic → (G ⊔ SimpleGraph.edge u v).IsAcyclic
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestMatch_iff_isLongestMatchAt_ofSliceFrom : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {base : s.Pos}
  (endPos : (s.sliceFrom base).Pos),
  String.Slice.Pattern.Model.IsLongestMatch pat endPos ↔
    String.Slice.Pattern.Model.IsLongestMatchAt pat base (String.Slice.Pos.ofSliceFrom endPos)
-- Mathlib.Algebra.Ring.Ext
NonUnitalNonAssocSemiring.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : NonUnitalNonAssocSemiring R},
  inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Mathlib.Data.ENNReal.Operations
ENNReal.iSup_zero : ∀ {ι : Sort u_1}, ⨆ x, 0 = 0
-- Lean.Parser.Command
Lean.Parser.Command.check.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.op_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  CategoryTheory.NatIso.op F.leftUnitor =
    F.op.leftUnitor.symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.opId C).symm F.op ≪≫
        ((CategoryTheory.Functor.id C).opComp F).symm
-- Mathlib.Algebra.DirectSum.Module
DirectSum.isInternal_biSup_submodule_of_iSupIndep : ∀ {R : Type u} [inst : Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {A : ι → Submodule R M} (s : Set ι),
  (iSupIndep fun i => A ↑i) → DirectSum.IsInternal fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.prod_atTop_atTop_eq : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β], Filter.atTop ×ˢ Filter.atTop = Filter.atTop
-- Lean.SubExpr
Lean.SubExpr.instToJsonGoalLocation.toJson : Lean.SubExpr.GoalLocation → Lean.Json
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets_intersect : ∀ {R : Type u_1} {E : Type u_6} {ι : Type u_9} [inst : SeminormedRing R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p : SeminormFamily R E ι) (U V : Set E), U ∈ p.basisSets → V ∈ p.basisSets → ∃ z ∈ p.basisSets, z ⊆ U ∩ V
-- Mathlib.Computability.Reduce
oneOneEquiv_refl : ∀ {α : Type u_1} [inst : Primcodable α] (p : α → Prop), OneOneEquiv p p
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_zero : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜), ↑0 = 0
-- Mathlib.RingTheory.Trace.Quotient
RingHom.quotientKerEquivOfSurjective.eq_1 : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {f : R →+* S} (hf : Function.Surjective ⇑f),
  RingHom.quotientKerEquivOfSurjective hf = RingHom.quotientKerEquivOfRightInverse ⋯
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
le_add_iff_lt_left_or_exists_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α} [inst_1 : Add α] [CanonicallyOrderedAdd α] [AddLeftMono α]
  [IsLeftCancelAdd α], a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
-- Mathlib.Topology.Inseparable
specializes_iff_pure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y ↔ pure x ≤ nhds y
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_inter_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioi a ∩ Set.Ioo c b = Set.Ioo (max a c) b
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.prod_unique : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : M →+ N × P), ((AddMonoidHom.fst N P).comp f).prod ((AddMonoidHom.snd N P).comp f) = f
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι]
  {𝔸' : Type u_3} [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) →
    derivWithin (∏ i ∈ u, f i) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_insertIfNew_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, k ∈ m.insertIfNew k v
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.fromAddMonoid_of_apply : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {γ : Type u₁}
  [inst_2 : AddCommMonoid γ] (i : ι) (f : γ →+ β i) (x : γ),
  (DirectSum.fromAddMonoid ((DirectSum.of (fun i => γ →+ β i) i) f)) x = (DirectSum.of β i) (f x)
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) {Z_1 : C}
  (h : ((ChainComplex.single₀ C).obj Z).X 0 ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (CategoryTheory.CategoryStruct.comp (P.π.f 0) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Init.Data.List.Impl
List.eraseP.eq_1 : ∀ {α : Type u} (p : α → Bool), List.eraseP p [] = []
-- Mathlib.Data.PNat.Basic
PNat.coe_coeMonoidHom : ⇑PNat.coeMonoidHom = PNat.val
-- Mathlib.Order.UpperLower.Basic
isLowerSet_Iio : ∀ {α : Type u_1} [inst : Preorder α] (a : α), IsLowerSet (Set.Iio a)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonDeleteFile.toJson : Lean.Lsp.DeleteFile → Lean.Json
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.apply_of_skipSuffixWhile_le_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos : s.Pos},
  s.skipSuffixWhile P ≤ pos → ∀ (h' : pos < s.endPos), P (pos.get ⋯)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.dropPrefix?_string_empty : ∀ {s : String}, s.dropPrefix? "" = some s.toSlice
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin_scalar : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (r : R),
  (Matrix.toLin v₁ v₁) ((Matrix.scalar n) r) = r • LinearMap.id
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- For `κ' := map κ (Prod.map (id : β → β) e)`, the hypothesis `hη` is `fst κ' ⊗ₖ η = κ'`.
The conclusion of the lemma is `fst κ ⊗ₖ borelMarkovFromReal Ω η = comapRight (fst κ' ⊗ₖ η) _`.  -/
ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal_eq_comapRight_compProd : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] [inst_1 : Nonempty Ω] (κ : ProbabilityTheory.Kernel α (β × Ω))
  [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) ℝ) [ProbabilityTheory.IsSFiniteKernel η],
  (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).fst.compProd η =
      κ.map (Prod.map id (MeasureTheory.embeddingReal Ω)) →
    κ.fst.compProd (ProbabilityTheory.Kernel.borelMarkovFromReal Ω η) =
      ((κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).fst.compProd η).comapRight ⋯
-- Mathlib.Data.Setoid.Partition
/-- A set of disjoint sets covering α partition α (classical).  -/
Setoid.eqv_classes_of_disjoint_union : ∀ {α : Type u_1} {c : Set (Set α)}, ⋃₀ c = Set.univ → c.PairwiseDisjoint id → ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
-- Mathlib.Data.EReal.Operations
EReal.mul_top_of_pos : ∀ {x : EReal}, 0 < x → x * ⊤ = ⊤
-- Mathlib.Algebra.Module.Pi
Pi.module : (I : Type u) →
  (f : I → Type v) →
    (α : Type u_1) →
      {r : Semiring α} → {m : (i : I) → AddCommMonoid (f i)} → [(i : I) → Module α (f i)] → Module α ((i : I) → f i)
-- Mathlib.Algebra.Lie.Matrix
Matrix.reindexLieEquiv_symm : ∀ {R : Type u} [inst : CommRing R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {m : Type w₁}
  [inst_3 : DecidableEq m] [inst_4 : Fintype m] (e : n ≃ m),
  (Matrix.reindexLieEquiv e).symm = Matrix.reindexLieEquiv e.symm
-- Lean.ImportingFlag
Lean.isInitializerExecutionEnabled : BaseIO Bool
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Coframe.toCompleteLattice : {α : Type u_1} → [self : Order.Coframe α] → CompleteLattice α
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.PlausibleStep : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [inst : Std.Iterator α m β] → Std.IterM m β → Std.IterStep (Std.IterM m β) β → Prop
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddCommMonoid β] →
          [inst_3 : ContinuousAdd β] →
            {R : Type u_5} →
              [inst_4 : Semiring R] →
                [inst_5 : Module R β] → [ContinuousConstSMul R β] → Module R (CompactlySupportedContinuousMap α β)
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.prop₂_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} (e : X ≅ Y), W₂ e.hom
-- Init.Prelude
SMul.mk : {M : Type u} → {α : Type v} → (M → α → α) → SMul M α
-- Aesop.Forward.State
Aesop.instInhabitedRuleState.default : Aesop.RuleState
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_inclusion : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  (h : S ≤ T) (s : ↥S), ↑((Subalgebra.inclusion h) s) = ↑s
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- **Alias** of `Metric.closedEBall_coe`.

---

Closed balls defined using the distance or the edistance coincide  -/
Metric.emetric_closedBall_nnreal : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : NNReal}, Metric.closedEBall x ↑ε = Metric.closedBall x ↑ε
-- Mathlib.Algebra.Homology.Augment
/-- Augmenting a truncated complex with the original object and morphism is isomorphic
(with components the identity) to the original complex.
 -/
CochainComplex.augmentTruncate : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (C : CochainComplex V ℕ) → (CochainComplex.truncate.obj C).augment (C.d 0 1) ⋯ ≅ C
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_toLinearEquiv : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ⇑↑e = ⇑e
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.ring : (α : Type u) → [Monoid α] → Ring (FreeAbelianGroup α)
-- Mathlib.AlgebraicTopology.DoldKan.Projections
/-- All the `Q q` coincide with `0` in degree 0.  -/
AlgebraicTopology.DoldKan.Q_f_0_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ), (AlgebraicTopology.DoldKan.Q q).f 0 = 0
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.whiskering_linearCoyoneda₂ : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C],
  (CategoryTheory.linearCoyoneda R C).comp
      ((CategoryTheory.Functor.whiskeringRight C (ModuleCat R) AddCommGrpCat).obj
        (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)) =
    CategoryTheory.preadditiveCoyoneda
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.tryCatch.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)) (h_2 : (ok : EStateM.Result ε σ α) → motive ok),
  (match EStateM.Result.error e s with
    | EStateM.Result.error e s => h_1 e s
    | ok => h_2 ok) =
    h_1 e s
-- Mathlib.Order.Std
/-- The `LT` instance of the order.  -/
Preorder.OfStdArgs.lt : {α : Type u_1} →
  (self : Preorder.OfStdArgs α) →
    let this := self.le;
    LT α
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.homeomorph_coe : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  [inst_1 : Topology.IsGeneratedBy X Y], ⇑Topology.IsGeneratedBy.homeomorph = ⇑Topology.WithGeneratedByTopology.equiv
-- Mathlib.Data.Set.Enumerate
Set.enumerate_eq_none : ∀ {α : Type u_1} (sel : Set α → Option α) {s : Set α} {n₁ n₂ : ℕ},
  Set.enumerate sel s n₁ = none → n₁ ≤ n₂ → Set.enumerate sel s n₂ = none
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below : {C : Type u} →
  {motive :
      {X Y : CategoryTheory.FreeMonoidalCategory C} →
        (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop} →
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      {a a_1 : X.Hom Y} → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop
-- Batteries.Data.List.Lemmas
List.foldlIdx_start : ∀ {α : Type u_1} {xs : List α} {α_1 : Sort u_2} {f : ℕ → α_1 → α → α_1} {i : α_1} {s : ℕ},
  List.foldlIdx f i xs s = List.foldlIdx (fun x => f (x + s)) i xs
-- Aesop.Rule.Name
Aesop.RuleName.mk.sizeOf_spec : ∀ (name : Lean.Name) (builder : Aesop.BuilderName) (phase : Aesop.PhaseName) (scope : Aesop.ScopeName) (hash : UInt64),
  sizeOf { name := name, builder := builder, phase := phase, scope := scope, hash := hash } =
    1 + sizeOf name + sizeOf builder + sizeOf phase + sizeOf scope + sizeOf hash
-- Lean.Parser.Basic
Lean.Parser.checkPrec : ℕ → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inr_desc_assoc : ∀ {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} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Z_1 : C} (h_1 : W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp inr (CategoryTheory.CategoryStruct.comp (hP.desc h k w) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv_succ : ∀ {n : ℕ} (m : Fin n), (finSuccEquiv n) m.succ = some m
-- Mathlib.Geometry.Manifold.Algebra.SMul
Diffeomorph.smul_symm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : Group G]
  [inst_12 : MulAction G M] {n : WithTop ℕ∞} [inst_13 : ContMDiffSMul I I' n G M] (g : G) (x : M),
  (Diffeomorph.smul I I' n g).symm x = g⁻¹ • x
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv_apply_fst : ∀ {m n : ℕ} {R : Type u_2} [inst : Ring R] (f : ↥(Polynomial.degreeLT R (m + n))),
  ↑((Polynomial.degreeLT.addLinearEquiv R m n) f).1 = ↑f %ₘ Polynomial.X ^ m
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofAlgebraAutOnUnits.eq_1 : ∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Rep.ofAlgebraAutOnUnits R S = Rep.ofMulDistribMulAction (S ≃ₐ[R] S) Sˣ
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.twoBlockTriangular_det' : ∀ {m : Type u_3} {R : Type v} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m] (M : Matrix m m R)
  (p : m → Prop) [inst_3 : DecidablePred p],
  (∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0) →
    M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i => ¬p i).det
-- Mathlib.Logic.Basic
not_iff_not : ∀ {a b : Prop}, (¬a ↔ ¬b) ↔ (a ↔ b)
-- Mathlib.Logic.Denumerable
Nat.Subtype.le_succ_of_forall_lt_le : ∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s] {x y : ↑s},
  (∀ z < x, z ≤ y) → x ≤ Nat.Subtype.succ y
-- Lean.Environment
/-- User-defined environment extensions are declared using the `initialize` command.
This command is just syntax sugar for the `init` attribute.
When we `import` lean modules, the vector stored at `envExtensionsRef` may increase in size because of
user-defined environment extensions. When this happens, we must adjust the size of the `env.extensions`.
This method is invoked when processing `import`s.
 -/
Lean.EnvExtension.ensureExtensionsArraySize : Array Lean.EnvExtensionState → IO (Array Lean.EnvExtensionState)
-- Init.Data.UInt.Lemmas
UInt32.toUSize_ofBitVec : ∀ {b : BitVec 32}, { toBitVec := b }.toUSize = { toBitVec := BitVec.setWidth System.Platform.numBits b }
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqIRType.beq : Lean.IR.IRType → Lean.IR.IRType → Bool
-- Mathlib.Algebra.Algebra.NonUnitalHom
MulHom.inverse.congr_simp : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f f_1 : M →ₙ* N) (e_f : f = f_1) (g g_1 : N → M)
  (e_g : g = g_1) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f),
  f.inverse g h₁ h₂ = f_1.inverse g_1 ⋯ ⋯
-- Mathlib.NumberTheory.MulChar.Basic
/-- If `a` is a unit and `n : ℕ`, then `(χ ^ n) a = (χ a) ^ n`.  -/
MulChar.pow_apply_coe : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R') (n : ℕ)
  (a : Rˣ), (χ ^ n) ↑a = χ ↑a ^ n
-- Mathlib.Algebra.CharP.Defs
CharP.ringChar_zero_iff_CharZero : ∀ (R : Type u_1) [inst : NonAssocRing R], ringChar R = 0 ↔ CharZero R
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_le_of_le_mul : ∀ {a b c : Ordinal.{u_4}}, a ≤ b * c → a / b ≤ c
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.lift_comp_of : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {f : Polynomial R} [inst_1 : CommRing S] {i : R →+* S} {a : S}
  (h : Polynomial.eval₂ i a f = 0), (AdjoinRoot.lift i a h).comp (AdjoinRoot.of f) = i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- A `CatCospanTransform F G F' G'` is a diagram
```
    F   G
  A ⥤ B ⥢ C
H₁|   |H₂ |H₃
  v   v   v
  A'⥤ B'⥢ C'
    F'  G'
```
with specified `CatCommSq`s expressing 2-commutativity of the squares.  -/
CategoryTheory.Limits.CatCospanTransform : {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] →
            CategoryTheory.Functor A B →
              CategoryTheory.Functor C B →
                {A' : Type u₄} →
                  {B' : Type u₅} →
                    {C' : Type u₆} →
                      [inst : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_3 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_4 : CategoryTheory.Category.{v₆, u₆} C'] →
                            CategoryTheory.Functor A' B' →
                              CategoryTheory.Functor C' B' →
                                Type
                                  (max
                                      (max
                                          (max
                                              (max (max (max (max (max (max (max (max u₁ u₂) u₃) u₄) u₅) u₆) v₁) v₂) v₃)
                                              v₄)
                                          v₅)
                                      v₆)
-- Mathlib.Data.Fin.Tuple.Basic
/-- Insert an element into a tuple at a given position. For `i = 0` see `Fin.cons`,
for `i = Fin.last n` see `Fin.snoc`. See also `Fin.succAboveCases` for a version elaborated
as an eliminator.  -/
Fin.insertNth : {n : ℕ} →
  {α : Fin (n + 1) → Sort u_1} → (i : Fin (n + 1)) → α i → ((j : Fin n) → α (i.succAbove j)) → (j : Fin (n + 1)) → α j
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_eq_zero_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b : α), lcm a b = 0 ↔ a = 0 ∨ b = 0
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Return `true` if `s` and `t` are equal up to swapping the `MVarId`s.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.isMVarSwap : Lean.Expr → Lean.Expr → Bool
-- Std.Http.Data.Status
Std.Http.Status.other.sizeOf_spec : ∀ (status : Std.Http.CustomStatus), sizeOf (Std.Http.Status.other status) = 1 + sizeOf status