mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.measurableSet_mutuallySingularSet : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ),
  MeasurableSet (κ.mutuallySingularSet η)
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- Flat descends along faithfully flat ring maps.  -/
Module.Flat.of_flat_tensorProduct : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Type u_1)
  [inst_3 : CommRing S] [inst_4 : Algebra R S] [Module.FaithfullyFlat R S] [Module.Flat S (TensorProduct R S M)],
  Module.Flat R M
-- Mathlib.NumberTheory.LucasLehmer
mersenne_lt_mersenne : ∀ {p q : ℕ}, mersenne p < mersenne q ↔ p < q
-- Mathlib.Logic.Basic
xor_not_not : ∀ {a b : Prop}, Xor (¬a) ¬b ↔ Xor a b
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- The additive equivalence `(X ⟶ Y) ≃+ (F X ⟶ F Y)` when `F : D → C` and
`C` is a preadditive category.  -/
CategoryTheory.InducedCategory.homAddEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u'} → {F : D → C} → {X Y : CategoryTheory.InducedCategory C F} → (X ⟶ Y) ≃+ (F X ⟶ F Y)
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameAux.visit : Lean.Expr → Lean.Elab.Command.NameGen.MkNameM✝ (List String × String)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k k' : α} {f : β → β},
  (Std.DHashMap.Const.modify m k f).getKey! k' = if (k == k') = true then if k ∈ m then k else default else m.getKey! k'
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.IsQuasiInverse.symm : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u : V₃ →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃},
  u.IsQuasiInverse v → v.IsQuasiInverse u
-- Mathlib.Order.SupClosed
IsSublattice_range : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : FunLike F α β]
  [LatticeHomClass F α β] (f : F), IsSublattice (Set.range ⇑f)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.instMkEvalWhiskerLeftMonoidalM : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft Mathlib.Tactic.Monoidal.MonoidalM
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → k ∉ t₁ ∩ t₂
-- Init.Data.Option.Attach
Option.attach_pfilter : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool},
  (o.pfilter p).attach = o.attach.pbind fun x h => if h' : p ↑x ⋯ = true then some ⟨↑x, ⋯⟩ else none
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.core.injEq : ∀ (a b : Lean.Expr) (ra rb : Lean.Grind.CommRing.Expr) (a_1 b_1 : Lean.Expr) (ra_1 rb_1 : Lean.Grind.CommRing.Expr),
  (Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.core a b ra rb =
      Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.core a_1 b_1 ra_1 rb_1) =
    (a = a_1 ∧ b = b_1 ∧ ra = ra_1 ∧ rb = rb_1)
-- Std.Data.ExtTreeSet.Basic
/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.ExtTreeSet.any : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → (α → Bool) → Bool
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instAddCommGroupAddUnits.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α],
  AddUnits.instAddCommGroupAddUnits = { toAddGroup := AddUnits.instAddGroup, add_comm := ⋯ }
-- Lean.Util.InstantiateLevelParams
_private.Lean.Util.InstantiateLevelParams.0.Lean.Expr.getParamSubst : List Lean.Name → List Lean.Level → Lean.Name → Option Lean.Level
-- Mathlib.Algebra.Homology.Bifunctor
/-- Given a functor `F : C₁ ⥤ C₂ ⥤ D`, this is the bifunctor which sends
`K₁ : HomologicalComplex C₁ c₁` and `K₂ : HomologicalComplex C₂ c₂` to the bicomplex
which is degree `(i₁, i₂)` consists of `(F.obj (K₁.X i₁)).obj (K₂.X i₂)`.  -/
CategoryTheory.Functor.mapBifunctorHomologicalComplex : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
              [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] →
                  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                    {I₁ : Type u_4} →
                      {I₂ : Type u_5} →
                        (c₁ : ComplexShape I₁) →
                          (c₂ : ComplexShape I₂) →
                            [F.PreservesZeroMorphisms] →
                              [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                CategoryTheory.Functor (HomologicalComplex C₁ c₁)
                                  (CategoryTheory.Functor (HomologicalComplex C₂ c₂) (HomologicalComplex₂ D c₁ c₂))
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findIdx.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (n : ℕ) (h_1 : (n : ℕ) → motive [] n)
  (h_2 : (a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n),
  (match [], n with
    | [], n => h_1 n
    | a :: l, n => h_2 a l n) =
    h_1 n
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.instBEqDatabase.beq : Mathlib.CrossRef.Database → Mathlib.CrossRef.Database → Bool
-- Mathlib.SetTheory.ZFC.PSet
PSet.not_nonempty_empty : ¬∅.Nonempty
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_mono_set : ∀ {α : Type u_2} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s t : Set α},
  s ⊆ t → μ.restrict s ≤ μ.restrict t
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Mk₁.map_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (i : Fin 2),
  CategoryTheory.ComposableArrows.Mk₁.map f i i ⋯ =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ i)
-- Mathlib.Analysis.Normed.Group.Defs
/-- A normed group is a group endowed with a norm for which `dist x y = ‖x⁻¹ * y‖` defines a metric
space structure.  -/
NormedCommGroup : Type u_8 → Type u_8
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.intTrace_eq_trace : ∀ (A : Type u_1) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsIntegrallyClosed A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B] [inst_7 : Module.Finite A B]
  [inst_8 : Module.IsTorsionFree A B] [Module.Free A B], Algebra.intTrace A B = Algebra.trace A B
-- Mathlib.CategoryTheory.Limits.MorphismProperty
/-- If `P` is closed under limits of shape `J` in `Comma L R`, then when `D` has
a limit in `Comma L R`, the forgetful functor creates this limit.  -/
CategoryTheory.MorphismProperty.Comma.forgetCreatesLimitOfClosed : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      {A : Type u_2} →
        {B : Type u_3} →
          {J : Type u_4} →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} A] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} B] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} J] →
                  {L : CategoryTheory.Functor A T} →
                    {R : CategoryTheory.Functor B T} →
                      (D : CategoryTheory.Functor J (CategoryTheory.MorphismProperty.Comma L R P ⊤ ⊤)) →
                        [(CategoryTheory.MorphismProperty.commaObj L R P).IsClosedUnderLimitsOfShape J] →
                          [CategoryTheory.Limits.HasLimit
                                (D.comp (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤))] →
                            CategoryTheory.CreatesLimit D (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤)
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
uliftZPowersHom_symm_apply : ∀ (G : Type u) [inst : Group G] (a : ULift.{u, 0} (Multiplicative ℤ) →* G),
  (uliftZPowersHom G).symm a = a (MulEquiv.ulift.symm (Multiplicative.ofAdd 1))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_map_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.AddMon C} (f : X ⟶ Y) (x : CategoryTheory.Discrete PUnit.{w + 1}),
  (CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit.inverse.map f).hom.app x = f.hom
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.pi.eq_1 : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → AddGroup (f i)] (I : Set η) (H : (i : η) → AddSubgroup (f i)),
  AddSubgroup.pi I H = { toAddSubmonoid := AddSubmonoid.pi I fun i => (H i).toAddSubmonoid, neg_mem' := ⋯ }
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- `P⁺` is always separated.  -/
CategoryTheory.GrothendieckTopology.Plus.sep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_5 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] {X : C}
  (P : CategoryTheory.Functor Cᵒᵖ D) (S : J.Cover X) (x y : CategoryTheory.ToType ((J.plusObj P).obj (Opposite.op X))),
  (∀ (I : S.Arrow),
      (CategoryTheory.ConcreteCategory.hom ((J.plusObj P).map I.f.op)) x =
        (CategoryTheory.ConcreteCategory.hom ((J.plusObj P).map I.f.op)) y) →
    x = y
-- Lean.Elab.App
/-- Returns `true` if there are positional or named arguments to be processed.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.hasArgsToProcess : Lean.Elab.Term.ElabAppArgs.M Bool
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_subset_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.ball x ε ⊆ Metric.closedBall x ε
-- Lean.Declaration
Lean.ConstantInfo.isUnsafe : Lean.ConstantInfo → Bool
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
isStrictlyPositive_ringInverse_iff : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [StarOrderedRing A] [inst_5 : Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A]
  {a : A}, IsStrictlyPositive (Ring.inverse a) ↔ IsStrictlyPositive a
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
adjacent side.  -/
Orientation.cos_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x + y) y).cos * ‖x + y‖ = ‖y‖
-- Mathlib.Algebra.Category.Grp.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
CommGrpCat.Hom.Simps.hom : (X Y : CommGrpCat) → X.Hom Y → ↑X →* ↑Y
-- Init.Data.Option.Attach
Option.attach_some : ∀ {α : Type u_1} {x : α}, (some x).attach = some ⟨x, ⋯⟩
-- Mathlib.LinearAlgebra.Ray
/-- `SameRay` follows from membership of `MulAction.orbit` for the `Units.posSubgroup`.  -/
sameRay_of_mem_orbit : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {v₁ v₂ : M},
  v₁ ∈ MulAction.orbit (↥(Units.posSubgroup R)) v₂ → SameRay R v₁ v₂
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.toHeap.go.eq_def : ∀ {α : Type u_1} (a : Batteries.BinomialHeap.Imp.HeapNode α) (a_1 : ℕ) (a_2 : Batteries.BinomialHeap.Imp.Heap α),
  Batteries.BinomialHeap.Imp.HeapNode.toHeap.go a a_1 a_2 =
    match a, a_1, a_2 with
    | Batteries.BinomialHeap.Imp.HeapNode.nil, x, res => res
    | Batteries.BinomialHeap.Imp.HeapNode.node a c s, n, res =>
      Batteries.BinomialHeap.Imp.HeapNode.toHeap.go s (n - 1) (Batteries.BinomialHeap.Imp.Heap.cons (n - 1) a c res)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
/-- Conjugation induces an equivariant map between the SubAddAction of
the stabilizer of a point and that of its translate.  -/
SubAddAction.ofStabilizer.conjMap : {G : Type u_3} →
  [inst : AddGroup G] →
    {α : Type u_4} →
      [inst_1 : AddAction G α] →
        {g : G} →
          {a b : α} →
            (hg : b = g +ᵥ a) →
              ↥(SubAddAction.ofStabilizer G a) →ₑ[⇑(AddAction.stabilizerEquivStabilizer hg)]
                ↥(SubAddAction.ofStabilizer G b)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- `Cocycle K L n` is the kernel of the differential on `HomComplex K L`.  -/
CochainComplex.HomComplex.Cocycle.isKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K L : CochainComplex C ℤ) →
        (n m : ℤ) →
          (hm : n + 1 = m) →
            CategoryTheory.Limits.IsLimit
              (CategoryTheory.Limits.KernelFork.ofι
                (AddCommGrpCat.ofHom (CochainComplex.HomComplex.Cocycle.toCochainAddMonoidHom K L n)) ⋯)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false →
        Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.Const.insertMany m l) k = Std.DHashMap.Raw.Const.get! m k
-- Init.Data.Array.Attach
Array.attachWith_congr : ∀ {α : Type u_1} {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H : ∀ x ∈ xs, P x},
  xs.attachWith P H = ys.attachWith P ⋯
-- Mathlib.LinearAlgebra.DFinsupp
/-- `DFinsupp.single` as a `LinearMap`  -/
DFinsupp.lsingle : {ι : Type u_1} →
  {R : Type u_3} →
    {M : ι → Type u_5} →
      [inst : Semiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] → [DecidableEq ι] → (i : ι) → M i →ₗ[R] Π₀ (i : ι), M i
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNorm_indicator_const₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {c : ε} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    p ≠ 0 → p ≠ ⊤ → MeasureTheory.eLpNorm (s.indicator fun x => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Product of a list of elements in an intermediate field is in the intermediate field.  -/
IntermediateField.list_prod_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {l : List L}, (∀ x ∈ l, x ∈ S) → l.prod ∈ S
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `Left.inv_le_one_iff`.

---

Uses `left` co(ntra)variant.  -/
one_le_of_inv_le_one : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a : α}, a⁻¹ ≤ 1 → 1 ≤ a
-- Lean.CoreM
Lean.Core.checkMaxHeartbeats : String → Lean.CoreM Unit
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f : X ⟶ Y} [inst_2 : SizeOf C]
  (toMapFactorizationData :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f)
  (s : Y ⟶ toMapFactorizationData.Z)
  (s_p :
    autoParam (CategoryTheory.CategoryStruct.comp s toMapFactorizationData.p = CategoryTheory.CategoryStruct.id Y)
      HomotopicalAlgebra.CofibrantBrownFactorization.s_p._autoParam)
  (cofibration_s :
    autoParam (HomotopicalAlgebra.Cofibration s)
      HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s._autoParam),
  sizeOf { toMapFactorizationData := toMapFactorizationData, s := s, s_p := s_p, cofibration_s := cofibration_s } =
    1 + sizeOf toMapFactorizationData + sizeOf s + sizeOf s_p + sizeOf cofibration_s
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- If two measures `ρ` and `ν` have, at every point of a set `s`, arbitrarily small sets in a
Vitali family satisfying `ρ a ≤ ν a`, then `ρ s ≤ ν s` if `ρ ≪ μ`.  -/
VitaliFamily.measure_le_of_frequently_le : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] {ρ : MeasureTheory.Measure α}
  (ν : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure ν],
  ρ.AbsolutelyContinuous μ → ∀ (s : Set α), (∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a) → ρ s ≤ ν s
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} [inst_3 : HasDerivedCategory C] {n : ℕ}
  {α β : CategoryTheory.Abelian.Ext X Y n}, α.hom = β.hom → α = β
-- Mathlib.RingTheory.Extension.Generators
Finsupp.sumFinsuppAddEquivProdFinsupp.eq_1 : ∀ {M : Type u_5} [inst : AddMonoid M] {α : Type u_12} {β : Type u_13},
  Finsupp.sumFinsuppAddEquivProdFinsupp = { toEquiv := Finsupp.sumFinsuppEquivProdFinsupp, map_add' := ⋯ }
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.fst : ∀ {α : Type u_4} {β : Type u_5} [inst : AddMonoid α] [inst_1 : AddMonoid β] {x : α × β},
  IsOfFinAddOrder x → IsOfFinAddOrder x.1
-- Mathlib.Algebra.GroupWithZero.Defs
/-- `a ^ (n + 1) = a ^ n * a`  -/
CommGroupWithZero.zpow_succ' : ∀ {G₀ : Type u_2} [self : CommGroupWithZero G₀] (n : ℕ) (a : G₀), a ^ ↑n.succ = a ^ ↑n * a
-- Mathlib.FieldTheory.Differential.Basic
Differential.logDeriv_algebraMap : ∀ {F : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Differential F] [inst_3 : Differential K]
  [inst_4 : Algebra F K] [DifferentialAlgebra F K] (a : F),
  Differential.logDeriv ((algebraMap F K) a) = (algebraMap F K) (Differential.logDeriv a)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCast.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (x : Std.DHashMap.Internal.AssocList α β)
  (x_1 : Std.DHashMap.Internal.AssocList.contains a x = true),
  Std.DHashMap.Internal.AssocList.getCast a x x_1 =
    match x, x_1 with
    | Std.DHashMap.Internal.AssocList.cons k v es, h =>
      if hka : (k == a) = true then cast ⋯ v else Std.DHashMap.Internal.AssocList.getCast a es ⋯
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [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]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι),
  ((Algebra.Generators.localizationAway T g).comp P).ker ^ 2 ≤
    RingHom.ker (Algebra.Generators.compLocalizationAwayAlgHom T g P)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalStringExpr : Lean.Expr → Lean.MetaM String
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.toPartialHomeomorph_injective : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Function.Injective OpenPartialHomeomorph.toPartialHomeomorph
-- Mathlib.Topology.Inseparable
SeparationQuotient.tendsto_lift_nhdsWithin_mk : ∀ {X : Type u_1} {α : Type u_4} [inst : TopologicalSpace X] {x : X} {f : X → α}
  {hf : ∀ (x y : X), Inseparable x y → f x = f y} {s : Set (SeparationQuotient X)} {l : Filter α},
  Filter.Tendsto (SeparationQuotient.lift f hf) (nhdsWithin (SeparationQuotient.mk x) s) l ↔
    Filter.Tendsto f (nhdsWithin x (SeparationQuotient.mk ⁻¹' s)) l
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_lt_one_iff_right₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 1 < a → (a ^ n < 1 ↔ n < 0)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- The `sInf` of a union of two sets is the min of the infima of each subset, under the assumptions
that all sets are bounded below and nonempty.  -/
csInf_union : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
  BddBelow s → s.Nonempty → BddBelow t → t.Nonempty → sInf (s ∪ t) = sInf s ⊓ sInf t
-- Mathlib.Data.List.Pi
/-- Given `α : ι → Sort*`, a list `l` and a term `i`, as well as a term `a : α i` and a
function `f` such that `f j : α j` for all `j` in `l`, `Pi.cons a f` is a function `g` such
that `g k : α k` for all `k` in `i :: l`.  -/
List.Pi.cons : {ι : Type u_1} →
  [DecidableEq ι] →
    {α : ι → Sort u_2} → (i : ι) → (l : List ι) → α i → ((j : ι) → j ∈ l → α j) → (j : ι) → j ∈ i :: l → α j
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.map_append : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v w : V} (p : G.Walk u v)
  (q : G.Walk v w), SimpleGraph.Walk.map f (p.append q) = (SimpleGraph.Walk.map f p).append (SimpleGraph.Walk.map f q)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonInitializationOptions : Lean.ToJson Lean.Lsp.InitializationOptions
-- Mathlib.Algebra.Group.Embedding
mulRightEmbedding.congr_simp : ∀ {G : Type u_1} [inst : Mul G] [inst_1 : IsRightCancelMul G] (g g_1 : G),
  g = g_1 → mulRightEmbedding g = mulRightEmbedding g_1
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_fmod_unique' : ∀ {a b r q : ℤ}, b < 0 → (a.fdiv b = q ∧ a.fmod b = r ↔ r + b * q = a ∧ b < r ∧ r ≤ 0)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- Two morphisms `f : X ⟶ Z` and `g : Y ⟶ Z` have a pullback if the diagram `cospan f g` has a
limit.  -/
CategoryTheory.Limits.HasPullback : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y Z : C} → (X ⟶ Z) → (Y ⟶ Z) → Prop
-- Mathlib.Algebra.Order.GroupWithZero.Defs
posMulReflectLE_iff : ∀ (α : Type u_1) [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α],
  PosMulReflectLE α ↔ ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x1 x2 => x1 ≤ x2
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.symm_trans_source_eq : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e e' : Bundle.Trivialization F proj),
  (e.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ
-- Lean.Attributes
Lean.registerAttributeOfBuilder : Lean.Environment → Lean.Name → Lean.Name → List Lean.DataValue → IO Lean.Environment
-- Std.Data.HashSet.Iterator
/-- Returns a finite iterator over the elements of a hash set.
The iterator yields the elements of the set in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.HashSet.Raw.iter : {α : Type u} → Std.HashSet.Raw α → Std.Iter α
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.Ctx.config : Lean.Elab.Tactic.Try.Ctx → Lean.Try.Config