mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_mul_right_add_left : ∀ (m n k : ℕ), (k * n + m).Coprime n ↔ m.Coprime n
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_mul_single_apply : ∀ {R : Type u_1} {G : Type u_3} [inst : Semiring R] [inst_1 : AddGroup G] (x : AddMonoidAlgebra R G) (r : R) (g h : G),
  (x * AddMonoidAlgebra.single g r).coeff h = x.coeff (h + -g) * r
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Alternative definition of the direction when the affine subspace is nonempty. This is defined so
that the order on submodules (as used in the definition of `Submodule.span`) can be used in the
proof of `coe_direction_eq_vsub_set`, and is not intended to be used beyond that proof.  -/
AffineSubspace.directionOfNonempty : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → {s : AffineSubspace k P} → (↑s).Nonempty → Submodule k V
-- Mathlib.Control.Functor.Multivariate
MvFunctor.id_map : ∀ {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [inst : MvFunctor F] [LawfulMvFunctor F] (x : F α),
  MvFunctor.map TypeVec.id x = x
-- Lean.CoreM
Lean.Core.Cache.mk : Lean.Core.InstantiateLevelCache → Lean.Core.InstantiateLevelCache → Lean.Core.Cache
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instInhabited : Inhabited ZFSet.{u_1}
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] →
        (toSquare : CategoryTheory.Square C) →
          autoParam (CategoryTheory.Mono toSquare.f₁₃)
              CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃._autoParam →
            (toSquare.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout →
              J.MayerVietorisSquare
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.HasWeakSheafify J B]
  [inst_4 : CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F],
  CategoryTheory.IsIso (CategoryTheory.toPresheafToSheafCompComposeAndSheafify J F)
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.instIsClosedUnderIsomorphismsEssImage : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}, F.essImage.IsClosedUnderIsomorphisms
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_isLocalDiffeomorphAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x), IsLocalDiffeomorphAt J I n (↑hf.localInverse.toPartialEquiv) (f x)
-- Lean.Compiler.NameMangling
/-- Given `s = nm.mangle pre` for some `nm : Name` and `pre : String` with `nm != Name.anonymous`,
returns `(mkBoxedName nm).mangle pre`. This is used in the interpreter to find names of boxed
IR declarations.
 -/
Lean.mkMangledBoxedName : String → String
-- Init.System.IO
IO.FS.DirEntry.mk.injEq : ∀ (root : System.FilePath) (fileName : String) (root_1 : System.FilePath) (fileName_1 : String),
  ({ root := root, fileName := fileName } = { root := root_1, fileName := fileName_1 }) =
    (root = root_1 ∧ fileName = fileName_1)
-- Mathlib.Order.Filter.NAry
Filter.map₂_pure_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {b : β},
  Filter.map₂ m f (pure b) = Filter.map (fun x => m x b) f
-- Mathlib.Dynamics.Ergodic.Action.Basic
ErgodicSMul.of_aestabilizer : ∀ (G : Type u_1) {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Group G]
  [inst_1 : MulAction G α] [inst_2 : MeasureTheory.SMulInvariantMeasure G α μ],
  (∀ (s : Set α), MeasurableSet s → MulAction.aestabilizer G μ s = ⊤ → Filter.EventuallyConst s (MeasureTheory.ae μ)) →
    ErgodicSMul G α μ
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.cechNerveEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C)
  (G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F),
  (CategoryTheory.SimplicialObject.cechNerveEquiv X F) G = CategoryTheory.SimplicialObject.equivalenceLeftToRight X F G
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- A function on `ℍ` which is invariant under `SL(2, ℤ)`, and bounded at `∞`, is uniformly
bounded.  -/
ModularGroup.exists_bound_of_invariant : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {f : UpperHalfPlane → E},
  Continuous f →
    UpperHalfPlane.IsBoundedAtImInfty f →
      (∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), f (g • τ) = f τ) →
        ∃ C, ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- **Alias** of `intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOfPred_lt_ne_zero`.

---

If `f` and `g` are two functions that are interval integrable on `a..b`, `a ≤ b`,
`f x ≤ g x` for a.e. `x ∈ Set.Ioc a b`, and `f x < g x` on a subset of `Set.Ioc a b`
of nonzero measure, then `∫ x in a..b, f x ∂μ < ∫ x in a..b, g x ∂μ`.  -/
intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero : ∀ {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b →
    IntervalIntegrable f μ a b →
      IntervalIntegrable g μ a b →
        f ≤ᵐ[μ.restrict (Set.Ioc a b)] g →
          (μ.restrict (Set.Ioc a b)) {x | f x < g x} ≠ 0 → ∫ (x : ℝ) in a..b, f x ∂μ < ∫ (x : ℝ) in a..b, g x ∂μ
-- Mathlib.Tactic.Algebra.AlgebraNF
/-- Turn scalar multiplication by an explicit constant in `R` into multiplication in `A`.

e.g. `(4 : ℚ) • x` becomes `4 * x` but `↑n • x` stays `↑n • x`.
 -/
Mathlib.Tactic.Algebra.cleanupConsts : Mathlib.Tactic.RingNF.Config → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg.eq_1 : ∀ (i : Int64), i.toNatClampNeg = i.toInt.toNat
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The inclusion `Δ[1] ⟶ Λ[2, 1]` which avoids `0`.  -/
SSet.horn₂₁.ι₁₂ : SSet.stdSimplex.obj { len := 1 } ⟶ (SSet.horn 2 1).toSSet
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.basicOpen_res_eq : ∀ (X : AlgebraicGeometry.Scheme) {V U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U)))
  (i : Opposite.op U ⟶ Opposite.op V) [CategoryTheory.IsIso i],
  X.basicOpen ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map i)) f) = X.basicOpen f
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {f : β → β},
  (m.modify k f).getKey? k' = if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Walk.ofBoxProdRight.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [inst : DecidableEq α]
  [inst_1 : DecidableRel H.Adj] {x : α × β}, SimpleGraph.Walk.nil.ofBoxProdRight = SimpleGraph.Walk.nil
-- Batteries.Data.Fin.Lemmas
Fin.findSomeRev?_eq_none_iff : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, Fin.findSomeRev? f = none ↔ ∀ (i : Fin n), f i = none
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Construct a morphism from the multicoequalizer from its universal property.  -/
CategoryTheory.Limits.Multicoequalizer.desc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] →
          (W : C) →
            (k : (b : J.R) → I.right b ⟶ W) →
              (∀ (a : J.L),
                  CategoryTheory.CategoryStruct.comp (I.fst a) (k (J.fst a)) =
                    CategoryTheory.CategoryStruct.comp (I.snd a) (k (J.snd a))) →
                (CategoryTheory.Limits.multicoequalizer I ⟶ W)
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
/-- Auxiliary lemma for `rnDeriv_add_right_of_mutuallySingular`.  -/
MeasureTheory.Measure.rnDeriv_add_right_of_mutuallySingular' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν ν' : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite ν'],
  μ.MutuallySingular ν' → ν.MutuallySingular ν' → μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν
-- Init.Data.UInt.Lemmas
UInt32.le_rfl : ∀ {a : UInt32}, a ≤ a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.addX_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.addX P (W'.neg P) = 0
-- Mathlib.Algebra.Order.Monoid.OrderDual
OrderDual.isOrderedAddMonoid : ∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α], IsOrderedAddMonoid αᵒᵈ
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.instFreeAsModuleOfNat : ∀ {R : Type u} [inst : CommSemiring R], Module.Free R (CommRing.Pic.AsModule 1)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.ofEquivFun.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι] (e : M ≃ₗ[R] ι → R),
  Module.Basis.ofEquivFun e = { repr := e ≪≫ₗ (Finsupp.linearEquivFunOnFinite R R ι).symm }
-- Mathlib.Algebra.Homology.Embedding.TruncGE
ComplexShape.Embedding.truncGEFunctor_obj : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsTruncGE]
  (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.CategoryWithHomology C]
  (K : HomologicalComplex C c'), (e.truncGEFunctor C).obj K = K.truncGE e
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction.congr_simp : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X : C} {X₀ : C₀}
  (f f_1 : F.obj X₀ ⟶ X),
  f = f_1 →
    CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction data G₀ f =
      CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction data G₀ f_1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- A monoid object `M` is commutative if and only if `X ⟶ M` is commutative for all `X`.  -/
CategoryTheory.isCommMonObj_iff_isMulCommutative : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.BraidedCategory C],
  CategoryTheory.IsCommMonObj M ↔ ∀ (X : C), IsMulCommutative (X ⟶ M)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial_one_eq : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (e : σ →₀ ℕ),
  (MvPowerSeries.monomial e) 1 = e.prod fun s n => MvPowerSeries.X s ^ n
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_stabilizerSubmonoid_iff : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] {a : α} {m : M},
  m ∈ MulAction.stabilizerSubmonoid M a ↔ m • a = a
-- Mathlib.SetTheory.Cardinal.Defs
/-- The indexed sum of cardinals is the cardinality of the
indexed disjoint union, i.e. sigma type.  -/
Cardinal.sum : {ι : Type u_1} → (ι → Cardinal.{u_2}) → Cardinal.{max u_2 u_1}
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.mapEquiv.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α ≃ β), M.mapEquiv f = M.mapEmbedding f.toEmbedding
-- Init.Data.UInt.Lemmas
UInt64.toUSize_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < UInt64.size → (UInt64.ofNatClamp n).toUSize = USize.ofNat n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.op_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y),
  (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).op = CategoryTheory.Limits.BinaryCofan.mk π₁.op π₂.op
-- Std.Data.TreeSet.Raw.Basic
/-- Returns the `n`-th smallest element, or `none` if `n` is at least `t.size`.  -/
Std.TreeSet.Raw.atIdx? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → ℕ → Option α
-- Mathlib.Data.Set.Subsingleton
/-- A set `s` is a `Subsingleton` if it has at most one element.  -/
Set.Subsingleton : {α : Type u} → Set α → Prop
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff_smul' : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] {V : Type u_8} [inst_1 : Zero V] [inst_2 : SMulZeroClass R V]
  (r : R) (x : HahnSeries Γ V), (r • x).coeff = r • x.coeff
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, k ∉ t₁ → (t₁ ∩ t₂).getKey! k = default
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.revSkip?_eq_revMatchAt? : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, pos.revSkip? pat = String.Slice.Pattern.Model.revMatchAt? pat pos
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- Turning an edge in the spanning tree into a loop gives the identity loop.  -/
IsFreeGroupoid.SpanningTree.loopOfHom_eq_id : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)]
  {a b : IsFreeGroupoid.Generators G},
  ∀ e ∈ Quiver.wideSubquiverSymmetrify T a b,
    IsFreeGroupoid.SpanningTree.loopOfHom T (IsFreeGroupoid.of e) =
      CategoryTheory.CategoryStruct.id (IsFreeGroupoid.SpanningTree.root'✝ T)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.comapMonoidHom.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6}
  [inst_2 : MulOneClass Z] (f : C(X, Y)),
  LocallyConstant.comapMonoidHom f = { toFun := LocallyConstant.comap f, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Data.List.Defs
/-- `dedup l` removes duplicates from `l` (taking only the last occurrence).
Defined as `pwFilter (≠)`.

See also `eraseDups` which keeps the first occurrence instead:
```
dedup [2, 0, 1, 0, 2, 0] = [1, 2, 0]
eraseDups [2, 0, 1, 0, 2, 0] = [2, 0, 1]
```  -/
List.dedup : {α : Type u_1} → [DecidableEq α] → List α → List α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_union_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} (mem : k ∈ t₂), (t₁ ∪ t₂).get k ⋯ = t₂.get k mem
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.Integrable.comp_mul_right : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : Group G] [MeasurableMul G] {f : G → F} [μ.IsMulRightInvariant],
  MeasureTheory.Integrable f μ → ∀ (g : G), MeasureTheory.Integrable (fun t => f (t * g)) μ
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.congr_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D),
  (CategoryTheory.MonoOver.congr X e).functor = CategoryTheory.MonoOver.lift (CategoryTheory.Over.post e.functor) ⋯
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.pushNone.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.VectorBundle.Basic
/-- The total space of the vector bundle, as a convenience function for dot notation.
It is by definition equal to `Bundle.TotalSpace F Z.Fiber`.  -/
VectorBundleCore.TotalSpace : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] → {ι : Type u_5} → VectorBundleCore R B F ι → Type (max u_2 u_3)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.π_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (c : CategoryTheory.Limits.PullbackCone f g), c.π.app CategoryTheory.Limits.WalkingCospan.right = c.snd
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.weightedSMul_nonneg : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder F] [IsOrderedModule ℝ F] (s : Set α) (x : F),
  0 ≤ x → 0 ≤ (MeasureTheory.weightedSMul μ s) x
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffOn.congr_mono : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {s s₁ : Set M}
  {n : WithTop ℕ∞}, ContMDiffOn I I' n f s → (∀ y ∈ s₁, f₁ y = f y) → s₁ ⊆ s → ContMDiffOn I I' n f₁ s₁
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.uniqueHomToTrivial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (A : CategoryTheory.Grp C) → Unique (A ⟶ CategoryTheory.Grp.trivial C)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (m₁ \ m₂).size + (m₁ ∩ m₂).size = m₁.size
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.range_isFinite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w))
  [CategoryTheory.PresheafIsFinite F] {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ F'),
  (CategoryTheory.Subfunctor.range f).IsFinite
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.eqToHom_snd : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] {X Y : C × D} (h : X = Y),
  (CategoryTheory.eqToHom h).2 = CategoryTheory.eqToHom ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.comp_app_assoc : ∀ {X Y Z : SSet} (f : X ⟶ Y) (g : Y ⟶ Z) (n : SimplexCategoryᵒᵖ) {Z_1 : Type u_1} (h : Z.obj n ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).app n) h =
    CategoryTheory.CategoryStruct.comp (f.app n) (CategoryTheory.CategoryStruct.comp (g.app n) h)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- Using `homogeneousLocalizationToStalk`, we construct a ring isomorphism between stalk at `x`
and homogeneous localization at `x` for any point `x` in `Proj`.  -/
AlgebraicGeometry.Proj.stalkIso' : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (x : ↑(ProjectiveSpectrum.top 𝒜)) →
                ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.stalk x) ≃+*
                  HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
FiberBundle.chartedSpace_chartAt_symm_fst : ∀ {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace F]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)] {HB : Type u_7}
  [inst_3 : TopologicalSpace HB] [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B] [inst_6 : FiberBundle F E]
  (x : Bundle.TotalSpace F E),
  ∀ y ∈ (chartAt (ModelProd HB F) x).target, (↑(chartAt (ModelProd HB F) x).symm y).proj = ↑(chartAt HB x.proj).symm y.1
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_inf : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (S T : Submonoid M) (f : F),
  Function.Injective ⇑f → Submonoid.map f (S ⊓ T) = Submonoid.map f S ⊓ Submonoid.map f T
-- Lean.Meta.Tactic.Grind.Arith.CommRing.PP
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.PP.0.Lean.Meta.Grind.Arith.CommRing.ppDiseqs? : Lean.Meta.Grind.Arith.CommRing.M✝ (Option Lean.MessageData)
-- Mathlib.Topology.Inseparable
/-- A map `f` between topological spaces is generalizing if generalizations lifts along `f`,
i.e. for each `y ⤳ f x'` there is some `x ⤳ x'` whose image is `y`.  -/
GeneralizingMap : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- This structure encodes the data required for a family of morphisms to be effective epimorphic.
 -/
CategoryTheory.EffectiveEpiFamilyStruct : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {B : C} → {α : Type u_2} → (X : α → C) → ((a : α) → X a ⟶ B) → Type (max (max u_1 u_2) v_1)
-- Mathlib.Topology.Closure
closure_iUnion₂_le_nat : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} (f : ℕ → Set X),
  closure (⋃ m, ⋃ (_ : m ≤ n), f m) = ⋃ m, ⋃ (_ : m ≤ n), closure (f m)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_eq_getD_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {fallback : β a}, t.getD a fallback = (t.get? a).getD fallback
-- Lean.Elab.Tactic.Rewrite
/-- Makes new goals be synthetic opaque, to be done once elaboration of the rewrite theorem is complete.

Workaround note: we are only doing this for proof goals, not data goals,
since there are many downstream cases of tactic proofs that later assign data goals by unification.
 -/
Lean.Elab.Tactic.finishElabRewrite : Lean.Meta.RewriteResult → Lean.MetaM Lean.Meta.RewriteResult