mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Multilinear.Pi
MultilinearMap.piFamily_smul : ∀ {ι : Type uι} {κ : ι → Type uκ} {S : Type uS} {R : Type uR} {M : (i : ι) → κ i → Type uM}
  {N : ((i : ι) → κ i) → Type uN} [inst : Semiring R] [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)]
  [inst_4 : (p : (i : ι) → κ i) → Module R (N p)] [inst_5 : Monoid S]
  [inst_6 : (p : (i : ι) → κ i) → DistribMulAction S (N p)] [inst_7 : ∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)]
  (s : S) (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)),
  MultilinearMap.piFamily (s • f) = s • MultilinearMap.piFamily f
-- Init.Data.Char.Ordinal
Char.lt_iff_ofOrdinal_lt : ∀ {f g : Fin Char.numCodePoints}, f < g ↔ Char.ofOrdinal f < Char.ofOrdinal g
-- Mathlib.Logic.Relation
Relation.transGen_idem : ∀ {α : Type u_1} {r : α → α → Prop}, Relation.TransGen (Relation.TransGen r) = Relation.TransGen r
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsUniformizer.is_generator : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] {v : Valuation K Γ}
  [hv : v.IsRankOneDiscrete] {π : ↥v.valuationSubring},
  v.IsUniformizer ↑π → IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {π}
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`.  -/
AddEquiv.symm_apply_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) (x : M), e.symm (e x) = x
-- Init.Data.SInt.Lemmas
Int64.toInt_div_of_ne_left : ∀ (a b : Int64), a ≠ Int64.minValue → (a / b).toInt = a.toInt.tdiv b.toInt
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_bot`. -/
Ideal.ramificationIdx_bot : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Ideal S},
  ⊥.ramificationIdx' P = 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isEmpty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m.isEmpty = true ↔ m = ∅
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.isRing : {R : Type u} → [inst : CommRing R] → (self : AlgCat R) → Ring ↑self
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `get!` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.get!ₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.OrientedOrd α] → [Std.LawfulEqOrd α] → Std.DTreeMap.Internal.Impl α β → (k : α) → [Inhabited (β k)] → β k
-- Mathlib.Probability.ProductMeasure
/-- The product measure of an arbitrary family of probability measures. It is defined as the unique
extension of the function which gives to cylinders the measure given by the associated product
measure.

It is defined via an `if ... then ... else` so that it can be manipulated without carrying
a proof that the measures are probability measures.  -/
MeasureTheory.Measure.infinitePi : {ι : Type u_1} →
  {X : ι → Type u_2} →
    {mX : (i : ι) → MeasurableSpace (X i)} →
      ((i : ι) → MeasureTheory.Measure (X i)) → MeasureTheory.Measure ((i : ι) → X i)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_inf_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Surjective ⇑f →
    ∀ (S T : Subsemigroup N), Subsemigroup.map f (Subsemigroup.comap f S ⊓ Subsemigroup.comap f T) = S ⊓ T
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.eq_algebraMap_of_spectrum_subset_singleton : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A) (r : R),
  spectrum R a ⊆ {r} → autoParam (p a) CFC.eq_algebraMap_of_spectrum_subset_singleton._auto_1 → a = (algebraMap R A) r
-- Mathlib.RingTheory.Coprime.Lemmas
exists_sum_eq_one_iff_pairwise_coprime : ∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {s : I → R} {t : Finset I} [inst_1 : DecidableEq I],
  t.Nonempty → ((∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (Function.onFun IsCoprime fun i => s ↑i))
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withTopCongr_trans : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : Add α] [inst_1 : Add β] [inst_2 : Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ),
  (e₁.trans e₂).withTopCongr = e₁.withTopCongr.trans e₂.withTopCongr
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.pullback_def : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : AddGroup A] [inst_1 : AddGroup B]
  [inst_2 : AddGroup C] [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C]
  {φ : A →+ B} {ψ : B →+ C} (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A]
  [inst_7 : IsTopologicalAddGroup B] [inst_8 : NormedAddCommGroup E] (f : CompactlySupportedContinuousMap B E) (b : B)
  (a : A), (H.pullback f b) a = f (b + φ a)
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- The restriction of a Scheme along an open embedding.  -/
AlgebraicGeometry.Scheme.restrict : {U : TopCat} →
  (X : AlgebraicGeometry.Scheme) →
    {f : U ⟶ TopCat.of ↥X} →
      Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) → AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Algebra.Equiv
/-- `Equiv.cast (congrArg _ h)` as an algebra equiv.

Note that unlike `Equiv.cast`, this takes an equality of indices rather than an equality of types,
to avoid having to deal with an equality of the algebraic structure itself.  -/
AlgEquiv.cast : {R : Type uR} →
  [inst : CommSemiring R] →
    {ι : Type u_1} →
      {A : ι → Type u_2} →
        [inst_1 : (i : ι) → Semiring (A i)] → [inst_2 : (i : ι) → Algebra R (A i)] → {i j : ι} → i = j → A i ≃ₐ[R] A j
-- Lean.Widget.UserWidget
/-- When present, the infoview will wrap the widget
in `<details><summary>{name}</summary>...</details>`.
This functionality is deprecated
but retained for backwards compatibility
with `UserWidgetDefinition`.  -/
Lean.Widget.PanelWidgetInstance.name? : Lean.Widget.PanelWidgetInstance → Option String
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_adapt_ReaderT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ρ ρ' α : Type u}
  {post : α → ρ → Pred} {epost : EPred} (f : ρ → ρ') (x : ReaderT ρ' m α),
  Std.Internal.Do.wp (ReaderT.adapt f x) post epost = fun r => Std.Internal.Do.wp x (fun a x => post a r) epost (f r)
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.instInhabitedOrigin.default : Lean.Meta.Grind.Origin
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.mem_of_mem : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {i : ι}, l.HasBasis p s → p i → s i ∈ l
-- Lean.Elab.Tactic.Grind.Config
Lean.Elab.Tactic.elabGrindConfig : Lean.Syntax → optParam Lean.Grind.Config { } → optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Grind.Config
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_interSmaller : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] (l₁ l₂ : List ((a : α) × β a)) (k : α),
  Std.Internal.List.getEntry? k (Std.Internal.List.interSmaller l₁ l₂) =
    Option.filter (fun kv => Std.Internal.List.containsKey kv.fst l₂) (Std.Internal.List.getEntry? k l₁)
-- Mathlib.RingTheory.Radical.NatInt
Nat.radical_dvd_iff : ∀ {n k : ℕ}, k ≠ 0 → (UniqueFactorizationMonoid.radical n ∣ k ↔ n.primeFactors ⊆ k.primeFactors)
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.sourceAffineLocally.congr_simp : ∀ (P P_1 : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop),
  P = P_1 →
    ∀ ⦃X Y : AlgebraicGeometry.Scheme⦄ (x x_1 : X ⟶ Y),
      x = x_1 →
        ∀ [inst : AlgebraicGeometry.IsAffine Y],
          AlgebraicGeometry.sourceAffineLocally P x = AlgebraicGeometry.sourceAffineLocally P_1 x_1
-- Mathlib.Algebra.Group.ULift
ULift.leftCancelSemigroup : {α : Type u} → [LeftCancelSemigroup α] → LeftCancelSemigroup (ULift.{u_1, u} α)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- There exists a trail of maximal length in a non-empty graph on finite edges.  -/
SimpleGraph.Walk.exists_isTrail_forall_isTrail_length_le_length : ∀ {V : Type u} (G : SimpleGraph V) [N : Nonempty V] [Finite ↑G.edgeSet],
  ∃ u v p, ∃ (_ : p.IsTrail), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.count_map : ∀ {α β β' : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] [inst_1 : Monad m]
  [inst_2 : Std.IteratorLoop α m m] [Std.Iterators.Finite α m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m]
  {it : Std.IterM m β} {f : β → β'}, (Std.IterM.map f it).length = it.length
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- All sets of the family are measurable.  -/
VitaliFamily.measurableSet : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (self : VitaliFamily μ) (x : X), ∀ s ∈ self.setsAt x, MeasurableSet s
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.Agree'.below.step : ∀ {F : PFunctor.{uA, uB}} {motive : (a : ℕ) → (a_1 a_2 : F.M) → PFunctor.M.Agree' a a_1 a_2 → Prop} {n : ℕ} {a : F.A}
  (x y : F.B a → F.M) {x' y' : F.M} (a_1 : x' = PFunctor.M.mk ⟨a, x⟩) (a_2 : y' = PFunctor.M.mk ⟨a, y⟩)
  (a_3 : ∀ (i : F.B a), PFunctor.M.Agree' n (x i) (y i)),
  (∀ (i : F.B a), PFunctor.M.Agree'.below ⋯) → (∀ (i : F.B a), motive n (x i) (y i) ⋯) → PFunctor.M.Agree'.below ⋯
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- The information we keep track of when encountering a binder for an instance of concern.  -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern : Type
-- Init.Data.SInt.Lemmas
Int16.mul_one : ∀ (a : Int16), a * 1 = a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.snippet.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.snippet = 1
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instAddCommGroup : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] →
            [inst_2 : Module R V] →
              [inst_3 : TopologicalSpace P] →
                [inst_4 : AddTorsor V P] →
                  [inst_5 : AddCommGroup W] →
                    [inst_6 : Module R W] →
                      [inst_7 : TopologicalSpace W] → [IsTopologicalAddGroup W] → AddCommGroup (P →ᴬ[R] W)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mem_nthRootsFinset : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {n : ℕ},
  0 < n → ∀ (a : R) {x : R}, x ∈ Polynomial.nthRootsFinset n a ↔ x ^ n = a
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X : HomotopicalAlgebra.CofibrantObject C),
  HomotopicalAlgebra.IsCofibrant (HomotopicalAlgebra.CofibrantObject.ι.obj X)
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_map : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J},
  F.IsEventuallyConstantFrom i₀ → ∀ {i j : J} (φ : i ⟶ j) (ι : i₀ ⟶ i), CategoryTheory.IsIso (F.map φ)
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_monomial : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p : ℕ) (d : σ →₀ ℕ) (r : R),
  (MvPolynomial.expand p) ((MvPolynomial.monomial d) r) = (MvPolynomial.monomial (p • d)) r
-- Lean.Parser.Basic
Lean.Parser.antiquotNestedExpr : Lean.Parser.Parser
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_neg : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
  (p : Polynomial T), (-p).aroots S = p.aroots S
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.MeasurableSingletonClass.of_separatesPoints : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Countable α] [MeasurableSpace.SeparatesPoints α],
  MeasurableSingletonClass α
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
/-- A meromorphic function has a finite set of poles if and only if the logarithmic counting function
for its pole-divisor is big-O of `log`.
 -/
ValueDistribution.logCounting_isBigO_log_iff_finite_support : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E},
  ValueDistribution.logCounting f ⊤ =O[Filter.atTop] Real.log ↔ (MeromorphicOn.divisor f Set.univ)⁻.support.Finite
-- Mathlib.Topology.MetricSpace.Isometry
EMetricSpace.isometry_induced : ∀ {α : Type u} {β : Type v} (f : α → β) (hf : Function.Injective f) [m : EMetricSpace β], Isometry f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Bitwise not.
 -/
Std.Tactic.BVDecide.BVUnOp.not : Std.Tactic.BVDecide.BVUnOp
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.fromLocalizedModule'_mk : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m : M) (s : ↥S),
  IsLocalizedModule.fromLocalizedModule' S f (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (f m)
-- Mathlib.Data.List.Sort
List.sortedGT_iff_nodup_and_sortedGE : ∀ {α : Type u_1} {l : List α} [inst : PartialOrder α], l.SortedGT ↔ l.Nodup ∧ l.SortedGE
-- Mathlib.Data.Finset.Insert
Finset.mem_singleton : ∀ {α : Type u_1} {a b : α}, b ∈ {a} ↔ b = a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.getKey! a = t.getKeyD a default
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.restrict_isColoop_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α},
  R ⊆ M.E → ((M.restrict R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R)
-- Batteries.Data.DList.Basic
/-- The `apply` function of a `DList` is completely determined by the list `apply []`.  -/
Batteries.DList.invariant : ∀ {α : Type u} (self : Batteries.DList α) (l : List α), self.apply l = self.apply [] ++ l
-- Mathlib.Topology.ContinuousMap.Weierstrass
/-- The special case of the Weierstrass approximation theorem for the interval `[0,1]`.
This is just a matter of unravelling definitions and using the Bernstein approximations.
 -/
polynomialFunctions_closure_eq_top' : (polynomialFunctions unitInterval).topologicalClosure = ⊤
-- Mathlib.Topology.Constructions
isOpen_set_pi : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {i : Set ι} {s : (a : ι) → Set (A a)},
  i.Finite → (∀ a ∈ i, IsOpen (s a)) → IsOpen (i.pi s)
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the forward direction of `mdifferentiableAt_iff_differentiableAt`.

---

For maps between vector spaces, `MDifferentiableAt` and `DifferentiableAt` coincide  -/
MDifferentiableAt.differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {x : E}, MDiffAt f x → DifferentiableAt 𝕜 f x
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂'_obj_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X₁ : C)
  {X₂ Y₂ : C} (φ : X₂ ⟶ Y₂) (X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂' C).obj X₁).map φ).app X₃ =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₃ φ)
-- Mathlib.Combinatorics.Additive.Dissociation
/-- The span of a finset `s` is the finset of elements of the form `∏ a ∈ s, a ^ ε a` where
`ε ∈ {-1, 0, 1} ^ s`.

This is an analog of the linear span in a vector space, but with the "scalars" restricted to
`0` and `±1`.  -/
Finset.mulSpan : {α : Type u_1} → [CommGroup α] → [DecidableEq α] → [Fintype α] → Finset α → Finset α
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The equivalence between `AddMonCat` and `MonCat`.  -/
AddMonCat.equivalence : AddMonCat ≌ MonCat
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.response.injEq : ∀ (id id_1 : Lean.JsonRpc.RequestID),
  (Lean.JsonRpc.MessageMetaData.response id = Lean.JsonRpc.MessageMetaData.response id_1) = (id = id_1)
-- Mathlib.Analysis.Normed.Group.Pointwise
sphere_div_singleton : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E), Metric.sphere x δ / {y} = Metric.sphere (x / y) δ
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.rewrite : {α : Type u_1} →
  {β : Type u_2} →
    (α → Lean.Widget.TaggedText α → Lean.Widget.TaggedText β) → Lean.Widget.TaggedText α → Lean.Widget.TaggedText β
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.coe_eval₂Hom : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {φ : R →+* S} {a : σ → S} [inst_4 : IsTopologicalSemiring R] [inst_5 : IsUniformAddGroup R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : CompleteSpace S] [inst_8 : T2Space S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : MvPowerSeries.HasEval a),
  ⇑(MvPowerSeries.eval₂Hom hφ ha) = MvPowerSeries.eval₂ φ a
-- Mathlib.MeasureTheory.Function.UnifTight
MeasureTheory.UnifTight.aeeq : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f g : ι → α → β} {p : ENNReal},
  MeasureTheory.UnifTight f p μ → (∀ (n : ι), f n =ᵐ[μ] g n) → MeasureTheory.UnifTight g p μ
-- Mathlib.Algebra.Azumaya.Matrix
/-- `AlgHom.mulLeftRight` for matrix algebra sends basis Eᵢⱼ⊗Eₖₗ to
the map `f : Eₛₜ ↦ Eᵢⱼ * Eₛₜ * Eₖₗ = δⱼₛδₜₖEᵢₗ`, therefore we construct the inverse
by sending `f` to `∑ᵢₗₛₜ f(Eₛₜ)ᵢₗ • Eᵢₛ⊗Eₜₗ`.  -/
AlgHom.mulLeftRightMatrix_inv : (R : Type u_1) →
  (n : Type u_2) →
    [inst : CommSemiring R] →
      [Fintype n] → [DecidableEq n] → Module.End R (Matrix n n R) →ₗ[R] TensorProduct R (Matrix n n R) (Matrix n n R)ᵐᵒᵖ
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_const : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : MeasureTheory.Measure Ω)
  [hσ : MeasureTheory.SigmaFinite (P.trim hm)] (c : ENNReal), P⁻[fun x => c | mΩ] = fun x => c
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
/-- An isometry between two bilinear spaces `M₁, B₁` and `M₂, B₂` over a ring `R`,
is a linear map between `M₁` and `M₂` that commutes with the bilinear forms.  -/
LinearMap.BilinForm.Isometry.«term_→bᵢ_» : Lean.TrailingParserDescr
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.propagateDiseqOf : ℕ → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec.map_app : ∀ {R S : CommRingCat} (f : R ⟶ S) (U : (AlgebraicGeometry.Spec R).Opens),
  AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Spec.map f) U =
    CommRingCat.ofHom
      (AlgebraicGeometry.StructureSheaf.comap (CommRingCat.Hom.hom f) U
        ((TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.map f).base).obj U) ⋯)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.π_comp_leftHomologyIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [inst_2 : S.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp h.π h.leftHomologyIso.inv =
    CategoryTheory.CategoryStruct.comp h.cyclesIso.inv S.leftHomologyπ
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_eq_single_zero_iff : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M] {y : M} {s : Fin n →₀ M} {x : M},
  (Finsupp.cons x s = fun₀ | 0 => y) ↔ s = 0 ∧ x = y
-- Mathlib.LinearAlgebra.Matrix.Permanent
/-- Permuting the columns does not change the permanent.  -/
Matrix.permanent_permute_cols : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R] (σ : Equiv.Perm n)
  (M : Matrix n n R), (M.submatrix (⇑σ) id).permanent = M.permanent
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.nu_inv_eq_sum_divisors_inv_selbergTerms : ∀ {s : BoundingSieve} {d : ℕ},
  d ∣ s.prodPrimes → (s.nu d)⁻¹ = ∑ l ∈ s.prodPrimes.divisors, if l ∣ d then (BoundingSieve.selbergTerms l)⁻¹ else 0
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_floor : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  Int.fract ↑⌊a⌋ = 0
-- Lean.Elab.Do.Basic
Lean.Elab.Do.MutVar.mk.sizeOf_spec : ∀ (ident : Lean.Ident) (baseId : Lean.FVarId),
  sizeOf { ident := ident, baseId := baseId } = 1 + sizeOf ident + sizeOf baseId
-- Mathlib.Logic.Equiv.PartialEquiv
/-- A very basic tactic to show that sets showing up in manifolds coincide or are included
in one another.  -/
Mathlib.Tactic.MfldSetTac.mfldSetTac : Lean.ParserDescr
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.symmetrify_reverse : ∀ {V : Type u_2} [inst : Quiver V] {a b : Quiver.Symmetrify V} (e : a ⟶ b), Quiver.reverse e = Sum.swap e
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- Given `h : LeftHomologyData S`, this is morphism `S.X₁ ⟶ h.K` induced
by `S.f : S.X₁ ⟶ S.X₂` and the fact that `h.K` is a kernel of `S.g : S.X₂ ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.f' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → (h : S.LeftHomologyData) → S.X₁ ⟶ h.K
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.ofList_eq_insertMany_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α}, Std.TreeSet.ofList l cmp = ∅.insertMany l
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The morphism between homotopy cofibers that is induced by a
morphism of arrows.  -/
HomologicalComplex.homotopyCofiber.mapArrowHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) →
              [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
                [inst_3 : DecidableRel c.Rel] →
                  {F' G' : HomologicalComplex C c} →
                    (φ' : F' ⟶ G') →
                      [inst_4 : HomologicalComplex.HasHomotopyCofiber φ'] →
                        (∀ (j : ι), ∃ i, c.Rel i j) →
                          (CategoryTheory.Arrow.mk φ ⟶ CategoryTheory.Arrow.mk φ') →
                            (HomologicalComplex.homotopyCofiber φ ⟶ HomologicalComplex.homotopyCofiber φ')
-- Mathlib.Algebra.Quaternion
/-- The equivalence between a quaternion algebra over `R` and `Fin 4 → R`.  -/
QuaternionAlgebra.equivTuple : {R : Type u_1} → (c₁ c₂ c₃ : R) → QuaternionAlgebra R c₁ c₂ c₃ ≃ (Fin 4 → R)
-- Mathlib.GroupTheory.Coxeter.Matrix
CoxeterMatrix.reindex_apply : ∀ {B : Type u_1} {B' : Type u_2} (e : B ≃ B') (M : CoxeterMatrix B) (i i' : B'),
  (CoxeterMatrix.reindex e M).M i i' = M.M (e.symm i) (e.symm i')
-- Init.Data.List.Count
List.one_le_count_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, 1 ≤ List.count a l ↔ a ∈ l