mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α],
  t.WF →
    ∀ {l : List α} {k : α},
      k ∉ t → l.contains k = false → (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).getKey! k = default
-- Mathlib.Data.DFinsupp.BigOperators
/-- **Alias** of `DFinsupp.prod_finsetSum_index`. -/
DFinsupp.prod_finset_sum_index : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {γ : Type w} {α : Type x}
  [inst_1 : (i : ι) → AddCommMonoid (β i)] [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ]
  {s : Finset α} {g : α → Π₀ (i : ι), β i} {h : (i : ι) → β i → γ},
  (∀ (i : ι), h i 0 = 1) →
    (∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂) → ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
-- Init.MetaTypes
/-- If true (default: false), lift non-extractable `let`s as far out as possible.  -/
Lean.Meta.ExtractLetsConfig.lift : Lean.Meta.ExtractLetsConfig → Bool
-- Mathlib.LinearAlgebra.Span.Defs
/-- An induction principle for span membership. This is a version of `Submodule.span_induction`
for binary predicates.  -/
Submodule.span_induction₂ : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
  {N : Type u_9} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {t : Set N}
  {p : (x : M) → (y : N) → x ∈ Submodule.span R s → y ∈ Submodule.span R t → Prop},
  (∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯) →
    (∀ (y : N) (hy : y ∈ Submodule.span R t), p 0 y ⋯ hy) →
      (∀ (x : M) (hx : x ∈ Submodule.span R s), p x 0 hx ⋯) →
        (∀ (x y : M) (z : N) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s) (hz : z ∈ Submodule.span R t),
            p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) →
          (∀ (x : M) (y z : N) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R t)
              (hz : z ∈ Submodule.span R t), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) →
            (∀ (r : R) (x : M) (y : N) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R t),
                p x y hx hy → p (r • x) y ⋯ hy) →
              (∀ (r : R) (x : M) (y : N) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R t),
                  p x y hx hy → p x (r • y) hx ⋯) →
                ∀ {a : M} {b : N} (ha : a ∈ Submodule.span R s) (hb : b ∈ Submodule.span R t), p a b ha hb
-- Mathlib.GroupTheory.Congruence.BigOperators
AddCon.finsuppSum : ∀ {ι : Type u_1} {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Zero β] (c : AddCon M)
  (h h' : ι → β → M) {f g : ι →₀ β},
  (∀ (i : ι), c (h i 0) 0) →
    (∀ (i : ι), c (h' i 0) 0) → (∀ (i : ι), c (h i (f i)) (h' i (g i))) → c (f.sum h) (g.sum h')
-- Lean.Elab.Tactic.Basic
/-- Assign `mvarId := sorry`  -/
Lean.Elab.admitGoal : Lean.MVarId → optParam Bool true → Lean.MetaM Unit
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddBelow.inv : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G},
  BddBelow s → BddAbove s⁻¹
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).get k h' = m₁.get k ⋯
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAtFilter_intCast : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (L : Filter (𝕜 × 𝕜)) [inst_3 : IntCast F] (z : ℤ), HasDerivAtFilter (↑z) 0 L
-- Mathlib.Data.Set.Semiring
SetSemiring.instCommMonoid : {α : Type u_1} → [CommMonoid α] → CommMonoid (SetSemiring α)
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.node.injEq : ∀ {α : Type u} (cs cs_1 : Array (Lean.PersistentArrayNode α)),
  (Lean.PersistentArrayNode.node cs = Lean.PersistentArrayNode.node cs_1) = (cs = cs_1)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
ContinuousLinearMap.instMeasurableSpace : {𝕜 : Type u_2} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_4} → [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → MeasurableSpace (E →L[𝕜] F)
-- Mathlib.Computability.NFA
NFA.Path.cons.injEq : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} (t s u : σ) (a : α) (x : List α) (a_1 : t ∈ M.step s a) (a_2 : M.Path t u x)
  (t_1 : σ) (a_3 : t_1 ∈ M.step s a) (a_4 : M.Path t_1 u x),
  (NFA.Path.cons t s u a x a_1 a_2 = NFA.Path.cons t_1 s u a x a_3 a_4) = (t = t_1 ∧ a_2 ≍ a_4)
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Returns true if an application should use explicit mode when delaborating.
Explicit mode turns off unexpanders
 -/
Lean.PrettyPrinter.Delaborator.useAppExplicit : ℕ → Array Lean.PrettyPrinter.Delaborator.ParamKind → Lean.PrettyPrinter.Delaborator.DelabM Bool
-- Init.Data.Bool
Bool.and_eq_true_iff : ∀ {x y : Bool}, (x && y) = true ↔ x = true ∧ y = true
-- Lean.Server.InfoUtils
/-- Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves).  -/
Lean.Elab.InfoTree.collectNodesBottomUpM : {m : Type → Type u_1} →
  {α : Type} →
    [Monad m] →
      (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List α → m (List α)) →
        Lean.Elab.InfoTree → m (List α)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- **Alias** of the reverse direction of `Module.End.hasUnifEigenvalue_iff_mem_spectrum`. -/
Module.End.HasUnifEigenvalue.of_mem_spectrum : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {f : Module.End K V} {μ : K}, μ ∈ spectrum K f → f.HasUnifEigenvalue μ 1
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instToStreamValuesStream : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → Std.ToStream (RBTree.RBMap.Values α β cmp) (RBTree.RBMap.Values.Stream α β)
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.induced : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace Y] (f : X → Y), Topology.IsInducing f
-- Mathlib.Analysis.Polynomial.Fourier
/-- Algebra map from `ℂ[X]` to `C(AddCircle (2 * π), ℂ)` that evaluates polynomials on the unit
circle. For a polynomial `p`, this maps it to the function `fun θ ↦ p (exp (I * θ))`.  -/
Polynomial.toAddCircle : Polynomial ℂ →ₐ[ℂ] C(AddCircle (2 * Real.pi), ℂ)
-- Mathlib.Order.UpperLower.Hom
LowerSet.coe_iicInfHom : ∀ {α : Type u_1} [inst : SemilatticeInf α], ⇑LowerSet.iicInfHom = LowerSet.Iic
-- Lean.Parser.Term
Lean.Parser.Term.showTermElabImpl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J K : C} (f : I ⟶ J) (g : J ⟶ K)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ChosenPullbacksAlong g]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)]
  [inst_4 : CategoryTheory.ExponentiableMorphism f] [inst_5 : CategoryTheory.ExponentiableMorphism g]
  [inst_6 : CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.comp f g)]
  {Z : CategoryTheory.Functor (CategoryTheory.Over I) (CategoryTheory.Over I)}
  (h : CategoryTheory.Functor.id (CategoryTheory.Over I) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.ExponentiableMorphism.pushforwardComp f g).hom
        (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.comp f g)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.comp f g)).counit
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.comp f g)).counit h
-- Lean.Data.JsonRpc
Lean.IO.FS.Stream.writeResponseErrorWithData : {α : Type u_1} → [Lean.ToJson α] → IO.FS.Stream → Lean.JsonRpc.ResponseError α → IO Unit
-- Mathlib.Algebra.TrivSqZeroExt.Basic
_private.Mathlib.Algebra.TrivSqZeroExt.Basic.0.TrivSqZeroExt.snd_pow_of_smul_comm.aux : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M),
  MulOpposite.op x.fst • x.snd = x.fst • x.snd → ∀ (n : ℕ), MulOpposite.op (x.fst ^ n) • x.snd = x.fst ^ n • x.snd
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ico_mul_zpow : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ico (a * b ^ n) (a * b ^ (n + 1)))
-- Mathlib.RingTheory.Algebraic.Integral
Transcendental.subalgebraAlgebraicClosure : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [NoZeroDivisors S]
  {a : S}, Transcendental R a → ∀ [inst_4 : IsDomain R], Transcendental (↥(Subalgebra.algebraicClosure R S)) a
-- Init.Data.BitVec.Bitblast
/-- The recursive addition of `w`-long words on two flattened bitvectors `x` and `y` (with different
number of words `len` and `len'`, respectively) returns the same value, if we can prove
that each `w`-long word in `x` results from the addition of two `w`-long words in `y`,
using exactly all `w`-long words in `y`.
 -/
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux_eq_of : ∀ {len w len' : ℕ} {x : BitVec (len * w)} {y : BitVec (len' * w)},
  len = (len' + 1) / 2 →
    (∀ i < (len' + 1) / 2,
        BitVec.extractLsb' (i * w) w x =
          BitVec.extractLsb' (2 * i * w) w y + BitVec.extractLsb' ((2 * i + 1) * w) w y) →
      BitVec.addRecAux✝ x len 0#w = BitVec.addRecAux✝ y len' 0#w
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- The reachability relation of a maximal acyclic subgraph agrees with that of the larger graph.
 -/
SimpleGraph.reachable_eq_of_maximal_isAcyclic : ∀ {V : Type u_1} {G : SimpleGraph V} (F : SimpleGraph V),
  Maximal (fun H => H ≤ G ∧ H.IsAcyclic) F → F.Reachable = G.Reachable
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dCokernelSequence_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_5),
  (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃).f = X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1CoresCoinfOfTrivial_f : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal]
  [inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)],
  (groupHomology.H1CoresCoinfOfTrivial A S).f =
    groupHomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A)) 1
-- Batteries.Lean.EStateM
EStateM.run'.eq_1 : ∀ {ε σ α : Type u} (x : EStateM ε σ α) (s : σ),
  x.run' s =
    match x.run s with
    | EStateM.Result.ok v a => some v
    | EStateM.Result.error a a_1 => none
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₂ → (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerRight_comp_symm : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h))
        (CategoryTheory.Bicategory.associator f' g h).inv)
-- Init.Data.UInt.Bitwise
UInt64.or_self : ∀ {a : UInt64}, a ||| a = a
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
/-- The coequalizer of two locally ringed spaces in the category of sheafed spaces is a locally
ringed space.  -/
AlgebraicGeometry.LocallyRingedSpace.coequalizer : {X Y : AlgebraicGeometry.LocallyRingedSpace} → (X ⟶ Y) → (X ⟶ Y) → AlgebraicGeometry.LocallyRingedSpace
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.brecOn_1.go : {α : Type u} →
  {motive_1 : Lean.Widget.TaggedText α → Sort u_1} →
    {motive_2 : Array (Lean.Widget.TaggedText α) → Sort u_1} →
      {motive_3 : List (Lean.Widget.TaggedText α) → Sort u_1} →
        (t : Array (Lean.Widget.TaggedText α)) →
          ((t : Lean.Widget.TaggedText α) → t.below → motive_1 t) →
            ((t : Array (Lean.Widget.TaggedText α)) → Lean.Widget.TaggedText.below_1 t → motive_2 t) →
              ((t : List (Lean.Widget.TaggedText α)) → Lean.Widget.TaggedText.below_2 t → motive_3 t) →
                motive_2 t ×' Lean.Widget.TaggedText.below_1 t
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.apply_apply : ∀ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ] (v : E) (f : E →L[𝕜] Fₗ),
  ((ContinuousLinearMap.apply 𝕜 Fₗ) v) f = f v
-- Lean.CoreM
Lean.Core.checkMaxHeartbeatsCore : String → Lean.Name → ℕ → Lean.CoreM Unit
-- Mathlib.Algebra.Group.Support
Function.support_fun_neg : ∀ {α : Type u_1} {G : Type u_3} [inst : SubtractionMonoid G] (f : α → G),
  (Function.support fun x => -f x) = Function.support f
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.measurable_preCDF' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)},
  Measurable fun a r => (ProbabilityTheory.preCDF ρ r a).toReal
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instCoeTC.eq_1 : ∀ {α : Type u}, WithOne.instCoeTC = { coe := WithOne.coe }
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
Returns `none` if `f` returns `none` for all outputs.

`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
iteration.

This function is deprecated. Instead of `it.allowNontermination.findSome?`, use `it.findSome?`.

Examples:
 * `([7, 6, 5, 8, 1, 2, 6].iterM Id).allowNontermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = pure (some 10)`
 * `([7, 6, 5, 8, 1, 2, 6].iterM Id).allowNontermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = pure none`
 -/
Std.IterM.Partial.findSome? : {α β γ : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → Std.IterM.Partial m β → (β → Option γ) → m (Option γ)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.exchange : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} {e : α},
  M.IsBase B₁ → M.IsBase B₂ → e ∈ B₁ \ B₂ → ∃ y ∈ B₂ \ B₁, M.IsBase (insert y (B₁ \ {e}))
-- Mathlib.Data.Part
Part.right_dom_of_mul_dom : ∀ {α : Type u_1} [inst : Mul α] {a b : Part α}, (a * b).Dom → b.Dom
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The Monge point lies in the affine span.  -/
Affine.Simplex.mongePoint_mem_affineSpan : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n), s.mongePoint ∈ affineSpan ℝ (Set.range s.points)
-- Mathlib.Order.KrullDimension
Order.KrullDimLE.mk : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α], Order.krullDim α ≤ ↑n → Order.KrullDimLE n α
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- A continuous function from `α` to `β` is ae strongly measurable when one of the two spaces is
second countable.  -/
Continuous.aestronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α] [TopologicalSpace.PseudoMetrizableSpace β]
  [SecondCountableTopologyEither α β], Continuous f → MeasureTheory.AEStronglyMeasurable f μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k} {fallback : α},
  (compare ((Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKeyD fallback) k).isLE = true
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.bisim₀ : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (R : P.M α → P.M α → Prop),
  Equivalence R →
    (∀ (x y : P.M α),
        R x y →
          MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P x) =
            MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P y)) →
      ∀ (x y : P.M α), R x y → x = y
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage f U).inv
      (CategoryTheory.CategoryStruct.comp U.ι f) =
    ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U).ι
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Prime.not_abundant : ∀ {n : ℕ}, Nat.Prime n → ¬n.Abundant
-- Mathlib.ModelTheory.Order
FirstOrder.Language.noTopOrder_of_dlo : ∀ (L : FirstOrder.Language) (M : Type w') [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : LE M]
  [L.OrderedStructure M] [M ⊨ L.dlo], NoTopOrder M
-- Init.Data.Int.DivMod.Basic
Int.fdiv.eq_2 : ∀ (m n : ℕ), (m = 0 → False) → (Int.ofNat m).fdiv (Int.ofNat n) = Int.ofNat (m / n)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.realize_one : ∀ {α : Type u_1} {R : Type u_2} [inst : Add R] [inst_1 : Mul R] [inst_2 : Neg R] [inst_3 : One R] [inst_4 : Zero R]
  [inst_5 : FirstOrder.Ring.CompatibleRing R] (v : α → R), FirstOrder.Language.Term.realize v 1 = 1
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_range : ∀ {A B : GrpCat} (f : A ⟶ B) {b : ↑B},
  b ∉ (GrpCat.Hom.hom f).range →
    GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨b • ↑(GrpCat.Hom.hom f).range, ⋯⟩ ≠
      GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(GrpCat.Hom.hom f).range, ⋯⟩
-- Lean.Elab.Do.InferControlInfo
/-- The variables that are syntactically reassigned somewhere in the `do` block.  -/
Lean.Elab.Do.ControlInfo.reassigns : Lean.Elab.Do.ControlInfo → Lean.NameSet
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- An object in `C`  -/
CategoryTheory.RegularMono.Z : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → {f : X ⟶ Y} → CategoryTheory.RegularMono f → C
-- Mathlib.Topology.Order.OrderClosed
/-- The set of antitone functions is closed.  -/
isClosed_antitone : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : Preorder β], IsClosed {f | Antitone f}
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSemilatticeInf : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [SemilatticeInf β] → SemilatticeInf (l.Germ β)
-- Mathlib.RingTheory.FinitePresentation
/-- This is used to prove the strictly stronger `ker_fg_of_surjective`. Use it instead.  -/
Algebra.FinitePresentation.ker_fg_of_mvPolynomial : ∀ {R : Type w₁} {A : Type w₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {n : ℕ}
  (f : MvPolynomial (Fin n) R →ₐ[R] A),
  Function.Surjective ⇑f → ∀ [Algebra.FinitePresentation R A], (RingHom.ker f.toRingHom).FG
-- Mathlib.Data.ENat.Pow
ENat.epow_one : ∀ {x : ℕ∞}, x ^ 1 = x
-- Init.Data.Int.Basic
Int.instMax : Max ℤ
-- Mathlib.Algebra.BigOperators.Finprod
Multiset.hasFiniteSupport_fun_nsmul_count : ∀ {α : Type u_1} {M : Type u_2} [inst : DecidableEq α] [inst_1 : AddCommMonoid M] (s : Multiset α) (f : α → M),
  Function.HasFiniteSupport fun a => Multiset.count a s • f a
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule : ∀ {ι : 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) [Nontrivial M],
  Nontrivial ↥P.invtRootSubmodule
-- Init.Core
/-- Heterogeneous equality precomposes with propositional equality.  -/
heq_of_heq_of_eq : ∀ {α β : Sort u} {a : α} {b b' : β}, a ≍ b → b = b' → a ≍ b'
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
PiLp.borelSpace : ∀ (p : ENNReal) {ι : Type u_2} {X : ι → Type u_3} [Countable ι] [inst : (i : ι) → MeasurableSpace (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), SecondCountableTopology (X i)],
  BorelSpace (PiLp p X)
-- Mathlib.Data.Set.Disjoint
Disjoint.inter_eq : ∀ {α : Type u} {s t : Set α}, Disjoint s t → s ∩ t = ∅
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The underlying modification of strong transformations.  -/
CategoryTheory.Oplax.StrongTrans.Hom.as : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Oplax.StrongTrans.Hom η θ → CategoryTheory.Oplax.StrongTrans.Modification η θ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instMonoidalMonForget₂Mon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.AddGrp.forget₂Mon C).Monoidal
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.functorComp_hom_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J)
  (X : CategoryTheory.Discrete I),
  (CategoryTheory.Discrete.functorComp f g).hom.app X = CategoryTheory.CategoryStruct.id (f (g X.as))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.diff_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → (t₁ \ t₃).Equiv (t₂ \ t₃)
-- Mathlib.Data.List.Sigma
List.lookupAll_nodup : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) {l : List (Sigma β)},
  l.NodupKeys → (List.lookupAll a l).Nodup
-- Init.Data.Array.Basic
/-- Swaps a new element with the element at the given index.

Returns the value formerly found at `i`, paired with an array in which the value at `i` has been
replaced with `v`.

Examples:
* `#["spinach", "broccoli", "carrot"].swapAt 1 "pepper" = ("broccoli", #["spinach", "pepper", "carrot"])`
* `#["spinach", "broccoli", "carrot"].swapAt 2 "pepper" = ("carrot", #["spinach", "broccoli", "pepper"])`
 -/
Array.swapAt : {α : Type u} → (xs : Array α) → (i : ℕ) → α → autoParam (i < xs.size) Array.swapAt._auto_1 → α × Array α
-- Init.Data.Int.Gcd
Int.gcd_sub_mul_right_right : ∀ (m n k : ℤ), m.gcd (n - k * m) = m.gcd n