mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.orderIsoOfPrime_symm_apply_coe : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (p : { p // p.IsPrime ∧ Disjoint ↑M ↑p }),
  ↑((RelIso.symm (IsLocalization.orderIsoOfPrime M S)) p) = Ideal.map (algebraMap R S) ↑p
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.dgoEquivHomologicalComplex_inverse : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.dgoEquivHomologicalComplex b V).inverse = HomologicalComplex.homologicalComplexToDGO b V
-- Lean.Data.PPContext
Lean.PPContext.env : Lean.PPContext → Lean.Environment
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.coe_comp : ∀ {M N K : SemiNormedGrp} (f : M ⟶ N) (g : N ⟶ K),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Data.Int.Init
/-- Inductively define a function on `ℤ` by defining it on `ℕ` and extending it from `n` to `-n`.  -/
Int.negInduction : {motive : ℤ → Sort u_1} → ((n : ℕ) → motive ↑n) → (((n : ℕ) → motive ↑n) → (n : ℕ) → motive (-↑n)) → (n : ℤ) → motive n
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.toEquiv_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N), ↑f.symm = (↑f).symm
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_toRingHom_comp_toRingHom : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (e : R ≃+* S),
  e.symm.toRingHom.comp e.toRingHom = RingHom.id R
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.coeFnAddMonoidHom_apply : ∀ {𝕜 : 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) (G : Type u_4)
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (a : LeftInvariantDerivation I G) (a_1 : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤),
  (LeftInvariantDerivation.coeFnAddMonoidHom I G) a a_1 = a a_1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_insertEntry_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
  {fallback v : β k}, Std.Internal.List.getValueCastD k (Std.Internal.List.insertEntry k v l) fallback = v
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.ElementarilyEquivalent.trans : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.Structure P], L.ElementarilyEquivalent M N → L.ElementarilyEquivalent N P → L.ElementarilyEquivalent M P
-- Lean.Elab.InfoTree.Types
Lean.Elab.TermInfo.mk.inj : ∀ {toElabInfo : Lean.Elab.ElabInfo} {lctx : Lean.LocalContext} {expectedType? : Option Lean.Expr} {expr : Lean.Expr}
  {isBinder isDisplayableTerm : Bool} {toElabInfo_1 : Lean.Elab.ElabInfo} {lctx_1 : Lean.LocalContext}
  {expectedType?_1 : Option Lean.Expr} {expr_1 : Lean.Expr} {isBinder_1 isDisplayableTerm_1 : Bool},
  { toElabInfo := toElabInfo, lctx := lctx, expectedType? := expectedType?, expr := expr, isBinder := isBinder,
        isDisplayableTerm := isDisplayableTerm } =
      { toElabInfo := toElabInfo_1, lctx := lctx_1, expectedType? := expectedType?_1, expr := expr_1,
        isBinder := isBinder_1, isDisplayableTerm := isDisplayableTerm_1 } →
    toElabInfo = toElabInfo_1 ∧
      lctx = lctx_1 ∧
        expectedType? = expectedType?_1 ∧
          expr = expr_1 ∧ isBinder = isBinder_1 ∧ isDisplayableTerm = isDisplayableTerm_1
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
AddMonoidAlgebra.instCoalgebra : (R : Type u_1) →
  [inst : CommSemiring R] →
    (A : Type u_2) →
      [inst_1 : Semiring A] →
        (X : Type u_3) → [inst_2 : Module R A] → [Coalgebra R A] → Coalgebra R (AddMonoidAlgebra A X)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.instFullChangeProp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {P P' : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} (hP : P ≤ P')
  [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative],
  (CategoryTheory.MorphismProperty.Comma.changeProp L R hP ⋯ ⋯).Full
-- Lean.Parser.Extension
Lean.Parser.parserAttributeHooks : IO.Ref (List Lean.Parser.ParserAttributeHook)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- Preimage of interior or interior of preimage coincide for open partial homeomorphisms,
when restricted to the source.  -/
OpenPartialHomeomorph.preimage_interior : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set Y), e.source ∩ ↑e ⁻¹' interior s = e.source ∩ interior (↑e ⁻¹' s)
-- Mathlib.Data.Matrix.Basic
Matrix.diagonal_pow : ∀ {n : Type u_3} {α : Type u_11} [inst : Semiring α] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (v : n → α) (k : ℕ),
  Matrix.diagonal v ^ k = Matrix.diagonal (v ^ k)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (m.alter k f)[k']? = if (k == k') = true then f m[k]? else m[k']?
-- Mathlib.Order.LiminfLimsup
/-- In a complete lattice, the limsup of a function is the infimum over sets `s` in the filter
of the supremum of the function over `s`  -/
Filter.limsup_eq_iInf_iSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {u : β → α},
  Filter.limsup u f = ⨅ s ∈ f, ⨆ a ∈ s, u a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.diff_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.diff t₂ = t₁ \ t₂
-- Mathlib.MeasureTheory.Constructions.Projective
MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder_of_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {I J : Finset ι},
  MeasureTheory.IsProjectiveMeasureFamily P →
    ∀ {S : Set ((i : ↥I) → α ↑i)} {T : Set ((i : ↥J) → α ↑i)},
      MeasurableSet T → MeasureTheory.cylinder I S = MeasureTheory.cylinder J T → J ⊆ I → (P I) S = (P J) T
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.isStableUnderRetracts_iff_retracts_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.IsStableUnderRetracts ↔ P.retracts ≤ P
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.MemLp.mul_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_3}
  [inst : NormedRing 𝕜] {f : α → 𝕜}, MeasureTheory.MemLp f p μ → ∀ (c : 𝕜), MeasureTheory.MemLp (fun x => f x * c) p μ
-- Mathlib.Analysis.Normed.Algebra.Spectrum
quasispectrum.isCompact : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {B : Type u_3} [inst_1 : NonUnitalNormedRing B] [inst_2 : NormedSpace 𝕜 B]
  [CompleteSpace B] [IsScalarTower 𝕜 B B] [SMulCommClass 𝕜 B B] [ProperSpace 𝕜] (a : B), IsCompact (quasispectrum 𝕜 a)
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
/-- **Alias** of the reverse direction of `ContinuousLinearMapWOT.continuousWithinAt_iff`. -/
ContinuousLinearMapWOT.continuousWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} [inst_7 : TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α} {a : α},
  (∀ (x : E) (y : F), ContinuousWithinAt (fun x_1 => inner 𝕜 y ((f x_1) x)) s a) → ContinuousWithinAt f s a
-- Mathlib.RepresentationTheory.Basic
Representation.instAddCommMonoidAsModule : {k : Type u_2} →
  {G : Type u_3} →
    {V : Type u_1} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → (x : Representation k G V) → AddCommMonoid x.asModule
-- Init.Data.String.Lemmas.Iterate
/-- A list of all positions starting at `p`.

This function is not meant to be used in actual programs. Actual programs should use
`Slice.positionsFrom` or `Slice.positions`.
 -/
String.Slice.Model.positionsFrom : {s : String.Slice} → s.Pos → List { p // p ≠ s.endPos }
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.incl.inj : ∀ {R : Type u} {x x_1 : R}, Rack.PreEnvelGroup.incl x = Rack.PreEnvelGroup.incl x_1 → x = x_1
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isUnit_iff_isRegular : ∀ {R : Type u_1} [inst : Semiring R] [IsArtinianRing R] {x : R}, IsUnit x ↔ IsRegular x
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- **Alias** of `FourierTransform.fourierCLE`. -/
SchwartzMap.fourierTransformCLE : (R : Type u_5) →
  (E : Type u_6) →
    {F : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : AddCommMonoid F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] →
                [inst_5 : FourierTransform E F] →
                  [FourierAdd E F] →
                    [FourierSMul R E F] →
                      [inst_8 : FourierTransformInv F E] →
                        [FourierPair E F] →
                          [FourierInvPair F E] →
                            [inst_11 : TopologicalSpace E] →
                              [inst_12 : TopologicalSpace F] →
                                [ContinuousFourier E F] → [ContinuousFourierInv F E] → E ≃L[R] F
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The forgetful functor mapping an arrow to its domain.  -/
CategoryTheory.Over.forget : {T : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} T] → (X : T) → CategoryTheory.Functor (CategoryTheory.Over X) T
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.Functor.toReflPrefunctor_toPrefunctor : ∀ {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑C ↑D),
  F.toReflPrefunctor.toPrefunctor = F.toPrefunctor
-- Mathlib.NumberTheory.Ostrowski
_private.Mathlib.NumberTheory.Ostrowski.0.Rat.AbsoluteValue.eq_of_eq_pow : ∀ {f : AbsoluteValue ℚ ℝ} {m n : ℕ},
  1 < m → 1 < n → (¬∀ (n : ℕ), f ↑n ≤ 1) → ∀ {s t : ℝ}, f ↑m = ↑m ^ s → f ↑n = ↑n ^ t → s = t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α}
  (k_eq : cmp k k' = Ordering.eq) {v : β k},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l → ⟨k, v⟩ ∈ l → (t.insertMany l).get? k' = some (cast ⋯ v)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- A non-unital subsemiring of a `NonUnitalCommSemiring` is a `NonUnitalCommSemiring`.  -/
NonUnitalSubsemiringClass.toNonUnitalCommSemiring : {S : Type v} →
  (s : S) →
    {R : Type u_1} →
      [inst : NonUnitalCommSemiring R] →
        [inst_1 : SetLike S R] → [NonUnitalSubsemiringClass S R] → NonUnitalCommSemiring ↥s
-- Init.Data.Order.PackageFactories
Std.instDecidableLT : {α : Type u_1} → [inst : Std.PreorderPackage α] → DecidableLT α
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Make all names with prefix `n₁` related to names with prefix `n₂`.  -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.DirectoryDependency.NamePrefixRel.insert : Mathlib.Linter.DirectoryDependency.NamePrefixRel✝ →
  Lean.Name → Lean.Name → Mathlib.Linter.DirectoryDependency.NamePrefixRel✝
-- Mathlib.Algebra.Torsor.Basic
vsub_right_cancel_iff : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ p : P}, p -ᵥ p₁ = p -ᵥ p₂ ↔ p₁ = p₂
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
/-- Dependent sum of an `n`-ary functor. The sum can range over
data types like `ℕ` or over `Type.{u-1}`  -/
MvQPF.Sigma : {n : ℕ} → {A : Type u} → (A → TypeVec.{u} n → Type u) → TypeVec.{u} n → Type u
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- `AdicCompletion I R` is a subring of `∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)`.  -/
AdicCompletion.subring : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → Subring ((n : ℕ) → R ⧸ I ^ n • ⊤)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryGT!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited ((a : α) × β a)],
          Std.DTreeMap.Internal.Impl.getEntryGT! k t₁ = Std.DTreeMap.Internal.Impl.getEntryGT! k t₂
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.prod_map_le_prod_map : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [MulLeftMono α] {s : Multiset ι}
  (f g : ι → α), (∀ i ∈ s, f i ≤ g i) → (Multiset.map f s).prod ≤ (Multiset.map g s).prod
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_le_one_iff_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν]
  [MeasureTheory.SigmaFinite ν], μ.AbsolutelyContinuous ν → (μ.rnDeriv ν ≤ᵐ[ν] 1 ↔ μ ≤ ν)
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_ofIntLE : ∀ {n : ℤ} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt),
  (Int16.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_Iic_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (i : α),
  ((Cardinal.mk α).ord = Ordinal.type fun x1 x2 => x1 < x2) →
    Cardinal.aleph0 ≤ Cardinal.mk α → Cardinal.mk ↑(Set.Iic i) < Cardinal.mk α
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
_private.Mathlib.Analysis.InnerProductSpace.ExteriorPower.0.exteriorPower.innerProductForm_ιMulti_family_of_orthonormal : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2}
  [inst_2 : LinearOrder ι] {v : ι → E},
  Orthonormal ℝ v →
    ∀ (s t : ↑(Set.powersetCard ι n)),
      (exteriorPower.innerProductForm✝ (exteriorPower.ιMulti_family ℝ n v s)) (exteriorPower.ιMulti_family ℝ n v t) =
        if s = t then 1 else 0
-- Mathlib.Data.Matrix.Basis
Matrix.subsemigroupCenter_eq_scalar_map : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Semiring α],
  Subsemigroup.center (Matrix n n α) = Subsemigroup.map (↑↑(Matrix.scalar n)) (Subsemigroup.center α)
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- The maximal atlas of a structure groupoid is stable under equivalence.  -/
StructureGroupoid.mem_maximalAtlas_of_eqOnSource : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {e e' : OpenPartialHomeomorph M H},
  e' ≈ e → e ∈ StructureGroupoid.maximalAtlas M G → e' ∈ StructureGroupoid.maximalAtlas M G
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- The three points of a cospherical set are affinely independent.  -/
EuclideanGeometry.Cospherical.affineIndependent_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.Cospherical {p₁, p₂, p₃} → p₁ ≠ p₂ → p₁ ≠ p₃ → p₂ ≠ p₃ → AffineIndependent ℝ ![p₁, p₂, p₃]
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.of_isEmbedding_isClosedMap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsEmbedding f → IsClosedMap f → Topology.IsClosedEmbedding f
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
/-- index of the inductive datatype of the argument we are recursing on.
If `< indAll.all`, a normal data type, else an auxiliary data type due to nested recursion
 -/
Lean.Elab.Structural.RecArgInfo.indIdx : Lean.Elab.Structural.RecArgInfo → ℕ
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swapEquiv_inverse_map_hom_toFun : ∀ {X Y : TwoP} (f : X ⟶ Y) (a : X.toBipointed.X),
  (TwoP.swapEquiv.inverse.map f).hom.toFun a = (CategoryTheory.ConcreteCategory.hom f.hom) a
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.edist_eval_le : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : PseudoEMetricSpace β] [inst_1 : Finite ↑𝔖]
  {f g : UniformOnFun α β 𝔖} {x : α},
  x ∈ ⋃₀ 𝔖 → edist ((UniformOnFun.toFun 𝔖) f x) ((UniformOnFun.toFun 𝔖) g x) ≤ edist f g
-- Mathlib.RingTheory.Flat.Basic
/-- An `R`-module linearly equivalent to a flat `R`-module is flat.  -/
Module.Flat.of_linearEquiv : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [Module.Flat R M] (e : N ≃ₗ[R] M), Module.Flat R N
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csSup_one : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : One M], sSup 1 = 1
-- Init.Data.Array.Lemmas
Array.filter_eq_self : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, Array.filter p xs = xs ↔ ∀ a ∈ xs, p a = true
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (i : Set α),
  MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i 0 = MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s (i \ ∅)
-- Mathlib.Data.Finsupp.Basic
/-- Extend the domain of a `Finsupp` by using `0` where `P x` does not hold.  -/
Finsupp.extendDomain : {α : Type u_1} → {M : Type u_12} → [inst : Zero M] → {P : α → Prop} → [DecidablePred P] → (Subtype P →₀ M) → α →₀ M
-- Mathlib.Tactic.Linter.UnusedTacticExtension
/-- `addAllowedUnusedTactic stxNodes` takes as input a `HashSet` of `SyntaxNodeKind`s and extends the
`allowedUnusedTacticExt` environment extension with its content.

These are tactics that the unused tactic linter will ignore, since they are expected to not change
the tactic state.

See the `#allow_unused_tactic! ids` command for dynamically extending the extension as a user-facing
command.
 -/
_private.Mathlib.Tactic.Linter.UnusedTacticExtension.0.Mathlib.Linter.UnusedTactic.addAllowedUnusedTactic : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Std.HashSet Lean.SyntaxNodeKind → m Unit
-- Mathlib.Order.OmegaCompletePartialOrder
/-- A monotone function `f : α →o β` is ωScott continuous if and only if it distributes over ωSup.  -/
OmegaCompletePartialOrder.ωScottContinuous_iff_map_ωSup_of_orderHom : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  {f : α →o β},
  OmegaCompletePartialOrder.ωScottContinuous ⇑f ↔
    ∀ (c : OmegaCompletePartialOrder.Chain α),
      f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map f)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pushforwardIsoBind_hom_s₀_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X)
  (a : (CategoryTheory.PreZeroHypercover.pushforward f E).I₀),
  ((CategoryTheory.PreZeroHypercover.pushforwardIsoBind f E).hom.s₀ a).snd = a
-- Lean.Meta.InferType
/-- Visit an application without beta reducing the head  -/
_private.Lean.Meta.InferType.0.Lean.Expr.instantiateBetaRevRange.visitApp : ℕ →
  ℕ →
    Array Lean.Expr →
      Lean.Expr → Lean.Expr → Lean.Expr → ℕ → Lean.MonadStateCacheT (Lean.ExprStructEq × ℕ) Lean.Expr Id Lean.Expr
-- Lean.Expr
/-- Metadata (aka annotations).

We use annotations to provide hints to the pretty-printer,
store references to `Syntax` nodes, position information, and save information for
elaboration procedures (e.g., we use the `inaccessible` annotation during elaboration to
mark `Expr`s that correspond to inaccessible patterns).

Note that `Expr.mdata data e` is definitionally equal to `e`.
 -/
Lean.Expr.mdata : Lean.MData → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.isCoprime_expand : ∀ {R : Type u} [inst : CommSemiring R] {f g : Polynomial R} {p : ℕ},
  p ≠ 0 → (IsCoprime ((Polynomial.expand R p) f) ((Polynomial.expand R p) g) ↔ IsCoprime f g)
-- Lean.Parser.Level
Lean.Parser.Level.addLit : Lean.Parser.TrailingParser
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.toGHSpace.eq_1 : ∀ (X : Type u) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X],
  GromovHausdorff.toGHSpace X = ⟦NonemptyCompacts.kuratowskiEmbedding X⟧
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- A bilinear map is left-separating if and only if it has a trivial kernel.  -/
LinearMap.separatingLeft_iff_ker_eq_bot : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M}, B.SeparatingLeft ↔ B.ker = ⊥
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- A topological space is completely pseudometrizable if there exists a pseudometric space
structure compatible with the topology which makes the space complete.
To endow such a space with a compatible distance, use
`letI := upgradeIsCompletelyPseudoMetrizable X`.  -/
TopologicalSpace.IsCompletelyPseudoMetrizableSpace : (X : Type u_3) → [t : TopologicalSpace X] → Prop
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, a ∈ t → t.getKey? a = some (t.getKeyD a fallback)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_append_toArray_roc : ∀ {l m n : ℕ}, l ≤ m → m ≤ n → (l<...=m).toArray ++ (m<...=n).toArray = (l<...=n).toArray
-- Mathlib.Algebra.Category.ModuleCat.Localization
ModuleCat.localizedModuleFunctor.congr_simp : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (S : Submonoid R),
  ModuleCat.localizedModuleFunctor S = ModuleCat.localizedModuleFunctor S
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.coe_iInf : ∀ {M : Type u_1} [inst : Mul M] {ι : Sort u_3} {S : ι → Subsemigroup M}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_cons : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (x : M) (f : Fin n → M), ∏ i, Fin.cons x f i = x * ∏ i, f i
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod'_ε_fst : ∀ {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] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C E) [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal],
  (CategoryTheory.Functor.LaxMonoidal.ε (F.prod' G)).1 = CategoryTheory.Functor.LaxMonoidal.ε F
-- Std.Internal.UV.System
Std.Internal.UV.System.instReprUnameInfo : Repr Std.Internal.UV.System.UnameInfo
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.throwTooManyScopeComponents : Lean.Name → List Lean.Elab.Command.Scope → Lean.Elab.Command.CommandElabM Unit
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm : ∀ {w : ℕ} (a b : BitVec w), (~~~a == b) = (a == ~~~b)
-- Mathlib.Data.List.Sublists
List.sublistsLen_zero : ∀ {α : Type u} (l : List α), List.sublistsLen 0 l = [[]]