mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.trivializationOfSMulDisjoint.eq_1 : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : Topology.IsQuotientMap f) [inst_4 : ContinuousConstSMul G E]
  (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) [inst_5 : TopologicalSpace G]
  [inst_6 : DiscreteTopology G] (U : Set E) (open_U : IsOpen U)
  (disjoint : ∀ (g : G), ((fun x => g • x) '' U ∩ U).Nonempty → g = 1),
  hf.trivializationOfSMulDisjoint hfG U open_U disjoint =
    IsOpen.trivializationDiscrete (fun g => (fun x => g • x) ⁻¹' U) (f '' U) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
Lex.instIsLeftCancelMulZero : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [IsLeftCancelMulZero α], IsLeftCancelMulZero (Lex α)
-- Init.Core
/-- `continue s` means that `continue` was called, meaning that we should continue
to the next iteration of the containing loop  -/
DoResultPRBC.continue : {α β σ : Type u} → σ → DoResultPRBC α β σ
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- The identity edge on a point, composed with itself, gives the identity.  -/
SSet.Edge.CompStruct.idCompId : {X : SSet} → (x : X.obj (Opposite.op { len := 0 })) → (SSet.Edge.id x).CompStruct (SSet.Edge.id x) (SSet.Edge.id x)
-- Mathlib.Algebra.GCDMonoid.Basic
instNonemptyNormalizationMonoid : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [NormalizationMonoid α], Nonempty (NormalizationMonoid α)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- A dependent version of `AddSubgroup.iSup_induction`.  -/
AddSubgroup.iSup_induction' : ∀ {G : Type u_2} [inst : AddGroup G] {ι : Sort u_5} (S : ι → AddSubgroup G) {C : (x : G) → x ∈ ⨆ i, S i → Prop},
  (∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯) →
    C 0 ⋯ →
      (∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) ⋯) →
        ∀ {x : G} (hx : x ∈ ⨆ i, S i), C x hx
-- Mathlib.Data.PNat.Notation
/-- `ℕ+` is the type of positive natural numbers. It is defined as a subtype,
and the VM representation of `ℕ+` is the same as `ℕ` because the proof
is not stored.  -/
«termℕ+» : Lean.ParserDescr
-- Mathlib.Analysis.Normed.MulAction
/-- Right multiplication is bounded.  -/
NonUnitalSeminormedRing.isBoundedSMulOpposite : ∀ {α : Type u_1} [inst : NonUnitalSeminormedRing α], IsBoundedSMul αᵐᵒᵖ α
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- The localization of an `R`-submodule of `M` at `p` viewed as an `Rₚ`-submodule of `Mₚ`.  -/
Submodule.localized : {R : Type u_1} →
  {M : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → (p : Submonoid R) → Submodule R M → Submodule (Localization p) (LocalizedModule p M)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compQuasiMeasurePreserving_congr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace γ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α → β} (g : β →ₘ[ν] γ)
  (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν) {f' : α → β} (hf' : Measurable f') (h : f =ᵐ[μ] f'),
  g.compQuasiMeasurePreserving f hf = g.compQuasiMeasurePreserving f' ⋯
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.map_map : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (N : AddSubgroup G) [nN : N.Normal]
  {I : Type u_5} [inst_2 : AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [inst_3 : M.Normal] [inst_4 : O.Normal]
  (f : G →+ H) (g : H →+ I) (hf : N ≤ AddSubgroup.comap f M) (hg : M ≤ AddSubgroup.comap g O)
  (hgf : optParam (N ≤ AddSubgroup.comap (g.comp f) O) ⋯) (x : G ⧸ N),
  (QuotientAddGroup.map M O g hg) ((QuotientAddGroup.map N M f hf) x) = (QuotientAddGroup.map N O (g.comp f) hgf) x
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
set_smul_sphere_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {s : Set 𝕜}, 0 ∉ s → ∀ (r : ℝ), s • Metric.sphere 0 r = (fun x => ‖x‖) ⁻¹' (fun x => ‖x‖ * r) '' s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.union_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₂.Equiv t₃ → (t₁ ∪ t₂).Equiv (t₁ ∪ t₃)
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.neg_apply : ∀ {ι : Type u_1} {I₀ : WithTop (BoxIntegral.Box ι)} {M : Type u_4} [inst : AddCommGroup M]
  (f : BoxIntegral.BoxAdditiveMap ι M I₀) (J : BoxIntegral.Box ι), (-f) J = -f J
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPullback.iso_inv_fst : ∀ {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 Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G]
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [inst_4 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).inv
      (G.map (CategoryTheory.Limits.pullback.fst f g)) =
    CategoryTheory.Limits.pullback.fst (G.map f) (G.map g)
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.List.toUnboundedSlice.eq_1 : ∀ {α : Type u} (as : List α) (start : ℕ),
  as.toUnboundedSlice start = { internalRepresentation := { list := List.drop start as, stop := none } }
-- Mathlib.GroupTheory.SpecificGroups.Alternating
/-- The group isomorphism between `alternatingGroup`s induced by the given `Equiv`.  -/
Equiv.altCongrHom : {α : Type u_1} →
  [inst : Fintype α] →
    [inst_1 : DecidableEq α] →
      {β : Type u_2} →
        [inst_2 : Fintype β] → [inst_3 : DecidableEq β] → α ≃ β → ↥(alternatingGroup α) ≃* ↥(alternatingGroup β)
-- Mathlib.Order.Category.Lat
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
Lat.Hom.Simps.hom : (X Y : Lat) → X.Hom Y → LatticeHom ↑X ↑Y
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerSkip_flatMapM_pure : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α Id β] [inst_4 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)} {it₁ it₁' : Std.Iter β},
  it₁.IsPlausibleStep (Std.IterStep.skip it₁') →
    (Std.Iter.flatMapAfterM f it₁ none).IsPlausibleStep (Std.IterStep.skip (Std.Iter.flatMapAfterM f it₁' none))
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.ofLE_val : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} [inst_2 : OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J} (e : d.Extension val₀ j)
  {i : J} (hij : i ≤ j),
  (e.ofLE hij).val = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij).op)) e.val
-- Mathlib.Topology.NhdsKer
nhdsKer_singleton_eq_ker_nhds : ∀ {X : Type u_2} [inst : TopologicalSpace X] (x : X), nhdsKer {x} = (nhds x).ker
-- Init.Data.UInt.Bitwise
USize.toBitVec_not : ∀ {a : USize}, (~~~a).toBitVec = ~~~a.toBitVec
-- Mathlib.Tactic.Linarith.Verification
/-- `mkLTZeroProof coeffs pfs` takes a list of proofs of the form `tᵢ Rᵢ 0`,
paired with coefficients `cᵢ`.
It produces a proof that `∑cᵢ * tᵢ R 0`, where `R` is as strong as possible.
 -/
Mathlib.Tactic.Linarith.mkLTZeroProof : List (Lean.Expr × ℕ) → Lean.MetaM Lean.Expr
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpoint.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (term? : Option Lean.Term) (fixpointType : Lean.Elab.PartialFixpointType),
  sizeOf { ref := ref, term? := term?, fixpointType := fixpointType } =
    1 + sizeOf ref + sizeOf term? + sizeOf fixpointType
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
/-- Derivative of `z ↦ (denom g z) ^ k`:
$\frac{d}{dz}[(cz+d)^k] = k \cdot c \cdot (cz+d)^{k-1}$.  -/
UpperHalfPlane.deriv_denom_zpow : ∀ (g : GL (Fin 2) ℝ) (k : ℤ) (τ : UpperHalfPlane),
  deriv (fun z => UpperHalfPlane.denom g z ^ k) ↑τ = ↑k * ↑(↑g 1 0) * UpperHalfPlane.denom g ↑τ ^ (k - 1)
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.cond.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.vertices_toPath : ∀ {V : Type u_1} [inst : Quiver V] {i j : V} (e : i ⟶ j), e.toPath.vertices = [i, j]
-- Init.Data.Iterators.Lemmas.Consumers.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Collect.0.Std.Iter.atIdxSlow?.match_1.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    (it : Std.Iter β) →
      (motive :
          (n : ℕ) →
            ((a' : Std.Iter β) →
                (b' : ℕ) →
                  InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                      (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, n⟩ →
                    Option β) →
              Sort u_2) →
        (n : ℕ) →
          (recur :
              (a' : Std.Iter β) →
                (b' : ℕ) →
                  InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                      (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, n⟩ →
                    Option β) →
            ((recur :
                  (a' : Std.Iter β) →
                    (b' : ℕ) →
                      InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                          (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, 0⟩ →
                        Option β) →
                motive 0 recur) →
              ((k : ℕ) →
                  (recur :
                      (a' : Std.Iter β) →
                        (b' : ℕ) →
                          InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                              (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, k + 1⟩ →
                            Option β) →
                    motive k.succ recur) →
                motive n recur
-- Mathlib.Algebra.Group.Units.Basic
divp_eq_one_iff_eq : ∀ {α : Type u} [inst : Monoid α] {a : α} {u : αˣ}, a /ₚ u = 1 ↔ a = ↑u
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.whiskerLeft_def : ∀ (R : Type u) [inst : CommRing R] (X x x_1 : CoalgCat R) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f =
    CoalgCat.ofHom (CoalgHom.lTensor (↑X.toModuleCat) f.toCoalgHom')
-- Init.Data.Repr
instReprAtomNat : ReprAtom ℕ
-- Mathlib.GroupTheory.GroupAction.OfQuotient
MulAction.coe_quotient_smul_fixedPoints : ∀ {G : Type u_1} [inst : Group G] {A : Type u_2} [inst_1 : MulAction G A] {H : Subgroup G} [inst_2 : H.Normal] (g : G)
  (a : ↑(MulAction.fixedPoints (↥H) A)), ↑g • a = g • a
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.Nonnegg.eq_3 : ∀ (c d a b : ℕ), Zsqrtd.Nonnegg c d (Int.negSucc a) (Int.ofNat b) = Zsqrtd.SqLe (a + 1) d b c
-- Mathlib.Topology.Order.Compact
Pi.compact_Icc_space' : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder β] [inst_1 : TopologicalSpace β] [CompactIccSpace β],
  CompactIccSpace (α → β)
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.isCompl_I_F : ∀ {P : Type u_2} [inst : Preorder P] (self : Order.Ideal.PrimePair P), IsCompl ↑self.I ↑self.F
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.get_in_bound : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} (s : aig.RefVec len) (idx : ℕ)
  (alt : aig.Ref) (hidx : idx < len), s.getD idx alt = s.get idx hidx
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover_diagonal : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  [inst : ∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)],
  (∀ (i : 𝒰.toPreZeroHypercover.1), Q.diagonal (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i)) → P.diagonal f
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- The map `a ↦ quasispectrum ℝ≥0 a` is upper hemicontinuous.  -/
upperHemicontinuous_quasispectrum_nnreal : ∀ (A : Type u_2) [inst : NonUnitalNormedRing A] [inst_1 : NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A]
  [CompleteSpace A], UpperHemicontinuous (quasispectrum NNReal)
-- Mathlib.CategoryTheory.MorphismProperty.Local
/-- **Alias** of `CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover`. -/
CategoryTheory.MorphismProperty.iff_of_zeroHypercover_source : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X),
  P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_one_apply_prime_pow : ∀ {p i : ℕ}, Nat.Prime p → (ArithmeticFunction.sigma 1) (p ^ i) = ∑ k ∈ Finset.range (i + 1), p ^ k
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.union_mem : ∀ {α : Type u_1} {C : Set (Set α)}, MeasureTheory.IsSetRing C → ∀ ⦃s t : Set α⦄, s ∈ C → t ∈ C → s ∪ t ∈ C
-- Mathlib.Algebra.Ring.Shrink
Shrink.instCommSemiring : {α : Type u_1} → [inst : Small.{v, u_1} α] → [CommSemiring α] → CommSemiring (Shrink.{v, u_1} α)
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.surjective_mk : ∀ {α : Type u_2} {rels : FreeAddMonoid α → FreeAddMonoid α → Prop}, Function.Surjective ⇑(PresentedAddMonoid.mk rels)
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.ofLinearEquiv_inv : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f : M ≃ₗ[R] M),
  LinearMap.GeneralLinearGroup.ofLinearEquiv f⁻¹ = (LinearMap.GeneralLinearGroup.ofLinearEquiv f)⁻¹
-- Mathlib.MeasureTheory.Measure.AEMeasurable
MeasureTheory.Measure.restrict_map_of_aemeasurable : ∀ {α : Type u_2} {δ : Type u_5} {m0 : MeasurableSpace α} [inst : MeasurableSpace δ] {μ : MeasureTheory.Measure α}
  {f : α → δ},
  AEMeasurable f μ →
    ∀ {s : Set δ},
      MeasurableSet s → (MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))
-- Mathlib.Order.Hom.Lattice
LatticeHomClass.toInfHomClass : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Lattice α} {inst_1 : Lattice β} {inst_2 : FunLike F α β}
  [self : LatticeHomClass F α β], InfHomClass F α β
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- Spec is a full functor.  -/
AlgebraicGeometry.instFullOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace : AlgebraicGeometry.Spec.toLocallyRingedSpace.Full
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.mem_support_filter_iff : ∀ {α : Type u_1} {p : PMF α} {s : Set α} (h : ∃ a ∈ s, a ∈ p.support) {a : α},
  a ∈ (p.filter s h).support ↔ a ∈ s ∧ a ∈ p.support
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_insertMany!_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List (α × β)},
      List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
        (∀ (a : α), Std.DTreeMap.Internal.Impl.contains a t = true → (List.map Prod.fst l).contains a = false) →
          (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).size = t.size + l.length
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
String.Slice.Pattern.Model.ForwardSliceSearcher.lawfulToForwardSearcherModel : ∀ {pat : String.Slice}, pat.isEmpty = false → String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat
-- Mathlib.Topology.Separation.Basic
disjoint_nhds_nhds_iff_not_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {x y : X}, Disjoint (nhds x) (nhds y) ↔ ¬Inseparable x y
-- Lean.Meta.Basic
Lean.Meta.Context.mk.sizeOf_spec : ∀ (keyedConfig : Lean.Meta.ConfigWithKey) (trackZetaDelta : Bool) (zetaDeltaSet : Lean.FVarIdSet)
  (lctx : Lean.LocalContext) (localInstances : Lean.LocalInstances) (defEqCtx? : Option Lean.Meta.DefEqContext)
  (synthPendingDepth : ℕ) (canUnfold? : Option (Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool))
  (univApprox inTypeClassResolution cacheInferType : Bool),
  sizeOf
      { keyedConfig := keyedConfig, trackZetaDelta := trackZetaDelta, zetaDeltaSet := zetaDeltaSet, lctx := lctx,
        localInstances := localInstances, defEqCtx? := defEqCtx?, synthPendingDepth := synthPendingDepth,
        canUnfold? := canUnfold?, univApprox := univApprox, inTypeClassResolution := inTypeClassResolution,
        cacheInferType := cacheInferType } =
    1 + sizeOf keyedConfig + sizeOf trackZetaDelta + sizeOf zetaDeltaSet + sizeOf lctx + sizeOf localInstances +
                sizeOf defEqCtx? +
              sizeOf synthPendingDepth +
            sizeOf canUnfold? +
          sizeOf univApprox +
        sizeOf inTypeClassResolution +
      sizeOf cacheInferType
-- Mathlib.Condensed.Light.Sequence
/-- Given a surjective map of light profinite spaces `T ⟶ S ⊗ ℕ∪{∞}`,
construct a (non-cartesian) commutative square
```
T' -> S' ⨯ OnePoint X
|         |
v         v
T  -> S  ⨯ OnePoint X
```
where every map is epi. The map `(π ≫ Prod.snd) ⁻¹' ∞ ⟶ T' ⟶ S' ⨯ ℕ∪{∞}` is split epi and
`cover` is epi. `S'` is constructed as the pullback of all the fibres.  -/
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.aux : ∀ {S T : LightProfinite} (π : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj S LightProfinite.NatUnionInfty)
  [CategoryTheory.Epi π],
  ∃ S' T' y' π' g',
    CategoryTheory.Epi π' ∧
      CategoryTheory.Epi y' ∧
        CategoryTheory.CategoryStruct.comp π'
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight y' LightProfinite.NatUnionInfty) =
            CategoryTheory.CategoryStruct.comp g' π ∧
          CategoryTheory.IsSplitEpi
              (CategoryTheory.CategoryStruct.comp
                (InternalProjectivityProof.LightProfinite.fibreIncl✝ OnePoint.infty
                  (CategoryTheory.CategoryStruct.comp π'
                    (CategoryTheory.SemiCartesianMonoidalCategory.snd S' LightProfinite.NatUnionInfty)))
                (CategoryTheory.CategoryStruct.comp π'
                  (CategoryTheory.SemiCartesianMonoidalCategory.fst S' LightProfinite.NatUnionInfty))) ∧
            CategoryTheory.Epi (InternalProjectivityProof.cover✝ π')
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.neg.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} [inst_1 : SizeOf J]
  (a : CommRingCat.Colimits.Prequotient F), sizeOf a.neg = 1 + sizeOf a
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.IsUniversal.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) (v : V), G.IsUniversal v = ∀ ⦃w : V⦄, v ≠ w → G.Adj v w
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- The subgroup generated by an element of a group equals the set of
integer powers of the element, such that each power is a unique element.
This is the stronger version of `Subgroup.mem_closure_singleton`.  -/
Subgroup.mem_closure_singleton_iff_existsUnique_zpow : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G},
  a ≠ 1 → (b ∈ Subgroup.closure {a} ↔ ∃! k, a ^ k = b)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_range : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁), (MvPolynomial.aeval f).range = Algebra.adjoin R (Set.range f)
-- Mathlib.Util.Qq
/-- Returns the integer literal `n`.

This is a Qq version of `Lean.mkIntLit`.  -/
Qq.mkIntLitQ : ℤ → Q(ℤ)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.Measure.coe_completion : ∀ {α : Type u_2} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α), ⇑μ.completion = ⇑μ
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- If a preadditive category has all cokernels, then it also has all coequalizers.  -/
CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasCokernels C], CategoryTheory.Limits.HasCoequalizers C
-- Init.Data.Bool
Bool.eq_and_not_self : ∀ {a b : Bool}, b = (a && !b) ↔ (!a) = true ∧ (!b) = true
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- A group object in a Cartesian monoidal category.  -/
CategoryTheory.Grp : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.CartesianMonoidalCategory C] → Type (max u₁ v₁)
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.natCast_pow : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (x k : ℕ), ↑(x ^ k) = ↑x ^ k
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_min?_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → t.min?.isSome = true
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.not_isG2_iff_isNotG2 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [P.IsCrystallographic]
  [P.IsReduced] [P.IsIrreducible] [Finite ι] [CharZero R] [IsDomain R], ¬P.IsG2 ↔ P.IsNotG2
-- Mathlib.Order.Heyting.Hom
OrderIsoClass.toBiheytingHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : BiheytingAlgebra α]
  {x : BiheytingAlgebra β} [OrderIsoClass F α β], BiheytingHomClass F α β
-- Mathlib.Data.Nat.Factorization.LCM
Nat.factorizationLCRight_zero_left : ∀ (b : ℕ), Nat.factorizationLCMRight 0 b = 1
-- Std.Time.Format.Modifier
Std.Time.Fraction.truncated.inj : ∀ {digits digits_1 : ℕ}, Std.Time.Fraction.truncated digits = Std.Time.Fraction.truncated digits_1 → digits = digits_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ)
  (acc lhs rhs : aig.RefVec w) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go aig lhs rhs curr acc).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go aig lhs rhs curr acc).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Order.CompleteLattice.Basic
iInf₂_le_of_le : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (i : ι)
  (j : κ i), f i j ≤ a → ⨅ i, ⨅ j, f i j ≤ a
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.Result.mk : {α : Type} →
  Option ProofWidgets.Html → ProofWidgets.Html → α → ProofWidgets.Html → Mathlib.Tactic.ClickSuggestions.Result α
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map_app_f : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C]
  {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (j : J),
  ((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map f).app j).f = f.f.app j
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.geometricallyIrreducible_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.GeometricallyIrreducible f ↔ AlgebraicGeometry.geometrically (fun x => IrreducibleSpace ↥x) f
-- Init.Data.Nat.Basic
/-- A recursor for `Nat` that uses the notations `0` for `Nat.zero` and `n + 1` for `Nat.succ`.

It is otherwise identical to the default recursor `Nat.rec`. It is used by the `induction` tactic
by default for `Nat`.
 -/
Nat.recAux : {motive : ℕ → Sort u} → motive 0 → ((n : ℕ) → motive n → motive (n + 1)) → (t : ℕ) → motive t