mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
/-- If a functor `G : C ⥤ (D, K)` is locally fully faithful and locally dense, `S` is
a covering in the restricted topology on `C` if its image generates a `K`-cover.  -/
CategoryTheory.Functor.mem_restrictedTopology_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D}
  {K : CategoryTheory.GrothendieckTopology D} [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K]
  {X : C} {S : CategoryTheory.Sieve X},
  S ∈ (G.restrictedTopology K) X ↔ CategoryTheory.Sieve.functorPushforward G S ∈ K (G.obj X)
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.instHashable : Hashable Std.Http.Header.Name
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₁)
  {h' : k ∈ m₁ ∪ m₂}, Std.DHashMap.Raw.Const.get (m₁ ∪ m₂) k h' = Std.DHashMap.Raw.Const.get m₂ k ⋯
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqLhs.injEq : ∀ (gen gen_1 : Bool),
  (Lean.Meta.Grind.EMatchTheoremKind.eqLhs gen = Lean.Meta.Grind.EMatchTheoremKind.eqLhs gen_1) = (gen = gen_1)
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.instSubsingletonUnits : ∀ {M : Type u_1} [inst : Monoid M] [Subsingleton Mˣ] {S : Submonoid M}, Subsingleton (↥S)ˣ
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instNonemptyExtensionProductIter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.Nonempty] (n : ℕ), (P.extensionProductIter n).Nonempty
-- Mathlib.Algebra.DirectSum.AddChar
/-- Direct sum of additive characters.  -/
AddChar.directSum : {ι : Type u_1} →
  {R : Type u_2} →
    {G : ι → Type u_3} →
      [DecidableEq ι] →
        [inst : (i : ι) → AddCommGroup (G i)] →
          [inst_1 : CommMonoid R] → ((i : ι) → AddChar (G i) R) → AddChar (DirectSum ι fun i => G i) R
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.ordered_mergeWith : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β}
  {f : α → β → β → β} (htb : t₁.Balanced),
  t₁.Ordered → (Std.DTreeMap.Internal.Impl.Const.mergeWith f t₁ t₂ htb).impl.Ordered
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.lift_iso : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'') [inst_7 : IsLocalizedModule S f]
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (x : LocalizedModule S M),
  (IsLocalizedModule.lift S f g h) ((IsLocalizedModule.iso S f) x) = (LocalizedModule.lift S g h) x
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.single_pos_nat_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : DecidableEq X] {x : X},
  0 < Function.locallyFinsuppWithin.single x 1
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Instance.mk.inj : ∀ {val : Lean.Expr} {synthOrder : Array ℕ} {val_1 : Lean.Expr} {synthOrder_1 : Array ℕ},
  { val := val, synthOrder := synthOrder } = { val := val_1, synthOrder := synthOrder_1 } →
    val = val_1 ∧ synthOrder = synthOrder_1
-- Batteries.Data.List.Lemmas
List.countBefore_lt_count_getElem : ∀ {α : Type u_1} {i : ℕ} [inst : BEq α] [ReflBEq α] {xs : List α} {h : i < xs.length},
  List.countBefore xs[i] xs i < List.count xs[i] xs
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Assume that
1. `C` has binary products and pullbacks,
2. `D` has pullbacks, binary products and a terminal object, and
3. `F : C ⥤ D` is full and preserves binary products and pullbacks.

For a morphism `g : F.obj a ⟶ pullback (terminal.from X) (terminal.from X)`,
the canonical morphism from `F.obj a` to
`pullback ((g ≫ pullback.fst _ _) ≫ terminal.from X) ((g ≫ pullback.snd _ _) ≫ terminal.from X)`
is relatively representable with respect to `F`.
 -/
CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C]
  [inst_3 : CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasBinaryProducts D]
  [inst_5 : CategoryTheory.Limits.HasTerminal D] [F.Full]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] {X : D}
  {a : C} [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  (g :
    F.obj a ⟶
      CategoryTheory.Limits.pullback (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from X)),
  F.relativelyRepresentable
    (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id (F.obj a))
      (CategoryTheory.CategoryStruct.id (F.obj a)) ⋯)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.iter_deriv_rpow_const : ∀ (r x : ℝ) (k : ℕ), deriv^[k] (fun x => x ^ r) x = Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - ↑k)
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- An n-ary version of `Set.mul_mem_mul`.  -/
Set.list_prod_mem_list_prod : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : List ι) (f : ι → Set α) (g : ι → α),
  (∀ i ∈ t, g i ∈ f i) → (List.map g t).prod ∈ (List.map f t).prod
-- Mathlib.Topology.Bornology.Basic
/-- **Alias** of the forward direction of `Bornology.isCobounded_compl_iff`. -/
Bornology.IsCobounded.of_compl : ∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsCobounded sᶜ → Bornology.IsBounded s
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.bin.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.bin k v l r = Std.DTreeMap.Internal.Impl.inner (l.size + 1 + r.size) k v l r
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- The obvious map `Fork f g → Cofork f.unop g.unop`  -/
CategoryTheory.Limits.Fork.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : Cᵒᵖ} → {f g : X ⟶ Y} → CategoryTheory.Limits.Fork f g → CategoryTheory.Limits.Cofork f.unop g.unop
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.of_add_right : ∀ {α : Type u_1} [inst : LE α] [inst_1 : AddSemigroup α] [AddLeftMono α] {a b : α},
  AddLECancellable (a + b) → AddLECancellable b
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.entryAtIdx?_eq_getElem? : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β},
  t.Balanced → ∀ {i : ℕ}, t.entryAtIdx? i = t.toListModel[i]?
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.zero_apply : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (v : V₁),
  0 v = 0
-- Init.Core
DoResultPRBC.pure.injEq : ∀ {α β σ : Type u} (a : α) (a_1 : σ) (a_2 : α) (a_3 : σ),
  (DoResultPRBC.pure a a_1 = DoResultPRBC.pure a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Topology.Semicontinuity.Defs
LowerSemicontinuous.lowerSemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β},
  LowerSemicontinuous f → ∀ (s : Set α) (x : α), LowerSemicontinuousWithinAt f s x
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Get the smallest element in the heap, including the passed in value `a`.  -/
Batteries.BinomialHeap.Imp.Heap.headD : {α : Type u_1} → (α → α → Bool) → α → Batteries.BinomialHeap.Imp.Heap α → α
-- Mathlib.Tactic.GRewrite.Core
Mathlib.Tactic.GRewrite.Config.toConfig : Mathlib.Tactic.GRewrite.Config → Lean.Meta.Rewrite.Config
-- Mathlib.Data.Nat.Choose.Basic
Nat.factorial_mul_factorial_dvd_factorial : ∀ {n k : ℕ}, k ≤ n → k.factorial * (n - k).factorial ∣ n.factorial
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.Construction.wIso_eq_isoOfHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (f : X ⟶ Y) (hf : W f),
  CategoryTheory.Localization.Construction.wIso f hf = CategoryTheory.Localization.isoOfHom W.Q W f hf
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comap_comap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {f : α → β} {g : β → γ},
  (∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)) →
    Function.Injective g →
      (∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)) →
        ∀ (μ : MeasureTheory.Measure γ),
          MeasureTheory.Measure.comap f (MeasureTheory.Measure.comap g μ) = MeasureTheory.Measure.comap (g ∘ f) μ
-- Mathlib.Order.RelIso.Basic
/-- Composition of two relation homomorphisms is a relation homomorphism.  -/
RelHom.comp : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → s →r t → r →r s → r →r t
-- Init.Data.List.Sublist
List.IsSuffix.mem : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, a ∈ l₁ → l₁ <:+ l₂ → a ∈ l₂
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instInhabited : {α : Type u_1} → [inst : TopologicalSpace α] → Inhabited (TopologicalSpace.CompactOpens α)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.SavedState : Type
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.invert.eq_1 : ∀ (f : Std.Sat.AIG.Fanin), f.invert = (1 &&& f.val != 0)
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Does every element of the map satisfy property `P`?

```
All (fun x ↦ x < 5) {1, 2, 3} = True
All (fun x ↦ x < 5) {1, 2, 3, 5} = False
```  -/
Ordnode.All : {α : Type u_1} → (α → Prop) → Ordnode α → Prop
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalCore_eq_iSup : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.normalCore = ⨆ N, ⨆ (_ : N.Normal), ⨆ (_ : N ≤ H), N
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃}
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (F.map f₀₁) (F.map f₁₂)) (F.map f₂₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) h) =
    CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv h))
-- Mathlib.Analysis.Analytic.Composition
Composition.blocksFun.hcongr_3 : ∀ (n n' : ℕ),
  n = n' →
    ∀ (c : Composition n) (c' : Composition n'),
      c ≍ c' → ∀ (a : Fin c.length) (a' : Fin c'.length), a ≍ a' → c.blocksFun a ≍ c'.blocksFun a'
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.fg_ker : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ) [Finite σ], P.ker.FG
-- Init.Data.List.Lemmas
List.getLast?_concat : ∀ {α : Type u_1} {l : List α} {a : α}, (l ++ [a]).getLast? = some a
-- Mathlib.GroupTheory.Nilpotent
Subgroup.IsDescendingCentralSeries.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : ℕ → Subgroup G),
  Subgroup.IsDescendingCentralSeries H = (H 0 = ⊤ ∧ ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1))
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.comp_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {G : CategoryTheory.PreZeroHypercover S} (f : E.Hom F) (g : F.Hom G)
  (i : E.I₀), (f.comp g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))
-- Std.Time.Format.Modifier
Std.Time.Modifier.s.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.s presentation = Std.Time.Modifier.s presentation_1) = (presentation = presentation_1)
-- Mathlib.Topology.Algebra.Support
tsupport_comp_eq_preimage : ∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] {Y : Type u_9}
  [inst_2 : TopologicalSpace Y] (g : Y → α) (f : X ≃ₜ Y), tsupport (g ∘ ⇑f) = ⇑f ⁻¹' tsupport g
-- Init.Data.Array.Attach
Array.unattach_attach : ∀ {α : Type u_1} {xs : Array α}, xs.attach.unattach = xs
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
StarSubalgebra.topologicalClosure.congr_simp : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A] (s s_1 : StarSubalgebra R A),
  s = s_1 → s.topologicalClosure = s_1.topologicalClosure
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.instReprRecurringRule : Repr Std.Time.TimeZone.RecurringRule
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_lt_arccos : ∀ {x y : ℝ}, -1 ≤ x → x < y → y ≤ 1 → Real.arccos y < Real.arccos x
-- Lean.Parser.Term.Basic
Lean.Parser.Term.strictImplicitLeftBracket : Lean.Parser.Parser
-- Mathlib.RingTheory.Etale.StandardEtale
/-- If `T` is an etale algebra, and a standard etale algebra surjects onto `T`, then
`T` is also standard etale.  -/
Algebra.IsStandardEtale.of_surjective : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [Algebra.IsStandardEtale R S] [Algebra.Etale R T] (f : S →ₐ[R] T),
  Function.Surjective ⇑f → Algebra.IsStandardEtale R T
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Spec.preimage_comp_assoc : ∀ {R S T : CommRingCat} (f : AlgebraicGeometry.Spec R ⟶ AlgebraicGeometry.Spec S)
  (g : AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec T) {Z : CommRingCat} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.preimage (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.preimage g)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.preimage f) h)
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The valuation subring associated to a valuation.  -/
Valuation.valuationSubring : {K : Type u} →
  [inst : Field K] → {Γ : Type u_1} → [inst_1 : LinearOrderedCommGroupWithZero Γ] → Valuation K Γ → ValuationSubring K
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_mul_inv_iff_le : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b : α}, 1 ≤ a * b⁻¹ ↔ b ≤ a
-- Mathlib.RingTheory.Multiplicity
Int.natCast_multiplicity : ∀ (a b : ℕ), multiplicity ↑a ↑b = multiplicity a b
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_smul_le : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M)
  (r : R), Submodule.span R (r • s) ≤ Submodule.span R s
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.mk_hom : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F'), (CategoryTheory.Functor.LeftExtension.mk F' α).hom = α
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.apply_mono : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) {s₁ s₂ : Set Ω}, s₁ ⊆ s₂ → μ s₁ ≤ μ s₂
-- Mathlib.RingTheory.AdicCompletion.Basic
IsPrecomplete.of_subsingleton : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Subsingleton M], IsPrecomplete I M
-- Mathlib.GroupTheory.Finiteness
/-- An equivalent expression of `Group.FG` in terms of `Set.Finite` instead of `Finset`.  -/
Group.fg_iff : ∀ {G : Type u_3} [inst : Group G], Group.FG G ↔ ∃ S, Subgroup.closure S = ⊤ ∧ S.Finite
-- Std.Do.SPred.Laws
Std.Do.SPred.bientails.symm : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, (P ⊣⊢ₛ Q) → Q ⊣⊢ₛ P
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Piecewise modified version of `g` with optimal asymptotics.  -/
WeakFEPair.g_modif : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → ℝ → E
-- Lean.Elab.DocString
Lean.Doc.FromDocArg.mk : {α : Type} → (Lean.Doc.DocArg → Lean.Elab.TermElabM α) → Lean.Doc.FromDocArg α
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.ofStarAlgHom_symm_apply : ∀ {R : Type u_8} {A : Type u_9} {B : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (f : A →⋆ₐ[R] B) (g : B →⋆ₐ[R] A)
  (h₁ : g.comp f = StarAlgHom.id R A) (h₂ : f.comp g = StarAlgHom.id R B) (a : B),
  (StarAlgEquiv.ofStarAlgHom f g h₁ h₂).symm a = g a
-- Lean.Server.Completion.CompletionItemCompression
_private.Lean.Server.Completion.CompletionItemCompression.0.Lean.Lsp.ResolvableCompletionList.compressItemsFast : String → Array Lean.Lsp.ResolvableCompletionItem → ℕ → String
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isAddCyclic_of_injective : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] [IsAddCyclic G'] (f : G →+ G'),
  Function.Injective ⇑f → IsAddCyclic G
-- Init.Data.String.Iterate
String.Slice.ByteIterator.offset : String.Slice.ByteIterator → String.Pos.Raw
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.map_shrinkCoyonedaEquiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : Cᵒᵖ}
  {P : CategoryTheory.Functor C (Type w)} (f : CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X ⟶ P) (g : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (P.map g.unop)) (CategoryTheory.shrinkCoyonedaEquiv f) =
    (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.unop Y)))
      (CategoryTheory.shrinkCoyonedaObjObjEquiv.symm g.unop)
-- Batteries.Data.Fin.Coding
Fin.decodeSigma.eq_1 : ∀ (x_2 : Fin 0 → ℕ) (val : ℕ) (h : val < Fin.sum x_2), Fin.decodeSigma x_2 ⟨val, h⟩ = ⋯.elim
-- Mathlib.RingTheory.Ideal.Quotient.Operations
AlgEquiv.quotientBot_symm_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : S),
  (AlgEquiv.quotientBot R S).symm s = (Ideal.Quotient.mk ⊥) s
-- Lean.Expr
Lean.Expr.letBody! : Lean.Expr → Lean.Expr
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientInfEquivSumNormalQuotient.eq_1 : ∀ {G : Type u} [inst : AddGroup G] (H N : AddSubgroup G) [hN : N.Normal],
  QuotientAddGroup.quotientInfEquivSumNormalQuotient H N = QuotientAddGroup.quotientInfEquivSumNormalizerQuotient H N ⋯
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.of_linearIndependent_subset : ∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} [inst : Semiring R] (s : Set ι') {v : ι → ι' → R},
  (LinearIndependent R fun i j => v i ↑j) → LinearIndependent R v
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.funLike.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N],
  MulHom.funLike = { coe := MulHom.toFun, coe_injective := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.coeff_eq_iff_of_forall_abs_le_one : ∀ {n : ℕ} {P : Polynomial ℝ},
  P.degree ≤ ↑n →
    (∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ 1) → (P.coeff n = 2 ^ (n - 1) ↔ P = Polynomial.Chebyshev.T ℝ ↑n)
-- Mathlib.Data.Stream.Init
Stream'.drop_zero : ∀ {α : Type u} {s : Stream' α}, Stream'.drop 0 s = s
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.inhabited : {N : Type u_1} → {X : Type u_2} → [inst : TopologicalSpace X] → {x : X} → Inhabited ↑(GenLoop N X x)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.basis_repr : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) (x : S) (i : Fin f.natDegree), (h.basis.repr x) i = (h.modByMonicHom x).coeff ↑i
-- Mathlib.Data.List.SplitLengths
_private.Mathlib.Data.List.SplitLengths.0.List.splitLengths.match_3.eq_1 : ∀ {α : Type u_1} (motive : List ℕ → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (n : ℕ) → (ns : List ℕ) → (x : List α) → motive (n :: ns) x),
  (match [], x with
    | [], x => h_1 x
    | n :: ns, x => h_2 n ns x) =
    h_1 x
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_ofBounded_iff : ∀ {α : Type u_2} {s : Set α} (B : Set (Set α)) {empty_mem : ∅ ∈ B} {subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B}
  {union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B} {sUnion_univ : ∀ (x : α), {x} ∈ B}, Bornology.IsBounded s ↔ s ∈ B
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.prod_trans : ∀ {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} {Z : Type u_5} {Z' : Type u_6}
  [inst : TopologicalSpace X] [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y]
  [inst_3 : TopologicalSpace Y'] [inst_4 : TopologicalSpace Z] [inst_5 : TopologicalSpace Z']
  (e : OpenPartialHomeomorph X Y) (f : OpenPartialHomeomorph Y Z) (e' : OpenPartialHomeomorph X' Y')
  (f' : OpenPartialHomeomorph Y' Z'), (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_le_of_le_one_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [PosMulMono α],
  0 ≤ a → b ≤ 1 → a * b ≤ a
-- Mathlib.Algebra.Star.Subalgebra
/-- The star subalgebra `StarSubalgebra.adjoin R {x}` generated by a single `x : A` is commutative
if `x` is normal.  -/
StarAlgebra.adjoinCommSemiringOfIsStarNormal : (R : Type u_2) →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : StarRing A] →
              [inst_5 : StarModule R A] → (x : A) → [IsStarNormal x] → CommSemiring ↥(StarAlgebra.adjoin R {x})
-- Mathlib.Data.Finset.Sort
Finset.sorted_last_eq_max' : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α}
  {h : (s.sort fun a b => a ≤ b).length - 1 < (s.sort fun a b => a ≤ b).length},
  (s.sort fun a b => a ≤ b)[(s.sort fun a b => a ≤ b).length - 1] = s.max' ⋯
-- Init.Data.List.MapIdx
/-- Applies a function to each element of the list along with the index at which that element is found,
returning the list of results.

`List.mapFinIdx` is a variant that additionally provides the function with a proof that the index
is valid.
 -/
List.mapIdx : {α : Type u_1} → {β : Type u_2} → (ℕ → α → β) → List α → List β
-- Mathlib.Topology.Separation.Regular
normal_separation : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X] {s t : Set X},
  IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t