mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Skeletal
/-- A functor `C ⥤ D` computably lowers to a functor `ThinSkeleton C ⥤ ThinSkeleton D`.  -/
CategoryTheory.ThinSkeleton.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.Functor (CategoryTheory.ThinSkeleton C) (CategoryTheory.ThinSkeleton D)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicValued_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {x : K},
  Valued.v x = (IsDedekindDomain.HeightOneSpectrum.valuation K v) x
-- Mathlib.Algebra.Ring.Defs
/-- A typeclass stating that multiplication is right distributive over addition.  -/
RightDistribClass : (R : Type u_1) → [Mul R] → [Add R] → Prop
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.algebraMap_surjective_of_isIdempotentElem : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (e : R),
  IsIdempotentElem e → ∀ [IsLocalization.Away e S], Function.Surjective ⇑(algebraMap R S)
-- Mathlib.Algebra.Group.Finsupp
Finsupp.coe_sub : ∀ {ι : Type u_1} {G : Type u_6} [inst : SubNegZeroMonoid G] (g₁ g₂ : ι →₀ G), ⇑(g₁ - g₂) = ⇑g₁ - ⇑g₂
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
/-- Unfold one scalar Bird recurrence step to the entry-wise formula.  -/
BirdDet.stepEntry_eq : ∀ {R : Type u_1} [inst : CommRing R] (n : ℕ) (A : Array R) (F : ℕ → ℕ → R) (i j : ℕ),
  BirdDet.stepEntry n A F i j =
    (-BirdDet.sumFrom n (i + 1) fun k => F k k) * BirdDet.get n A i j +
      BirdDet.sumFrom n (i + 1) fun k => F i k * BirdDet.get n A k j
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.mk₀_eq_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {M N : C} (f : M ⟶ N), CategoryTheory.Abelian.Ext.mk₀ f = 0 ↔ f = 0
-- Mathlib.Topology.QuasiSeparated
/-- A subset `s` of a topological space is quasi-separated if the intersections of any pairs of
compact open subsets of `s` are still compact.

Note that this is equivalent to `s` being a `QuasiSeparatedSpace` only when `s` is open.  -/
IsQuasiSeparated : {α : Type u_1} → [TopologicalSpace α] → Set α → Prop
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inlRingHom_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A] (r : R),
  (Unitization.inlRingHom R A) r = Unitization.inl r
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.map_ofFixingAddSubgroupUnion_def : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α}
  (x : ↥(SubAddAction.ofFixingAddSubgroup M (s ∪ t))), ↑↑((SubAddAction.map_ofFixingAddSubgroupUnion M s t) x) = ↑x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.shift_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n a : ℤ), CochainComplex.HomComplex.Cochain.shift 0 a = 0
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.Derives.eq_or_head : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u w : List (Symbol T g.NT)},
  g.Derives u w → u = w ∨ ∃ v, g.Produces u v ∧ g.Derives v w
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal_filter_le_fst_of_le : ∀ {n k : ℕ},
  k ≤ n →
    {a ∈ Finset.HasAntidiagonal.antidiagonal n | k ≤ a.1} =
      Finset.map ({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Function.Embedding.refl ℕ))
        (Finset.HasAntidiagonal.antidiagonal (n - k))
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.to_nil : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  t.Bounded o₁ o₂ → Ordnode.nil.Bounded o₁ o₂
-- Mathlib.Order.Hom.Basic
OrderHom.instPartialOrder : {α : Type u_2} → [inst : Preorder α] → {β : Type u_6} → [inst_1 : PartialOrder β] → PartialOrder (α →o β)
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.factor_comp_apply : ∀ {R : Type u} [inst : Ring R] {S T U : Ideal R} [inst_1 : S.IsTwoSided] [inst_2 : T.IsTwoSided] [inst_3 : U.IsTwoSided]
  (H1 : S ≤ T) (H2 : T ≤ U) (x : R ⧸ S),
  (Ideal.Quotient.factor H2) ((Ideal.Quotient.factor H1) x) = (Ideal.Quotient.factor ⋯) x
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_algebraMap : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Finite R S] [Module.Flat R S]
  (x : PrimeSpectrum R),
  AlgebraicGeometry.Scheme.Hom.finrank (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) x =
    Module.rankAtStalk S x
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
/-- [Kerodon Tag 01BJ](https://kerodon.net/tag/01BJ) -/
SSet.quasicategory_of_innerFibration : ∀ {X Y : SSet} (p : X ⟶ Y) [SSet.InnerFibration p] [hY : Y.Quasicategory], X.Quasicategory
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- A monotone function remains monotone when composed with the partial application
of a covariant operator. E.g., `∀ (m : ℕ), Monotone f → Monotone (fun n ↦ f (m + n))`.  -/
Monotone.covariant_of_const : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {α : Type u_3} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α}
  [CovariantClass M N μ fun x1 x2 => x1 ≤ x2], Monotone f → ∀ (m : M), Monotone fun x => f (μ m x)
-- Lean.Parser.Attr
Lean.Parser.Attr.recursor.formatter : Lean.PrettyPrinter.Formatter
-- Std.Sync.Notify
Std.Notify.state : Std.Notify → Std.Mutex Std.Notify.State
-- Mathlib.Data.PFun
PFun.get_prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β)
  (h : (f.prodMap g x).Dom), (f.prodMap g x).get h = ((f x.1).get ⋯, (g x.2).get ⋯)
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.submodule_ne_top : ∀ {R : Type u} {M : Type v} {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  [self : Module.FaithfullyFlat R M] ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
-- Init.Data.String.Basic
String.str_sliceTo : ∀ {s : String} {p : s.Pos}, (s.sliceTo p).str = s
-- Init.Data.UInt.Lemmas
USize.toNat_toUInt32 : ∀ (x : USize), x.toUInt32.toNat = x.toNat % 2 ^ 32
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_inter!_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false →
          Std.DTreeMap.Internal.Impl.Const.getD (m₁.inter! m₂) k fallback = fallback
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub_nsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - ↑m
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instSupSet.eq_1 : ∀ {E : Type u_3} [inst : Group E],
  GroupSeminorm.instSupSet =
    {
      sSup := fun s =>
        if h : BddAbove s then { toFun := fun x => ⨆ p, ↑p x, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } else 0 }
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isBase_iff_indep_closure_eq : ∀ {α : Type u_2} {M : Matroid α} {B : Set α}, M.IsBase B ↔ M.Indep B ∧ M.closure B = M.E
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`.  -/
ContinuousMulEquiv.symm_apply_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N) (x : M), e.symm (e x) = x
-- Mathlib.MeasureTheory.Measure.ResolventTransform
MeasureTheory.resolventTransform_apply : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : NormedAlgebra 𝕜 A] {m𝕜 : MeasurableSpace 𝕜} (μ : MeasureTheory.Measure 𝕜) (a : A),
  MeasureTheory.resolventTransform μ a = ∫ (x : 𝕜), resolvent a x ∂μ
-- Mathlib.Topology.Partial
pcontinuous_iff' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X →. Y},
  PContinuous f ↔ ∀ {x : X} {y : Y}, y ∈ f x → Filter.PTendsto' f (nhds x) (nhds y)
-- Lean.Data.Json.Basic
Lean.Json.brecOn_2.go : {motive_1 : Lean.Json → Sort u} →
  {motive_2 : Array Lean.Json → Sort u} →
    {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} →
      {motive_4 : List Lean.Json → Sort u} →
        {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u} →
          {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u} →
            (t : Std.TreeMap.Raw String Lean.Json compare) →
              ((t : Lean.Json) → t.below → motive_1 t) →
                ((t : Array Lean.Json) → Lean.Json.below_1 t → motive_2 t) →
                  ((t : Std.TreeMap.Raw String Lean.Json compare) → Lean.Json.below_2 t → motive_3 t) →
                    ((t : List Lean.Json) → Lean.Json.below_3 t → motive_4 t) →
                      ((t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) → Lean.Json.below_4 t → motive_5 t) →
                        ((t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) →
                            Lean.Json.below_5 t → motive_6 t) →
                          motive_3 t ×' Lean.Json.below_2 t
-- Lean.DocString.Parser
/-- The indentation of list indicators.  -/
Lean.Doc.Parser.InList.indentation : Lean.Doc.Parser.InList → ℕ
-- Mathlib.Data.Set.Lattice
Set.sUnion_empty : ∀ {α : Type u_1}, ⋃₀ ∅ = ∅
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.image_eq_preimage_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α),
  ⇑e '' s = ⇑e.symm ⁻¹' s
-- Mathlib.Analysis.CStarAlgebra.Spectrum
IsSelfAdjoint.spectralRadius_eq_nnnorm : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a : A}, IsSelfAdjoint a → spectralRadius ℂ a = ↑‖a‖₊
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- Two edges `f` and `g` are right homotopic if there is a `CompStruct` with
(0, 1)-edge `Edge.id`, (1, 2)-edge `f`, and (0, 2)-edge `g`. We use `Nonempty` to
have a `Prop` valued `HomotopicR`.
 -/
SSet.Truncated.HomotopicR : {X : SSet.Truncated 2} →
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })} →
    SSet.Truncated.Edge x y → SSet.Truncated.Edge x y → Prop
-- Mathlib.Data.EReal.Basic
/-- `x.toENNReal` returns `x` if it is nonnegative, `0` otherwise.  -/
EReal.toENNReal : EReal → ENNReal
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
/-- Left whiskering of a lax natural transformation and a modification.  -/
CategoryTheory.Oplax.LaxTrans.whiskerLeft : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.OplaxFunctor B C} →
          (η : F ⟶ G) →
            {θ ι : G ⟶ H} → (θ ⟶ ι) → (CategoryTheory.CategoryStruct.comp η θ ⟶ CategoryTheory.CategoryStruct.comp η ι)
-- Mathlib.Analysis.Matrix.Normed
/-- Normed group instance (using sup norm of L1 norm) for matrices over a normed ring.  Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.linftyOpNormedAddCommGroup : {m : Type u_3} →
  {n : Type u_4} →
    {α : Type u_5} → [Fintype m] → [Fintype n] → [NormedAddCommGroup α] → NormedAddCommGroup (Matrix m n α)
-- Mathlib.RingTheory.PowerSeries.Restricted
_private.Mathlib.RingTheory.PowerSeries.Restricted.0.PowerSeries.isRestricted_comp_uniqueEquiv : ∀ {R : Type u_1} [inst : NormedRing R] (c : ℝ) (f : PowerSeries R),
  (fun t => ‖(MvPowerSeries.coeff t) f‖ * t.prod fun x x_1 => c ^ x_1) =
    (fun n => ‖(PowerSeries.coeff n) f‖ * c ^ n) ∘ ⇑(Finsupp.uniqueEquiv ())
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if `M` is flat,
if any two elements of `↥(M ⊓ N)` are commutative, then the rank of `↥(M ⊓ N)` is at most one.  -/
Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N → ∀ [Module.Flat R ↥M], (∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n) → Module.rank R ↥(M ⊓ N) ≤ 1
-- Init.Data.Int.Order
Int.mul_lt_mul_of_pos_right : ∀ {a b c : ℤ}, a < b → 0 < c → a * c < b * c
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_pos_iff_of_pos_left : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [PosMulStrictMono α] [PosMulReflectLT α],
  0 < a → (0 < a * b ↔ 0 < b)
-- Mathlib.ModelTheory.LanguageMap
/-- The composition of equivalences of first-order languages.  -/
FirstOrder.Language.LEquiv.trans : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} → {L'' : FirstOrder.Language} → (L ≃ᴸ L') → (L' ≃ᴸ L'') → (L ≃ᴸ L'')
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.ofQuotientStabilizer_mem_orbit : ∀ (G : Type u) {X : Type v} [inst : Group G] [inst_1 : MulAction G X] (x : X) (g : G ⧸ MulAction.stabilizer G x),
  MulAction.ofQuotientStabilizer G x g ∈ MulAction.orbit G x
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.rightQuotientEquiv.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : AddSubgroup.IsComplement (↑H) T),
  hT.rightQuotientEquiv = (Equiv.ofBijective (T.domRestrict Quotient.mk'') ⋯).symm
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_const : ∀ {b : ENNReal}, b ≠ 0 → b ≠ ⊤ → (ExpGrowth.expGrowthInf fun x => b) = 0
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- If `u'` is a quasi-inverse of `u` and `w` is a quasi-inverse of `v ∘ₗ u`, then
`u ∘ₗ w` is a quasi-inverse of `v`.  -/
LinearMap.IsQuasiInverse.of_comp_left : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V]
  [inst_2 : Module K V] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : AddCommGroup V₃]
  [inst_6 : Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {u' : V₂ →ₗ[K] V} {w : V₃ →ₗ[K] V},
  u'.IsQuasiInverse u → w.IsQuasiInverse (v ∘ₗ u) → (u ∘ₗ w).IsQuasiInverse v
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C}
  {e e' : F.CorepresentableBy X},
  e = e' ↔ e.homEquiv (CategoryTheory.CategoryStruct.id X) = e'.homEquiv (CategoryTheory.CategoryStruct.id X)
-- Lean.Parser.Term
/-- `leftact% f a b` elaborates `f a b` as a left action using the type propagation protocol in `Lean.Elab.Extra`.
In particular, it is like a unary operation with a fixed parameter `a`, where only the right argument `b` participates in the operator coercion elaborator.  -/
Lean.Parser.Term.leftact : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_surjective : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : AddCommMonoid R] [Nonempty n],
  Function.Surjective Matrix.trace
-- Mathlib.Topology.UniformSpace.Closeds
Filter.HasBasis.uniformity_hausdorff : ∀ {α : Type u_1} [inst : UniformSpace α] {ι : Sort u_4} {p : ι → Prop} {s : ι → Set (α × α)},
  (uniformity α).HasBasis p s → (uniformity (Set α)).HasBasis p (hausdorffEntourage ∘ s)
-- Mathlib.Order.Filter.CountableSeparatingOn
HasCountableSeparatingOn.mono : ∀ {α : Type u_1} {p₁ p₂ : Set α → Prop} {t₁ t₂ : Set α} [h : HasCountableSeparatingOn α p₁ t₁],
  (∀ (s : Set α), p₁ s → p₂ s) → t₂ ⊆ t₁ → HasCountableSeparatingOn α p₂ t₂
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- An disequality `a ≠ b` coming from the core. That is, `(a = b) = False` in the core.
`p₁` and `p₂` are the polynomials corresponding to `a` and `b`.
 -/
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core : Lean.Expr →
  Lean.Expr → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.congr_map : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : U ⥤q V) {X Y : U} {f g : X ⟶ Y},
  f = g → F.map f = F.map g
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.addParams : Lean.IR.LocalContext → Array Lean.IR.Param → Lean.IR.LocalContext
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, k ∈ Std.TreeMap.map f t ↔ k ∈ t
-- Init.Data.Array.MapIdx
Array.mapIdx_eq_mapIdx_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f g : ℕ → α → α_1} {xs : Array α},
  Array.mapIdx f xs = Array.mapIdx g xs ↔ ∀ (i : ℕ) (h : i < xs.size), f i xs[i] = g i xs[i]
-- Init.Data.List.Lemmas
List.cons_eq_flatten_iff : ∀ {α : Type u_1} {xs : List (List α)} {y : α} {ys : List α},
  y :: ys = xs.flatten ↔ ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ l ∈ as, l = []) ∧ ys = bs ++ cs.flatten
-- Mathlib.Tactic.Linter.UnusedTactic
/-- The monad for collecting the ranges of the syntaxes that do not modify any goal.  -/
_private.Mathlib.Tactic.Linter.UnusedTactic.0.Mathlib.Linter.UnusedTactic.M : Type → Type
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.symm_apply_lt : ∀ {R : Type u_6} {S : Type u_7} [inst : Mul R] [inst_1 : Add R] [inst_2 : Mul S] [inst_3 : Add S] [inst_4 : Preorder R]
  [inst_5 : Preorder S] (e : R ≃+*o S) {x : R} {y : S}, e.symm y < x ↔ y < e x
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_pow : ∀ {x : ℝ}, 0 ≤ x → ∀ (n : ℕ), (x ^ n).toNNReal = x.toNNReal ^ n
-- Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
MeasureTheory.MemLp.meas_ge_lt_top_enorm : ∀ {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} [inst : TopologicalSpace ε'] [inst_1 : ContinuousENorm ε']
  {p : ENNReal} {μ : MeasureTheory.Measure α} {f : α → ε'},
  MeasureTheory.MemLp f p μ → p ≠ 0 → p ≠ ⊤ → ∀ {ε : NNReal}, ε ≠ 0 → μ {x | ↑ε ≤ ‖f x‖ₑ} < ⊤
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.of_restrictScalars : ∀ (R : Type u_1) [inst : CommRing R] (A : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra R A] (B : Type u_3)
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B]
  [Algebra.FormallyUnramified R B], Algebra.FormallyUnramified A B
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_inter_lt_top_of_left_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α}, μ s ≠ ⊤ → μ (s ∩ t) < ⊤
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.MCore : Type → Type
-- Batteries.Data.List.Lemmas
List.idxOfNth_lt_idxOfNth_iff : ∀ {α : Type u_1} {x : α} {n m : ℕ} [inst : BEq α] {xs : List α},
  List.idxOfNth x xs n < List.idxOfNth x xs m ↔ n < List.count x xs ∧ n < m
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.insertIdxTR.go.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → List α → Array α → Sort u_2) →
    (x : ℕ) →
      (x_1 : List α) →
        (x_2 : Array α) →
          ((l : List α) → (acc : Array α) → motive 0 l acc) →
            ((x : ℕ) → (acc : Array α) → (x = 0 → False) → motive x [] acc) →
              ((n : ℕ) → (a : α) → (l : List α) → (acc : Array α) → motive n.succ (a :: l) acc) → motive x x_1 x_2
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_natDegree_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.natDegree = 0 → f.Splits
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_nsmul_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIocMod hp a (m • p + b) = toIocMod hp a b
-- Mathlib.Topology.Compactness.Lindelof
IsLindelof.countable_of_discrete : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [DiscreteTopology X], IsLindelof s → s.Countable
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `lowerSemicontinuousOn_inv_iff`. -/
UpperSemicontinuousOn.inv : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} [inst_1 : PartialOrder β]
  [inst_2 : CommGroup β] [IsOrderedMonoid β], UpperSemicontinuousOn f s → LowerSemicontinuousOn f⁻¹ s
-- Lean.Elab.DeprecatedArg
Lean.Elab.DeprecatedArgEntry.text? : Lean.Elab.DeprecatedArgEntry → Option String
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The set of points in the `realSpace` that are equal to `0` at a fixed place has volume zero.  -/
NumberField.mixedEmbedding.realSpace.volume_eq_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (w : NumberField.InfinitePlace K),
  MeasureTheory.volume {x | x w = 0} = 0
-- Mathlib.Analysis.Convex.Side
AffineSubspace.not_wSameSide_bot : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x y : P),
  ¬⊥.WSameSide x y
-- Mathlib.Order.RelIso.Basic
RelHom.instRelHomClass : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, RelHomClass (r →r s) r s
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.coe_sub : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f g : M [⋀^ι]→L[R] N) [inst_7 : IsTopologicalAddGroup N], ⇑(f - g) = ⇑f - ⇑g
-- Init.Data.List.Lemmas
List.mem_iff_get : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l ↔ ∃ n, l.get n = a
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.trans_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor C D} (α : F ≅ G) (β : G ≅ H) (X : C), (α ≪≫ β).app X = α.app X ≪≫ β.app X
-- Std.Data.Internal.List.Associative
Std.Internal.List.nil_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)},
  (∀ (k : α), Std.Internal.List.containsKey k l = false) ↔ l = []
-- Lean.Util.CollectFVars
Lean.CollectFVars.main : Lean.Expr → Lean.CollectFVars.Visitor
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.negAt_apply_snd : ∀ {K : Type u_1} [inst : Field K] {s : Set { w // w.IsReal }} (x : NumberField.mixedEmbedding.mixedSpace K),
  ((NumberField.mixedEmbedding.negAt s) x).2 = x.2
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- The conjunction of two prelocal predicates is prelocal.  -/
TopCat.LocalPredicate.and : {X : TopCat} → {T : ↑X → Type u_1} → TopCat.LocalPredicate T → TopCat.LocalPredicate T → TopCat.LocalPredicate T
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {p q : α → Prop},
  MeasurableSet {x | p x} → MeasurableSet {x | q x} → MeasurableSet {x | p x ↔ q x}
-- Mathlib.Data.Sym.Sym2
Set.sym2_empty : ∀ {α : Type u_1}, ∅.sym2 = ∅
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
/-- The manifold derivative within `range I` of `(extChartAt I x).symm` at the chart point is
the identity.  -/
mfderivWithin_range_extChartAt_symm : ∀ {𝕜 : 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] [IsManifold I 1 M] {x : M},
  mfderiv[Set.range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x) =
    ContinuousLinearMap.id 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x) x))
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.instFaithfulUnderToUnder : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor D T) [F.Faithful], (CategoryTheory.StructuredArrow.toUnder X F).Faithful