mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.HasBasis.uniformity_of_nhds_zero_neg_add_swapped : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Sort u_3} {p : ι → Prop}
  {U : ι → Set α}, (nhds 0).HasBasis p U → (uniformity α).HasBasis p fun i => {x | -x.2 + x.1 ∈ U i}
-- Mathlib.Order.RelClasses
WellFoundedLT.toWellFoundedRelation.eq_1 : ∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedLT α],
  WellFoundedLT.toWellFoundedRelation = IsWellFounded.toWellFoundedRelation fun x1 x2 => x1 < x2
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  CategoryTheory.Bicategory.whiskerRight (F.mapId a).inv (F.map f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom
      (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv)
        (F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom)
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.matchEqnsExt : Lean.EnvExtension Lean.Meta.Match.MatchEqnsExtState
-- Mathlib.Algebra.Algebra.Prod
AlgHom.coe_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A →ₐ[R] B) (g : A →ₐ[R] C), ⇑(f.prod g) = Function.prod ⇑f ⇑g
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- When `p = ∞`, this lemma does not hold without the additional assumption `Nonempty ι` because
the left-hand side simplifies to `0`, while the right-hand side simplifies to `‖b‖₊`. See
`PiLp.norm_toLp_const'` for a version which exchanges the hypothesis `p ≠ ∞` for
`Nonempty ι`.  -/
PiLp.norm_toLp_const : ∀ {p : ENNReal} {ι : Type u_2} [hp : Fact (1 ≤ p)] [inst : Fintype ι] {β : Type u_5}
  [inst_1 : SeminormedAddCommGroup β],
  p ≠ ⊤ → ∀ (b : β), ‖WithLp.toLp p (Function.const ι b)‖ = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof : Type
-- Mathlib.RingTheory.RingHomProperties
/-- A morphism property `P` is `IsStableUnderBaseChange` if `P(S →+* A)` implies
`P(B →+* A ⊗[S] B)`.  -/
RingHom.IsStableUnderBaseChange : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.Order.Filter.Prod
Filter.coprod_inf_prod_le : ∀ {α : Type u_1} {β : Type u_2} (f₁ f₂ : Filter α) (g₁ g₂ : Filter β), f₁.coprod g₁ ⊓ f₂ ×ˢ g₂ ≤ f₁ ×ˢ g₂ ⊔ f₂ ×ˢ g₁
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpTriggerKind.invoked.sizeOf_spec : sizeOf Lean.Lsp.SignatureHelpTriggerKind.invoked = 1
-- Batteries.Control.Lemmas
ReaderT.run_orElse : ∀ {m : Type u_1 → Type u_2} {ρ α : Type u_1} [inst : Monad m] [inst_1 : Alternative m] (x y : ReaderT ρ m α) (ctx : ρ),
  (x <|> y).run ctx = (x.run ctx <|> y.run ctx)
-- Mathlib.NumberTheory.Divisors
Nat.divisors_prime_pow : ∀ {p : ℕ} (pp : Nat.Prime p) (k : ℕ),
  (p ^ k).divisors = Finset.map { toFun := fun x => p ^ x, inj' := ⋯ } (Finset.range (k + 1))
-- Mathlib.Order.SuccPred.Basic
Order.Icc_subset_Ioc_pred_left : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Icc b a ⊆ Set.Ioc (Order.pred b) a
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- A choice of pre-image of `Q.relation r` under the canonical
map `MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' S` given by the evaluation of `P`.  -/
Algebra.Presentation.compRelationAux : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              {ι' : Type u_1} →
                {σ' : Type u_2} →
                  {T : Type u_3} →
                    [inst_3 : CommRing T] →
                      [inst_4 : Algebra S T] →
                        Algebra.Presentation S T ι' σ' → Algebra.Presentation R S ι σ → σ' → MvPolynomial (ι' ⊕ ι) R
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.col_strict : ∀ {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → T i1 j < T i2 j
-- Mathlib.MeasureTheory.Category.MeasCat
/-- The category of measurable spaces and measurable functions.  -/
MeasCat : Type (u + 1)
-- Lean.Meta.Basic
Lean.Meta.instMonadMCtxMetaM : Lean.MonadMCtx Lean.MetaM
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_eq_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {k : α}, m.contains k = true → m.getKey! k = k
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ReturnCont.mk.injEq : ∀ (resultType : Lean.Expr) (k : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr) (resultType_1 : Lean.Expr)
  (k_1 : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr),
  ({ resultType := resultType, k := k } = { resultType := resultType_1, k := k_1 }) =
    (resultType = resultType_1 ∧ k = k_1)
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomLeft : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {d d' : D} (f : d ⟶ d') (c : Cᴹᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c.unmop f
-- Init.Data.String.Substring
Substring.Raw.hasBeq : BEq Substring.Raw
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.sum_mul_boole : ∀ {ι : Type u_1} {R : Type u_4} [inst : NonAssocSemiring R] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → R) (i : ι),
  (∑ j ∈ s, f j * if i = j then 1 else 0) = if i ∈ s then f i else 0
-- Mathlib.GroupTheory.Nilpotent
/-- The ⊤-specialization of `lowerCentralSeries_prod`.  -/
Subgroup.top_lowerCentralSeries_prod : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Group G₁] [inst_1 : Group G₂] (n : ℕ),
  ⊤.lowerCentralSeries n = (⊤.lowerCentralSeries n).prod (⊤.lowerCentralSeries n)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α},
  k ∉ m₂ → Std.DHashMap.Const.get! (m₁.union m₂) k = Std.DHashMap.Const.get! m₁ k
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull_nonempty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s : Set E}, ((absConvexHull 𝕜) s).Nonempty ↔ s.Nonempty
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_eq_iSup_nat : ∀ {f : ℕ → ENNReal}, ∑' (i : ℕ), f i = ⨆ i, ∑ a ∈ Finset.range i, f a
-- Mathlib.Algebra.Group.Action.Option
Option.instSMulCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
  SMulCommClass M N (Option α)
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.PreOneHypercover.map_Y : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} (E : CategoryTheory.PreOneHypercover X) (F : CategoryTheory.Functor C D)
  (x x_1 : (CategoryTheory.PreZeroHypercover.map F E.toPreZeroHypercover).I₀) (j : E.I₁ x x_1),
  (E.map F).Y j = F.obj (E.Y j)
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_expand_map_frobenius : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p : ℕ} [inst_2 : ExpChar R p] {f : Polynomial R}
  [PerfectRing R p], Multiset.map (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots = p • f.roots
-- Mathlib.RingTheory.Ideal.Defs
Ideal.instIsTwoSided : ∀ {α : Type u} [inst : CommSemiring α] (I : Ideal α), I.IsTwoSided
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
_private.Mathlib.AlgebraicTopology.DoldKan.NCompGamma.0.Fin.succ.match_1.splitter : {n : ℕ} → (motive : Fin n → Sort u_1) → (x : Fin n) → ((i : ℕ) → (h : i < n) → motive ⟨i, h⟩) → motive x
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidRevSearchFrom.startPos_of_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {p : s.Pos}
  {l : List (String.Slice.Pattern.SearchStep s)},
  p = s.startPos → l = [] → String.Slice.Pattern.Model.IsValidRevSearchFrom pat p l
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.lift_map : ∀ {V : Type u} [inst : Quiver V] {C : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} C] (F : V ⥤q C)
  {X Y : CategoryTheory.Paths V} (f : X ⟶ Y),
  (CategoryTheory.Quiv.lift F).map f = CategoryTheory.composePath (F.mapPath f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.maxKey!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxKey! = t₂.maxKey!
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddGroup.toNorm : {E : Type u_8} → [self : SeminormedAddGroup E] → Norm E
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- `one` approximates the unit function.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.one_approximates : ∀ {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis → Tactic.ComputeAsymptotics.MultiseriesExpansion.one.Approximates
-- Mathlib.Analysis.Calculus.DerivativeTest
deriv_neg_left_of_sign_deriv : ∀ {f : ℝ → ℝ} {x₀ : ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x - x₀)) →
    ∀ᶠ (b : ℝ) in nhdsWithin x₀ (Set.Iio x₀), deriv f b < 0
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue.congr_simp : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] (u u_1 : ι → Ω → β),
  u = u_1 →
    ∀ (τ τ_1 : Ω → WithTop ι),
      τ = τ_1 → ∀ (a a_1 : Ω), a = a_1 → MeasureTheory.stoppedValue u τ a = MeasureTheory.stoppedValue u_1 τ_1 a_1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.takeUntil_takeUntil : ∀ {V : Type u} {G : SimpleGraph V} {v u : V} [inst : DecidableEq V] {w x : V} (p : G.Walk u v) (hw : w ∈ p.support)
  (hx : x ∈ (p.takeUntil w hw).support), (p.takeUntil w hw).takeUntil x hx = p.takeUntil x ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- the left morphism of the pushout square `isPushout i d`: this is
the coproduct of copies of the boundary inclusion `∂Δ[d] ⟶ Δ[d]` indexed
by the nondegenerate `d`-simplices of `Y` not in the range of `i`.  -/
SSet.relativeCellComplexOfMono.l : {X Y : SSet} →
  (i : X ⟶ Y) →
    (d : ℕ) → SSet.relativeCellComplexOfMono.sigmaBoundary i d ⟶ SSet.relativeCellComplexOfMono.sigmaStdSimplex i d
-- Mathlib.Analysis.InnerProductSpace.Defs
_private.Mathlib.Analysis.InnerProductSpace.Defs.0.InnerProductSpace.Core.termExt_iff_1 : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.Commute.zpow_right : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A B : Matrix n' n' R}, Commute A B → ∀ (m : ℤ), Commute A (B ^ m)
-- Batteries.Lean.LawfulMonadLift
EIO.adapt_pure : ∀ {ε₁ ε₂ α : Type} (f : ε₁ → ε₂) (a : α), EIO.adapt f (pure a) = pure a
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ofCoreEq_toCore : ∀ {α : Type ua} (u : UniformSpace α) (t : TopologicalSpace α) (h : t = u.toCore.toTopologicalSpace),
  UniformSpace.ofCoreEq u.toCore t h = u
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.leibnizPushout_obj_obj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) [inst_3 : CategoryTheory.Limits.HasPushouts C₃]
  (f₁ : CategoryTheory.Arrow C₁) (f₂ : CategoryTheory.Arrow C₂),
  (F.leibnizPushout.obj f₁).obj f₂ =
    CategoryTheory.Arrow.mk (CategoryTheory.Functor.PushoutObjObj.ofHasPushout F f₁.hom f₂.hom).ι
-- Batteries.Data.List.Basic
List.takeListTR.go.eq_def : ∀ {α : Type u_1} (a : List ℕ) (a_1 : List α) (a_2 : Array (List α)),
  List.takeListTR.go a a_1 a_2 =
    match a, a_1, a_2 with
    | [], xs, acc => (acc.toList, xs)
    | n :: ns, xs, acc =>
      match List.splitAt n xs with
      | (xs₁, xs₂) => List.takeListTR.go ns xs₂ (acc.push xs₁)
-- Mathlib.CategoryTheory.MarkovCategory.Basic
/-- Process then discard equals discard directly.  -/
CategoryTheory.MarkovCategory.discard_natural_assoc : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MarkovCategory C] {X Y : C} (f : X ⟶ Y) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit h
-- Init.Data.Vector.Find
Vector.find?_eq_none : ∀ {α : Type} {p : α → Bool} {n : ℕ} {l : Vector α n}, Vector.find? p l = none ↔ ∀ x ∈ l, ¬p x = true
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_union_add_inter : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [T2Space M] [inst_3 : ContinuousAdd M] {v : MeasureTheory.VectorMeasure α M} {s t : Set α},
  MeasurableSet s → MeasurableSet t → v.restrict (s ∪ t) + v.restrict (s ∩ t) = v.restrict s + v.restrict t
-- Mathlib.Logic.Basic
ite_and : ∀ {α : Sort u_1} (P Q : Prop) [inst : Decidable P] (a b : α) [inst_1 : Decidable Q],
  (if P ∧ Q then a else b) = if P then if Q then a else b else b
-- Mathlib.Algebra.Module.Injective
Module.Injective.extension_property : ∀ (R : Type uR) [inst : Ring R] [Small.{uM, uR} R] (M : Type uM) [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inj : Module.Injective R M] (P : Type uP) [inst_4 : AddCommGroup P] [inst_5 : Module R P] (P' : Type uP')
  [inst_6 : AddCommGroup P'] [inst_7 : Module R P'] (f : P →ₗ[R] P'),
  Function.Injective ⇑f → ∀ (g : P →ₗ[R] M), ∃ h, h ∘ₗ f = g
-- Mathlib.Data.Nat.ModEq
/-- **Alias** of the forward direction of `AddCommGroup.natCast_modEq_natCast`. -/
Nat.ModEq.of_natCast : ∀ {M : Type u_1} [inst : AddCommMonoidWithOne M] [CharZero M] {a b n : ℕ}, ↑a ≡ ↑b [PMOD ↑n] → a ≡ b [MOD n]
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.sub_left : ∀ {R : Type uR} [inst : Ring R] {r : R → R → Prop} ⦃a b c : R⦄, RingQuot.Rel r a b → RingQuot.Rel r (a - c) (b - c)
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Types.instPreservesColimitsOfSizeForgetTypeFun : CategoryTheory.Limits.PreservesColimitsOfSize.{u_1, u_2, u, u, u + 1, u + 1} (CategoryTheory.forget (Type u))
-- Mathlib.Data.Multiset.Count
Multiset.coe_countP : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : List α),
  Multiset.countP p ↑l = List.countP (fun b => decide (p b)) l
-- Mathlib.Data.SetLike.Basic
SetLike.ext_iff : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, p = q ↔ ∀ (x : B), x ∈ p ↔ x ∈ q
-- Mathlib.Combinatorics.Digraph.Basic
/-- The difference of two digraphs `x \ y` has the edges of `x` with the edges of `y` removed.  -/
Digraph.sdiff : {V : Type u_2} → SDiff (Digraph V)
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.isMinOn_of_leftDeriv_eq_zero : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ}, ConvexOn ℝ S f → x ∈ interior S → derivWithin f (Set.Iio x) x = 0 → IsMinOn f S x
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.congr_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.HashSet α}, m₁.Equiv m₂ → (m₃.Equiv m₁ ↔ m₃.Equiv m₂)
-- Lean.Linter.UnusedVariables
/-- Enables linting variables defined in tactic blocks, may be expensive for complex proofs  -/
Lean.Linter.linter.unusedVariables.analyzeTactics : Lean.Option Bool
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_ofIntClamp_of_lt : ∀ {n : ℤ}, n < 2 ^ 31 → (ISize.ofIntClamp n).toNatClampNeg = n.toNat
-- Mathlib.RingTheory.Polynomial.Wronskian
/-- Degree of `W(a,b)` is strictly less than the sum of degrees of `a` and `b` (both nonzero).  -/
Polynomial.degree_wronskian_lt_add : ∀ {R : Type u_1} [inst : CommRing R] {a b : Polynomial R}, a ≠ 0 → b ≠ 0 → (a.wronskian b).degree < a.degree + b.degree
-- Mathlib.RingTheory.Congruence.Defs
RingCon.mk.injEq : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (toCon : Con R)
  (add' : ∀ {w x y z : R}, toCon.toSetoid w x → toCon.toSetoid y z → toCon.toSetoid (w + y) (x + z)) (toCon_1 : Con R)
  (add'_1 : ∀ {w x y z : R}, toCon_1.toSetoid w x → toCon_1.toSetoid y z → toCon_1.toSetoid (w + y) (x + z)),
  ({ toCon := toCon, add' := add' } = { toCon := toCon_1, add' := add'_1 }) = (toCon = toCon_1)
-- Mathlib.Algebra.Order.UpperLower
UpperSet.addCommSemigroup : {α : Type u_1} →
  [inst : AddCommGroup α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → AddCommSemigroup (UpperSet α)
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm_inv_mul_self_nhdsNE : ∀ {E : Type u_4} [inst : NormedGroup E] (a : E),
  Filter.Tendsto (fun x => ‖x⁻¹ * a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β k},
        (m₁.inter m₂).getD k fallback = if m₂.contains k = true then m₁.getD k fallback else fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coneOfIsSplitMono_π_app : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y) [inst_1 : CategoryTheory.IsSplitMono f]
  (X_1 : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.coneOfIsSplitMono f).π.app X_1 =
    CategoryTheory.Limits.WalkingParallelPair.casesOn (motive := fun t =>
      X_1 = t →
        (((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj X).obj X_1 ⟶
          (CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.id Y)
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f)).obj
            X_1))
      X_1 (fun h => ⋯ ▸ f) (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y)) ⋯
-- Mathlib.Order.Interval.Basic
/-- `toDualProd` as an order embedding.  -/
NonemptyInterval.toDualProdHom : {α : Type u_1} → [inst : LE α] → NonemptyInterval α ↪o αᵒᵈ × α
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.leftAdjointMate_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.HasLeftDual X] [inst_3 : CategoryTheory.HasLeftDual Y] {f : X ⟶ Y} {g : ᘁX ⟶ Z},
  CategoryTheory.CategoryStruct.comp (ᘁf) g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor ᘁY).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (η_ (ᘁX) X) ᘁY)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom g f) ᘁY)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z Y ᘁY).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (ε_ (ᘁY) Y))
              (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom))))
-- Mathlib.Algebra.Homology.GrothendieckAbelian
HomologicalComplex.instHasFilteredColimitsOfSize : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w', v, u} C],
  CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w', max t v, max (max t u) v} (HomologicalComplex C c)
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
/-- **Alias** of `CategoryTheory.constantCommuteCompose_hom_app_hom`. -/
CategoryTheory.constantCommuteCompose_hom_app_val : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {B : Type u_3} [inst_3 : CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B)
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [inst_5 : J.PreservesSheafification U] [inst_6 : J.HasSheafCompose U]
  (X : D),
  ((CategoryTheory.constantCommuteCompose J U).hom.app X).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.sheafifyComposeIso J U ((CategoryTheory.Functor.const Cᵒᵖ).obj X)).inv
      (CategoryTheory.sheafifyMap J (CategoryTheory.Functor.constComp Cᵒᵖ X U).hom)
-- Lean.Data.Lsp.Extra
Lean.Lsp.DependencyBuildMode.never.sizeOf_spec : sizeOf Lean.Lsp.DependencyBuildMode.never = 1
-- Init.Data.UInt.Lemmas
UInt64.sub_eq_add_neg : ∀ (a b : UInt64), a - b = a + -b
-- Lean.DocString.DeferredCheck
Lean.Doc.DeferredCheck.mk : Lean.Doc.DeferredCheckSite →
  ℕ → String → Array Lean.Name → Lean.Name → List Lean.OpenDecl → Lean.Options → Dynamic → Lean.Doc.DeferredCheck
-- Plausible.Random
/-- Generate a random `Bool`.
 -/
Plausible.Random.randBool : {m : Type → Type u_1} → [Monad m] → {g : Type} → [RandomGen g] → Plausible.RandGT g m Bool
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.addEquiv_toEquiv : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (e : M ≃+ N),
  ↑(Finsupp.mapRange.addEquiv e) = Finsupp.mapRange.equiv ↑e ⋯
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_closure_congr : ∀ {α : Type u} {M : Matroid α} {X Y : Set α} [M.InvariantCardinalRank], M.closure X = M.closure Y → M.cRk X = M.cRk Y
-- Lean.Data.Json.Elab
/-- Json string syntax.  -/
Lean.Json.json_ : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.mem_submodule_iff : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (s : Projectivization.Subspace K V) {v : V} (hv : v ≠ 0),
  v ∈ Projectivization.Subspace.submodule s ↔ Projectivization.mk K v hv ∈ s
-- Mathlib.Analysis.Convex.Between
mem_const_vsub_affineSegment : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (p : P),
  p -ᵥ z ∈ affineSegment R (p -ᵥ x) (p -ᵥ y) ↔ z ∈ affineSegment R x y
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.linMulLin.congr_simp : ∀ {R : Type u_3} {M : Type u_4} {A : Type u_7} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] (f f_1 : M →ₗ[R] A),
  f = f_1 → ∀ (g g_1 : M →ₗ[R] A), g = g_1 → QuadraticMap.linMulLin f g = QuadraticMap.linMulLin f_1 g_1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The singleton operation as an `AddHom`.  -/
Finset.singletonAddHom : {α : Type u_2} → [inst : DecidableEq α] → [inst_1 : Add α] → α →ₙ+ Finset α
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLE.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (lowerBound : α),
  Std.DTreeMap.Internal.Impl.pruneLE✝ Std.DTreeMap.Internal.Impl.leaf lowerBound = Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.darts_dropUntil_suffix_darts : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.dropUntil u h).darts <:+ p.darts