mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.SelfAdjoint
/-- **Alias** of the reverse direction of `IsSelfAdjoint.invOf_iff`. -/
IsSelfAdjoint.invOf : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (x : R) [inst_2 : Invertible x],
  IsSelfAdjoint x → IsSelfAdjoint ⅟x
-- Mathlib.CategoryTheory.SmallObject.Basic
/-- If `I : MorphismProperty C` permits the small object argument,
then the class of morphisms that have the left lifting property with respect to
the maps that have the right lifting property with respect to `I` are
exactly the retracts of transfinite compositions
of pushouts of coproducts of morphisms in `C`.  -/
CategoryTheory.MorphismProperty.llp_rlp_of_hasSmallObjectArgument : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C)
  [I.HasSmallObjectArgument],
  I.rlp.llp =
    (CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u}
        (CategoryTheory.MorphismProperty.coproducts.{w, v, u} I).pushouts).retracts
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- Suppose `X Y : SheafedSpace C`, where `C` is a concrete category,
whose forgetful functor reflects isomorphisms, preserves limits and filtered colimits.
Then a morphism `X ⟶ Y` that is a topological open embedding
is an open immersion iff every stalk map is an iso.
 -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_stalk_iso : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y),
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base) →
    ∀
      [stalk_iso :
        ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)],
      AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ext : ∀ {α : Type ua} {u₁ u₂ : UniformSpace α}, uniformity α = uniformity α → u₁ = u₂
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The `MorphismProperty C` satisfied by regular epimorphisms in `C`.  -/
CategoryTheory.MorphismProperty.regularEpi : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.MorphismProperty C
-- Mathlib.Analysis.InnerProductSpace.Adjoint
Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] (u : ↥(unitary (H →L[𝕜] H))),
  (Unitary.linearIsometryEquiv u).conjStarAlgEquiv = (Unitary.conjStarAlgAut 𝕜 (H →L[𝕜] H)) u
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsTree.isBipartite : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsTree → G.IsBipartite
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocRing.toAddCommGroup : {α : Type u} → [self : NonUnitalNonAssocRing α] → AddCommGroup α
-- Mathlib.LinearAlgebra.TensorProduct.Prod
TensorProduct.prodRight_symm_tmul : ∀ (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [inst : CommSemiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃]
  [inst_5 : Algebra R S] [inst_6 : Module R M₁] [inst_7 : Module S M₁] [inst_8 : IsScalarTower R S M₁]
  [inst_9 : Module R M₂] [inst_10 : Module R M₃] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃),
  (TensorProduct.prodRight R S M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₂, m₁ ⊗ₜ[R] m₃) = m₁ ⊗ₜ[R] (m₂, m₃)
-- Mathlib.Order.Filter.AtTopBot.Ring
Filter.zero_pow_eventuallyEq : ∀ {α : Type u_1} [inst : MonoidWithZero α], (fun n => 0 ^ n) =ᶠ[Filter.atTop] fun x => 0
-- Mathlib.RingTheory.RingHom.Injective
RingHom.injective_stableUnderComposition : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] f => Function.Injective ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
/-- The initial functor `ℕᵒᵖ ⥤ J`, which allows us to turn cofiltered limits over countable preorders
into sequential limits.

TODO: redefine this as `(IsFiltered.sequentialFunctor Jᵒᵖ).leftOp`. This would need API for initial/
final functors of the form `leftOp`/`rightOp`.
 -/
CategoryTheory.Limits.IsCofiltered.sequentialFunctor : (J : Type u_2) → [Countable J] → [inst : Preorder J] → [CategoryTheory.IsCofiltered J] → CategoryTheory.Functor ℕᵒᵖ J
-- Mathlib.Data.ENNReal.Basic
ENNReal.instMin : Min ENNReal
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Param.mk.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (binderName : Lean.Name) (type : Lean.Expr) (borrow : Bool)
  (fvarId_1 : Lean.FVarId) (binderName_1 : Lean.Name) (type_1 : Lean.Expr) (borrow_1 : Bool),
  ({ fvarId := fvarId, binderName := binderName, type := type, borrow := borrow } =
      { fvarId := fvarId_1, binderName := binderName_1, type := type_1, borrow := borrow_1 }) =
    (fvarId = fvarId_1 ∧ binderName = binderName_1 ∧ type = type_1 ∧ borrow = borrow_1)
-- Mathlib.Logic.Equiv.Basic
Function.piCongrLeft'_update : ∀ {α : Sort u_1} {β : Sort u_4} [inst : DecidableEq α] [inst_1 : DecidableEq β] (P : α → Sort u_10) (e : α ≃ β)
  (f : (a : α) → P a) (b : β) (x : P (e.symm b)),
  (Equiv.piCongrLeft' P e) (Function.update f (e.symm b) x) = Function.update ((Equiv.piCongrLeft' P e) f) b x
-- Mathlib.Data.Option.Basic
Option.elim'_update : ∀ {α : Type u_5} {β : Type u_6} [inst : DecidableEq α] (f : β) (g : α → β) (a : α) (x : β),
  Option.elim' f (Function.update g a x) = Function.update (Option.elim' f g) (some a) x
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.equiv_symm : ∀ {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {E' : Type u_7} [inst_4 : Fintype ι']
  [inst_5 : NormedAddCommGroup E'] [inst_6 : InnerProductSpace 𝕜 E'] (b : OrthonormalBasis ι 𝕜 E)
  (b' : OrthonormalBasis ι' 𝕜 E') (e : ι ≃ ι'), (b.equiv b' e).symm = b'.equiv b e.symm
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.w₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C}
  (h_1 : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₂ (CategoryTheory.CategoryStruct.comp f₂ h_1) =
    CategoryTheory.CategoryStruct.comp h.p h_1
-- Mathlib.Algebra.Order.Ring.Abs
_private.Mathlib.Algebra.Order.Ring.Abs.0.geomSum.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.sum_nonneg : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (x : X),
  0 ≤ ∑ᶠ (i : ι), (f i) x
-- Mathlib.ModelTheory.Order
FirstOrder.Language.order.instStrongHomClassOfOrderIsoClass : ∀ {M : Type w'} [inst : FirstOrder.Language.order.Structure M] [inst_1 : LE M]
  [FirstOrder.Language.order.OrderedStructure M] {N : Type u_1} [inst_3 : FirstOrder.Language.order.Structure N]
  [inst_4 : LE N] [FirstOrder.Language.order.OrderedStructure N] {F : Type u_2} [inst_6 : EquivLike F M N]
  [OrderIsoClass F M N], FirstOrder.Language.order.StrongHomClass F M N
-- Init.Data.String.PosRaw
String.Pos.Raw.zero_add_string_eq : ∀ (s : String), 0 + s = { byteIdx := s.utf8ByteSize }
-- Init.Data.Array.Erase
Array.getElem?_eraseIdx_of_lt : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size) {j : ℕ}, j < i → (xs.eraseIdx i h)[j]? = xs[j]?
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.GridLines.T_empty : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i))
  [inst_1 : DecidableEq ι] {p : ℝ} (f : ((i : ι) → A i) → ENNReal) (x : (i : ι) → A i),
  MeasureTheory.GridLines.T μ p f ∅ x = f x ^ (1 + p)
-- Mathlib.Topology.Constructible
/-- [Stacks Tag 09YG](https://stacks.math.columbia.edu/tag/09YG) -/
Topology.IsConstructible.image_of_isClosedEmbedding : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  Topology.IsClosedEmbedding f →
    IsRetrocompact (Set.range f)ᶜ → Topology.IsConstructible s → Topology.IsConstructible (f '' s)
-- Mathlib.Algebra.Order.BigOperators.Group.List
/-- See also `List.single_le_sum`.  -/
List.le_sum_of_mem : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [CanonicallyOrderedAdd M] {xs : List M} {x : M},
  x ∈ xs → x ≤ xs.sum
-- Mathlib.Algebra.BigOperators.Ring.Finset
Int.cast_prod : ∀ {ι : Type u_5} {R : Type u_6} [inst : CommRing R] (f : ι → ℤ) (s : Finset ι), ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_single_ne : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i j : ι} (x : β i),
  i ≠ j → (DFinsupp.erase j fun₀ | i => x) = fun₀ | i => x
-- Mathlib.Data.Nat.ModEq
Nat.add_div_of_dvd_left : ∀ {a b c : ℕ}, c ∣ b → (a + b) / c = a / c + b / c
-- Mathlib.GroupTheory.RegularWreathProduct
IteratedWreathProduct_succ : ∀ (G : Type u) (n : ℕ), IteratedWreathProduct G (n + 1) = IteratedWreathProduct G n ≀ᵣ G
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.normalize_gcd : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α}, normalize (s.gcd f) = s.gcd f
-- Mathlib.Data.Nat.MaxPowDiv
/-- **Alias** of `padicValNat_zero_left`. -/
Nat.maxPowDiv.zero_base : ∀ (n : ℕ), padicValNat 0 n = 0
-- Mathlib.Topology.Order
isOpen_iff_continuous_mem : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, IsOpen s ↔ Continuous fun x => x ∈ s
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.instIsZeroOrProbabilityMeasureMap : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ] {f : α → β},
  MeasureTheory.IsZeroOrProbabilityMeasure (MeasureTheory.Measure.map f μ)
-- Mathlib.Topology.UniformSpace.Equiv
/-- A subset of a uniform space is uniformly isomorphic to its image under a uniform isomorphism.
 -/
UniformEquiv.image : {α : Type u} →
  {β : Type u_1} → [inst : UniformSpace α] → [inst_1 : UniformSpace β] → (e : α ≃ᵤ β) → (s : Set α) → ↑s ≃ᵤ ↑(⇑e '' s)
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instForInProdOfTransCmpOfLawfulMonad : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {m : Type w → Type w₂} →
        [Std.TransCmp cmp] → [inst : Monad m] → [LawfulMonad m] → ForIn m (Std.ExtTreeMap α β cmp) (α × β)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
primitiveRoots_zero : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R], primitiveRoots 0 R = ∅
-- Mathlib.Algebra.Module.Torsion.Basic
Ideal.mem_torsionOf_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M) (a : R),
  a ∈ Ideal.torsionOf R M x ↔ a • x = 0
-- Mathlib.Tactic.FieldSimp
/-- Given two terms `l₁`, `l₂` of type `qNF M`, i.e. lists of `(ℤ × Q($M)) × ℕ`s (an integer, an
`Expr` and a natural number), recursively construct a proof that in the field `$M`, the product of
the "multiplicative linear combinations" represented by `l₁` and `l₂` is the multiplicative linear
combination represented by `FieldSimp.qNF.mul l₁ l₁`.  -/
Mathlib.Tactic.FieldSimp.qNF.mkMulProof : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (l₁ l₂ : Mathlib.Tactic.FieldSimp.qNF M) →
        have a := (l₁.mul l₂).toNF;
        have a_1 := l₂.toNF;
        have a_2 := l₁.toNF;
        Q(«$a_2».eval * «$a_1».eval = «$a».eval)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.length_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Plausible.Testable
Plausible.Configuration.mk : ℕ → ℕ → ℕ → Bool → Bool → Bool → Bool → Option ℕ → Bool → Bool → Plausible.Configuration
-- Lean.Compiler.IR.Basic
/-- RC decrement for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not.
If `persistent == true` then `x` is statically known to be a persistent object.  -/
Lean.IR.FnBody.dec : Lean.IR.VarId → ℕ → Bool → Bool → Lean.IR.FnBody → Lean.IR.FnBody
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiff_one_iff_hasFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  ContDiff 𝕜 1 f ↔ ∃ f', Continuous f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x
-- Mathlib.CategoryTheory.Equivalence
/-- Every equivalence of categories consisting of functors `F` and `G` such that `F ⋙ G` and
`G ⋙ F` are naturally isomorphic to identity functors can be transformed into a half-adjoint
equivalence without changing `F` or `G`.  -/
CategoryTheory.Equivalence.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (G : CategoryTheory.Functor D C) →
            (CategoryTheory.Functor.id C ≅ F.comp G) → (G.comp F ≅ CategoryTheory.Functor.id D) → (C ≌ D)
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.MkHInjTypeResult.us : Lean.Meta.MkHInjTypeResult✝ → List Lean.Level
-- Aesop.Tree.Data
Aesop.Goal.parent : Aesop.Goal → Aesop.MVarClusterRef
-- Lean.Meta.Tactic.Grind.PP
Lean.Meta.Grind.ppExprArray : Lean.Name →
  String → Array Lean.Expr → optParam Lean.Name (Lean.Name.mkSimple "_") → optParam Bool true → Lean.MessageData
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivWithinAt_natCast : ∀ {𝕜 : 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] [inst_7 : NatCast F] (n : ℕ) (x : E) (s : Set E), HasFDerivWithinAt (↑n) 0 s x
-- Mathlib.Algebra.Order.Group.Multiset
/-- `count a`, the multiplicity of `a` in a multiset, promoted to an `AddMonoidHom`.  -/
Multiset.countAddMonoidHom : {α : Type u_1} → [DecidableEq α] → α → Multiset α →+ ℕ
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
conditionallyCompleteLatticeOfLatticeOfsInf.eq_1 : ∀ (α : Type u_5) [H1 : Lattice α] [inst : InfSet α]
  (isLUB_sSup : ∀ (s : Set α), BddBelow s → s.Nonempty → IsGLB s (sInf s)),
  conditionallyCompleteLatticeOfLatticeOfsInf α isLUB_sSup =
    { toLattice := H1, toSupSet := (conditionallyCompleteLatticeOfsInf α ⋯ ⋯ isLUB_sSup).toSupSet,
      toInfSet := (conditionallyCompleteLatticeOfsInf α ⋯ ⋯ isLUB_sSup).toInfSet, isLUB_csSup := ⋯, isGLB_csInf := ⋯ }
-- Init.Data.SInt.Basic
/-- Converts `true` to `1` and `false` to `0`.
 -/
Bool.toISize : Bool → ISize
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.sInf_isNormal : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (s : Set (CategoryTheory.Subgroupoid C)),
  (∀ S ∈ s, S.IsNormal) → (sInf s).IsNormal
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.push.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} (ref : aig.Ref)
  (refs : Vector Std.Sat.AIG.Fanin len) (hrefs : ∀ {i : ℕ} (h : i < len), refs[i].gate < aig.decls.size),
  { refs := refs, hrefs := hrefs }.push ref =
    { refs := refs.push (Std.Sat.AIG.Fanin.mk ref.gate ref.invert), hrefs := ⋯ }
-- Mathlib.Topology.Algebra.Order.Field
/-- If a (possibly non-unital and/or non-associative) ring `R` admits a submultiplicative
nonnegative norm `norm : R → 𝕜`, where `𝕜` is a linear ordered field, and the open balls
`{ x | norm x < ε }`, `ε > 0`, form a basis of neighborhoods of zero, then `R` is a topological
ring.  -/
IsTopologicalRing.of_norm : ∀ {R : Type u_1} {𝕜 : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : Field 𝕜] [inst_2 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_4 : TopologicalSpace R] [IsTopologicalAddGroup R] (norm : R → 𝕜),
  (∀ (x : R), 0 ≤ norm x) →
    (∀ (x y : R), norm (x * y) ≤ norm x * norm y) →
      ((nhds 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}) → IsTopologicalRing R
-- Mathlib.Tactic.DeriveCountable
_private.Mathlib.Tactic.DeriveCountable.0.Mathlib.Deriving.Countable.mkInjThmMatch : Lean.Elab.Deriving.Context → Lean.Elab.Deriving.Header → Lean.InductiveVal → Lean.Elab.TermElabM Lean.Term
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_nat_add : ∀ (f : CircleDeg1Lift) (n : ℕ) (x : ℝ), f (↑n + x) = ↑n + f x
-- Mathlib.Analysis.Normed.Module.DoubleDual
/-- If `S` is bounded set in `WeakSpace X` and the weak-star closure of its image under
the embedding into the weak-star double dual lies in the range of that embedding,
then `closure S` is compact in the weak topology.

This combines Banach–Alaoglu (compactness of bounded weak-star–closed sets) with the topological
embedding `inclusionInDoubleDualWeak_isEmbedding` to transfer compactness back to the weak
topology on `X`.  -/
NormedSpace.isCompact_closure_of_isBounded : ∀ (𝕜 : Type u_3) [inst : RCLike 𝕜] (X : Type u_4) [inst_1 : NormedAddCommGroup X] [inst_2 : NormedSpace 𝕜 X]
  (S : Set (WeakSpace 𝕜 X)),
  Bornology.IsBounded (⇑(toWeakSpace 𝕜 X) ⁻¹' S) →
    closure (⇑(NormedSpace.inclusionInDoubleDualWeak 𝕜 X) '' S) ⊆
        Set.range ⇑(NormedSpace.inclusionInDoubleDualWeak 𝕜 X) →
      IsCompact (closure S)
-- Mathlib.Algebra.Module.FinitePresentation
/-- Let `M` be a finite `R`-module, and `N` be a finitely presented `R`-module.
If `l : M →ₗ[R] N` is a linear map whose localization at `S : Submonoid R` is bijective,
then `l` is already bijective under the localization at some `r ∈ S`.
 -/
exists_bijective_map_powers : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Submonoid R) {M' : Type u_1} [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] (f : M →ₗ[R] M') [inst_7 : IsLocalizedModule S f] {N' : Type u_2} [inst_8 : AddCommGroup N']
  [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] [Module.Finite R M]
  [Module.FinitePresentation R N] (l : M →ₗ[R] N),
  Function.Bijective ⇑((IsLocalizedModule.map S f g) l) →
    ∃ r ∈ S, ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l)
-- Mathlib.LinearAlgebra.Vandermonde
_private.Mathlib.LinearAlgebra.Vandermonde.0.Matrix.det_projVandermonde_of_field : ∀ {K : Type u_2} [inst : Field K] {n : ℕ} (v w : Fin n → K),
  (Matrix.projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.instMaxOfAddLeftMonoOfAddRightMono : {X : Type u_1} →
  {R : Type u_2} →
    [inst : AddZeroClass R] → [inst_1 : SemilatticeSup R] → [AddLeftMono R] → [AddRightMono R] → Max (PseudoMetric X R)
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.map'_succAboveOrderEmb : ∀ {n : ℕ} (i : Fin (n + 2)) (x : Fin (n + 3)), SimplexCategory.II.map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_add_of_degree_lt' : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.degree < p.degree → (p + q).leadingCoeff = p.leadingCoeff
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_of_isEmpty_insertMany : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {ρ : Type w}
  [inst : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {l : ρ},
  (m.insertMany l).isEmpty = true → m.isEmpty = true
-- Init.Data.UInt.Lemmas
USize.toBitVec_zero : USize.toBitVec 0 = 0#System.Platform.numBits
-- Mathlib.Geometry.Manifold.Submersion
/-- A `C^n` submersion at `x` is `C^n` at `x`.  -/
Manifold.IsSubmersionAt.contMDiffAt : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M}, Manifold.IsSubmersionAt I J n f x → ContMDiffAt I J n f x
-- Mathlib.Data.Rat.Floor
Rat.num_lt_succ_floor_mul_den : ∀ (q : ℚ), q.num < (⌊q⌋ + 1) * ↑q.den
-- Mathlib.Topology.Category.TopCommRingCat
/-- carrier of a topological commutative ring.  -/
TopCommRingCat.α : TopCommRingCat → Type u
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_units_conj : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸]
  [CompleteSpace 𝔸] (U : (Matrix m m 𝔸)ˣ) (A : Matrix m m 𝔸),
  NormedSpace.exp (↑U * A * ↑U⁻¹) = ↑U * NormedSpace.exp A * ↑U⁻¹
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.select_isPoly : ∀ {p : ℕ} {P : ℕ → Prop}, WittVector.IsPoly p fun x x_1 x_2 => WittVector.select P x_2
-- Mathlib.NumberTheory.Dioph
IsPoly.sub : ∀ {α : Type u_1} {f g : (α → ℕ) → ℤ}, IsPoly f → IsPoly g → IsPoly fun x => f x - g x
-- Mathlib.Order.Booleanisation
Booleanisation.LT.comp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α},
  a < b → (Booleanisation.comp b).LT (Booleanisation.comp a)
-- Mathlib.Topology.Order.LeftRightLim
Antitone.le_leftLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f → ∀ {x y : α}, x ≤ y → f y ≤ Function.leftLim f x
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)}
  (h : (F.map f).toFunctor.obj ((F.map (CategoryTheory.CategoryStruct.id a)).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).inv.toNatTrans.app X)) h =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X) h)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mem_mk : ∀ {α : Type u_1} [inst : LE α] {s : Set α} (hs : IsUpperSet s) {a : α}, a ∈ { carrier := s, upper' := hs } ↔ a ∈ s
-- Mathlib.Algebra.Order.Group.Indicator
Set.le_mulIndicator_apply : ∀ {α : Type u_2} {M : Type u_3} [inst : LE M] [inst_1 : One M] {s : Set α} {g : α → M} {a : α} {y : M},
  (a ∈ s → y ≤ g a) → (a ∉ s → y ≤ 1) → y ≤ s.mulIndicator g a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.copy_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {Q' H' : C} (eQ : Q' ≅ h.Q) (eH : H' ≅ h.H),
  (h.copy eQ eH).ι = CategoryTheory.CategoryStruct.comp eH.hom (CategoryTheory.CategoryStruct.comp h.ι eQ.inv)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.modular_S_smul : ∀ (z : UpperHalfPlane), ModularGroup.S • z = { coe := (-↑z)⁻¹, coe_im_pos := ⋯ }