mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Function
Function.leftInverse_of_surjective_of_rightInverse : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α},
  Function.Surjective f → Function.RightInverse f g → Function.LeftInverse f g
-- Mathlib.Algebra.Group.InjSurj
/-- A type has right-cancellative addition, if it admits an injective map that
preserves `+` to another type with right-cancellative addition.  -/
Function.Injective.isRightCancelAdd : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Add M₂] [IsRightCancelAdd M₂] (f : M₁ → M₂),
  Function.Injective f → (∀ (x y : M₁), f (x + y) = f x + f y) → IsRightCancelAdd M₁
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instIsAddMonHomε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal],
  CategoryTheory.IsAddMonHom (CategoryTheory.Functor.LaxMonoidal.ε F)
-- Mathlib.Topology.Basic
TopologicalSpace.ext_iff_isClosed : ∀ {X : Type u_2} {t₁ t₂ : TopologicalSpace X}, t₁ = t₂ ↔ ∀ (s : Set X), IsClosed s ↔ IsClosed s
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.EditableDocument.mk.injEq : ∀ (toEditableDocumentCore : Lean.Server.FileWorker.EditableDocumentCore) (reporter : Lean.Server.ServerTask Unit)
  (toEditableDocumentCore_1 : Lean.Server.FileWorker.EditableDocumentCore) (reporter_1 : Lean.Server.ServerTask Unit),
  ({ toEditableDocumentCore := toEditableDocumentCore, reporter := reporter } =
      { toEditableDocumentCore := toEditableDocumentCore_1, reporter := reporter_1 }) =
    (toEditableDocumentCore = toEditableDocumentCore_1 ∧ reporter = reporter_1)
-- Mathlib.Tactic.Widget.SelectPanelUtils
/-- The range in the source document where the command will be inserted.  -/
SelectInsertParams.replaceRange : SelectInsertParams → Lean.Lsp.Range
-- Init.Data.Vector.Basic
/-- Lexicographic comparator for vectors.

`lex v w lt` is true if
- `v` is pairwise equivalent via `==` to `w`, or
- there is an index `i` such that `lt v[i] w[i]`, and for all `j < i`, `v[j] == w[j]`.
 -/
Vector.lex : {α : Type u_1} → {n : ℕ} → [BEq α] → Vector α n → Vector α n → autoParam (α → α → Bool) Vector.lex._auto_1 → Bool
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Get the smallest element in the tree that is `≥ x`.

```
findGe 2 {1, 2, 4} = some 2
findGe 3 {1, 2, 4} = some 4
findGe 5 {1, 2, 4} = none
```  -/
Ordnode.findGe : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → Option α
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
mul_inv_le_iff_le_mul' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, a * b⁻¹ ≤ c ↔ a ≤ b * c
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAtFilter_iff_hasFDerivAtFilter : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)} [inst_4 : ContinuousSMul 𝕜 F],
  HasDerivAtFilter f f' L ↔ HasFDerivAtFilter f (ContinuousLinearMap.toSpanSingleton 𝕜 f') L
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.isInteriorPoint_disjointUnion_right : ∀ {𝕜 : 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] {M' : Type u_5} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {p : M ⊕ M'},
  I.IsInteriorPoint p → ∀ (hright : p.isRight = true), I.IsInteriorPoint (p.getRight hright)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.smul_refl : ∀ {R : Type u_1} {S : Type u_4} {M : Type u_5} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass R S M] [inst_6 : SMul S R]
  [inst_7 : IsScalarTower S R M] (α : Sˣ), α • LinearEquiv.refl R M = DistribMulAction.toLinearEquiv R M α
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_update_ne : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) {n i : ℕ} (a : R), i ≠ n → (p.update n a).coeff i = p.coeff i
-- ProofWidgets.Presentation.Expr
ProofWidgets.getExprPresentations : ProofWidgets.GetExprPresentationsParams → Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.ExprPresentations)
-- Lean.Parser.Term
Lean.Parser.Term.match.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGE_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α fun x => β}
  (hto : t.Ordered) {k : α} (he : ∃ a ∈ t, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.Const.getEntryGE k t hto he =
    ((Std.DTreeMap.Internal.Impl.getEntryGE k t hto he).fst, (Std.DTreeMap.Internal.Impl.getEntryGE k t hto he).snd)
-- Mathlib.Data.Finsupp.Weight
/-- A weight function is nontorsion if its values are not torsion.  -/
Finsupp.NonTorsionWeight : {σ : Type u_1} →
  {M : Type u_2} → (R : Type u_3) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → (σ → M) → Prop
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_sub_norm_sub_le_norm_sub : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (u v w : E), ‖u - w‖ - ‖v - w‖ ≤ ‖u - v‖
-- Mathlib.Analysis.Convex.Topology
/-- A convex set `s` is strictly convex provided that for any two distinct points `x`, `y` of
`s \ interior s`, the segment with endpoints `x`, `y` has nonempty intersection with
`interior s`.  -/
Convex.strictConvex : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → ((s \ interior s).Pairwise fun x y => (segment 𝕜 x y \ frontier s).Nonempty) → StrictConvex 𝕜 s
-- Mathlib.RingTheory.Etale.Pi
Algebra.FormallyEtale.instForallOfFinite : ∀ {R : Type u_1} {I : Type u_2} (A : I → Type u_3) [inst : CommRing R] [inst_1 : (i : I) → CommRing (A i)]
  [inst_2 : (i : I) → Algebra R (A i)] [Finite I] [∀ (i : I), Algebra.FormallyEtale R (A i)],
  Algebra.FormallyEtale R ((i : I) → A i)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_of_le_of_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g₁ g₂ : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    g₁ ≤ᵐ[μ] f →
      f ≤ᵐ[μ] g₂ → MeasureTheory.Integrable g₁ μ → MeasureTheory.Integrable g₂ μ → MeasureTheory.Integrable f μ
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_natDegree_eq_C : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R),
  (Polynomial.hasseDeriv f.natDegree) f = Polynomial.C f.leadingCoeff
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- Construct a modification isomorphism between strong transformations
by giving object level isomorphisms, and checking naturality only in the forward direction.
 -/
CategoryTheory.Pseudofunctor.StrongTrans.isoMk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          {η θ : F ⟶ G} →
            (app : (a : B) → η.app a ≅ θ.app a) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
                        (θ.naturality f).hom =
                      CategoryTheory.CategoryStruct.comp (η.naturality f).hom
                        (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f)))
                  CategoryTheory.Pseudofunctor.StrongTrans.isoMk._auto_1 →
                (η ≅ θ)
-- Init.Control.Lawful.Instances
ExceptT.bind_throw : ∀ {m : Type u_1 → Type u_2} {α ε β : Type u_1} {e : ε} [inst : Monad m] [LawfulMonad m] (f : α → ExceptT ε m β),
  throw e >>= f = throw e
-- Init.Data.Nat.Basic
Nat.pow_add_one : ∀ (n m : ℕ), n ^ (m + 1) = n ^ m * n
-- Mathlib.RingTheory.Kaehler.Basic
instAddCommGroupKaehlerDifferential : (R : Type u_2) →
  (S : Type u_1) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → AddCommGroup Ω[S⁄R]
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.skipBlock.nonEmptyLine : Lean.Parser.ParserFn
-- Mathlib.Data.Set.Card
Set.ncard_sumEquiv_symm_apply : ∀ {α : Type u_3} (s : Set α), (Set.sumEquiv.symm (s, s)).ncard = s.ncard + s.ncard
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.monad_seq_eq_seq : ∀ {α β : Type u} (q : PMF (α → β)) (p : PMF α), q <*> p = q.seq p
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.isPushout : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] (j : ι),
  CategoryTheory.IsPushout (f.t j) (f.m j) (SSet.Subcomplex.homOfLE ⋯) (f.b j)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictMonoOn.mul_const' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [MulRightStrictMono α], StrictMonoOn f s → ∀ (c : α), StrictMonoOn (fun x => f x * c) s
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
_private.Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes.0.CategoryTheory.Limits.WalkingPair.swap.match_1.eq_2 : ∀ (motive : CategoryTheory.Limits.WalkingPair → Sort u_1) (h_1 : Unit → motive CategoryTheory.Limits.WalkingPair.left)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingPair.right),
  (match CategoryTheory.Limits.WalkingPair.right with
    | CategoryTheory.Limits.WalkingPair.left => h_1 ()
    | CategoryTheory.Limits.WalkingPair.right => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.yonedaFunctor_reflectsLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} CategoryTheory.yoneda
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.update_zero_eq_erase : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), p.update n 0 = Polynomial.erase n p
-- Mathlib.Data.Set.Lattice.Image
Set.preimage_sInter : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set β)}, f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t
-- Init.PropLemmas
Decidable.not_exists_not : ∀ {α : Sort u_1} {p : α → Prop} [(x : α) → Decidable (p x)], (¬∃ x, ¬p x) ↔ ∀ (x : α), p x
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_neg_I : Complex.log (-Complex.I) = -(↑Real.pi / 2) * Complex.I
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.ensureDefEq : Lean.Expr → Lean.Expr → Lean.MetaM Unit
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_to_bool : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → Bool}, MeasurableSet (f ⁻¹' {true}) → Measurable f
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.instRespectsIsoIsLocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C),
  P.isLocal.RespectsIso
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
isInertiaField_iff : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (E : Type u_6) [inst_4 : Field E] [inst_5 : Algebra E L]
  [inst_6 : MulSemiringAction Gal(L/K) B], IsInertiaField K L P E ↔ IsGaloisGroup (↥(Ideal.inertia Gal(L/K) P)) E L
-- Mathlib.Data.Set.Prod
Set.forall_prod_set : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {p : α × β → Prop},
  (∀ x ∈ s ×ˢ t, p x) ↔ ∀ x ∈ s, ∀ y ∈ t, p (x, y)
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorAccess.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (next : α) → motive (some next)),
  (match none with
    | none => h_1 ()
    | some next => h_2 next) =
    h_1 ()
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.one_lt_prod_iff_of_one_le : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : CommMonoid M] [inst_2 : PartialOrder M]
  [IsOrderedCancelMonoid M] {f : ι → M}, 1 ≤ f → (1 < ∏ i, f i ↔ 1 < f)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.Cauchy.exists_lb_eventual_support : ∀ {K : Type u_2} [inst : Field K] {ℱ : Filter (LaurentSeries K)},
  Cauchy ℱ → ∃ N, ∀ᶠ (f : LaurentSeries K) in ℱ, ∀ n < N, f.coeff n = 0
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- A variant of `iteratedDeriv_mul_const` without differentiability assumption when
the multiplication is in a division ring.  -/
iteratedDeriv_mul_const_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_6} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {n : ℕ} (f : 𝕜 → 𝕜') (c : 𝕜'),
  iteratedDeriv n (fun x => f x * c) x = iteratedDeriv n f x * c
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {a : α},
  t.contains a = false → t.get! a = default
-- Mathlib.Logic.Function.Iterate
Function.iterate_succ' : ∀ {α : Type u} (f : α → α) (n : ℕ), f^[n.succ] = f ∘ f^[n]
-- Init.Data.Array.Find
Array.find?_empty : ∀ {α : Type u_1} {p : α → Bool}, Array.find? p #[] = none
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.one_lt_mul'`.  -/
Right.one_lt_mul' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b : α}, 1 < a → 1 < b → 1 < a * b
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  [inst_2 : CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f}
  (i : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).snd = CategoryTheory.Limits.Cofork.π c
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instAddCommGroup : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : AddCommGroup γ] → [IsTopologicalAddGroup γ] → AddCommGroup (α →ₘ[μ] γ)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.congr_of_eventuallyEq : ∀ {𝕜 : 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'} {x : M} {s : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
  HasMFDerivAt[s] f x f' → f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → HasMFDerivAt[s] f₁ x f'
-- Init.Core
Std.instCommutativeIff : Std.Commutative Iff
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.grw.inj : ∀ {i : Mathlib.Tactic.ClickSuggestions.GrwInfo} {arr : Array Mathlib.Tactic.ClickSuggestions.GrwLemma}
  {i_1 : Mathlib.Tactic.ClickSuggestions.GrwInfo} {arr_1 : Array Mathlib.Tactic.ClickSuggestions.GrwLemma},
  Mathlib.Tactic.ClickSuggestions.Candidates.grw✝ i arr = Mathlib.Tactic.ClickSuggestions.Candidates.grw✝ i_1 arr_1 →
    i = i_1 ∧ arr = arr_1
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The (finite!) set of machine states visited during the course of evaluation of `c`,
including the state `ret k` but not any states after that (that is, the states visited while
evaluating `k`).  -/
Turing.PartrecToTM2.codeSupp' : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Finset Turing.PartrecToTM2.Λ'
-- Mathlib.Algebra.Order.Hom.Basic
le_map_add_map_sub' : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [AddGroupSeminormClass F α β] (f : F) (x y : α), f x ≤ f y + f (y - x)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.unop_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.Splitting), h.unop.s = h.r.unop
-- Mathlib.RingTheory.Algebraic.Denominator
Algebra.natDenominator_def : ∀ {S : Type u_2} [inst : CommRing S] (x : S), Algebra.natDenominator x = (Algebra.denominator ℤ x).natAbs
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixedPoints_addSubgroup_iSup : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] {ι : Sort u_3} {P : ι → AddSubgroup M},
  AddAction.fixedPoints (↥(iSup P)) α = ⋂ i, AddAction.fixedPoints (↥(P i)) α
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mclosure_range_inl_union_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddSubmonoid.closure (Set.range ⇑AddMonoid.Coprod.inl ∪ Set.range ⇑AddMonoid.Coprod.inr) = ⊤
-- Plausible.Arbitrary
Plausible.Int.Arbitrary : Plausible.Arbitrary ℤ
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
/-- The sublattice of invariant submodules of the root space.  -/
RootPairing.invtRootSubmodule : {ι : 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] → RootPairing ι R M N → Sublattice (Submodule R M)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_empty : ∀ {ι : Type u'} (R : Type u_2) {M : Type u_4} (v : ι → M) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndepOn R v ∅
-- Lean.Meta.ArgsPacker
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.withCurriedDecl.go : {α : Type} →
  Lean.Meta.ArgsPacker → Lean.Name → (Array Lean.Expr → Lean.MetaM α) → List Lean.Expr → Array Lean.Expr → Lean.MetaM α
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContinuousOn.continuousOn_iteratedFDerivWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F}
  {n : WithTop ℕ∞} {k : ℕ},
  ContDiffOn 𝕜 n f s → UniqueDiffOn 𝕜 s → ↑k ≤ n → ContinuousOn (iteratedFDerivWithin 𝕜 k f s) s
-- Lean.Elab.Coinductive
/-- Given the number of parameters and the `InductiveVal` containing flat inductives
(see `mkFlatInductive`) and `CoinductiveElabData` associated with the mutual coinductive
predicates, generates their constructors that correspond to the
constructors given in the original syntax.
 -/
_private.Lean.Elab.Coinductive.0.Lean.Elab.Command.generateCoinductiveConstructors : ℕ → Array Lean.InductiveVal → Array Lean.Elab.Command.CoinductiveElabData → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.natAbs_le_self_sq : ∀ (a : ℤ), ↑a.natAbs ≤ a ^ 2
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.Const.getEntryGED : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → α × β → α × β
-- Mathlib.Order.CompleteLattice.Defs
sSup_mem_upperBounds : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α}, sSup s ∈ upperBounds s
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.extend_apply_self : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  (hs : LinearIndepOn K id s) (x : ↑(hs.extend ⋯)), (Module.Basis.extend hs) x = ↑x
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.toSignedMeasure_smul : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : NNReal),
  (r • j).toSignedMeasure = r • j.toSignedMeasure
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.ceil_logb_natCast : ∀ {b : ℕ} {r : ℝ}, 0 ≤ r → ⌈Real.logb (↑b) r⌉ = Int.clog b r
-- Mathlib.Order.RelSeries
RelSeries.head_cons : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newHead : α) (rel : (newHead, p.head) ∈ r),
  (p.cons newHead rel).head = newHead
-- Mathlib.Topology.Order.Basic
SuccOrder.hasBasis_nhds_Ioc_of_exists_lt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SuccOrder α] {a : α},
  (∃ l, l < a) → (nhds a).HasBasis (fun x => x < a) fun x => Set.Ioc x a
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteSpanningSetsIn.mk : {α : Type u_1} →
  {m0 : MeasurableSpace α} →
    {μ : MeasureTheory.Measure α} →
      {C : Set (Set α)} →
        (set : ℕ → Set α) →
          (∀ (i : ℕ), set i ∈ C) → (∀ (i : ℕ), μ (set i) < ⊤) → ⋃ i, set i = Set.univ → μ.FiniteSpanningSetsIn C
-- Batteries.Tactic.OpenPrivate
/-- Elaborator for `export private`.  -/
Lean.Elab.Command.elabExportPrivate : Lean.Elab.Command.CommandElab
-- Mathlib.Data.Finset.PImage
Part.toFinset.eq_1 : ∀ {α : Type u_1} (o : Part α) [inst : Decidable o.Dom], o.toFinset = o.toOption.toFinset
-- Mathlib.Analysis.Normed.Affine.Simplex
Affine.Simplex.Scalene.dist_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : Module R V] [inst_4 : NormedAddTorsor V P] {n : ℕ}
  {s : Affine.Simplex R P n},
  s.Scalene →
    ∀ {i₁ i₂ i₃ i₄ : Fin (n + 1)},
      i₁ ≠ i₂ →
        i₃ ≠ i₄ →
          ¬(i₁ = i₃ ∧ i₂ = i₄) →
            ¬(i₁ = i₄ ∧ i₂ = i₃) → dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
-- Std.Do.SPred.Notation
/-- Entailment in `SPred`; sugar for `SPred.entails`.  -/
Std.Do.«term_⊢ₛ_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmodRepr_natCast_ofNat : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {n : ℕ}, OfNat.ofNat n < p → (OfNat.ofNat n).zmodRepr = OfNat.ofNat n
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.add_one_mul_T_eq_poly_in_U : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ),
  (↑n + 1) * Polynomial.Chebyshev.T R (n + 1) =
    Polynomial.X * Polynomial.Chebyshev.U R n -
      (1 - Polynomial.X ^ 2) * Polynomial.derivative (Polynomial.Chebyshev.U R n)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_smul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {R : Type u_10} [inst : SMul R α] (c : R) (M : Matrix m n α),
  (c • M).transpose = c • M.transpose
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The orthogonal projection of the circumcenter onto a face is the
circumcenter of that face.  -/
Affine.Simplex.orthogonalProjection_circumcenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {fs : Finset (Fin (n + 1))} {m : ℕ}
  (h : fs.card = m + 1), ↑((s.face h).orthogonalProjectionSpan s.circumcenter) = (s.face h).circumcenter
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOver_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X A A' : C} (f : A ⟶ A'),
  (CategoryTheory.toOver X).map f = CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X) ⋯
-- Mathlib.Combinatorics.Additive.Convolution
Finset.addConvolution_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A B : Finset G} {x : G},
  A.addConvolution B x ≠ 0 ↔ x ∈ A + B