mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instLeftCancelMonoidOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : LeftCancelMonoid Mᵐᵒᵖ], DomMulAct.instLeftCancelMonoidOfMulOpposite = inst
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instIsZariskiLocalAtSourceTopologicallyIsOpenMap : AlgebraicGeometry.IsZariskiLocalAtSource
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsOpenMap)
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.ExceptT.run_bind.match_1.splitter : {ε α : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((x : α) → motive (Except.ok x)) → ((e : ε) → motive (Except.error e)) → motive x
-- Init.Data.Vector.Attach
Vector.find?_subtype : ∀ {α : Type} {n : ℕ} {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Option.map Subtype.val (Vector.find? f xs) = Vector.find? g xs.unattach
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- A copy of `invOf_mul_cancel_right` for rectangular matrices.  -/
Matrix.invOf_mul_cancel_right : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
  (A : Matrix m n α) (B : Matrix n n α) [inst_3 : Invertible B], A * ⅟B * B = A
-- Mathlib.Tactic.Linarith.Preprocessing
/-- `isNatProp tp` is true iff `tp` is an inequality or equality between natural numbers
or the negation thereof.
 -/
Mathlib.Tactic.Linarith.isNatProp : Lean.Expr → Lean.MetaM Bool
-- Std.Time.DateTime.PlainDateTime
/-- Adds a `Nanosecond.Offset` to a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds overflow.
 -/
Std.Time.PlainDateTime.addNanoseconds : Std.Time.PlainDateTime → Std.Time.Nanosecond.Offset → Std.Time.PlainDateTime
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Greatest fixed point of functor F. The result is a functor with one fewer parameters
than the input. For `F a b c` a ternary functor, fix F is a binary functor such that

```lean
Cofix F a b = F a b (Cofix F a b)
```
 -/
MvQPF.Cofix : {n : ℕ} → (F : TypeVec.{u} (n + 1) → Type u) → [MvQPF F] → TypeVec.{u} n → Type u
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF →
    ∀ [inst : Inhabited α] {k : α} {f : β → β},
      (Std.DTreeMap.Raw.Const.modify t k f).getKey! k = if k ∈ t then k else default
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.instIsDomainRingOfIntegers : ∀ (K : Type u_1) [inst : Field K], IsDomain (NumberField.RingOfIntegers K)
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.one : ∀ {G : Type u} [inst : Group G] {B : GroupFilterBasis G} {U : Set G}, U ∈ B → 1 ∈ U
-- Mathlib.Topology.Algebra.InfiniteSum.Module
HasSum.const_smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid α]
  [inst_2 : DistribSMul γ α] [ContinuousConstSMul γ α] {f : β → α} {L : SummationFilter β} {a : α} (b : γ),
  HasSum f a L → HasSum (fun i => b • f i) (b • a) L
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instConcreteCategoryMonoidHomCarrier.eq_1 : CommGrpCat.instConcreteCategoryMonoidHomCarrier =
  { hom := fun {X Y} => CommGrpCat.Hom.hom', ofHom := fun {X Y} => CommGrpCat.Hom.mk✝,
    hom_ofHom := @CommGrpCat.instConcreteCategoryMonoidHomCarrier._proof_1,
    ofHom_hom := @CommGrpCat.instConcreteCategoryMonoidHomCarrier._proof_2,
    id_apply := @CommGrpCat.instConcreteCategoryMonoidHomCarrier._proof_3,
    comp_apply := @CommGrpCat.instConcreteCategoryMonoidHomCarrier._proof_4 }
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- Given a splitting of a short complex `S`, this shows that `S.f` is a split monomorphism.  -/
CategoryTheory.ShortComplex.Splitting.splitMono_f : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} → S.Splitting → CategoryTheory.SplitMono S.f
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.l_u_l_eq_l : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ (b : β), l (u (l b)) = l b
-- Aesop.Nanos
Aesop.Nanos.instDecidableRelLe : DecidableRel fun x1 x2 => x1 ≤ x2
-- Mathlib.Topology.MetricSpace.Bounded
/-- The diameter of a union is controlled by the sum of the diameters, and the distance between
any two points in each of the sets. This lemma is true without any side condition, since it is
obviously true if `s ∪ t` is unbounded.  -/
Metric.diam_union : ∀ {α : Type u} {s : Set α} {x y : α} [inst : PseudoMetricSpace α] {t : Set α},
  x ∈ s → y ∈ t → Metric.diam (s ∪ t) ≤ Metric.diam s + dist x y + Metric.diam t
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_toMeasurable_union : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  μ (MeasureTheory.toMeasurable μ s ∪ t) = μ (s ∪ t)
-- Mathlib.Order.SuccPred.Basic
Order.lt_succ_of_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α], a ≤ b → a < Order.succ b
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_iff_ker : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M}, LinearIndependent R v ↔ (Finsupp.linearCombination R v).ker = ⊥
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_eq_head?_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.minKey? = t.keys.head?
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- A class guaranteeing that the non-unital continuous functional calculus is uniquely determined
by the properties that it is a continuous non-unital star algebra homomorphism mapping the
(restriction of) the identity to `a`. This is the necessary tool used to establish `cfcₙHom_comp`
and the more common variant `cfcₙ_comp`.

This class will have instances in each of the common cases `ℂ`, `ℝ` and `ℝ≥0` as a consequence of
the Stone-Weierstrass theorem.  -/
ContinuousMapZero.UniqueHom : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : MetricSpace R] →
          [IsTopologicalSemiring R] →
            [ContinuousStar R] →
              [inst_5 : NonUnitalRing A] →
                [StarRing A] →
                  [TopologicalSpace A] → [inst_8 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → Prop
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- Let `f : X → Y`. Suppose that to prove that `f` is continuous, it suffices to show that
for every compact Hausdorff space `K` and every continuous map `g : K → X`, `f ∘ g` is continuous.
Then `X` is compactly generated.  -/
compactlyGeneratedSpace_of_continuous_maps : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ {Y : Type u} [inst_1 : TopologicalSpace Y] (f : X → Y),
      (∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (g : K → X),
          Continuous g → Continuous (f ∘ g)) →
        Continuous f) →
    CompactlyGeneratedSpace X
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_vadd_null : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α},
  μ s = 0 → ∀ (c : G), μ (c +ᵥ s) = 0
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- If a point belongs to the closure of `s`, then its infimum distance to `s` equals zero.
The converse is true provided that `s` is nonempty, see `Metric.mem_closure_iff_infDist_zero`.  -/
Metric.infDist_zero_of_mem_closure : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, x ∈ closure s → Metric.infDist x s = 0
-- Std.Async.Basic
Std.Async.ETask.instMonad : {ε : Type} → Monad (Std.Async.ETask ε)
-- Lean.HeadIndex
Lean.HeadIndex.fvar.inj : ∀ {fvarId fvarId_1 : Lean.FVarId}, Lean.HeadIndex.fvar fvarId = Lean.HeadIndex.fvar fvarId_1 → fvarId = fvarId_1
-- Mathlib.Data.Countable.Defs
Quotient.countable : ∀ {α : Sort u} [Countable α] {r : α → α → Prop}, Countable (Quot r)
-- Mathlib.Analysis.Normed.Ring.Basic
ULift.normedRing : {α : Type u_2} → [NormedRing α] → NormedRing (ULift.{u_5, u_2} α)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.coproducts_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C}
  [CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{w, v, u} Q],
  CategoryTheory.MorphismProperty.coproducts.{w, v, u} P ≤ Q ↔ P ≤ Q
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename_coe : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [inst : Filter.TendstoCofinite f] [inst_1 : CommSemiring R]
  (p : MvPolynomial σ R), (MvPowerSeries.rename f) ↑p = ↑((MvPolynomial.rename f) p)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.matchTreeStars.isEq : List Lean.Meta.RefinedDiscrTree.Key →
  List Lean.Meta.RefinedDiscrTree.Key →
    Option (List Lean.Meta.RefinedDiscrTree.Key × List Lean.Meta.RefinedDiscrTree.Key)
-- Mathlib.Algebra.Module.PUnit
PUnit.instVAddAssocClassOfVAdd : ∀ {R : Type u_1} {S : Type u_2} [inst : VAdd R S], VAddAssocClass R S PUnit.{u_3 + 1}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k a : α}, (m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidRevSearchFrom.brecOn : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {motive :
    (a : s.Pos) →
      (a_1 : List (String.Slice.Pattern.SearchStep s)) →
        String.Slice.Pattern.Model.IsValidRevSearchFrom pat a a_1 → Prop}
  {a : s.Pos} {a_1 : List (String.Slice.Pattern.SearchStep s)}
  (t : String.Slice.Pattern.Model.IsValidRevSearchFrom pat a a_1),
  (∀ (a : s.Pos) (a_2 : List (String.Slice.Pattern.SearchStep s))
      (t : String.Slice.Pattern.Model.IsValidRevSearchFrom pat a a_2),
      String.Slice.Pattern.Model.IsValidRevSearchFrom.below t → motive a a_2 t) →
    motive a a_1 t
-- Lean.Data.JsonRpc
/-- Invalid method parameter(s).  -/
Lean.JsonRpc.ErrorCode.invalidParams : Lean.JsonRpc.ErrorCode
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isIso_truncLT_map_truncLTι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ),
  a ≤ b → ∀ (X : C), CategoryTheory.IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
-- Lean.Meta.Tactic.Grind.Core
/-- Pops and returns the next equality to be processed.  -/
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.popNextFact? : Lean.Meta.Grind.GoalM (Option Lean.Meta.Grind.NewFact)
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.defaultRatCDF.eq_1 : ∀ (q : ℚ), ProbabilityTheory.defaultRatCDF q = if q < 0 then 0 else 1
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- Proof-producing ring arithmetic.  -/
Mathlib.Tactic.Determinant.Ctx.rc : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      Mathlib.Tactic.Determinant.Ctx rα →
        Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.RatCoeff
          (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα)
-- Init.Data.String.Defs
String.singleton_eq_asString : ∀ {c : Char}, String.singleton c = String.ofList [c]
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo.mk.sizeOf_spec : ∀ (declName : Lean.Name) (levelParams : List Lean.Name) (type value : Lean.Expr) (declNames : Array Lean.Name)
  (declNameNonRec : Lean.Name) (fixedParamPerms : Lean.Elab.FixedParamPerms)
  (fixpointType : Array Lean.Elab.PartialFixpointType),
  sizeOf
      { declName := declName, levelParams := levelParams, type := type, value := value, declNames := declNames,
        declNameNonRec := declNameNonRec, fixedParamPerms := fixedParamPerms, fixpointType := fixpointType } =
    1 + sizeOf declName + sizeOf levelParams + sizeOf type + sizeOf value + sizeOf declNames + sizeOf declNameNonRec +
        sizeOf fixedParamPerms +
      sizeOf fixpointType
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
/-- **Alias** of `PrimeSpectrum.sigmaToPi_apply`. -/
PrimeSpectrum.coe_sigmaToPi_asIdeal : ∀ {ι : Type u_3} (R : ι → Type u_2) [inst : (i : ι) → CommSemiring (R i)] (i : ι) (p : PrimeSpectrum (R i)),
  PrimeSpectrum.sigmaToPi R ⟨i, p⟩ = PrimeSpectrum.comap (Pi.evalRingHom R i) p
-- Mathlib.Algebra.Ring.Invertible
/-- A version of `inv_sub_inv'` for `Ring.inverse`.  -/
Ring.inverse_sub_inverse : ∀ {R : Type u_1} [inst : Ring R] {a b : R},
  (IsUnit a ↔ IsUnit b) → Ring.inverse a - Ring.inverse b = Ring.inverse a * (b - a) * Ring.inverse b
-- Init.Data.UInt.Lemmas
USize.toUInt64_le : ∀ {a b : USize}, a.toUInt64 ≤ b.toUInt64 ↔ a ≤ b
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `CommMonoid.torsion.isMulTorsion`.

---

Torsion submonoids are torsion.  -/
CommMonoid.torsion.isTorsion : ∀ {G : Type u_1} [inst : CommMonoid G], IsMulTorsion ↥(CommMonoid.torsion G)
-- Init.Data.List.TakeDrop
List.rotateLeft_zero : ∀ {α : Type u_1} {l : List α}, l.rotateLeft 0 = l
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
_private.Mathlib.MeasureTheory.VectorMeasure.Variation.Basic.0.MeasureTheory.VectorMeasure.variation_smul_le : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : NormedAddCommGroup V]
  {μ : MeasureTheory.VectorMeasure X V} {𝕜 : Type u_3} [inst_1 : NormedField 𝕜] [inst_2 : NormedSpace 𝕜 V] {c : 𝕜},
  (c • μ).variation ≤ ‖c‖₊ • μ.variation
-- Init.Data.FloatArray.Basic
FloatArray.instBEq.beq : FloatArray → FloatArray → Bool
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.mul_apply : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (e₁ e₂ : α ≃ᵢ α) (x : α), (e₁ * e₂) x = e₁ (e₂ x)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false}
  {fallback : α}, t.getD (t.min he) fallback = t.min he
-- Init.Data.Option.Basic
Option.mapM_some : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Applicative m] (x : α) (f : α → m β),
  Option.mapM f (some x) = some <$> f x
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- **Alias** of `Metric.eball_coe`.

---

Balls defined using the distance or the edistance coincide  -/
Metric.emetric_ball_nnreal : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : NNReal}, Metric.eball x ↑ε = Metric.ball x ↑ε
-- Init.SimpLemmas
not_true_eq_false : (¬True) = False
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flipFunctor_map_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) {K L : HomologicalComplex₂ C c₁ c₂}
  (f : K ⟶ L) (i : I₂) (j : I₁), (((HomologicalComplex₂.flipFunctor C c₁ c₂).map f).f i).f j = (f.f j).f i
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_insertEntryIfNew_le_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k}, (compare (Std.Internal.List.minKey! (Std.Internal.List.insertEntryIfNew k v l)) k).isLE = true
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.postcomposing₂_obj_app_toFunctor_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (f : a ⟶ b) (x : Bᵒᵖ) {X Y : Opposite.unop x ⟶ a}
  (x_1 : X ⟶ Y),
  (((CategoryTheory.Bicategory.postcomposing₂ a b).obj f).app x).toFunctor.map x_1 =
    CategoryTheory.Bicategory.whiskerRight x_1 f
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_beq : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, Option.all (fun x => x == k) (m.get? k) = true
-- Mathlib.Topology.UniformSpace.Basic
Filter.Tendsto.congr_uniformity : ∀ {α : Type u_2} {β : Type u_3} [inst : UniformSpace β] {f g : α → β} {l : Filter α} {b : β},
  Filter.Tendsto f l (nhds b) → Filter.Tendsto (fun x => (f x, g x)) l (uniformity β) → Filter.Tendsto g l (nhds b)
-- Mathlib.Algebra.Group.Hom.Instances
instIsCancelMulMonoidHom : ∀ {M : Type uM} {N : Type uN} [inst : MulOneClass M] [inst_1 : CommMonoid N] [IsCancelMul N], IsCancelMul (M →* N)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.surj : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (z : N), ∃ x, z + f ↑x.2 = f x.1
-- Init.Data.Nat.Gcd
/-- Characterization of the value of `Nat.gcd`.  -/
Nat.gcd_eq_iff : ∀ {g a b : ℕ}, a.gcd b = g ↔ g ∣ a ∧ g ∣ b ∧ ∀ (c : ℕ), c ∣ a → c ∣ b → c ∣ g
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.sum_apply : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {α : Type u_1} (s : Finset α)
  (g : α → DirectSum ι fun i => β i) (i : ι), (∑ a ∈ s, g a) i = ∑ a ∈ s, (g a) i
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rootSet_def : ∀ {T : Type w} [inst : CommRing T] (p : Polynomial T) (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra T S] [inst_4 : DecidableEq S], p.rootSet S = ↑(p.aroots S).toFinset
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_ric_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Subarray α} {hi : ℕ},
  (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rco.Sliceable.mkSlice xs 0...hi + 1
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.prod_smul_X_eq_smul_monomial_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {A : Type u_4} [inst_1 : CommSemiring A] [inst_2 : Algebra A R]
  (e : σ →₀ ℕ) (a : σ → A),
  (e.prod fun s n => (a s • MvPowerSeries.X s) ^ n) = (e.prod fun s n => a s ^ n) • (MvPowerSeries.monomial e) 1
-- Mathlib.RingTheory.Valuation.Quotient
/-- The extension of valuation `v` on `R` to valuation on `R / J` if `J ⊆ supp v`.  -/
Valuation.onQuot : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] →
        (v : Valuation R Γ₀) → {J : Ideal R} → J ≤ v.supp → Valuation (R ⧸ J) Γ₀
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.gfpApprox_mono_mid : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), Monotone (OrdinalApprox.gfpApprox f)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits
SheafOfModules.instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [J.WEqualsLocallyBijective AddCommGrpCat]
  [CategoryTheory.Limits.HasColimitsOfSize.{w', w, max u' v, max (max (max (v + 1) u) u') v'}
      (PresheafOfModules R.obj)],
  CategoryTheory.Limits.HasColimitsOfSize.{w', w, max u' v, max (max (max (v + 1) u) u') v'} (SheafOfModules R)
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.of_formallyUnramified_and_formallySmooth : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FormallyUnramified R A] [Algebra.FormallySmooth R A], Algebra.FormallyEtale R A
-- Lean.Elab.InfoTree.Main
/-- Resets the trees state `t₀`, runs `x` to produce a new trees state `t₁` and sets the state to be
`t₀ ++ (InfoTree.context (PartialContextInfo.commandCtx Γ) <$> t₁)` where `Γ` is the context derived
from the monad state.
 -/
Lean.Elab.withSaveInfoContext : {m : Type → Type} →
  [Monad m] →
    [Lean.Elab.MonadInfoTree m] →
      {α : Type} →
        [Lean.MonadNameGenerator m] →
          [MonadFinally m] →
            [Lean.MonadEnv m] →
              [Lean.MonadOptions m] → [Lean.MonadMCtx m] → [Lean.MonadResolveName m] → [Lean.MonadFileMap m] → m α → m α
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.mem_saturation_iff' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : AddSubmonoid M} {x : M}, x ∈ s.saturation ↔ ∃ y, y + x ∈ s
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_sdiff_null' : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  μ.real (s₁ ∩ s₂) = 0 →
    autoParam (μ s₁ ≠ ⊤) MeasureTheory.measureReal_sdiff_null'._auto_1 → μ.real (s₁ \ s₂) = μ.real s₁
-- Mathlib.CategoryTheory.Filtered.Small
/-- Implementation detail for the instance
`EssentiallySmall.{max v w} (FullSubcategory (cofilteredClosure f))`.  -/
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.AbstractCofilteredClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsCofilteredOrEmpty C] → {α : Type w} → (α → C) → Type (max v w)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
SemimoduleCat.MonoidalCategory.braiding_naturality : ∀ {R : Type u} [inst : CommSemiring R] {X₁ X₂ Y₁ Y₂ : SemimoduleCat R} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (Y₁.braiding Y₂).hom =
    CategoryTheory.CategoryStruct.comp (X₁.braiding X₂).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom g f)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_eq_fract_mul : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] [inst_3 : FloorRing α]
  {p : α} (hp : 0 < p) (b : α), toIcoMod hp 0 b = Int.fract (b / p) * p
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_iInter_eq_iInter_closure_of_iUnion_indep : ∀ {α : Type u_2} {M : Matroid α} {ι : Sort u_3} [hι : Nonempty ι] (Is : ι → Set α),
  M.Indep (⋃ i, Is i) → M.closure (⋂ i, Is i) = ⋂ i, M.closure (Is i)
-- Mathlib.Algebra.Group.Center
/-- addition commutes  -/
IsAddCentral.comm : ∀ {M : Type u_1} [inst : Add M] {z : M}, IsAddCentral z → ∀ (a : M), AddCommute z a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Polynomial.Chebyshev.integral_T_real_mul_self_measureT_of_ne_zero : ∀ {n : ℕ},
  n ≠ 0 →
    ∫ (x : ℝ),
        Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) *
          Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) ∂Polynomial.Chebyshev.measureT =
      Real.pi / 2
-- Mathlib.Algebra.Group.Commute.Basic
Commute.inv_inv_iff : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a⁻¹ b⁻¹ ↔ Commute a b
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerivedDesc.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (RF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α α_1 : F ⟶ L.comp RF) (e_α : α = α_1) (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1)
  [inst_3 : L.IsLocalization W] [inst_4 : RF.IsRightDerivedFunctor α W] (G : CategoryTheory.Functor D H)
  (β β_1 : F ⟶ L.comp G), β = β_1 → RF.rightDerivedDesc α W G β = RF.rightDerivedDesc α_1 W_1 G β_1