mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_singleton : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {k : α} {v : β},
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity [(k, v)]) =
    Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insert k v
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.ofAlgEquiv_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] (f : A ≃ₐ[R] B)
  (counit_comp : (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A)
  (map_comp_comul :
    (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f)
  (a : A), (BialgEquiv.ofAlgEquiv f counit_comp map_comp_comul) a = f.toFun a
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.hausdorffMeasure_smul₀ : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedDivisionRing 𝕜] [inst_2 : Module 𝕜 E]
  [NormSMulClass 𝕜 E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] {d : ℝ},
  0 ≤ d →
    ∀ {r : 𝕜},
      r ≠ 0 →
        ∀ (s : Set E),
          (MeasureTheory.Measure.hausdorffMeasure d) (r • s) = ‖r‖₊ ^ d • (MeasureTheory.Measure.hausdorffMeasure d) s
-- Lean.Elab.BuiltinNotation
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.mkPPairs.loop : Array Lean.Term → ℕ → Lean.Term → Lean.MacroM Lean.Term
-- Lean.Parser.Term
Lean.Parser.Term.attrInstance : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorAlgebra.toDirectSum_ofDirectSum : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (x : DirectSum ℕ fun n => TensorPower R n M), TensorAlgebra.toDirectSum (TensorAlgebra.ofDirectSum x) = x
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- **Alias** of `fun_iteratedFDerivWithin_add_apply`.

---

Eta-expanded form of `iteratedFDerivWithin_add_apply`

---

The iterated derivative of the sum of two functions is the sum of the iterated derivatives.
 -/
iteratedFDerivWithin_add_apply' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {x : E} {i : ℕ} {f g : E → F},
  ContDiffWithinAt 𝕜 (↑i) f s x →
    ContDiffWithinAt 𝕜 (↑i) g s x →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          iteratedFDerivWithin 𝕜 i (fun i => f i + g i) s x =
            iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x
-- Init.Data.Nat.Basic
Nat.beq_refl : ∀ (a : ℕ), a.beq a = true
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
/-- If `F : C ⥤ D` is dense at `Y : D`, and `G` is a functor that is isomorphic to `F`,
then `G` is also dense at `Y`.  -/
CategoryTheory.Functor.DenseAt.ofNatIso : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {Y : D} → F.DenseAt Y → {G : CategoryTheory.Functor C D} → (F ≅ G) → G.DenseAt Y
-- Aesop.Rule.Forward
Aesop.ForwardRulePriority.normSafe.injEq : ∀ (n n_1 : ℤ), (Aesop.ForwardRulePriority.normSafe n = Aesop.ForwardRulePriority.normSafe n_1) = (n = n_1)
-- Mathlib.Algebra.Divisibility.Basic
dvd_refl : ∀ {α : Type u_1} [inst : Monoid α] (a : α), a ∣ a
-- Init.Data.List.Nat.Sum
List.min_le_sum_div_length_nat : ∀ {xs : List ℕ} (h : xs ≠ []), xs.min h ≤ xs.sum / xs.length
-- Aesop.Tree.Traversal
Aesop.TreeRef.mvarCluster.sizeOf_spec : ∀ (cref : Aesop.MVarClusterRef), sizeOf (Aesop.TreeRef.mvarCluster cref) = 1 + sizeOf cref
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  {Y Z : C} (f : Y ⟶ Z) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X Z) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.fderiv_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E}, f₁ =ᶠ[nhds x] f → fderiv 𝕜 f₁ x = fderiv 𝕜 f x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
CategoryTheory.CommGrpObj.toIsCommMonObj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {X : C} [self : CategoryTheory.CommGrpObj X],
  CategoryTheory.IsCommMonObj X
-- Mathlib.NumberTheory.Dioph
/-- The set of places where one Diophantine function divides another is Diophantine.  -/
Dioph.«term_D∣_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry_uncurry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y : C}
  [inst_2 : CategoryTheory.Closed A] (f : X ⟶ A ⟹ Y),
  CategoryTheory.MonoidalClosed.curry (CategoryTheory.MonoidalClosed.uncurry f) = f
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- `Under.pushout f` preserves finite limits if `f` is flat.  -/
CommRingCat.Under.preservesFiniteLimits_of_flat : ∀ {R S : CommRingCat} (f : R ⟶ S),
  (CommRingCat.Hom.hom f).Flat → CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Under.pushout f)
-- Mathlib.Topology.Order.Bornology
IsOrderBornology.cobounded_eq_atBot : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : LinearOrder α] [IsOrderBornology α] [NoMinOrder α] [OrderTop α],
  Bornology.cobounded α = Filter.atBot
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.ext : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α}, (∀ (i j : n), star (A j i) = A i j) → A.IsHermitian
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true ↔ ∀ (a : α), a ∉ t
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.eq_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y) {x : X}
  {y : Y}, x = e.symm y ↔ e x = y
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.mk.inj : ∀ {R : Type u_1} {a b c re imI imJ imK re_1 imI_1 imJ_1 imK_1 : R},
  { re := re, imI := imI, imJ := imJ, imK := imK } = { re := re_1, imI := imI_1, imJ := imJ_1, imK := imK_1 } →
    re = re_1 ∧ imI = imI_1 ∧ imJ = imJ_1 ∧ imK = imK_1
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- The entrywise sup norm of a unitary matrix is at most 1.  -/
entrywise_sup_norm_bound_of_unitary : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {U : Matrix n n 𝕜},
  U ∈ Matrix.unitaryGroup n 𝕜 → ‖U‖ ≤ 1
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- Reflection is its own inverse.  -/
Submodule.reflection_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection], K.reflection.symm = K.reflection
-- Mathlib.Data.Finset.Density
Finset.dens_mono : ∀ {α : Type u_2} [inst : Fintype α], Monotone Finset.dens
-- Mathlib.Algebra.Order.Monoid.Submonoid
Submonoid.coe_oneLE : ∀ (M : Type u_1) [inst : Monoid M] [inst_1 : Preorder M] [inst_2 : MulLeftMono M], ↑(Submonoid.oneLE M) = Set.Ici 1
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {fallback : β}, k ∉ m₂ → (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.exists_mem_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) (x : X), ∃ n, K n ∈ nhds x
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- If `f` is a continuous monotone map `ℝ → ℝ`, `f (x + 1) = f x + 1`, then there exists `x`
such that `f x = x + τ f`.  -/
CircleDeg1Lift.exists_eq_add_translationNumber : ∀ (f : CircleDeg1Lift), Continuous ⇑f → ∃ x, f x = x + f.translationNumber
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.iff_flat_and_rTensor_faithful : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.FaithfullyFlat R M ↔
    Module.Flat R M ∧
      ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N],
        Nontrivial N → Nontrivial (TensorProduct R N M)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.cone_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g), h.cone.fst = fst
-- Mathlib.Algebra.Group.Hom.Defs
/-- The proposition that the function preserves multiplication  -/
MulHomClass.map_mul : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {inst : Mul M} {inst_1 : Mul N}
  {inst_2 : FunLike F M N} [self : MulHomClass F M N] (f : F) (x y : M), f (x * y) = f x * f y
-- Mathlib.Analysis.Normed.Lp.lpSpace
LipschitzWith.coordinate : ∀ {α : Type u_3} {ι : Type u_5} [inst : PseudoMetricSpace α] {f : α → ↥(lp (fun x => ℝ) ⊤)} (K : NNReal),
  LipschitzWith K f ↔ ∀ (i : ι), LipschitzWith K fun a => ↑(f a) i
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.ext : ∀ {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] {Q Q' : QuadraticMap R M N}, (∀ (x : M), Q x = Q' x) → Q = Q'
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- The "matrix" morphism `X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂` with specified components.
 -/
CategoryTheory.Biprod.ofComponents : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {X₁ X₂ Y₁ Y₂ : C} → (X₁ ⟶ Y₁) → (X₁ ⟶ Y₂) → (X₂ ⟶ Y₁) → (X₂ ⟶ Y₂) → (X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂)
-- Mathlib.Data.Finset.Powerset
/-- For `1 ≤ r ≤ q`, the map `powersetCard r` is injective on the finsets of cardinality `q`.  -/
Finset.powersetCard_injOn : ∀ {α : Type u_1} {q r : ℕ}, r ≠ 0 → r ≤ q → Set.InjOn (fun a => Finset.powersetCard r a) {a | a.card = q}
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_mul_div_cancel₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, b ≠ 0 → a / b * (b / c) = a / c
-- Mathlib.Algebra.Order.UpperLower
LowerSet.coe_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α] (s t : LowerSet α),
  ↑(s + t) = ↑s + ↑t
-- Aesop.Util.Basic
Aesop.updateSimpEntryPriority : ℕ → Lean.Meta.SimpEntry → Lean.Meta.SimpEntry
-- Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
isCompactOperator_id_iff_finiteDimensional : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyCompactSpace 𝕜], IsCompactOperator id ↔ FiniteDimensional 𝕜 E
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.epi_snd_of_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Epi f]
  {s : CategoryTheory.Limits.PullbackCone f g} (hs : CategoryTheory.Limits.IsLimit s), CategoryTheory.Epi s.snd
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.simplicialEvalσ_monotone : ∀ (L : List ℕ), Monotone (SimplexCategoryGenRel.simplicialEvalσ L)
-- Mathlib.CategoryTheory.Category.Basic
/-- `f : X ⟶ Y` is a monomorphism iff for all `Z`, composition of morphisms `Z ⟶ X` with `f`
is injective.  -/
CategoryTheory.mono_iff_forall_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : Y ⟶ X),
  CategoryTheory.Mono f ↔ ∀ (Z : C), Function.Injective fun g => CategoryTheory.CategoryStruct.comp g f
-- Mathlib.Order.SuccPred.CompleteLinearOrder
/-- See `csSup_mem_of_not_isSuccLimit` for the `ConditionallyCompleteLinearOrder` version.  -/
csSup_mem_of_not_isSuccPrelimit : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α}, ¬Order.IsSuccPrelimit (sSup s) → sSup s ∈ s
-- Mathlib.Order.UpperLower.Closure
UpperSet.sdiff.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (s : UpperSet α) (t : Set α),
  s.sdiff t = { carrier := ↑s \ ↑(lowerClosure t), upper' := ⋯ }
-- Init.Data.SInt.Bitwise
ISize.zero_and : ∀ {a : ISize}, 0 &&& a = 0
-- Mathlib.CategoryTheory.NatTrans
/-- `vcomp α β` is the vertical compositions of natural transformations.  -/
CategoryTheory.NatTrans.vcomp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G H : CategoryTheory.Functor C D} →
          CategoryTheory.NatTrans F G → CategoryTheory.NatTrans G H → CategoryTheory.NatTrans F H
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabelPart.mk : String → Option String → Option Lean.Elab.InlayHintLinkLocation → Lean.Elab.InlayHintLabelPart
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app_assoc : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H) (β : F ⟶ L.comp G) (X : C)
  {Z : H} (h : G.obj (L.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.app X)
      (CategoryTheory.CategoryStruct.comp ((F'.descOfIsLeftKanExtension α G β).app (L.obj X)) h) =
    CategoryTheory.CategoryStruct.comp (β.app X) h
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- If `f : X → Z` is a Borel measurable map from a standard Borel space to a
countably separated measurable space and the range of `f` is measurable,
then the preimage of a set `s` is measurable
if and only if the intersection with `Set.range f` is measurable.  -/
Measurable.measurableSet_preimage_iff_inter_range : ∀ {X : Type u_3} {Z : Type u_5} [inst : MeasurableSpace X] [StandardBorelSpace X] [inst_2 : MeasurableSpace Z]
  {f : X → Z} [MeasurableSpace.CountablySeparated ↑(Set.range f)],
  Measurable f → MeasurableSet (Set.range f) → ∀ {s : Set Z}, MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ Set.range f)
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
/-- A continuous even function has bounded range if and only if `f =O[atTop] 1`.  -/
Continuous.isBounded_range_iff_isBigO_atTop_of_even : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : LinearOrder β]
  [OrderClosedTopology β] [CompactIccSpace β] [NoMaxOrder β] [NoMinOrder β] [inst_7 : AddCommGroup β]
  [IsOrderedAddMonoid β] {f : β → E},
  Continuous f → Function.Even f → (Bornology.IsBounded (Set.range f) ↔ f =O[Filter.atTop] 1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_apply_ring' : ∀ {k : Type u_1} [inst : Ring k] (a b c : k), (AffineMap.lineMap a b) c = c * (b - a) + a
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.toMonoid.eq_1 : ∀ {M : Type u_5} [inst : Monoid M] (S : Submonoid M), S.toMonoid = SubmonoidClass.toMonoid S
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.subpresheafToTypes_map : ∀ {X : TopCat} {T : ↑X → Type u_1} (P : TopCat.PrelocalPredicate T) {X_1 Y : (TopologicalSpace.Opens ↑X)ᵒᵖ}
  (i : X_1 ⟶ Y), (TopCat.subpresheafToTypes P).map i = TypeCat.ofHom fun f => ⟨fun x => ↑f (i.unop x), ⋯⟩
-- Init.System.IO
/-- Releases any previously-acquired lock on the handle. Succeeds even if no lock has been acquired.
 -/
IO.FS.Handle.unlock : IO.FS.Handle → IO Unit
-- Mathlib.Topology.Algebra.UniformField
UniformSpace.Completion.instNontrivialOfT0Space : ∀ (K : Type u_1) [Field K] [inst : UniformSpace K] [T0Space K], Nontrivial (UniformSpace.Completion K)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainBialgHomEquiv_symm_apply : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : AddGroup G]
  [inst_3 : AddGroup H] (f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H),
  AddMonoidAlgebra.mapDomainBialgHomEquiv.symm f = AddMonoidAlgebra.mapDomainOfBialgHom f
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc : ∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V) {Z : CommRingCat} (h_1 : (X.restrict h).presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)
      (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h x).inv h_1) =
    CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) h_1
-- Mathlib.CategoryTheory.EpiMono
/-- All epis are split  -/
CategoryTheory.SplitEpiCategory.isSplitEpi_of_epi : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.SplitEpiCategory C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Epi f], CategoryTheory.IsSplitEpi f
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_mul_of_lt_of_lt : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftStrictMono α] [MulRightStrictMono α] {a b c d : α},
  a < b → c < d → a * c < b * d
-- Mathlib.RingTheory.RingHom.Surjective
RingHom.surjective_stableUnderComposition : RingHom.StableUnderComposition fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f
-- Lean.Meta.Basic
/-- Runs `k x` with the local declaration `<name> : <type> := <val>` added to the local context, where `x` is the new free variable.
Afterwards, the local declaration is zeta-reduced into the result.
 -/
Lean.Meta.mapLetDeclZeta : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      [MonadLiftT Lean.MetaM n] →
        Lean.Name →
          Lean.Expr →
            Lean.Expr →
              (Lean.Expr → n Lean.Expr) →
                optParam Bool false → optParam Lean.LocalDeclKind Lean.LocalDeclKind.default → n Lean.Expr
-- Mathlib.Order.OmegaCompletePartialOrder
Part.ωSup.eq_1 : ∀ {α : Type u_2} (c : OmegaCompletePartialOrder.Chain (Part α)),
  Part.ωSup c = if h : ∃ a, Part.some a ∈ c then Part.some (Classical.choose h) else Part.none
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.isUniformInducing_equivBoundedOfCompact : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β],
  IsUniformInducing ⇑(ContinuousMap.equivBoundedOfCompact α β)
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.lt_of_lt_of_eq : ∀ {α : Type u} [inst : Semiring α] [inst_1 : PartialOrder α] {a b : α}, a < 0 → b = 0 → a + b < 0
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalars.smul_def' : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {M : ModuleCat S} (r : R) (m : ↑M),
  (r •
      have this := m;
      this) =
    f r • m
-- Mathlib.Data.Ordmap.Invariants
Ordnode.node4L_size : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α},
  m.Sized → (l.node4L x m y r).size = l.size + m.size + r.size + 2
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_assoc_flip_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M] {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.AddMonObj.add)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M M).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add M)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h))
-- Init.Internal.Order.Basic
Lean.Order.monotone_readerTRun : ∀ {γ : Sort u_1} {m : Type u_2 → Type u_3} {α σ : Type u_2} [inst : Lean.Order.PartialOrder γ] [Monad m]
  [inst_2 : Lean.Order.PartialOrder (m α)] (f : γ → ReaderT σ m α),
  Lean.Order.monotone f → ∀ (s : σ), Lean.Order.monotone fun x => (f x).run s
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.cancel_left' : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {g : M₂ →SL[σ₂₃] M₃} {f₁ f₂ : M₁ →SL[σ₁₂] M₂},
  Function.Injective ⇑g → (g ∘SL f₁ = g ∘SL f₂ ↔ f₁ = f₂)
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.noSibling_tail? : ∀ {α : Type u_1} {le : α → α → Bool} {s' s : Batteries.PairingHeapImp.Heap α},
  Batteries.PairingHeapImp.Heap.tail? le s = some s' → s'.NoSibling
-- Mathlib.Tactic.GRewrite.Elab
/-- `grewrite [e₁, ..., eₙ]` uses each expression `eᵢ : Rᵢ aᵢ bᵢ` (where `Rᵢ` is any two-argument
relation) as a generalized rewrite rule on the main goal, replacing occurrences of `aᵢ` with `bᵢ`.
Use `grewrite [← eᵢ]` to rewrite in the other direction, replacing occurrences of `bᵢ` with `aᵢ`.

If an expression `e` is a defined constant, then the equational theorems associated with `e` are
used. This provides a convenient way to unfold `e`. If `e` has parameters, the tactic will try to
fill these in by unification with the matching part of the target. Parameters are only filled in
once per rule, restricting which later rewrites can be found. Parameters that are not filled in
after unification will create side goals.

To be able to use `grewrite`, the relevant lemmas need to be tagged with `@[gcongr]`.
To rewrite inside a transitive relation, you can also give it an `IsTrans` instance.

Rewriting with a strict inequality `a < b` may change a constant in the goal,
such as changing `<` to `≤`. If this is not possible, then `a < b` is treated the same as `a ≤ b`.

`grw` is like `grewrite` but tries to close the goal afterwards by "cheap" (reducible) `rfl`.
To rewrite only in the `n`-th position, use `nth_grewrite n`.
`apply_rewrite [e₁, ..., eₙ]` is a shorthand for `grewrite +implicationHyp [e₁, ..., eₙ]`: it
interprets `· → ·` as a relation instead of adding the hypothesis as a side condition.

* `grewrite [← e]` applies the rewrite rule `e : R a b` in the reverse direction, replacing
  occurrences of `b` with `a`.
* `grewrite (config := cfg) [e₁, ..., eₙ]` uses `cfg` as configuration. See `GRewrite.Config` for
  details.
  * To let `grewrite` unfold more aggressively, as in `erw`, use
    `grewrite (transparency := default) [e₁, ..., eₙ]`.
  * `grewrite +implicationHyp [e₁, ..., eₙ]` interprets `· → ·` as a relation (see `apply_rewrite`).
* `grewrite [e₁, ..., eₙ] at l` rewrites at the location(s) `l`.
 -/
Mathlib.Tactic.GRewrite.grewriteSeq : Lean.ParserDescr