mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
EisensteinSeries.E2_slash_action : ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  SlashAction.map 2 γ EisensteinSeries.E2 = EisensteinSeries.E2 - (1 / (2 * riemannZeta 2)) • EisensteinSeries.D2 γ
-- Mathlib.Order.Category.BddOrd
BddOrd.hasForgetToBipointed : CategoryTheory.HasForget₂ BddOrd Bipointed
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.ofHom : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X S : C} → (X ⟶ S) → CategoryTheory.OverClass X S
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_zpow : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : DivisionRing R]
  (v : Valuation R Γ₀) (x : WithVal v) (z : ℤ), (x ^ z).ofVal = x.ofVal ^ z
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosed : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] {s : Set α} [Topology.IsScott α Set.univ],
  IsClosed s ↔ IsLowerSet s ∧ DirSupClosed s
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.indep_biSup_limsup : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {p : Set ι → Prop} {f : Filter ι},
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iIndep s μ →
      (∀ (t : Set ι), p t → tᶜ ∈ f) → ∀ {t : Set ι}, p t → ProbabilityTheory.Indep (⨆ n ∈ t, s n) (Filter.limsup s f) μ
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_smul_mul_eq_smul_mul_smul : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M N : Submodule R A)
  (x y : R), (x * y) • (M * N) = x • M * y • N
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestMatchAt_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat pos₁ pos₂ ↔
    ∃ (h : pos₁ ≤ pos₂), String.Slice.Pattern.Model.IsLongestMatch pat (pos₁.sliceFrom pos₂ h)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_lt_card_verts : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (v : V),
  G.degree v < Fintype.card V
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_counitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D],
  (CategoryTheory.Monoidal.comonFunctorCategoryEquivalence C D).counitIso =
    CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toArray_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  {f : (a : α) → β a → γ a},
  (Std.DTreeMap.Internal.Impl.map f t).toArray = Array.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toArray
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
hasSum_pi_single : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : DecidableEq β] (b : β)
  (a : α), HasSum (Pi.single b a) a
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.opEquiv_apply : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A), Subalgebra.opEquiv S = S.op
-- Init.Data.Nat.Div.Lemmas
Nat.succ_div : ∀ {a b : ℕ}, (a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0
-- Mathlib.RingTheory.Perfection
Perfection.coeff_iterate_frobenius : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] (f : Perfection R p)
  (n m : ℕ), (Perfection.coeff R p (n + m)) ((⇑(frobenius (Perfection R p) p))^[m] f) = (Perfection.coeff R p n) f
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
  {fallback : β a},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCastD a (Std.Internal.List.eraseKey k l) fallback =
      if (k == a) = true then fallback else Std.Internal.List.getValueCastD a l fallback
-- Lean.Elab.PreDefinition.Structural.Eqns
_private.Lean.Elab.PreDefinition.Structural.Eqns.0.Lean.Elab.Structural.mkProof.go : Lean.Name → Lean.MVarId → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEq_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') {i'' j'' : E.I₀} (hii'' : i' = i'') (hjj'' : j' = j'')
  (k : E.I₁ i j),
  (CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii'' hjj'')
      ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k) =
    (CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) k
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_sup_not : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α},
  (Filter.blimsup u f p ⊔ Filter.blimsup u f fun x => ¬p x) = Filter.limsup u f
-- Init.Data.Array.Find
Array.isNone_findFinIdx? : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, (Array.findFinIdx? p xs).isNone = xs.all fun x => decide ¬p x = true
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim : ∀ {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (hm : m ≤ m0) {f : α → E},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ) →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0) →
      MeasureTheory.FinStronglyMeasurable f (μ.trim hm) → f =ᵐ[μ] 0
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.transitionMap_map_one : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {m n : ℕ} (hmn : m ≤ n), (AdicCompletion.transitionMap I R hmn) 1 = 1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.jp.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl decl_1 : Lean.Compiler.LCNF.FunDecl pu),
  (Lean.Compiler.LCNF.CodeDecl.jp decl = Lean.Compiler.LCNF.CodeDecl.jp decl_1) = (decl = decl_1)
-- Std.Data.HashMap.Lemmas
_private.Std.Data.HashMap.Lemmas.0.Std.HashMap.ext : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m m' : Std.HashMap α β}, m.inner = m'.inner → m = m'
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.hasPullbacksOfInclusions : ∀ {P : TopCat → Prop} [inst : CompHausLike.HasExplicitFiniteCoproducts P],
  (∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
      Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) → CompHausLike.HasExplicitPullback f g) →
    CompHausLike.HasExplicitPullbacksOfInclusions P
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : TopologicalSpace α} {inst_1 : Preorder α} {inst_2 : TopologicalSpace β}
  {inst_3 : Preorder β} {toContinuousOrderHom : α →Co β}
  {exists_map_eq_of_map_le' :
    ∀ ⦃a : α⦄ ⦃b : β⦄, toContinuousOrderHom.toFun a ≤ b → ∃ c, a ≤ c ∧ toContinuousOrderHom.toFun c = b}
  {toContinuousOrderHom_1 : α →Co β}
  {exists_map_eq_of_map_le'_1 :
    ∀ ⦃a : α⦄ ⦃b : β⦄, toContinuousOrderHom_1.toFun a ≤ b → ∃ c, a ≤ c ∧ toContinuousOrderHom_1.toFun c = b},
  { toContinuousOrderHom := toContinuousOrderHom, exists_map_eq_of_map_le' := exists_map_eq_of_map_le' } =
      { toContinuousOrderHom := toContinuousOrderHom_1, exists_map_eq_of_map_le' := exists_map_eq_of_map_le'_1 } →
    toContinuousOrderHom = toContinuousOrderHom_1
-- Mathlib.Probability.Process.Adapted
MeasureTheory.stronglyAdapted_zero' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] (β : ι → Type u_3)
  [inst_1 : (i : ι) → TopologicalSpace (β i)] [inst_2 : (i : ι) → Zero (β i)] (f : MeasureTheory.Filtration ι m),
  MeasureTheory.StronglyAdapted f 0
-- Mathlib.Order.Filter.AtTopBot.Field
Filter.tendsto_const_mul_pow_atTop_iff : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {c : α} {n : ℕ},
  Filter.Tendsto (fun x => c * x ^ n) Filter.atTop Filter.atTop ↔ n ≠ 0 ∧ 0 < c
-- Lean.Elab.ConfigEval.Basic
/-- Evaluates `f e`, and if that does `throwUnsupportedExpr`, evaluates `f (← whnf e)`.
If either throw another exception, aborts immediately with that exception.
If both do `throwUnsupportedExpr`, then this generates an exception.
 -/
Lean.Elab.ConfigEval.EvalExpr.withWHNF : {α : Type} → (Lean.Expr → Lean.MetaM α) → Lean.Expr → Lean.MessageData → Lean.MetaM α
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Compatible families of elements for a presheaf of types `P` and a presieve `R`
are in 1-1 correspondence with compatible families for the same presheaf and
the sieve generated by `R`, through extension and restriction.  -/
CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} → {R : CategoryTheory.Presieve X} → { x // x.Compatible } ≃ { x // x.Compatible }
-- Std.Sat.CNF.Basic
Std.Sat.CNF.sat_empty : ∀ {α : Type u_1} {assign : α → Bool}, Std.Sat.CNF.Sat assign Std.Sat.CNF.empty
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_ne_of_ne : ∀ {a b : UInt8}, a ≠ b → a.toBitVec ≠ b.toBitVec
-- Init.Core
PLift.up.inj : ∀ {α : Sort u} {down down_1 : α}, { down := down } = { down := down_1 } → down = down_1
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_exact.sizeOf_spec : ∀ (lhs : Bool) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr),
  sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.simp_exact lhs c₁ c₂) = 1 + sizeOf lhs + sizeOf c₁ + sizeOf c₂
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instSMul_1 : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      [inst_1 : Ring R] → (v : Valuation R Γ₀) → {S : Type u_3} → [SMul R S] → SMul (WithVal v) S
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piUnique_symm_apply : ∀ {δ' : Type u_5} (π : δ' → Type u_6) [inst : (x : δ') → MeasurableSpace (π x)] [inst_1 : Unique δ'],
  ⇑(MeasurableEquiv.piUnique π).symm = uniqueElim
-- Batteries.Data.Array.Scan
Array.scanr_map : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ → γ} {g : α → β} (init : γ) (as : Array α),
  Array.scanr f init (Array.map g as) = Array.scanr (fun x acc => f (g x) acc) init as
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false →
    Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.Const.insertMany t l) k fallback =
      Std.ExtDTreeMap.Const.getD t k fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_le_size_insertManyIfNewUnit!_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t.WF → ∀ {l : List α}, t.size ≤ (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).size
-- Mathlib.Order.IsNormal
PrincipalSeg.isNormal : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] (f : α <i β),
  Order.IsNormal ⇑f.toRelEmbedding
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.toImplicit.match_1.eq_1 : ∀ (motive : Lean.Expr → Sort u_1) (binderName : Lean.Name) (t : Lean.Expr) (binderName_1 : Lean.Name)
  (binderType body : Lean.Expr) (binderInfo binderInfo_1 : Lean.BinderInfo)
  (h_1 :
    (binderName : Lean.Name) →
      (t b : Lean.Expr) →
        (binderName_2 : Lean.Name) →
          (binderType body : Lean.Expr) →
            (binderInfo : Lean.BinderInfo) →
              b = Lean.Expr.forallE binderName_2 binderType body binderInfo →
                (binderInfo_2 : Lean.BinderInfo) →
                  motive
                    (Lean.Expr.forallE binderName t (Lean.Expr.forallE binderName_2 binderType body binderInfo)
                      binderInfo_2))
  (h_2 : (e : Lean.Expr) → motive e),
  (match Lean.Expr.forallE binderName t (Lean.Expr.forallE binderName_1 binderType body binderInfo) binderInfo_1 with
    | Lean.Expr.forallE binderName t (b@h:(Lean.Expr.forallE binderName_2 binderType body binderInfo)) binderInfo_2 =>
      h_1 binderName t b binderName_2 binderType body binderInfo h binderInfo_2
    | e => h_2 e) =
    h_1 binderName t (Lean.Expr.forallE binderName_1 binderType body binderInfo) binderName_1 binderType body binderInfo
      ⋯ binderInfo_1
-- Init.Data.List.Erase
List.length_eraseP_of_mem : ∀ {α : Type u_1} {l : List α} {a : α} {p : α → Bool}, a ∈ l → p a = true → (List.eraseP p l).length = l.length - 1
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- If `s` is a dense set in a monoid `M`, `Submonoid.closure s = ⊤`, then in order to prove that
some predicate `p` holds for all `x : M` it suffices to verify `p x` for `x ∈ s`, verify `p 1`,
and verify that `p x` and `p y` imply `p (x * y)`.  -/
Submonoid.dense_induction : ∀ {M : Type u_1} [inst : MulOneClass M] {motive : M → Prop} (s : Set M),
  Submonoid.closure s = ⊤ →
    (∀ x ∈ s, motive x) → motive 1 → (∀ (x y : M), motive x → motive y → motive (x * y)) → ∀ (x : M), motive x
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
isStationary_iUnion_iff_of_cof_le_one : ∀ {α : Type v} [inst : LinearOrder α] {ι : Sort u_1} {f : ι → Set α},
  Order.cof α ≤ 1 → (IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i))
-- Mathlib.Data.Set.Image
Subtype.exists_set_subtype : ∀ {α : Type u_1} {t : Set α} (p : Set α → Prop), (∃ s, p (Subtype.val '' s)) ↔ ∃ s ⊆ t, p s
-- Mathlib.Tactic.FunProp.Mor
Mathlib.Meta.FunProp.Mor.instInhabitedArg : Inhabited Mathlib.Meta.FunProp.Mor.Arg
-- Mathlib.Algebra.Lie.Basic
/-- A Lie ring module bracket is additive in its first component.  -/
LieRingModule.add_lie : ∀ {L : Type v} {M : Type w} {inst : LieRing L} {inst_1 : AddCommGroup M} [self : LieRingModule L M] (x y : L) (m : M),
  ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
-- Mathlib.Topology.Order
TopologicalSpace.not_nontrivial_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], ¬NontrivialTopology α ↔ IndiscreteTopology α
-- Mathlib.Topology.Constructions
Continuous.restrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X}
  {t : Set Y} (h1 : Set.MapsTo f s t), Continuous f → Continuous (Set.MapsTo.restrict f s t h1)
-- Mathlib.Algebra.Algebra.Equiv
/-- The equivalence between `RingEquiv` and `ℤ`-algebra isomorphisms.  -/
RingEquiv.equivIntAlgEquiv : (R : Type u_1) → (S : Type u_2) → [inst : Ring R] → [inst_1 : Ring S] → R ≃+* S ≃ R ≃ₐ[ℤ] S
-- Init.Data.Char.Basic
Char.instLE : LE Char
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the angle between three points is `π`, the first two points are not equal.  -/
EuclideanGeometry.left_ne_of_oangle_eq_pi : ∀ {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}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi → p₁ ≠ p₂
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.erase.match_1.splitter : {α : Type u_1} →
  (as : Array α) →
    (motive : Option (Fin as.size) → Sort u_2) →
      (x : Option (Fin as.size)) → (Unit → motive none) → ((i : Fin as.size) → motive (some i)) → motive x
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.Hereditarily.eq_def : ∀ (p : ZFSet.{u_1} → Prop) (x : ZFSet.{u_1}), ZFSet.Hereditarily p x = (p x ∧ ∀ y ∈ x, ZFSet.Hereditarily p y)
-- Mathlib.LinearAlgebra.Pi
/-- If `ι` has a unique element, then `ι → M` is linearly equivalent to `M`.  -/
LinearEquiv.funUnique : (ι : Type u_5) →
  (R : Type u_6) →
    (M : Type u_7) →
      [Unique ι] → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (ι → M) ≃ₗ[R] M
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Context.mk.sizeOf_spec : ∀ (simp : Lean.Meta.Simp.Context) (simpMethods : Lean.Meta.Simp.Methods) (config : Lean.Grind.Config)
  (anchorRefs? : Option (Array Lean.Meta.Grind.AnchorRef)) (cheapCases reportMVarIssue : Bool)
  (splitSource : Lean.Meta.Grind.SplitSource) (ematchDiagSource : Lean.Meta.Grind.EMatchDiagSource)
  (symPrios : Lean.Meta.Grind.SymbolPriorities) (extensions : Lean.Meta.Grind.ExtensionStateArray)
  (debug ematchDiag : Bool),
  sizeOf
      { simp := simp, simpMethods := simpMethods, config := config, anchorRefs? := anchorRefs?,
        cheapCases := cheapCases, reportMVarIssue := reportMVarIssue, splitSource := splitSource,
        ematchDiagSource := ematchDiagSource, symPrios := symPrios, extensions := extensions, debug := debug,
        ematchDiag := ematchDiag } =
    1 + sizeOf simp + sizeOf simpMethods + sizeOf config + sizeOf anchorRefs? + sizeOf cheapCases +
                  sizeOf reportMVarIssue +
                sizeOf splitSource +
              sizeOf ematchDiagSource +
            sizeOf symPrios +
          sizeOf extensions +
        sizeOf debug +
      sizeOf ematchDiag
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_mem : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g g' : M → M'} {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    (∀ y ∈ s, g' y = g y) → x ∈ s → (ChartedSpace.LiftPropWithinAt P g' s x ↔ ChartedSpace.LiftPropWithinAt P g s x)
-- Mathlib.Order.SupIndep
/-- **Alias** of the reverse direction of `iSupIndep_comp_coe_iff_supIndep`. -/
Finset.SupIndep.independent : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {s : Finset ι} {f : ι → α},
  s.SupIndep f → iSupIndep (f ∘ Subtype.val)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.mk' : {X : SSet} → {A : X.Subcomplex} → (toN : X.N) → toN.simplex ∉ A.obj (Opposite.op { len := toN.dim }) → A.N
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- If `x` is not a non zero divisor, `ordMonoidWithZeroHom` is equal to `0`.
 -/
Ring.ordMonoidWithZeroHom_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Nontrivial R] {x : R},
  x ∉ nonZeroDivisors R → (Ring.ordMonoidWithZeroHom R) x = 0
-- Mathlib.Geometry.Euclidean.Projection
Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : Affine.Simplex 𝕜 P 1)
  (i : Fin 2) (p : P), ↑((s.faceOpposite i).orthogonalProjectionSpan p) = s.points i.rev
-- Mathlib.RingTheory.Polynomial.Vieta
Multiset.prod_X_sub_C_coeff : ∀ {R : Type u_1} [inst : CommRing R] (s : Multiset R) {k : ℕ},
  k ≤ s.card →
    (Multiset.map (fun t => Polynomial.X - Polynomial.C t) s).prod.coeff k = (-1) ^ (s.card - k) * s.esymm (s.card - k)
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.instIsFiniteKernelSingularPart : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [hκ : ProbabilityTheory.IsFiniteKernel κ]
  [inst : ProbabilityTheory.IsFiniteKernel η], ProbabilityTheory.IsFiniteKernel (κ.singularPart η)
-- Init.Data.BitVec.Lemmas
BitVec.uaddOverflow.eq_1 : ∀ {w : ℕ} (x y : BitVec w), x.uaddOverflow y = decide (x.toNat + y.toNat ≥ 2 ^ w)
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.mapDomain_eq_zero : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} (f : α → β) [inst : AddCommMonoid M] [inst_1 : Filter.TendstoCofinite f]
  (v : α → M) {i : β}, i ∉ Set.range f → Filter.TendstoCofinite.mapDomain f v i = 0
-- Mathlib.RingTheory.AdjoinRoot
/-- Produce an algebra homomorphism `AdjoinRoot f →ₐ[R] S` sending `root f` to
a root of `f` in `S`.  -/
AdjoinRoot.liftAlgHom : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra S R] →
              [inst_4 : Algebra S T] →
                (p : Polynomial R) → (i : R →ₐ[S] T) → (x : T) → Polynomial.eval₂ (↑i) x p = 0 → AdjoinRoot p →ₐ[S] T
-- Mathlib.Algebra.Group.Defs
AddCancelCommMonoid.toAddCommMonoid : {M : Type u} → [self : AddCancelCommMonoid M] → AddCommMonoid M
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.Barrier.mk.sizeOf_spec : ∀ (lock : Std.Mutex Std.BarrierState✝) (cvar : Std.Condvar) (numThreads : ℕ),
  sizeOf { lock := lock, cvar := cvar, numThreads := numThreads } = 1 + sizeOf lock + sizeOf cvar + sizeOf numThreads
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
/-- The object `Δ[0]` is terminal in `SSet`.  -/
SSet.stdSimplex.isTerminalObj₀ : CategoryTheory.Limits.IsTerminal (SSet.stdSimplex.obj { len := 0 })
-- Mathlib.Data.Seq.Defs
/-- Get the nth element of a sequence (if it exists)  -/
Stream'.Seq.get? : {α : Type u} → Stream'.Seq α → ℕ → Option α
-- Mathlib.Topology.Separation.Hausdorff
tendsto_nhds_unique' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T2Space X] {f : Y → X} {l : Filter Y} {a b : X},
  l.NeBot → Filter.Tendsto f l (nhds a) → Filter.Tendsto f l (nhds b) → a = b
-- Init.Grind.ToInt
Lean.Grind.ToInt.Neg.mk : ∀ {α : Type u} [inst : Neg α] {I : outParam Lean.Grind.IntInterval} [inst_1 : Lean.Grind.ToInt α I],
  (∀ (x : α), ↑(-x) = I.wrap (-↑x)) → Lean.Grind.ToInt.Neg α I
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
/-- Replacing the first argument of `Majorized` by an eventually equal function preserves it.  -/
Tactic.ComputeAsymptotics.Majorized.of_eventuallyEq : ∀ {f g b : ℝ → ℝ} {exp : ℝ},
  g =ᶠ[Filter.atTop] f → Tactic.ComputeAsymptotics.Majorized f b exp → Tactic.ComputeAsymptotics.Majorized g b exp
-- Lean.Meta.DiscrTree.Basic
_private.Lean.Meta.DiscrTree.Basic.0.Lean.Meta.DiscrTree.keysAsPattern.go : optParam Bool true → StateRefT' IO.RealWorld (List Lean.Meta.DiscrTree.Key) Lean.CoreM Lean.MessageData
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atBot_add_left_of_ge' : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  (∀ᶠ (x : α) in l, f x ≤ C) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
-- Mathlib.Topology.Constructions
ContinuousAt.finSnoc : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} {A : Fin (n + 1) → Type u_9}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)] {f : X → (j : Fin n) → A j.castSucc} {g : X → A (Fin.last n)}
  {x : X}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun a => Fin.snoc (f a) (g a)) x
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.associated_iff_roots_eq_roots : ∀ {k : Type u} [inst : Field k] [IsAlgClosed k] {p q : Polynomial k},
  p ≠ 0 → q ≠ 0 → (Associated p q ↔ p.roots = q.roots)
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.cast_cast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig1 aig2 aig3 : Std.Sat.AIG α}
  (s : aig1.RefVec len) (h1 : aig1.decls.size ≤ aig2.decls.size) (h2 : aig2.decls.size ≤ aig3.decls.size),
  (s.cast h1).cast h2 = s.cast ⋯
-- Lean.Parser.Types
Lean.Parser.ParserInfo.firstTokens : Lean.Parser.ParserInfo → Lean.Parser.FirstTokens
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.locallyLipschitz : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} [FiniteDimensional ℝ E],
  ConcaveOn ℝ Set.univ f → LocallyLipschitz f