mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- In a non-trivial module, zero is not non-degenerate.  -/
LinearMap.BilinForm.not_nondegenerate_zero : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial M],
  ¬LinearMap.BilinForm.Nondegenerate 0
-- Lean.Meta.Order
/-- Given `packedInst : CCPO α `, returns an underlying instance of the type
`PartialOrder α`. Can handle `CompleteLattice` as well.
Takes an optional argument with the type `α`. If the optional argument is `none`,
it is treated implicitly.
 -/
Lean.Meta.toPartialOrder : Lean.Expr → optParam (Option Lean.Expr) none → Lean.MetaM Lean.Expr
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Return.mk.sizeOf_spec : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {w : ℕ} (result : aig.ExtendingRefVecEntry w)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑result).aig),
  sizeOf { result := result, cache := cache } = 1 + sizeOf result + sizeOf cache
-- Lean.Environment
/-- Auxiliary function to signal to the structure instance elaborator that `default` should be used as
the default value for a field but only if `_otherField` has been given, which is added as an
artificial dependency.
 -/
Lean.useDefaultIfOtherFieldGiven : {α : Sort u_1} → {β : Sort u_2} → α → β → α
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_eq_norm_mul_iff_div : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, x ≠ 0 → (inner 𝕜 x y = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y)
-- Mathlib.Algebra.Order.Sub.Defs
tsub_eq_of_eq_add : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftReflectLE α], a = c + b → a - b = c
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.coe_smul_of_det_pos : ∀ {g : GL (Fin 2) ℝ},
  0 < ↑(Matrix.GeneralLinearGroup.det g) →
    ∀ (z : UpperHalfPlane), ↑(g • z) = UpperHalfPlane.num g ↑z / UpperHalfPlane.denom g ↑z
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instFree : ∀ {R : Type u_3} (c₁ c₂ c₃ : R) [inst : CommRing R], Module.Free R (QuaternionAlgebra R c₁ c₂ c₃)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} [inst_2 : Inhabited (β a)],
  Std.Internal.List.getValueCast! a [] = default
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.bddAbove_range_approx : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (x : X),
  BddAbove (Set.range fun n => Urysohns.CU.approx n c x)
-- Std.Time.Date.Unit.Month
/-- Transforms `Month.Ordinal` into `Day.Offset`.
 -/
Std.Time.Month.Ordinal.toDays : Bool → Std.Time.Month.Ordinal → Std.Time.Day.Offset
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id._auto_1),
  CategoryTheory.CategoryStruct.comp (X.toCycles (CategoryTheory.CategoryStruct.id i₀) f f ⋯ n₀)
      (X.cyclesIsoH f n₀ n₁ hn₁).hom =
    CategoryTheory.CategoryStruct.id ((X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Mathlib.Logic.Equiv.PartialEquiv
/-- We say that `t : Set β` is an image of `s : Set α` under a partial equivalence if
any of the following equivalent conditions hold:

* `e '' (e.source ∩ s) = e.target ∩ t`;
* `e.source ∩ e ⁻¹ t = e.source ∩ s`;
* `∀ x ∈ e.source, e x ∈ t ↔ x ∈ s` (this one is used in the definition).
 -/
PartialEquiv.IsImage : {α : Type u_1} → {β : Type u_2} → PartialEquiv α β → Set α → Set β → Prop
-- Mathlib.Order.Lattice
sup_le_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c d : α}, a ≤ b → c ≤ d → a ⊔ c ≤ b ⊔ d
-- Mathlib.Analysis.Calculus.Deriv.Slope
isSeparable_range_deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [TopologicalSpace.SeparableSpace 𝕜] (f : 𝕜 → F),
  TopologicalSpace.IsSeparable (Set.range (deriv f))
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- If two cyclic permutations agree on all terms in their intersection,
and that intersection is not empty, then the two cyclic permutations must be equal.  -/
Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr : ∀ {α : Type u_2} {f g : Equiv.Perm α} {x : α} [inst : DecidableEq α] [inst_1 : Fintype α],
  f.IsCycle → g.IsCycle → (∀ x ∈ f.support ∩ g.support, f x = g x) → f x = g x → x ∈ f.support → f = g
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.injective_restrict_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {p : Submodule R M} {q : Submodule R₂ M₂} {f : M →ₛₗ[τ₁₂] M₂} (hf : ∀ x ∈ p, f x ∈ q),
  Function.Injective ⇑(f.restrict hf) ↔ Disjoint p f.ker
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivWithinAt.smul_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'} {c' : 𝕜'},
  HasDerivWithinAt c c' s x → ∀ (f : F), HasDerivWithinAt (fun y => c y • f) (c' • f) s x
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- Consider a monotone function `u` parameterizing some points of a set `s`. Given `x ∈ s`, then
one can find another monotone function `v` parameterizing the same points as `u`, with `x` added.
In particular, the variation of a function along `u` is bounded by its variation along `v`.  -/
eVariationOn.add_point : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α} {x : α},
  x ∈ s →
    ∀ (u : ℕ → α),
      Monotone u →
        (∀ (i : ℕ), u i ∈ s) →
          ∀ (n : ℕ),
            ∃ v m,
              Monotone v ∧
                (∀ (i : ℕ), v i ∈ s) ∧
                  x ∈ v '' Set.Iio m ∧
                    ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤
                      ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- **Fermat's Theorem**: the derivative of a function at a local minimum equals zero.  -/
IsLocalMin.deriv_eq_zero : ∀ {f : ℝ → ℝ} {a : ℝ}, IsLocalMin f a → deriv f a = 0
-- Mathlib.Data.Finset.Powerset
/-- For predicate `p` decidable on subsets, it is decidable whether `p` holds for every subset.  -/
Finset.decidableForallOfDecidableSubsets' : {α : Type u_1} → {s : Finset α} → {p : Finset α → Prop} → [(t : Finset α) → Decidable (p t)] → Decidable (∀ t ⊆ s, p t)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
/-- The function `Real.arsinh` is real analytic.  -/
Real.analyticOn_arsinh : ∀ {s : Set ℝ}, AnalyticOn ℝ Real.arsinh s
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.instOne : {E : Type u_3} → [inst : AddGroup E] → [DecidableEq E] → One (AddGroupNorm E)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_insertIfNew_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {v : β}, (cmp (t.insertIfNew k v).minKey! k).isLE = true
-- Mathlib.Algebra.Ring.Subring.IntPolynomial
Polynomial.int_eval₂_eq : ∀ {K : Type u_1} [inst : Field K] (R : Subring K) (P : Polynomial K) (hP : ∀ (n : ℕ), P.coeff n ∈ R) {L : Type u_2}
  [inst_1 : Field L] [inst_2 : Algebra K L] (x : L),
  Polynomial.eval₂ (algebraMap (↥R) L) x (Polynomial.int R P hP) = (Polynomial.aeval x) P
-- Mathlib.Logic.Equiv.PartialEquiv
/-- **Alias** of the forward direction of `PartialEquiv.IsImage.iff_symm_preimage_eq`. -/
PartialEquiv.IsImage.symm_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  e.IsImage s t → e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t
-- Mathlib.NumberTheory.PellMatiyasevic
_private.Mathlib.NumberTheory.PellMatiyasevic.0.Pell.IsPell.match_1.eq_1 : ∀ {d : ℤ} (motive : ℤ√d → Sort u_1) (x y : ℤ) (h_1 : (x y : ℤ) → motive { re := x, im := y }),
  (match { re := x, im := y } with
    | { re := x, im := y } => h_1 x y) =
    h_1 x y
-- Init.Data.BitVec.Lemmas
BitVec.toFin_ofFin : ∀ {w : ℕ} (n : Fin (2 ^ w)), { toFin := n }.toFin = n
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.toN : {X : SSet} → {A : X.Subcomplex} → A.N → X.N
-- Mathlib.RingTheory.Smooth.Basic
/-- An `R`-algebra `A` is formally smooth iff "for every `R`-algebra `B`,
every square-zero ideal `I : Ideal B` and `f : A →ₐ[R] B ⧸ I`, there exists
at least one lift `A →ₐ[R] B`".
 -/
Algebra.FormallySmooth.iff_comp_surjective : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.FormallySmooth R A ↔
    ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- If `f` is a transfinite composition of shape `J` of morphisms
in `W.inverseImage F`, then `F` is a transfinite composition of shape `J`
of morphisms in `W` provided `F` preserves suitable colimits.  -/
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {J : Type w} →
          [inst_2 : LinearOrder J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : OrderBot J] →
                [inst_5 : WellFoundedLT J] →
                  {X Y : C} →
                    {f : X ⟶ Y} →
                      {W : CategoryTheory.MorphismProperty D} →
                        {F : CategoryTheory.Functor C D} →
                          [CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J F] →
                            [CategoryTheory.Limits.PreservesColimitsOfShape J F] →
                              (W.inverseImage F).TransfiniteCompositionOfShape J f →
                                W.TransfiniteCompositionOfShape J (F.map f)
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The bundled commutative group giving the filtered colimit of a diagram.  -/
CommGrpCat.FilteredColimits.colimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J CommGrpCat → CommGrpCat
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.WEquiv.ind : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (a : (MvQPF.P F).A)
  (f' : ((MvQPF.P F).drop.B a).Arrow α) (f₀ f₁ : (MvQPF.P F).last.B a → (MvQPF.P F).W α),
  (∀ (x : (MvQPF.P F).last.B a), MvQPF.WEquiv (f₀ x) (f₁ x)) →
    MvQPF.WEquiv ((MvQPF.P F).wMk a f' f₀) ((MvQPF.P F).wMk a f' f₁)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_mem_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {l : List (α × β)} {k : α}, k ∈ t.insertMany l → (List.map Prod.fst l).contains k = false → k ∈ t
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.Total.Hom.w_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {k l : CategoryTheory.Limits.ColimitPresentation.Total P} (self : k.Hom l) {Z : C} (h : D.obj l.fst ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (CategoryTheory.CategoryStruct.comp (D.map self.base) h) =
    CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp ((P l.fst).ι.app l.snd) h)
-- Aesop.Index.Basic
Aesop.IndexMatchResult.mk.inj : ∀ {α : Type} {rule : α} {locations : Array Aesop.IndexMatchLocation}
  {patternSubsts? : Option (Array Aesop.Substitution)} {rule_1 : α} {locations_1 : Array Aesop.IndexMatchLocation}
  {patternSubsts?_1 : Option (Array Aesop.Substitution)},
  { rule := rule, locations := locations, patternSubsts? := patternSubsts? } =
      { rule := rule_1, locations := locations_1, patternSubsts? := patternSubsts?_1 } →
    rule = rule_1 ∧ locations = locations_1 ∧ patternSubsts? = patternSubsts?_1
-- Init.Data.SInt.Lemmas
UInt16.ofBitVec_int16ToBitVec : ∀ (x : Int16), { toBitVec := x.toBitVec } = x.toUInt16
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.instProdTopologicalSpace : (p : ENNReal) →
  (α : Type u_2) → (β : Type u_3) → [TopologicalSpace α] → [TopologicalSpace β] → TopologicalSpace (WithLp p (α × β))
-- Lean.Elab.Quotation
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.resolveSectionVariable.loop : Lean.NameMap Lean.Name → Lean.MacroScopesView → Lean.Name → List String → List (Lean.Name × List String)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_le_size_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)}, m.size ≤ (m.insertMany l).size
-- Mathlib.Order.Filter.CardinalInter
Filter.CardinalGenerateSets.sInter : ∀ {α : Type u} {c : Cardinal.{u}} {g S : Set (Set α)},
  Cardinal.mk ↑S < c → (∀ s ∈ S, Filter.CardinalGenerateSets g s) → Filter.CardinalGenerateSets g (⋂₀ S)
-- Mathlib.Order.Interval.Finset.Fin
Fin.card_Icc : ∀ {n : ℕ} (a b : Fin n), (Finset.Icc a b).card = ↑b + 1 - ↑a
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Being filtered or empty is preserved by equivalence of categories.  -/
CategoryTheory.IsFilteredOrEmpty.of_equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (h : C ≌ D), CategoryTheory.IsFilteredOrEmpty D
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac._auto_1)
  [inst_3 : CategoryTheory.Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)]
  [inst_4 : CategoryTheory.Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)] {Z : C} (h : S.obj ⟨k + 2, ⋯⟩ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (S.map' k (k + 1) ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp (hS.cokerIsoKer k ⋯).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (S.map' (k + 2) (k + 3) ⋯ ⋯)) h)) =
    CategoryTheory.CategoryStruct.comp (S.map' (k + 1) (k + 2) ⋯ ⋯) h
-- Mathlib.RingTheory.Morita.Basic
IsMoritaEquivalent.trans : ∀ (R : Type u₀) [inst : CommSemiring R] {A B C : Type u₁} [inst_1 : Ring A] [inst_2 : Ring B] [inst_3 : Ring C]
  [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C],
  IsMoritaEquivalent R A B → IsMoritaEquivalent R B C → IsMoritaEquivalent R A C
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.Config.mk.injEq : ∀ (red : Lean.Meta.TransparencyMode) (zetaDelta contextual : Bool) (red_1 : Lean.Meta.TransparencyMode)
  (zetaDelta_1 contextual_1 : Bool),
  ({ red := red, zetaDelta := zetaDelta, contextual := contextual } =
      { red := red_1, zetaDelta := zetaDelta_1, contextual := contextual_1 }) =
    (red = red_1 ∧ zetaDelta = zetaDelta_1 ∧ contextual = contextual_1)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8}
  [inst : NormedAddCommGroup G''] [inst_1 : PartialOrder G''] [IsOrderedAddMonoid G''] [inst_3 : NormedSpace ℝ G'']
  [inst_4 : NormedAddCommGroup G'] [inst_5 : PartialOrder G'] [inst_6 : NormedSpace ℝ G'] [ClosedIciTopology G'']
  {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) →
    ∀ {f : α → G'}, 0 ≤ᵐ[μ] f → 0 ≤ MeasureTheory.setToFun μ T hT f
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsLeftAdjoint], F.PreservesEpimorphisms
-- Mathlib.Topology.NhdsSet
principal_le_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, Filter.principal s ≤ nhdsSet s
-- Mathlib.RingTheory.LocalRing.Quotient
IsLocalRing.basisQuotient_repr : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [inst_4 : Module.Finite R S] [inst_5 : Module.Free R S] {ι : Type u_4} [inst_6 : Fintype ι]
  (b : Module.Basis ι R S) (x : S) (i : ι),
  ((IsLocalRing.basisQuotient b).repr ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) x))
      i =
    (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R)) ((b.repr x) i)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.toList_rio : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => Unit),
  t.Ordered →
    ∀ (bound : α),
      Std.Slice.toList (Std.Rio.Sliceable.mkSlice t *...bound) = List.filter (fun e => (compare e bound).isLT) t.keys
-- Lean.Elab.Tactic.RCases
/-- Convert a list of patterns to a tuple pattern, but mapping `[p]` to `p` instead of `⟨p⟩`.  -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.tuple' : List Lean.Elab.Tactic.RCases.RCasesPatt → Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ico_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Ico a b)), Subtype.val '' Set.Ioi c = Set.Ioo (↑c) b
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Choose inductively large balls with centers that are not contained in the union of already
chosen balls. This is a transfinite induction.  -/
Besicovitch.TauPackage.index : {α : Type u_1} → [MetricSpace α] → {β : Type u} → [Nonempty β] → Besicovitch.TauPackage β α → Ordinal.{u} → β
-- Mathlib.Order.Hom.Basic
OrderHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), f.comp OrderHom.id = f
-- Mathlib.Dynamics.Minimal
MulAction.IsMinimal.dense_orbit : ∀ {M : Type u_1} {α : Type u_2} {inst : Monoid M} {inst_1 : TopologicalSpace α} {inst_2 : MulAction M α}
  [self : MulAction.IsMinimal M α] (x : α), Dense (MulAction.orbit M x)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.instFullFunctorWhiskeringLeftFunctor' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W], (CategoryTheory.Localization.whiskeringLeftFunctor' L W E).Full
-- Mathlib.Algebra.Order.Floor.Extended
ENat.preimage_toENNReal_Icc : ∀ (a b : ENNReal), ENat.toENNReal ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉ₑ ⌊b⌋ₑ
-- Mathlib.Algebra.Group.Prod
Prod.subNegMonoid.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : SubNegMonoid G] [inst_1 : SubNegMonoid H],
  Prod.subNegMonoid =
    { toAddMonoid := Prod.instAddMonoid, toNeg := Prod.instNeg, toSub := Prod.instSub,
      zsmul := fun z a => (ZSMul.zsmul z a.1, ZSMul.zsmul z a.2), sub_eq_add_neg := ⋯, zsmul_zero' := ⋯,
      zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_comm`.  -/
hammingDist_comm : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] (x y : (i : ι) → β i),
  hammingDist x y = hammingDist y x
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instRxcIsAlwaysFinite : ∀ {n : ℕ}, Std.Rxc.IsAlwaysFinite (BitVec n)
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
/-- A class of almost everywhere equal functions is `Integrable` if its function representative
is integrable.  -/
MeasureTheory.AEEqFun.Integrable : {α : Type u_1} →
  {ε : Type u_3} →
    {m : MeasurableSpace α} →
      {μ : MeasureTheory.Measure α} → [inst : TopologicalSpace ε] → [ContinuousENorm ε] → (α →ₘ[μ] ε) → Prop
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
/-- If a monoid homomorphism `f` between two `GroupWithZero`s maps `0` to `0`, then it maps `x^n`,
`n : ℤ`, to `(f x)^n`.  -/
map_zpow₀ : ∀ {F : Type u_8} {G₀ : Type u_9} {G₀' : Type u_10} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero G₀']
  [inst_2 : FunLike F G₀ G₀'] [MonoidWithZeroHomClass F G₀ G₀'] (f : F) (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.toListRev_iter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap α β},
  m.iter.toListRev = m.toList.reverse
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.liesOver_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (h : optParam (IsLocalRing S) ⋯),
  (IsLocalRing.maximalIdeal S).LiesOver I
-- Std.Data.DTreeMap.Internal.Balancing
/-- A single left rotation.  -/
Std.DTreeMap.Internal.Impl.singleL : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        Std.DTreeMap.Internal.Impl α β →
          (rk : α) →
            β rk → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Init.Data.Array.Bootstrap
Array.foldlM.loop.congr_simp : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f f_1 : β → α → m β),
  f = f_1 →
    ∀ (as as_1 : Array α) (e_as : as = as_1) (stop stop_1 : ℕ) (e_stop : stop = stop_1) (h : stop ≤ as.size)
      (i i_1 : ℕ),
      i = i_1 →
        ∀ (j j_1 : ℕ),
          j = j_1 →
            ∀ (b b_1 : β),
              b = b_1 → Array.foldlM.loop f as stop h i j b = Array.foldlM.loop f_1 as_1 stop_1 ⋯ i_1 j_1 b_1
-- Mathlib.Algebra.Group.Invertible.Defs
/-- A copy of `invertibleMul` for dot notation.  -/
Invertible.mul : {α : Type u} → [inst : Monoid α] → {a b : α} → Invertible a → Invertible b → Invertible (a * b)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inr_isoIsPushout_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y}
  {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : CategoryTheory.IsPushout f g inl inr)
  (h' : CategoryTheory.IsPushout f g inl' inr') {Z_1 : C} (h_1 : P' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPushout.isoIsPushout X Y h h').hom h_1) =
    CategoryTheory.CategoryStruct.comp inr' h_1