mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularCompactLTTop.instWeaklyRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [BorelSpace α]
  [R1Space α] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsFiniteMeasure μ], μ.WeaklyRegular
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialCosimplicialEquiv_inverse_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Functor SimplexCategory Cᵒᵖ} (η : X ⟶ Y),
  (CategoryTheory.simplicialCosimplicialEquiv C).inverse.map η = (CategoryTheory.NatTrans.leftOp η).op
-- Mathlib.Algebra.Group.Finsupp
Finsupp.update_eq_single_add_erase : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (f : ι →₀ M) (a : ι) (b : M),
  f.update a b = (fun₀ | a => b) + Finsupp.erase a f
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.differentiableAt_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) → DifferentiableAt ℝ (ProbabilityTheory.mgf X μ) t
-- Mathlib.Topology.EMetricSpace.Defs
Metric.closedEBall_top : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α), Metric.closedEBall x ⊤ = Set.univ
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz.0.SimpleGraph.zarankiewicz.eq_1 : ∀ (m n s t : ℕ),
  SimpleGraph.zarankiewicz m n s t =
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x =>
      x.edgeFinset.card
-- Mathlib.LinearAlgebra.Center
/-- Over a domain, an endomorphism `f` of a free module `V`
of rank ≠ 1 such that `f v` and `v` are collinear, for all `v : V`,
consists of homotheties with central ratio.

In the commutative case, use `LinearMap.exists_eq_smul_id`.

This is a variant of `LinearMap.exists_mem_center_apply_smul`
which switches the use of `StrongRankInduction` and `finrank`
for the cardinality of a given basis.

When `finrank R V = 1`, up to a linear equivalence `V ≃ₗ[R] R`,
then any `f` is *right*-multiplication by some `a : R`,
but not necessarily *left*-multiplication by an element of the center of `R`.  -/
LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  {f : V →ₗ[R] V} {ι : Type u_3} [Nontrivial ι] (b : Module.Basis ι R V),
  (∀ (v : V), ¬LinearIndependent R ![v, f v]) → ∃ a, f = a • 1
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.preimage_closure : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (S : Set B), ⇑e ⁻¹' closure S = closure (⇑e ⁻¹' S)
-- Std.Time.Internal.UnitVal
/-- Returns the absolute value of a `UnitVal`.
 -/
Std.Time.Internal.UnitVal.abs : {α : ℚ} → Std.Time.Internal.UnitVal α → Std.Time.Internal.UnitVal α
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
/-- [Stacks Tag 054I](https://stacks.math.columbia.edu/tag/054I) -/
AlgebraicGeometry.Scheme.Hom.isConstructible_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {s : Set ↥Y},
  Topology.IsConstructible s → Topology.IsConstructible (⇑f ⁻¹' s)
-- Lean.DeprecatedModule
Lean.instInhabitedDeprecatedModuleEntry : Inhabited Lean.DeprecatedModuleEntry
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_maxKey?_of_isSome_maxKey?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).maxKey?.isSome = true → t.maxKey?.isSome = true
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_ite_eq_of_mem : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M),
  a ∈ s → (∏ x ∈ s, if a = x then b x else 1) = b a
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.instAddCancelCommMonoidSyn : {σ : Type u_1} → (m : MonomialOrder σ) → AddCancelCommMonoid m.syn
-- Mathlib.Algebra.Star.Basic
/-- A type endowed with `star` is a star module over some other type with `star` if it admits an
injective map that preserves `star` and `•` to a star module. See note [reducible non-instances].  -/
Function.Injective.starModule : ∀ {R : Type u} {S : Type v} (f : R → S) (𝕜 : Type u_1) [inst : Star 𝕜] [inst_1 : SMul 𝕜 R] [inst_2 : Star R]
  [inst_3 : SMul 𝕜 S] [inst_4 : Star S] [StarModule 𝕜 S],
  Function.Injective f →
    (∀ (x : R), f (star x) = star (f x)) → (∀ (r : 𝕜) (x : R), f (r • x) = r • f x) → StarModule 𝕜 R
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instZero : {m : Type u_1} → {n : Type u_2} → {α : m → n → Type v} → [(i : m) → (j : n) → Zero (α i j)] → Zero (DMatrix m n α)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.ReflectsLimit.reflects : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : Type w} {inst_2 : CategoryTheory.Category.{w', w} J} {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.ReflectsLimit K F] {c : CategoryTheory.Limits.Cone K}
  (hc : CategoryTheory.Limits.IsLimit (F.mapCone c)), Nonempty (CategoryTheory.Limits.IsLimit c)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranObjObjIsoLimit_inv_π_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (F : CategoryTheory.Functor C H)
  [inst_4 : L.HasPointwiseRightKanExtension F] (X : D) (f : CategoryTheory.StructuredArrow X L) {Z : H}
  (h : F.obj f.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.ranObjObjIsoLimit F X).inv
      (CategoryTheory.CategoryStruct.comp ((L.ran.obj F).map f.hom)
        (CategoryTheory.CategoryStruct.comp ((L.ranCounit.app F).app f.right) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj X L).comp F) f) h
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_three_assoc : ∀ {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₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ : C₁} {X₂ : C₂} {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃) (g : X₂ ⟶ (G.obj (Opposite.op X₁)).obj X₃) {Z : C₃} (h : Y₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (adj₂.homEquiv.symm (CategoryTheory.CategoryStruct.comp g ((G.obj (Opposite.op X₁)).map f₃))) h =
    CategoryTheory.CategoryStruct.comp (adj₂.homEquiv.symm g) (CategoryTheory.CategoryStruct.comp f₃ h)
-- Mathlib.CategoryTheory.Adhesive.Basic
/-- A convenient formulation for a pushout being a van Kampen colimit. For any commutative cube of
which a van Kampen pushout forms the bottom face and the back faces are pullbacks, the front faces
are pullbacks if and only if the top face is a pushout. See `IsPushout.isVanKampen_iff` below.  -/
CategoryTheory.IsPushout.IsVanKampen : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} → {f : W ⟶ X} → {g : W ⟶ Y} → {h : X ⟶ Z} → {i : Y ⟶ Z} → CategoryTheory.IsPushout f g h i → Prop
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_dvd_self : ∀ {a : ℤ}, ↑a.natAbs ∣ a
-- Mathlib.GroupTheory.Nilpotent
/-- Quotienting the `center G` reduces the nilpotency class by 1.  -/
AddGroup.nilpotencyClass_quotient_center : ∀ {G : Type u_1} [inst : AddGroup G],
  AddGroup.nilpotencyClass (G ⧸ AddSubgroup.center G) = AddGroup.nilpotencyClass G - 1
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LVal.isFieldName : Lean.Elab.Term.LVal → Bool
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ici_add_one_eq_Ioi : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrderTop α] [inst_3 : Add α]
  [SuccAddOrder α] [NoMaxOrder α] (a : α), Finset.Ici (a + 1) = Finset.Ioi a
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.map.congr_simp : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (f f_1 : F),
  f = f_1 →
    ∀ (S S_1 : NonUnitalStarSubalgebra R A),
      S = S_1 → NonUnitalStarSubalgebra.map f S = NonUnitalStarSubalgebra.map f_1 S_1
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- See Note [custom simps projection]  -/
BialgEquiv.Simps.symm_apply : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      {B : Type u_3} →
        [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] → (A ≃ₐc[R] B) → B → A
-- Init.Data.BitVec.Basic
BitVec.instDiv : {n : ℕ} → Div (BitVec n)
-- Aesop.RuleTac.Basic
Aesop.CasesTarget : Type
-- Mathlib.Data.Complex.Basic
Complex.instCharZero : CharZero ℂ
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.mem_vonNeumann' : ∀ {o : Ordinal.{u}} {x : ZFSet.{u}}, x ∈ ZFSet.vonNeumann o ↔ ∃ a < o, x ⊆ ZFSet.vonNeumann a
-- Mathlib.Analysis.Normed.Group.Constructions
pi_norm_comp_le : ∀ {ι : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Fintype ι] [inst_1 : SeminormedAddGroup E] [inst_2 : Fintype F]
  (g : ι → E) (f : F → ι), ‖g ∘ f‖ ≤ ‖g‖
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_eq_iSup_iSup_edist : ∀ {α : Type u_1} {G : SimpleGraph α}, G.ediam = ⨆ u, ⨆ v, G.edist u v
-- Mathlib.RingTheory.Coprime.Ideal
/-- A finite family of ideals is pairwise coprime (that is, any two of them generate the whole ring)
iff when taking all the possible intersections of all but one of these ideals, the resulting family
of ideals still generate the whole ring.

For example with three ideals : `I ⊔ J = I ⊔ K = J ⊔ K = ⊤ ↔ (I ⊓ J) ⊔ (I ⊓ K) ⊔ (J ⊓ K) = ⊤`.

When ideals are all of the form `I i = R ∙ s i`, this is equivalent to the
`exists_sum_eq_one_iff_pairwise_coprime` lemma.  -/
Ideal.iSup_iInf_eq_top_iff_pairwise : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {t : Finset ι},
  t.Nonempty → ∀ (I : ι → Ideal R), ⨆ i ∈ t, ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j = ⊤ ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.eq_1 : ∀ (bytes : ByteArray) (i : ℕ),
  bytes.utf8DecodeChar? i =
    if h₀ : i < bytes.size then
      match h : ByteArray.utf8DecodeChar?.parseFirstByte bytes[i] with
      | ByteArray.utf8DecodeChar?.FirstByte.invalid => none
      | ByteArray.utf8DecodeChar?.FirstByte.done => ByteArray.utf8DecodeChar?.assemble₁ bytes[i] h
      | ByteArray.utf8DecodeChar?.FirstByte.oneMore =>
        if h₁ : i + 1 < bytes.size then ByteArray.utf8DecodeChar?.assemble₂ bytes[i] bytes[i + 1] else none
      | ByteArray.utf8DecodeChar?.FirstByte.twoMore =>
        if h₁ : i + 2 < bytes.size then ByteArray.utf8DecodeChar?.assemble₃ bytes[i] bytes[i + 1] bytes[i + 2] else none
      | ByteArray.utf8DecodeChar?.FirstByte.threeMore =>
        if h₁ : i + 3 < bytes.size then
          ByteArray.utf8DecodeChar?.assemble₄ bytes[i] bytes[i + 1] bytes[i + 2] bytes[i + 3]
        else none
    else none
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M}
  (f g : Module.End R M) (hf : Set.MapsTo ⇑f ↑p ↑p) (hg : Set.MapsTo ⇑g ↑p ↑p) {μ₁ μ₂ : R},
  Set.MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂) →
    Set.MapsTo ⇑(LinearMap.restrict f hf) ↑(Module.End.maxGenEigenspace (LinearMap.restrict g hg) μ₁)
      ↑(Module.End.maxGenEigenspace (LinearMap.restrict g hg) μ₂)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure_eq_of_le : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {k : Set G},
  k ⊆ ↑K → K ≤ AddSubgroup.closure k → AddSubgroup.closure k = K
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_neg : ∀ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (p : Submodule R M) [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂),
  Submodule.map (-f) p = Submodule.map f p
-- Init.Sym.Lemmas
Lean.Sym.Int64.le_eq_true : ∀ (a b : Int64), decide (a ≤ b) = true → (a ≤ b) = True
-- Mathlib.Data.Stream.Init
Stream'.ext_iff : ∀ {α : Type u} {s₁ s₂ : Stream' α}, s₁ = s₂ ↔ ∀ (n : ℕ), s₁.get n = s₂.get n
-- Lean.Elab.Do.Basic
Lean.Elab.Do.SavedState.term : Lean.Elab.Do.SavedState → Lean.Elab.Term.SavedState
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.finsetSum_iSup_of_monotone : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder ι] [IsDirectedOrder ι] {s : Finset α} {f : α → ι → ENNReal},
  (∀ (a : α), Monotone (f a)) → ∑ a ∈ s, iSup (f a) = ⨆ n, ∑ a ∈ s, f a n
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.rescale_mul : ∀ {σ : Type u_1} {R : Type u_9} [inst : CommSemiring R] (a b : σ → R),
  MvPowerSeries.rescale (a * b) = (MvPowerSeries.rescale b).comp (MvPowerSeries.rescale a)
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.eulerMascheroniSeq.eq_1 : ∀ (n : ℕ), Real.eulerMascheroniSeq n = ↑(harmonic n) - Real.log (↑n + 1)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.realizeValue.unsafe_impl_21 : Lean.RealizationContext✝ → Lean.Environment
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.exists_of_mem_map : ∀ {α : Type u} {β : Type v} {f : α → β} {b : β} {s : Stream'.WSeq α}, b ∈ Stream'.WSeq.map f s → ∃ a ∈ s, f a = b
-- Init.Data.Bool
Bool.or_and_distrib_right : ∀ (x y z : Bool), (x && y || z) = ((x || z) && (y || z))
-- Lean.Linter.UnusedVariables
_private.Lean.Linter.UnusedVariables.0.Lean.Linter.UnusedVariables.collectReferences.go : Lean.Syntax.Range →
  Lean.Linter.LinterSets →
    Array Lean.Elab.InfoTree →
      Option Lean.Elab.ContextInfo →
        ReaderT Bool (StateRefT' IO.RealWorld Lean.Linter.UnusedVariables.References IO) Unit
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The domain of a 2-isomorphism.  -/
Mathlib.Tactic.BicategoryLike.StructuralAtom.srcM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.StructuralAtom → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.lift.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') [inst_7 : IsLocalizedModule S f] (g : M →ₗ[R] M'')
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)),
  IsLocalizedModule.lift S f g h = LocalizedModule.lift S g h ∘ₗ ↑(IsLocalizedModule.iso S f).symm
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportFailure.mk.sizeOf_spec : ∀ (module const : Lean.Name) (exception : Lean.Exception),
  sizeOf { module := module, const := const, exception := exception } =
    1 + sizeOf module + sizeOf const + sizeOf exception
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.Coindep.delete_isBase_iff : ∀ {α : Type u_1} {M : Matroid α} {B D : Set α}, M.Coindep D → ((M.delete D).IsBase B ↔ M.IsBase B ∧ Disjoint B D)
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_div_mul_left : ∀ {c : ENNReal} (a b : ENNReal), c ≠ 0 → c ≠ ⊤ → c * a / (c * b) = a / b
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.div_add_div_of_dvd : ∀ {R : Type u} [inst : EuclideanDomain R] {x y z t : R},
  y ≠ 0 → t ≠ 0 → y ∣ x → t ∣ z → x / y + z / t = (t * x + y * z) / (t * y)
-- Init.Data.String.Defs
String.Pos.Raw.IsValid.le_utf8ByteSize : ∀ {s : String} {off : String.Pos.Raw}, String.Pos.Raw.IsValid s off → off.byteIdx ≤ s.utf8ByteSize
-- Init.Meta.Defs
Lean.Name.getRoot : Lean.Name → Lean.Name
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
rel_of_act_rel_act : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [ContravariantClass M N μ r] (m : M) {a b : N},
  r (μ m a) (μ m b) → r a b
-- Std.Data.DHashMap.Basic
/-- Creates a hash map from an array of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.DHashMap.Const.ofArray : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Array (α × β) → Std.DHashMap α fun x => β
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_inj : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r₁ r₂ : R} {m₁ m₂ : M},
  AddMonoidAlgebra.single m₁ r₁ = AddMonoidAlgebra.single m₂ r₂ ↔ m₁ = m₂ ∧ r₁ = r₂ ∨ r₁ = 0 ∧ r₂ = 0
-- Mathlib.Data.PNat.Find
PNat.one_le_find : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n), 1 < PNat.find h ↔ ¬p 1
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.wellFoundedGT_characterisations : ∀ (α : Type u_2) [inst : CompleteLattice α],
  [WellFoundedGT α, CompleteLattice.IsSupFiniteCompact α, CompleteLattice.IsSupClosedCompact α,
      ∀ (k : α), IsCompactElement k].TFAE
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_norm_add_norm_inv_mul : ∀ {E : Type u_5} [inst : SeminormedGroup E] (u v : E), ‖u‖ ≤ ‖v‖ + ‖u⁻¹ * v‖
-- Lean.Elab.Tactic.Omega.Frontend
Lean.Elab.Tactic.Omega.MetaProblem.mk.sizeOf_spec : ∀ (problem : Lean.Elab.Tactic.Omega.Problem) (facts disjunctions : List Lean.Expr)
  (processedFacts : Std.HashSet Lean.Expr),
  sizeOf { problem := problem, facts := facts, disjunctions := disjunctions, processedFacts := processedFacts } =
    1 + sizeOf problem + sizeOf facts + sizeOf disjunctions + sizeOf processedFacts
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.ringEquivOfRingEquivHom_injective : ∀ (A : Type u_8) (K : Type u_9) [inst : CommRing A] [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K], Function.Injective ⇑(IsFractionRing.ringEquivOfRingEquivHom A K)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.decompEquiv.eq_1 : ∀ (R : Type u_1) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace Q]
  [inst_10 : IsTopologicalAddTorsor Q],
  ContinuousAffineMap.decompEquiv R V Q =
    { toFun := fun f => (f 0, f.contLinear),
      invFun := fun p => p.2.toContinuousAffineMap +ᵥ ContinuousAffineMap.const R V p.1, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Sites.Coherent.Comparison
/-- The union of the extensive and regular coverages generates the coherent topology on `C`.  -/
CategoryTheory.extensive_regular_generate_coherent : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.FinitaryPreExtensive C],
  (CategoryTheory.extensiveCoverage C ⊔ CategoryTheory.regularCoverage C).toGrothendieck =
    CategoryTheory.coherentTopology C
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.instCoframe : {α : Type u_2} → [inst : TopologicalSpace α] → Order.Coframe (TopologicalSpace.Closeds α)
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_add_ball : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E), {x} + Metric.ball y δ = Metric.ball (x + y) δ
-- Mathlib.Order.Monotone.Defs
/-- A function `f` is strictly antitone on `s` if, for all `a, b ∈ s`, `a < b` implies
`f b < f a`.  -/
StrictAntiOn : {α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → Set α → Prop
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr₂_mapAccumr_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {s₁ : σ₁}
  {s₂ : σ₂} (xs : List.Vector α n) (ys : List.Vector β n) (f₁ : α → γ → σ₁ → σ₁ × ζ) (f₂ : β → σ₂ → σ₂ × γ),
  List.Vector.mapAccumr₂ f₁ xs (List.Vector.mapAccumr f₂ ys s₂).2 s₁ =
    have m :=
      List.Vector.mapAccumr₂
        (fun x y s =>
          have r₂ := f₂ y s.2;
          have r₁ := f₁ x r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ m.insertMany l}, (m.insertMany l)[k] = m[k]
-- Mathlib.Analysis.Normed.Lp.Matrix
Matrix.toLpLin_eq_toLin : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  (p q : ENNReal) [inst_3 : Finite m], Matrix.toLpLin p q = Matrix.toLin (PiLp.basisFun p R n) (PiLp.basisFun q R m)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (u v : V), G.edist u v = ⨅ w, ↑w.length
-- Lean.Elab.App
/-- Returns the current parameter's name.
Only valid if `fTypeIsForall` has returned `true`.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.getParamName : Lean.Elab.Term.ElabAppArgs.M Lean.Name
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.excenter_eq_incenter_iff : ∀ {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 : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs → (s.excenter signs = s.incenter ↔ signs = ∅ ∨ signs = Finset.univ)
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.IsTopCompl.isCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M}, Submodule.IsTopCompl p q → IsCompl p q
-- Mathlib.Combinatorics.SimpleGraph.Trails
SimpleGraph.Walk.IsEulerian.card_filter_odd_degree : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : Fintype V] [inst_2 : DecidableRel G.Adj] {u v : V}
  {p : G.Walk u v}, p.IsEulerian → ∀ {s : Finset V}, s = {v | Odd (G.degree v)} → s.card = 0 ∨ s.card = 2
-- Mathlib.GroupTheory.Nilpotent
/-- Abelian groups have nilpotency class at most one.  -/
AddCommGroup.nilpotencyClass_nonpos : ∀ {G : Type u_2} [inst : AddCommGroup G], AddGroup.nilpotencyClass G ≤ 1
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.unop.instNormal : ∀ {G : Type u_2} [inst : AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} [H.Normal], H.unop.Normal
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The norm on a `NormedRing`, as a `RingNorm`.  -/
NormedRing.toRingNorm : (R : Type u_2) → [inst : NormedRing R] → RingNorm R
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.factor_comp_mk : ∀ {R : Type u} [inst : Ring R] {S T : Ideal R} [inst_1 : S.IsTwoSided] [inst_2 : T.IsTwoSided] (H : S ≤ T),
  (Ideal.Quotient.factor H).comp (Ideal.Quotient.mk S) = Ideal.Quotient.mk T
-- Mathlib.Algebra.Ring.ULift
ULift.down_ofNat : ∀ {R : Type u} [inst : NatCast R] (n : ℕ) [inst_1 : n.AtLeastTwo], (OfNat.ofNat n).down = OfNat.ofNat n
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.exists_natDegree_lt : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R} {n : ℕ},
  n ≠ 0 → p.IsMonicOfDegree n → ∃ q, p = Polynomial.X ^ n + q ∧ q.natDegree < n