mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Descriptive.Tree
/-- A tree is a set of finite sequences, implemented as `List A`, that is stable under
taking prefixes. For the definition we use the equivalent property `x ++ [a] ∈ T → x ∈ T`,
which is more convenient to check. We define `tree A` as a complete sublattice of
`Set (List A)`, which coerces to the type of trees on `A`.  -/
Descriptive.tree : (A : Type u_1) → CompleteSublattice (Set (List A))
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivary_neg_right`. -/
Monovary.neg_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommGroup β]
  [inst_2 : PartialOrder β] [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β}, Monovary f g → Antivary f (-g)
-- Std.Data.HashMap.Lemmas
Std.HashMap.not_mem_of_isEmpty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.isEmpty = true → a ∉ m
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.mem_iff_one_sub_mem : ∀ {β : Type u_2} [inst : Ring β] [inst_1 : PartialOrder β] [IsOrderedRing β] {t : β},
  t ∈ Set.Icc 0 1 ↔ 1 - t ∈ Set.Icc 0 1
-- Init.Data.List.Find
List.find?_replicate_of_pos : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α},
  p a = true → List.find? p (List.replicate n a) = if n = 0 then none else some a
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.ofList_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α},
  (Std.TreeSet.ofList l cmp).Equiv (List.foldl (fun acc a => acc.insert a) ∅ l)
-- Mathlib.Order.Category.BddDistLat
_private.Mathlib.Order.Category.BddDistLat.0.BddDistLat.Hom.mk.inj : ∀ {X Y : BddDistLat} {hom' hom'_1 : BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opcyclesOpIso_hom_toCycles_op_assoc : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [inst_2 : K.HasHomology i]
  (j : ι) {Z : Vᵒᵖ} (h : Opposite.op (K.X j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.opcyclesOpIso i).hom
      (CategoryTheory.CategoryStruct.comp (K.toCycles j i).op h) =
    CategoryTheory.CategoryStruct.comp (K.op.fromOpcycles i j) h
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.filter_fst_eq_antidiagonal : ∀ {A : Type u_1} [inst : AddCommMonoid A] [inst_1 : PartialOrder A] [CanonicallyOrderedAdd A] [inst_3 : Sub A]
  [OrderedSub A] [AddLeftReflectLE A] [inst_6 : Finset.HasAntidiagonal A] (n m : A)
  [inst_7 : DecidablePred fun x => x = m] [inst_8 : Decidable (m ≤ n)],
  {x ∈ Finset.HasAntidiagonal.antidiagonal n | x.1 = m} = if m ≤ n then {(m, n - m)} else ∅
-- Mathlib.Topology.Homotopy.LocallyContractible
/-- A topological space is **strongly locally contractible** if, at every point, contractible
neighborhoods form a neighborhood basis. Here "contractible" means contractible as a subspace.

This is strictly stronger than the classical notion of locally contractible, which only requires
null-homotopic inclusions.
This distinction is witnessed by an example from Borsuk-Mazurkiewicz [borsuk_mazurkiewicz1934];
see also [MO88628] for discussion and the Whitehead manifold example.  -/
StronglyLocallyContractibleSpace : (X : Type u_4) → [TopologicalSpace X] → Prop
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonDeclInfo : Lean.FromJson Lean.Lsp.DeclInfo
-- Mathlib.Algebra.Ring.Defs
NonUnitalCommRing.toNonUnitalCommSemiring : {α : Type u} → [s : NonUnitalCommRing α] → NonUnitalCommSemiring α
-- Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Set.zero_div_subset : ∀ {α : Type u_1} [inst : GroupWithZero α] (s : Set α), 0 / s ⊆ 0
-- Mathlib.Topology.Sets.Compacts
/-- In a nonempty locally compact space, there exists a compact set with nonempty interior.  -/
TopologicalSpace.PositiveCompacts.nonempty' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [WeaklyLocallyCompactSpace α] [Nonempty α],
  Nonempty (TopologicalSpace.PositiveCompacts α)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.bijOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), Set.BijOn (↑e) e.source e.target
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.snd_toFun : ∀ (R : Type u) [inst : Monoid R] (A : Type v) (B : Type w) [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : DistribMulAction R B] (self : A × B),
  (NonUnitalAlgHom.snd R A B) self = self.2
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.mk : {α : Type u} → [inst : Preorder α] → (ℕ →o α) → OmegaCompletePartialOrder.Chain α
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Functor.functorPushforward_imageSieve_mem : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {D : Type uD} [inst_1 : CategoryTheory.Category.{vD, uD} D]
  (G : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [G.IsLocallyFull K] {U V : C}
  (f : G.obj U ⟶ G.obj V), CategoryTheory.Sieve.functorPushforward G (G.imageSieve f) ∈ K (G.obj U)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.min!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.min! = t₂.min!
-- Mathlib.ModelTheory.Syntax
/-- Applies a unary function to a term.  -/
FirstOrder.Language.Functions.apply₁ : {L : FirstOrder.Language} → {α : Type u'} → L.Functions 1 → L.Term α → L.Term α
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.map_id : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R], MvPowerSeries.map (RingHom.id R) = RingHom.id (MvPowerSeries σ R)
-- Init.Data.SInt.Lemmas
ISize.ofIntClamp.eq_1 : ∀ (i : ℤ),
  ISize.ofIntClamp i =
    if hl : ISize.minValue.toInt ≤ i then
      if hr : i ≤ ISize.maxValue.toInt then ISize.ofIntLE i hl hr else ISize.maxValue
    else ISize.minValue
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_iSup_right : ∀ {ι : Sort uι} {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M]
  [inst_5 : Module R N] [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) (s : Submodule R M) (t : ι → Submodule R N),
  Submodule.map₂ f s (⨆ i, t i) = ⨆ i, Submodule.map₂ f s (t i)
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Eta-expanded form of `meromorphicNFOn_closedBall_comp_sub_const_iff_meromorphicNFOn_closedBall`

---

`MeromorphicNFOn` is invariant under translation, special case where the set is a closed ball.
 -/
meromorphicNFOn_closedBall_fun_comp_sub_const_iff_meromorphicNFOn_closedBall : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicNFOn (fun x => f (x - c)) (Metric.closedBall c R) ↔ MeromorphicNFOn f (Metric.closedBall 0 R)
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.indicator_const_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : Zero β] {s : Set α} {c : β},
  Filter.EventuallyConst (s.indicator fun x => c) l ↔ c = 0 ∨ Filter.EventuallyConst s l
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.inverse_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {X Y : CategoryTheory.ShrinkHoms.{u} C} (f : X ⟶ Y),
  (CategoryTheory.ShrinkHoms.inverse C).map f = (equivShrink (X.fromShrinkHoms ⟶ Y.fromShrinkHoms)).symm f
-- Std.Data.ExtTreeMap.Basic
/-- Partitions a tree map into two tree maps based on a predicate.  -/
Std.ExtTreeMap.partition : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (α → β → Bool) → Std.ExtTreeMap α β cmp → Std.ExtTreeMap α β cmp × Std.ExtTreeMap α β cmp
-- Mathlib.Algebra.Group.Defs
CommMonoid.toCommSemigroup : {M : Type u} → [self : CommMonoid M] → CommSemigroup M
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : Inhabited α] {a : α} {c : ℕ},
  (Std.HashSet.emptyWithCapacity c).get! a = default
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- Consider an element of the projectivization as a submodule of `V`.  -/
Projectivization.submodule : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Projectivization K V → Submodule K V
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.opow_lt_veblen_opow_iff : ∀ {o a : Ordinal.{u}}, Ordinal.omega0 ^ a < Ordinal.veblen o (Ordinal.omega0 ^ a) ↔ a < Ordinal.veblen o a
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.fold_eq_fold_toIterM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  {f : γ → β → γ} {init : γ} {it : Std.Iter β}, Std.Iter.fold f init it = (Std.IterM.fold f init it.toIterM).run
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.top : {α : Type u_1} → [inst : HeytingAlgebra α] → Top (Heyting.Regular α)
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- **Equational criterion for flatness**, forward direction.

If $M$ is flat, then every relation $\sum_i f_i x_i = 0$ in $M$ is trivial.  -/
Module.Flat.isTrivialRelation_of_sum_smul_eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  {ι : Type u_3} [inst_4 : Fintype ι] {f : ι → R} {x : ι → M}, ∑ i, f i • x i = 0 → Module.IsTrivialRelation f x
-- Mathlib.Order.Hom.Bounded
TopHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Top β] {f g : TopHom α β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet.precomp : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ι → Set Ω} {ι' : Type u_5} {g : ι' → ι},
  Function.Injective g → ProbabilityTheory.Kernel.iIndepSet s κ μ → ProbabilityTheory.Kernel.iIndepSet (s ∘ g) κ μ
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
hasSum_mul_right_iff : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a₁ a₂ : α}, a₂ ≠ 0 → (HasSum (fun i => f i * a₂) (a₁ * a₂) L ↔ HasSum f a₁ L)
-- Mathlib.Algebra.Module.Torsion.Free
instIsTorsionFreeIntOfIsAddTorsionFree : ∀ {M : Type u_3} [inst : AddCommGroup M] [IsAddTorsionFree M], Module.IsTorsionFree ℤ M
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
FDerivMeasurableAux.isOpen_B : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {K : Set (E →L[𝕜] F)} {r s ε : ℝ}, IsOpen (FDerivMeasurableAux.B f K r s ε)
-- Init.Notation
/-- Applies a function inside a functor. This is used to overload the `<$>` operator.

When mapping a constant function, use `Functor.mapConst` instead, because it may be more
efficient.


Conventions for notations in identifiers:

 * The recommended spelling of `<$>` in identifiers is `map`. -/
«term_<$>_» : Lean.TrailingParserDescr
-- Lean.Elab.WhereFinally
Lean.Elab.WhereFinallyView.mk.injEq : ∀ (ref : Lean.Syntax) (tactic : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (ref_1 : Lean.Syntax)
  (tactic_1 : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq),
  ({ ref := ref, tactic := tactic } = { ref := ref_1, tactic := tactic_1 }) = (ref = ref_1 ∧ tactic = tactic_1)
-- Mathlib.Algebra.GradedMonoid
SetLike.isHomogeneousElem_coe : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] {A : ι → S} {i : ι} (x : ↥(A i)),
  SetLike.IsHomogeneousElem A ↑x
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.of_comul : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : Ring X] [inst_2 : HopfAlgebra R X],
  CoalgebraStruct.comul = CoalgebraStruct.comul
-- Lean.Parser.Command
Lean.Parser.Command.structCtor.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.ext : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} (x : Submonoid A)
  {c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x}, c1.deg = c2.deg → ↑c1.num = ↑c2.num → ↑c1.den = ↑c2.den → c1 = c2
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- The orthogonal family constituting the summands in the Hilbert sum.  -/
IsHilbertSum.OrthogonalFamily : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E},
  IsHilbertSum 𝕜 G V → OrthogonalFamily 𝕜 G V
-- Mathlib.Data.Fintype.Order
/-- A finite bounded distributive lattice is completely distributive.  -/
Fintype.toCompleteDistribLatticeMinimalAxioms : ∀ (α : Type u_2) [inst : Fintype α] [inst_1 : DistribLattice α] [inst_2 : BoundedOrder α],
  CompleteDistribLattice.MinimalAxioms α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.one_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.GrpObj G] {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one
      (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
/-- For every `X : D`, there exists an object `p` of `C` with an effective epi `F.obj p ⟶ X`.  -/
CategoryTheory.Functor.EffectivelyEnough.presentation : ∀ {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} {F : CategoryTheory.Functor C D} [self : F.EffectivelyEnough] (X : D),
  Nonempty (F.EffectivePresentation X)
-- Init.Data.Ord.Basic
Ordering.lt_then : ∀ {o : Ordering}, Ordering.lt.then o = Ordering.lt
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.ereal_toReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → EReal}, Measurable f → Measurable fun x => (f x).toReal
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.del.inj : ∀ {x : Lean.IR.VarId} {b : Lean.IR.FnBody} {x_1 : Lean.IR.VarId} {b_1 : Lean.IR.FnBody},
  Lean.IR.FnBody.del x b = Lean.IR.FnBody.del x_1 b_1 → x = x_1 ∧ b = b_1
-- Mathlib.Algebra.Category.MonCat.Colimits
_private.Mathlib.Algebra.Category.MonCat.Colimits.0.MonCat.Colimits.descFunLift.match_1.eq_2 : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] (F : CategoryTheory.Functor J MonCat)
  (motive : MonCat.Colimits.Prequotient F → Sort u_3)
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (MonCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive MonCat.Colimits.Prequotient.one)
  (h_3 : (x y : MonCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match MonCat.Colimits.Prequotient.one with
    | MonCat.Colimits.Prequotient.of j x => h_1 j x
    | MonCat.Colimits.Prequotient.one => h_2 ()
    | x.mul y => h_3 x y) =
    h_2 ()
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinite_indep : ∀ {α : Type u_1} {E : Set α} (hE : E.Finite) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E),
  (IndepMatroid.ofFinite hE Indep indep_empty indep_subset indep_aug subset_ground).Indep = Indep
-- Mathlib.FieldTheory.SeparableClosure
/-- A compositum of two separable extensions is separable.  -/
IntermediateField.isSeparable_sup : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L1 L2 : IntermediateField F E)
  [h1 : Algebra.IsSeparable F ↥L1] [h2 : Algebra.IsSeparable F ↥L2], Algebra.IsSeparable F ↥(L1 ⊔ L2)
-- Mathlib.Topology.Algebra.Support
subset_mulTSupport : ∀ {X : Type u_1} {α : Type u_2} [inst : One α] [inst_1 : TopologicalSpace X] (f : X → α),
  Function.mulSupport f ⊆ mulTSupport f
-- Mathlib.LinearAlgebra.Matrix.Reindex
/-- `Matrix.reindex` as a `RingEquiv` between `R`-matrices.  -/
Matrix.reindexRingEquiv : {m : Type u_2} →
  {n : Type u_3} →
    (R : Type u_11) →
      [inst : Fintype m] →
        [inst_1 : Fintype n] → [inst_2 : Mul R] → [inst_3 : AddCommMonoid R] → m ≃ n → Matrix m m R ≃+* Matrix n n R
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.instMonoidHomClass : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N],
  MonoidHomClass (S.LocalizationMap N) M N
-- Batteries.Logic
instDecidablePredComp_batteries : {α : Sort u_1} → {β : Sort u_2} → {p : β → Prop} → {f : α → β} → [DecidablePred p] → DecidablePred (p ∘ f)
-- Init.Data.Array.Basic
Array.instEmptyCollection : {α : Type u} → EmptyCollection (Array α)
-- Mathlib.Data.Int.Bitwise
Int.shiftLeft_add' : ∀ (m : ℤ) (n : ℕ) (k : ℤ), m <<< (↑n + k) = m <<< ↑n <<< k
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.inter.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m₁ m₁_1 : Std.ExtDHashMap α β),
  m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.ExtDHashMap α β), m₂ = m₂_1 → m₁.inter m₂ = m₁_1.inter m₂_1
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsRevMatch.matches_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch pat startPos →
    String.Slice.Pattern.Model.PatternModel.Matches pat (s.sliceFrom startPos).copy
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Pointwise star on functions induced from continuous star preserves strong measurability.  -/
MeasureTheory.StronglyMeasurable.star : ∀ {α : Type u_1} {R : Type u_5} [inst : MeasurableSpace α] [inst_1 : Star R] [inst_2 : TopologicalSpace R]
  [ContinuousStar R] (f : α → R), MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable (star f)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  IsScalarTower R ↑((AlgebraicGeometry.structurePresheafInCommRingCat R).stalk x)
    ↑(TopCat.Presheaf.stalk (AlgebraicGeometry.moduleStructurePresheaf R M).presheaf x)
-- Mathlib.Topology.Order.LiminfLimsup
Monotone.limsup_nhdsGT_eq_iInf₂_of_exists_gt : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [DenselyOrdered α] [inst_4 : CompleteLattice β] {f : α → β},
  Monotone f → ∀ (a : α), (∃ b, a < b) → Filter.limsup f (nhdsWithin a (Set.Ioi a)) = ⨅ r, ⨅ (_ : r > a), f r
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.constMonoidHom.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MulOneClass Y],
  LocallyConstant.constMonoidHom = { toFun := LocallyConstant.const X, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.approxOn_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α}
  (h₀ : y₀ ∈ s) [inst_4 : TopologicalSpace.SeparableSpace ↑s] (x : β),
  (MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ 0) x = y₀
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.mem_toList_iff_mem : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {a : α}, a ∈ r.toList ↔ a ∈ r
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportFailure.mk.inj : ∀ {module const : Lean.Name} {exception : Lean.Exception} {module_1 const_1 : Lean.Name} {exception_1 : Lean.Exception},
  { module := module, const := const, exception := exception } =
      { module := module_1, const := const_1, exception := exception_1 } →
    module = module_1 ∧ const = const_1 ∧ exception = exception_1
-- Mathlib.Topology.Path
Path.map.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} (γ γ_1 : Path x y),
  γ = γ_1 → ∀ {f : X → Y} (h : Continuous f), γ.map h = γ_1.map h
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∪ m₂).getKey? k = m₂.getKey? k
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_maxKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [BEq α] [inst_3 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {km : α}, Std.Internal.List.maxKey? l = some km → Std.Internal.List.getKey? km l = some km
-- Init.Data.Slice.Array.Basic
instSliceableSubarrayNat_1 : {α : Type u} → Std.Rco.Sliceable (Subarray α) ℕ (Subarray α)
-- Mathlib.GroupTheory.OreLocalization.OreSet
AddOreLocalization.addOreSetComm.eq_1 : ∀ {R : Type u_2} [inst : AddCommMonoid R] (S : AddSubmonoid R),
  AddOreLocalization.addOreSetComm S =
    { ore_right_cancel := ⋯, oreMin := fun r x => r, oreSubtra := fun x s => s, ore_eq := ⋯ }
-- Mathlib.Order.Filter.Bases.Basic
/-- The set of filter basis sets is nonempty.  -/
FilterBasis.nonempty : ∀ {α : Type u_6} (self : FilterBasis α), self.sets.Nonempty
-- Mathlib.Analysis.Fourier.Notation
FourierAdd.fourier_add : ∀ {E : Type u_5} {F : outParam (Type u_6)} {inst : Add E} {inst_1 : Add F} {inst_2 : FourierTransform E F}
  [self : FourierAdd E F] (f g : E),
  FourierTransform.fourier (f + g) = FourierTransform.fourier f + FourierTransform.fourier g
-- Mathlib.Data.NNRat.BigOperators
NNRat.toNNRat_prod_of_nonneg : ∀ {α : Type u_1} {s : Finset α} {f : α → ℚ}, (∀ a ∈ s, 0 ≤ f a) → (∏ a ∈ s, f a).toNNRat = ∏ a ∈ s, (f a).toNNRat
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.concatCM_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b c : α}
  [inst_3 : Fact (a ≤ b)] [inst_4 : Fact (b ≤ c)] {E : Type u_2} [inst_5 : TopologicalSpace E] {x : ↑(Set.Icc a c)}
  (hx : b ≤ ↑x) {fg : { fg // fg.1 ⊤ = fg.2 ⊥ }}, (ContinuousMap.concatCM fg) x = (↑fg).2 ⟨↑x, ⋯⟩
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
IsStronglyTranscendental.of_isLocalization_left : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] (M : Submonoid R) [IsLocalization M S]
  [IsScalarTower R S T] {x : T}, IsStronglyTranscendental R x → IsStronglyTranscendental S x
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.mk.sizeOf_spec : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] [inst_7 : SizeOf R] [inst_8 : SizeOf E₁] [inst_9 : SizeOf E₂] (toLinearMap : E₁ →ₗ[R] E₂)
  (monotone' : Monotone toLinearMap.toFun),
  sizeOf { toLinearMap := toLinearMap, monotone' := monotone' } = 1 + sizeOf toLinearMap