mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
/-- A sequence of functions `Fₙ` converges locally uniformly on a set `s` to a limiting function
`f` with respect to a filter `p` if, for any entourage of the diagonal `u`, for any `x ∈ s`, one
has `p`-eventually `(f y, Fₙ y) ∈ u` for all `y` in a neighborhood of `x` in `s`.  -/
TendstoLocallyUniformlyOn : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_4} → [TopologicalSpace α] → [UniformSpace β] → (ι → α → β) → (α → β) → Filter ι → Set α → Prop
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_comm`.

---

The Hausdorff edistances of `s` to `t` and of `t` to `s` coincide.  -/
EMetric.hausdorffEdist_comm : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α}, Metric.hausdorffEDist s t = Metric.hausdorffEDist t s
-- Mathlib.SetTheory.Ordinal.Notation
ONote.FundamentalSequenceProp.eq_1 : ∀ (o : ONote), o.FundamentalSequenceProp (Sum.inl none) = (o = 0)
-- Init.Data.String.Lemmas.Basic
String.Pos.Raw.isValidForSlice_zero : ∀ {s : String.Slice}, String.Pos.Raw.IsValidForSlice s 0
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_subset_uIcc_iff_mem : ∀ {α : Type u_1} [inst : Lattice α] {a₁ a₂ b₁ b₂ : α},
  Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂ ↔ a₁ ∈ Set.uIcc a₂ b₂ ∧ b₁ ∈ Set.uIcc a₂ b₂
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.pow_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Monoid (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)]
  (x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (n : ℕ) (i : ι), (x ^ n) i = x i ^ n
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.exists_lt_lintegral_simpleFunc_of_lt_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → NNReal}
  {L : ENNReal},
  L < ∫⁻ (x : α), ↑(f x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
-- Init.Task
_private.Init.Task.0.Task.mapList.go : {α : Type u_1} → {β : Type u_2} → (List α → β) → Task.Priority → Bool → List (Task α) → List α → Task β
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `none` if the
map is empty.
 -/
Std.DTreeMap.minEntry? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Option ((a : α) × β a)
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.RatAlgebra.dpow_eq_of_mem : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} [inst_1 : DecidablePred fun x => x ∈ I] (n : ℕ) {x : R},
  x ∈ I → DividedPowers.RatAlgebra.dpow I n x = Ring.inverse ↑n.factorial * x ^ n
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.inv_sub_one : ∀ {p q : ℝ}, p.HolderConjugate q → p⁻¹ - 1 = -q⁻¹
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).isEmpty = ((t.erase k).isEmpty && (f (Std.DTreeMap.Const.get? t k)).isNone)
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
/-- We choose `GrpCat.of (G × H)` as the product of `G` and `H` and `GrpCat.of PUnit` as
the terminal object.  -/
GrpCat.cartesianMonoidalCategoryGrp : CategoryTheory.CartesianMonoidalCategory GrpCat
-- Mathlib.GroupTheory.NoncommCoprod
/-- Coproduct of two `MonoidHom`s with the same codomain,
with a commutation assumption:
`f.noncommCoprod g _ (p : M × N) = f p.1 * g p.2`.
(Noncommutative case; in the commutative case, use `MonoidHom.coprod`.)  -/
MonoidHom.noncommCoprod : {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} →
      [inst : MulOneClass M] →
        [inst_1 : MulOneClass N] →
          [inst_2 : Monoid P] → (f : M →* P) → (g : N →* P) → (∀ (m : M) (n : N), Commute (f m) (g n)) → M × N →* P
-- Mathlib.Topology.Algebra.Ring.Basic
_private.Mathlib.Topology.Algebra.Ring.Basic.0.RingTopology.def_sInf : {R : Type u_1} → [inst : Ring R] → Set (RingTopology R) → RingTopology R
-- Lean.Parser.Command
Lean.Parser.Command.registerErrorExplanationStx.formatter : Lean.PrettyPrinter.Formatter
-- Init.Control.ExceptCps
ExceptCpsT.runK_pure : ∀ {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x : α} {s : ε} {a : Type u_1} {ok : α → m a}
  {error : ε → m a}, (pure x).runK s ok error = ok x
-- Mathlib.Logic.Encodable.Basic
/-- If `β` is encodable and there is an injection `f : α → β`, then `α` is encodable as well.  -/
Encodable.ofInj : {α : Type u_1} → {β : Type u_2} → [Encodable β] → (f : α → β) → Function.Injective f → Encodable α
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instMax : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → Max (CategoryTheory.Precoverage C)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceCastSucc : Lean.Meta.Simp.DSimproc
-- Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
/-- Measurable equivalence between the non-top elements of `WithTop ι` and `ι`.  -/
WithTop.MeasurableEquiv.neTopEquiv : {ι : Type u_1} →
  [inst : LinearOrder ι] →
    [inst_1 : TopologicalSpace ι] →
      [inst_2 : OrderTopology ι] → [inst_3 : MeasurableSpace ι] → [BorelSpace ι] → ↑{r | r ≠ ⊤} ≃ᵐ ι
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_spec : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) (n k : ℕ),
  MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg n ≤ k → μ {x | 2⁻¹ ^ n ≤ edist (f k x) (g x)} ≤ 2⁻¹ ^ n
-- Mathlib.Topology.UniformSpace.UniformEmbedding
SeparationQuotient.isUniformInducing_mk : ∀ {α : Type u} [inst : UniformSpace α], IsUniformInducing SeparationQuotient.mk
-- Mathlib.Algebra.Group.Units.Hom
IsAddUnit.addUnit_neg_map : ∀ {F : Type u_1} {M : Type u_3} {N : Type u_4} [inst : FunLike F M N] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  [inst_3 : AddMonoidHomClass F M N] (f : F) {x : M} (h : IsAddUnit x), ↑(-⋯.addUnit) = f ↑(-h.addUnit)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.equiv_equivWithAbs_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  {v w : AbsoluteValue R S} {x : WithAbs w},
  (WithAbs.equiv v) ((WithAbs.congr v w (RingEquiv.refl R)).symm x) = (WithAbs.equiv w) x
-- Mathlib.Topology.Category.LightProfinite.Extend
LightProfinite.Extend.functor_obj : ∀ {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite))
  (i : ℕᵒᵖ), (LightProfinite.Extend.functor c).obj i = CategoryTheory.StructuredArrow.mk (c.π.app i)
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Combinatorial viewpoint on a composition of `n` as consecutive integers `{0, ..., n-1}`  -/
CompositionAsSet.boundaries : {n : ℕ} → CompositionAsSet n → Finset (Fin n.succ)
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.v.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  {inst_5 : DecidableEq ι} [inst_6 : DecidableEq ι] (i i_1 : ι),
  i = i_1 →
    ∀ (a a_1 : ↥b.support ⊕ ι),
      a = a_1 → RootPairing.GeckConstruction.v b i a = RootPairing.GeckConstruction.v b i_1 a_1
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.lt_log_of_rpow_lt : ∀ {x y z : ℝ}, 0 < x → x ^ z < y → z * Real.log x < Real.log y
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.finite_setOfPred_isRoot : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {p : Polynomial R}, p ≠ 0 → {x | p.IsRoot x}.Finite
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- The limit along a Vitali family of `ρ a / μ a` where it makes sense, and garbage otherwise.
Do *not* use this definition: it is only a temporary device to show that this ratio tends almost
everywhere to the Radon-Nikodym derivative.  -/
VitaliFamily.limRatio : {α : Type u_1} →
  [inst : PseudoMetricSpace α] →
    {m0 : MeasurableSpace α} → {μ : MeasureTheory.Measure α} → VitaliFamily μ → MeasureTheory.Measure α → α → ENNReal
-- Lean.Elab.InfoTree.Types
Lean.Elab.instMonadInfoTreeOfMonadLift : {m n : Type → Type} → [MonadLift m n] → [Lean.Elab.MonadInfoTree m] → Lean.Elab.MonadInfoTree n
-- Init.Data.Bool
Bool.and_xor_distrib_right : ∀ (x y z : Bool), ((x ^^ y) && z) = (x && z ^^ y && z)
-- Mathlib.Order.Lattice
inf_le_ite : ∀ {α : Type u} [inst : SemilatticeInf α] (a b : α) (P : Prop) [inst_1 : Decidable P], a ⊓ b ≤ if P then a else b
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.trailingDegree_mul : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p q : Polynomial R},
  (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balance!.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          motive
            (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rr : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k : α) →
                (v : β k) →
                  (l r : Std.DTreeMap.Internal.Impl α β) →
                    rr = Std.DTreeMap.Internal.Impl.inner size_1 k v l r →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                          (Std.DTreeMap.Internal.Impl.inner size_1 k v l r)))
  (h_4 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (size_1 : ℕ) →
            (rlk : α) →
              (rlv : β rlk) →
                (l r : Std.DTreeMap.Internal.Impl α β) →
                  motive
                    (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                      Std.DTreeMap.Internal.Impl.leaf))
  (h_5 :
    (rs : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rls : ℕ) →
            (rlk : α) →
              (rlv : β rlk) →
                (rll rlr rr : Std.DTreeMap.Internal.Impl α β) →
                  (size : ℕ) →
                    (k : α) →
                      (v : β k) →
                        (l r : Std.DTreeMap.Internal.Impl α β) →
                          rr = Std.DTreeMap.Internal.Impl.inner size k v l r →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner rs rk rv
                                (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
                                (Std.DTreeMap.Internal.Impl.inner size k v l r))),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf =>
      h_2 size k v
    |
    Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
        rr@h:(Std.DTreeMap.Internal.Impl.inner size_1 k v l r) =>
      h_3 size rk rv rr size_1 k v l r h
    |
    Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
        Std.DTreeMap.Internal.Impl.leaf =>
      h_4 size rk rv size_1 rlk rlv l r
    |
    Std.DTreeMap.Internal.Impl.inner rs rk rv (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
        rr@h:(Std.DTreeMap.Internal.Impl.inner size k v l r) =>
      h_5 rs rk rv rls rlk rlv rll rlr rr size k v l r h) =
    h_1 ()
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.mapSnakeInput_f₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂)
  (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j),
  (HomologicalComplex.HomologySequence.mapSnakeInput φ hS₁ hS₂ i j hij).f₁ =
    (HomologicalComplex.opcyclesFunctor C c i).mapShortComplex.map φ
-- Init.Data.List.Lemmas
List.map_filter_eq_foldr : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {p : α → Bool} {as : List α},
  List.map f (List.filter p as) = List.foldr (fun a bs => bif p a then f a :: bs else bs) [] as
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.mem_vars_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R)
  {j : τ}, j ∈ ((MvPolynomial.bind₁ f) φ).vars → ∃ i ∈ φ.vars, j ∈ (f i).vars
-- Mathlib.Order.Sublattice
Sublattice.coe_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L : Sublattice α) (M : Sublattice β),
  ↑(L.prod M) = ↑L ×ˢ ↑M
-- Mathlib.Geometry.Euclidean.Altitude
/-- Extension for the `positivity` tactic: the height of a simplex is always positive.  -/
Affine.Simplex.evalHeight : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Data.Nat.Multiplicity
Nat.Prime.emultiplicity_factorial_le_div_pred : ∀ {p : ℕ}, Nat.Prime p → ∀ (n : ℕ), emultiplicity p n.factorial ≤ ↑(n / (p - 1))
-- Lean.Expr
Lean.mkForallEx : Lean.Name → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.Expr
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_mul_iff_le_two_or_omega0_opow_opow`.

---

The main characterization theorem for multiplicative principal ordinals.  -/
Ordinal.principal_mul_iff_le_two_or_omega0_opow_opow : ∀ {o : Ordinal.{u}},
  Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o ↔ o ≤ 2 ∨ o ∈ Set.range fun x => Ordinal.omega0 ^ Ordinal.omega0 ^ x
-- Mathlib.Analysis.CStarAlgebra.Projection
IsStarProjection.le_iff_idempotent_sub : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {p q : A},
  IsStarProjection p → IsStarProjection q → (p ≤ q ↔ IsIdempotentElem (q - p))
-- Mathlib.Analysis.Convolution
MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      ∀ (x : G), MeasureTheory.AEStronglyMeasurable (fun t => (L (f (x - t))) (g t)) μ
-- Mathlib.Logic.Equiv.Defs
Equiv.inhabited' : {α : Sort u} → Inhabited (α ≃ α)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.map_some : ∀ {R : Type r} {S : Type s} {F : Type u} {K : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field F]
  [inst_3 : Field K] {W' : WeierstrassCurve.Affine R} [inst_4 : DecidableEq F] [inst_5 : DecidableEq K]
  [inst_6 : Algebra R S] [inst_7 : Algebra R F] [inst_8 : Algebra S F] [inst_9 : IsScalarTower R S F]
  [inst_10 : Algebra R K] [inst_11 : Algebra S K] [inst_12 : IsScalarTower R S K] (f : F →ₐ[S] K) {x y : F}
  (h : (W'.baseChange F).Nonsingular x y),
  (WeierstrassCurve.Affine.Point.map f) (WeierstrassCurve.Affine.Point.some x y h) =
    WeierstrassCurve.Affine.Point.some (f x) (f y) ⋯
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.FunctorsInverting.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {W : CategoryTheory.MorphismProperty C} {F₁ F₂ : W.FunctorsInverting D}, F₁ = F₂ ↔ F₁.obj = F₂.obj
-- Mathlib.Order.Filter.Pointwise
Filter.smulCommClass_filter : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α γ] [inst_1 : SMul β γ] [SMulCommClass α β γ],
  SMulCommClass α β (Filter γ)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.write.injEq : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (a : Γ → σ → Γ) (a_1 : Turing.TM1.Stmt Γ Λ σ) (a_2 : Γ → σ → Γ)
  (a_3 : Turing.TM1.Stmt Γ Λ σ), (Turing.TM1.Stmt.write a a_1 = Turing.TM1.Stmt.write a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_hom_app_app_f : ∀ (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]
  (X : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D))
  (P : CategoryTheory.Idempotents.Karoubi C),
  (((CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso C D).hom.app X).app P).f = (X.map P.decompId_p).f
-- Std.Net.Addr
Std.Net.InterfaceAddress.physicalAddress : Std.Net.InterfaceAddress → Std.Net.MACAddr
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.martingale_nat : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ]
  {f : ℕ → Ω → E},
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (∀ (i : ℕ), f i =ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]) → MeasureTheory.Martingale f 𝒢 μ
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.mk.sizeOf_spec : ∀ {n : ℕ} (A : Type u) (B : A → TypeVec.{u} n), sizeOf { A := A, B := B } = 1 + sizeOf A
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.emptyWithCapacity.eq_1 : ∀ {α : Type u} {β : α → Type v} (capacity : ℕ),
  Std.DHashMap.Internal.Raw₀.emptyWithCapacity capacity =
    ⟨{ size := 0,
        buckets :=
          Array.replicate (Std.DHashMap.Internal.numBucketsForCapacity✝ capacity).nextPowerOfTwo
            Std.DHashMap.Internal.AssocList.nil },
      ⋯⟩
-- Mathlib.Order.RelIso.Set
/-- `Subrel r p` is the inherited relation on a subtype.

We could also consider a Set.Subrel r s variant for dot notation, but this ends up interacting
poorly with `simpNF`.  -/
Subrel : {α : Type u_1} → (α → α → Prop) → (p : α → Prop) → Subtype p → Subtype p → Prop
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry.param.inj : ∀ {a a_1 : Lean.IR.IRType}, Lean.IR.LocalContextEntry.param a = Lean.IR.LocalContextEntry.param a_1 → a = a_1
-- Mathlib.Logic.Encodable.Basic
/-- Failsafe variant of `decode`. `decode₂ α n` returns the preimage of `n` under `encode` if it
exists, and returns `none` if it doesn't. This requirement could be imposed directly on `decode` but
is not to help make the definition easier to use.  -/
Encodable.decode₂ : (α : Type u_3) → [Encodable α] → ℕ → Option α
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- notation for categorical coproducts  -/
CategoryTheory.Limits.«term∐_» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The spans of two sets of points in a projective space are equal if and only if each set of
points is contained in the span of the other set.  -/
Projectivization.Subspace.span_eq_span_iff : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S T : Set (Projectivization K V)},
  Projectivization.Subspace.span S = Projectivization.Subspace.span T ↔
    S ⊆ ↑(Projectivization.Subspace.span T) ∧ T ⊆ ↑(Projectivization.Subspace.span S)
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.lift_comp_of : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i → G j} (P : Type u_3) [inst_2 : CommRing P] (F : Ring.DirectLimit G f →+* P),
  Ring.DirectLimit.lift G f P (fun i => F.comp (Ring.DirectLimit.of G f i)) ⋯ = F
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_self' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x : ↥M}, IsLocalization.mk' S (↑x) x = 1
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.lift_left_add_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj B] {f g : A ⟶ B} (i : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f i) CategoryTheory.AddMonObj.add =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g i)
        CategoryTheory.AddMonObj.add →
    f = g
-- Init.Data.BitVec.Bitblast
/-- `uppcRec` is the unsigned parallel prefix, `x.uppcRec s = true` iff `x.toNat` is greater or equal
than `2 ^ (w - 1 - (s - 1))`.
 -/
BitVec.uppcRec : {w : ℕ} → BitVec w → (s : ℕ) → s < w → Bool
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sectR_prodMkRight : ∀ {α : Type u_1} {mα : MeasurableSpace α} {γ : Type u_4} {mγ : MeasurableSpace γ} (β : Type u_6)
  [inst : MeasurableSpace β] (κ : ProbabilityTheory.Kernel α γ) (b : β) {a : α},
  ((ProbabilityTheory.Kernel.prodMkRight β κ).sectR a) b = κ a
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- An induction principle for span membership.

If `p` holds for 0 and all elements of `s`,
and is preserved under addition and left and right multiplication,
then `p` holds for all elements of the span of `s`.  -/
TwoSidedIdeal.span_induction : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {s : Set R} {p : (x : R) → x ∈ TwoSidedIdeal.span s → Prop},
  (∀ (x : R) (h : x ∈ s), p x ⋯) →
    p 0 ⋯ →
      (∀ (x y : R) (hx : x ∈ TwoSidedIdeal.span s) (hy : y ∈ TwoSidedIdeal.span s), p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x : R) (hx : x ∈ TwoSidedIdeal.span s), p x hx → p (-x) ⋯) →
          (∀ (a x : R) (hx : x ∈ TwoSidedIdeal.span s), p x hx → p (a * x) ⋯) →
            (∀ (b x : R) (hx : x ∈ TwoSidedIdeal.span s), p x hx → p (x * b) ⋯) →
              ∀ {x : R} (hx : x ∈ TwoSidedIdeal.span s), p x hx
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.rank_lt_of_mem : ∀ {x y : ZFSet.{u}}, y ∈ x → y.rank < x.rank
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.comp.match_1.eq_1 : ∀ {C : Type u_1}
  (motive : CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Sort u_2)
  (_X _Y _Z : C)
  (h_1 :
    (_X _Y _Z : C) →
      motive (CategoryTheory.WithTerminal.of _X) (CategoryTheory.WithTerminal.of _Y)
        (CategoryTheory.WithTerminal.of _Z))
  (h_2 :
    (_X : C) →
      (x : CategoryTheory.WithTerminal C) →
        motive (CategoryTheory.WithTerminal.of _X) x CategoryTheory.WithTerminal.star)
  (h_3 :
    (_X : C) →
      (x : CategoryTheory.WithTerminal C) →
        motive CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of _X) x)
  (h_4 :
    (x : CategoryTheory.WithTerminal C) →
      (_Y : C) → motive x CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of _Y))
  (h_5 :
    Unit → motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.of _X, CategoryTheory.WithTerminal.of _Y, CategoryTheory.WithTerminal.of _Z with
    | CategoryTheory.WithTerminal.of _X, CategoryTheory.WithTerminal.of _Y, CategoryTheory.WithTerminal.of _Z =>
      h_1 _X _Y _Z
    | CategoryTheory.WithTerminal.of _X, x, CategoryTheory.WithTerminal.star => h_2 _X x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _X, x => h_3 _X x
    | x, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _Y => h_4 x _Y
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star => h_5 ()) =
    h_1 _X _Y _Z