mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Finset.Basic
Finset.eq_of_mem_uIcc_of_mem_uIcc : ∀ {α : Type u_2} [inst : DistribLattice α] [inst_1 : LocallyFiniteOrder α] {a b c : α},
  a ∈ Finset.uIcc b c → b ∈ Finset.uIcc a c → a = b
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `lt_sub_iff_add_lt`. -/
lt_sub_right_of_add_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b c : α}, a + b < c → a < c - b
-- Init.Data.UInt.Lemmas
UInt16.add_eq_right : ∀ {a b : UInt16}, a + b = b ↔ a = 0
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- A subgraph of a `SimpleGraph` is a subset of vertices along with a restriction of the adjacency
relation that is symmetric and is supported by the vertex subset.  They also form a bounded lattice.

Thinking of `V → V → Prop` as `Set (V × V)`, a set of darts (i.e., half-edges), then
`Subgraph.adj_sub` is that the darts of a subgraph are a subset of the darts of `G`.  -/
SimpleGraph.Subgraph : {V : Type u} → SimpleGraph V → Type u
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal.congr_simp : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {inst_1 : DecidableEq δ}
  [inst_2 : DecidableEq δ] (μ μ_1 : (i : δ) → MeasureTheory.Measure (X i)),
  μ = μ_1 →
    ∀ (s s_1 : Finset δ),
      s = s_1 →
        ∀ (f f_1 : ((i : δ) → X i) → ENNReal),
          f = f_1 → ∀ (x x_1 : (i : δ) → X i), x = x_1 → (∫⋯∫⁻_s, f ∂μ) x = (∫⋯∫⁻_s_1, f_1 ∂μ_1) x_1
-- Mathlib.Topology.Algebra.Ring.Basic
/-- A topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See `IsTopologicalSemiring.continuousNeg_of_mul`
and `IsTopologicalSemiring.toIsTopologicalRing`)  -/
IsTopologicalRing : (R : Type u_1) → [TopologicalSpace R] → [NonUnitalNonAssocRing R] → Prop
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.f_lie_v_same : ∀ {ι : 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}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι] (i : ↥b.support),
  ⁅RootPairing.GeckConstruction.f i, RootPairing.GeckConstruction.v b ↑i⁆ = RootPairing.GeckConstruction.u i
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The exceptional split Lie algebra of type e₈.  -/
LieAlgebra.e₈ : (R : Type u) → [CommRing R] → Type u
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.lipschitzOnWith_of_abs_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {ε r M : ℝ},
  ConvexOn ℝ (Metric.ball x₀ r) f →
    0 < ε → (∀ (a : E), dist a x₀ < r → |f a| ≤ M) → LipschitzOnWith (2 * M / ε).toNNReal f (Metric.ball x₀ (r - ε))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint32 : UInt32 → Lean.Compiler.LCNF.LitValue
-- Mathlib.Analysis.SpecificLimits.Normed
NormedAddCommGroup.cauchy_series_of_le_geometric' : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] {C : ℝ} {u : ℕ → α} {r : ℝ},
  r < 1 → (∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n) → CauchySeq fun n => ∑ k ∈ Finset.range (n + 1), u k
-- Lean.Meta.Basic
Lean.Meta.ProjReductionKind.yes.sizeOf_spec : sizeOf Lean.Meta.ProjReductionKind.yes = 1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_filterMap_le_size : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → Option (γ a)}, (Std.DTreeMap.filterMap f t).size ≤ t.size
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.mk.sizeOf_spec : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : SizeOf A] (dpow : ℕ → A → A)
  (dpow_null : ∀ {n : ℕ} {x : A}, x ∉ I → dpow n x = 0) (dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1)
  (dpow_one : ∀ {x : A}, x ∈ I → dpow 1 x = x) (dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow n x ∈ I)
  (dpow_add :
    ∀ {n : ℕ} {x y : A},
      x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, dpow k.1 x * dpow k.2 y)
  (dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow n (a * x) = a ^ n * dpow n x)
  (mul_dpow : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow m x * dpow n x = ↑((m + n).choose m) * dpow (m + n) x)
  (dpow_comp : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow m (dpow n x) = ↑(m.uniformBell n) * dpow (m * n) x),
  sizeOf
      { dpow := dpow, dpow_null := dpow_null, dpow_zero := dpow_zero, dpow_one := dpow_one, dpow_mem := dpow_mem,
        dpow_add := dpow_add, dpow_mul := dpow_mul, mul_dpow := mul_dpow, dpow_comp := dpow_comp } =
    1
-- Mathlib.Combinatorics.Graph.Basic
Graph.not_inc_of_notMem_edgeSet : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, e ∉ G.edgeSet → ¬G.Inc e x
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_eq_zero_of_not_injective : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M),
  ¬Function.Injective v → f v = 0
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.toSyn_degree_mul_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.toSyn (m.degree (f * g)) ≤ m.toSyn (m.degree f) + m.toSyn (m.degree g)
-- Mathlib.Algebra.RingQuot
RingQuot.natCast.eq_1 : ∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop) (n : ℕ),
  RingQuot.natCast r n = { toQuot := Quot.mk (RingQuot.Rel r) ↑n }
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.sum_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {N : Type u_3} [inst_1 : AddCommMonoid N]
  {f : SkewMonoidAlgebra k G}, (f.sum fun x x_1 => 0) = 0
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.forIn'_congr : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_8 : Monad m] {γ : Type u} {init init' : γ}
  {r r' : Std.Rio α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)}
  (hr : r = r'),
  init = init' → (∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) → forIn' r init f = forIn' r' init' f'
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.prod_le : ∀ {R : Type u} {ι : Type u_1} [inst : CommSemiring R] {s : Finset ι} {f : ι → Ideal R} {P : Ideal R},
  P.IsPrime → (s.prod f ≤ P ↔ ∃ i ∈ s, f i ≤ P)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)}
  (φ : X ⟶ Y),
  (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₄ =
    CategoryTheory.Arrow.Hom.right (CategoryTheory.Arrow.Hom.right φ)
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Given an arbitrary set `s`, then `μ (s ∩ closedBall x r) / μ (closedBall x r)` converges
to `1` when `r` tends to `0`, for almost every `x` in `s`.
This shows that almost every point of `s` is a Lebesgue density point for `s`.
A stronger version holds for measurable sets, see `ae_tendsto_measure_inter_div_of_measurableSet`.

See also `IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div`.  -/
Besicovitch.ae_tendsto_measure_inter_div : ∀ {β : Type u} [inst : MetricSpace β] [inst_1 : MeasurableSpace β] [BorelSpace β] [SecondCountableTopology β]
  [HasBesicovitchCovering β] (μ : MeasureTheory.Measure β) [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set β),
  ∀ᵐ (x : β) ∂μ.restrict s,
    Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
      (nhds 1)
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_sum_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜) (x : E), FormalMultilinearSeries.ofScalarsSum c x = ∑' (n : ℕ), c n • x ^ n
-- Mathlib.GroupTheory.PGroup
isPGroup_iff_isPGroup_prod_primeFactors : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], p ≠ 0 → (IsPGroup p G ↔ IsPGroup (p.primeFactors.prod id) G)
-- Mathlib.RingTheory.Etale.Weakly
/-- `S` is a weakly-étale `R`-algebra if both `R → S` and `S ⊗[R] S → R` are flat.
This is also called absolutely flat.  -/
Algebra.WeaklyEtale : (R : Type u_3) → (S : Type u_4) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Prop
-- Mathlib.Topology.Bornology.Basic
Bornology.ofBounded_cobounded : ∀ {α : Type u_4} (B : Set (Set α)) (empty_mem : ∅ ∈ B) (subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B)
  (union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B) (singleton_mem : ∀ (x : α), {x} ∈ B),
  Bornology.cobounded α = Filter.comk (fun x => x ∈ B) empty_mem subset_mem union_mem
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.fstFunctor_map : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {X_1 Y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (f : X_1 ⟶ Y), (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.fstFunctor F G X).map f = f.fst
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
/-- The base change map for linear maps with source a free finite module.  -/
IsBaseChange.linearMapLeftRightHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {M : Type u_3} →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                {N : Type u_4} →
                  [inst_5 : AddCommMonoid N] →
                    [inst_6 : Module R N] →
                      {P : Type u_5} →
                        [inst_7 : AddCommMonoid P] →
                          [inst_8 : Module R P] →
                            {Q : Type u_6} →
                              [inst_9 : AddCommMonoid Q] →
                                [inst_10 : Module R Q] →
                                  [inst_11 : Module S P] →
                                    [inst_12 : IsScalarTower R S P] →
                                      [inst_13 : Module S Q] →
                                        [inst_14 : IsScalarTower R S Q] →
                                          {α : M →ₗ[R] P} → IsBaseChange S α → (N →ₗ[R] Q) → (M →ₗ[R] N) →ₗ[R] P →ₗ[S] Q
-- Mathlib.Order.Basic
min_rec' : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α} (p : α → Prop), p a → p b → p (min a b)
-- Init.Grind.Ordered.Order
Lean.Grind.Preorder.not_gt_of_lt : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b : α}, a < b → ¬a > b
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg.eq_1 : ∀ (i : Int16), i.toNatClampNeg = i.toInt.toNat
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- Given a commutative ring `R` and an `R`-algebra `A`, the *spectrum* of `a : A`
is the `Set R` consisting of those `r : R` for which `r•1 - a` is not a unit of the
algebra `A`.

The spectrum is simply the complement of the resolvent set.  -/
spectrum : (R : Type u) → {A : Type v} → [inst : CommSemiring R] → [inst_1 : Ring A] → [Algebra R A] → A → Set R
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.preimage_image : ∀ {𝕜 : 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] (I : ModelWithCorners 𝕜 E H) (s : Set H),
  ↑I ⁻¹' ↑I '' s = s
-- Init.Data.UInt.Lemmas
UInt64.toUInt64_toUInt16 : ∀ (n : UInt64), n.toUInt16.toUInt64 = n % 65536
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.sl2SubmoduleOfRoot_ne_bot : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [inst_6 : LieModule.IsTriangularizable K (↥H) L] [inst_7 : CharZero K]
  (α : LieModule.Weight K (↥H) L) (hα : α.IsNonZero), LieAlgebra.IsKilling.sl2SubmoduleOfRoot hα ≠ ⊥
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.IntegrableOn.comp_neg_Ioi : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : PartialOrder G] [inst_3 : AddCommGroup G] [IsOrderedAddMonoid G] [MeasurableNeg G] [μ.IsNegInvariant]
  {c : G} {f : G → F},
  MeasureTheory.IntegrableOn f (Set.Iio (-c)) μ → MeasureTheory.IntegrableOn (fun x => f (-x)) (Set.Ioi c) μ
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- The topology on a topological semiring `R` agrees with the module topology when considering
`R` as an `R`-module in the obvious way (i.e., via `Semiring.toModule`).  -/
IsTopologicalSemiring.toIsModuleTopology : ∀ (R : Type u_1) [inst : Semiring R] [τR : TopologicalSpace R] [IsTopologicalSemiring R], IsModuleTopology R R
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.eraseJoinPointDecl : Lean.IR.LocalContext → Lean.IR.JoinPointId → Lean.IR.LocalContext
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.toLinearMap_smul : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (a : A) (f : ρ.IntertwiningMap σ),
  (a • f).toLinearMap = a • f.toLinearMap
-- Mathlib.LinearAlgebra.Matrix.Invertible
Matrix.add_mul_mul_mul_invOf_eq_one' : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] [inst_4 : Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α)
  [inst_5 : Invertible A] [inst_6 : Invertible (C + C * V * ⅟A * U * C)],
  (⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A) * (A + U * C * V) = 1
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.affineCombinationLineMapWeights.congr_simp : ∀ {k : Type u_1} [inst : Ring k] {ι : Type u_4} {inst_1 : DecidableEq ι} [inst_2 : DecidableEq ι] (i i_1 : ι),
  i = i_1 →
    ∀ (j j_1 : ι),
      j = j_1 →
        ∀ (c c_1 : k),
          c = c_1 →
            ∀ (a a_1 : ι),
              a = a_1 →
                Finset.affineCombinationLineMapWeights i j c a = Finset.affineCombinationLineMapWeights i_1 j_1 c_1 a_1
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.dist_vadd_Lp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f g : ↥(MeasureTheory.Lp E p μ)), dist (c +ᵥ f) (c +ᵥ g) = dist f g
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- Composition as an additive monoid homomorphism.  -/
ZeroAtInftyContinuousMap.compAddMonoidHom : {β : Type v} →
  {γ : Type w} →
    {δ : Type u_2} →
      [inst : TopologicalSpace β] →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : TopologicalSpace δ] →
            [inst_3 : AddMonoid δ] →
              [inst_4 : ContinuousAdd δ] →
                CocompactMap β γ → ZeroAtInftyContinuousMap γ δ →+ ZeroAtInftyContinuousMap β δ
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorem.priority : Lean.Meta.SimpCongrTheorem → ℕ
-- Mathlib.Data.ENNReal.Basic
/-- The extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure.  -/
ENNReal : Type
-- Mathlib.Topology.ContinuousMap.Polynomial
/-- The preimage of polynomials on `[0,1]` under the pullback map by `x ↦ (b-a) * x + a`
is the polynomials on `[a,b]`.  -/
polynomialFunctions.comap_compRightAlgHom_iccHomeoI : ∀ (a b : ℝ) (h : a < b),
  Subalgebra.comap (ContinuousMap.compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions unitInterval) =
    polynomialFunctions (Set.Icc a b)
-- Lean.Data.Options
Lean.instInhabitedOption : {a : Type} → [Inhabited a] → Inhabited (Lean.Option a)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Sentence.realize_cardGe : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] (n : ℕ),
  M ⊨ FirstOrder.Language.Sentence.cardGe L n ↔ ↑n ≤ Cardinal.mk M
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- `SignedMeasure.toMeasureOfLEZero` is a finite measure.  -/
MeasureTheory.SignedMeasure.toMeasureOfLEZero_finite : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) {i : Set α}
  (hi : MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i) (hi₁ : MeasurableSet i),
  MeasureTheory.IsFiniteMeasure (s.toMeasureOfLEZero i hi₁ hi)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.updateCell.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α)
  (f f_1 : Std.DTreeMap.Internal.Cell α β (compare k) → Std.DTreeMap.Internal.Cell α β (compare k)),
  f = f_1 →
    ∀ (l : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced),
      Std.DTreeMap.Internal.Impl.updateCell k f l hl = Std.DTreeMap.Internal.Impl.updateCell k f_1 l hl
-- Init.LawfulBEqTactics
DerivingHelpers.deriving_lawful_beq_helper_nd : ∀ {α : Type u_1} {x y : α} [inst : BEq α] [ReflBEq α] {P : Prop},
  ((x == y) = true → x = y) → (x = y → P) → (x == y) = true → P
-- Mathlib.Order.Filter.Basic
Filter.set_eventuallyLE_iff_inf_principal_le : ∀ {α : Type u} {s t : Set α} {l : Filter α}, s ≤ᶠ[l] t ↔ l ⊓ Filter.principal s ≤ l ⊓ Filter.principal t
-- Init.Data.SInt.Bitwise
Int16.xor_assoc : ∀ (a b c : Int16), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
-- Mathlib.Algebra.Order.Interval.Basic
Interval.mulOneClass : {α : Type u_2} → [inst : CommMonoid α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → MulOneClass (Interval α)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.exact_δ_map : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  Function.Exact ⇑(Algebra.Generators.H1Cotangent.δ Q P) ⇑(KaehlerDifferential.mapBaseChange R S T)
-- Init.Data.String.PosRaw
String.Pos.Raw.add_byteIdx : ∀ {p₁ p₂ : String.Pos.Raw}, (p₂.offsetBy p₁).byteIdx = p₁.byteIdx + p₂.byteIdx
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.nonempty_finset : ∀ {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)), (SimplexCategory.II.finset f x).Nonempty
-- Mathlib.Computability.Primrec.List
/-- An alternative inductive definition of `Primrec` which
does not use the pairing function on ℕ, and so has to
work with n-ary functions on ℕ instead of unary functions.
We prove that this is equivalent to the regular notion
in `to_prim` and `of_prim`.  -/
Nat.Primrec' : {n : ℕ} → (List.Vector ℕ n → ℕ) → Prop
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_eq_mul_of_div_eq_div : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {b d : G₀} (a c : G₀), b ≠ 0 → d ≠ 0 → a / b = c / d → a * d = c * b
-- Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
IsSepClosed.hasEnoughRootsOfUnity_pow : ∀ (F : Type u_1) [inst : Field F] (n k : ℕ) [NeZero ↑n] [IsSepClosed F], HasEnoughRootsOfUnity F (n ^ k)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.dist_le_iff_of_nonempty : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β} {C : ℝ} [Nonempty α], dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The left Kan extension of `g` along `f`.  -/
CategoryTheory.Bicategory.lan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → (f : a ⟶ b) → (g : a ⟶ c) → [CategoryTheory.Bicategory.HasLeftKanExtension f g] → b ⟶ c
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H0Iso.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.H0Iso A = (groupHomology.inhomogeneousChains A).isoHomologyι₀ ≪≫ groupHomology.opcyclesIso₀ A
-- Mathlib.Topology.MetricSpace.Cover
/-- **Alias** of `Metric.isCover_iff_subset_iUnion_closedEBall`. -/
Metric.isCover_iff_subset_iUnion_emetricClosedBall : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {s N : Set X},
  Metric.IsCover ε s N ↔ s ⊆ ⋃ y ∈ N, Metric.closedEBall y ↑ε
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionParams.toPartialResultParams : Lean.Lsp.CodeActionParams → Lean.Lsp.PartialResultParams
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append.eq_1 : ∀ {m n : ℕ} {α : Sort u_1} (a : Fin m → α) (b : Fin n → α), Fin.append a b = Fin.addCases a b
-- Init.Grind.Lemmas
Lean.Grind.Bool.eq_false_of_or_eq_false_left : ∀ {a b : Bool}, (a || b) = false → a = false
-- Init.Prelude
/-- Implementation of `TSyntaxArray.raw`.  -/
Lean.TSyntaxArray.rawImpl : {ks : Lean.SyntaxNodeKinds} → Lean.TSyntaxArray ks → Array Lean.Syntax
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.Tendsto.cauchySeq : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : SemilatticeSup β] [Nonempty β] {f : β → α} {x : α},
  Filter.Tendsto f Filter.atTop (nhds x) → CauchySeq f
-- Mathlib.SetTheory.ZFC.Class
Class.eq_univ_of_forall : ∀ {A : Class.{u}}, (∀ (x : ZFSet.{u}), A x) → A = Class.univ
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toList_roc' : ∀ {m n k : ℤ}, List.map (fun x => k + x) (m<...=n).toList = ((k + m)<...=k + n).toList
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tsum_of_add_one_of_neg_add_one : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : ℤ → M},
  (Summable fun n => f (↑n + 1)) →
    (Summable fun n => f (-(↑n + 1))) → ∑' (n : ℤ), f n = ∑' (n : ℕ), f (↑n + 1) + f 0 + ∑' (n : ℕ), f (-(↑n + 1))
-- Mathlib.Data.Set.Function
Function.Semiconj.mapsTo_preimage : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β},
  Function.Semiconj f fa fb → ∀ {s t : Set β}, Set.MapsTo fb s t → Set.MapsTo fa (f ⁻¹' s) (f ⁻¹' t)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrp_obj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (A : CategoryTheory.AddGrp C),
  (F.mapAddGrp.obj A).X = F.obj A.X
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_loopless : ∀ {α : Type u_1} (M : Matroid α), M.removeLoops.Loopless
-- Mathlib.Topology.Order.LocalExtr
/-- `IsLocalMax f a` means that `f x ≤ f a` for all `x ∈ s` in some neighborhood of `a`.  -/
IsLocalMax : {α : Type u} → {β : Type v} → [TopologicalSpace α] → [Preorder β] → (α → β) → α → Prop
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Context.mk : Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.VarSet → Bool → Lean.Elab.Term.Do.ToCodeBlock.Context
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.rightIso_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {R₁ : CategoryTheory.Functor B T}
  {L₁ : CategoryTheory.Functor A T} {X Y : CategoryTheory.Comma L₁ R₁} (α : X ≅ Y),
  (CategoryTheory.Comma.rightIso α).hom = α.hom.right