mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Join.Opposites
_private.Mathlib.CategoryTheory.Join.Opposites.0.CategoryTheory.Join.opEquiv.match_1.eq_2 : ∀ (C : Type u_2) (D : Type u_1) [inst : CategoryTheory.Category.{u_3, u_2} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_1} D] (motive : (CategoryTheory.Join C D)ᵒᵖ → Sort u_5) (a : D)
  (h_1 : (a : C) → motive (Opposite.op (CategoryTheory.Join.left a)))
  (h_2 : (a : D) → motive (Opposite.op (CategoryTheory.Join.right a))),
  (match Opposite.op (CategoryTheory.Join.right a) with
    | Opposite.op (CategoryTheory.Join.left a) => h_1 a
    | Opposite.op (CategoryTheory.Join.right a) => h_2 a) =
    h_2 a
-- Mathlib.Data.Set.Image
/-- Alias of `Set.image_compl_eq_range_sdiff_image`.  -/
Set.range_sdiff_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set α), Set.range f \ f '' s = f '' sᶜ
-- Mathlib.Algebra.Order.Group.Int.Sum
/-- Sharp lower bound for the sum of a finset of integers that is bounded below, `range` version.  -/
Finset.sum_range_le_sum : ∀ {s : Finset ℤ} {c : ℤ}, (∀ x ∈ s, c ≤ x) → ∑ n ∈ Finset.range s.card, (c + ↑n) ≤ ∑ x ∈ s, x
-- Mathlib.Tactic.Order.CollectFacts
/-- State for `CollectFactsM`. It contains a map that maps a type to atomic facts collected for
this type.  -/
Mathlib.Tactic.Order.CollectFactsState : Type
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constEntryAtIdx_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {i : ℕ} {h' : i < t₁.size} (h : t₁.Equiv t₂),
  Std.DTreeMap.Const.entryAtIdx t₁ i h' = Std.DTreeMap.Const.entryAtIdx t₂ i ⋯
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Methods.toMethodsRef : Lean.Meta.Sym.Simp.Methods → Lean.Meta.Sym.Simp.MethodsRef
-- Mathlib.Algebra.Group.Basic
neg_involutive : ∀ {G : Type u_3} [inst : InvolutiveNeg G], Function.Involutive Neg.neg
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∈ t₂ → (t₁ ∩ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric_smul : ∀ {X : Type u_2} [inst : EMetricSpace X] (m : ENNReal → ENNReal) {c : ENNReal},
  c ≠ ⊤ → c ≠ 0 → MeasureTheory.OuterMeasure.mkMetric (c • m) = c • MeasureTheory.OuterMeasure.mkMetric m
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.monotoneOn_leftDeriv : ∀ {S : Set ℝ} {f : ℝ → ℝ}, ConvexOn ℝ S f → MonotoneOn (fun x => derivWithin f (Set.Iio x) x) (interior S)
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Entries.mk.sizeOf_spec : ∀ (s : Lean.ExprMap Mathlib.Explode.Entry) (l : List Mathlib.Explode.Entry),
  sizeOf { s := s, l := l } = 1 + sizeOf s + sizeOf l
-- Mathlib.ModelTheory.Algebra.Field.CharP
FirstOrder.Field.realize_eqZero : ∀ {K : Type u_1} [inst : CommRing K] [inst_1 : FirstOrder.Ring.CompatibleRing K] (n : ℕ) (v : Empty → K),
  FirstOrder.Language.Formula.Realize (FirstOrder.Field.eqZero n) v ↔ ↑n = 0
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instUpwardEnumerable_eq : Int8.instUpwardEnumerable = HasModel.instUpwardEnumerable✝
-- Mathlib.Logic.Function.Basic
Function.RightInverse.leftInverse : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.RightInverse g f → Function.LeftInverse f g
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeReachable.mono : ∀ {V : Type u_1} {G H : SimpleGraph V} {k : ℕ} {u v : V}, G ≤ H → G.IsEdgeReachable k u v → H.IsEdgeReachable k u v
-- Init.Data.BitVec.Lemmas
BitVec.or_comm : ∀ {w : ℕ} (x y : BitVec w), x ||| y = y ||| x
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
minSmoothness_eq_infty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞},
  minSmoothness 𝕜 n = ↑⊤ ↔ n = ↑⊤ ∧ IsRCLikeNormedField 𝕜
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.star_val_eq : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : StarAddMonoid R] {x : ↥(selfAdjoint R)}, star ↑x = ↑x
-- Mathlib.Logic.Equiv.Nat
Equiv.natSumNatEquivNat_symm_apply : ∀ (a : ℕ), Equiv.natSumNatEquivNat.symm a = if a.bodd = true then Sum.inr a.div2 else Sum.inl a.div2
-- Init.Data.SInt.Bitwise
Int32.toISize_and : ∀ (a b : Int32), (a &&& b).toISize = a.toISize &&& b.toISize
-- Mathlib.LinearAlgebra.Prod
LinearMap.ker_fst : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (LinearMap.fst R M M₂).ker = (LinearMap.inr R M M₂).range
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorMk_map_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} (mor₁ : obj₁ ⟶ obj₂)
  (mor₂ : obj₂ ⟶ obj₃) (mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)) {X Y : J} (φ : X ⟶ Y),
  ((CategoryTheory.Pretriangulated.Triangle.functorMk mor₁ mor₂ mor₃).map φ).hom₂ = obj₂.map φ
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_flip : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LinearMap.flip (LieModule.traceForm R L M) = LieModule.traceForm R L M
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.number : Lean.Lsp.SemanticTokenType
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.comp_toGlued_eq : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) {U : AlgebraicGeometry.Scheme} {i j : ι}
  (a : U ⟶ X i) (b : U ⟶ X j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map a) (f i) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map b) (f j) →
    CategoryTheory.CategoryStruct.comp a (AlgebraicGeometry.Scheme.LocalRepresentability.toGlued hf i) =
      CategoryTheory.CategoryStruct.comp b (AlgebraicGeometry.Scheme.LocalRepresentability.toGlued hf j)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.uproj.inj : ∀ {i : ℕ} {x : Lean.IR.VarId} {i_1 : ℕ} {x_1 : Lean.IR.VarId},
  Lean.IR.Expr.uproj i x = Lean.IR.Expr.uproj i_1 x_1 → i = i_1 ∧ x = x_1
-- Mathlib.FieldTheory.IsPerfectClosure
/-- Composition of `p`-radical ring homomorphisms is also `p`-radical.  -/
IsPRadical.trans : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommSemiring K] [inst_1 : CommSemiring L]
  [inst_2 : CommSemiring M] (i : K →+* L) (f : L →+* M) (p : ℕ) [IsPRadical i p] [IsPRadical f p],
  IsPRadical (f.comp i) p
-- Mathlib.Algebra.Order.Field.Basic
_private.Mathlib.Algebra.Order.Field.Basic.0.exists_lt_mul_left_of_nonneg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b c : α},
  0 ≤ a → 0 ≤ c → c < a * b → ∃ a' ∈ Set.Ico 0 a, c < a' * b
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
MonoidHom.CompTriple.instId_comp : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] {φ : M →* N} {ψ : N →* N}
  [MonoidHom.CompTriple.IsId ψ], φ.CompTriple ψ φ
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAt.comp_hasFDerivWithinAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {h₂ : 𝕜' → 𝕜'} {h₂' y : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s : Set E} (x : E),
  HasDerivAt h₂ h₂' y → HasFDerivWithinAt f f' s x → y = f x → HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
-- Mathlib.LinearAlgebra.Contraction
_private.Mathlib.LinearAlgebra.Contraction.0.dualTensorHom_self_right_bijective : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.Bijective ⇑(dualTensorHom R M R)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Spec.preimage_map : ∀ {R S : CommRingCat} (φ : R ⟶ S), AlgebraicGeometry.Spec.preimage (AlgebraicGeometry.Spec.map φ) = φ
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.coeff_det_one_add_X_smul_one : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  (1 + Polynomial.X • M.map ⇑Polynomial.C).det.coeff 1 = M.trace
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure' : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {D₁ : Type u_1} {D₂ : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D₁] [inst_3 : CategoryTheory.Category.{v_2, u_2} D₂]
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
  (F : CategoryTheory.Functor D₁ D₂) [h : Φ.IsLeftDerivabilityStructure] (e : Φ.functor.comp L₂ ≅ L₁.comp F),
  CategoryTheory.TwoSquare.GuitartExact e.inv
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_finset_eq_prod : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (s : Finset α),
  ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ s, f i
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.mk' : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂]
  (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] (hG : G.FullyFaithful),
  Φ.IsLocalizedFullyFaithful
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.removeUnnecessaryCasts.isDummyEqRec : Lean.Expr → Bool
-- Mathlib.Algebra.Homology.Embedding.Extend
/-- Given `K : HomologicalComplex C c` and `e : c.Embedding c'`,
this is the extension of `K` in `HomologicalComplex C c'`: it is
zero in the degrees that are not in the image of `e.f`.  -/
HomologicalComplex.extend : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [CategoryTheory.Limits.HasZeroObject C] →
              [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
                HomologicalComplex C c → c.Embedding c' → HomologicalComplex C c'
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Bounding the Hausdorff distance by exhibiting, for any point in each set,
another point in the other set at controlled distance  -/
Metric.hausdorffDist_le_of_mem_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {r : ℝ},
  0 ≤ r → (∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r) → (∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r) → Metric.hausdorffDist s t ≤ r
-- Mathlib.CategoryTheory.ObjectProperty.SiteLocal
CategoryTheory.ObjectProperty.IsLocal.component : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C}
  {K : CategoryTheory.Precoverage C} [self : P.IsLocal K] {X : C} {R : CategoryTheory.Presieve X},
  R ∈ K.coverings X → ∀ {Y : C} (f : Y ⟶ X), R f → P X → P Y
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α}, m.size ≤ (m.insertManyIfNewUnit l).size
-- Mathlib.LinearAlgebra.TensorProduct.Vanishing
/-- Every expression $\sum_i m_i \otimes n_i$ which vanishes also vanishes trivially if and only if
for every finitely generated submodule $M' \subseteq M$, the map $M' \otimes N \to M \otimes N$ is
injective.  -/
TensorProduct.forall_vanishesTrivially_iff_forall_fg_rTensor_injective : ∀ (R : Type u_1) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N],
  (∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n) ↔
    ∀ (M' : Submodule R M), M'.FG → Function.Injective ⇑(LinearMap.rTensor N M'.subtype)
-- Mathlib.Order.Sublattice
Sublattice.subtype_injective : ∀ {α : Type u_2} [inst : Lattice α] (L : Sublattice α), Function.Injective ⇑L.subtype
-- Mathlib.Order.Category.Lat
Lat.hom_ext_iff : ∀ {X Y : Lat} {f g : X ⟶ Y}, f = g ↔ Lat.Hom.hom f = Lat.Hom.hom g
-- Init.Data.SInt.Lemmas
Int32.sub_nonneg_of_le : ∀ {a b : Int32}, 0 ≤ b → b ≤ a → 0 ≤ a - b
-- Mathlib.Topology.MetricSpace.BundledFun
/-- A pseudometric as a bundled function.  -/
PseudoMetric : Type u_1 → (R : Type u_2) → [Zero R] → [Add R] → [LE R] → Type (max u_1 u_2)
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- A subgroup is either the trivial subgroup or nontrivial.  -/
AddSubgroup.bot_or_nontrivial : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H = ⊥ ∨ Nontrivial ↥H
-- Mathlib.Algebra.Group.Pi.Basic
Sum.elim_neg_neg : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α → γ) (b : β → γ) [inst : Neg γ],
  Sum.elim (-a) (-b) = -Sum.elim a b
-- Mathlib.Analysis.SpecificLimits.Normed
summable_geometric_of_norm_lt_one : ∀ {K : Type u_4} [inst : NormedRing K] [HasSummableGeomSeries K] {x : K}, ‖x‖ < 1 → Summable fun n => x ^ n
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.of_finite : ∀ {S : AlgebraicGeometry.Scheme} {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme}
  {𝒰 : AlgebraicGeometry.Scheme.Cover K S} [AlgebraicGeometry.Scheme.JointlySurjective K]
  [∀ (i : 𝒰.I₀), AlgebraicGeometry.QuasiCompact (𝒰.f i)] [Finite 𝒰.I₀],
  AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover
-- Init.Data.UInt.Lemmas
UInt8.ofNat_toNat : ∀ {x : UInt8}, UInt8.ofNat x.toNat = x
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- The seminorm is invariant under inversion.  -/
GroupSeminorm.inv' : ∀ {G : Type u_6} [inst : Group G] (self : GroupSeminorm G) (x : G), self.toFun x⁻¹ = self.toFun x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_union_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂).getKey k ⋯ = m₂.getKey k mem
-- Mathlib.Data.Finset.Pi
Finset.dependsOn_restrict : ∀ {ι : Type u_2} {π : ι → Type u_3} (s : Finset ι), DependsOn s.restrict ↑s
-- Init.MetaTypes
Lean.Meta.LiftLetsConfig.mk : Lean.Meta.ExtractLetsConfig → Lean.Meta.LiftLetsConfig
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Under.liftCone_π_app : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt) (j : J),
  (CategoryTheory.Under.liftCone c f).π.app j = CategoryTheory.Under.homMk (c.π.app j) ⋯
-- Lean.Message
Lean.Message.isTrace : Lean.Message → Bool
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instInvolutiveInv : {α : Type u_1} → [InvolutiveInv α] → InvolutiveInv (WithZero α)
-- Std.Data.TreeMap.Basic
/-- Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
 -/
Std.TreeMap.getKey : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → (t : Std.TreeMap α β cmp) → (a : α) → a ∈ t → α
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- See also `MeasureTheory.ae_restrict_uIoc_iff`.  -/
MeasureTheory.ae_uIoc_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : LinearOrder α] {a b : α} {P : α → Prop},
  (∀ᵐ (x : α) ∂μ, x ∈ Set.uIoc a b → P x) ↔
    (∀ᵐ (x : α) ∂μ, x ∈ Set.Ioc a b → P x) ∧ ∀ᵐ (x : α) ∂μ, x ∈ Set.Ioc b a → P x
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nhdsWithin_Ici_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : Preorder α]
  {a b : α} [ClosedIciTopology α], (nhdsWithin a (Set.Ici b)).IsMeasurablyGenerated
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.comp_right_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β}
  {μc : MeasureTheory.Measure γ} {g : α → β} {e : γ ≃ᵐ α},
  MeasureTheory.MeasurePreserving (⇑e) μc μa →
    (MeasureTheory.MeasurePreserving (g ∘ ⇑e) μc μb ↔ MeasureTheory.MeasurePreserving g μa μb)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.Adj.coe : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u v : V} (h : H.Adj u v), H.coe.Adj ⟨u, ⋯⟩ ⟨v, ⋯⟩
-- Std.Data.TreeMap.Basic
Std.TreeMap.mk : {α : Type u} →
  {β : Type v} →
    {cmp : autoParam (α → α → Ordering) Std.TreeMap._auto_1} → Std.DTreeMap α (fun x => β) cmp → Std.TreeMap α β cmp
-- Init.Grind.Lemmas
Lean.Grind.forall_propagator : ∀ (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = True), q ⋯ = q' → (∀ (hp : p), q hp) = q'
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSets.symm : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {s₁ s₂ : Set (Set Ω)},
  ProbabilityTheory.Kernel.IndepSets s₁ s₂ κ μ → ProbabilityTheory.Kernel.IndepSets s₂ s₁ κ μ
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
CategoryTheory.MorphismProperty.instIsMultiplicativeInjective : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC],
  (CategoryTheory.MorphismProperty.injective C).IsMultiplicative
-- Mathlib.Tactic.NormNum.Irrational
Mathlib.Meta.NormNum.irrational_sqrt_rat_of_den : ∀ {x : ℝ} {num den den_k : ℕ},
  Mathlib.Meta.NormNum.IsNNRat x num den → num.Coprime den → den_k ^ 2 < den → den < (den_k + 1) ^ 2 → Irrational √x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.IsConj.eq : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)},
  NumberField.ComplexEmbedding.IsConj φ σ → ∀ (x : K), φ (σ x) = star (φ x)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.op_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.op.g = S.f.op
-- Init.PropLemmas
exists_const : ∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], (∃ x, b) ↔ b
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k fallback : α),
  Std.DTreeMap.Internal.Impl.leaf.getKeyD k fallback = fallback
-- Mathlib.RingTheory.PowerSeries.Restricted
PowerSeries.isRestricted_iff : ∀ {R : Type u_1} [inst : NormedRing R] (c : ℝ) (f : PowerSeries R),
  PowerSeries.IsRestricted c f ↔ Filter.Tendsto (fun t => ‖(PowerSeries.coeff t) f‖ * c ^ t) Filter.cofinite (nhds 0)
-- Mathlib.Data.Sigma.Basic
/-- A specialized ext lemma for equality of `PSigma` types over an indexed subtype.  -/
PSigma.subtype_ext : ∀ {α : Sort u_1} {β : Sort u_3} {p : α → β → Prop} {x₀ x₁ : (a : α) ×' Subtype (p a)},
  x₀.fst = x₁.fst → ↑x₀.snd = ↑x₁.snd → x₀ = x₁
-- Mathlib.GroupTheory.OreLocalization.Cardinality
AddOreLocalization.oreSub_zero_surjective_of_finite_left : ∀ {R : Type u} [inst : AddMonoid R] (S : AddSubmonoid R) [inst_1 : AddOreLocalization.AddOreSet S] (X : Type v)
  [inst_2 : AddAction R X] [Finite ↥S], Function.Surjective fun x => x -ₒ 0
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl)
A cone for the diagram `(D ⋙ forget T) ⋙ T` found by composing the natural transformation `γ`
with the limiting cone for `D ⋙ forget T`.
 -/
CategoryTheory.Comonad.ForgetCreatesLimits'.newCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          {D : CategoryTheory.Functor J T.Coalgebra} →
            CategoryTheory.Limits.Cone (D.comp T.forget) →
              CategoryTheory.Limits.Cone ((D.comp T.forget).comp T.toFunctor)
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyEntourage_le_coverEntropy : ∀ {X : Type u_1} {U : SetRel X X} [inst : UniformSpace X] (T : X → X) (F : Set X),
  U ∈ uniformity X → Dynamics.netEntropyEntourage T F U ≤ Dynamics.coverEntropy T F
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_toNonUnitalAlgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] {f : A →⋆ₙₐ[R] B}, ⇑f.toNonUnitalAlgHom = ⇑f
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.ext_iff : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] {f g : CentroidHom α}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- A costructured arrow is called universal if it is terminal.  -/
CategoryTheory.CostructuredArrow.IsUniversal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} → {S : CategoryTheory.Functor C D} → CategoryTheory.CostructuredArrow S T → Type (max (max u₁ v₂) v₁)
-- Mathlib.Analysis.Meromorphic.Order
/-- Eta-expanded form of `meromorphicOrderAt_zpow_id_sub_const`

---

The order of `(· - x) ^ n` at `x` is `n`.  -/
fun_meromorphicOrderAt_zpow_id_sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℤ}, meromorphicOrderAt (fun i => (i - x) ^ n) x = ↑n
-- Init.Data.Array.Find
Array.find?_filter : ∀ {α : Type u_1} {xs : Array α} (p q : α → Bool),
  Array.find? q (Array.filter p xs) = Array.find? (fun a => decide (p a = true ∧ q a = true)) xs
-- Mathlib.Algebra.Category.Ring.Basic
/-- This prevents `SemiRingCat.of R` being printed as `{ carrier := R, semiring := ... }` by
`delabStructureInstance`.  -/
SemiRingCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.RingTheory.Perfection
Perfection.coeff_toMonoidHom : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] (n : ℕ),
  ↑(Perfection.coeff R p n) = Perfection.coeffMonoidHom R p n
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.intTrace_eq_of_isLocalization : ∀ (A : Type u_1) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {Aₘ : Type u_9}
  {Bₘ : Type u_10} [inst_3 : CommRing Aₘ] [inst_4 : CommRing Bₘ] [inst_5 : Algebra Aₘ Bₘ] [inst_6 : Algebra A Aₘ]
  [inst_7 : Algebra B Bₘ] [inst_8 : Algebra A Bₘ] [IsScalarTower A Aₘ Bₘ] [IsScalarTower A B Bₘ] (M : Submonoid A)
  [IsLocalization M Aₘ] [IsLocalization (Algebra.algebraMapSubmonoid B M) Bₘ] [inst_13 : IsDomain A]
  [inst_14 : IsIntegrallyClosed A] [inst_15 : IsDomain B] [inst_16 : IsIntegrallyClosed B] [inst_17 : Module.Finite A B]
  [inst_18 : Module.IsTorsionFree A B] [inst_19 : IsDomain Aₘ] [inst_20 : IsIntegrallyClosed Aₘ] [inst_21 : IsDomain Bₘ]
  [inst_22 : IsIntegrallyClosed Bₘ] [inst_23 : Module.IsTorsionFree Aₘ Bₘ] [inst_24 : Module.Finite Aₘ Bₘ] (x : B),
  (algebraMap A Aₘ) ((Algebra.intTrace A B) x) = (Algebra.intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)