mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.Const.alter.eq_def : ∀ {α : Type u} [inst : BEq α] {β : Type v} (a : α) (f : Option β → Option β)
  (x : Std.DHashMap.Internal.AssocList α fun x => β),
  Std.DHashMap.Internal.AssocList.Const.alter a f x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil =>
      match f none with
      | none => Std.DHashMap.Internal.AssocList.nil
      | some b => Std.DHashMap.Internal.AssocList.cons a b Std.DHashMap.Internal.AssocList.nil
    | Std.DHashMap.Internal.AssocList.cons k v l =>
      if (k == a) = true then
        match f (some v) with
        | none => l
        | some b => Std.DHashMap.Internal.AssocList.cons a b l
      else
        have tail := Std.DHashMap.Internal.AssocList.Const.alter a f l;
        Std.DHashMap.Internal.AssocList.cons k v tail
-- Mathlib.Algebra.QuadraticAlgebra.Defs
/-- The equivalence between quadratic algebra over `R` and `R × R`.  -/
QuadraticAlgebra.equivProd : {R : Type u_1} → (a b : R) → QuadraticAlgebra R a b ≃ R × R
-- Mathlib.Data.Finset.Basic
Finset.insert_erase_subset : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), s ⊆ insert a (s.erase a)
-- Mathlib.Algebra.MonoidAlgebra.Support
/-- **Alias** of `MonoidAlgebra.support_coeff_one_subset`. -/
MonoidAlgebra.support_one_subset : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : One G], (MonoidAlgebra.coeff 1).support ⊆ 1
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.aeval_ne_zero_of_isCoprime : ∀ {S : Type v} {R : Type u_1} [inst : CommSemiring R] [Nontrivial S] [inst_2 : Semiring S] [inst_3 : Algebra R S]
  {p q : Polynomial R}, IsCoprime p q → ∀ (s : S), (Polynomial.aeval s) p ≠ 0 ∨ (Polynomial.aeval s) q ≠ 0
-- Mathlib.Algebra.Order.Interval.Basic
Interval.one_ne_bot : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : One α], 1 ≠ ⊥
-- Mathlib.Data.Sum.Basic
Sum.LiftRel.isLeft_congr : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ},
  Sum.LiftRel r s x y → (x.isLeft = true ↔ y.isLeft = true)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castAdd_Ioo : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m '' Set.Ioo i j = Set.Ioo (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject.Split C) (n : ℕ),
  (CategoryTheory.SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app X).f.f n =
    X.s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n }))
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- `Multipliable f` means that `f` has some (infinite) product with respect to `L`. Use `tprod` to
get the value.  -/
Multipliable : {α : Type u_1} →
  {β : Type u_2} →
    [CommMonoid α] →
      [TopologicalSpace α] → (β → α) → optParam (SummationFilter β) (SummationFilter.unconditional β) → Prop
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgSemiHomClass.toMulHomClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} {inst : Monoid R} {inst_1 : Monoid S}
  {φ : outParam (R →* S)} {A : outParam (Type u_4)} {B : outParam (Type u_5)} {inst_2 : NonUnitalNonAssocSemiring A}
  {inst_3 : NonUnitalNonAssocSemiring B} {inst_4 : DistribMulAction R A} {inst_5 : DistribMulAction S B}
  {inst_6 : FunLike F A B} [self : NonUnitalAlgSemiHomClass F φ A B], MulHomClass F A B
-- Aesop.Tree.Data
Aesop.Goal.addedInIteration : Aesop.Goal → Aesop.Iteration
-- Mathlib.Order.PiLex
Pi.instNoMinOrderLexForallOfWellFoundedLTOfNonempty : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] [WellFoundedLT ι] [Nonempty ι]
  [inst_3 : (i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMinOrder (β i)], NoMinOrder (Lex ((i : ι) → β i))
-- Mathlib.Algebra.Algebra.Unitization
Unitization.algHom_ext : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring S] [inst_1 : CommSemiring R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : Module R A] [inst_4 : SMulCommClass R A A] [inst_5 : IsScalarTower R A A]
  {B : Type u_4} [inst_6 : Semiring B] [inst_7 : Algebra S B] [inst_8 : Algebra S R] [inst_9 : DistribMulAction S A]
  [inst_10 : IsScalarTower S R A] {F : Type u_6} [inst_11 : FunLike F (Unitization R A) B]
  [AlgHomClass F S (Unitization R A) B] {φ ψ : F},
  (∀ (a : A), φ ↑a = ψ ↑a) →
    (∀ (r : R), φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)) → φ = ψ
-- Mathlib.Data.PNat.Xgcd
PNat.instInhabitedXgcdType.default : PNat.XgcdType
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.coe_top : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], ↑⊤ = Set.univ
-- Init.Data.List.Monadic
List.forIn'_congr : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {as bs : List α} (w : as = bs) {b b' : β},
  b = b' →
    ∀ {f : (a' : α) → a' ∈ as → β → m (ForInStep β)} {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)},
      (∀ (a : α) (m_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b) → forIn' as b f = forIn' bs b' g
-- Mathlib.Computability.Reduce
manyOneEquiv_toNat : ∀ {α : Type u} [inst : Primcodable α] [inst_1 : Inhabited α] {β : Type v} [inst_2 : Primcodable β]
  [inst_3 : Inhabited β] (p : Set α) (q : Set β), ManyOneEquiv (toNat p) (toNat q) ↔ ManyOneEquiv p q
-- Mathlib.Data.Prod.TProd
Set.tprod.eq_1 : ∀ {ι : Type u} {α : ι → Type v} (x : (i : ι) → Set (α i)), Set.tprod [] x = Set.univ
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.id_apply : ∀ (X : AddSemigrp) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.contains a t = false → t.getKey! a = default
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
/-- An isomorphism between `PGL(n, F)` and `PSL(n, F)` in the case of an algebraically closed field
induced from the natural inclusion map.  -/
Matrix.ProjectiveSpecialLinearGroup.isoPSLOfAlgClosedOfNonempty : {n : Type u_1} →
  [inst : Fintype n] →
    [inst_1 : DecidableEq n] →
      [Nonempty n] →
        {F : Type u_3} →
          [inst_3 : Field F] → [IsAlgClosed F] → Matrix.ProjGenLinGroup n F ≃* Matrix.ProjectiveSpecialLinearGroup n F
-- Mathlib.Data.Finsupp.Single
Finsupp.erase_ne : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {f : α →₀ M}, a' ≠ a → (Finsupp.erase a f) a' = f a'
-- Mathlib.Data.Sym.Sym2
Sym2.Rel.refl : ∀ {α : Type u} (x y : α), Sym2.Rel α (x, y) (x, y)
-- Mathlib.Algebra.Ring.Commute
sub_sq : ∀ {R : Type u} [inst : CommRing R] (a b : R), (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
-- Init.MetaTypes
Lean.Meta.Command.ReduceConfig.mk.injEq : ∀ (types proofs implicits : Bool) (transparency : Lean.Meta.TransparencyMode)
  (smartUnfolding check ignoreStuckTC types_1 proofs_1 implicits_1 : Bool) (transparency_1 : Lean.Meta.TransparencyMode)
  (smartUnfolding_1 check_1 ignoreStuckTC_1 : Bool),
  ({ types := types, proofs := proofs, implicits := implicits, transparency := transparency,
        smartUnfolding := smartUnfolding, check := check, ignoreStuckTC := ignoreStuckTC } =
      { types := types_1, proofs := proofs_1, implicits := implicits_1, transparency := transparency_1,
        smartUnfolding := smartUnfolding_1, check := check_1, ignoreStuckTC := ignoreStuckTC_1 }) =
    (types = types_1 ∧
      proofs = proofs_1 ∧
        implicits = implicits_1 ∧
          transparency = transparency_1 ∧
            smartUnfolding = smartUnfolding_1 ∧ check = check_1 ∧ ignoreStuckTC = ignoreStuckTC_1)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- `mvfderivWithin I J f s x` is the `mfderiv` of a vector-valued function `f` on `M` at `x`
within the set `s`, but taking values in the target normed space directly.
The difference to `mfderivWithin` is explained in the module-docstring for
`Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean`.

Future: this could be generalised to functions into additive torsors over abelian Lie groups.
 -/
mvfderivWithin : {𝕜 : 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] →
                      {F : Type u_8} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] → (M → F) → Set M → (x : M) → TangentSpace I x →L[𝕜] F
-- Mathlib.Order.SymmDiff
himp_bihimp_right : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), b ⇨ bihimp a b = b ⇨ a
-- Mathlib.Algebra.Ring.Basic
Subsingleton.to_isCancelMulZero : ∀ (α : Type u_3) [inst : Mul α] [inst_1 : Zero α] [Subsingleton α], IsCancelMulZero α
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- A variant of `sum_range_succ` which pulls off the first term in the sum rather
than the last.  -/
List.sum_range_succ' : ∀ {M : Type u_4} [inst : AddMonoid M] (f : ℕ → M) (n : ℕ),
  (List.map f (List.range n.succ)).sum = f 0 + (List.map (fun i => f i.succ) (List.range n)).sum
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projection_eq_id_sub_projection`. -/
Submodule.IsCompl.projection_eq_id_sub_projection : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q), q.projection p ⋯ = LinearMap.id - p.projection q hpq
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.DocumentUri : Type
-- Mathlib.RingTheory.Unramified.Basic
Algebra.Unramified.mk : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A],
  autoParam (Algebra.FormallyUnramified R A) Algebra.Unramified.formallyUnramified._autoParam →
    autoParam (Algebra.FiniteType R A) Algebra.Unramified.finiteType._autoParam → Algebra.Unramified R A
-- Mathlib.Data.Fintype.Card
Finite.injective_iff_surjective_of_equiv : ∀ {α : Type u_1} {β : Type u_2} [Finite α] {f : α → β} (e : α ≃ β), Function.Injective f ↔ Function.Surjective f
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.SheafCondition.instCategoryOpensLeCover : {X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      CategoryTheory.Category.{u_1, u_1} (TopCat.Presheaf.SheafCondition.OpensLeCover U)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Reinterpret `f : α → β` as an element of `α →ᵤ β`.  -/
UniformFun.ofFun : {α : Type u_1} → {β : Type u_2} → (α → β) ≃ UniformFun α β
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
MeasureTheory.integrable_piLp_iff : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {ι : Type u_2} [inst_1 : Fintype ι] {E : ι → Type u_3} [inst_2 : (i : ι) → NormedAddCommGroup (E i)]
  {f : X → PiLp q E}, MeasureTheory.Integrable f μ ↔ ∀ (i : ι), MeasureTheory.Integrable (fun x => (f x).ofLp i) μ
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_empty`. -/
EMetric.infEdist_empty : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, Metric.infEDist x ∅ = ⊤
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_leftUnitor_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.LaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.leftUnitor η).hom.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {km : α}, Std.Internal.List.minKey? l = some km → Std.Internal.List.containsKey km l = true
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four : ∀ {ι : 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) (S : Type u_5)
  {i j : ι} [Finite ι] [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] [inst_9 : CommRing S]
  [inst_10 : Algebra S R] [FaithfulSMul S R] [inst_12 : P.IsValuedIn S],
  LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeightIn S i j ≠ 4
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.dvd_span_singleton : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] {I : Ideal A} {x : A}, I ∣ Ideal.span {x} ↔ x ∈ I
-- Mathlib.Analysis.Analytic.CPolynomialDef
FormalMultilinearSeries.sum.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : ContinuousConstSMul 𝕜 E]
  [inst_10 : ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (x : E),
  p.sum x = ∑' (n : ℕ), (p n) fun x_1 => x
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (a : CochainComplex.HomComplex.CohomologyClass ((CochainComplex.singleFunctor C 0).obj X) R.cochainComplex ↑n),
  R.extAddEquivCohomologyClass.symm a = R.extEquivCohomologyClass.symm a
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_prod : ∀ {β : Type u_3} {M : Type u_5} {α : Type u_6} [inst : SMul M α] [inst_1 : SMul M β] (c : M) (s : Set α) (t : Set β),
  c • s ×ˢ t = (c • s) ×ˢ (c • t)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.liftWith_trans : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPred} {n₁ n₂ : Type u → Type v} [inst_4 : MonadControl n₁ m]
  [inst_5 : MonadControlT n₂ n₁] (f : ({β : Type u} → m β → n₂ (stM n₂ m β)) → n₂ α),
  ⦃ Std.Internal.Do.wp (MonadControl.liftWith fun x₂ => liftWith fun x₁ => f fun {β} => x₁ ∘ x₂) post epost ⦄
    liftWith f ⦃ post; epost ⦄
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.eq_append_of_dropPrefix?_eq_some : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s res : String.Slice},
  s.dropPrefix? pat = some res → ∃ t, String.Slice.Pattern.Model.PatternModel.Matches pat t ∧ s.copy = t ++ res.copy
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.method : Lean.Lsp.SymbolKind
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → Inhabited (CategoryTheory.CommGrp C)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.IsReal.coe_embedding_apply : ∀ {K : Type u_1} [inst : Field K] {φ : K →+* ℂ} (hφ : NumberField.ComplexEmbedding.IsReal φ) (x : K),
  ↑(hφ.embedding x) = φ x
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
/-- Lebesgue dominated convergence theorem for filters with a countable basis  -/
intervalIntegral.tendsto_integral_filter_of_dominated_convergence : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} {ι : Type u_3} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → ℝ → E} (bound : ℝ → ℝ),
  (∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) (μ.restrict (Set.uIoc a b))) →
    (∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.uIoc a b → ‖F n x‖ ≤ bound x) →
      IntervalIntegrable bound μ a b →
        (∀ᵐ (x : ℝ) ∂μ, x ∈ Set.uIoc a b → Filter.Tendsto (fun n => F n x) l (nhds (f x))) →
          Filter.Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (nhds (∫ (x : ℝ) in a..b, f x ∂μ))
-- Mathlib.Algebra.Ring.Ext
NonUnitalCommRing.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : NonUnitalCommRing R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.coe_pointwise_smul : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (m : M)
  (S : Subsemiring R), ↑(m • S) = m • ↑S
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Unsigned division.
 -/
Std.Tactic.BVDecide.BVBinOp.udiv : Std.Tactic.BVDecide.BVBinOp
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
/-- Construct a model that satisfies all constraints in the cutsat model.
It also assigns values to integer terms that have not been internalized by the
cutsat model.

Remark: it uses rational numbers because cutsat may have failed to build an
integer model.
 -/
Lean.Meta.Grind.Arith.Cutsat.mkModel : Lean.Meta.Grind.Goal → Lean.MetaM (Array (Lean.Expr × ℚ))
-- Mathlib.Order.Interval.Finset.Defs
/-- Left-closed right-closed interval  -/
LocallyFiniteOrder.finsetIcc : {α : Type u_1} → {inst : Preorder α} → [self : LocallyFiniteOrder α] → α → α → Finset α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → γ a}, (Std.DHashMap.map f m).isEmpty = m.isEmpty
-- Mathlib.GroupTheory.Congruence.BigOperators
AddCon.coe_dfinsuppSumAddHom : ∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M]
  [inst_2 : (i : ι) → AddCommMonoid (β i)] (c : AddCon M) (h : (i : ι) → β i →+ M) (f : Π₀ (i : ι), β i),
  ↑((DFinsupp.sumAddHom h) f) = (DFinsupp.sumAddHom fun i => c.mk'.comp (h i)) f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ \ m₂).getKey! k = default
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.SMulCandidate.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          {α : R₀ ⟶ R.obj} →
            {M₀ : PresheafOfModules R₀} →
              {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                {φ : M₀.presheaf ⟶ A.obj} →
                  {X : Cᵒᵖ} →
                    {r : ↑(R.obj.obj X)} →
                      {m : ↑(A.obj.obj X)} →
                        (x : ↑(A.obj.obj X)) →
                          (∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
                              (CategoryTheory.ConcreteCategory.hom (α.app Y)) r₀ =
                                  (CategoryTheory.ConcreteCategory.hom (R.obj.map f)) r →
                                ∀ (m₀ : ↑(M₀.obj Y)),
                                  (CategoryTheory.ConcreteCategory.hom (φ.app Y)) m₀ =
                                      (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) m →
                                    (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) x =
                                      (CategoryTheory.ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)) →
                            PresheafOfModules.Sheafify.SMulCandidate α φ r m
-- Init.Data.Nat.Bitwise.Basic
Nat.instShiftLeft : ShiftLeft ℕ
-- Init.Internal.Order.Basic
Lean.Order.monotone_of_monotone_apply : ∀ {α : Sort u} {β : α → Sort v} {γ : Sort w} [inst : Lean.Order.PartialOrder γ]
  [inst_1 : (x : α) → Lean.Order.PartialOrder (β x)] (f : γ → (x : α) → β x),
  (∀ (y : α), Lean.Order.monotone fun x => f x y) → Lean.Order.monotone f
-- Lean.Elab.Match
Lean.Elab.Term.ElabMatchTypeAndDiscrsResult.discrs : Lean.Elab.Term.ElabMatchTypeAndDiscrsResult → Array Lean.Elab.Term.Discr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushout_inr_inv_inl_of_right_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.inv (CategoryTheory.Limits.pushout.inl f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) f
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.snd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)), κ.snd = κ.mapOfMeasurable Prod.snd ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_of_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.getValueCast? k (Std.Internal.List.insertList l toInsert) =
        (Std.Internal.List.getValueCast? k toInsert).or (Std.Internal.List.getValueCast? k l)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_le_maxKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {k : α} {v : β k} {fallback : α}, (cmp (t.maxKeyD fallback) ((t.insert k v).maxKeyD fallback)).isLE = true
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.abLeftHomologyData_π : ∀ (S : CategoryTheory.ShortComplex Ab),
  S.abLeftHomologyData.π = AddCommGrpCat.ofHom (QuotientAddGroup.mk' S.abToCycles.range)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.withTermInfoContext' : Lean.Name →
  Lean.Syntax →
    Lean.Elab.TermElabM Lean.Expr →
      optParam (Option Lean.Expr) none →
        optParam (Option Lean.LocalContext) none →
          optParam Bool false → optParam Bool false → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_continuous : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a),
  Continuous ⇑(cfcₙHom ha)
-- Std.Data.TreeSet.Basic
/-- Monadically computes a value by folding the given function over the elements in the tree set in
descending order.
 -/
Std.TreeSet.foldrM : {α : Type u} →
  {cmp : α → α → Ordering} →
    {m : Type u_1 → Type u_2} → {δ : Type u_1} → [Monad m] → (α → δ → m δ) → δ → Std.TreeSet α cmp → m δ
-- Lean.PrettyPrinter.Delaborator.FieldNotation
_private.Lean.PrettyPrinter.Delaborator.FieldNotation.0.Lean.PrettyPrinter.Delaborator.testAppOf : Lean.Expr → Lean.Name → Lean.MetaM Bool
-- Lean.Meta.Tactic.FunIndCollect
/-- the full calls  -/
Lean.Meta.FunInd.SeenCalls.calls : Lean.Meta.FunInd.SeenCalls → Array Lean.Expr