mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.int_rawCast_neg : ∀ {n : ℕ} {R : Type u_2} [inst : Ring R], (Int.negOfNat n).rawCast = -n.rawCast
-- Mathlib.Topology.UniformSpace.UniformEmbedding
completeSpace_ulift_iff : ∀ {α : Type u} [inst : UniformSpace α], CompleteSpace (ULift.{u_1, u} α) ↔ CompleteSpace α
-- Mathlib.Algebra.BigOperators.Finprod
finsum_true : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : True → M), ∑ᶠ (i : True), f i = f trivial
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Returns the key-value pair `(a, b)` such that `a ≥ k` for all keys in the RBMap.  -/
RBTree.RBMap.max? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → Option (α × β)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.isShared.inj : ∀ {x x_1 : Lean.IR.VarId}, Lean.IR.Expr.isShared x = Lean.IR.Expr.isShared x_1 → x = x_1
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.domDomCongrEquiv_symm_apply : ∀ {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] [inst_5 : TopologicalSpace M₂]
  [inst_6 : TopologicalSpace M₃] {ι' : Type u_1} (e : ι ≃ ι') (f : ContinuousMultilinearMap R (fun x => M₂) M₃),
  (ContinuousMultilinearMap.domDomCongrEquiv e).symm f = ContinuousMultilinearMap.domDomCongr e.symm f
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.eq_1 : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
  μ.AbsolutelyContinuous ν = ∀ ⦃s : Set α⦄, ν s = 0 → μ s = 0
-- Init.Data.BitVec.Lemmas
BitVec.le_antisymm : ∀ {n : ℕ} {x y : BitVec n}, x ≤ y → y ≤ x → x = y
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).mop =
    CategoryTheory.MonoidalCategoryStruct.rightUnitor { unmop := X }
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- A field extension `E / F` of exponential characteristic `q` is purely inseparable
if and only if for every element `x` of `E`, the minimal polynomial of `x` over `F` is of form
`(X - x) ^ (q ^ n)` for some natural number `n`.  -/
isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow : ∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [hF : ExpChar F q],
  IsPurelyInseparable F E ↔
    ∀ (x : E), ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n
-- Batteries.Lean.PersistentHashSet
/-- Insert all elements from a collection into a `PersistentHashSet`.
 -/
Lean.PersistentHashSet.insertMany : {α : Type u_1} →
  [inst : BEq α] →
    [inst_1 : Hashable α] → {ρ : Type u_2} → [ForIn Id ρ α] → Lean.PersistentHashSet α → ρ → Lean.PersistentHashSet α
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instContMDiffAddSelf : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞}, ContMDiffAdd (modelWithCornersSelf 𝕜 E) n E
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerYield : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m (Std.IterM m β)] [inst_1 : Std.Iterator α₂ m β]
  {it₁ : Std.IterM m (Std.IterM m β)} {it₂ it₂' : Std.IterM m β} {b : β},
  it₂.IsPlausibleStep (Std.IterStep.yield it₂' b) →
    Std.Iterators.Types.Flatten.IsPlausibleStep { internalState := { it₁ := it₁, it₂ := some it₂ } }
      (Std.IterStep.yield { internalState := { it₁ := it₁, it₂ := some it₂' } } b)
-- Mathlib.Algebra.FreeMonoid.Count
FreeMonoid.count.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α), FreeMonoid.count x = FreeMonoid.countP fun x_1 => x_1 = x
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_hom : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₃ : C₃ᵒᵖ} {X₂ : C₂ᵒᵖ} (g : B.op.obj X₃ ⟶ R.op.obj X₂) (f : (w.op.StructuredArrowRightwards g)ᵒᵖ),
  ((CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor w g).obj f).left.hom =
    (CategoryTheory.StructuredArrow.right (Opposite.unop f)).hom.unop
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `i` is an isomorphism such that `l ≫ i.hom = f`, the kernel of `f` is a kernel of `l`.  -/
CategoryTheory.Limits.kernel.ofCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            {Z : C} →
              (l : X ⟶ Z) →
                (i : Z ≅ Y) →
                  (h : CategoryTheory.CategoryStruct.comp l i.hom = f) →
                    CategoryTheory.Limits.IsLimit
                      (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.kernel.ι f) ⋯)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_ne_zero : ∀ {R : Type u} {a : R} [inst : Semiring R], Polynomial.C a ≠ 0 ↔ a ≠ 0
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_pow : ∀ {R : Type u_1} [inst : Ring R] (s : Subring R) (x : ↥s) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.toSubtype_π : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p)
      (CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) j) =
    CategoryTheory.Limits.biproduct.π f ↑j
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.Nonempty.of_vadd_right : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t : Finset β},
  (s +ᵥ t).Nonempty → t.Nonempty
-- Mathlib.Util.WhatsNew
/-- `#whats_new in` executes the following command and then prints the
declarations that were added to the environment.  -/
Mathlib.WhatsNew.oldStx : Lean.ParserDescr
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The distinguished short root of an embedded `𝔤₂` root pairing.  -/
RootPairing.EmbeddedG2.short : {ι : 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) → [self : P.EmbeddedG2] → ι
-- Mathlib.Algebra.Lie.SkewAdjoint
skewAdjointMatricesLieSubalgebraEquiv_apply : ∀ {R : Type u} {n : Type w} [inst : CommRing R] [inst_1 : Fintype n] (J : Matrix n n R) [inst_2 : DecidableEq n]
  (P : Matrix n n R) (h : Invertible P) (A : ↥(skewAdjointMatricesLieSubalgebra J)),
  ↑((skewAdjointMatricesLieSubalgebraEquiv J P h) A) = P⁻¹ * ↑A * P
-- Mathlib.Analysis.Quaternion
Quaternion.imK_coeComplex : ∀ (z : ℂ), (↑z).imK = 0
-- Mathlib.Algebra.Opposites
AddOpposite.eq_1 : ∀ (α : Type u_3), αᵃᵒᵖ = PreOpposite α
-- Mathlib.Algebra.GradedMonoid
List.dProd_nil : ∀ {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMonoid A] (fι : α → ι)
  (fA : (a : α) → A (fι a)), [].dProd fι fA = GradedMonoid.GOne.one
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_image_source_inter : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f f' : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H},
  ↑(f.extend I) '' (f.source ∩ f'.source) = (ModelWithCorners.extendCoordChange f f').source
-- Init.Data.String.Lemmas.TakeDrop
String.Slice.takeEnd_eq_sliceFrom : ∀ {s : String.Slice} {n : ℕ}, s.takeEnd n = s.sliceFrom (s.endPos.prevn n)
-- Lean.Elab.ConfigEval.Basic
/-- Runs `mx` using a fresh meta and term state.
This should be used around any configuration elaboration.
 -/
Lean.Elab.ConfigEval.runConfigElab : {α : Type} → Lean.Elab.TermElabM α → Lean.CoreM α
-- Mathlib.Analysis.SpecificLimits.Normed
cauchy_series_of_le_geometric : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] {C : ℝ} {u : ℕ → α} {r : ℝ},
  r < 1 → (∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n) → CauchySeq fun n => ∑ k ∈ Finset.range n, u k
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.isGood.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (l : Profinite.NobelingProof.Products I),
  Profinite.NobelingProof.Products.isGood C l =
    (Profinite.NobelingProof.Products.eval C l ∉
      Submodule.span ℤ (Profinite.NobelingProof.Products.eval C '' {m | m < l}))
-- Mathlib.GroupTheory.HNNExtension
/-- The canonical embedding `G →* HNNExtension G A B φ`  -/
HNNExtension.of : {G : Type u_1} → [inst : Group G] → {A B : Subgroup G} → {φ : ↥A ≃* ↥B} → G →* HNNExtension G A B φ
-- Init.Meta.Defs
Lean.Meta.ApplyNewGoals.nonDependentOnly : Lean.Meta.ApplyNewGoals
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_prod : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {s : Subring R} {t : Subring S}
  {p : R × S}, p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
-- Lean.Data.KVMap
Lean.KVMap.size : Lean.KVMap → ℕ
-- Mathlib.Algebra.Group.Prod
AddHom.coe_prodMap : ∀ {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [inst : Add M] [inst_1 : Add N] [inst_2 : Add M']
  [inst_3 : Add N'] (f : M →ₙ+ M') (g : N →ₙ+ N'), ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
-- Mathlib.Data.Multiset.UnionInter
Multiset.inter_le_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ∩ t ≤ t
-- Mathlib.CategoryTheory.Category.Cat.Adjunction
/-- `typeToCat : Type ⥤ Cat` is right adjoint to `connectedComponents : Cat ⥤ Type`  -/
CategoryTheory.Cat.connectedComponentsTypeToCatAdj : CategoryTheory.Cat.connectedComponents ⊣ CategoryTheory.typeToCat
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_vadd`. -/
EMetric.infEdist_vadd : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {M : Type u_2} [inst_1 : VAdd M α] [IsIsometricVAdd M α] (c : M) (x : α)
  (s : Set α), Metric.infEDist (c +ᵥ x) (c +ᵥ s) = Metric.infEDist x s
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.functor.eq_1 : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C),
  CategoryTheory.Discrete.functor F =
    { obj := F ∘ CategoryTheory.Discrete.as,
      map := fun {X Y} f => id (ULift.casesOn f fun down => PLift.casesOn down fun h => CategoryTheory.eqToHom ⋯),
      map_id := ⋯, map_comp := ⋯ }
-- Init.Data.Nat.Div.Lemmas
Nat.succ_div_of_mod_eq_zero : ∀ {a b : ℕ}, (a + 1) % b = 0 → (a + 1) / b = a / b + 1
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.mkHom_id_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e : C ≌ D},
  CategoryTheory.Equivalence.mkHom (CategoryTheory.CategoryStruct.id e.inverse) =
    CategoryTheory.CategoryStruct.id e.symm
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.le_pow_iff_log_le : ∀ {x y : ℝ} {n : ℕ}, 0 < x → 0 < y → (x ≤ y ^ n ↔ Real.log x ≤ ↑n * Real.log y)
-- Mathlib.Logic.Function.Defs
/-- Sends a dependent function `a : ∀ i, α i` to a dependent function `Pi.map f a : ∀ i, β i`
by applying `f i` to `i`-th component.  -/
Pi.map : {ι : Sort u_1} → {α : ι → Sort u_2} → {β : ι → Sort u_3} → ((i : ι) → α i → β i) → ((i : ι) → α i) → (i : ι) → β i
-- Mathlib.Topology.Spectral.Prespectral
IsPreirreducible.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X),
  IsPreirreducible s =
    ∀ (u v : Set X), IsOpen u → IsOpen v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
-- Lean.Parser.Term
Lean.Parser.Term.falseVal : Lean.Parser.Parser
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
max_add_add_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α] [AddLeftMono α] (a b c : α), max (a + b) (a + c) = a + max b c
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_opMap_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.ShortComplex.opMap φ) ↔ CategoryTheory.ShortComplex.QuasiIso φ
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.comapRight_compProd_id_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {δ : Type u_4} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η]
  {f : δ → γ} (hf : MeasurableEmbedding f), (κ.compProd η).comapRight ⋯ = κ.compProd (η.comapRight hf)
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a complete distributive lattice
with possibly different definitional equalities.  -/
CompleteDistribLattice.copy : {α : Type u} →
  (c : CompleteDistribLattice α) →
    (le : α → α → Prop) →
      le = LE.le →
        (top : α) →
          top = ⊤ →
            (bot : α) →
              bot = ⊥ →
                (sup : α → α → α) →
                  sup = max →
                    (inf : α → α → α) →
                      inf = min →
                        (sdiff : α → α → α) →
                          sdiff = SDiff.sdiff →
                            (hnot : α → α) →
                              hnot = HNot.hnot →
                                (himp : α → α → α) →
                                  himp = HImp.himp →
                                    (compl : α → α) →
                                      compl = Compl.compl →
                                        (sSup : Set α → α) →
                                          sSup = SupSet.sSup →
                                            (sInf : Set α → α) → sInf = InfSet.sInf → CompleteDistribLattice α
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.findEndSectionCompletionCandidates : Array String → Array String → Array String
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.sSup_apply : ∀ {α : Type u_1} (ms : Set (MeasureTheory.OuterMeasure α)) (s : Set α), (sSup ms) s = ⨆ m ∈ ms, m s
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.notCore : Lean.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.mk : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.natDegree = n → p.Monic → p.IsMonicOfDegree n
-- Mathlib.Data.List.Cycle
List.prev.eq_3 : ∀ {α : Type u_1} [inst : DecidableEq α] (x y z : α) (xs : List α) (x_1 : x ∈ y :: z :: xs),
  (y :: z :: xs).prev x x_1 = if hx : x = y then (z :: xs).getLast ⋯ else if x = z then y else (z :: xs).prev x ⋯
-- Mathlib.Analysis.InnerProductSpace.Adjoint
IsSelfAdjoint.adjoint_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {A : E →L[𝕜] E}, IsSelfAdjoint A → ContinuousLinearMap.adjoint A = A
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- Every functor `F` to a codiscrete category is naturally isomorphic (actually, equal) to
`Codiscrete.as ∘ F.obj`.  -/
CategoryTheory.Codiscrete.natIsoFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} →
      {F : CategoryTheory.Functor C (CategoryTheory.Codiscrete A)} →
        F ≅ CategoryTheory.Codiscrete.functor (CategoryTheory.Codiscrete.as ∘ F.obj)
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldInfo.mk.injEq : ∀ (projName fieldName : Lean.Name) (lctx : Lean.LocalContext) (val : Lean.Expr) (stx : Lean.Syntax)
  (projName_1 fieldName_1 : Lean.Name) (lctx_1 : Lean.LocalContext) (val_1 : Lean.Expr) (stx_1 : Lean.Syntax),
  ({ projName := projName, fieldName := fieldName, lctx := lctx, val := val, stx := stx } =
      { projName := projName_1, fieldName := fieldName_1, lctx := lctx_1, val := val_1, stx := stx_1 }) =
    (projName = projName_1 ∧ fieldName = fieldName_1 ∧ lctx = lctx_1 ∧ val = val_1 ∧ stx = stx_1)
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The isomorphism between the free group on a unique type and the integers.  -/
FreeGroup.mulEquivIntOfUnique : {α : Type u} → [Unique α] → FreeGroup α ≃* Multiplicative ℤ
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.State.mk : Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Expr → Lean.PHashSet Lean.Meta.Sym.AlphaKey → Lean.Meta.Sym.State✝
-- Mathlib.MeasureTheory.Measure.AEMeasurable
MeasureTheory.Measure.map_finset_sum' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {ι : Type u_7} {β : Type u_8} [inst : Fintype ι] {mβ : MeasurableSpace β}
  {m : ι → MeasureTheory.Measure α} {f : α → β},
  AEMeasurable f (∑ i, m i) → MeasureTheory.Measure.map f (∑ i, m i) = ∑ i, MeasureTheory.Measure.map f (m i)
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
uliftMultiplesHom_symm_apply : ∀ (M : Type u) [inst : AddMonoid M] (a : ULift.{u, 0} ℕ →+ M), (uliftMultiplesHom M).symm a = a (AddEquiv.ulift.symm 1)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_eq_psi_coe_floor : ∀ (x : ℝ), Chebyshev.psi x = Chebyshev.psi ↑⌊x⌋₊
-- Init.Data.SInt.Lemmas
Int32.toInt16_toISize : ∀ (n : Int32), n.toISize.toInt16 = n.toInt16
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.top_lowerCentralSeries_one : ∀ {G : Type u_1} [inst : AddGroup G], ⊤.lowerCentralSeries 1 = addCommutator G
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_eq_fallback : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α},
  a ∉ m → m.getD a fallback = fallback
-- Std.Http.Internal.Char
Std.Http.Internal.Char.vchar.eq_1 : ∀ (c : Char), Std.Http.Internal.Char.vchar c = decide (c ≥ '!' ∧ c ≤ '~')
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.instOverXPullbackCoverOver' : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      (j : 𝒰.I₀) → ((AlgebraicGeometry.Scheme.Cover.pullbackCoverOver' S 𝒰 f).X j).Over S
-- Mathlib.Algebra.Order.Sub.Defs
tsub_le_tsub_right : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b : α},
  a ≤ b → ∀ (c : α), a - c ≤ b - c
-- Init.Data.Char.Basic
/-- Returns `true` if the character is an ASCII letter.

The ASCII letters are the following: `ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz`.
 -/
Char.isAlpha : Char → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₀_app_snd_apply : ∀ {X : SSet} {m : ℕ} (x : X.obj (Opposite.op { len := m })) (k : Fin (m + 1)),
  ((CategoryTheory.ConcreteCategory.hom (SSet.ι₀.app (Opposite.op { len := m }))) x).2 k = 0
-- Mathlib.Algebra.Group.Units.Basic
Units.eq_mul_inv_iff_mul_eq : ∀ {α : Type u} [inst : Monoid α] (c : αˣ) {a b : α}, a = b * ↑c⁻¹ ↔ a * ↑c = b
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_subset_closure_iff_subset_closure : ∀ {α : Type u_2} {M : Matroid α} {X Y : Set α},
  autoParam (X ⊆ M.E) Matroid.closure_subset_closure_iff_subset_closure._auto_1 →
    (M.closure X ⊆ M.closure Y ↔ X ⊆ M.closure Y)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- An ideal of `R` is not the whole ring if and only if it is contained in an element of
`HeightOneSpectrum R`  -/
IsDedekindDomain.HeightOneSpectrum.ideal_ne_top_iff_exists : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R], ¬IsField R → ∀ (I : Ideal R), I ≠ ⊤ ↔ ∃ P, I ≤ P.asIdeal
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
neg_of_slope_pos : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {f : 𝕜 → 𝕜} {x₀ b : 𝕜},
  b < x₀ → 0 < slope f x₀ b → f x₀ = 0 → f b < 0
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindexFinsetRange.eq_1 : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) [inst_3 : Fintype ι] [inst_4 : DecidableEq M],
  b.reindexFinsetRange = b.reindexRange.reindex ((Equiv.refl M).subtypeEquiv ⋯)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w),
  (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph
-- Mathlib.Analysis.Asymptotics.Defs
/-- Definition of `IsBigOWith`. We record it in a lemma as `IsBigOWith` is irreducible.  -/
Asymptotics.isBigOWith_iff : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  {l : Filter α}, Asymptotics.IsBigOWith c l f g ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUInt64HAndNegOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 &&& x2) (-1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.empty_equiv_iff_isEmpty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m.WF → (∅.Equiv m ↔ m.isEmpty = true)
-- Lean.Server.ServerTask
Lean.Server.ServerTask.IO.mapTaskCheap : {α : Type u_1} →
  {β : Type} → (α → IO β) → Lean.Server.ServerTask α → BaseIO (Lean.Server.ServerTask (Except IO.Error β))
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.integrate.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A] [inst_10 : BorelSpace A] (μA : MeasureTheory.Measure A)
  [hμA : μA.IsHaarMeasure] [inst_11 : NormedSpace ℝ E] [inst_12 : IsTopologicalGroup C]
  [inst_13 : LocallyCompactSpace B] [inst_14 : MeasurableSpace C] [inst_15 : BorelSpace C]
  (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure],
  H.integrate μA μC = { toFun := fun f => ∫ (c : C), ((H.pushforward μA) f) c ∂μC, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.RepresentationTheory.Coinvariants
/-- The functor sending a representation to its coinvariants.  -/
Rep.coinvariantsFunctor : (k : Type u) →
  (G : Type v) → [inst : CommRing k] → [inst_1 : Monoid G] → CategoryTheory.Functor (Rep.{w, u, v} k G) (ModuleCat k)
-- Mathlib.Analysis.Convex.Combination
Finset.centroid_mem_convexHull : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (s : Finset E),
  s.Nonempty → Finset.centroid R s id ∈ (convexHull R) ↑s