mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- In the topology of pointwise convergence, `a` converges to `a₀` iff for every `x : E` the map
`a · x` converges to `a₀ x`.  -/
PointwiseConvergenceCLM.tendsto_iff_forall_tendsto : ∀ {ι : Type u_2} {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂}
  {E : Type u_7} {F : Type u_8} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜₁ E] [inst_8 : Module 𝕜₂ F]
  {p : Filter ι} {a : ι → E →SLₚₜ[σ] F} {a₀ : E →SLₚₜ[σ] F},
  Filter.Tendsto a p (nhds a₀) ↔ ∀ (x : E), Filter.Tendsto (fun x_1 => (a x_1) x) p (nhds (a₀ x))
-- Mathlib.CategoryTheory.Sites.Point.Category
/-- The natural transformation on fibers of sheaves that is induced
by a morphism of points of a site.  -/
CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
            {Φ₁ Φ₂ : J.Point} → (Φ₁ ⟶ Φ₂) → (Φ₂.sheafFiber ⟶ Φ₁.sheafFiber)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideCoequalizer.condition_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y))
  [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] (j₁ j₂ : J) {Z : C}
  (h : CategoryTheory.Limits.wideCoequalizer f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f j₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) h) =
    CategoryTheory.CategoryStruct.comp (f j₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) h)
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.copy.congr_simp : ∀ {X : Type u_1} [inst : MetricSpace X] (D D_1 : Delone.DeloneSet X) (e_D : D = D_1) (carrier carrier_1 : Set X)
  (e_carrier : carrier = carrier_1) (packingRadius packingRadius_1 : NNReal)
  (e_packingRadius : packingRadius = packingRadius_1) (coveringRadius coveringRadius_1 : NNReal)
  (e_coveringRadius : coveringRadius = coveringRadius_1) (h_carrier : carrier = D.carrier)
  (h_packing : packingRadius = D.packingRadius) (h_covering : coveringRadius = D.coveringRadius),
  D.copy carrier packingRadius coveringRadius h_carrier h_packing h_covering =
    D_1.copy carrier_1 packingRadius_1 coveringRadius_1 ⋯ ⋯ ⋯
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.Ico_ae_eq_Ioc : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a b : α}, Set.Ico a b =ᵐ[μ] Set.Ioc a b
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.save : Lean.Meta.Sym.ExprPtr × ℕ → Lean.Expr → Lean.Meta.Sym.M✝ Lean.Expr
-- Init.Meta.Defs
/-- If `allowSynthFailures` is `true`, then `apply` will return instance implicit arguments
for which typeclass search failed as new goals.
 -/
Lean.Meta.ApplyConfig.allowSynthFailures : Lean.Meta.ApplyConfig → Bool
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α} {v : β}, (m.getThenInsertIfNew? k v).1 = m[k]?
-- Mathlib.Algebra.Group.Defs
/-- An additive commutative monoid is an additive monoid with commutative `(+)`.  -/
AddCommMonoid : Type u → Type u
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (c :
    CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory)
      (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C)))
  (X : CategoryTheory.WithInitial SimplexCategory),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.inverse.obj c).obj X =
    match X with
    | CategoryTheory.WithInitial.of x => c.right.obj x
    | CategoryTheory.WithInitial.star => c.left
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_X : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], Polynomial.X.trailingDegree = 1
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
/-- A matrix `M` is nondegenerate if it is both left-separating and right-separating.

See also `Matrix.Nonsingular`.  -/
Matrix.Nondegenerate : {m : Type u_1} →
  {n : Type u_2} → {R : Type u_3} → [NonUnitalNonAssocSemiring R] → [Finite m] → [Finite n] → Matrix m n R → Prop
-- Init.Data.UInt.Bitwise
UInt16.toUInt32_or : ∀ (a b : UInt16), (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.le_innerContent : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) (K : TopologicalSpace.Compacts G)
  (U : TopologicalSpace.Opens G), ↑K ⊆ ↑U → μ K ≤ μ.innerContent U
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_mulRight : ∀ {R : Type u_1} [inst : CommRing R] (a : R), LinearMap.det (LinearMap.mulRight R a) = a
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.Hom.mk_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnrichedOrdinary C}
  {f g h : X ⟶ Y} (α : CategoryTheory.CatEnrichedOrdinary.homEquiv f ⟶ CategoryTheory.CatEnrichedOrdinary.homEquiv g)
  (β : CategoryTheory.CatEnrichedOrdinary.homEquiv g ⟶ CategoryTheory.CatEnrichedOrdinary.homEquiv h),
  CategoryTheory.CatEnrichedOrdinary.Hom.mk (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CatEnrichedOrdinary.Hom.mk α)
      (CategoryTheory.CatEnrichedOrdinary.Hom.mk β)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv._auto_3) {Z : C}
  (h : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.pOpcycles f₂ f₃ n₁)
      (CategoryTheory.CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv h) =
    CategoryTheory.CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles h
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.lhs_cast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α}
  (s : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig1) (hcast : aig1.decls.size ≤ aig2.decls.size),
  (s.cast hcast).lhs = s.lhs.cast hcast
-- Lean.Meta.CongrTheorems
/-- Similar to `mkCongrSimp?`, but uses reserved names to ensure we don't keep creating the
same congruence theorem over and over again.
 -/
Lean.Meta.mkCongrSimpForConst? : Lean.Name → List Lean.Level → Lean.MetaM (Option Lean.Meta.CongrTheorem)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntryD_eq_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α} {fallback : (a : α) × β a},
  Std.Internal.List.getEntryD a fallback l = (Std.Internal.List.getEntry? a l).getD fallback
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.separatingRight_toLinearMap₂'_iff_det_ne_zero : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] [IsDomain R]
  {M : Matrix n n R}, ((Matrix.toLinearMap₂' R) M).SeparatingRight ↔ M.det ≠ 0
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_lt_add_left : ∀ {a b c : ENNReal}, a ≠ ⊤ → b < c → a + b < a + c
-- Mathlib.Algebra.GroupWithZero.ProdHom
/-- Given groups with zero `G₀`, `H₀`, the natural inclusion ordered homomorphism from
`H₀` to `WithZero (G₀ˣ × H₀ˣ)`, which is the group with zero that can be identified
as their product.  -/
MonoidWithZeroHom.inr : (G₀ : Type u_1) →
  (H₀ : Type u_2) →
    [inst : GroupWithZero G₀] →
      [inst_1 : GroupWithZero H₀] → [DecidablePred fun x => x = 0] → H₀ →*₀ WithZero (G₀ˣ × H₀ˣ)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.mem_map_of_mem : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) {S : AddSubsemigroup M} {x : M},
  x ∈ S → f x ∈ AddSubsemigroup.map f S
-- Mathlib.Algebra.BigOperators.Fin
Fin.add_sum_removeNth : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (i : Fin (n + 1)) (f : Fin (n + 1) → M),
  f i + ∑ j, i.removeNth f j = ∑ j, f j
-- Init.Data.Iterators.Basic
/-- This structure provides a more convenient way to define `Finite α m` instances using
`Finite.of_finitenessRelation : FinitenessRelation α m → Finite α m`.
 -/
Std.Iterators.FinitenessRelation : (α : Type w) → (m : Type w → Type w') → {β : Type w} → [Std.Iterator α m β] → Type w
-- Mathlib.Data.Set.Finite.Basic
Set.infinite_range_of_injective : ∀ {α : Type u} {β : Type v} [Infinite α] {f : α → β}, Function.Injective f → (Set.range f).Infinite
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.singleton_mem_precoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {X Y : C}
  (f : X ⟶ Y), CategoryTheory.Presieve.singleton f ∈ P.precoverage.coverings Y ↔ P f
-- Mathlib.Probability.Independence.Kernel.Indep
/-- **Alias** of the forward direction of `ProbabilityTheory.Kernel.indepSet_congr`. -/
ProbabilityTheory.Kernel.indepSet.congr : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ η : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {s t : Set Ω},
  ⇑κ =ᵐ[μ] ⇑η → ProbabilityTheory.Kernel.IndepSet s t κ μ → ProbabilityTheory.Kernel.IndepSet s t η μ
-- Mathlib.Testing.Plausible.Functions
/-- Create an injective function from one list and a permutation of that list.  -/
Plausible.InjectiveFunction.mk : {α : Type u} → (xs ys : List α) → xs.Perm ys → ys.Nodup → Plausible.InjectiveFunction α
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- The *identity principle* for analytic functions, global version: if two functions on a normed
field `𝕜` are analytic everywhere and coincide at points which accumulate to a point `z₀`, then
they coincide globally.
For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`,
see `AnalyticOnNhd.eq_of_eventuallyEq`.  -/
AnalyticOnNhd.eq_of_frequently_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} [ConnectedSpace 𝕜],
  AnalyticOnNhd 𝕜 f Set.univ → AnalyticOnNhd 𝕜 g Set.univ → (∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = g z) → f = g
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constToArray_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.toArray t₁ = Std.DTreeMap.Raw.Const.toArray t₂
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ClientCapabilities.window? : Lean.Lsp.ClientCapabilities → Option Lean.Lsp.WindowClientCapabilities
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.CotangentSpace.map_comp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [inst_10 : CommRing R''] [inst_11 : CommRing S'']
  [inst_12 : Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [inst_13 : Algebra R R''] [inst_14 : Algebra S S'']
  [inst_15 : Algebra R S''] [inst_16 : IsScalarTower R R'' S''] [inst_17 : Algebra R' R''] [inst_18 : Algebra S' S'']
  [inst_19 : Algebra R' S''] [inst_20 : IsScalarTower R' R'' S''] [inst_21 : IsScalarTower R R' R'']
  [inst_22 : IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P''),
  Algebra.Extension.CotangentSpace.map (g.comp f) =
    ↑S (Algebra.Extension.CotangentSpace.map g) ∘ₗ Algebra.Extension.CotangentSpace.map f
-- Mathlib.Topology.Order.DenselyOrdered
nhdsGT_neBot_of_exists_gt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α},
  (∃ b, a < b) → (nhdsWithin a (Set.Ioi a)).NeBot
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_def' : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (e : Int.Internal.Linear.Expr)
  (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_def'_cert x e p = true →
    Int.Internal.Linear.Var.denote ctx x = Int.Internal.Linear.Expr.denote ctx e →
      Int.Internal.Linear.Poly.denote' ctx p = 0
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
IsUnramifiedAtInfinitePlaces.trans : ∀ (k : Type u_1) [inst : Field k] (K : Type u_2) [inst_1 : Field K] (F : Type u_3) [inst_2 : Field F]
  [inst_3 : Algebra k K] [inst_4 : Algebra k F] [inst_5 : Algebra K F] [IsScalarTower k K F]
  [h₁ : IsUnramifiedAtInfinitePlaces k K] [h₂ : IsUnramifiedAtInfinitePlaces K F], IsUnramifiedAtInfinitePlaces k F
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.iSup_edist_pairSet : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] {E : Type u_2}
  [inst_2 : PseudoEMetricSpace E],
  1 < a → ∀ (f : T → E), ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE_congr : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V V' : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (e₁ : U = U') (e₂ : V = V')
  (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme),
  P (AlgebraicGeometry.Scheme.Hom.resLE f U V e) ↔ P (AlgebraicGeometry.Scheme.Hom.resLE f U' V' ⋯)
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_add_of_natDegree_lt_right : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R},
  p.natDegree < q.natDegree → (p + q).eraseLead = p + q.eraseLead
-- Lean.Expr
Lean.Literal.typeEx : Lean.Literal → Lean.Expr
-- Aesop.Script.SScript
Aesop.Script.SScript.focusAndSolve.inj : ∀ {goalPos : ℕ} {here tail : Aesop.Script.SScript} {goalPos_1 : ℕ} {here_1 tail_1 : Aesop.Script.SScript},
  Aesop.Script.SScript.focusAndSolve goalPos here tail = Aesop.Script.SScript.focusAndSolve goalPos_1 here_1 tail_1 →
    goalPos = goalPos_1 ∧ here = here_1 ∧ tail = tail_1
-- Mathlib.Algebra.Polynomial.Degree.Units
Polynomial.natDegree_pos_of_not_isUnit_of_dvd_monic : ∀ {R : Type u} [inst : CommSemiring R] {a p : Polynomial R}, p.Monic → ¬IsUnit a → a ∣ p → 0 < a.natDegree
-- Init.Data.BitVec.Bitblast
/-- We instantiate `extractAndExtendAux` to extend each bit to `len`, extending
each bit in `x` to have width `w` and returning a `BitVec (w * w)`.  -/
BitVec.extractAndExtend : {w : ℕ} → (len : ℕ) → BitVec w → BitVec (w * len)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instPow.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β], OrderDual.instPow = inst
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMapWithPostcondition.match_3.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2)
  (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.CategoryTheory.Subfunctor.Basic
/-- The inclusion of a subfunctor to a larger subfunctor  -/
CategoryTheory.Subfunctor.homOfLe : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type w)} →
      {G G' : CategoryTheory.Subfunctor F} → G ≤ G' → (G.toFunctor ⟶ G'.toFunctor)
-- Init.Core
instInhabitedTrue : Inhabited True
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.Context.mk : Lean.Name → Bool → Lean.BinderInfo → Lean.MVarIdSet → Lean.MetavarContext.MkBinding.Context
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.regularizedGaussHGFun.eq_1 : ∀ (a b c z : ℂ), a.regularizedGaussHGFun b c z = (a.regularizedGaussHGFunSeries b c).sum z
-- Init.Data.BitVec.Lemmas
BitVec.instLawfulOrderLT : ∀ {n : ℕ}, Std.LawfulOrderLT (BitVec n)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.isPullback_SpecMap_of_isPushout : ∀ {A B C P : CommRingCat} (f : A ⟶ B) (g : A ⟶ C) (inl : B ⟶ P) (inr : C ⟶ P),
  CategoryTheory.IsPushout f g inl inr →
    CategoryTheory.IsPullback (AlgebraicGeometry.Spec.map inl) (AlgebraicGeometry.Spec.map inr)
      (AlgebraicGeometry.Spec.map f) (AlgebraicGeometry.Spec.map g)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_maxKey?_eq_not_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  (Std.Internal.List.maxKey? l).isSome = !l.isEmpty
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.ratio_inv : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (e : X ≃ᵈ X), Dilation.ratio e⁻¹ = (Dilation.ratio e)⁻¹
-- Mathlib.Tactic.GRewrite.Elab
/-- Analogous to `finishElabRewrite`.  -/
_private.Mathlib.Tactic.GRewrite.Elab.0.Mathlib.Tactic.GRewrite.finishElabGRewrite : Mathlib.Tactic.GRewrite.GRewriteResult → Lean.MetaM Mathlib.Tactic.GRewrite.GRewriteResult
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- If a function is `C^n` on a domain with unique derivatives, with `1 ≤ n`, then its bundled
derivative is continuous there.  -/
ContMDiffOn.continuousOn_tangentMapWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  [Is : IsManifold I 1 M] [I's : IsManifold I' 1 M'],
  ContMDiffOn I I' n f s →
    1 ≤ n → UniqueMDiff[s] → ContinuousOn (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder : {α : Type u_2} →
  {β : Type u_3} →
    [inst : OmegaCompletePartialOrder α] → [inst_1 : OmegaCompletePartialOrder β] → OmegaCompletePartialOrder (α →o β)
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assoc : ∀ (X : TopCat) {Z : SSet} (h : TopCat.toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X TopCat.I) ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₀
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (TopCat.toSSet.obj X) SSet.stdSimplex.toSSetObjI)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I) h)) =
    CategoryTheory.CategoryStruct.comp (TopCat.toSSet.map TopCat.ι₀) h
-- Mathlib.Data.Set.Image
Function.Injective.preimage_surjective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → Function.Surjective (Set.preimage f)
-- Init.Data.Fin.Lemmas
Fin.lt_asymm : ∀ {n : ℕ} {a b : Fin n}, a < b → ¬b < a
-- Init.Data.Vector.Lemmas
Vector.map_eq_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Vector α 1} {b : β},
  Vector.map f xs = #v[b] ↔ ∃ a, xs = #v[a] ∧ f a = b
-- Mathlib.Topology.EMetricSpace.Diam
/-- The extended diameter is monotonous with respect to inclusion  -/
Metric.ediam_mono : ∀ {X : Type u_2} {s t : Set X} [inst : PseudoEMetricSpace X], s ⊆ t → Metric.ediam s ≤ Metric.ediam t
-- Init.Data.Int.Basic
/-- Decides whether `a ≤ b`.

```
#eval ¬ ( (7 : Int) ≤ (0 : Int) ) -- true
#eval (0 : Int) ≤ (0 : Int) -- true
#eval (7 : Int) ≤ (10 : Int) -- true
```

Implemented by efficient native code.  -/
Int.decLe : (a b : ℤ) → Decidable (a ≤ b)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A morphism `k : W ⟶ X` satisfying `∀ j₁ j₂, k ≫ f j₁ = k ≫ f j₂` induces a morphism
`l : W ⟶ wideEqualizer f` satisfying `l ≫ wideEqualizer.ι f = k`.  -/
CategoryTheory.Limits.wideEqualizer.lift' : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] →
            [Nonempty J] →
              {W : C} →
                (k : W ⟶ X) →
                  (∀ (j₁ j₂ : J),
                      CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)) →
                    { l // CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.wideEqualizer.ι f) = k }
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.function_commute_add_left : ∀ {G : Type u_1} [inst : AddSemigroup G] {a b : G}, AddCommute a b → Function.Commute (fun x => a + x) fun x => b + x
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a `k`-linear `G`-representation `(V, ρ)`, this is the linear equivalence
`(V ⊗ k[G])_G ≃ₗ[k] V` sending `⟦v ⊗ single g r⟧ ↦ r • ρ(g⁻¹)(v)`.  -/
Representation.coinvariantsTprodLeftRegularLEquiv : {k : Type u_6} →
  {G : Type u_7} →
    {V : Type u_8} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) → (ρ.tprod (Representation.leftRegular k G)).Coinvariants ≃ₗ[k] V
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm.congr_simp : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S],
  Ideal.absNorm = Ideal.absNorm
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.elim_stack : ∀ (a b c d : List Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.stack = d
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddCommGroup.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α], Colex.instAddCommGroup = { toAddGroup := Colex.instAddGroup, add_comm := ⋯ }
-- Mathlib.LinearAlgebra.QuadraticForm.Real
/-- **Sylvester's law of inertia**: A real quadratic form is equivalent to a weighted
sum of squares with the weights being ±1 or 0, `SignType` version.  -/
QuadraticForm.equivalent_signType_weighted_sum_squared : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M),
  ∃ w, QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instSetLike : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → SetLike (OpenAddSubgroup G) G
-- Mathlib.Geometry.Manifold.Instances.Real
Icc_isBoundaryPoint_bot : ∀ {x y : ℝ} [hxy : Fact (x < y)], (modelWithCornersEuclideanHalfSpace 1).IsBoundaryPoint ⊥
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instDecidableEqOffset : DecidableEq Std.Time.Millisecond.Offset