mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- The Dirac vector measure with mass `v` at a point `x`. It gives mass `v` to measurable sets
containing `x`, and `0` otherwise.  -/
MeasureTheory.VectorMeasure.dirac : {β : Type u_2} →
  {M : Type u_3} →
    [inst : AddCommMonoid M] →
      [inst_1 : TopologicalSpace M] → [inst_2 : MeasurableSpace β] → β → M → MeasureTheory.VectorMeasure β M
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.mem_toArray_iff_mem : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α] {a : α}, a ∈ r.toArray ↔ a ∈ r
-- Std.Do.Triple.SpecLemmas
/-- The type of loop invariants used by the specifications of `for ... in ...` loops.
A loop invariant is a `PostCond` that takes as parameters

* A `List.Cursor xs` representing the iteration state of the loop. It is parameterized by the list
  of elements `xs` that the `for` loop iterates over.
* A state tuple of type `β`, which will be a nesting of `MProd`s representing the elaboration of
  `let mut` variables and early return.

The loop specification lemmas will use this in the following way:
Before entering the loop, the cursor's prefix is empty and the suffix is `xs`.
After leaving the loop, the cursor's prefix is `xs` and the suffix is empty.
During the induction step, the invariant holds for a suffix with head element `x`.
After running the loop body, the invariant then holds after shifting `x` to the prefix.
 -/
Std.Do.Invariant : {α : Type u₁} → List α → Type u₂ → Std.Do.PostShape → Type (max u₂ u₁)
-- Mathlib.Data.Fintype.Quotient
/-- Given a function that for each `i : ι` gives a term of the corresponding
truncation type, then there is corresponding term in the truncation of the product.  -/
Trunc.finChoice : {ι : Type u_1} → [DecidableEq ι] → [Fintype ι] → {α : ι → Sort u_2} → ((i : ι) → Trunc (α i)) → Trunc ((i : ι) → α i)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂).getKey k h_mem = m₁.getKey k ⋯
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- The uniform structure associated with `ContinuousLinearMap.strongTopology`. We make sure
that this has nice definitional properties.  -/
UniformConvergenceCLM.instUniformSpace : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {E : Type u_3} →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜₁ E] →
                  [inst_4 : TopologicalSpace E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : Module 𝕜₂ F] →
                        [inst_7 : UniformSpace F] →
                          [IsUniformAddGroup F] → (𝔖 : Set (Set E)) → UniformSpace (UniformConvergenceCLM σ F 𝔖)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The fifth simplicial identity  -/
SimplexCategory.σ_comp_σ : ∀ {n : ℕ} {i j : Fin (n + 1)},
  i ≤ j →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i.castSucc) (SimplexCategory.σ j) =
      CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j.succ) (SimplexCategory.σ i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
ContinuousOn.arccos : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℝ} {s : Set X},
  ContinuousOn f s → ContinuousOn (fun x => Real.arccos (f x)) s
-- Mathlib.AlgebraicGeometry.Sites.Proetale
/-- The (small) pro-étale site of a scheme `S`: Its objects are the schemes weakly étale over `S`.
We prefer to work with weakly étale morphisms instead of pro-étale morphisms, since the property
of being pro-étale is not well-behaved: it is not local on the target.
[Definition 4.1.1][proetale2015]
 -/
AlgebraicGeometry.Scheme.ProEt : AlgebraicGeometry.Scheme → Type (u + 1)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), PowerSeries.coeff n = MvPowerSeries.coeff fun₀ | () => n
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
/-- [Stacks Tag 09GH](https://stacks.math.columbia.edu/tag/09GH) -/
fg_adjoin_of_finite : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {s : Set A},
  s.Finite → (∀ x ∈ s, IsIntegral R x) → (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobeniusPolyRat.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (n n_1 : ℕ),
  n = n_1 → WittVector.frobeniusPolyRat p n = WittVector.frobeniusPolyRat p_1 n_1
-- Mathlib.Order.WithBot
WithBot.ofDual_symm : ∀ {α : Type u_1}, WithBot.ofDual.symm = WithTop.toDual
-- Mathlib.Topology.Maps.Basic
Topology.IsQuotientMap.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsQuotientMap g → Topology.IsQuotientMap f → Topology.IsQuotientMap (g ∘ f)
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Set
Std.IterM.toExtTreeSet_eq_ofList : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {cmp : β → β → Ordering} [inst_6 : Std.TransCmp cmp],
  it.toExtTreeSet cmp = (fun x => Std.ExtTreeSet.ofList x cmp) <$> it.toList
-- Mathlib.Data.Set.Prod
Set.prod_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {f : γ → α} {g : δ → β},
  (f ⁻¹' s) ×ˢ (g ⁻¹' t) = (fun p => (f p.1, g p.2)) ⁻¹' s ×ˢ t
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.symm_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.symm.h₃ = -h.h₃
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMapBilinear_apply_apply : ∀ {R : Type u_1} {S : Type u_2} {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10}
  {n : Type u_11} {p : Type u_12} [inst : Semiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid α]
  [inst_3 : AddCommMonoid β] [inst_4 : AddCommMonoid γ] [inst_5 : Module R α] [inst_6 : Module R γ]
  [inst_7 : Module S β] [inst_8 : Module S γ] [inst_9 : SMulCommClass S R γ] (f : α →ₗ[R] β →ₗ[S] γ)
  (m_1 : Matrix l m α) (B : Matrix n p β),
  ((Matrix.kroneckerMapBilinear f) m_1) B = Matrix.kroneckerMap (fun r s => (f r) s) m_1 B
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [inst_5 : CategoryTheory.Limits.PreservesLimitsOfShape J F]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G).hom
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.limit.π G j) F) =
    CategoryTheory.Limits.limit.π (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.homologyπ_extendHomologyIso_hom_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'] {Z : C} (h : K.homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((K.extend e).homologyπ j')
      (CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').hom h) =
    CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom
      (CategoryTheory.CategoryStruct.comp (K.homologyπ j) h)
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.toContinuousMap_injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Function.Injective LocallyConstant.toContinuousMap
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_eq_addOrderOf_iff : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {H : Type u_6} [inst_1 : AddMonoid H] {y : H},
  addOrderOf x = addOrderOf y ↔ ∀ (n : ℕ), n • x = 0 ↔ n • y = 0
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Methods.dpre : Lean.Meta.Simp.Methods → Lean.Meta.Simp.DSimproc
-- Init.Data.Array.Attach
/-- Implementation of `pmap` using the zero-copy version of `attach`.  -/
Array.pmapImpl : {α : Type u_1} → {β : Type u_2} → {P : α → Prop} → ((a : α) → P a → β) → (xs : Array α) → (∀ a ∈ xs, P a) → Array β
-- Mathlib.Algebra.Torsor.Defs
/-- Subtracting two points in the reverse order produces the negation
of subtracting them.  -/
neg_vsub_eq_vsub_rev : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p₁ p₂ : P), -(p₁ -ᵥ p₂) = p₂ -ᵥ p₁
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.brecOn_1.eq : ∀ {α : Type u} {motive_1 : Lean.PersistentArrayNode α → Sort u_1}
  {motive_2 : Array (Lean.PersistentArrayNode α) → Sort u_1} {motive_3 : List (Lean.PersistentArrayNode α) → Sort u_1}
  (t : Array (Lean.PersistentArrayNode α)) (F_1 : (t : Lean.PersistentArrayNode α) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.PersistentArrayNode α)) → Lean.PersistentArrayNode.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.PersistentArrayNode α)) → Lean.PersistentArrayNode.below_2 t → motive_3 t),
  Lean.PersistentArrayNode.brecOn_1 t F_1 F_2 F_3 = F_2 t (Lean.PersistentArrayNode.brecOn_1.go t F_1 F_2 F_3).2
-- Mathlib.Data.ENNReal.Operations
ENNReal.toReal_sInf : ∀ (s : Set ENNReal), (∀ r ∈ s, r ≠ ⊤) → (sInf s).toReal = sInf (ENNReal.toReal '' s)
-- Lean.Meta.CoeAttr
/-- Information associated to a coercion function to enable sensible delaboration.  -/
Lean.Meta.CoeFnInfo : Type
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.equivWithVal_symm_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] {Γ'₀ : Type u_3}
  [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation R Γ₀) (w : Valuation R Γ'₀) {x : WithVal w},
  (WithVal.congr v w (RingEquiv.refl R)).symm x = (WithVal.equiv v).symm ((WithVal.equiv w) x)
-- Init.Data.Int.Gcd
Int.gcd_sub_self_left : ∀ (m n : ℤ), (n - m).gcd m = n.gcd m
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- **Bézout's lemma**  -/
exists_gcd_eq_mul_add_mul : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] [IsDomain R] [inst_3 : GCDMonoid R] (a b : R),
  ∃ x y, gcd a b = a * x + b * y
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_fst_prod' : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {l : Filter α} {f' : α → E' × F'}, (fun x => (f' x).1) =O[l] f'
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsRegular.of_isWeaklyRegular_of_mem_maximalIdeal : ∀ {R : Type u_7} [inst : CommRing R] [inst_1 : IsLocalRing R] (L : Type u_8) [inst_2 : AddCommGroup L]
  [inst_3 : Module R L] [Module.Finite R L] [Nontrivial L] {rs : List R},
  (∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R) →
    RingTheory.Sequence.IsWeaklyRegular L rs → RingTheory.Sequence.IsRegular L rs
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuous_ciInf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Sort u_4} {δ' : Type u_6}
  [inst_1 : ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'},
  (∀ (x : α), BddBelow (Set.range fun i => f i x)) →
    (∀ (i : ι), UpperSemicontinuous (f i)) → UpperSemicontinuous fun x' => ⨅ i, f i x'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_insertIfNew_le_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {v : β} {km kmi : α}, t.minKey? = some km → (t.insertIfNew k v).minKey?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.apply_of_lt_skipPrefixWhile_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos : s.Pos} (h : pos < s.skipPrefixWhile P),
  P (pos.get ⋯)
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
completeIntegralClosure_eq_integralClosure : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsNoetherianRing R]
  [IsDomain R] [IsFractionRing R S], completeIntegralClosure R S = integralClosure R S
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.δ_μ_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.Monoidal] (X Y : C) {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y) h) =
    h
-- Mathlib.Analysis.Convex.MetricSpace
/-- **Alias** of `Convexity.IsConvexDist`.

---

A convex metric space is a real convex space with a compatible metric structure.
Concretely, we ask for `dist(∑ tᵢ xᵢ, ∑ tᵢ yᵢ) ≤ ∑ tᵢ dist(xᵢ, yᵢ)`,
which is what one would expect from the triangle inequality.

In particular, convex subsets of normed affine spaces are convex metric spaces.

Note that there is a separate notion of
[convex metric spaces](https://en.wikipedia.org/wiki/Convex_metric_space) in the literature
that has little to do with this definition.  -/
Convexity.IsConvexMetricSpace : (X : Type u_2) → [inst₁ : Convexity.ConvexSpace ℝ X] → [inst₂ : MetricSpace X] → Prop
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.otherVertexOfIncident.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] {v : V} {e : Sym2 V} (h : e ∈ G.incidenceSet v),
  G.otherVertexOfIncident h = Sym2.Mem.other' ⋯
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_le_castPred_iff : ∀ {n : ℕ} {i j : Fin (n + 1)} {hi : i ≠ Fin.last n} {hj : j ≠ Fin.last n}, i.castPred hi ≤ j.castPred hj ↔ i ≤ j
-- Mathlib.Data.ENNReal.Operations
ENNReal.image_coe_uIcc : ∀ (x y : NNReal), ENNReal.ofNNReal '' Set.uIcc x y = Set.uIcc ↑x ↑y
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.lift_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x)
  (X : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.lift F M hM).obj X =
    match X with
    | CategoryTheory.WithTerminal.of x => F.obj x
    | CategoryTheory.WithTerminal.star => Z
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.rootNumber.congr_simp : ∀ {N : ℕ} [inst : NeZero N] (χ χ_1 : DirichletCharacter ℂ N), χ = χ_1 → χ.rootNumber = χ_1.rootNumber
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_mono : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K K' : Subgroup N},
  K ≤ K' → Subgroup.comap f K ≤ Subgroup.comap f K'
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.eq_of_add_pow : ∀ {α : Type u_1} {a a' b b' : α} [inst : Ring α] [IsReduced α] (n : ℕ), a = b → (a' - b') ^ n - (a - b) = 0 → a' = b'
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.ofFintype.congr_simp : ∀ {α : Type u_1} [inst : Fintype α] (f f_1 : α → ENNReal) (e_f : f = f_1) (h : ∑ a, f a = 1),
  PMF.ofFintype f h = PMF.ofFintype f_1 ⋯
-- Mathlib.Order.Partition.Equipartition
Finpartition.IsEquipartition.card_part_eq_average_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {P : Finpartition s},
  P.IsEquipartition → t ∈ P.parts → (t.card = s.card / P.parts.card ↔ t.card ≠ s.card / P.parts.card + 1)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_doubleL : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (rs : ℕ) (rk : α) (rv : β rk)
  (rls : ℕ) (rlk : α) (rlv : β rlk) (rll rlr rr : Std.DTreeMap.Internal.Impl α β),
  l.Balanced →
    (Std.DTreeMap.Internal.Impl.inner rs rk rv (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr) rr).Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size rs ∨
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond rs l.size →
        rs > Std.DTreeMap.Internal.delta * l.size →
          ¬rls < Std.DTreeMap.Internal.ratio * rr.size →
            (Std.DTreeMap.Internal.Impl.doubleL k v l rk rv rlk rlv rll rlr rr).Balanced
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getValueCast?.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List ((a : α) × β a) → Sort u_3) (k : α) (v : β k)
  (l : List ((a : α) × β a)) (h_1 : Unit → motive [])
  (h_2 : (k : α) → (v : β k) → (l : List ((a : α) × β a)) → motive (⟨k, v⟩ :: l)),
  (match ⟨k, v⟩ :: l with
    | [] => h_1 ()
    | ⟨k, v⟩ :: l => h_2 k v l) =
    h_2 k v l
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.expand_one_apply : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (f : MvPowerSeries σ R), (MvPowerSeries.expand 1 ⋯) f = f
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.inrₗ_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β] (a : β), (OrderAddMonoidHom.inrₗ α β) a = toLex (0, a)
-- Mathlib.RingTheory.Etale.Locus
Algebra.mem_etaleLocus_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {p : PrimeSpectrum A},
  p ∈ Algebra.etaleLocus R A ↔ Algebra.IsEtaleAt R p.asIdeal
-- Mathlib.Data.Multiset.Antidiagonal
Multiset.antidiagonal_add : ∀ {α : Type u_1} (s t : Multiset α),
  (s + t).antidiagonal = s.antidiagonal.bind fun p => Multiset.map (fun q => (p.1 + q.1, p.2 + q.2)) t.antidiagonal
-- Mathlib.Analysis.Calculus.LHopital
/-- **L'Hôpital's rule** for approaching +∞, `deriv` version  -/
deriv.lhopital_zero_atTop : ∀ {l : Filter ℝ} {f g : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in Filter.atTop, DifferentiableAt ℝ f x) →
    (∀ᶠ (x : ℝ) in Filter.atTop, deriv g x ≠ 0) →
      Filter.Tendsto f Filter.atTop (nhds 0) →
        Filter.Tendsto g Filter.atTop (nhds 0) →
          Filter.Tendsto (fun x => deriv f x / deriv g x) Filter.atTop l →
            Filter.Tendsto (fun x => f x / g x) Filter.atTop l
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- Open immersions are stable under base-change.  -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_of_left : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Analysis.Normed.Order.Lattice
continuous_posPart : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α],
  Continuous posPart
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instFromJsonDiagnosticSeverity : Lean.FromJson Lean.Lsp.DiagnosticSeverity
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors_one : ArithmeticFunction.cardFactors 1 = 0
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_iSup : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {κ : Sort u_4}
  (s : κ → HomogeneousIdeal 𝒜), (⨆ i, s i).toIdeal = ⨆ i, (s i).toIdeal
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.gcdA_zero_left : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] {s : R}, EuclideanDomain.gcdA 0 s = 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m₁ \ m₂).getKey? k = if k ∈ m₂ then none else m₁.getKey? k
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.HasLimits.limit_π_homDiagram_eqToHom : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat}
  (X Y : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) (j : J) (h : X = Y),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j))
      (CategoryTheory.eqToHom h) =
    CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Tropical.Basic
Tropical.add_eq_left_iff : ∀ {R : Type u} [inst : LinearOrder R] {x y : Tropical R}, x + y = x ↔ x ≤ y
-- Mathlib.Data.Rel
SetRel.cod_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, R.cod = ∅ ↔ R = ∅
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃ : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (self : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r : ℤ) (pq : κ)
  (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_9),
  self.i₂ pq ≤ self.i₃ r pq ⋯
-- Mathlib.Data.Matrix.Basis
Matrix.map_single : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n) (a : α) {β : Type u_10} [inst_3 : Zero β] {F : Type u_11} [inst_4 : FunLike F α β] [ZeroHomClass F α β]
  (f : F), (Matrix.single i j a).map ⇑f = Matrix.single i j (f a)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.symm_symm : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), e.symm.symm = e
-- Lean.ExtraModUses
Lean.getIndirectModUses : Lean.Environment → Lean.ModuleIdx → Array Lean.IndirectModUse
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAt.isTheta_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E},
  HasFDerivAt f f' x → Topology.IsInducing ⇑f' → (fun x_1 => f x_1 - f x) =Θ[nhds x] fun x_1 => x_1 - x
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
ContinuousLinearMap.bound_of_antilipschitz : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : Ring 𝕜₂]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜₂ F]
  {σ : 𝕜 →+* 𝕜₂} (f : E →SL[σ] F) {K : NNReal}, AntilipschitzWith K ⇑f → ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖