mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Units.Defs
/-- See `isUnit_iff_exists_and_exists` for a similar lemma with two existentials.  -/
isUnit_iff_exists : ∀ {M : Type u_1} [inst : Monoid M] {x : M}, IsUnit x ↔ ∃ b, x * b = 1 ∧ b * x = 1
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.le_kernelSubobject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] (A : CategoryTheory.Subobject X),
  CategoryTheory.CategoryStruct.comp A.arrow f = 0 → A ≤ CategoryTheory.Limits.kernelSubobject f
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSheafFor_over_map_op_comp_ofArrows_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {B B' : C} (p : B ⟶ B')
  (P : CategoryTheory.Functor (CategoryTheory.Over B')ᵒᵖ (Type w)) {X : CategoryTheory.Over B}
  {Y : I → CategoryTheory.Over B} (f : (i : I) → Y i ⟶ X),
  CategoryTheory.Presieve.IsSheafFor ((CategoryTheory.Over.map p).op.comp P) (CategoryTheory.Presieve.ofArrows Y f) ↔
    CategoryTheory.Presieve.IsSheafFor P
      (CategoryTheory.Presieve.ofArrows (fun i => (CategoryTheory.Over.map p).obj (Y i)) fun i =>
        (CategoryTheory.Over.map p).map (f i))
-- Mathlib.Topology.Germ
/-- If the germ of `f` w.r.t. each `𝓝 x` is constant, `f` is locally constant.  -/
IsLocallyConstant.of_germ_isConstant : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  (∀ (x : X), (↑f).IsConstant) → IsLocallyConstant f
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.isIso_homologyMap_shortComplexTruncLE_g : ∀ {ι : 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.Abelian C] (K : HomologicalComplex C c')
  (e : c.Embedding c') [inst_2 : e.IsTruncLE] (i' : ι'),
  (∀ (i : ι), e.f i ≠ i') → CategoryTheory.IsIso (HomologicalComplex.homologyMap (K.shortComplexTruncLE e).g i')
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.comp_reflectsLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
  [CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (F.comp G)
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.jacobson_mono : ∀ {R : Type u} [inst : Ring R] {I J : Ideal R}, I ≤ J → I.jacobson ≤ J.jacobson
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.toEnd_eq_zero_iff : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieModule.IsFaithful R L M] {x : L}, (LieModule.toEnd R L M) x = 0 ↔ x = 0
-- Mathlib.Data.Sym.Basic
Sym.cons_of_coe_eq : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n), a ::ₛ Sym.ofVector v = Sym.ofVector (a ::ᵥ v)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_le_minKeyD_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false →
    ∀ {fallback : α},
      (compare (t.minKeyD fallback) ((Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKeyD fallback)).isLE = true
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.SublistForall₂.sum_le_sum : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddRightMono M] [AddLeftMono M] {l₁ l₂ : List M},
  List.SublistForall₂ (fun x1 x2 => x1 ≤ x2) l₁ l₂ → (∀ a ∈ l₂, 0 ≤ a) → l₁.sum ≤ l₂.sum
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- The Fourier integral of the Fréchet derivative of a function is obtained by multiplying the
Fourier integral of the original function by `2πI ⟪v, w⟫`.  -/
Real.fourier_fderiv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {f : V → E},
  MeasureTheory.Integrable f MeasureTheory.volume →
    Differentiable ℝ f →
      MeasureTheory.Integrable (fderiv ℝ f) MeasureTheory.volume →
        FourierTransform.fourier (fderiv ℝ f) = VectorFourier.fourierSMulRight (-innerSL ℝ) (FourierTransform.fourier f)
-- Lean.Data.PersistentArray
_private.Lean.Data.PersistentArray.0.Lean.List.toPArray'.loop : {α : Type u} → List α → Lean.PersistentArray α → Lean.PersistentArray α
-- Lean.PrivateName
Lean.mkPrivateNameCore : Lean.Name → Lean.Name → Lean.Name
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_self_re_eq_norm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), RCLike.re (inner 𝕜 x x) = ‖inner 𝕜 x x‖
-- Mathlib.Tactic.Ring.Common
/-- `ExProd BaseType sα e` stores the structure of a normalized monomial expression `e`.
A monomial here is a product of powers of `ExBase` expressions, terminated by a (nonzero) constant
coefficient. The data of the constant coefficient is stored in the `BaseType`.  -/
Mathlib.Tactic.Ring.Common.ExProd : {u : Lean.Level} → {α : Q(Type u)} → (Q(«$α») → Type) → Q(CommSemiring «$α») → Q(«$α») → Type
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_X_pow : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] (n : ℕ), (Polynomial.X ^ n).trailingDegree = ↑n
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableOn_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {s : Set E}, DifferentiableOn 𝕜 0 s
-- Mathlib.Algebra.BigOperators.Group.Finset.Powerset
/-- A product over `powerset s` is equal to the double product over sets of subsets of `s` with
`#s = k`, for `k = 0, ..., #s`.  -/
Finset.prod_powerset : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid β] (s : Finset α) (f : Finset α → β),
  ∏ t ∈ s.powerset, f t = ∏ j ∈ Finset.range (s.card + 1), ∏ t ∈ Finset.powersetCard j s, f t
-- Mathlib.Topology.ClusterPt
/-- Variant of `accPt_iff_frequently`: A point `x` is an accumulation point of a set `C` iff points in
punctured neighborhoods are frequently contained in `C`.
 -/
accPt_iff_frequently_nhdsNE : ∀ {X : Type u_3} [inst : TopologicalSpace X] {x : X} {C : Set X},
  AccPt x (Filter.principal C) ↔ ∃ᶠ (y : X) in nhdsWithin x {x}ᶜ, y ∈ C
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Auxiliary method for adding a global declaration to a `SimpTheorems` datastructure.  -/
Lean.Meta.SimpTheorems.addConst : Lean.Meta.SimpTheorems →
  Lean.Name → optParam Bool true → optParam Bool false → optParam ℕ 1000 → Lean.MetaM Lean.Meta.SimpTheorems
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with the 202 status code.
 -/
Std.Http.Response.accepted : Std.Http.Response.Builder
-- Mathlib.Topology.Defs.Basic
/-- Converts an element of `X` to an element of `WithTopology X t`.  -/
WithTopology.toTopology : {X : Type u_1} → (t : TopologicalSpace X) → X → WithTopology X t
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.singleMapHomologicalComplex_hom_app_ne : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] [inst_4 : CategoryTheory.Limits.HasZeroObject W₁]
  [inst_5 : CategoryTheory.Limits.HasZeroObject W₂] (F : CategoryTheory.Functor W₁ W₂)
  [inst_6 : F.PreservesZeroMorphisms] (c : ComplexShape ι) [inst_7 : DecidableEq ι] {i j : ι},
  i ≠ j → ∀ (X : W₁), ((HomologicalComplex.singleMapHomologicalComplex F c j).hom.app X).f i = 0
-- Mathlib.Topology.Homotopy.Path
/-- The image of a path homotopy class `P₀` under a map `f`.
This is `Path.map` descended to the quotient.  -/
Path.Homotopic.Quotient.map : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {x₀ x₁ : X} → Path.Homotopic.Quotient x₀ x₁ → (f : C(X, Y)) → Path.Homotopic.Quotient (f x₀) (f x₁)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput.hle : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {old : Std.Sat.AIG α} {w : ℕ}
  (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput old w),
  old.decls.size ≤ self.aig.decls.size
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso_inv_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  [inst_4 : CategoryTheory.Limits.HasKernels Cᵒᵖ] [inst_5 : CategoryTheory.Limits.HasCokernels Cᵒᵖ]
  (X : (CategoryTheory.ShortComplex C)ᵒᵖ),
  (CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso C).inv.app X = (Opposite.unop X).rightHomologyOpIso.hom
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.of_apply : ∀ (R : Type u_8) (M : Type u_9) [inst : Semiring R] [inst_1 : MulOneClass M] (a : M),
  (MonoidAlgebra.of R M) a = MonoidAlgebra.single a 1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.coreToInt.inj : ∀ {a b toIntThm : Lean.Expr} {lhs rhs : Int.Internal.Linear.Expr} {a_1 b_1 toIntThm_1 : Lean.Expr}
  {lhs_1 rhs_1 : Int.Internal.Linear.Expr},
  Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.coreToInt a b toIntThm lhs rhs =
      Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.coreToInt a_1 b_1 toIntThm_1 lhs_1 rhs_1 →
    a = a_1 ∧ b = b_1 ∧ toIntThm = toIntThm_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_induction : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] (s : Finset α) (f : α → β)
  (comm : (↑s).Pairwise (Function.onFun AddCommute f)) (p : β → Prop),
  (∀ (a b : β), p a → p b → p (a + b)) → p 0 → (∀ x ∈ s, p (f x)) → p (s.noncommSum f comm)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  m.getKey? k = some k' → (Std.ExtHashMap.filterMap f m)[k]! = (m[k]?.bind (f k')).get!
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.const.injEq : ∀ (decl decl_1 : Lean.Name), (Aesop.ElabRuleTerm.const decl = Aesop.ElabRuleTerm.const decl_1) = (decl = decl_1)
-- Init.Data.Order.Ord
/-- Swapping the arguments to `cmp` swaps the outcome.  -/
Std.OrientedCmp.eq_swap : ∀ {α : Type u} {cmp : α → α → Ordering} [self : Std.OrientedCmp cmp] {a b : α}, cmp a b = (cmp b a).swap
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.instSMulCommClassAEEqFun_2 : ∀ {M : Type u_3} {N : Type u_1} {α : Type u_2} {β : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : SMul M α] [inst_3 : MeasurableConstSMul M α]
  [inst_4 : MeasureTheory.SMulInvariantMeasure M α μ] [inst_5 : SMul N α] [inst_6 : MeasurableConstSMul N α]
  [inst_7 : MeasureTheory.SMulInvariantMeasure N α μ] [SMulCommClass M N α], SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ (α →ₘ[μ] β)
-- Mathlib.Data.Fin.Tuple.Basic
/-- The tail of an `n+1` tuple, i.e., its last `n` entries.  -/
Fin.tail : {n : ℕ} → {α : Fin (n + 1) → Sort u} → ((i : Fin (n + 1)) → α i) → (i : Fin n) → α i.succ
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsInt.to_isNat : ∀ {α : Type u_1} [inst : Ring α] {a : α} {n : ℕ},
  Mathlib.Meta.NormNum.IsInt a (Int.ofNat n) → Mathlib.Meta.NormNum.IsNat a n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_alter_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)} {h : k ∈ m.alter k f}, (m.alter k f).get k h = (f (m.get? k)).get ⋯
-- Lean.Elab.PatternVar
Lean.Elab.Term.PatternVar : Type
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
/-- **Alias** of `UniqueFactorizationMonoid.strongNormalizationMonoid`.

---

Noncomputably defines a `StrongNormalizationMonoid` structure on a `UniqueFactorizationMonoid`.
 -/
UniqueFactorizationMonoid.normalizationMonoid : {α : Type u_1} → [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → StrongNormalizationMonoid α
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- "Left-handed" version of the natural product map on measures (acting on functions
as first integrating along `X`, and then integrating the result along `Y`).  -/
AbstractMeasure.prodMk : {X : Type u_1} →
  {Y : Type u_2} →
    {R : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : CommRing R] →
            [inst_3 : TopologicalSpace R] →
              [inst_4 : IsTopologicalRing R] →
                [LocallyCompactSpace X] →
                  [LocallyCompactSpace Y] →
                    AbstractMeasure X R R →ₗ[R] AbstractMeasure Y R R →ₗ[R] AbstractMeasure (X × Y) R R
-- Mathlib.Topology.Order.IsLUB
/-- The lower bounds of the image of a continuous function on a dense set are equal to the lower
bounds of the range of the universe.  -/
Dense.lowerBounds_image : ∀ {γ : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] {f : γ → α}
  [inst_3 : TopologicalSpace γ] {S : Set γ}, Dense S → Continuous f → lowerBounds (f '' S) = lowerBounds (Set.range f)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.range_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [Nonempty α] [inst_2 : Zero β],
  MeasureTheory.SimpleFunc.range 0 = {0}
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.quotientPiLift_mk : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] {Ns : ι → Type u_5} [inst_3 : (i : ι) → AddCommGroup (Ns i)]
  [inst_4 : (i : ι) → Module R (Ns i)] (p : (i : ι) → Submodule R (Ms i)) (f : (i : ι) → Ms i →ₗ[R] Ns i)
  (hf : ∀ (i : ι), p i ≤ (f i).ker) (x : (i : ι) → Ms i),
  (Submodule.quotientPiLift p f hf) (Submodule.Quotient.mk x) = fun i => (f i) (x i)
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.μ_bddAbove' : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R),
  μ 1 ≤ 1 →
    ∀ {s : ℕ → ℕ},
      (∀ (n : ℕ), s n ≤ n) → ∀ (x : R) (ψ : ℕ → ℕ), BddAbove ((fun n => μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) '' Set.univ)
-- Mathlib.Topology.Algebra.Monoid
instSeparatelyContinuousMulULift : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M],
  SeparatelyContinuousMul (ULift.{u, u_3} M)
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.coeff_one_Xzero : ∀ {R : Type u_1} [inst : CommRing R] (F : FormalGroup R), (PowerSeries.coeff 1) F.Xzero = 1
-- Std.Data.ByteSlice
ByteSlice.size_le_size_byteArray : ∀ {s : ByteSlice}, s.size ≤ s.byteArray.size
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.setRoot.eq_2 : ∀ {α : Type u_1} (v : α) (c : RBTree.RBColor) (a : RBTree.RBNode α) (v_1 : α) (b : RBTree.RBNode α),
  RBTree.RBNode.setRoot v (RBTree.RBNode.node c a v_1 b) = RBTree.RBNode.node c a v b
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `_private.Mathlib.Combinatorics.Matroid.Basic.0.Matroid.sdiff_subset_ground`. -/
Matroid.diff_subset_ground : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, X ⊆ M.E → X \ Y ⊆ M.E
-- Mathlib.GroupTheory.Submonoid.Center
AddSubsemigroup.centerCongr_symm_apply_coe : ∀ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) (s : ↥(AddSubsemigroup.center N)),
  ↑((AddSubsemigroup.centerCongr e).symm s) = e.symm ↑s
-- Init.Control.State
/-- Retrieves the current value of the monad's mutable state.

This increments the reference count of the state, which may inhibit in-place updates.
 -/
StateT.get : {σ : Type u} → {m : Type u → Type v} → [Monad m] → StateT σ m σ
-- Mathlib.Data.Multiset.Bind
Multiset.prod_join : ∀ {α : Type u_1} [inst : CommMonoid α] {S : Multiset (Multiset α)}, S.join.prod = (Multiset.map Multiset.prod S).prod
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.Context.mk : Lean.Meta.Simp.Config →
  Lean.Options →
    Lean.FVarIdSet →
      Lean.FVarIdSet →
        Lean.Meta.ConfigWithKey →
          Lean.Meta.ConfigWithKey →
            UInt32 →
              Lean.Meta.SimpTheoremsArray →
                Lean.Meta.SimpCongrTheorems → Option Lean.Expr → UInt32 → ℕ → Bool → Lean.Meta.Simp.Context
-- Mathlib.Topology.Instances.Matrix
Summable.matrix_blockDiag' : ∀ {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} {f : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R},
  Summable f L → Summable (fun x => (f x).blockDiag') L
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_const : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G]
  [MeasureTheory.IsFiniteMeasure μ.variation] (c : E), ∫ᵛ (x : X), c ∂[B; μ] = (B c) (μ Set.univ)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderivWithin_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s t : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [ContinuousAdd F] [ContinuousSMul 𝕜 F] [T2Space F],
  t ∈ nhdsWithin x s →
    UniqueDiffWithinAt 𝕜 s x → DifferentiableWithinAt 𝕜 f t x → fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittMul_vars : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), (WittVector.wittMul p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Mathlib.Tactic.FunProp.Types
/-- Cache storing failed goals such that they are not tried again.  -/
Mathlib.Meta.FunProp.State.failureCache : Mathlib.Meta.FunProp.State → Lean.ExprSet
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_coe : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S] (I : Ideal S), Ideal.comap (↑f) I = Ideal.comap f I
-- Mathlib.Algebra.Category.MonCat.Yoneda
/-- The Hom bifunctor sending a type `X` and a commutative monoid `M` to the commutative monoid
`X → M` with pointwise operations.

This is also the coyoneda embedding of `Type` into `AddCommMonCat`-valued presheaves of commutative
monoids.  -/
AddCommMonCat.coyonedaType : CategoryTheory.Functor Type uᵒᵖ (CategoryTheory.Functor AddCommMonCat AddCommMonCat)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.forgetCreatesPullbackOfLeft : {X Y Z : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      [H : AlgebraicGeometry.IsOpenImmersion f] →
        CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan f g)
          AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Mathlib.Data.List.Basic
List.replicate_left_inj : ∀ {α : Type u} {a : α} {n m : ℕ}, List.replicate n a = List.replicate m a ↔ n = m
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {k : α} {v : β k}, m.get? k = some v ↔ ∃ (h : k ∈ m), m.get k h = v
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.id_left : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented C),
  (CategoryTheory.CategoryStruct.id X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.instFiniteIndexGamma : ∀ (N : ℕ) [NeZero N], (CongruenceSubgroup.Gamma N).FiniteIndex
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.addXYZ_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  W'.Equation P → W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![1, 1, 0]
-- Mathlib.Algebra.WithConv
WithConv.ext : ∀ {A : Type u_2} {x y : WithConv A}, x.ofConv = y.ofConv → x = y
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k},
      Std.Internal.List.minKey (Std.Internal.List.insertEntry k v l) ⋯ =
        (Std.Internal.List.minKey? l).elim k fun k' => if (compare k k').isLE = true then k else k'
-- Lean.AuxRecursor
Lean.markAuxRecursor : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (unit : CategoryTheory.Functor.id C ⟶ F.comp G)
  (counit : G.comp F ⟶ CategoryTheory.Functor.id D)
  (left_triangle_components :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (F.map (unit.app X)) (counit.app (F.obj X)) =
          CategoryTheory.CategoryStruct.id (F.obj X))
      CategoryTheory.Adjunction.left_triangle_components._autoParam)
  (right_triangle_components :
    autoParam
      (∀ (Y : D),
        CategoryTheory.CategoryStruct.comp (unit.app (G.obj Y)) (G.map (counit.app Y)) =
          CategoryTheory.CategoryStruct.id (G.obj Y))
      CategoryTheory.Adjunction.right_triangle_components._autoParam)
  (unit_1 : CategoryTheory.Functor.id C ⟶ F.comp G) (counit_1 : G.comp F ⟶ CategoryTheory.Functor.id D)
  (left_triangle_components_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (F.map (unit_1.app X)) (counit_1.app (F.obj X)) =
          CategoryTheory.CategoryStruct.id (F.obj X))
      CategoryTheory.Adjunction.left_triangle_components._autoParam)
  (right_triangle_components_1 :
    autoParam
      (∀ (Y : D),
        CategoryTheory.CategoryStruct.comp (unit_1.app (G.obj Y)) (G.map (counit_1.app Y)) =
          CategoryTheory.CategoryStruct.id (G.obj Y))
      CategoryTheory.Adjunction.right_triangle_components._autoParam),
  ({ unit := unit, counit := counit, left_triangle_components := left_triangle_components,
        right_triangle_components := right_triangle_components } =
      { unit := unit_1, counit := counit_1, left_triangle_components := left_triangle_components_1,
        right_triangle_components := right_triangle_components_1 }) =
    (unit = unit_1 ∧ counit = counit_1)
-- Mathlib.Topology.Constructible
Topology.IsConstructible.biUnion : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Type u_4} {f : ι → Set X} {t : Set ι},
  t.Finite → (∀ i ∈ t, Topology.IsConstructible (f i)) → Topology.IsConstructible (⋃ i ∈ t, f i)
-- Mathlib.Topology.Order.Compact
ContinuousOn.sInf_image_Icc_le : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : TopologicalSpace β] [DenselyOrdered α] [inst_5 : ConditionallyCompleteLinearOrder β]
  [OrderTopology β] {f : α → β} {a b c : α},
  ContinuousOn f (Set.Icc a b) → c ∈ Set.Icc a b → sInf (f '' Set.Icc a b) ≤ f c