mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Impl.treeSize.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β),
  x.treeSize =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf => 0
    | Std.DTreeMap.Internal.Impl.inner size k v l r => 1 + l.treeSize + r.treeSize
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.circularOrder : {α : Type u_1} →
  [inst : AddCommGroup α] →
    [inst_1 : LinearOrder α] →
      [IsOrderedAddMonoid α] →
        [hα : Archimedean α] → {p : α} → [hp' : Fact (0 < p)] → CircularOrder (α ⧸ AddSubgroup.zmultiples p)
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.map_continuousOn : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {F : Set X},
  JoinedIn F x y → ∀ {f : X → Y}, ContinuousOn f F → JoinedIn (f '' F) (f x) (f y)
-- Mathlib.Topology.Constructions
Pi.continuous_precomp' : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {ι' : Type u_9} (φ : ι' → ι),
  Continuous fun f j => f (φ j)
-- Mathlib.Logic.Equiv.PartialEquiv
Set.BijOn.toPartialEquiv_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : α → β) (s : Set α) (t : Set β) (hf : Set.BijOn f s t),
  ↑(Set.BijOn.toPartialEquiv f s t hf).symm = Function.invFunOn f s
-- Init.SimpLemmas
Bool.and_self : ∀ (b : Bool), (b && b) = b
-- Mathlib.Order.Hom.Lattice
InfHom.coe_top : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] [inst_2 : Top β], ⇑⊤ = ⊤
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.coe_curry_symm : ∀ (ι : Type u_6) (κ : Type u_7) (X : Type u_8) [inst : MeasurableSpace X],
  ⇑(MeasurableEquiv.curry ι κ X).symm = Function.uncurry
-- Mathlib.Probability.Kernel.MeasurableLIntegral
Measurable.lintegral_kernel_prod_left' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {f : β × α → ENNReal},
  Measurable f → Measurable fun y => ∫⁻ (x : β), f (x, y) ∂κ y
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_ediv_iff_mul_dvd : ∀ {a b c : ℤ}, c ∣ b → (a ∣ b / c ↔ c * a ∣ b)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.opObjEquiv_apply : ∀ {d n : ℕ} (f : (SSet.stdSimplex.obj { len := n }).op.obj (Opposite.op { len := d })) (i : Fin (d + 1)),
  (SSet.stdSimplex.opObjEquiv f) i = ((SSet.opObjEquiv f) i.rev).rev
-- Std.Data.Internal.List.Associative
Std.Internal.List.forIn_eq_forIn_keys : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m']
  {f : α → δ → m' (ForInStep δ)} {init : δ} {l : List ((a : α) × β a)},
  (forIn l init fun a d => f a.fst d) = forIn (Std.Internal.List.keys l) init f
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceSucc : Lean.Meta.Simp.DSimproc
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {len : ℕ} →
        (aig : Std.Sat.AIG α) →
          aig.BinaryRefVec len →
            (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) →
              [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func] →
                [Std.Sat.AIG.RefVec.LawfulZipOperator α func] → Std.Sat.AIG.RefVecEntry α len
-- Mathlib.RingTheory.Algebraic.Denominator
Algebra.isIntegral_denominator_smul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsPrincipalIdealRing R] [inst_2 : CommRing S]
  [inst_3 : Algebra R S] (x : S), IsIntegral R (Algebra.denominator R x • x)
-- Mathlib.ModelTheory.DirectLimit
/-- The direct limit of countably many countably generated structures is countably generated.  -/
FirstOrder.Language.DirectLimit.cg : ∀ {L : FirstOrder.Language} {ι : Type u_1} [Countable ι] [inst : Preorder ι] [inst_1 : IsDirectedOrder ι]
  [inst_2 : Nonempty ι] {G : ι → Type w} [inst_3 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)),
  (∀ (i : ι), FirstOrder.Language.Structure.CG L (G i)) →
    ∀ [inst_4 : DirectedSystem G fun i j h => ⇑(f i j h)],
      FirstOrder.Language.Structure.CG L (FirstOrder.Language.DirectLimit G f)
-- Mathlib.Order.Monotone.Basic
MonotoneOn.strictMonoOn_of_injOn : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : PartialOrder β] {f : α → β} {s : Set α},
  MonotoneOn f s → Set.InjOn f s → StrictMonoOn f s
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k fallback : α},
  k ∈ m → (m.insertManyIfNewUnit l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.GroupTheory.Congruence.Defs
/-- In order to define a function `(Con.Quotient c)ˣ → α` on the units of `Con.Quotient c`,
where `c : Con M` is a multiplicative congruence on a monoid, it suffices to define a function `f`
that takes elements `x y : M` with proofs of `c (x * y) 1` and `c (y * x) 1`, and returns an element
of `α` provided that `f x y _ _ = f x' y' _ _` whenever `c x x'` and `c y y'`.  -/
AddCon.liftOnAddUnits : {M : Type u_1} →
  {α : Type u_4} →
    [inst : AddMonoid M] →
      {c : AddCon M} →
        AddUnits c.Quotient →
          (f : (x y : M) → c (x + y) 0 → c (y + x) 0 → α) →
            (∀ (x y : M) (hxy : c (x + y) 0) (hyx : c (y + x) 0) (x' y' : M) (hxy' : c (x' + y') 0)
                (hyx' : c (y' + x') 0), c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx') →
              α
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.relabel.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (g : α → β) (x : L.Term α),
  FirstOrder.Language.Term.relabel g x =
    match x with
    | FirstOrder.Language.var i => FirstOrder.Language.var (g i)
    | FirstOrder.Language.func f ts => FirstOrder.Language.func f fun {i} => FirstOrder.Language.Term.relabel g (ts i)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonNatTrans.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [inst_5 : F'.LaxMonoidal] (f : F ⟶ F')
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal f],
  CategoryTheory.Functor.mapMonNatTrans f =
    { app := fun X => CategoryTheory.Mon.Hom.mk' (f.app X.X) ⋯ ⋯, naturality := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.zero_add_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.AddMonObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.zero X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom h
-- Mathlib.Algebra.Lie.TensorProduct
TensorProduct.LieModule.lift_apply : ∀ (R : Type u) [inst : CommRing R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] [inst_11 : AddCommGroup P] [inst_12 : Module R P] [inst_13 : LieRingModule L P]
  [inst_14 : LieModule R L P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N),
  ((TensorProduct.LieModule.lift R L M N P) f) (m ⊗ₜ[R] n) = (f m) n
-- Mathlib.Topology.Algebra.Monoid
AddSubmonoid.topologicalClosure.eq_1 : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : SeparatelyContinuousAdd M]
  (s : AddSubmonoid M), s.topologicalClosure = { carrier := closure ↑s, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_list_count : ∀ {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq M] (s : List M),
  s.sum = ∑ m ∈ s.toFinset, List.count m s • m
-- Mathlib.Tactic.FieldSimp
/-- Given two terms `l₁`, `l₂` of type `qNF M`, i.e. lists of `(ℤ × Q($M)) × ℕ`s (an integer, an
`Expr` and a natural number), construct another such term `l`, which will have the property that in
the field `$M`, the product of the "multiplicative linear combinations" represented by `l₁` and
`l₂` is the multiplicative linear combination represented by `l`.

The construction assumes, to be valid, that the lists `l₁` and `l₂` are in strictly decreasing order
by `ℕ`-component, and that if pairs `(a₁, x₁)` and `(a₂, x₂)` appear in `l₁`, `l₂` respectively with
the same `ℕ`-component `k`, then the expressions `x₁` and `x₂` are equal.

The construction is as follows: merge the two lists, except that if pairs `(a₁, x₁)` and `(a₂, x₂)`
appear in `l₁`, `l₂` respectively with the same `ℕ`-component `k`, then contribute a term
`(a₁ + a₂, x₁)` to the output list with `ℕ`-component `k`.  -/
Mathlib.Tactic.FieldSimp.qNF.mul : {v : Lean.Level} →
  {M : Q(Type v)} →
    Mathlib.Tactic.FieldSimp.qNF q(«$M») → Mathlib.Tactic.FieldSimp.qNF q(«$M») → Mathlib.Tactic.FieldSimp.qNF q(«$M»)
-- Mathlib.Tactic.Linter.EmptyLine
/-- The "emptyLine" linter emits a warning on empty lines inside a command, but outside of a
doc-string/module-doc.

The linter is only active when there are no other warnings, so as to not add noise when developing
incomplete proofs.
 -/
Mathlib.Linter.EmptyLine.emptyLineLinter : Lean.Linter
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.cos_arcsin : ∀ (x : ℝ), Real.cos (Real.arcsin x) = √(1 - x ^ 2)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
/-- Given a `k`-linear `G`-representation `A`, this is the complex of inhomogeneous cochains
$$0 \to \mathrm{Fun}(G^0, A) \to \mathrm{Fun}(G^1, A) \to \mathrm{Fun}(G^2, A) \to \dots$$
which calculates the group cohomology of `A`.  -/
groupCohomology.inhomogeneousCochains : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → CochainComplex (ModuleCat k) ℕ
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.commute : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] [FaithfulSMul M X]
  {P Q : M}, IsLprojection X P → IsLprojection X Q → Commute P Q
-- Mathlib.Data.Nat.Choose.Multinomial
Finset.sum_pow : ∀ {α : Type u_1} {R : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring R] {s : Finset α} (x : α → R) (n : ℕ),
  s.sum x ^ n = ∑ k ∈ s.sym n, ↑(↑k).countPerms * (Multiset.map x ↑k).prod
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.of_comp_iso : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {b' : 𝒳}
  (φ' : b ≅ b') [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ'.hom],
  p.IsCartesian f (CategoryTheory.CategoryStruct.comp φ φ'.hom)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_empty_eq_ground_iff : ∀ {α : Type u_2} {M : Matroid α}, M.closure ∅ = M.E ↔ M = Matroid.loopyOn M.E
-- Aesop.RuleTac.GoalDiff
Aesop.getNewFVars : Lean.MVarId → Lean.LocalContext → Lean.LocalContext → Lean.MetaM (Std.HashSet Lean.FVarId)
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.mk.inj : ∀ {R : Type u} {inst : CommSemiring R} {A : Type v} {B : Type w} {inst_1 : Semiring A} {inst_2 : Semiring B}
  {inst_3 : Algebra R A} {inst_4 : Algebra R B} {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B}
  {toCoalgEquiv : A ≃ₗc[R] B}
  {map_mul' : ∀ (x y : A), toCoalgEquiv.toFun (x * y) = toCoalgEquiv.toFun x * toCoalgEquiv.toFun y}
  {toCoalgEquiv_1 : A ≃ₗc[R] B}
  {map_mul'_1 : ∀ (x y : A), toCoalgEquiv_1.toFun (x * y) = toCoalgEquiv_1.toFun x * toCoalgEquiv_1.toFun y},
  { toCoalgEquiv := toCoalgEquiv, map_mul' := map_mul' } = { toCoalgEquiv := toCoalgEquiv_1, map_mul' := map_mul'_1 } →
    toCoalgEquiv = toCoalgEquiv_1
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.toOrderHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : PseudoEpimorphism α β),
  ⇑f.toOrderHom = ⇑f
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.mclosure_isSwap : ∀ {α : Type u} [inst : DecidableEq α] [Finite α], Submonoid.closure {σ | σ.IsSwap} = ⊤
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.mulL.inj : ∀ {k : ℕ} {a : Nat.Internal.Linear.Expr} {k_1 : ℕ} {a_1 : Nat.Internal.Linear.Expr},
  Nat.Internal.Linear.Expr.mulL k a = Nat.Internal.Linear.Expr.mulL k_1 a_1 → k = k_1 ∧ a = a_1
-- Mathlib.Data.Array.Defs
Array.cyclicPermute!.cyclicPermuteAux : {α : Type u} → Array α → List ℕ → α → ℕ → Array α
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiable_of_mdifferentiableOn_union_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s t : Set M},
  MDiff[s] f → MDiff[t] f → s ∪ t = Set.univ → IsOpen s → IsOpen t → MDiff f
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.regularizedHGFunCoeff_eq_zero_left : ∀ (a b : Multiset ℂ) (n m : ℕ),
  autoParam (-↑m ∈ a) Complex.regularizedHGFunCoeff_eq_zero_left._auto_1 →
    autoParam (m < n) Complex.regularizedHGFunCoeff_eq_zero_left._auto_3 → Complex.regularizedHGFunCoeff a b n = 0
-- Init.Data.FloatArray.Basic
FloatArray.data : FloatArray → Array Float
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
/-- Any (locally-closed) immersion can be factored into
a closed immersion followed by a (dominant) open immersion.
 -/
AlgebraicGeometry.Scheme.Hom.liftCoborder_ι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsImmersion f] {Z : AlgebraicGeometry.Scheme}
  (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.liftCoborder f)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.coborderRange f).ι h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.comp_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {R S T : CategoryTheory.AddGrp C} (f : R ⟶ S) (g : S ⟶ T),
  (CategoryTheory.CategoryStruct.comp f g).hom.hom = CategoryTheory.CategoryStruct.comp f.hom.hom g.hom.hom
-- Init.Data.Int.DivMod.Lemmas
Int.sub_mul_fmod_self_right : ∀ (a b c : ℤ), (a - b * c).fmod c = a.fmod c
-- Mathlib.AlgebraicGeometry.Morphisms.LocalIso
AlgebraicGeometry.IsLocalIso.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsLocalIso
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mkPiAlgebraFin_apply : ∀ {R : Type u} {n : ℕ} {A : Type u_1} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace A] [inst_4 : ContinuousMul A] (m : Fin n → A),
  (ContinuousMultilinearMap.mkPiAlgebraFin R n A) m = (List.ofFn m).prod
-- Lean.Meta.HaveTelescope
/-- The type of `expr`. It may contain loose bound variables like in the `expr` field.
Used in proof construction.
 -/
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.SimpHaveResult.exprType : Lean.Meta.SimpHaveResult✝ → Lean.Expr
-- Init.Data.Range.Polymorphic.UInt
USize.instLawfulHasSize_1 : Std.Rxo.LawfulHasSize USize
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.ι_map_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C), ⊤.map P.ι = P.isoClosure
-- Mathlib.RingTheory.Multiplicity
multiplicity_pow_self_of_prime : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p : α},
  Prime p → ∀ (n : ℕ), multiplicity p (p ^ n) = n
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.MonoidalCategoryAux.tensorHom_toLinearMap : ∀ {R : Type u} [inst : CommRing R] {M N P Q : Type u} [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : AddCommGroup P] [inst_4 : AddCommGroup Q] [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P]
  [inst_8 : Module R Q] [inst_9 : Coalgebra R M] [inst_10 : Coalgebra R N] [inst_11 : Coalgebra R P]
  [inst_12 : Coalgebra R Q] (f : M →ₗc[R] N) (g : P →ₗc[R] Q),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom (CoalgCat.ofHom f) (CoalgCat.ofHom g)).toCoalgHom'.toLinearMap =
    TensorProduct.map f.toLinearMap g.toLinearMap
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instSDiffOfBEqOfHashable : {α : Type u} → [BEq α] → [Hashable α] → SDiff (Std.HashSet.Raw α)
-- Mathlib.Topology.Category.TopCat.Sphere
/-- `𝔻 n` denotes the `n`-disk.  -/
TopCat.term𝔻_ : Lean.ParserDescr
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.explicitBinderF : Lean.Parser.Parser
-- Mathlib.RingTheory.LocalRing.ResidueField.Defs
/-- The quotient map from a local ring to its residue field.  -/
IsLocalRing.residue : (R : Type u_1) → [inst : CommRing R] → [inst_1 : IsLocalRing R] → R →+* IsLocalRing.ResidueField R
-- Init.Data.List.Monadic
List.zipWithM'_eq_zipWithM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} [inst : Monad m] [LawfulMonad m]
  {f : α → β → m γ} {l : List α} {l' : List β}, List.zipWithM' f l l' = List.zipWithM f l l'
-- Batteries.Tactic.Alias
/-- The command `alias name := target` creates a synonym of `target` with the given name.

The command `alias ⟨fwd, rev⟩ := target` creates synonyms for the forward and reverse directions
of an iff theorem. Use `_` if only one direction is required.

These commands accept all modifiers and attributes that `def` and `theorem` do.
 -/
Batteries.Tactic.Alias.alias : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.mk_Iio_lt : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (i : α),
  ((Cardinal.mk α).ord = Ordinal.type fun x1 x2 => x1 < x2) → Cardinal.mk ↑(Set.Iio i) < Cardinal.mk α
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.instIsIsoSchemeMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : Y.Opens), CategoryTheory.IsIso (f ∣_ U)
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The identity functor on `C`, viewed as a functor from `C` to its monoidal opposite.  -/
CategoryTheory.mopFunctor : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor C Cᴹᵒᵖ
-- Mathlib.CategoryTheory.ObjectProperty.Ind
_private.Mathlib.CategoryTheory.ObjectProperty.Ind.0.CategoryTheory.ObjectProperty.ind_pi_of_ind : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {ι : Type w}
  [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete ι)] [inst_2 : CategoryTheory.Limits.HasProductsOfShape ι C]
  [CategoryTheory.Limits.IsIPCOfShape.{w, w, v, u} ι C] {X : ι → C}, (∀ (i : ι), P.ind (X i)) → P.ind (∏ᶜ X)
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {a : α} {b : β},
  t.WF → (t.insertIfNew a b).WF
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.card_le_card_biUnion : ∀ {ι : Type u_1} {α : Type u_2} [inst : DecidableEq α] {s : Finset ι} {f : ι → Finset α},
  (↑s).PairwiseDisjoint f → (∀ i ∈ s, (f i).Nonempty) → s.card ≤ (s.biUnion f).card
-- Init.Data.String.Basic
String.startInclusive_sliceFrom : ∀ {s : String} {p : s.Pos}, (s.sliceFrom p).startInclusive = p
-- Mathlib.Analysis.Complex.Exponential
Real.exp_le_exp_of_le : ∀ {x y : ℝ}, x ≤ y → Real.exp x ≤ Real.exp y
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Avoid using this. Use the isomorphism `AlgebraicGeometry.Scheme.Modules.restrictAppIso`
instead.  -/
AlgebraicGeometry.Scheme.Modules.restrict_map : ∀ {X Y : AlgebraicGeometry.Scheme} (M : Y.Modules) (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f]
  {U V : TopologicalSpace.Opens ↥X} (i : U ⟶ V),
  (M.restrict f).presheaf.map i.op = M.presheaf.map ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).map i).op
-- Lean.Parser.StrInterpolation
_private.Lean.Parser.StrInterpolation.0.Lean.Parser.interpolatedStrFn.parse : Lean.Parser.ParserFn →
  ℕ → String.Pos.Raw → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsUnramified.eq : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsUnramified k w → (w.comap (algebraMap k K)).mult = w.mult
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When a short complex has homology, its homology can be computed using
any left homology data.  -/
CategoryTheory.ShortComplex.LeftHomologyData.homologyIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → (h : S.LeftHomologyData) → [inst_2 : S.HasHomology] → S.homology ≅ h.H
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_maxKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {km : α}, t.maxKey? = some km → t.getKey? km = some km
-- Mathlib.Algebra.Group.Translate
translate_comm : ∀ {α : Type u_2} {G : Type u_5} [inst : AddCommGroup G] (a b : G) (f : G → α),
  translate a (translate b f) = translate b (translate a f)
-- Mathlib.RingTheory.Flat.Rank
PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Module.Finite R S] (p : PrimeSpectrum R),
  0 < Module.rankAtStalk S p ↔ p ∈ Set.range (PrimeSpectrum.comap (algebraMap R S))
-- Std.Http.Data.URI.Basic
Std.Http.URI.instToStringHost : ToString Std.Http.URI.Host
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
SimpleGraph.lineGraph_bot : ∀ {V : Type u_1}, ⊥.lineGraph = ⊥
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ActionToRep_obj_ρ : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] (X : Action (ModuleCat k) G),
  ((Rep.ActionToRep k G).obj X).ρ = X.V.endRingEquiv.toMonoidHom.comp X.ρ
-- Mathlib.Geometry.Manifold.PoincareConjecture
_private.Mathlib.Geometry.Manifold.PoincareConjecture.0.termℝ__ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.Sieves
/-- For all arrows `f` and `g` in `R`, the pullback of `f` and `g` exists.  -/
CategoryTheory.Presieve.HasPairwisePullbacks.has_pullbacks : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X : C} {R : CategoryTheory.Presieve X}
  [self : R.HasPairwisePullbacks] {Y Z : C} {f : Y ⟶ X},
  R f → ∀ {g : Z ⟶ X}, R g → CategoryTheory.Limits.HasPullback f g
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_inv_nhdsGE_inv : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousInv H] {a : H}, Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Ici a⁻¹)) (nhdsWithin a (Set.Iic a))
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.instIsCocontinuousOverForgetOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C),
  (CategoryTheory.Over.forget X).IsCocontinuous (J.over X) J
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.trans : ∀ {α : Type u} {β : α → Type v} {t₁ t₂ t₃ : Std.DTreeMap.Internal.Impl α β}, t₁.Equiv t₂ → t₂.Equiv t₃ → t₁.Equiv t₃