mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.appIso_homOfLE_inv : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (h : U ≤ V) (W : (↑U).Opens),
  (AlgebraicGeometry.Scheme.Hom.appIso (X.homOfLE h) W).inv = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Std.Sat.CNF.Basic
Std.Sat.CNF.instDecidableMemClauseOfDecidableEq : {α : Type u_1} → {c : Std.Sat.CNF.Clause α} → {f : Std.Sat.CNF α} → [DecidableEq α] → Decidable (c ∈ f)
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.ι_colimitCompWhiskeringRightIsoColimitComp_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [inst_5 : CategoryTheory.Limits.PreservesColimitsOfShape J F]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j)
      (CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G).hom =
    CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.colimit.ι G j) F
-- Std.Http.Data.Body.Basic
/-- Non-blocking receive attempt. Returns `none` if no chunk is immediately available,
`some (some chunk)` when a chunk is ready, or `some none` at end-of-stream.
 -/
Std.Http.Body.tryRecv : {α : Type} → [self : Std.Http.Body α] → α → Std.Async.Async (Option (Option Std.Http.Chunk))
-- Mathlib.Order.Filter.IndicatorFunction
Filter.EventuallyEq.of_mulIndicator : ∀ {α : Type u_1} {β : Type u_2} [inst : One β] {l : Filter α} {f : α → β},
  (∀ᶠ (x : α) in l, f x ≠ 1) → ∀ {s t : Set α}, s.mulIndicator f =ᶠ[l] t.mulIndicator f → s =ᶠ[l] t
-- Init.Data.Vector.Basic
Vector.extract.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (start stop : ℕ),
  xs.extract start stop = Vector.mk (xs.toArray.extract start stop) ⋯
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RioSliceData.mk.inj : ∀ {α : Type u} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit} {range : Std.Rio α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit} {range_1 : Std.Rio α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- One semiconjugates any element to itself.  -/
SemiconjBy.one_left : ∀ {M : Type u_2} [inst : MulOneClass M] (x : M), SemiconjBy 1 x x
-- Mathlib.Logic.Embedding.Basic
Equiv.embeddingSurjectiveEquiv_apply : ∀ {α : Sort u_1} {β : Type u_2} (f : { f // Function.Surjective ⇑f }),
  Equiv.embeddingSurjectiveEquiv f = (↑f).equivOfSurjective ⋯
-- Mathlib.Probability.Independence.Process.Basic
/-- Two stochastic processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ are independent if
for all $s_1, ..., s_p \in S$ and $t_1, ..., t_q \in T$ the two families
$(X_{s_1}, ..., X_{s_p})$ and $(Y_{t_1}, ..., Y_{t_q})$ are independent.  -/
ProbabilityTheory.Kernel.IndepFun.process_indepFun_process : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {T : Type u_5} {𝓧 : S → Type u_6} {𝓨 : T → Type u_7}
  [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : (j : T) → MeasurableSpace (𝓨 j)] {X : (i : S) → Ω → 𝓧 i}
  {Y : (j : T) → Ω → 𝓨 j},
  (∀ (i : S), Measurable (X i)) →
    (∀ (j : T), Measurable (Y j)) →
      (∀ (I : Finset S) (J : Finset T),
          ProbabilityTheory.Kernel.IndepFun (fun ω i => X (↑i) ω) (fun ω j => Y (↑j) ω) κ P) →
        ∀ [ProbabilityTheory.IsZeroOrMarkovKernel κ],
          ProbabilityTheory.Kernel.IndepFun (fun ω i => X i ω) (fun ω j => Y j ω) κ P
-- Batteries.Recycling.RBTree.Alter
/-- A sufficient condition for `ModifyWF` is that the new element compares equal to the original.
 -/
RBTree.RBSet.ModifyWF.of_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {f : α → α} {t : RBTree.RBSet α cmp},
  (∀ {x : α}, RBTree.RBNode.find? cut ↑t = some x → RBTree.RBNode.cmpEq cmp (f x) x) → t.ModifyWF cut f
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.quotMk_of : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] (i : ι) (x : G i),
  Quot.mk (⇑(Module.DirectLimit.moduleCon f).toSetoid) ((DirectSum.of G i) x) = (Module.DirectLimit.of R ι G f i) x
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- If a function is `r`-Hölder and `t`-Hölder, then it is `s`-Hölder for `r ≤ s ≤ t`.  -/
MemHolder.memHolder_of_le_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {s t : NNReal}, MemHolder r f → MemHolder t f → r ≤ s → s ≤ t → MemHolder s f
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.comp_smul : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M]
  [inst_5 : Monoid S] [inst_6 : DistribMulAction S M₂] [inst_7 : Module R M₂] [inst_8 : Module R M₃]
  [inst_9 : SMulCommClass R S M₂] [inst_10 : DistribMulAction S M₃] [inst_11 : SMulCommClass R S M₃]
  [LinearMap.CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃), g ∘ₗ (a • f) = a • g ∘ₗ f
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_eq_of_pairing_eq_zero' : ∀ {ι : 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} {i j : ι},
  P.pairing i j = 0 → (P.reflectionPerm i) j = j
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.lt_of_pos_of_infinitesimal : ∀ {x : ℝ*}, x.Infinitesimal → ∀ (r : ℝ), 0 < r → x < ↑r
-- Mathlib.Analysis.Normed.Module.Basic
Metric.diam_sphere_eq : ∀ {E : Type u_6} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) {r : ℝ},
  0 ≤ r → Metric.diam (Metric.sphere x r) = 2 * r
-- Lean.Environment
_private.Lean.Environment.0.Lean.finalizeImport.unsafe_8 : Lean.Environment → BaseIO Lean.Environment
-- Lean.Meta.Tactic.Grind.Types
/-- The generation in which this enode was created.  -/
Lean.Meta.Grind.ENode.generation : Lean.Meta.Grind.ENode → ℕ
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.collect.processExplicitArg : Bool →
  Lean.Elab.Term.CollectPatternVars.Context →
    Lean.Elab.Term.CollectPatternVars.M Lean.Elab.Term.CollectPatternVars.Context
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_X_mul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m : σ →₀ ℕ) (s : σ) (p : MvPolynomial σ R),
  MvPolynomial.coeff ((fun₀ | s => 1) + m) (MvPolynomial.X s * p) = MvPolynomial.coeff m p
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.propagateExpectedTypeFor : Lean.Expr → Lean.Elab.TermElabM Bool
-- Mathlib.RingTheory.Valuation.Basic
Valuation.mk : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    [inst : LinearOrderedCommMonoidWithZero Γ₀] →
      [inst_1 : Ring R] →
        (toMonoidWithZeroHom : R →*₀ Γ₀) →
          (∀ (x y : R),
              (↑toMonoidWithZeroHom).toFun (x + y) ≤
                max ((↑toMonoidWithZeroHom).toFun x) ((↑toMonoidWithZeroHom).toFun y)) →
            Valuation R Γ₀
-- Mathlib.Util.DelabNonCanonical
/-- Delaborate an expression with arity `arity` into a unary notation `mkStx` iff the argument
`arg` is a non-canonical instance (is not defeq to what is synthesized for its type, or else
instance synthesis fails).  -/
Delab.Noncanonical.delabUnary : ℕ → ℕ → (Lean.Term → Lean.PrettyPrinter.Delaborator.Delab) → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Order.Filter.Pointwise
Filter.addSemigroup.eq_1 : ∀ {α : Type u_2} [inst : AddSemigroup α], Filter.addSemigroup = { toAdd := Filter.instAdd, add_assoc := ⋯ }
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Variables that come from a lambda or forall binder.
The list index gives the De Bruijn index.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.Context.bvars : Lean.Meta.RefinedDiscrTree.Context✝ → List Lean.FVarId
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.ofReal_measureReal : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  autoParam (μ s ≠ ⊤) MeasureTheory.ofReal_measureReal._auto_1 → ENNReal.ofReal (μ.real s) = μ s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l →
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKeyD k'
            fallback =
          k
-- Lean.Expr
Lean.ExprStructEq.mk.injEq : ∀ (val val_1 : Lean.Expr), ({ val := val } = { val := val_1 }) = (val = val_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.index_of_iso : ∀ {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {Y : SSet} (e : X ≅ Y) {d : ℕ} (hd : x.dim = d),
  ⋯.index hd = hxy.index hd
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.pointSmallEtale_fiber : ∀ {S : AlgebraicGeometry.Scheme} {Ω : Type u} [inst : Field Ω] [inst_1 : IsSepClosed Ω]
  (s : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S),
  (AlgebraicGeometry.Scheme.pointSmallEtale s).fiber =
    (AlgebraicGeometry.Scheme.Etale.forget S).comp
      (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Over.mk s)))
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.fg_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ⊥.FG
-- Mathlib.Data.Finset.Card
Finset.card_le_card_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β),
  Set.MapsTo f ↑s ↑t → Set.InjOn f ↑s → s.card ≤ t.card
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.ppSimpTheorem : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Meta.SimpTheorem → m Lean.MessageData
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.ext_iff : ∀ {X Y : Semigrp} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Init.Data.Array.Range
Array.map_snd_add_zipIdx_eq_zipIdx : ∀ {α : Type u_1} {xs : Array α} {n k : ℕ}, Array.map (Prod.map id fun x => x + n) (xs.zipIdx k) = xs.zipIdx (n + k)
-- Mathlib.AlgebraicTopology.MooreComplex
/-- The differentials in the normalized Moore complex.
 -/
AlgebraicTopology.NormalizedMooreComplex.objD : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (X : CategoryTheory.SimplicialObject C) →
        (n : ℕ) →
          CategoryTheory.Subobject.underlying.obj (AlgebraicTopology.NormalizedMooreComplex.objX X (n + 1)) ⟶
            CategoryTheory.Subobject.underlying.obj (AlgebraicTopology.NormalizedMooreComplex.objX X n)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- An algebra morphism with an underlying isomorphism hom in `C` is an algebra isomorphism.  -/
CategoryTheory.Endofunctor.Algebra.iso_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (f : A₀ ⟶ A₁) [CategoryTheory.IsIso f.f], CategoryTheory.IsIso f
-- Mathlib.GroupTheory.OrderOfElement
/-- If `S` is a nonempty subset of a finite additive group `G`, then `|G| • S` is a subgroup  -/
smulCardAddSubgroup : {G : Type u_6} → [inst : AddGroup G] → [Fintype G] → (S : Set G) → S.Nonempty → AddSubgroup G
-- Mathlib.Data.Nat.Log
Nat.log_div_base_pow : ∀ (b n k : ℕ), Nat.log b (n / b ^ k) = Nat.log b n - k
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.modify_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : EquivBEq α] [inst_2 : Hashable α]
  {m : Std.DHashMap.Raw α fun x => β} (h : m.WF) {k : α} {f : β → β},
  Std.DHashMap.Raw.Const.modify m k f = ↑(Std.DHashMap.Internal.Raw₀.Const.modify ⟨m, ⋯⟩ k f)
-- Mathlib.CategoryTheory.SingleObj
CategoryTheory.SingleObj.functor_obj : ∀ {M : Type u} [inst : Monoid M] {C : Type v} [inst_1 : CategoryTheory.Category.{w, v} C] {X : C}
  (f : M →* CategoryTheory.End X) (x : CategoryTheory.SingleObj M), (CategoryTheory.SingleObj.functor f).obj x = X
-- Mathlib.Algebra.GroupWithZero.Defs
IsCancelMulZero.mk : ∀ {M₀ : Type u} [inst : Mul M₀] [inst_1 : Zero M₀] [toIsLeftCancelMulZero : IsLeftCancelMulZero M₀]
  [toIsRightCancelMulZero : IsRightCancelMulZero M₀], IsCancelMulZero M₀
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `self_subset_setOfPred_gauge_le_one`. -/
self_subset_gauge_le_one : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E}, s ⊆ {x | gauge s x ≤ 1}
-- Init.Data.List.Lex
List.le_total : ∀ {α : Type u_1} [inst : LT α] [i : Std.Asymm fun x1 x2 => x1 < x2] (l₁ l₂ : List α), l₁ ≤ l₂ ∨ l₂ ≤ l₁
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_int8 : ∀ (x : Int8), ↑x = x.toInt
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
/-- `coconePointwiseProduct` is invariant under isomorphisms of cocones.  -/
CategoryTheory.Limits.coconePointwiseProductIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type u_1} →
      {I : α → Type u_2} →
        [inst_1 : (i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] →
          [inst_2 : CategoryTheory.Limits.HasProductsOfShape α C] →
            (F : (i : α) → CategoryTheory.Functor (I i) C) →
              {c c' : (i : α) → CategoryTheory.Limits.Cocone (F i)} →
                ((i : α) → c i ≅ c' i) →
                  (CategoryTheory.Limits.coconePointwiseProduct c ≅ CategoryTheory.Limits.coconePointwiseProduct c')
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Regular C] {A B : C} (f : A ⟶ B)
  (A' : CategoryTheory.Subobject A) (B' : CategoryTheory.Subobject B),
  (CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation f A' B').I =
    CategoryTheory.Subobject.underlying.obj ((CategoryTheory.Subobject.exists f).obj A' ⊓ B')
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coe_ofFinsupp : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {f : α →₀ HahnSeries Γ R}, ⇑(HahnSeries.SummableFamily.ofFinsupp f) = ⇑f
-- Mathlib.Analysis.Complex.Norm
Complex.dist_eq_re_im : ∀ (z w : ℂ), dist z w = √((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2)
-- Init.Grind.AC
Lean.Grind.AC.Seq.insert.eq_def : ∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.insert x s =
    match s with
    | Lean.Grind.AC.Seq.var y =>
      if Nat.blt x y = true then Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.var y)
      else Lean.Grind.AC.Seq.cons y (Lean.Grind.AC.Seq.var x)
    | Lean.Grind.AC.Seq.cons y s =>
      if Nat.blt x y = true then Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.cons y s)
      else Lean.Grind.AC.Seq.cons y (Lean.Grind.AC.Seq.insert x s)
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Lattice.BicartSq.mk : ∀ {T : Type u} {x₁ x₂ x₃ x₄ : T} [inst : Lattice T], x₂ ⊔ x₃ = x₄ → x₂ ⊓ x₃ = x₁ → Lattice.BicartSq x₁ x₂ x₃ x₄
-- Mathlib.NumberTheory.BernoulliPolynomials
/-- The Bernoulli polynomials are defined in terms of the negative Bernoulli numbers.  -/
Polynomial.bernoulli : ℕ → Polynomial ℚ
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.next_f : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncGE]
  {j k : ι}, c.next j = k → c'.next (e.f j) = e.f k
-- Mathlib.Data.List.Nodup
List.nodup_tail_reverse : ∀ {α : Type u} (l : List α), l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.mvPolynomial_val : ∀ (R : Type u) (ι : Type w) [inst : CommRing R], (Algebra.Generators.mvPolynomial R ι).val = MvPolynomial.X
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The set of machine states reachable via downward label jumps, discounting jumps via `ret`.  -/
Turing.PartrecToTM2.trStmts₁ : Turing.PartrecToTM2.Λ' → Finset Turing.PartrecToTM2.Λ'
-- Init.Prelude
/-- The value returned from a combined state and exception monad in which exceptions do not
automatically roll back the state.

`Result ε σ α` is equivalent to `Except ε α × σ`, but using a single combined inductive type yields
a more efficient data representation.
 -/
EStateM.Result : Type u → Type u → Type u → Type u
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearEquiv.isSymmetric_symm_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E ≃ₗ[𝕜] E}, (↑T.symm).IsSymmetric ↔ (↑T).IsSymmetric
-- Lean.Expr
/-- Similar to `getArg!`, but skips mdata  -/
Lean.Expr.getArg!' : (e : Lean.Expr) → ℕ → optParam ℕ e.getAppNumArgs' → Lean.Expr
-- Mathlib.NumberTheory.MulChar.Basic
/-- The restriction of a `MulChar` to a submonoid.
 -/
MulChar.domRestrict : {R : Type u_1} →
  [inst : CommMonoid R] →
    {R' : Type u_2} →
      [inst_1 : CommMonoidWithZero R'] →
        {S : Type u_3} →
          [inst_2 : SetLike S R] → [inst_3 : SubmonoidClass S R] → (T : S) → MulChar R R' → MulChar (↥T) R'
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
MeasureTheory.Measure.MeasureDense.nonempty : ∀ {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)}, μ.MeasureDense 𝒜 → 𝒜.Nonempty
-- Mathlib.MeasureTheory.Group.ModularCharacter
MeasureTheory.Measure.modularCharacterFun_pos : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : LocallyCompactSpace G] (g : G), 0 < MeasureTheory.Measure.modularCharacterFun g
-- Lean.CoreM
Lean.Core.instMonadQuotationCoreM : Lean.MonadQuotation Lean.CoreM
-- Mathlib.NumberTheory.Ostrowski
/-- The equivalence class of an absolute value on the rationals is determined by its values on
the natural numbers.  -/
Rat.AbsoluteValue.exists_nat_rpow_iff_isEquiv : ∀ {f g : AbsoluteValue ℚ ℝ}, (∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n) ↔ f.IsEquiv g
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The inverse of a based natural transformation whose underlying natural transformation is an
isomorphism.  -/
CategoryTheory.BasedNatIso.mkNatIso : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} →
        {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} →
          (α : F.toFunctor ≅ G.toFunctor) →
            (∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (α.hom.app a)) → (F ≅ G)
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
/-- Subtracting `(qExpansion 1 f).coeff 0 • g` from `f` (where `g` has constant qExpansion 1)
gives a cusp form.  -/
ModularForm.sub_smul_isCuspForm : ∀ {k : ℤ} (f g : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k),
  (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑g) = 1 →
    (f - (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) • g).IsCuspForm
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapOpcyclesIso_inv_naturality_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasRightHomology]
  [inst_6 : S₂.HasRightHomology] [inst_7 : F.PreservesRightHomologyOf S₁] [inst_8 : F.PreservesRightHomologyOf S₂]
  {Z : D} (h : (S₂.map F).opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.opcyclesMap φ))
      (CategoryTheory.CategoryStruct.comp (S₂.mapOpcyclesIso F).inv h) =
    CategoryTheory.CategoryStruct.comp (S₁.mapOpcyclesIso F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap (F.mapShortComplex.map φ)) h)
-- Lean.Environment
/-- The declaration prefix to which the environment is restricted to, if any.  -/
Lean.Environment.asyncPrefix? : Lean.Environment → Option Lean.Name
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.eval_not : ∀ {α : Type} {a : α → Bool} {x : Std.Tactic.BVDecide.BoolExpr α},
  Std.Tactic.BVDecide.BoolExpr.eval a x.not = !Std.Tactic.BVDecide.BoolExpr.eval a x
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.add_sUnion : ∀ {α : Type u_2} [inst : Add α] (s : Set α) (T : Set (Set α)), s + ⋃₀ T = ⋃ t ∈ T, s + t
-- Mathlib.Analysis.Convex.Side
AffineSubspace.not_sSameSide_bot : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x y : P),
  ¬⊥.SSameSide x y
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR.run.eq_def : ∀ {α : Type u_1} (le : α → α → Bool) {n : ℕ} (a : { l // l.length = n }),
  List.MergeSort.Internal.mergeSortTR.run✝ le a =
    match n, a with
    | 0, ⟨[], property⟩ => []
    | 1, ⟨[a], property⟩ => [a]
    | n.succ.succ, xs =>
      match List.MergeSort.Internal.splitInTwo xs with
      | (l, r) =>
        List.MergeSort.Internal.mergeTR (List.MergeSort.Internal.mergeSortTR.run✝ le l)
          (List.MergeSort.Internal.mergeSortTR.run✝ le r) le
-- Mathlib.RingTheory.Binomial
/-- A multichoose function, giving the quotient of Pochhammer evaluations by factorials.  -/
BinomialRing.multichoose : {R : Type u_1} → {inst : AddCommMonoid R} → {inst_1 : Pow R ℕ} → [self : BinomialRing R] → R → ℕ → R
-- Batteries.Data.Array.Basic
/-- Returns the first maximal element among `d` and elements of the array.
If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered (in addition to `d`).
 -/
Array.maxWith : {α : Type u_1} → [ord : Ord α] → (xs : Array α) → α → optParam ℕ 0 → optParam ℕ xs.size → α
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.tuple.sizeOf_spec : ∀ (args : List Lean.Parser.Tactic.MRefinePat), sizeOf (Lean.Parser.Tactic.MRefinePat.tuple args) = 1 + sizeOf args
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.eq_of_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → Function.IsFixedPt (⇑f) y → x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S')
  (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
  (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
  [inst_2 : CategoryTheory.Mono i₃],
  CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁)
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂))
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂))