mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.ext_iff : ∀ {p : ENNReal} {ι : Type u_1} {α : ι → Type u_2} {x y : PiLp p α}, x = y ↔ ∀ (i : ι), x.ofLp i = y.ofLp i
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Expr.toPoly.go.match_1.eq_3 : ∀ (motive : Nat.Internal.Linear.Expr → Sort u_1) (a b : Nat.Internal.Linear.Expr)
  (h_1 : (k : ℕ) → motive (Nat.Internal.Linear.Expr.num k))
  (h_2 : (i : Nat.Internal.Linear.Var) → motive (Nat.Internal.Linear.Expr.var i))
  (h_3 : (a b : Nat.Internal.Linear.Expr) → motive (a.add b))
  (h_4 : (k : ℕ) → (a : Nat.Internal.Linear.Expr) → motive (Nat.Internal.Linear.Expr.mulL k a))
  (h_5 : (a : Nat.Internal.Linear.Expr) → (k : ℕ) → motive (a.mulR k)),
  (match a.add b with
    | Nat.Internal.Linear.Expr.num k => h_1 k
    | Nat.Internal.Linear.Expr.var i => h_2 i
    | a.add b => h_3 a b
    | Nat.Internal.Linear.Expr.mulL k a => h_4 k a
    | a.mulR k => h_5 a k) =
    h_3 a b
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.trim_withDensity : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ENNReal},
  Measurable f → (μ.withDensity f).trim hm = (μ.trim hm).withDensity f
-- Mathlib.RingTheory.LocalRing.Etale
/-- A finite étale extension of local rings is generated by a single element.
This is Lemma 3.2, part 1 of [arXiv:2503.07846](https://arxiv.org/abs/2503.07846).
The proof lifts a primitive element of the residue field extension via Nakayama's lemma.  -/
IsLocalRing.exists_adjoin_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsLocalRing S]
  [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S] [Algebra.FormallyUnramified R S], ∃ β, R[β] = ⊤
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
/-- Given a finite-dimensional subspace `W` of a space `V` with separating dual, any
linear functional on `W` extends to a continuous linear functional on `V`.
This is stated more generally for an injective linear map from `W` to `V`.  -/
SeparatingDual.dualMap_surjective_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Field R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace V] [IsTopologicalRing R] [inst_5 : Module R V] [SeparatingDual R V] {W : Type u_3}
  [inst_7 : AddCommGroup W] [inst_8 : Module R W] [FiniteDimensional R W] {f : W →ₗ[R] V},
  Function.Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap) ↔ Function.Injective ⇑f
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_hom_app_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)}
  {obj₁' obj₂' obj₃' : CategoryTheory.Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'}
  {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂')
  (iso₃ : obj₃ ≅ obj₃')
  (comm₁ : CategoryTheory.CategoryStruct.comp mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom mor₁')
  (comm₂ : CategoryTheory.CategoryStruct.comp mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom mor₂')
  (comm₃ :
    CategoryTheory.CategoryStruct.comp mor₃
        (CategoryTheory.Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp iso₃.hom mor₃')
  (j : J),
  ((CategoryTheory.Pretriangulated.Triangle.functorIsoMk' iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom.app j).hom₂ =
    iso₂.hom.app j
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
RightDerivMeasurableAux.measurableSet_B : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {K : Set F} {r s ε : ℝ},
  MeasurableSet (RightDerivMeasurableAux.B f K r s ε)
-- Mathlib.Algebra.Lie.AdjointAction.Derivation
LieDerivation.lie_ad : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x : L)
  (D : LieDerivation R L L), ⁅(LieDerivation.ad R L) x, D⁆ = ⁅x, D⁆
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.diagonalCover_map : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (𝒱 :
    (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover)
  (I : (AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱).I₀),
  (AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱).f I =
    CategoryTheory.Limits.pullback.map
      (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.1) (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f I.fst))
      (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.2) (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f I.fst))
      f f (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.1) (CategoryTheory.Limits.pullback.fst f (𝒰.f I.fst)))
      (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.2) (CategoryTheory.Limits.pullback.fst f (𝒰.f I.fst)))
      (𝒰.f I.fst) ⋯ ⋯
-- Mathlib.Algebra.Group.Defs
/-- A `AddMonoid` which `IsMulCommutative` is a `AddCommMonoid`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsAddCommutative.instAddCommMonoid : {M : Type u_2} → [inst : AddMonoid M] → [IsAddCommutative M] → AddCommMonoid M
-- Mathlib.Tactic.Ring.Common
/-- `ExSumNat e` stores the structure of a normalized polynomial expression `e : Q(ℕ)`, which is
a sum of monomials.

Used to represent normalized natural number expressions in exponents.

`ExSumNat q($e)` is equivalent to `ExSum btℕ sℕ q($e)`, and one can cast between the two.  -/
Mathlib.Tactic.Ring.Common.ExSumNat : Q(ℕ) → Type
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.congr_trans : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8}
  {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [inst_3 : AddCommMonoid M]
  [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid N₂] [inst_7 : AddCommMonoid M₃]
  [inst_8 : AddCommMonoid N₃] [inst_9 : Module R M] [inst_10 : Module R N] [inst_11 : Module R₂ M₂]
  [inst_12 : Module R₂ N₂] [inst_13 : Module R₃ M₃] [inst_14 : Module R₃ N₃] {σ₂₁ : R₂ →+* R}
  [inst_15 : RingHomInvPair σ₁₂ σ₂₁] [inst_16 : RingHomInvPair σ₂₁ σ₁₂] {σ₃₂ : R₃ →+* R₂}
  [inst_17 : RingHomInvPair σ₂₃ σ₃₂] [inst_18 : RingHomInvPair σ₃₂ σ₂₃] {σ₃₁ : R₃ →+* R}
  [inst_19 : RingHomInvPair σ₁₃ σ₃₁] [inst_20 : RingHomInvPair σ₃₁ σ₁₃] [inst_21 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  [inst_22 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] (f₂ : M₂ ≃ₛₗ[σ₂₃] M₃) (g₂ : N₂ ≃ₛₗ[σ₂₃] N₃) (f₁ : M ≃ₛₗ[σ₁₂] M₂)
  (g₁ : N ≃ₛₗ[σ₁₂] N₂),
  TensorProduct.congr (f₁.trans f₂) (g₁.trans g₂) = (TensorProduct.congr f₁ g₁).trans (TensorProduct.congr f₂ g₂)
-- Mathlib.Algebra.Homology.DerivedCategory.KProjective
CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {K L : CochainComplex C ℤ}
  {n : ℤ}
  [inst_2 :
    CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L]
  [inst_3 : K.IsKProjective] (x : CochainComplex.HomComplex.CohomologyClass K L n),
  CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective x = x.toSmallShiftedHom
-- Mathlib.Probability.Independence.BoundedContinuousFunction
/-- Two families of random variables $(X_1, ..., X_p)$ and $(Y_1, ..., Y_q)$ are independent if
for all real bounded continuous functions $f$ and $g$,
$$P[f(X_1, ..., X_p) g(Y_1, ..., Y_q)] = P[f(X_1, ..., X_p)] * P[g(Y_1, ..., Y_q)].$$  -/
pi_indepFun_pi_of_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  {F : T → Type u_5} [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)]
  [∀ (s : S), BorelSpace (E s)] [∀ (s : S), HasOuterApproxClosed (E s)] [inst_4 : (t : T) → TopologicalSpace (F t)]
  [inst_5 : (t : T) → MeasurableSpace (F t)] [∀ (t : T), BorelSpace (F t)] [∀ (t : T), HasOuterApproxClosed (F t)]
  {X : (s : S) → Ω → E s} {Y : (t : T) → Ω → F t} [MeasureTheory.IsFiniteMeasure P] [Finite S] [Finite T],
  (∀ (s : S), AEMeasurable (X s) P) →
    (∀ (t : T), AEMeasurable (Y t) P) →
      (∀ (f : BoundedContinuousFunction ((s : S) → E s) ℝ) (g : BoundedContinuousFunction ((t : T) → F t) ℝ),
          ∫ (x : Ω), (fun ω => (f fun x => X x ω) * g fun x => Y x ω) x ∂P =
            (∫ (x : Ω), (fun ω => f fun x => X x ω) x ∂P) * ∫ (x : Ω), (fun ω => g fun x => Y x ω) x ∂P) →
        ProbabilityTheory.IndepFun (fun ω s => X s ω) (fun ω t => Y t ω) P
-- Mathlib.MeasureTheory.Covering.DensityTheorem
Vitali.vitaliFamily.eq_1 : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [inst_2 : OpensMeasurableSpace α]
  [inst_3 : SecondCountableTopology α] (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ]
  (C : NNReal)
  (h :
    ∀ (x : α),
      ∃ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), μ (Metric.closedBall x (3 * r)) ≤ ↑C * μ (Metric.closedBall x r)),
  Vitali.vitaliFamily μ C h =
    {
      setsAt := fun x =>
        {a |
          IsClosed a ∧
            (interior a).Nonempty ∧ ∃ r, a ⊆ Metric.closedBall x r ∧ μ (Metric.closedBall x (3 * r)) ≤ ↑C * μ a},
      measurableSet := ⋯, nonempty_interior := ⋯, nontrivial := ⋯, covering := ⋯ }
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntry.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : x.isEmpty = false) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  (r : Std.DTreeMap.Internal.Impl α β) →
                    (x :
                        (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
                      motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (size_1 : ℕ) →
                      (k_1 : α) →
                        (v_1 : β k_1) →
                          (l r r_1 : Std.DTreeMap.Internal.Impl α β) →
                            (h :
                                (Std.DTreeMap.Internal.Impl.inner size k v
                                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
                                  false) →
                              motive
                                (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
                                h) →
              motive x x_1
-- Mathlib.Topology.Instances.AddCircle.DenseSubgroup
/-- The multiples of a number `a` are dense on a circle of length `p` iff `a / p` is irrational.  -/
AddCircle.denseRange_zsmul_coe_iff : ∀ {a p : ℝ}, (DenseRange fun x => x • ↑a) ↔ Irrational (a / p)
-- Mathlib.Tactic.CongrExclamation
Congr!.elabConfig : Lean.Syntax → optParam Congr!.Config { } → optParam Bool true → Lean.Elab.Tactic.TacticM Congr!.Config
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassP.eq_1 : ∀ (L : PeriodPair) (z : ℂ), L.derivWeierstrassP z = -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3
-- Mathlib.Analysis.Seminorm
ball_normSeminorm : ∀ (𝕜 : Type u_3) (E : Type u_7) [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E],
  (normSeminorm 𝕜 E).ball = Metric.ball
-- Std.Http.Data.Body.Stream
/-- Creates a body from a fixed byte array.
 -/
Std.Http.Body.fromBytes : ByteArray → Std.Async.Async Std.Http.Body.Stream
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_zero : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α}, Metric.ball x 0 = ∅
-- Mathlib.Topology.Separation.CompletelyRegular
CompletelyRegularSpace.of_isTopologicalBasis_clopens : ∀ {X : Type u} [inst : TopologicalSpace X],
  TopologicalSpace.IsTopologicalBasis {s | IsClopen s} → CompletelyRegularSpace X
-- Mathlib.Order.Filter.AtTopBot.Archimedean
/-- See also `Filter.Tendsto.atBot_mul_const` for a version of this lemma for
linearly ordered fields which does not require the `Archimedean` assumption.  -/
Filter.Tendsto.atBot_mul_const' : ∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [inst : Ring R] [inst_1 : LinearOrder R]
  [IsStrictOrderedRing R] [Archimedean R],
  0 < r → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x * r) l Filter.atBot
-- Mathlib.CategoryTheory.Shift.Pullback
/-- The shift on `PullbackShift C φ` is obtained by precomposing the shift on `C` with
the monoidal functor `Discrete.addMonoidalFunctor φ : Discrete A ⥤ Discrete B`.  -/
CategoryTheory.instHasShiftPullbackShift : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_2} →
      {B : Type u_3} →
        [inst_1 : AddMonoid A] →
          [inst_2 : AddMonoid B] →
            [inst_3 : CategoryTheory.HasShift C B] →
              (φ : A →+ B) → CategoryTheory.HasShift (CategoryTheory.PullbackShift C φ) A
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- If `f` is an alternating map from `M` to `N`,
`alternatingMapLinearEquiv f` is the corresponding linear map from `⋀[R]^n M` to `N`,
and if `g` is a linear map from `N` to `N'`, then
the alternating map `g.compAlternatingMap f` from `M` to `N'` corresponds to the linear
map `g.comp (alternatingMapLinearEquiv f)` on `⋀[R]^n M`.  -/
exteriorPower.alternatingMapLinearEquiv_comp : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} {N' : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : AddCommGroup N']
  [inst_6 : Module R N'] (g : N →ₗ[R] N') (f : M [⋀^Fin n]→ₗ[R] N),
  exteriorPower.alternatingMapLinearEquiv (g.compAlternatingMap f) = g ∘ₗ exteriorPower.alternatingMapLinearEquiv f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m).WF → ∀ {k a : α}, (m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a
-- Init.Data.Vector.Basic
Vector.foldr : {α : Type u_1} → {β : Type u_2} → {n : ℕ} → (α → β → β) → β → Vector α n → β
-- Mathlib.Logic.Equiv.List
/-- `List ℕ` is equivalent to `ℕ`.  -/
Equiv.listNatEquivNat : List ℕ ≃ ℕ
-- Mathlib.RepresentationTheory.Invariants
/-- The adjunction between the functor equipping a module with the trivial representation, and
the functor sending a representation to its submodule of invariants.  -/
Rep.invariantsAdjunction : (k : Type u) →
  (G : Type v) → [inst : CommRing k] → [inst_1 : Group G] → Rep.trivialFunctor k G ⊣ Rep.invariantsFunctor k G
-- Mathlib.RingTheory.Localization.Integral
/-- A ring is algebraic over the ring `A` iff it is algebraic over the field of fractions of `A`.
 -/
IsFractionRing.comap_isAlgebraic_iff : ∀ {A : Type u_3} {K : Type u_4} {C : Type u_5} [inst : CommRing A] [IsDomain A] [inst_2 : Field K]
  [inst_3 : Algebra A K] [IsFractionRing A K] [inst_5 : CommRing C] [inst_6 : Algebra A C] [inst_7 : Algebra K C]
  [IsScalarTower A K C], Algebra.IsAlgebraic A C ↔ Algebra.IsAlgebraic K C
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_symm_toHomeomorph : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), ⇑e.toHomeomorph.symm = ⇑e.symm
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
NonarchimedeanRing.mk : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [toIsTopologicalRing : IsTopologicalRing R],
  (∀ U ∈ nhds 0, ∃ V, ↑V ⊆ U) → NonarchimedeanRing R
-- Init.Grind.Offset
Lean.Grind.Nat.le_eq_true_of_le : ∀ (u v : ℕ), u ≤ v → (u ≤ v) = True
-- Mathlib.Algebra.Order.Group.Basic
zsmul_le_zsmul_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {n : ℤ} {a b : α},
  0 ≤ n → a ≤ b → n • a ≤ n • b
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.equiv_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [inst_2 : L.IsLocalization W] {X Y : C}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] (f : X ⟶ Y),
  (CategoryTheory.Localization.SmallHom.equiv W L) (CategoryTheory.Localization.SmallHom.mk W f) = L.map f
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.not_matchesAt_skipWhile : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String.Slice} (pos : s.Pos),
  ¬String.Slice.Pattern.Model.MatchesAt pat (pos.skipWhile pat)
-- Std.Time.Date.Unit.Week
/-- `Ordinal` represents the number of weeks within a month, ranging between 1 and 6.
 -/
Std.Time.Week.Ordinal : Type
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.congr_arg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  (f : X ⟶ Y) {x x' : CategoryTheory.ToType X},
  x = x' → (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom f) x'
-- Mathlib.Data.NNReal.Defs
NNReal.iSup_of_not_bddAbove : ∀ {ι : Sort u_1} {f : ι → NNReal}, ¬BddAbove (Set.range f) → ⨆ i, f i = 0
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
/-- An operation `Φ` on sections of a vector bundle `V` over `M` is *tensorial* at `x : M`, if it
respects addition and scalar multiplication by germs of differentiable functions at `f`.  -/
TensorialAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [ChartedSpace H M] →
                      (F : Type u_5) →
                        [inst_6 : NormedAddCommGroup F] →
                          [NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [(x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [FiberBundle F V] →
                                        {A : Type u_9} →
                                          [inst_13 : AddCommGroup A] → [Module 𝕜 A] → (((x : M) → V x) → A) → M → Prop
-- Mathlib.Order.SuccPred.Relation
/-- For `m ≤ n`, `(n, m)` is in the reflexive-transitive closure of `~` if `i ~ pred i`
for all `i` between `n` and `m`.  -/
reflTransGen_of_pred_of_ge : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ioc m n, r i (Order.pred i)) → m ≤ n → Relation.ReflTransGen r n m
-- Mathlib.Tactic.LinearCombination
Mathlib.Tactic.LinearCombination.Expanded.const.injEq : ∀ (c c_1 : Lean.Term),
  (Mathlib.Tactic.LinearCombination.Expanded.const c = Mathlib.Tactic.LinearCombination.Expanded.const c_1) = (c = c_1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toArray.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] (r : Std.Roi α), r.toArray = (Std.Roi.Internal.iter r).toArray
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_nil_start : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (q : G.Walk u v), SimpleGraph.Walk.nil.IsSubwalk q
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.notDefEq.injEq : ∀ (lhs : ℕ) (rhs : Lean.Meta.Grind.CnstrRHS) (lhs_1 : ℕ) (rhs_1 : Lean.Meta.Grind.CnstrRHS),
  (Lean.Meta.Grind.EMatchTheoremConstraint.notDefEq lhs rhs =
      Lean.Meta.Grind.EMatchTheoremConstraint.notDefEq lhs_1 rhs_1) =
    (lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.Spanning.eRank_restrict : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Spanning X → (M.restrict X).eRank = M.eRank
-- Batteries.Logic
congrFun₃ : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4}
  {f g : (a : α) → (b : β a) → (c : γ a b) → δ a b c}, f = g → ∀ (a : α) (b : β a) (c : γ a b), f a b c = g a b c
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
CategoryTheory.Limits.pointwiseBinaryBicone_snd_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [inst_3 : CategoryTheory.Category.{v_2, u_2} D]
  (F G : CategoryTheory.Functor D C) (X : D),
  (CategoryTheory.Limits.pointwiseBinaryBicone F G).snd.app X = CategoryTheory.Limits.biprod.snd
-- Mathlib.Algebra.Group.Indicator
Set.indicatorHom.eq_1 : ∀ {α : Type u_6} (M : Type u_7) [inst : AddZeroClass M] (s : Set α),
  Set.indicatorHom M s = { toFun := s.indicator, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isOpen_subsets_of_isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α] {U : Set α}, IsOpen U → IsOpen {K | ↑K ⊆ U}
-- Mathlib.Data.Finset.NAry
/-- Symmetric statement to `Finset.image_image₂_right_anticomm`.  -/
Finset.image_image₂_antidistrib_right : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq α']
  [inst_1 : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [inst_2 : DecidableEq δ] {g : γ → δ}
  {f' : β → α' → δ} {g' : α → α'},
  (∀ (a : α) (b : β), g (f a b) = f' b (g' a)) →
    Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' t (Finset.image g' s)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.coe_comap : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) (s : Subfield L),
  ↑(Subfield.comap f s) = ⇑f ⁻¹' ↑s
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
DirectedOn.ciSup_set_le_iff : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {ι : Type u_5} {s : Set ι} {f : ι → α} {a : α},
  s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) (f '' s) → BddAbove (f '' s) → (⨆ i, f ↑i ≤ a ↔ ∀ i ∈ s, f i ≤ a)
-- Lean.Elab.InfoTree.Types
/-- The context object is created at appropriate points during elaboration  -/
Lean.Elab.InfoTree.context : Lean.Elab.PartialContextInfo → Lean.Elab.InfoTree → Lean.Elab.InfoTree
-- Mathlib.Algebra.Opposites
AddOpposite.instIsEmpty : ∀ {α : Type u_1} [IsEmpty α], IsEmpty αᵃᵒᵖ