mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.HahnSeries.Multiplication
/-- `C a` is the constant Hahn Series `a`. `C` is provided as a ring homomorphism.  -/
HahnSeries.C : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [inst_2 : IsOrderedCancelAddMonoid Γ] → [inst_3 : NonAssocSemiring R] → R →+* HahnSeries Γ R
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
/-- This is the principal ideal generated by `X` in the ring of polynomials over a field K,
regarded as an element of the height-one-spectrum.  -/
Polynomial.idealX : (K : Type u_1) → [inst : Field K] → IsDedekindDomain.HeightOneSpectrum (Polynomial K)
-- Init.Data.UInt.Lemmas
USize.ofNatTruncate_uInt32ToNat : ∀ (n : UInt32), USize.ofNatClamp n.toNat = n.toUSize
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.residue_surjective : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑X.toTopCat),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (X.residue x))
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- Same as `get?_zero_mul_tail_prod`, but avoiding the `List.headI` garbage complication by
requiring the list to be nonempty.  -/
List.headI_mul_tail_prod_of_ne_nil : ∀ {M : Type u_4} [inst : Monoid M] [inst_1 : Inhabited M] (l : List M), l ≠ [] → l.headI * l.tail.prod = l.prod
-- Mathlib.Order.Antisymmetrization
not_gt_of_antisymmRel : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → ¬b < a
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- The norm structure on `Matrix m n 𝕜` arising from the operator norm given by the identification
with (continuous) linear maps of `EuclideanSpace`.  -/
Matrix.instL2OpNormedAddCommGroup : {𝕜 : Type u_1} →
  {m : Type u_2} →
    {n : Type u_3} → [RCLike 𝕜] → [Fintype m] → [Fintype n] → [DecidableEq n] → NormedAddCommGroup (Matrix m n 𝕜)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1CoresCoinfOfTrivial_X₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal]
  [inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)],
  (groupHomology.H1CoresCoinfOfTrivial A S).X₂ = groupHomology.H1 A
-- Aesop.RuleTac.Basic
/-- If the rule is indexed, the locations (i.e. hyps or the target) matched by
the rule's index entries. Otherwise an empty set. The array contains no
duplicates.  -/
Aesop.RuleTacInput.indexMatchLocations : Aesop.RuleTacInput → Array Aesop.IndexMatchLocation
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.instPartialOrder : {R : Type u} →
  {M : Type v} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → PartialOrder (Submodule R M)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.empty_presheaf : AlgebraicGeometry.Scheme.empty.presheaf =
  (CategoryTheory.Functor.const (TopologicalSpace.Opens ↑(TopCat.of PEmpty.{u_1 + 1}))ᵒᵖ).obj
    (CommRingCat.of PUnit.{u_1 + 1})
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'Map_comp : ∀ {ι : 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]
  {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [inst_2 : e.IsTruncLE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : ∀ (i' : ι'), M.HasHomology i'],
  HomologicalComplex.truncLE'Map (CategoryTheory.CategoryStruct.comp φ φ') e =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncLE'Map φ e) (HomologicalComplex.truncLE'Map φ' e)
-- Mathlib.RingTheory.WittVector.WittPolynomial
wittPolynomial_vars_subset : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [hp : NeZero p] (n : ℕ), (wittPolynomial p R n).vars ⊆ Finset.range (n + 1)
-- Mathlib.Algebra.GroupWithZero.Basic
eq_zero_of_one_div_eq_zero : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, 1 / a = 0 → a = 0
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.instContinuousMapClass : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂],
  ContinuousMapClass (NormedAddGroupHom V₁ V₂) V₁ V₂
-- Mathlib.Data.Finsupp.Order
Finsupp.single_le_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] {i : ι}
  {x : α} {f : ι →₀ α}, (fun₀ | i => x) ≤ f ↔ x ≤ f i
-- Batteries.Data.List.Lemmas
List.idxOfNth_cons_of_not_beq : ∀ {α : Type u_1} {x : α} {xs : List α} {n : ℕ} {a : α} [inst : BEq α],
  (a == x) = false → List.idxOfNth x (a :: xs) n = List.idxOfNth x xs n + 1
-- Mathlib.RingTheory.RingHom.QuasiFinite
/-- The predicate for a ring hom being quasi-finite at a prime.  -/
RingHom.QuasiFiniteAt : {R : Type u_6} →
  {S : Type u_7} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → (p : Ideal S) → [p.IsPrime] → Prop
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.comp_symm : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (f : L.Equiv M N) (g : L.Equiv N P), (g.comp f).symm = f.symm.comp g.symm
-- Mathlib.Tactic.GRewrite.Elab
/-- `grw [e₁, ..., eₙ]` uses each expression `eᵢ : Rᵢ aᵢ bᵢ` (where `Rᵢ` is any two-argument
relation) as a generalized rewrite rule on the main goal, replacing occurrences of `aᵢ` with `bᵢ`,
then tries to close the main goal by "cheap" (reducible) `rfl`.
Use `grw [← eᵢ]` to rewrite in the other direction, replacing occurrences of `bᵢ` with `aᵢ`.

If an expression `e` is a defined constant, then the equational theorems associated with `e` are
used. This provides a convenient way to unfold `e`. If `e` has parameters, the tactic will try to
fill these in by unification with the matching part of the target. Parameters are only filled in
once per rule, restricting which later rewrites can be found. Parameters that are not filled in
after unification will create side goals.

To be able to use `grw`, the relevant lemmas need to be tagged with `@[gcongr]`.
To rewrite inside a transitive relation, you can also give it an `IsTrans` instance.

Rewriting with a strict inequality `a < b` may change the goal, such as changing `<` to `≤`.
If this is not possible, then `a < b` is treated the same as `a ≤ b`.

`grewrite` is like `grw` but does not try to apply `rfl` afterwards.
To rewrite only in the `n`-th position, use `nth_grw n`.
`apply_rw [e₁, ..., eₙ]` is a shorthand for `grw +implicationHyp [e₁, ..., eₙ]`: it interprets
`· → ·` as a relation instead of adding the hypothesis as a side condition.

* `grw [← e]` applies the rewrite rule `e : R a b` in the reverse direction, replacing occurrences
  of `b` with `a`.
* `grw (config := cfg) [e₁, ..., eₙ]` uses `cfg` as configuration. See `GRewrite.Config` for
  details.
  * To let `grw` unfold more aggressively, as in `erw`, use
    `grw (transparency := default) [e₁, ..., eₙ]`.
  * `grw +implicationHyp [e₁, ..., eₙ]` interprets `· → ·` as a relation (see `apply_rw`).
* `grw [e₁, ..., eₙ] at l` rewrites at the location(s) `l`.

Examples:

```lean
variable {a b c d n : ℤ}

example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
  grw [h₁, h₂]

example (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
  grw [h]

example (h₁ : a ∣ b) (h₂ : b ∣ a ^ 2 * c) : a ∣ b ^ 2 * c := by
  grw [h₁] at *
  exact h₂

-- To replace the RHS with the LHS of the given relation, use the `←` notation (just like in `rw`):
example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
  grw [← h₂, ← h₁]
```
 -/
Mathlib.Tactic.GRewrite.grwSeq : Lean.ParserDescr
-- Mathlib.Analysis.Complex.AbelLimit
Complex.nhdsWithin_stolzCone_le_nhdsWithin_stolzSet : ∀ {s : ℝ}, 0 < s → ∃ M, nhdsWithin 1 (Complex.stolzCone s) ≤ nhdsWithin 1 (Complex.stolzSet M)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.deriv_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G}
  (h : IsBoundedBilinearMap 𝕜 f) (p q : E × F), (h.deriv p) q = f (p.1, q.2) + f (q.1, p.2)
-- Init.Data.UInt.Bitwise
USize.toUInt16_xor : ∀ (a b : USize), (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.unitization_algebraMap : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : NormedSpace 𝕜 A]
  [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A] (r : 𝕜),
  ((algebraMap 𝕜 (WithLp 1 (Unitization 𝕜 A))) r).ofLp = (algebraMap 𝕜 (Unitization 𝕜 A)) r
-- Init.Core
Function.const_apply : ∀ {β : Sort u_1} {α : Sort u_2} {y : β} {x : α}, Function.const α y x = y
-- Batteries.Lean.NameMapAttribute
/-- The declaration which creates the attribute  -/
Lean.NameMapAttributeImpl.ref : {α : Type} → Lean.NameMapAttributeImpl α → Lean.Name
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- `HasPushoutsAlong f` states that pushouts of all morphisms out of `X`
along `f : X ⟶ Y` exist.  -/
CategoryTheory.Limits.HasPushoutsAlong : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → Prop
-- Mathlib.RingTheory.FiniteType
AlgHom.Finite.finiteType : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {f : A →ₐ[R] B}, f.Finite → f.FiniteType
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- Descend along an effective epi.  -/
CategoryTheory.EffectiveEpi.desc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y W : C} →
      (f : Y ⟶ X) →
        [CategoryTheory.EffectiveEpi f] →
          (e : Y ⟶ W) →
            (∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
                CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
                  CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) →
              (X ⟶ W)
-- Std.Do.Internal.Ensures.Def
Std.Do.Internal.Ensures.mk : ∀ {m : Type u → Type v} [inst : Bind m] {α : Type u} {P : α → Prop} {x : m α},
  (∃ y, Std.Do.Internal.ErasesTo y x) → Std.Do.Internal.Ensures P x
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- Auxiliary definition for `StrictSegalCore.spineToSimplex`.  -/
SSet.StrictSegalCore.spineToSimplexAux : {X : SSet} → ((n : ℕ) → X.StrictSegalCore n) → {n : ℕ} → (p : X.Path n) → { s // X.spine n s = p }
-- Init.GrindInstances.ToInt
Lean.Grind.instAddInt16SintOfNatNat : Lean.Grind.ToInt.Add Int16 (Lean.Grind.IntInterval.sint 16)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C),
  (X.ofRestrict ⋯).c = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_functor_map_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D} (η : X ⟶ Y),
  (CategoryTheory.WithTerminal.equivComma.functor.map η).right = η.app CategoryTheory.WithTerminal.star
-- Mathlib.Order.SuccPred.Relation
/-- For `n ≠ m`, `(n, m)` is in the transitive closure of a relation `~` if `i ~ pred i` and
`pred i ~ i` for all `i` between `n` and `m`.  -/
transGen_of_pred_of_ne : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ioc m n, r i (Order.pred i)) → (∀ i ∈ Set.Ioc n m, r (Order.pred i) i) → n ≠ m → Relation.TransGen r n m
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
/-- The connecting homomorphism of the Mayer-Vietoris long exact sequence
in sheaf cohomology.  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] →
        [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] →
            (S : J.MayerVietorisSquare) →
              (F : CategoryTheory.Sheaf J AddCommGrpCat) → (n₀ n₁ : ℕ) → n₀ + 1 = n₁ → (F.H' n₀ S.X₁ ⟶ F.H' n₁ S.X₄)
-- Lean.Elab.Tactic.Omega.MinNatAbs
Lean.Elab.Tactic.Omega.List.nonzeroMinimum_le_iff : ∀ {xs : List ℕ} {y : ℕ},
  Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs ≤ y ↔
    Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs = 0 ∨ ∃ x ∈ xs, x ≤ y ∧ x ≠ 0
-- Init.Data.Ord.Basic
List.isGE_compareLex_nil_left : ∀ {α : Type u_1} {cmp : α → α → Ordering} {xs : List α}, (List.compareLex cmp [] xs).isGE = true ↔ xs = []
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.labelledStar.injEq : ∀ (id id_1 : ℕ),
  (Lean.Meta.RefinedDiscrTree.Key.labelledStar id = Lean.Meta.RefinedDiscrTree.Key.labelledStar id_1) = (id = id_1)
-- Mathlib.Topology.UniformSpace.Completion
_private.Mathlib.Topology.UniformSpace.Completion.0.CauchyFilter.symm_gen : ∀ {α : Type u} [inst : UniformSpace α],
  Filter.map Prod.swap ((uniformity α).lift' CauchyFilter.gen) ≤ (uniformity α).lift' CauchyFilter.gen
-- Batteries.Data.ByteArray
ByteArray.getElem_ofFn : ∀ {n : ℕ} (f : Fin n → UInt8) (i : ℕ) (h : i < (ByteArray.ofFn f).size), (ByteArray.ofFn f)[i] = f ⟨i, ⋯⟩
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializationOptions.logCfg? : Lean.Lsp.InitializationOptions → Option Lean.Lsp.LogConfig
-- Mathlib.Algebra.Algebra.Defs
Algebra.algebraMap_self_apply : ∀ {R : Type u} [inst : CommSemiring R] (x : R), (algebraMap R R) x = x
-- Mathlib.InformationTheory.Hamming
Hamming.ofHamming_inj : ∀ {ι : Type u_2} {β : ι → Type u_3} {x y : Hamming β}, Hamming.ofHamming x = Hamming.ofHamming y ↔ x = y
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.liftStar_lift_map : ∀ {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) → Z ⟶ F.obj x)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (x : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.WithInitial.liftStar F M hM).hom
      ((CategoryTheory.WithInitial.lift F M hM).map
        (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.incl.obj x))) =
    CategoryTheory.CategoryStruct.comp (M x) ((CategoryTheory.WithInitial.inclLift F M hM).hom.app x)
-- Mathlib.RingTheory.WittVector.Compare
TruncatedWittVector.card_zmod : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.parallel_pair_connected : CategoryTheory.IsConnected CategoryTheory.Limits.WalkingParallelPair
-- Mathlib.Order.Fin.Basic
Fin.revOrderIso_toEquiv : ∀ {n : ℕ}, Fin.revOrderIso.toEquiv = OrderDual.ofDual.trans Fin.revPerm
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.exists_pos_forall_lt_edist`. -/
EMetric.exists_pos_forall_lt_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  IsCompact s → IsClosed t → Disjoint s t → ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `HasDerivAt.finsetProd`. -/
HasDerivAt.finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι] {𝔸' : Type u_3}
  [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'} {f' : ι → 𝔸'},
  (∀ i ∈ u, HasDerivAt (f i) (f' i) x) → HasDerivAt (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.braiding_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C),
  (CategoryTheory.Limits.biprod.braiding P Q).inv =
    CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_mul : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Mul β]
  [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.Kernel.IndepFun (f i * f j) (f k * f l) κ μ
-- Lean.Elab.Do.Basic
Lean.Elab.Do.mkDoElemElabAttributeUnsafe : Lean.Name → IO (Lean.KeyedDeclsAttribute Lean.Elab.Do.DoElab)
-- Batteries.Data.UInt
UInt16.ext_iff : ∀ {x y : UInt16}, x = y ↔ x.toNat = y.toNat
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false} {km : α},
      Std.Internal.List.minKey l he = km ↔
        Std.Internal.List.getKey? km l = some km ∧
          ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare km k).isLE = true
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_modifyKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    ∀ (h : Std.Internal.List.containsKey k (Std.Internal.List.modifyKey k f l) = true),
      Std.Internal.List.getKey k (Std.Internal.List.modifyKey k f l) h = k
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.comapDomain'_add : ∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : (i : ι) → AddZeroClass (β i)] (h : κ → ι) {h' : ι → κ}
  (hh' : Function.LeftInverse h' h) (f g : Π₀ (i : ι), β i),
  DFinsupp.comapDomain' h hh' (f + g) = DFinsupp.comapDomain' h hh' f + DFinsupp.comapDomain' h hh' g
-- Mathlib.Order.GaloisConnection.Basic
/-- **Alias** of `gciIciSInf`.

---

`toDual ∘ Ici` and `sInf ∘ ofDual` form a Galois coinsertion.  -/
gci_Ici_sInf : {α : Type u} →
  [inst : CompleteSemilatticeInf α] → GaloisCoinsertion (⇑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ⇑OrderDual.ofDual)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_zero : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ↑0 = 0
-- Batteries.Data.Vector.Basic
Vector.uget.congr_simp : ∀ {α : Type u_1} {n : ℕ} (xs xs_1 : Vector α n),
  xs = xs_1 → ∀ (i i_1 : USize) (e_i : i = i_1) (h : i.toNat < n), xs.uget i h = xs_1.uget i_1 ⋯
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_le_one : ∀ {o : Ordinal.{u_1}}, o.card ≤ 1 ↔ o ≤ 1
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.MeasurePreserving.add_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddRightInvariant] (g : G) {X : Type u_3} [inst_4 : MeasurableSpace X] {μ' : MeasureTheory.Measure X}
  {f : X → G}, MeasureTheory.MeasurePreserving f μ' μ → MeasureTheory.MeasurePreserving (fun x => f x + g) μ' μ
-- Init.Data.ToString.Basic
instToStringUnit : ToString Unit
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.predictablePart_bdd_difference : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {R : ℝ} {f : ℕ → Ω → E} (ℱ : MeasureTheory.Filtration ℕ m0),
  (∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ‖f (i + 1) ω - f i ω‖ ≤ R) →
    ∀ᵐ (ω : Ω) ∂μ,
      ∀ (i : ℕ), ‖MeasureTheory.predictablePart f ℱ μ (i + 1) ω - MeasureTheory.predictablePart f ℱ μ i ω‖ ≤ R
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypicOfType.isotypicComponent : ∀ (R : Type u_2) (M : Type u) (S : Type u_4) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S] [IsSimpleModule R S], IsIsotypicOfType R (↥(isotypicComponent R M S)) S
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_eraseₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α} {t : Std.DTreeMap.Internal.Impl α β}
  (htb : t.Balanced), t.Ordered → (Std.DTreeMap.Internal.Impl.eraseₘ k t htb).Ordered
-- Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
CliffordAlgebra.isUnit_ι_of_isUnit : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) {m : M}, IsUnit (Q m) → IsUnit ((CliffordAlgebra.ι Q) m)
-- Qq.Macro
Qq.Impl.MVarSynth.term.inj : ∀ {quotedType : Lean.Expr} {unquotedMVar : Lean.MVarId} {quotedType_1 : Lean.Expr} {unquotedMVar_1 : Lean.MVarId},
  Qq.Impl.MVarSynth.term quotedType unquotedMVar = Qq.Impl.MVarSynth.term quotedType_1 unquotedMVar_1 →
    quotedType = quotedType_1 ∧ unquotedMVar = unquotedMVar_1
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.congrRight` as a linear equivalence.  -/
LocallyConstant.congrRightₗ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {Z : Type u_6} →
        (R : Type u_7) →
          [inst_1 : Semiring R] →
            [inst_2 : AddCommMonoid Y] →
              [inst_3 : Module R Y] →
                [inst_4 : AddCommMonoid Z] →
                  [inst_5 : Module R Z] → (Y ≃ₗ[R] Z) → LocallyConstant X Y ≃ₗ[R] LocallyConstant X Z
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenLowerSections.inter : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f g : α → Set β},
  HasOpenLowerSections f → HasOpenLowerSections g → HasOpenLowerSections fun x => f x ∩ g x
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.symm_self_conj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.End X),
  α.symm.conj (α.conj f) = f
-- Mathlib.Algebra.Group.Action.Sum
Sum.instVAdd : {M : Type u_1} → {α : Type u_3} → {β : Type u_4} → [VAdd M α] → [VAdd M β] → VAdd M (α ⊕ β)
-- Plausible.Shrinkable
Plausible.Subtype.shrinkable : {α : Type u} →
  {β : α → Prop} → [Plausible.Shrinkable α] → [(x : α) → Decidable (β x)] → Plausible.Shrinkable { x // β x }
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- `mapCompIso` gives rise to the oplax functoriality constraint  -/
CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F : CategoryTheory.OplaxFunctor B C} (self : F.PseudoCore) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (self.mapCompIso f g).hom = F.mapComp f g
-- Mathlib.Data.DFinsupp.Order
DFinsupp.coe_strictMono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)],
  Monotone DFunLike.coe
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_Ioo : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (a b : α i), Function.update f i '' Set.Ioo a b = Set.Ioo (Function.update f i a) (Function.update f i b)
-- Mathlib.Topology.Order.OrderClosed
Filter.Tendsto.eventually_const_le : ∀ {α : Type u} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {l : Filter γ}
  {f : γ → α} {u v : α}, u < v → Filter.Tendsto f l (nhds v) → ∀ᶠ (a : γ) in l, u ≤ f a
-- Init.Data.Array.Attach
Array.pmap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a),
  Array.pmap f xs H = (List.pmap f xs.toList ⋯).toArray
-- Mathlib.Order.CompleteLattice.Basic
iInf_sigma : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {p : β → Type u_8} {f : Sigma p → α},
  ⨅ x, f x = ⨅ i, ⨅ j, f ⟨i, j⟩