mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.prod_apply : ∀ {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [inst : Ring 𝕜] [inst_1 : Preorder α] [inst_2 : Preorder β]
  (f : IncidenceAlgebra 𝕜 α) (g : IncidenceAlgebra 𝕜 β) (x y : α × β), (f.prod g) x y = f x.1 y.1 * g x.2 y.2
-- Mathlib.LinearAlgebra.Complex.Module
imaginaryPart_eq_neg_I_smul_skewAdjointPart : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  (x : A), ↑(imaginaryPart x) = -Complex.I • ↑((skewAdjointPart ℝ) x)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succ_le_succ : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LE a b → Std.PRange.UpwardEnumerable.LE (Std.PRange.succ a) (Std.PRange.succ b)
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.homGroupoid : (B : Type u₁) →
  [inst : CategoryTheory.Bicategory B] → (a b : CategoryTheory.Bicategory.Pith B) → CategoryTheory.Groupoid (a ⟶ b)
-- Mathlib.Data.Stream.Init
Stream'.cons_get_inits_core : ∀ {α : Type u} (a : α) (n : ℕ) (l : List α) (s : Stream' α),
  a :: (Stream'.initsCore l s).get n = (Stream'.initsCore (a :: l) s).get n
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.DBuilderName.instToString : ToString Aesop.Frontend.DBuilderName
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.monomorphisms_le_monoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass],
  CategoryTheory.MorphismProperty.monomorphisms C ≤ P.monoModSerre
-- Mathlib.Order.Basic
/-- **Alias** of `ge_antisymm`. -/
LE.le.antisymm' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ≤ a → a ≤ b → a = b
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.instToJsonModuleHierarchy : Lean.ToJson Lean.Lsp.Ipc.ModuleHierarchy
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.coe_comp : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B]
  [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B),
  ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Lean.Level
/-- Auxiliary function used at `normalize`.
Remarks:
- `lvls` are sorted using `normLt`
- `extraK` is the outer offset of the `max` term. We will push it inside.
- `i` is the current array index
- `prev + prevK` is the "previous" level that has not been added to `result` yet.
- `result` is the accumulator
 -/
_private.Lean.Level.0.Lean.Level.mkMaxAux : Array Lean.Level → ℕ → ℕ → Lean.Level → ℕ → Lean.Level → Lean.Level
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_inv_app_app_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type}
  [inst_1 : CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) (X : J)
  (X_1 : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)
  (a :
    ((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A K).obj
          X).obj
      X_1),
  (CategoryTheory.ConcreteCategory.hom
        (((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso A
                    K).inv.app
              X).app
          X_1))
      a =
    a
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_congr : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} {f g : α → E}, f =ᵐ[μ] g → ⨍ (x : α), f x ∂μ = ⨍ (x : α), g x ∂μ
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.AtomM.Recurse.Config
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on `R`, the sphere of radius `r`
around zero `{x | v.restrict x = r}` is clopen in the valuative topology.  -/
Valuation.isClopen_sphere : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  {r : (MonoidWithZeroHom.ofClass v).ValueGroup₀}, r ≠ 0 → IsClopen {x | v.restrict x = r}
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iic_disjoint_Ioc : ∀ {α : Type u_2} {a b c : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : LocallyFiniteOrder α],
  a ≤ b → Disjoint (Finset.Iic a) (Finset.Ioc b c)
-- Mathlib.Topology.ContinuousMap.Basic
/-- Giving a continuous map out of a disjoint union is the same as giving a continuous map out of
each term
 -/
ContinuousMap.piEquiv : {I : Type u_5} →
  (A : Type u_6) →
    (X : I → Type u_7) →
      [inst : TopologicalSpace A] →
        [inst_1 : (i : I) → TopologicalSpace (X i)] → ((i : I) → C(A, X i)) ≃ C(A, (i : I) → X i)
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.measure_mul_right_null : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] {s : Set G} [MeasurableInv G] [μ.IsMulLeftInvariant] (y : G),
  μ ((fun x => x * y) ⁻¹' s) = 0 ↔ μ s = 0
-- Mathlib.Algebra.Homology.BifunctorShift
/-- Given `K₁ : CochainComplex C₁ ℤ`, `K₂ : CochainComplex C₂ ℤ`,
a bifunctor `F : C₁ ⥤ C₂ ⥤ D`, this `mapBifunctor K₁ K₂ F : CochainComplex D ℤ`
is the total complex of the bicomplex obtained by applying `F` to `K₁` and `K₂`.  -/
CochainComplex.mapBifunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
              [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                (K₁ : CochainComplex C₁ ℤ) →
                  (K₂ : CochainComplex C₂ ℤ) →
                    [inst_5 : CategoryTheory.Preadditive D] →
                      (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                        [inst_6 : F.PreservesZeroMorphisms] →
                          [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                            [K₁.HasMapBifunctor K₂ F] → CochainComplex D ℤ
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_Ioo_add_eq_sum_Ioc : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a < b → ∑ x ∈ Finset.Ioo a b, f x + f b = ∑ x ∈ Finset.Ioc a b, f x
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.length_add : ∀ {α : Type u_1} (a b : FreeAddMonoid α), (a + b).length = a.length + b.length
-- Mathlib.Data.Complex.Basic
/-- The natural `AddEquiv` from `ℂ` to `ℝ × ℝ`.  -/
Complex.equivRealProdAddHom : ℂ ≃+ ℝ × ℝ
-- Std.Time.Zoned.Database.Basic
/-- Converts a transition.
 -/
Std.Time.TimeZone.convertTransition : Array Std.Time.TimeZone.LocalTimeType → ℕ → Std.Time.TimeZone.TZif.TZifV1 → Option Std.Time.TimeZone.Transition
-- Mathlib.Topology.PartialHomeomorph.Defs
/-- Replace `toPartialEquiv` field to provide better definitional equalities.  -/
PartialHomeomorph.replacePartialEquiv : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e : PartialHomeomorph X Y) → (e' : PartialEquiv X Y) → e.toPartialEquiv = e' → PartialHomeomorph X Y
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.group : {k : Type u_1} →
  {P₁ : Type u_2} →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] → [inst_2 : Module k V₁] → [inst_3 : AddTorsor V₁ P₁] → Group (P₁ ≃ᵃ[k] P₁)
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.sub_mul_left_left_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime (x - y * z) y ↔ IsRelPrime x y
-- Std.Data.ExtDHashMap.Basic
/-- Inserts multiple keys with the value `()` into the hash map by iterating over the given collection
and calling `insertIfNew`. If the same key appears multiple times, the first occurrence takes
precedence.

This is mainly useful to implement `HashSet.insertMany`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.
 -/
Std.ExtDHashMap.Const.insertManyIfNewUnit : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      [EquivBEq α] →
        [LawfulHashable α] →
          {ρ : Type w} → [ForIn Id ρ α] → (Std.ExtDHashMap α fun x => Unit) → ρ → Std.ExtDHashMap α fun x => Unit
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.span_extend_eq_span : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s t : Set V}
  (hs : LinearIndepOn K id s) (hst : s ⊆ t), Submodule.span K (hs.extend hst) = Submodule.span K t
-- Std.Async.System
Std.Async.System.GroupInfo.mk.inj : ∀ {groupName : String} {groupId : Std.Async.System.GroupId} {members : Array String} {groupName_1 : String}
  {groupId_1 : Std.Async.System.GroupId} {members_1 : Array String},
  { groupName := groupName, groupId := groupId, members := members } =
      { groupName := groupName_1, groupId := groupId_1, members := members_1 } →
    groupName = groupName_1 ∧ groupId = groupId_1 ∧ members = members_1
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- If the action is not trivial, then the trivial blocks condition implies preprimitivity
(pretransitivity is automatic)  -/
AddAction.IsPreprimitive.mk' : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X],
  AddAction.fixedPoints G X ≠ ⊤ →
    (∀ {B : Set X}, AddAction.IsBlock G B → AddAction.IsTrivialBlock B) → AddAction.IsPreprimitive G X
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- The bifunctor `Cᵒᵖ ⥤ C ⥤ V` which sends `X : Cᵒᵖ` and `Y : C` to `X ⟶[V] Y`.  -/
CategoryTheory.eHomFunctor : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u) →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [CategoryTheory.EnrichedOrdinaryCategory V C] → CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C V)
-- Init.Data.List.MinMaxOn
List.foldl.induct_unfolding : ∀ {α : Type u} {β : Type v} (f : α → β → α) (motive : α → List β → α → Prop),
  (∀ (a : α), motive a [] a) →
    (∀ (a : α) (b : β) (l : List β),
        motive (f a b) l (List.foldl f (f a b) l) → motive a (b :: l) (List.foldl f (f a b) l)) →
      ∀ (init : α) (a : List β), motive init a (List.foldl f init a)
-- Init.GrindInstances.Ring.UInt
UInt8.natCast : NatCast UInt8
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.ediam_image : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (s : Set E), Metric.ediam (⇑e '' s) = Metric.ediam s
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace : ∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {p : ENNReal} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [hm : Fact (m ≤ m0)]
  [CompleteSpace F] [hp : Fact (1 ≤ p)], CompleteSpace ↥(MeasureTheory.lpMeas F 𝕜 m p μ)
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a `Cone F.op` into a `Cocone F`.  -/
CategoryTheory.Limits.Cone.unop : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.Cone F.op → CategoryTheory.Limits.Cocone F
-- Init.Data.Array.Lemmas
Array.filterMap_eq_push_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {ys : Array β} {b : β},
  Array.filterMap f xs = ys.push b ↔
    ∃ as a bs, xs = as.push a ++ bs ∧ Array.filterMap f as = ys ∧ f a = some b ∧ ∀ x ∈ bs, f x = none
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `L` is an algebraically closed field containing `E`, such that the map
`(E →+* L) → (F →+* L)` induced by `algebraMap F E` is injective, then `E / F` is
purely inseparable. As a corollary, epimorphisms in the category of fields must be
purely inseparable extensions.  -/
IsPurelyInseparable.of_injective_comp_algebraMap : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : Type w) [inst_3 : Field L]
  [IsAlgClosed L] [Nonempty (E →+* L)], (Function.Injective fun f => f.comp (algebraMap F E)) → IsPurelyInseparable F E
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- The functor `κ.ord.ToType ⥤ Arrow C ⥤ Arrow C` corresponding to the
iterations of the successor structure `succStruct I κ`.  -/
CategoryTheory.SmallObject.iterationFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [I.IsCardinalForSmallObjectArgument κ] →
              CategoryTheory.Functor κ.ord.ToType
                (CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow C))
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.greatestFib_eq_zero : ∀ {n : ℕ}, n.greatestFib = 0 ↔ n = 0
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `α` and `β` are arbitrary types and there is a bijection between them,
then the induced map on their free groups is also bijective.  -/
FreeGroup.map_bijective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Bijective f → Function.Bijective ⇑(FreeGroup.map f)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.neg_Ioi : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a : α),
  -Set.Ioi a = Set.Iio (-a)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.erase_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.erase k = ∅ ↔ t = ∅ ∨ t.size = 1 ∧ k ∈ t
-- Mathlib.Topology.Compactness.Lindelof
IsLindelof.compl_mem_coLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsLindelof s → sᶜ ∈ Filter.coLindelof X
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.smulZeroClass : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → {A : Type u_8} → [SMulZeroClass A R] → SMulZeroClass A (AddMonoidAlgebra R M)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasFDerivWithinAt.sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {s : Set E}, HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Real.sinh (f x)) (Real.cosh (f x) • f') s x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldl.eq_1 : ∀ {σ : Sort u_1} {α : Type u_2} (f : σ → α → σ) (x : σ), RBTree.RBNode.foldl f x RBTree.RBNode.nil = x
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRelO.refl : ∀ {α : Type u} (R : α → α → Prop) [Std.Refl R], Std.Refl (Stream'.WSeq.LiftRelO R fun x1 x2 => x1 = x2)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.comp_contDiffAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {g : F → G} {f : E → F} (x : E),
  ContDiff 𝕜 n g → ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n (g ∘ f) x
-- Mathlib.Data.Fintype.Sets
Set.toFinset_ofPred : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : Fintype ↑{x | p x}],
  {x | p x}.toFinset = Finset.filter p Finset.univ
-- Mathlib.Data.List.Basic
List.idxOf_getLast : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l : List α} (hl : l ≠ []),
  l.getLast hl ∉ l.dropLast → List.idxOf (l.getLast hl) l = l.length - 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.keys_insertIfNew_perm : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (m.insertIfNew k v).keys.Perm (if k ∈ m then m.keys else k :: m.keys)
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.spanSingleton_div_self : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {x : K},
  x ≠ 0 →
    FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x / FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x = 1
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- A point belongs to the closure of `s` iff its infimum edistance to this set vanishes  -/
Metric.mem_closure_iff_infEDist_zero : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, x ∈ closure s ↔ Metric.infEDist x s = 0
-- Lean.Level
/-- Auxiliary function for `normalize`. It assumes `lvls` has been sorted using `normLt`.
It finds the first position that is not an explicit universe.
 -/
_private.Lean.Level.0.Lean.Level.skipExplicit : Array Lean.Level → ℕ → ℕ
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeUnopOppositeOfIsClosedUnderColimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] (Q : CategoryTheory.ObjectProperty Cᵒᵖ)
  [Q.IsClosedUnderColimitsOfShape J], Q.unop.IsClosedUnderLimitsOfShape Jᵒᵖ
-- Mathlib.Computability.Partrec
Partrec.sumCasesOn_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
  [inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ → σ},
  Computable f → Partrec₂ g → Computable₂ h → Partrec fun a => Sum.casesOn (f a) (g a) fun c => Part.some (h a c)
-- Batteries.Util.ProofWanted
/-- Parses the surface syntax of `def_wanted` and forwards to the shared `elabWanted`.  -/
elabDefWanted : Lean.Elab.Command.CommandElab
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_le_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k km : α} (hc : k ∈ t),
  t.min?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalAlgebra.elemental.le_of_mem : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] [inst_5 : TopologicalSpace A]
  [inst_6 : IsSemitopologicalSemiring A] [inst_7 : ContinuousConstSMul R A] {x : A} {s : NonUnitalSubalgebra R A},
  IsClosed ↑s → x ∈ s → NonUnitalAlgebra.elemental R x ≤ s
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.comm₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f self.h₁ + self.h₀ + φ₂.τ₁
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.logRatio_nonneg : ∀ {c : ENNReal}, 2⁻¹ ≤ c → c ≤ 1 → 0 ≤ ProbabilityTheory.Fernique.logRatio c
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
dist_prod_same_right : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {x₁ x₂ : α} {y : β},
  dist (x₁, y) (x₂, y) = dist x₁ x₂
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv_inter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t₁ t₂ : Set β}, s /ₛ t₁ ∩ t₂ ⊆ (s /ₛ t₁) ∩ (s /ₛ t₂)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The duality isomorphism `S.L₂'.op ≅ S.op.L₁'`.  -/
CategoryTheory.ShortComplex.SnakeInput.L₂'OpIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → (S : CategoryTheory.ShortComplex.SnakeInput C) → S.L₂'.op ≅ S.op.L₁'
-- Mathlib.Order.DirSupClosed
DirSupInacc.mem_iff_of_antisymmRel : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  DirSupInacc s → ∀ {a b : α}, AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → (a ∈ s ↔ b ∈ s)
-- Mathlib.Order.Defs.Unbundled
/-- An upper set in an order `α` is a set such that any element greater than one of its members is
also a member. Also called up-set, upward-closed set.  -/
IsUpperSet : {α : Type u_1} → [LE α] → Set α → Prop
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_iff_isBoundedUnder_le_div : ∀ {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [inst : Norm E] [inst_1 : NormedAddCommGroup F''] {f : α → E}
  {g'' : α → F''} {l : Filter α},
  (∀ᶠ (x : α) in l, g'' x ≠ 0) → (f =O[l] g'' ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x‖ / ‖g'' x‖)
-- Mathlib.Algebra.Exact.Basic
Function.MulExact.of_ladder_mulEquiv_of_mulExact' : ∀ {X₁ : Type u_8} {X₂ : Type u_9} {X₃ : Type u_10} {Y₁ : Type u_11} {Y₂ : Type u_12} {Y₃ : Type u_13}
  [inst : CommMonoid X₁] [inst_1 : CommMonoid X₂] [inst_2 : CommMonoid X₃] [inst_3 : CommMonoid Y₁]
  [inst_4 : CommMonoid Y₂] [inst_5 : CommMonoid Y₃] (e₁ : X₁ ≃* Y₁) (e₂ : X₂ ≃* Y₂) (e₃ : X₃ ≃* Y₃) {f₁₂ : X₁ →* X₂}
  {f₂₃ : X₂ →* X₃} {g₁₂ : Y₁ →* Y₂} {g₂₃ : Y₂ →* Y₃},
  g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂ →
    g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃ → Function.MulExact ⇑g₁₂ ⇑g₂₃ → Function.MulExact ⇑f₁₂ ⇑f₂₃
-- Mathlib.Probability.Kernel.CondDistrib
/-- For almost every `a : α`, the `condDistrib Y X μ` kernel applied to `X a` and a measurable set
`s` is equal to the conditional expectation of the indicator of `Y ⁻¹' s`.  -/
ProbabilityTheory.condDistrib_ae_eq_condExp : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {s : Set Ω},
  Measurable X →
    Measurable Y →
      MeasurableSet s →
        (fun a => ((ProbabilityTheory.condDistrib Y X μ) (X a)).real s) =ᵐ[μ]
          μ[(Y ⁻¹' s).indicator fun ω => 1 | MeasurableSpace.comap X mβ]
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.pOpcyclesIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i i_1 : ι) (e_i : i = i_1) (j : ι)
  (hi : c.prev j = i) (h : K.d i j = 0) [inst_2 : K.HasHomology j], K.pOpcyclesIso i j hi h = K.pOpcyclesIso i_1 j ⋯ ⋯
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- `AlgHom` version of `RingHom.liftOfSurjective` that descends an algebra homomorphism
along a surjection.  -/
AlgHom.liftOfSurjective : {R : Type u_5} →
  {A : Type u_6} →
    {B : Type u_7} →
      {C : Type u_8} →
        [inst : CommRing R] →
          [inst_1 : CommRing A] →
            [inst_2 : CommRing B] →
              [inst_3 : CommRing C] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Algebra R B] →
                    [inst_6 : Algebra R C] →
                      (f : A →ₐ[R] B) →
                        Function.Surjective ⇑f →
                          (g : A →ₐ[R] C) → RingHom.ker f.toRingHom ≤ RingHom.ker g.toRingHom → B →ₐ[R] C