mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Oscillation
oscillationWithin.eq_1 : ∀ {E : Type u} {F : Type v} [inst : PseudoEMetricSpace F] [inst_1 : TopologicalSpace E] (f : E → F) (D : Set E) (x : E),
  oscillationWithin f D x = ⨅ S ∈ Filter.map f (nhdsWithin x D), Metric.ediam S
-- Mathlib.Algebra.Algebra.Subalgebra.Order
Subalgebra.toIsStrictOrderedRing : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : PartialOrder A]
  [IsStrictOrderedRing A] [inst_4 : Algebra R A] (S : Subalgebra R A), IsStrictOrderedRing ↥S
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.rat_dense : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (q : ℚ_[p]) {ε : ℝ}, 0 < ε → ∃ r, ‖q - ↑r‖ < ε
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.PartialMatch.mk.sizeOf_spec : ∀ (keys : List Lean.Meta.RefinedDiscrTree.Key) (score : ℕ) (trie : Lean.Meta.RefinedDiscrTree.TrieIndex)
  (treeStars : Std.HashMap ℕ (List Lean.Meta.RefinedDiscrTree.Key)),
  sizeOf { keys := keys, score := score, trie := trie, treeStars := treeStars } =
    1 + sizeOf keys + sizeOf score + sizeOf trie + sizeOf treeStars
-- Mathlib.RingTheory.KrullDimension.Regular
/-- [Stacks Tag 00KW](https://stacks.math.columbia.edu/tag/00KW) -/
ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] {x : R},
  x ∈ nonZeroDivisors R → x ∈ IsLocalRing.maximalIdeal R → ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR.run.match_3.splitter : {α : Type u_1} →
  (motive : (x : ℕ) → { l // l.length = x } → Sort u_2) →
    (x : ℕ) →
      (x_1 : { l // l.length = x }) →
        ((property : [].length = 0) → motive 0 ⟨[], property⟩) →
          ((a : α) → (property : [a].length = 1) → motive 1 ⟨[a], property⟩) →
            ((n : ℕ) → (xs : { l // l.length = n + 2 }) → motive n.succ.succ xs) → motive x x_1
-- Mathlib.LinearAlgebra.Matrix.ToLin
dotProductBilin_apply_apply : ∀ {m : Type u_2} (R : Type u_4) (S : Type u_5) {A : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : SMulCommClass S R A]
  [inst_6 : SMulCommClass S A A] [inst_7 : IsScalarTower R A A] [inst_8 : Fintype m] (x y : m → A),
  ((dotProductBilin R S) x) y = x ⬝ᵥ y
-- Mathlib.Data.Multiset.ZeroCons
Multiset.instUniqueOfIsEmpty : {α : Type u_1} → [IsEmpty α] → Unique (Multiset α)
-- Mathlib.Order.Sublattice
Sublattice.pi_univ_eq_bot_iff : ∀ {κ : Type u_5} {π : κ → Type u_6} [inst : (i : κ) → Lattice (π i)] {L : (i : κ) → Sublattice (π i)},
  Sublattice.pi Set.univ L = ⊥ ↔ ∃ i, L i = ⊥
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.pOpcycles_restrictionOpcyclesIso_hom_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j : ι) (hi : c.prev j = i) {i' j' : ι'}
  (hi' : e.f i = i') (hj' : e.f j = j') (hi'' : c'.prev j' = i') [inst_3 : K.HasHomology j']
  [inst_4 : (K.restriction e).HasHomology j] {Z : C} (h : K.opcycles j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((K.restriction e).pOpcycles j)
      (CategoryTheory.CategoryStruct.comp (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom h) =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').hom
      (CategoryTheory.CategoryStruct.comp (K.pOpcycles j') h)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
two_mul_le_add_of_sq_eq_mul : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R]
  [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] {a b r : R}, 0 ≤ a → 0 ≤ b → r ^ 2 = a * b → 2 * r ≤ a + b
-- Mathlib.RingTheory.PicardGroup
/-- Exactness of the sequence `1 → Rˣ → Aˣ → (Submodule R A)ˣ → Pic R → Pic A` at `Pic R`.  -/
Submodule.mulExact_unitsToPic_mapAlgebra : ∀ (R : Type u) (A : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A], Function.MulExact ⇑(Submodule.unitsToPic R A) ⇑(CommRing.Pic.mapAlgebra R A)
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
`none` if no such element is found.

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

This variant requires terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.findM?`.

Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].iter.findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false
```
```output
Almost! 6
Almost! 5
```
```output
some 1
```
 -/
Std.Iter.Total.findM? : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α Id β] →
        [Std.IteratorLoop α Id m] →
          [Std.Iterators.Finite α Id] → Std.Iter.Total β → (β → m (ULift.{w, 0} Bool)) → m (Option β)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.isBigO : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → u =O[l] v
-- Init.Data.Nat.Coprime
Nat.Coprime.gcd_eq_one : ∀ {m n : ℕ}, m.Coprime n → m.gcd n = 1
-- Mathlib.Tactic.CrossRefAttribute
/-- The main parser for Wikidata identifiers: it accepts `Q` followed by one or more digits.  -/
Mathlib.CrossRef.wikidataIdFn : Lean.Parser.ParserFn
-- Init.Data.Float.Model.Float32
/-- Compute the ordering between two `Float32.Model` as specified by IEEE. Returns an
`Option Ordering` to account for the fact that `NaN` is incomparable with everything.
Also, positive and negative zero are equal.
 -/
Float32.Model.compare : Float32.Model → Float32.Model → Option Ordering
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_neg : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
  (x : ↥p), ↑(-x) = -↑x
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, returning `none` if no such key exists.
 -/
Std.ExtTreeMap.getKeyLE? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → Option α
-- Batteries.Data.List.Interleave
List.nil_interleave : ∀ {α : Type u_1} (l₂ : List α), [].interleave l₂ = l₂
-- Mathlib.Data.Set.Image
Set.compl_range_inl : ∀ {α : Type u_1} {β : Type u_2}, (Set.range Sum.inl)ᶜ = Set.range Sum.inr
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.state : {α : Type} → Std.CloseableChannel.Unbounded✝ α → Std.Mutex (Std.CloseableChannel.Unbounded.State✝ α)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} [inst_4 : F₁.LaxMonoidal] [inst_5 : F₂.LaxMonoidal],
  autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F₁)
          (τ.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) =
        CategoryTheory.Functor.LaxMonoidal.ε F₂)
      CategoryTheory.NatTrans.IsMonoidal.unit._autoParam →
    autoParam
        (∀ (X Y : C),
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F₁ X Y)
              (τ.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) =
            CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (τ.app X) (τ.app Y))
              (CategoryTheory.Functor.LaxMonoidal.μ F₂ X Y))
        CategoryTheory.NatTrans.IsMonoidal.tensor._autoParam →
      CategoryTheory.NatTrans.IsMonoidal τ
-- Lean.Data.Lsp.Basic
Lean.Lsp.RenameFile.annotationId? : Lean.Lsp.RenameFile → Option String
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.exists_iff : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ {P : Set α → Prop}, (∀ ⦃s t : Set α⦄, s ⊆ t → P t → P s) → ((∃ s ∈ l, P s) ↔ ∃ i, p i ∧ P (s i))
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_Ioc : ∀ (x y : ↑unitInterval), MeasureTheory.volume (Set.Ioc x y) = ENNReal.ofReal (↑y - ↑x)
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.instNeg : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → Neg (M →ₗ⁅R,L⁆ N)
-- Mathlib.Order.Hom.Order
OrderHom.coe_iSup : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {ι : Sort u_3} [inst_1 : CompleteLattice β] (f : ι → α →o β),
  ⇑(⨆ i, f i) = ⨆ i, ⇑(f i)
-- Init.Data.UInt.Bitwise
UInt64.toUInt16_or : ∀ (a b : UInt64), (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.swap_copy : ∀ {α : Type u_1} {mα : MeasurableSpace α},
  (ProbabilityTheory.Kernel.swap α α).comp (ProbabilityTheory.Kernel.copy α) = ProbabilityTheory.Kernel.copy α
-- Mathlib.Topology.Path
/-- Pointwise multiplication of paths in a topological group.  -/
Path.mul : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    [inst_1 : Mul X] → [ContinuousMul X] → {a₁ b₁ a₂ b₂ : X} → Path a₁ b₁ → Path a₂ b₂ → Path (a₁ * a₂) (b₁ * b₂)
-- Init.Grind.ToInt
/-- The embedding takes addition to addition, wrapped into the range interval.  -/
Lean.Grind.ToInt.Add.toInt_add : ∀ {α : Type u} {inst : Add α} {I : outParam Lean.Grind.IntInterval} {inst_1 : Lean.Grind.ToInt α I}
  [self : Lean.Grind.ToInt.Add α I] (x y : α), ↑(x + y) = I.wrap (↑x + ↑y)
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The structure morphism associated to an algebra.  -/
CategoryTheory.Monad.Algebra.a : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} → (self : T.Algebra) → T.obj self.A ⟶ self.A
-- Mathlib.Data.ENNReal.Action
ENNReal.smul_def : ∀ {M : Type u_1} [inst : MulAction ENNReal M] (c : NNReal) (x : M), c • x = ↑c • x
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsFraisseLimit.age : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} {M : Type w} [inst : L.Structure M]
  [inst_1 : Countable ((l : ℕ) × L.Functions l)] [inst_2 : Countable M],
  FirstOrder.Language.IsFraisseLimit K M → L.age M = K
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_erase!_le_maxKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false →
        (compare (Std.DTreeMap.Internal.Impl.erase! k t).maxKey! t.maxKey!).isLE = true
-- Mathlib.Algebra.Field.ULift
ULift.field : {α : Type u} → [Field α] → Field (ULift.{u_1, u} α)
-- Init.Data.Dyadic.Basic
Dyadic.ble.eq_2 : ∀ (n k : ℤ) (hn : n % 2 = 1), Dyadic.zero.ble (Dyadic.ofOdd n k hn) = decide (0 ≤ n)
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf_of_mem : ∀ {α : Type u_1} [inst : SemilatticeInf α] {s : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : BoundedOrder α]
  (h : a ∈ upperClosure ↑s), s.truncatedInf a = {b ∈ s | b ≤ a}.inf' ⋯ id
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.postcompEquiv_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} [inst_3 : W.RespectsIso]
  [inst_4 : W.IsCompatibleWithShift M] [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Y]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y]
  [inst_10 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z] (f : Y ⟶ Z) (hf : W f) {a : M}
  (β : CategoryTheory.Localization.SmallShiftedHom W X Z a),
  (CategoryTheory.Localization.SmallShiftedHom.postcompEquiv f hf).symm β =
    β.comp (CategoryTheory.Localization.SmallShiftedHom.mk₀Inv 0 ⋯ f hf) ⋯
-- Mathlib.SetTheory.Cardinal.Defs
/-- Similar to `mk_sigma_congr` with indexing types in different universes. This is not a strict
generalization.  -/
Cardinal.mk_sigma_congr' : ∀ {ι : Type u} {ι' : Type v} {f : ι → Type (max w u v)} {g : ι' → Type (max w u v)} (e : ι ≃ ι'),
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) → Cardinal.mk ((i : ι) × f i) = Cardinal.mk ((i : ι') × g i)
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
/-- Given `X : TopCat`, this is the bijection between `1`-simplices of the
singular simplicial set of `X` and the type of morphisms `I ⟶ X`.  -/
TopCat.toSSetObj₁Equiv : {X : TopCat} → (TopCat.toSSet.obj X).obj (Opposite.op { len := 1 }) ≃ (TopCat.I ⟶ X)
-- Mathlib.FieldTheory.Separable
isSeparable_algebraMap : ∀ {F : Type u_1} [inst : Field F] {K : Type u_2} [inst_1 : Ring K] [inst_2 : Algebra F K] (x : F),
  IsSeparable F ((algebraMap F K) x)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.fst_toFun : ∀ (R : Type u) [inst : Monoid R] (A : Type v) (B : Type w) [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : DistribMulAction R B] (self : A × B),
  (NonUnitalAlgHom.fst R A B) self = self.1
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.interSmallerFn.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3)
  (h_1 : (kv' : (a : α) × β a) → motive (some kv')) (h_2 : Unit → motive none),
  (match none with
    | some kv' => h_1 kv'
    | none => h_2 ()) =
    h_2 ()
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_eq_getElem?_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.min? = t.toArray[0]?
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
MulLeftReflectLE.mk : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : LE M], (∀ {a b₁ b₂ : M}, a * b₁ ≤ a * b₂ → b₁ ≤ b₂) → MulLeftReflectLE M
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.addCommGroup.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R],
  AddMonoidAlgebra.addCommGroup =
    { toAddMonoid := AddMonoidAlgebra.instAddMonoid,
      neg := fun a => AddMonoidAlgebra.coeffEquiv.2 (-AddMonoidAlgebra.coeffEquiv.toFun a),
      sub := fun a a_1 =>
        AddMonoidAlgebra.coeffEquiv.2 (AddMonoidAlgebra.coeffEquiv.toFun a - AddMonoidAlgebra.coeffEquiv.toFun a_1),
      toZSMul := ZSMul.ofSMul, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯,
      neg_add_cancel := ⋯, add_comm := ⋯ }
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.of_symm_smul : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (r : R) (x : LieAlgebra.ofTwoCocycle c),
  (LieAlgebra.ofProd c).symm (r • x) = r • (LieAlgebra.ofProd c).symm x
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
AlternatingMap.measure_def : ∀ {G : Type u_4} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] [inst_2 : MeasurableSpace G]
  [inst_3 : BorelSpace G] [inst_4 : FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (Module.finrank ℝ G = n)]
  (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ),
  ω.measure = ‖ω ⇑(Module.finBasisOfFinrankEq ℝ G ⋯)‖₊ • (Module.finBasisOfFinrankEq ℝ G ⋯).addHaar
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_le_minKey!_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → (cmp t.minKey! (t.erase k).minKey!).isLE = true
-- Mathlib.Order.CompleteLattice.Basic
sSup_union : ∀ {α : Type u_1} [inst : CompleteLattice α] {s t : Set α}, sSup (s ∪ t) = sSup s ⊔ sSup t
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.ext_iff : ∀ {M : Type u_1} [inst : Mul M] {S T : Subsemigroup M}, S = T ↔ ∀ (x : M), x ∈ S ↔ x ∈ T
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The center of a (not necessarily unital or associative) semiring
is isomorphic to the center of its opposite.  -/
NonUnitalSubsemiring.centerToMulOpposite : {R : Type u} →
  [inst : NonUnitalNonAssocSemiring R] → ↥(NonUnitalSubsemiring.center R) ≃+* ↥(NonUnitalSubsemiring.center Rᵐᵒᵖ)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.mul_le_right_iff_opow_omega0_dvd : ∀ {a b : Ordinal.{u_1}}, 0 < a → (a * b ≤ b ↔ a ^ Ordinal.omega0 ∣ b)
-- Lean.Meta.Match.CaseArraySizes
Lean.Meta.getArrayArgType : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.Finsupp.Basic
Finsupp.mem_frange : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {y : M}, y ∈ f.frange ↔ y ≠ 0 ∧ y ∈ Set.range ⇑f
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.SelectM.State.mk.sizeOf_spec : ∀ (suggestions : Array Lean.Meta.Tactic.TryThis.Suggestion) (thms : Array Lean.Meta.Grind.EMatchTheorem),
  sizeOf { suggestions := suggestions, thms := thms } = 1 + sizeOf suggestions + sizeOf thms
-- Mathlib.Order.Bounds.Image
image2_lowerBounds_upperBounds_subset_upperBounds_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → Set.image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (Set.image2 f s t)
-- Std.Time.Date.Unit.Week
Std.Time.Week.instReprOffset : Repr Std.Time.Week.Offset
-- Init.Data.Bool
Bool.not_and_eq_left_iff_and : ∀ {a b : Bool}, (!a && b) = a ↔ (!a) = true ∧ (!b) = true
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- `reflectionCircumcenterWeightsWithCircumcenter` sums to 1.  -/
Affine.Simplex.sum_reflectionCircumcenterWeightsWithCircumcenter : ∀ {n : ℕ} {i₁ i₂ : Fin (n + 1)}, i₁ ≠ i₂ → ∑ i, Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i = 1
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `mdifferentiableOn_baseSet_localFrameCoeff`.

---

If `s` is differentiable on `e.baseSet`, so is its coefficient `b.localFrameCoeff e i` in the
local frame induced by `e`  -/
mdifferentiableOn_baseSet_localFrame_coeff : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x}
  [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜],
  MDiff[e.baseSet] (T% s) →
    ∀ (i : ι), MDiff[e.baseSet] ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s)
-- Mathlib.Data.Sym.Sym2
/-- **Alias** of `Sym2.fromRel_irrefl`. -/
Sym2.fromRel_irreflexive : ∀ {α : Type u_1} {r : α → α → Prop} {sym : Std.Symm r}, Std.Irrefl r ↔ ∀ {z : Sym2 α}, z ∈ Sym2.fromRel sym → ¬z.IsDiag
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.beq_iff_equiv : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.TreeMap α β cmp} [inst : BEq β] [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [LawfulBEq β], (m₁ == m₂) = true ↔ m₁.Equiv m₂
-- Mathlib.GroupTheory.Rank
Group.rank_eq_zero : ∀ (G : Type u_1) [inst : Group G] [inst_1 : Subsingleton G], Group.rank G = 0
-- Mathlib.Order.SuccPred.Basic
Order.pred_le_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, b ≤ a → Order.pred b ≤ Order.pred a
-- Init.Data.String.TakeDrop
/-- Creates a new string by removing the longest suffix from `s` in which `pat` matches
\(potentially repeatedly\).

This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use `String.Slice.copy`.

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".dropEndWhile Char.isLower == "red green ".toSlice`

* `"red green blue".dropEndWhile 'e' == "red green blu".toSlice`

* `"red green blue".dropEndWhile (fun (_ : Char) => true) == "".toSlice`
 -/
String.dropEndWhile : {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → String.Slice
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mapRingHom_comp_mapRingHom : ∀ {R : Type u} [inst : CommSemiring R] {S : Type u_7} {T : Type u_8} [inst_1 : CommSemiring S] [inst_2 : CommSemiring T]
  {f : R →+* S} {g : S →+* T},
  (CommRing.Pic.mapRingHom g).comp (CommRing.Pic.mapRingHom f) = CommRing.Pic.mapRingHom (g.comp f)
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.refl_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b),
  CategoryTheory.BicategoricalCoherence.iso = CategoryTheory.Iso.refl f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_zero_right_eq_nil : ∀ {m : ℕ}, (m...0).toArray = #[]
-- Init.Data.String.PosRaw
String.Pos.Raw.dec_lt_iff : ∀ {p q : String.Pos.Raw}, p ≠ 0 → (p.dec < q ↔ p ≤ q)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_succ_right_eq_push : ∀ {m n : ℤ}, m ≤ n → (m<...=n + 1).toArray = (m<...=n).toArray.push (n + 1)
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.preimage_comap_zeroLocus : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (s : Set R),
  PrimeSpectrum.comap f ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus (⇑f '' s)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.nonempty : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α), (↑s).Nonempty
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.base_subset : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C), D ⊆ ↑E
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- A cone of a functor `K : J ⥤ Over X` consists of an object of `Over X`, together
with morphisms. This same object is a cone of the extended functor
`liftFromOver.obj K : WithTerminal J ⥤ C`.  -/
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.coneLift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          {K : CategoryTheory.Functor J (CategoryTheory.Over X)} →
            CategoryTheory.Functor (CategoryTheory.Limits.Cone K)
              (CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K))