mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vsub_iUnion₂ : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : VSub α β] (s : Set β)
  (t : (i : ι) → κ i → Set β), s -ᵥ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s -ᵥ t i j
-- Mathlib.Tactic.ProxyType
Mathlib.ProxyType.ProxyEquivConfig.mk.inj : ∀ {proxyName proxyEquivName : Lean.Name}
  {mkCtorProxyType : List (Lean.Expr × Lean.Name) → Lean.Elab.TermElabM (Lean.Expr × Lean.Term)}
  {mkProxyType :
    Array (Lean.Name × Lean.Expr × Lean.Term) →
      Lean.Elab.TermElabM (Lean.Expr × Array Lean.Term × Lean.TSyntax `tactic)}
  {proxyName_1 proxyEquivName_1 : Lean.Name}
  {mkCtorProxyType_1 : List (Lean.Expr × Lean.Name) → Lean.Elab.TermElabM (Lean.Expr × Lean.Term)}
  {mkProxyType_1 :
    Array (Lean.Name × Lean.Expr × Lean.Term) →
      Lean.Elab.TermElabM (Lean.Expr × Array Lean.Term × Lean.TSyntax `tactic)},
  { proxyName := proxyName, proxyEquivName := proxyEquivName, mkCtorProxyType := mkCtorProxyType,
        mkProxyType := mkProxyType } =
      { proxyName := proxyName_1, proxyEquivName := proxyEquivName_1, mkCtorProxyType := mkCtorProxyType_1,
        mkProxyType := mkProxyType_1 } →
    proxyName = proxyName_1 ∧
      proxyEquivName = proxyEquivName_1 ∧ mkCtorProxyType = mkCtorProxyType_1 ∧ mkProxyType = mkProxyType_1
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableOn.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E → F) (s : Set E),
  DifferentiableOn 𝕜 f s = ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Data.Analysis.Topology
Ctop.mk.injEq : ∀ {α : Type u_1} {σ : Type u_2} (f : σ → Set α) (top : α → σ) (top_mem : ∀ (x : α), x ∈ f (top x))
  (inter : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ)
  (inter_mem : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (inter a b x h))
  (inter_sub : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (inter a b x h) ⊆ f a ∩ f b) (f_1 : σ → Set α) (top_1 : α → σ)
  (top_mem_1 : ∀ (x : α), x ∈ f_1 (top_1 x)) (inter_1 : (a b : σ) → (x : α) → x ∈ f_1 a ∩ f_1 b → σ)
  (inter_mem_1 : ∀ (a b : σ) (x : α) (h : x ∈ f_1 a ∩ f_1 b), x ∈ f_1 (inter_1 a b x h))
  (inter_sub_1 : ∀ (a b : σ) (x : α) (h : x ∈ f_1 a ∩ f_1 b), f_1 (inter_1 a b x h) ⊆ f_1 a ∩ f_1 b),
  ({ f := f, top := top, top_mem := top_mem, inter := inter, inter_mem := inter_mem, inter_sub := inter_sub } =
      { f := f_1, top := top_1, top_mem := top_mem_1, inter := inter_1, inter_mem := inter_mem_1,
        inter_sub := inter_sub_1 }) =
    (f = f_1 ∧ top = top_1 ∧ inter ≍ inter_1)
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.vandermonde_transpose_mul_vandermonde : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v : Fin n → R) (i j : Fin n),
  ((Matrix.vandermonde v).transpose * Matrix.vandermonde v) i j = ∑ k, v k ^ (↑i + ↑j)
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.eComp.eq_1 : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] (X Y Z : C),
  CategoryTheory.eComp V X Y Z = CategoryTheory.EnrichedCategory.comp X Y Z
-- Init.Data.List.MinMaxOn
List.minOn?.fun_cases_unfolding : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) (motive : List α → Option α → Prop),
  motive [] none →
    (∀ (x : α) (xs : List α), motive (x :: xs) (some (List.foldl (minOn f) x xs))) →
      ∀ (l : List α), motive l (List.minOn? f l)
-- Lean.Linter.Init
/-- Linter sets are represented as a map from linter name to set name,
to make it easy to look up which sets to check for enabling a linter.
 -/
Lean.Linter.LinterSets : Type
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m m_1 : Std.DHashMap.Raw α β), m = m_1 → ∀ (a : α) [inst_3 : Inhabited (β a)], m.get! a = m_1.get! a
-- Mathlib.RingTheory.Noetherian.Basic
/-- A sequence `f` of submodules of a Noetherian module,
with `f (n+1)` disjoint from the supremum of `f 0`, ..., `f n`,
is eventually zero.  -/
IsNoetherian.disjoint_partialSups_eventually_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsNoetherian R M]
  (f : ℕ → Submodule R M), (∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))) → ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥
-- Mathlib.RingTheory.Localization.Away.Basic
selfZPow_pow_sub : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B] (a : R) (b : B) (m d : ℤ),
  selfZPow x B (m - d) * IsLocalization.mk' B a 1 = b ↔ selfZPow x B m * IsLocalization.mk' B a 1 = selfZPow x B d * b
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
/-- If `ω` is a closed `1`-form on an open convex set `s`, then it admits a primitive,
a version stated in terms of `fderiv`.  -/
Convex.exists_forall_hasFDerivAt_of_fderiv_symmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : NormedSpace ℝ F] {s : Set E} {ω : E → E →L[𝕜] F} [CompleteSpace F],
  Convex ℝ s →
    IsOpen s →
      DifferentiableOn ℝ ω s →
        (∀ a ∈ s, ∀ (x y : E), ((fderiv ℝ ω a) x) y = ((fderiv ℝ ω a) y) x) → ∃ f, ∀ a ∈ s, HasFDerivAt f (ω a) a
-- Mathlib.Data.Finsupp.Basic
Finsupp.equivMapDomain_trans' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [inst : Zero M] (f : α ≃ β) (g : β ≃ γ),
  Finsupp.equivMapDomain (f.trans g) = Finsupp.equivMapDomain g ∘ Finsupp.equivMapDomain f
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitStatus.notReady : Lean.Meta.Grind.SplitStatus
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `upperSemicontinuousAt_iff_frequently`. -/
UpperSemicontinuousAt.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {x : α},
  UpperSemicontinuousAt f x → ∀ (y : β), (∃ᶠ (x' : α) in nhds x, f x' ≥ y) → f x ≥ y
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.map_I : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [inst_3 : CategoryTheory.Category.{v₁, u₁} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v',
        max (max (u + 1) u₁) v₁}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)), (G.map F η).I = G.I
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `sum_apply`. -/
ProbabilityTheory.Kernel.finset_sum_apply : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) (x : α),
  (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instLERange : LE Lean.Lsp.Range
-- Mathlib.Order.BooleanAlgebra.Basic
Disjoint.sdiff_unique : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], Disjoint x z → z ≤ y → y ≤ x ⊔ z → y \ x = z
-- Lean.Meta.Sym.Offset
/-- Variant of `isOffset?` that first checks if `declName` is `Nat.succ` or `HAdd.hAdd`.  -/
Lean.Meta.Sym.isOffset?' : Lean.Name → Lean.Expr → OptionT Id Lean.Meta.Sym.Offset
-- Init.Meta.Defs
Lean.Syntax.instBEqTSyntax : {k : Lean.SyntaxNodeKinds} → BEq (Lean.TSyntax k)
-- Mathlib.Order.SuccPred.Tree
/-- The `SubRootedTree` rooted at a given node.
 -/
RootedTree.subtree : (t : RootedTree) → ↑t → SubRootedTree t
-- Init.Data.Array.Zip
Array.unzip_zip_right : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β}, bs.size ≤ as.size → (as.zip bs).unzip.2 = bs
-- Init.Data.Nat.Basic
Nat.add_one_pos : ∀ (n : ℕ), 0 < n + 1
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
/-- Additive convolution exists at `x` when the fiber sum is summable.  -/
DiscreteConvolution.AddConvolutionExistsAt : {M : Type u_1} →
  {S : Type u_2} →
    {E : Type u_3} →
      {E' : Type u_4} →
        {F : Type u_6} →
          [AddMonoid M] →
            [inst : CommSemiring S] →
              [inst_1 : AddCommMonoid E] →
                [inst_2 : AddCommMonoid E'] →
                  [inst_3 : AddCommMonoid F] →
                    [inst_4 : Module S E] →
                      [inst_5 : Module S E'] →
                        [inst_6 : Module S F] →
                          [TopologicalSpace F] → (E →ₗ[S] E' →ₗ[S] F) → (M → E) → (M → E') → M → Prop
-- Mathlib.Algebra.Module.Submodule.EqLocus
LinearMap.le_eqLocus : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f g : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M}, S ≤ f.eqLocus g ↔ Set.EqOn ⇑f ⇑g ↑S
-- Mathlib.GroupTheory.GroupAction.ConjAct
MulAut.conjNormal_symm_apply : ∀ {G : Type u_3} [inst : Group G] {H : Subgroup G} [inst_1 : H.Normal] (g : G) (h : ↥H),
  ↑((MulEquiv.symm (MulAut.conjNormal g)) h) = g⁻¹ * ↑h * g
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.map_star_eq_intCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Ring α] [inst_2 : StarRing α] {M : Matrix n n α} {d : ℤ},
  M.map star = ↑d ↔ M = ↑d
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.insertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {a : α} {b : β a},
  m.WF → (m.insertIfNew a b).WF
-- Mathlib.NumberTheory.Chebyshev
/-- Chebyshev's upper bound on the prime counting function  -/
Chebyshev.eventually_primeCounting_le : ∀ {ε : ℝ}, 0 < ε → ∀ᶠ (x : ℝ) in Filter.atTop, ↑⌊x⌋₊.primeCounting ≤ (Real.log 4 + ε) * x / Real.log x
-- Mathlib.Data.Finset.Lattice.Fold
/-- **Alias** of `Finset.apply_inf_eq_inf_comp_of_linearOrder`. -/
Finset.comp_inf_eq_inf_comp_of_is_total : ∀ {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderTop α] {s : Finset ι} {f : ι → α}
  [inst_2 : SemilatticeInf β] [inst_3 : OrderTop β] (g : α → β), Monotone g → g ⊤ = ⊤ → g (s.inf f) = s.inf (g ∘ f)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_restrictIndex_equiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {ι : Type w'}
  (e : ι ≃ E.I₀), (E.restrictIndex ⇑e).presieve₀ = E.presieve₀
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.nilRankAux_basis_indep : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ι' : Type u_6} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ι'] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ι'] [inst_9 : Module.Free R M] [inst_10 : Module.Finite R M] [Nontrivial R]
  (b : Module.Basis ι R L) (b' : Module.Basis ι' R L), φ.nilRankAux b = (φ.polyCharpoly b').natTrailingDegree
-- Mathlib.Order.WithBot
Equiv.withBotCongr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β),
  e.withBotCongr = { toFun := WithBot.map ⇑e, invFun := WithBot.map ⇑e.symm, left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Inhabited α] {k k' : α}
  {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! k' (Std.Internal.List.alterKey k f l) =
      if (k == k') = true then if (f (Std.Internal.List.getValueCast? k l)).isSome = true then k else default
      else Std.Internal.List.getKey! k' l
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
/-- The conversion from a Weierstrass curve to affine coordinates.  -/
WeierstrassCurve.toAffine : {R : Type r} → WeierstrassCurve R → WeierstrassCurve.Affine R
-- Mathlib.Topology.Piecewise
ite_inter_closure_compl_eq_of_inter_frontier_eq : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s s' t : Set α},
  s ∩ frontier t = s' ∩ frontier t → t.ite s s' ∩ closure tᶜ = s' ∩ closure tᶜ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂Iso_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : C ≌ A} {G : D ≌ B} (α : L' ⟶ G.functor.obj L) (α' : L ⟶ G.inverse.obj L')
  (β : R.comp G.functor ⟶ F.functor.comp R') (β' : R'.comp G.inverse ⟶ F.inverse.comp R)
  (hαα' : CategoryTheory.CategoryStruct.comp α (G.functor.map α') = G.counitIso.inv.app L')
  (hα'α : CategoryTheory.CategoryStruct.comp α' (G.inverse.map α) = G.unitIso.hom.app L)
  (hββ' :
    CategoryTheory.CategoryStruct.comp R.rightUnitor.hom
        (CategoryTheory.CategoryStruct.comp R.leftUnitor.inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom R)
            (F.functor.associator F.inverse R).hom)) =
      CategoryTheory.CategoryStruct.comp (R.whiskerLeft G.unitIso.hom)
        (CategoryTheory.CategoryStruct.comp (R.associator G.functor G.inverse).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G.inverse)
            (CategoryTheory.CategoryStruct.comp (F.functor.associator R' G.inverse).hom (F.functor.whiskerLeft β')))))
  (hβ'β :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β' G.functor)
        (CategoryTheory.CategoryStruct.comp (F.inverse.associator R G.functor).hom
          (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft β)
            (CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor R').inv
              (CategoryTheory.Functor.whiskerRight F.counitIso.hom R')))) =
      CategoryTheory.CategoryStruct.comp (R'.associator G.inverse G.functor).hom
        (CategoryTheory.CategoryStruct.comp (R'.whiskerLeft G.counitIso.hom)
          (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv))),
  (CategoryTheory.StructuredArrow.map₂Iso α α' β β' hαα' hα'α hββ' hβ'β).counitIso =
    CategoryTheory.StructuredArrow.map₂CompMap₂Iso α β α' β' ≪≫
      CategoryTheory.StructuredArrow.map₂Congr (CategoryTheory.CategoryStruct.comp α (G.functor.map α'))
          (CategoryTheory.CategoryStruct.comp (R'.associator G.inverse G.functor).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β' G.functor)
              (CategoryTheory.CategoryStruct.comp (F.inverse.associator R G.functor).hom
                (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft β)
                  (F.inverse.associator F.functor R').inv))))
          F.counitIso G.counitIso (CategoryTheory.CategoryStruct.id L')
          (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv) ⋯ ⋯ ≪≫
        CategoryTheory.StructuredArrow.map₂IdIso L' (CategoryTheory.CategoryStruct.id L')
          (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv) ⋯ ⋯
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instAddOffset : Add Std.Time.Millisecond.Offset
-- Mathlib.Algebra.Group.Defs
AddGroup.toSubtractionMonoid.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  AddGroup.toSubtractionMonoid =
    { toSubNegMonoid := inst.toSubNegMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mrange_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.mrange (MonoidHom.inr M N) = ⊥.prod ⊤
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.mk.sizeOf_spec : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : SizeOf R] [inst_4 : SizeOf S] [inst_5 : SizeOf ι] [inst_6 : SizeOf σ]
  (toGenerators : Algebra.Generators R S ι) (relation : σ → toGenerators.Ring)
  (span_range_relation_eq_ker : Ideal.span (Set.range relation) = toGenerators.ker),
  sizeOf
      { toGenerators := toGenerators, relation := relation, span_range_relation_eq_ker := span_range_relation_eq_ker } =
    1 + sizeOf toGenerators + sizeOf span_range_relation_eq_ker
-- Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
SimpleGraph.turanDensity_eq_csInf : ∀ {W : Type u_1} (H : SimpleGraph W),
  H.turanDensity = sInf {x | ∃ n ∈ Set.Ici 2, ↑(SimpleGraph.extremalNumber n H) / ↑(n.choose 2) = x}
-- Mathlib.Data.Set.Basic
Function.Injective.nonempty_apply_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Set α → Set β},
  Function.Injective f → f ∅ = ∅ → ∀ {s : Set α}, (f s).Nonempty ↔ s.Nonempty
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.instDivSubtypeMem : {K : Type u} → [inst : DivisionRing K] → (s : Subfield K) → Div ↥s
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.falsum : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.unbox.inj : ∀ {x x_1 : Lean.IR.VarId}, Lean.IR.Expr.unbox x = Lean.IR.Expr.unbox x_1 → x = x_1
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_refl : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] (f : α → E) (l : Filter α), f =O[l] f
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.instNegSubtypeMem : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → (I : TwoSidedIdeal R) → Neg ↥I
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.coneBack_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)}
  {t₁ t₂ : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)} {f : t₁ ⟶ t₂},
  (CategoryTheory.WithTerminal.coneBack✝.map f).hom = CategoryTheory.Over.homMk f.hom ⋯
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.uSquash_eq_uSquashOrUnit : ∀ {α : Type v} [inst : Std.Internal.Small α], Std.Internal.USquash α = Std.Internal.USquashOrUnit α
-- Lean.Parser.Command
Lean.Parser.Term.open.formatter : Lean.PrettyPrinter.Formatter
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swap.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → ℕ → Sort u_2) →
    (x : List α) →
      (x_1 x_2 : ℕ) →
        ((x x_3 : ℕ) → motive [] x x_3) →
          ((a : α) → (xs : List α) → motive (a :: xs) 0 0) →
            ((a : α) → (xs : List α) → (i : ℕ) → motive (a :: xs) 0 i.succ) →
              ((a : α) → (xs : List α) → (i : ℕ) → motive (a :: xs) i.succ 0) →
                ((a : α) → (xs : List α) → (i j : ℕ) → motive (a :: xs) i.succ j.succ) → motive x x_1 x_2
-- Mathlib.Data.Nat.Basic
Nat.leRecOn_surjective : ∀ {C : ℕ → Sort u_1} {n m : ℕ} (hnm : n ≤ m) (next : {k : ℕ} → C k → C (k + 1)),
  (∀ (n : ℕ), Function.Surjective next) → Function.Surjective (Nat.leRecOn hnm fun {k} => next)
-- Mathlib.Condensed.Light.AB
LightCondensed.instIsGrothendieckAbelianLightCondMod : ∀ {R : Type u} [inst : Ring R], CategoryTheory.IsGrothendieckAbelian.{u, u + 1, u + 1} (LightCondMod R)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.String.0.String.reduceBinPred : Lean.Name → ℕ → (String → String → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.nearestPtInd.eq_2 : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  (e : ℕ → α) (N : ℕ),
  MeasureTheory.SimpleFunc.nearestPtInd e N.succ =
    MeasureTheory.SimpleFunc.piecewise (⋂ k, ⋂ (_ : k ≤ N), {x | edist (e (N + 1)) x < edist (e k) x}) ⋯
      (MeasureTheory.SimpleFunc.const α (N + 1)) (MeasureTheory.SimpleFunc.nearestPtInd e N)
-- Mathlib.Data.Finset.NAry
/-- Symmetric statement to `Finset.image_image₂_distrib_right`.  -/
Finset.image_image₂_right_comm : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq β']
  [inst_1 : DecidableEq γ] {s : Finset α} {t : Finset β} [inst_2 : DecidableEq δ] {f : α → β' → γ} {g : β → β'}
  {f' : α → β → δ} {g' : δ → γ},
  (∀ (a : α) (b : β), f a (g b) = g' (f' a b)) →
    Finset.image₂ f s (Finset.image g t) = Finset.image g' (Finset.image₂ f' s t)
-- Plausible.Shrinkable
Plausible.USize.shrinkable : Plausible.Shrinkable USize
-- Init.Data.Array.Count
Array.countP_map : ∀ {α : Type u_2} {β : Type u_1} {p : β → Bool} {f : α → β} {xs : Array α},
  Array.countP p (Array.map f xs) = Array.countP (p ∘ f) xs
-- Mathlib.RingTheory.Extension.Basic
/-- The base change of an `R`-extension of `S` to `T` gives a `T`-extension of `T ⊗[R] S`.  -/
Algebra.Extension.baseChange : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {T : Type u_1} →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] → Algebra.Extension R S → Algebra.Extension T (TensorProduct R T S)
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_inv_id_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.CategoryStruct.comp s.toKaroubiNondegComplexIsoN₁.hom.f s.toKaroubiNondegComplexIsoN₁.inv.f =
    CategoryTheory.CategoryStruct.id s.nondegComplex
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.toHomeomorph_eq_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (f : M ≃ₜ+ N), f.toHomeomorph = ↑f
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Icc_right_eq_Icc_add_one : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] {a b : α}, a ≤ b + 1 → insert (b + 1) (Finset.Icc a b) = Finset.Icc a (b + 1)
-- Mathlib.Algebra.Group.Prod
AddHom.fst.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : Add M] [inst_1 : Add N], AddHom.fst M N = { toFun := Prod.fst, map_add' := ⋯ }
-- Mathlib.Control.Functor.Multivariate
MvFunctor.mk : {n : ℕ} → {F : TypeVec.{u_2} n → Type u_1} → ({α β : TypeVec.{u_2} n} → α.Arrow β → F α → F β) → MvFunctor F
-- Mathlib.Topology.Order.Compact
IsCompact.exists_isMaxOn_mem_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIciTopology α] {f : β → α} {s t : Set β} {z : β},
  IsCompact t → ContinuousOn f t → z ∈ t → (∀ z' ∈ t \ s, f z' < f z) → ∃ x ∈ s, IsMaxOn f t x
-- Lean.Meta.Tactic.Grind.MatchCond
/-- Constructs a proof for a satisfied `match`-expression condition.  -/
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.mkMatchCondProof? : Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)