mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMap_multiset_sum : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (B : Multiset (LinearMap.BilinMap R M N)),
  B.sum.toQuadraticMap = (Multiset.map LinearMap.BilinMap.toQuadraticMap B).sum
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.isComplex₂_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ComposableArrows C 2),
  S.IsComplex ↔
    CategoryTheory.CategoryStruct.comp
        (S.map' 0 1 CategoryTheory.ComposableArrows.isComplex₂_iff._proof_2
          CategoryTheory.ComposableArrows.isComplex₂_iff._proof_4)
        (S.map' 1 2 CategoryTheory.ComposableArrows.isComplex₂_iff._proof_4
          CategoryTheory.ComposableArrows.isComplex₂_iff._proof_5) =
      0
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- `x ^ s = o(exp x)` as `x → ∞` for any real `s`.  -/
isLittleO_rpow_exp_atTop : ∀ (s : ℝ), (fun x => x ^ s) =o[Filter.atTop] Real.exp
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.neg_neg_iff : ∀ {R : Type u} [inst : CommRing R] (x y : R), IsCoprime (-x) (-y) ↔ IsCoprime x y
-- Init.Data.SInt.Lemmas
Int64.ofInt_int8ToInt : ∀ (x : Int8), Int64.ofInt x.toInt = x.toInt64
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- **Alias** of `CategoryTheory.MorphismProperty.pullbackLift_fst_snd`. -/
CategoryTheory.MorphismProperty.baseChange_map' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange] {S S' X Y : C} (f : S' ⟶ S) {v₁₂ : X ⟶ S} {v₂₂ : Y ⟶ S} {g : X ⟶ Y}
  (hv₁₂ : v₁₂ = CategoryTheory.CategoryStruct.comp g v₂₂) [inst_2 : CategoryTheory.Limits.HasPullback v₁₂ f]
  [inst_3 : CategoryTheory.Limits.HasPullback v₂₂ f],
  P g →
    P
      (CategoryTheory.Limits.pullback.lift
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst v₁₂ f) g)
        (CategoryTheory.Limits.pullback.snd v₁₂ f) ⋯)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.mk.injEq : ∀ (carrier : Type u) [str : AddCommGroup carrier] (carrier_1 : Type u) (str_1 : AddCommGroup carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_coe_sub : ∀ {r : NNReal} {b : ENNReal}, Filter.Tendsto (fun b => ↑r - b) (nhds b) (nhds (↑r - b))
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.measure_fundamentalDomain_ne_zero : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E)
  [Finite ι] [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure],
  μ (ZSpan.fundamentalDomain b) ≠ 0
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.transIsBigOIsEquivalent : {α : Type u_1} →
  {β : Type u_2} →
    {β₂ : Type u_3} →
      [inst : NormedAddCommGroup β] →
        [inst_1 : Norm β₂] →
          {l : Filter α} → Trans (Asymptotics.IsBigO l) (Asymptotics.IsEquivalent l) (Asymptotics.IsBigO l)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- The minimum of the valuations of `q` and `r` is at most the valuation of `q + r`.  -/
padicValRat.min_le_padicValRat_add : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
  q + r ≠ 0 → min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.ofCoprodI.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Monoid (G i)] [inst_1 : Monoid H]
  {φ : (i : ι) → H →* G i}, Monoid.PushoutI.ofCoprodI = Monoid.CoprodI.lift Monoid.PushoutI.of
-- Mathlib.Tactic.Translate.Core
/-- Add a translation to the translations map. If the translation attribute is dual,
also add the reverse translation.  -/
Mathlib.Tactic.Translate.insertTranslation : Mathlib.Tactic.Translate.TranslateData →
  Lean.Name →
    Lean.Name → Mathlib.Tactic.Translate.Reorder → Mathlib.Tactic.Translate.RelevantArg → Lean.Syntax → Lean.CoreM Unit
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.orderTop_sub : ∀ {R : Type u_3} [inst : AddGroup R] {Γ : Type u_8} [inst_1 : LinearOrder Γ] {x y : HahnSeries Γ R},
  x.orderTop < y.orderTop → (x - y).orderTop = x.orderTop
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- The composition of a presentation `P` with a
localization away from an element has the form `R[Xᵢ, Y]/(fⱼ, (P.σ g) Y - 1)`,
if the chosen section of `P` preserves `-1` and `0`.
Note: If `S` is non-trivial, we can ensure this by only modifying `P.σ`.  -/
Algebra.Presentation.relation_comp_localizationAway_inl : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [inst_6 : IsScalarTower R S T]
  (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Presentation R S ι σ),
  P.σ (-1) = -1 →
    P.σ 0 = 0 →
      ∀ (r : Unit),
        ((Algebra.Presentation.localizationAway T g).comp P).relation (Sum.inl r) =
          (MvPolynomial.rename Sum.inr) (P.σ g) * MvPolynomial.X (Sum.inl ()) - 1
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformly.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β]
  {F : ι → α → β} {f : α → β} {p : Filter ι} [inst_2 : TopologicalSpace γ],
  TendstoLocallyUniformly F f p → ∀ (g : γ → α), Continuous g → TendstoLocallyUniformly (fun n => F n ∘ g) (f ∘ g) p
-- Lean.Parser.Command
Lean.Parser.Command.structExplicitBinder.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Set.Sigma
Set.sigma_empty : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι}, (s.sigma fun i => ∅) = ∅
-- Mathlib.Topology.Order.LawsonTopology
/-- If `α` is equipped with the Lawson topology, then it is homeomorphic to `WithLawson α`.
 -/
Topology.WithLawson.homeomorph : {α : Type u_1} →
  [inst : Preorder α] → [inst_1 : TopologicalSpace α] → [Topology.IsLawson α] → Topology.WithLawson α ≃ₜ α
-- Mathlib.Data.Sum.Basic
Sum.rec_update_left : ∀ {α : Type u} {β : Type v} {γ : α ⊕ β → Sort u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β]
  (f : (a : α) → γ (Sum.inl a)) (g : (b : β) → γ (Sum.inr b)) (a : α) (x : γ (Sum.inl a)),
  (fun t => Sum.rec (Function.update f a x) g t) = Function.update (fun t => Sum.rec f g t) (Sum.inl a) x
-- Mathlib.Data.NNReal.Defs
NNReal.coe_max : ∀ (x y : NNReal), ↑(max x y) = max ↑x ↑y
-- Mathlib.Topology.Connected.LocallyConnected
TopologicalSpace.IsTopologicalBasis.isOpen_isPreconnected : ∀ {α : Type u} [inst : TopologicalSpace α] [LocallyConnectedSpace α],
  TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ IsPreconnected s}
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
  ⨍⁻ (x : α), f x ∂μ = (∫⁻ (x : α), f x ∂μ) / μ Set.univ
-- Batteries.Recycling.RBTree.Alter
/-- Auxiliary definition for `alter`.  -/
RBTree.RBMap.alter.adapt : {α : Type u_1} → {β : Type u_2} → α → (Option β → Option β) → Option (α × β) → Option (α × β)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T U : CategoryTheory.Over X} (f : R ⟶ S) (g : T ⟶ U),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
      (CategoryTheory.ChosenPullbacksAlong.snd S.hom U.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom T.hom)
      (CategoryTheory.Over.Hom.left g)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The distinguished long root of an embedded `𝔤₂` root pairing.  -/
RootPairing.EmbeddedG2.long : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        {inst : CommRing R} →
          {inst_1 : AddCommGroup M} →
            {inst_2 : Module R M} →
              {inst_3 : AddCommGroup N} → {inst_4 : Module R N} → (P : RootPairing ι R M N) → [self : P.EmbeddedG2] → ι
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.mk_map : ∀ {V : Type u_1} {W : Type u_2} [inst : Quiver V] [inst_1 : Quiver W] {obj : V → W}
  {map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)} {X Y : V} {f : X ⟶ Y}, { obj := obj, map := map }.map f = map f
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.instReflectsIsomorphismsElementsπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)),
  (CategoryTheory.CategoryOfElements.π F).ReflectsIsomorphisms
-- Mathlib.Order.CompleteLattice.Defs
CompleteSemilatticeInf.mk : {α : Type u_8} →
  [toPartialOrder : PartialOrder α] →
    [toInfSet : InfSet α] → (∀ (s : Set α), IsGLB s (sInf s)) → CompleteSemilatticeInf α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.inv_hom_id_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone F} (f : c ≅ d) {Z : C} (h : d.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.inv.hom (CategoryTheory.CategoryStruct.comp f.hom.hom h) = h
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.over_def : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X), AlgebraicGeometry.Spec (X.presheaf.stalk x) ↘ X = X.fromSpecStalk x
-- Aesop.Tree.Data
Aesop.GoalOrigin.copied.sizeOf_spec : ∀ («from» rep : Aesop.GoalId), sizeOf (Aesop.GoalOrigin.copied «from» rep) = 1 + sizeOf «from» + sizeOf rep
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.forIn_eq_forIn_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.Raw.forIn (fun a x d => f a d) init ↑m = forIn (↑m).keys init f
-- Mathlib.Data.Finset.Basic
Finset.erase_eq_iff_eq_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s → a ∉ t → (s.erase a = t ↔ s = insert a t)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.braiding_naturality_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  {F G : CategoryTheory.Functor C V} (η : F ⟶ G) (H : CategoryTheory.Functor C V)
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F H]
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution H F]
  [inst_8 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_9 : CategoryTheory.MonoidalCategory.DayConvolution H G] {Z : CategoryTheory.Functor C V}
  (h : CategoryTheory.MonoidalCategory.DayConvolution.convolution H G ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map η (CategoryTheory.CategoryStruct.id H))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding G H).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding F H).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id H) η) h)
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.coe_toMulHom : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {f : M ≃* N}, ⇑f.toMulHom = ⇑f
-- Mathlib.NumberTheory.FermatPsp
/-- If `n` passes the Fermat primality test to base `b`, then `n` is coprime with `b`, assuming that
`n` and `b` are both positive.
 -/
Nat.coprime_of_probablePrime : ∀ {n b : ℕ}, n.ProbablePrime b → 1 ≤ n → 1 ≤ b → n.Coprime b
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Walk.length_boxProd : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {a₁ a₂ : α} {b₁ b₂ : β} [inst : DecidableEq α]
  [inst_1 : DecidableEq β] [inst_2 : DecidableRel G.Adj] [inst_3 : DecidableRel H.Adj]
  (w : (G □ H).Walk (a₁, b₁) (a₂, b₂)), w.length = w.ofBoxProdLeft.length + w.ofBoxProdRight.length
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_add_iff_right : ∀ {a b c : ℕ}, a ∣ b → (a.Coprime (b + c) ↔ a.Coprime c)
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.instIsAddCommutative_closure : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_3} [inst_1 : SetLike S G] [inst_2 : AddMemClass S G] (s : S)
  [IsAddCommutative ↥s], IsAddCommutative ↥(AddSubgroup.closure ↑s)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.continuous_integral : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}, Continuous fun f => ∫ (a : α), ↑↑f a ∂μ
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.Hom.ext_iff : ∀ {A B : AddGrpCat} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.RingTheory.Ideal.Nonunits
Submonoid.isUnit_iff_of_ne_zero : ∀ {α : Type u_2} {C : Type u_4} [inst : SetLike C α] [inst_1 : GroupWithZero α] [inst_2 : SubmonoidClass C α] {S : C}
  {a : ↥S}, ↑a ≠ 0 → (IsUnit a ↔ (↑a)⁻¹ ∈ S)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
/-- Given an isomorphism `Y ≅ X` of simplicial sets, a pairing `P` of a subcomplex
`A` of `X`, this is a pairing for a subcomplex `B` of `Y` if `A.preimage e.hom = B`.  -/
SSet.Subcomplex.Pairing.ofIso : {X : SSet} →
  {A : X.Subcomplex} → A.Pairing → {Y : SSet} → {B : Y.Subcomplex} → (e : Y ≅ X) → A.preimage e.hom = B → B.Pairing
-- Mathlib.Algebra.Star.Basic
/-- A star module `A` over a star ring `R` is a module which is a star additive monoid,
and the two star structures are compatible in the sense
`star (r • a) = star r • star a`.

Note that it is up to the user of this typeclass to enforce
`[Semiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A]`, and that
the statement only requires `[Star R] [Star A] [SMul R A]`.

If used as `[CommRing R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A]`, this represents a
star algebra.
 -/
StarModule : (R : Type u) → (A : Type v) → [Star R] → [Star A] → [SMul R A] → Prop
-- Mathlib.Order.Hom.Lattice
/-- `id` as a `SupHom`.  -/
SupHom.id : (α : Type u_2) → [inst : Max α] → SupHom α α
-- Std.Tactic.Do.Syntax
Lean.Parser.Category.mintroPat : Lean.Parser.Category
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.char_apply : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} {he : Continuous ⇑e} {hL : Continuous fun p => (L p.1) p.2} (w : W) (v : V),
  (BoundedContinuousFunction.char he hL w) v = ↑(e ((L v) w))
-- Mathlib.Algebra.Ring.Defs
/-- Zero is a right absorbing element for multiplication  -/
Semiring.mul_zero : ∀ {α : Type u} [self : Semiring α] (a : α), a * 0 = 0
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.eq_append_of_dropSuffix?_string_eq_some : ∀ {pat : String} {s res : String.Slice}, s.dropSuffix? pat = some res → s.copy = res.copy ++ pat
-- Mathlib.GroupTheory.Congruence.Defs
/-- The function on the quotient by a congruence relation `c` induced by a function that is
constant on `c`'s equivalence classes.  -/
Con.liftOn : {M : Type u_1} →
  [inst : Mul M] → {β : Sort u_4} → {c : Con M} → c.Quotient → (f : M → β) → (∀ (a b : M), c a b → f a = f b) → β
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.foldr_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → δ → δ} {init : δ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.foldr f init t₁ = Std.DTreeMap.Raw.foldr f init t₂
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Radon-Nikodym derivative of a sum of two measures.
See also `rnDeriv_add`, which has no hypothesis on `μ` but requires finite `ν₁` and `ν₂`.  -/
MeasureTheory.Measure.rnDeriv_add' : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν₁ ν₂ μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite ν₁]
  [MeasureTheory.SigmaFinite ν₂] [MeasureTheory.SigmaFinite μ], (ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ
-- Mathlib.Data.Finset.Max
Finset.min_pair : ∀ {α : Type u_2} [inst : LinearOrder α] (a b : α), {a, b}.min = min ↑a ↑b
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
RightDerivMeasurableAux.le_of_mem_A : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {r ε : ℝ} {L : F} {x : ℝ},
  x ∈ RightDerivMeasurableAux.A f L r ε →
    ∀ {y z : ℝ}, y ∈ Set.Icc x (x + r / 2) → z ∈ Set.Icc x (x + r / 2) → ‖f z - f y - (z - y) • L‖ ≤ ε * r
-- Mathlib.RingTheory.Nilpotent.Basic
instIsReducedProd : ∀ {R : Type u_1} {S : Type u_2} [inst : Zero R] [inst_1 : Pow R ℕ] [inst_2 : Zero S] [inst_3 : Pow S ℕ] [IsReduced R]
  [IsReduced S], IsReduced (R × S)
-- Init.Data.Nat.Lemmas
Nat.div_div_self : ∀ {n m : ℕ}, n ∣ m → m ≠ 0 → m / (m / n) = n
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.neg.sizeOf_spec : ∀ (a : Lean.Grind.CommRing.Expr), sizeOf a.neg = 1 + sizeOf a
-- Init.Grind.ToIntLemmas
Lean.Grind.IntInterval.hi?.eq_2 : ∀ (lo : ℤ), (Lean.Grind.IntInterval.ci lo).hi? = none
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.brecOn.eq : ∀ {motive_1 : Aesop.Script.StepTree → Sort u} {motive_2 : Array Aesop.Script.StepTree → Sort u}
  {motive_3 : List Aesop.Script.StepTree → Sort u} (t : Aesop.Script.StepTree)
  (F_1 : (t : Aesop.Script.StepTree) → t.below → motive_1 t)
  (F_2 : (t : Array Aesop.Script.StepTree) → Aesop.Script.StepTree.below_1 t → motive_2 t)
  (F_3 : (t : List Aesop.Script.StepTree) → Aesop.Script.StepTree.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Aesop.Script.StepTree.brecOn.go t F_1 F_2 F_3).2
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.annotateNamedArg : Lean.Name → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instCovariantClassHSMulLeOfENNReal : ∀ {α : Type u_1} {R : Type u_6} {m0 : MeasurableSpace α} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal] [CovariantClass R ENNReal (fun x1 x2 => x1 • x2) fun x1 x2 => x1 ≤ x2],
  CovariantClass R (MeasureTheory.Measure α) (fun x1 x2 => x1 • x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.hom_ext_iff : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] {W : C} {k l : CategoryTheory.Limits.coequalizer f g ⟶ W},
  k = l ↔
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) k =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) l
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
/-- A lift of the projective seminorm to `FreeAddMonoid (𝕜 × Π i, Eᵢ)`, useful to prove the
properties of `projectiveSeminorm`.  -/
PiTensorProduct.projectiveSeminormAux : {ι : Type u_1} →
  [Fintype ι] →
    {𝕜 : Type u_2} →
      {E : ι → Type u_3} →
        [(i : ι) → SeminormedAddCommGroup (E i)] → [NormedField 𝕜] → FreeAddMonoid (𝕜 × ((i : ι) → E i)) → ℝ
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- Variant of `Under.equalizerFork'` for algebra maps. This is definitionally equal to
`Under.equalizerFork` but this is costly in applications.  -/
CommRingCat.Under.equalizerFork' : {R : CommRingCat} →
  {A B : Type u} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra (↑R) A] →
          [inst_3 : Algebra (↑R) B] → (f g : A →ₐ[↑R] B) → CategoryTheory.Limits.Fork f.toUnder g.toUnder
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_eq_zero_iff_range_orderOf_infinite : ∀ {G : Type u} [inst : Monoid G], (∀ (g : G), 0 < orderOf g) → (Monoid.exponent G = 0 ↔ (Set.range orderOf).Infinite)
-- Mathlib.RingTheory.Polynomial.Radical
natDegree_radical_le : ∀ {k : Type u_1} [inst : Field k] [inst_1 : DecidableEq k] {a : Polynomial k},
  (UniqueFactorizationMonoid.radical a).natDegree ≤ a.natDegree
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The adjunction between the category `CofibrantObject.HoCat C` and `BifibrantObject.HoCat C`.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.adj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution ⊣
        HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_image_prod : ∀ {α : Type u_2} [inst : Sub α] {s t : Set α}, (fun x => x.1 - x.2) '' s ×ˢ t = s - t
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_swap : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous Prod.swap
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- See note [partially-applied ext lemmas].  -/
SkewMonoidAlgebra.distribMulActionHom_ext' : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : DistribMulAction R M] [inst_4 : DistribMulAction R N] {α : Type u_6} {f g : SkewMonoidAlgebra M α →+[R] N},
  (∀ (a : α),
      f.comp (SkewMonoidAlgebra.DistribMulActionHom.single a) =
        g.comp (SkewMonoidAlgebra.DistribMulActionHom.single a)) →
    f = g
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) ⦃A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F⦄ (f : A ⟶ B),
  Function.Surjective
    ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.PreGaloisCategory.autGaloisSystem F).map f))
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.instInnerRegularOfIsAddHaarMeasureOfCompactSpace : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] [CompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ], μ.InnerRegular
-- Mathlib.Algebra.Module.LinearMap.End
/-- Scalar multiplication on the left, as a linear map.  -/
Module.End.smulLeft : {R : Type u_1} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (α : R) → α ∈ Set.center R → Module.End R M
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_congr : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] {s₁ s₂ : Finset α} {f g : α → β} (h₁ : s₁ = s₂)
  (h₂ : ∀ x ∈ s₂, f x = g x) (comm : (↑s₁).Pairwise (Function.onFun AddCommute f)),
  s₁.noncommSum f comm = s₂.noncommSum g ⋯
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_sort : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  (s : Lean.Grind.AC.Seq), Lean.Grind.AC.Seq.denote ctx s.sort = Lean.Grind.AC.Seq.denote ctx s
-- Mathlib.Algebra.Group.Pi.Lemmas
Set.range_one : ∀ {α : Type u_5} {β : Type u_6} [inst : One β] [Nonempty α], Set.range 1 = {1}
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix.eq_1 : ∀ (R : Type u_1) {α : Type u_2} (G : SimpleGraph α) [inst : Zero R] [inst_1 : One R] [inst_2 : DecidableEq α]
  [inst_3 : DecidableRel G.Adj], SimpleGraph.incMatrix R G = Matrix.of fun a e => if e ∈ G.incidenceSet a then 1 else 0