mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.KrullDimension.Regular
Module.exists_ltSeries_support_isMaximal_last_of_ltSeries_support : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (q : LTSeries ↑(Module.support R M)), ∃ p, q.length ≤ p.length ∧ (↑(RelSeries.last p)).asIdeal.IsMaximal
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- If there is an `n`-th primitive root of unity in `R` and `b` divides `n`,
then there is a `b`-th primitive root of unity in `R`.  -/
IsPrimitiveRoot.pow : ∀ {M : Type u_1} [inst : CommMonoid M] {ζ : M} {n a b : ℕ},
  0 < n → IsPrimitiveRoot ζ n → n = a * b → IsPrimitiveRoot (ζ ^ a) b
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_left_inj : ∀ {a b c : ENNReal}, c ≠ 0 → c ≠ ⊤ → (a * c = b * c ↔ a = b)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_sup_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Injective ⇑f →
    ∀ (S T : AddSubmonoid M), AddSubmonoid.comap f (AddSubmonoid.map f S ⊔ AddSubmonoid.map f T) = S ⊔ T
-- Aesop.Rule
Aesop.instInhabitedNormRuleInfo.default : Aesop.NormRuleInfo
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_inv`. -/
Antivary.of_inv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : CommGroup β] [inst_4 : PartialOrder β] [IsOrderedMonoid β] {f : ι → α} {g : ι → β},
  Antivary f⁻¹ g⁻¹ → Antivary f g
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.one_lt_tau : ∀ {β : Type u_1} {α : Type u_2} (self : Besicovitch.TauPackage β α), 1 < self.τ
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.pmap_map : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {γ : Type x}
  {x : Std.Iterators.HetT m α} {f : α → β} {g : (b : β) → (Std.Iterators.HetT.map f x).Property b → γ},
  (Std.Iterators.HetT.map f x).pmap g = x.pmap fun a ha => g (f a) ⋯
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E],
  IsBoundedLinearMap 𝕜 fun x => x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.range_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Topology.IsInducing f), Set.range (TopologicalSpace.Compacts.map f ⋯) = {K | ↑K ⊆ Set.range f}
-- Init.Data.SInt.Bitwise
UInt64.toInt64_and : ∀ (a b : UInt64), (a &&& b).toInt64 = a.toInt64 &&& b.toInt64
-- Std.Http.Data.URI.Basic
/-- An IPv4 address.
 -/
Std.Http.URI.Host.ipv4 : Std.Net.IPv4Addr → Std.Http.URI.Host
-- Mathlib.Algebra.Category.Ring.Under.Property
RingHom.HasEqualizers.hasEqualizers : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => Q) →
      ∀ (R : CommRingCat),
        CategoryTheory.Limits.HasEqualizers
          ((RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q).Under ⊤ R)
-- Mathlib.Order.Concept
Concept.extent_swap : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r), c.swap.extent = c.intent
-- Mathlib.Topology.Constructions.SumProd
/-- The sum of `X` with any empty topological space is homeomorphic to `X`.  -/
Homeomorph.sumEmpty : (X : Type u) → (Y : Type v) → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → [IsEmpty Y] → X ⊕ Y ≃ₜ X
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `zero_apply`. -/
ModularForm.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Mathlib.LinearAlgebra.Dual.Defs
LinearEquiv.dualMap_apply : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (f : M₁ ≃ₗ[R] M₂) (g : Module.Dual R M₂)
  (x : M₁), (f.dualMap g) x = g (f x)
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_eq_zero_or_self : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] (s : Set α) (f : α → M) (a : α),
  s.indicator f a = 0 ∨ s.indicator f a = f a
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.triangle : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  (F G U : CategoryTheory.Functor C V) [inst_9 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  [inst_10 : CategoryTheory.MonoidalCategory.DayConvolution F U]
  [inst_11 : CategoryTheory.MonoidalCategory.DayConvolution U G]
  [inst_12 :
    CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution U G)]
  [inst_13 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F U) G]
  [inst_14 : CategoryTheory.MonoidalCategory.DayConvolution F G],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator F U G).hom
      (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F)
        (CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U G).hom) =
    CategoryTheory.MonoidalCategory.DayConvolution.map
      (CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F).hom (CategoryTheory.CategoryStruct.id G)
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.mkContext : Lean.Name → String → Lean.Name → optParam Bool true → Lean.Elab.TermElabM Lean.Elab.Deriving.Context
-- Mathlib.Order.Filter.Basic
Filter.nonempty_of_neBot : ∀ {α : Type u} (f : Filter α) [f.NeBot], Nonempty α
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.reachable_eq_reflTransGen : ∀ {V : Type u} {G : SimpleGraph V}, G.Reachable = Relation.ReflTransGen G.Adj
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- The relation that one `SimpleGraph` is a subgraph of another.
Note that this should be spelled `≤`.  -/
SimpleGraph.IsSubgraph : {V : Type u} → SimpleGraph V → SimpleGraph V → Prop
-- Mathlib.Topology.TietzeExtension
Unique.instTietzeExtension : ∀ {Y : Type v} [inst : TopologicalSpace Y] [Nonempty Y] [Subsingleton Y], TietzeExtension Y
-- Init.Data.Fin.Basic
/-- Bitwise right shift of bounded numbers.

This operator corresponds to logical rather than arithmetic bit shifting. The new bits are always
`0`.

Examples:
 * `(15 : Fin 16) >>> (1 : Fin 16) = (7 : Fin 16)`
 * `(15 : Fin 16) >>> (2 : Fin 16) = (3 : Fin 16)`
 * `(15 : Fin 17) >>> (2 : Fin 17) = (3 : Fin 17)`
 -/
Fin.shiftRight : {n : ℕ} → Fin n → Fin n → Fin n
-- Aesop.Index.Basic
Aesop.IndexingMode.brecOn_1.go : {motive_1 : Aesop.IndexingMode → Sort u} →
  {motive_2 : Array Aesop.IndexingMode → Sort u} →
    {motive_3 : List Aesop.IndexingMode → Sort u} →
      (t : Array Aesop.IndexingMode) →
        ((t : Aesop.IndexingMode) → t.below → motive_1 t) →
          ((t : Array Aesop.IndexingMode) → Aesop.IndexingMode.below_1 t → motive_2 t) →
            ((t : List Aesop.IndexingMode) → Aesop.IndexingMode.below_2 t → motive_3 t) →
              motive_2 t ×' Aesop.IndexingMode.below_1 t
-- Batteries.Recycling.RBTree.Basic
/-- The second half of Okasaki's `balance`, concerning red-red sequences in the right child.  -/
RBTree.RBNode.balance2 : {α : Type u_1} → RBTree.RBNode α → α → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.RingTheory.Localization.Basic
AlgEquiv.extendScalarsOfIsLocalization_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  (S : Type u_4) [inst_3 : CommSemiring S] [inst_4 : Algebra R S] (M : Submonoid R) [inst_5 : IsLocalization M S]
  [inst_6 : Algebra R A] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] [inst_9 : Algebra R B]
  [inst_10 : Algebra S B] [inst_11 : IsScalarTower R S B] (f : A ≃ₐ[R] B) (a : B),
  (AlgEquiv.extendScalarsOfIsLocalization S M f).symm a = f.invFun a
-- Mathlib.Data.NNRat.Defs
NNRat.coe_le_coe : ∀ {p q : ℚ≥0}, ↑p ≤ ↑q ↔ p ≤ q
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instMulRightMono : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : PartialOrder β]
  [inst_3 : MulZeroClass β] [inst_4 : ContinuousMul β] [MulRightMono β],
  MulRightMono (CompactlySupportedContinuousMap α β)
-- Lean.Widget.Commands
/-- Use `show_panel_widgets [<widget>]` to mark that `<widget>`
should always be displayed, including in downstream modules.

The type of `<widget>` must implement `Widget.ToModule`,
and the type of `<props>` must implement `Server.RpcEncodable`.
In particular, `<props> : Json` works.

Use `show_panel_widgets [<widget> with <props>]`
to specify the `<props>` that the widget should be given
as arguments.

Use `show_panel_widgets [local <widget> (with <props>)?]` to mark it
for display in the current section, namespace, or file only.

Use `show_panel_widgets [scoped <widget> (with <props>)?]` to mark it
for display only when the current namespace is open.

Use `show_panel_widgets [-<widget>]` to temporarily hide a previously shown widget
in the current section, namespace, or file.
Note that persistent erasure is not possible, i.e.,
`-<widget>` has no effect on downstream modules.  -/
Lean.Widget.showPanelWidgetsCmd : Lean.ParserDescr
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- A function `fun cfg item => ...`.  -/
Lean.Elab.ConfigEval.EvalConfigItemHandler.body : Lean.Elab.ConfigEval.EvalConfigItemHandler → Lean.Term
-- Lean.Util.Trace
Lean.instMonadAlwaysExceptStateRefT' : {m : Type → Type} → {ε ω σ : Type} → [always : Lean.MonadAlwaysExcept ε m] → Lean.MonadAlwaysExcept ε (StateRefT' ω σ m)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C)
  (X_1 : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.inverse.obj X).obj X_1 =
    match
      match Opposite.unop X_1 with
      | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
      | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of x => X.left.obj x
    | CategoryTheory.WithTerminal.star => X.right
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzWith_iff_norm_inv_mul_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {f : E → F} {C : NNReal},
  LipschitzWith C f ↔ ∀ (x y : E), ‖(f x)⁻¹ * f y‖ ≤ ↑C * ‖x⁻¹ * y‖
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.has_finite_coproducts : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.NonPreadditiveAbelian C],
  CategoryTheory.Limits.HasFiniteCoproducts C
-- Mathlib.RingTheory.Noetherian.Basic
IsNoetherianRing.eq_1 : ∀ (R : Type u_1) [inst : Semiring R], IsNoetherianRing R = IsNoetherian R R
-- Mathlib.Control.Monad.Cont
MonadCont.Label.mk.inj : ∀ {α : Type w} {m : Type u → Type v} {β : Type u} {apply apply_1 : α → m β},
  { apply := apply } = { apply := apply_1 } → apply = apply_1
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.exists_appTop_π_eq_of_isLimit : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] (s : ↑(c.pt.presheaf.obj (Opposite.op ⊤)))
  [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)],
  ∃ i t, s = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (c.π.app i))) t
-- Lean.Expr
Lean.mkApp4 : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Std.Time.Time.PlainTime
/-- Creates a `PlainTime` value from the provided hours, minutes, and seconds.
 -/
Std.Time.PlainTime.ofHourMinuteSeconds : Std.Time.Hour.Ordinal → Std.Time.Minute.Ordinal → Std.Time.Second.Ordinal true → Std.Time.PlainTime
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- The condition that a property of morphisms is stable by finite products.  -/
CategoryTheory.MorphismProperty.IsStableUnderFiniteProducts : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.GroupTheory.GroupAction.ConjAct
Subgroup.centralizer_eq_comap_stabilizer : ∀ {G : Type u_3} [inst : Group G] (g : G),
  Subgroup.centralizer {g} = Subgroup.comap ConjAct.toConjAct.toMonoidHom (MulAction.stabilizer (ConjAct G) g)
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
/-- The Gaussian integers, defined as `ℤ√(-1)`.  -/
GaussianInt : Type
-- Init.MetaTypes
Lean.Meta.Occurrences.pos.inj : ∀ {idxs idxs_1 : List ℕ}, Lean.Meta.Occurrences.pos idxs = Lean.Meta.Occurrences.pos idxs_1 → idxs = idxs_1
-- Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
/-- Every Yoneda-presheaf is a sheaf for the coherent topology.  -/
CategoryTheory.coherentTopology.isSheaf_yoneda_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Precoherent C] (W : C),
  CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology C) (CategoryTheory.yoneda.obj W)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_eq_bot : ∀ {α : Type u} [inst : Add α] {x y : WithBot α}, x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.mul_toFun : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Semiring R] (s : HahnSeries.SummableFamily Γ R α)
  (t : HahnSeries.SummableFamily Γ R β) (a : α × β), (s.mul t) a = s a.1 * t a.2
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.ne.injEq : ∀ (lhs rhs : ℕ) (proof : Lean.Expr) (lhs_1 rhs_1 : ℕ) (proof_1 : Lean.Expr),
  (Mathlib.Tactic.Order.AtomicFact.ne lhs rhs proof = Mathlib.Tactic.Order.AtomicFact.ne lhs_1 rhs_1 proof_1) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1)
-- Init.Data.Nat.Div.Basic
Nat.div_le_self : ∀ (n k : ℕ), n / k ≤ n
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_pair : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {x y : α}, x ≠ y → {x, y}.einfsep = edist x y
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- `SemimoduleCat.Hom.hom` bundled as an `Equiv`.  -/
SemimoduleCat.homEquiv : {R : Type u} → [inst : Semiring R] → {M N : SemimoduleCat R} → (M ⟶ N) ≃ (↑M →ₗ[R] ↑N)
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
Conformal.conformalAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : NormedAddCommGroup X] [inst_1 : NormedAddCommGroup Y] [inst_2 : NormedSpace ℝ X]
  [inst_3 : NormedSpace ℝ Y] {f : X → Y}, Conformal f → ∀ (x : X), ConformalAt f x
-- Mathlib.Topology.ContinuousOn
/-- Variant of `Continuous.comp_continuousOn` using the form `fun y ↦ g (f y)`
instead of `g ∘ f`.  -/
Continuous.comp_continuousOn' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α},
  Continuous g → ContinuousOn f s → ContinuousOn (fun x => g (f x)) s
-- Mathlib.LinearAlgebra.FreeModule.PID
Module.Basis.SmithNormalForm.mk.sizeOf_spec : ∀ {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M}
  {ι : Type u_4} {n : ℕ} [inst_3 : SizeOf R] [inst_4 : SizeOf M] [inst_5 : SizeOf ι] (bM : Module.Basis ι R M)
  (bN : Module.Basis (Fin n) R ↥N) (f : Fin n ↪ ι) (a : Fin n → R) (snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)),
  sizeOf { bM := bM, bN := bN, f := f, a := a, snf := snf } = 1 + sizeOf bM + sizeOf bN + sizeOf f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.cooper.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.CooperSplit),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.cooper c = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.cooper c_1) =
    (c = c_1)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.finitelyManySteps.congr_simp : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] [inst_1 : Std.Iterators.Finite α m]
  (it it_1 : Std.IterM m β), it = it_1 → it.finitelyManySteps = it_1.finitelyManySteps
-- Init.GetElem
isSome_getElem? : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem? cont idx elem dom]
  [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)], (c[i]?.isSome = true) = dom c i
-- Init.Meta.Defs
/-- Decodes a 'scientific number' string which is consumed by the `OfScientific` class. Takes as input a
string such as `123`, `123.456e7` and returns a triple `(n, sign, e)` with value given by
`n * 10^-e` if `sign` else `n * 10^e`.
 -/
Lean.Syntax.decodeScientificLitVal? : String → Option (ℕ × Bool × ℕ)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.instPreorder : {M : Type u_2} →
  [inst : CommGroup M] → [inst_1 : LinearOrder M] → [IsOrderedMonoid M] → Preorder (MulArchimedeanOrder M)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.mk.sizeOf_spec : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] [inst_6 : SizeOf R] [inst_7 : SizeOf S] [inst_8 : SizeOf A] [inst_9 : SizeOf B]
  (toDistribMulActionHom : A →ₑ+[φ] B)
  (map_mul' :
    ∀ (x y : A), toDistribMulActionHom.toFun (x * y) = toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y),
  sizeOf { toDistribMulActionHom := toDistribMulActionHom, map_mul' := map_mul' } = 1 + sizeOf toDistribMulActionHom
-- Init.Data.List.MinMaxIdx
List.minIdxOn_append : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []),
  List.minIdxOn f (xs ++ ys) ⋯ =
    if f (List.minOn f xs hxs) ≤ f (List.minOn f ys hys) then List.minIdxOn f xs hxs
    else xs.length + List.minIdxOn f ys hys
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
/-- If `P` is a morphism property affine locally defined by `affineAnd Q`, `P` is stable under
base change if `Q` is.  -/
AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderBaseChange : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
      (RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q) → P.IsStableUnderBaseChange
-- Init.Data.Vector.Count
Vector.countP_le_size : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {xs : Vector α n}, Vector.countP p xs ≤ n
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Init.Data.BitVec.Lemmas
BitVec.cast_append_left : ∀ {w v w' : ℕ} (h : w + v = w' + v) (x : BitVec w) (y : BitVec v), BitVec.cast h (x ++ y) = BitVec.cast ⋯ x ++ y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k : α},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.Const.unitOfList l cmp) k = if l.contains k = true then some () else none
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.tprod_sigma' : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousMul α] [T3Space α]
  {γ : β → Type u_4} {f : (b : β) × γ b → α},
  (∀ (b : β), Multipliable fun c => f ⟨b, c⟩) →
    Multipliable f → ∏' (p : (b : β) × γ b), f p = ∏' (b : β) (c : γ b), f ⟨b, c⟩
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.inter_eq_of_inter_eq_of_eqOn : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {e' : PartialEquiv α β},
  e.IsImage s t →
    e'.IsImage s t → e.source ∩ s = e'.source ∩ s → Set.EqOn (↑e) (↑e') (e.source ∩ s) → e.target ∩ t = e'.target ∩ t
-- Mathlib.ModelTheory.Skolem
FirstOrder.Language.Substructure.coeSort_elementarySkolem₁Reduct : ∀ {L : FirstOrder.Language} {M : Type w} [inst : Nonempty M] [inst_1 : L.Structure M]
  (S : (L.sum L.skolem₁).Substructure M), ↥S.elementarySkolem₁Reduct = ↥S
-- Init.Prelude
Neg.mk : {α : Type u} → (α → α) → Neg α
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.μ_comp_lTensor : ∀ {G : Type v} [inst : Monoid G] {X Y : Action (Type w) G} {k : Type u} [inst_1 : CommSemiring k] (f : X ⟶ Y)
  (Z : Action (Type w) G),
  (Representation.LinearizeMonoidal.μ Z Y).comp
      (Representation.IntertwiningMap.lTensor (Representation.linearize k G Z) (Representation.linearizeMap f)) =
    (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)).comp
      (Representation.LinearizeMonoidal.μ Z X)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.instZeroTerm : {α : Type u_1} → Zero (FirstOrder.Language.presburger.Term α)
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_addString : ∀ (p : String.Pos.Raw) (s : String), (p + s).byteIdx = p.byteIdx + s.utf8ByteSize
-- Mathlib.RingTheory.Extension.Basic
/-- The canonical map `P → P/I²` as maps between extensions.  -/
Algebra.Extension.toInfinitesimal : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → P.Hom P.infinitesimal
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.eq_def : ∀ {n : ℕ} (acc : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool))
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder acc l =
    match acc with
    | none => none
    | some map =>
      match map.getThenInsertIfNew? l.1 l.2 with
      | (val?, map) =>
        match val? with
        | some val' => if (l.2 != val') = true then none else some map
        | x => some map