mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
CategoryTheory.Limits.fiberwiseColimitLimitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  {J : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} J] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (K : CategoryTheory.Functor J (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H))
  [inst_3 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J H]
  [inst_5 : ∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] (X : C),
  (CategoryTheory.Limits.fiberwiseColimitLimitIso K).inv.app X =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation (K.comp (CategoryTheory.Limits.fiberwiseColim F H)) X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.HasLimit.isoOfNatIso
            (K.associator
                ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj X)) (CategoryTheory.Grothendieck F) H).obj
                  (CategoryTheory.Grothendieck.ι F X))
                CategoryTheory.Limits.colim ≪≫
              K.isoWhiskerLeft (CategoryTheory.Limits.fiberwiseColimCompEvaluationIso X).symm ≪≫
                (K.associator (CategoryTheory.Limits.fiberwiseColim F H)
                    ((CategoryTheory.evaluation C H).obj X)).symm)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.preservesLimitIso CategoryTheory.Limits.colim
              (K.comp
                ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj X)) (CategoryTheory.Grothendieck F) H).obj
                  (CategoryTheory.Grothendieck.ι F X)))).inv
          (CategoryTheory.Limits.HasColimit.isoOfNatIso
              (CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit K
                  (CategoryTheory.Grothendieck.ι F X)).symm).inv))
-- Mathlib.Tactic.Sat.FromLRAT
/-- Parse an LRAT file into a list of steps.  -/
Mathlib.Tactic.Sat.Parser.parseLRAT : Std.Internal.Parsec.String.Parser (Array Mathlib.Tactic.Sat.LRATStep)
-- Init.Core
UInt32.ofBitVec.inj : ∀ {toBitVec toBitVec_1 : BitVec 32}, { toBitVec := toBitVec } = { toBitVec := toBitVec_1 } → toBitVec = toBitVec_1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.interSmallerFn : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] [BEq α] (m₁ m₂ : Std.DTreeMap.Internal.Impl α β)
  (hm₂ : m₂.WF) (k : α), (↑(m₁.interSmallerFn ⟨m₂, ⋯⟩ k)).WF
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_finset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s₁ s₂ : Finset β} {a : α},
  a • (s₁ ∪ s₂) = a • s₁ ∪ a • s₂
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.assoc_flip`. -/
CategoryTheory.Mod_.assoc_flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] (M : CategoryTheory.Mod D A),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A CategoryTheory.ModObj.smul)
      CategoryTheory.ModObj.smul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso A A M.X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonObj.mul M.X)
        CategoryTheory.ModObj.smul)
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.normedCommGroup : {E : Type u_2} → [NormedCommGroup E] → NormedCommGroup Eᵒᵈ
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.MemLp.const_smul : ∀ {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] {f : α → F} {𝕜 : Type u_3} [inst_1 : NormedRing 𝕜] [inst_2 : MulActionWithZero 𝕜 F]
  [IsBoundedSMul 𝕜 F], MeasureTheory.MemLp f p μ → ∀ (c : 𝕜), MeasureTheory.MemLp (c • f) p μ
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.lanPresheafNatIso.eq_1 : ∀ {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)}
  (hF :
    (S : LightProfinite) →
      CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))),
  LightCondensed.lanPresheafNatIso hF =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        match x with
        | Opposite.op S => LightCondensed.lanPresheafIso (hF S))
      ⋯
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.coe_top : ∀ {V : Type u} {G : SimpleGraph V} [inst : Finite V], ↑⊤ = ⊤
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
/-- If scalar multiplication by elements of `α` sends `(0 : β)` to zero,
then the same is true for `(0 : Finset β)`.  -/
Finset.smulZeroClass : {α : Type u_1} → {β : Type u_2} → [DecidableEq β] → [inst : Zero β] → [SMulZeroClass α β] → SMulZeroClass α (Finset β)
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_ofNatLT : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatLT n hn).toUInt16 = UInt16.ofNat n
-- Aesop.Search.SearchM
Aesop.SearchM.run : {Q : Type} →
  [inst : Aesop.Queue Q] →
    {α : Type} →
      Aesop.LocalRuleSet →
        Aesop.Options' →
          Lean.Meta.Simp.Config →
            Option Lean.Term → Lean.MVarId → Aesop.SearchM Q α → Aesop.BaseM (α × Aesop.SearchM.State Q × Aesop.Tree)
-- Mathlib.Topology.EMetricSpace.Defs
Metric.nhds_basis_eball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, (nhds x).HasBasis (fun ε => 0 < ε) (Metric.eball x)
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.mk.sizeOf_spec : ∀ {D : Type u_1} {Q : Type u_2} [inst : SizeOf D] [inst_1 : SizeOf Q] (left : Q → D) (right : Q),
  sizeOf { left := left, right := right } = 1 + sizeOf right
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.map_zero_eq_self_iff`. -/
Topology.CWComplex.map_zero_eq_self_iff : ∀ {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [inst : Topology.RelCWComplex C D]
  {x z : Topology.RelCWComplex.cell C 0},
  ↑(Topology.RelCWComplex.map 0 x) ![] = ↑(Topology.RelCWComplex.map 0 z) ![] ↔ x = z
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSets.iUnion : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)} {s' : Set (Set Ω)},
  (∀ (n : ι), ProbabilityTheory.CondIndepSets m' hm' (s n) s' μ) →
    ProbabilityTheory.CondIndepSets m' hm' (⋃ n, s n) s' μ
-- Mathlib.Data.List.MinMax
List.maximum_nil : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α], [].maximum = ⊥
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.repsFintype : (k : ℤ) → Fintype ↑(FixedDetMatrices.reps k)
-- Mathlib.Data.Set.Enumerate
Set.enumerate_inj : ∀ {α : Type u_1} (sel : Set α → Option α) {n₁ n₂ : ℕ} {a : α} {s : Set α},
  (∀ (s : Set α) (a : α), sel s = some a → a ∈ s) →
    Set.enumerate sel s n₁ = some a → Set.enumerate sel s n₂ = some a → n₁ = n₂
-- Mathlib.GroupTheory.Sylow
/-- A generalization of **Sylow's second theorem**.
If the number of Sylow `p`-subgroups is finite, then all Sylow `p`-subgroups are conjugate.  -/
Sylow.isPretransitive_of_finite : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [hp : Fact (Nat.Prime p)] [Finite (Sylow p G)],
  MulAction.IsPretransitive G (Sylow p G)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- A pseudofunctor carries an adjunction `f ⊣ g` to an adjunction `F.map f ⊣ F.map g`.  -/
CategoryTheory.Pseudofunctor.mapAdjunction : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {a b : B} →
          {f : a ⟶ b} →
            {g : b ⟶ a} →
              (F : CategoryTheory.Pseudofunctor B C) →
                CategoryTheory.Bicategory.Adjunction f g → CategoryTheory.Bicategory.Adjunction (F.map f) (F.map g)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotencyClass_le_of_surjective`.

---

The nilpotency class of the range of a surjective homomorphism from a
nilpotent group is less or equal the nilpotency class of the domain.  -/
nilpotencyClass_le_of_surjective : ∀ {G : Type u_1} [inst : Group G] {G' : Type u_2} [inst_1 : Group G'] (f : G →* G'),
  Function.Surjective ⇑f → ∀ [h : Group.IsNilpotent G], Group.nilpotencyClass G' ≤ Group.nilpotencyClass G
-- Mathlib.Control.Random
BoundedRandom.mk : {m : Type u → Type u_1} →
  {α : Type u} →
    [inst : Preorder α] →
      ({g : Type} → (lo hi : α) → lo ≤ hi → [RandomGen g] → RandGT g m { a // lo ≤ a ∧ a ≤ hi }) → BoundedRandom m α
-- Batteries.Recycling.RBTree.Basic
/-- Returns `red` if the node is red, otherwise `black`. (Nil nodes are treated as `black`.)  -/
RBTree.RBNode.isRed : {α : Type u_1} → RBTree.RBNode α → RBTree.RBColor
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_apply : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {p : α → Prop} {a : Subtype p} {v : α →₀ M},
  (Finsupp.subtypeDomain p v) a = v ↑a
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.FirstByte.done.sizeOf_spec : sizeOf ByteArray.utf8DecodeChar?.FirstByte.done = 1
-- Batteries.Tactic.GeneralizeProofs
_private.Batteries.Tactic.GeneralizeProofs.0.Batteries.Tactic.GeneralizeProofs.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Batteries.Tactic.GeneralizeProofs.Config
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Preconnected.map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (f : G →g H),
  Function.Surjective ⇑f → G.Preconnected → H.Preconnected
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.sectionsMk.congr_simp : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  (d d_1 : F.WellOrderInductionData),
  d = d_1 →
    ∀ [inst_2 : OrderBot J] [inst_3 : WellFoundedLT J] (val₀ val₀_1 : F.obj (Opposite.op ⊥)),
      val₀ = val₀_1 → d.sectionsMk val₀ = d_1.sectionsMk val₀_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.contains_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).contains k = (f (Std.DTreeMap.Raw.Const.get? t k)).isSome
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.quotientToEndObjectHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {F : CategoryTheory.Functor C FintypeCat} →
      [inst_1 : CategoryTheory.GaloisCategory C] →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          (V : OpenSubgroup (CategoryTheory.Aut F)) →
            {U : OpenSubgroup (CategoryTheory.Aut F)} →
              (h : (↑U).Normal) →
                {A : C} →
                  ((CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
                      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F)
                        (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U))) →
                    ↥↑V ⧸ (↑U).subgroupOf ↑V →* CategoryTheory.End A
-- Mathlib.RingTheory.KrullDimension.Basic
Ring.KrullDimLE.mk₀ : ∀ {R : Type u_1} [inst : CommSemiring R], (∀ (I : Ideal R), I.IsPrime → I.IsMaximal) → Ring.KrullDimLE 0 R
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
CategoryTheory.IsRegularEpi.exists_of_isKernelPair : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (π : X ⟶ Y) [CategoryTheory.IsRegularEpi π] {Z : C}
  {fst snd : Z ⟶ X},
  CategoryTheory.IsKernelPair π fst snd →
    ∀ {W : C} (f : X ⟶ W),
      CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd f →
        ∃ g, CategoryTheory.CategoryStruct.comp π g = f
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- Copy of a sub_mul_action with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
SubMulAction.copy : {R : Type u} → {M : Type v} → [inst : SMul R M] → (p : SubMulAction R M) → (s : Set M) → s = ↑p → SubMulAction R M
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- An orthogonal basis with respect to a nondegenerate bilinear form has no self-orthogonal
elements.  -/
LinearMap.BilinForm.iIsOrtho.not_isOrtho_basis_self_of_nondegenerate : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : Type w}
  [Nontrivial R] {B : LinearMap.BilinForm R M} {v : Module.Basis n R M},
  B.iIsOrtho ⇑v → B.Nondegenerate → ∀ (i : n), (B (v i)) (v i) ≠ 0
-- Mathlib.Algebra.Algebra.Unitization
/-- The minimal unitization of a non-unital `R`-algebra `A`. This is just a structure wrapper for
`R × A`.  -/
Unitization : Type u_1 → Type u_2 → Type (max u_1 u_2)
-- Init.Data.Vector.OfFn
_private.Init.Data.Vector.OfFn.0.Vector.ofFnM.go.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] (f : Fin n → m α) (i : ℕ) (h' : i ≤ n)
  (acc : Array α) (w : acc.size = i),
  Vector.ofFnM.go✝ f i h' acc w =
    if h : i < n then do
      let __do_lift ← f ⟨i, h⟩
      Vector.ofFnM.go✝ f (i + 1) ⋯ (acc.push __do_lift) ⋯
    else pure (Vector.mk acc ⋯)
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.Kind.fromCache.sizeOf_spec : sizeOf Mathlib.Tactic.LibraryRewrite.Kind.fromCache = 1
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.sup_apply : ∀ (f g : CircleDeg1Lift) (x : ℝ), (f ⊔ g) x = max (f x) (g x)
-- Mathlib.Data.List.Sort
/-- Variant of `Perm.eq_of_pairwise` using relation typeclasses.  -/
List.Perm.eq_of_pairwise' : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Antisymm r] {l₁ l₂ : List α},
  List.Pairwise r l₁ → List.Pairwise r l₂ → l₁.Perm l₂ → l₁ = l₂
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_dite_of_true : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : AddCommMonoid M] {p : ι → Prop} [inst_1 : DecidablePred p]
  (h : ∀ i ∈ s, p i) (f : (i : ι) → p i → M) (g : (i : ι) → ¬p i → M),
  (∑ i ∈ s, if hi : p i then f i hi else g i hi) = ∑ i, f ↑i ⋯
-- Mathlib.Algebra.Field.NegOnePow
Int.cast_negOnePow : ∀ (K : Type u_1) (n : ℤ) [inst : DivisionRing K], ↑↑n.negOnePow = (-1) ^ n
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.iteratedLineDerivOp_zero : ∀ {V : Type u_5} {E : Type u_6} [inst : LineDeriv V E E] {n : ℕ} (m : Fin n → V) [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup E] [LineDerivAdd V E E], LineDeriv.iteratedLineDerivOp m 0 = 0
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.homogeneousHull_eq_iSup : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜] (I : Ideal A),
  Ideal.homogeneousHull 𝒜 I = ⨆ i, { toSubmodule := Ideal.span (⇑(GradedRing.proj 𝒜 i) '' ↑I), is_homogeneous' := ⋯ }
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The bornology on `WeakDual 𝕜 F` is the norm bornology inherited from `StrongDual 𝕜 F`.

Note: This is a pragmatic choice. To be precise, the bornology of a weak topology should be
the von Neumann bornology (pointwise boundedness). However, in the normed setting,
`IsBounded` is most useful when referring to the operator norm (e.g., to state
Banach-Alaoglu concisely).

Pointwise boundedness is instead captured by `Bornology.IsVonNBounded`.
For Banach spaces, these notions coincide via `isBounded_iff_isVonNBounded`.
See the module docstring for more details.  -/
WeakDual.instBornology : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → Bornology (WeakDual 𝕜 E)
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The suggestions that close the goal.  -/
Mathlib.Tactic.ClickSuggestions.State.solvedSuggestions : Mathlib.Tactic.ClickSuggestions.State → Array ProofWidgets.Html
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instZero.eq_1 : ∀ {α : Type u_1} [inst : Zero α], Lex.instZero = inst
-- Mathlib.CategoryTheory.ConnectedComponents
/-- Each connected component of the category is connected.  -/
CategoryTheory.instIsConnectedComponent : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] (j : CategoryTheory.ConnectedComponents J),
  CategoryTheory.IsConnected j.Component
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.Context.mk.sizeOf_spec : ∀ (elaborator : Lean.Name) (recover : Bool),
  sizeOf { elaborator := elaborator, recover := recover } = 1 + sizeOf elaborator + sizeOf recover
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformlyOn.exists_multipliableUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {x : β} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] [LocallyCompactSpace β],
  MultipliableLocallyUniformlyOn f s → s ∈ nhds x → ∃ t ∈ nhdsWithin x s, MultipliableUniformlyOn f t
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.mkComputedFieldOverrides : Lean.Name → Array Lean.Name → Lean.MetaM Unit
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
/-- `factorPow` for `n = m + 1`  -/
Submodule.factorPowSucc : {R : Type u_1} →
  [inst : Ring R] →
    (I : Ideal R) →
      (M : Type u_2) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (m : ℕ) → M ⧸ I ^ (m + 1) • ⊤ →ₗ[R] M ⧸ I ^ m • ⊤
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- The property of being a sheaf is preserved by isomorphism.  -/
CategoryTheory.Presieve.isSheaf_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (J : CategoryTheory.GrothendieckTopology C) {P' : CategoryTheory.Functor Cᵒᵖ (Type w)} (i : P ≅ P'),
  CategoryTheory.Presieve.IsSheaf J P → CategoryTheory.Presieve.IsSheaf J P'
-- Init.Data.SInt.Basic
Int16.toBitVec.inj : ∀ {x y : Int16}, x.toBitVec = y.toBitVec → x = y
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_singleton_eq_bot : ∀ {α : Type u} [inst : Semiring α] {x : α}, Ideal.span {x} = ⊥ ↔ x = 0
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.coevaluation_comp_leftAdjointMate : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasLeftDual X] [inst_3 : CategoryTheory.HasLeftDual Y] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (η_ (ᘁY) Y) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ᘁf) Y) =
    CategoryTheory.CategoryStruct.comp (η_ (ᘁX) X) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (ᘁX) f)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_eq_top_iff`. -/
Metric.infEdist_eq_top_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, Metric.infEDist x s = ⊤ ↔ s = ∅
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_closure_iff : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α], Bornology.IsBounded (closure s) ↔ Bornology.IsBounded s
-- Mathlib.Algebra.NeZero
zero_ne_one : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : One α] [NeZero 1], 0 ≠ 1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.precomp_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle G K n) (f : F ⟶ G),
  ↑(z.precomp f) = (CochainComplex.HomComplex.Cochain.ofHom f).comp ↑z ⋯
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
/-- If an initial object `0` exists in a CCC then `0^B ≅ 1` for any `B`.  -/
CategoryTheory.powZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {B : C} →
        [CategoryTheory.BraidedCategory C] →
          {I : C} →
            CategoryTheory.Limits.IsInitial I →
              [inst_3 : CategoryTheory.MonoidalClosed C] → I ⟹ B ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.updateLambda!Impl : Lean.Expr → Lean.BinderInfo → Lean.Expr → Lean.Expr → Lean.Expr
-- Lean.Elab.Match
/-- This method is part of the "discriminant refinement" procedure. It in invoked when the
type of the `pattern` does not match the expected type. The expected type is based on the
motive computed using the `match` discriminants.
It tries to compute a path to an index of the discriminant type.
For example, suppose the user has written
```
inductive Mem (a : α) : List α → Prop where
  | head {as} : Mem a (a::as)
  | tail {as} : Mem a as → Mem a (a'::as)

infix:50 " ∈ " => Mem

example (a b : Nat) (h : a ∈ [b]) : b = a :=
match h with
| Mem.head => rfl
```
The motive for the match is `a ∈ [b] → b = a`, and get a type mismatch between the type
of `Mem.head` and `a ∈ [b]`. This procedure return the path `[2, 1]` to the index `b`.
We use it to produce the following refinement
```
example (a b : Nat) (h : a ∈ [b]) : b = a :=
match b, h with
| _, Mem.head => rfl
```
which produces the new motive `(x : Nat) →  a ∈ [x] → x = a`
After this refinement step, the `match` is elaborated successfully.

This method relies on the fact that the dependent pattern matcher compiler solves equations
between indices of indexed inductive families.
The following kinds of equations are supported by this compiler:
- `x = t`
- `t = x`
- `ctor ... = ctor ...`

where `x` is a free variable, `t` is an arbitrary term, and `ctor` is constructor.
Our procedure ensures that "information" is not lost, and will *not* succeed in an
example such as
```
example (a b : Nat) (f : Nat → Nat) (h : f a ∈ [f b]) : f b = f a :=
  match h with
  | Mem.head => rfl
```
and will not add `f b` as a new discriminant. We may add an option in the future to
enable this more liberal form of refinement.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.findDiscrRefinementPath : Lean.Expr → Lean.Expr → OptionT Lean.MetaM (List ℕ)
-- Mathlib.Control.Bifunctor
Bifunctor.fst_snd : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α₀ α₁ : Type u₀} {β₀ β₁ : Type u₁}
  (f : α₀ → α₁) (f' : β₀ → β₁) (x : F α₀ β₀), Bifunctor.fst f (Bifunctor.snd f' x) = bimap f f' x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_of_mem_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k}, a ∈ m.insert k v → (k == a) = false → a ∈ m
-- Mathlib.Data.List.MinMax
List.minimum_mem : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] {l : List α} {m : α}, l.minimum = ↑m → m ∈ l
-- Mathlib.Dynamics.Ergodic.Function
/-- Let `f : α → α` be a (quasi)ergodic map. Let `g : α → X` be a null-measurable function
from `α` to a nonempty space with a countable family of measurable sets
separating points of a set `s` such that `g x ∈ s` for a.e. `x`.
If `g` is a.e.-invariant under `f`, then `g` is a.e. constant.  -/
QuasiErgodic.ae_eq_const_of_ae_eq_comp_of_ae_range₀ : ∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Nonempty X]
  [inst_2 : MeasurableSpace X] {s : Set X} [MeasurableSpace.CountablySeparated ↑s] {f : α → α} {g : α → X},
  QuasiErgodic f μ →
    (∀ᵐ (x : α) ∂μ, g x ∈ s) → MeasureTheory.NullMeasurable g μ → g ∘ f =ᵐ[μ] g → ∃ c, g =ᵐ[μ] Function.const α c
-- Std.Data.Internal.List.Associative
Std.Internal.List.eraseKey_cons_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.eraseKey k (⟨k, v⟩ :: l) = l
-- Mathlib.Tactic.IntervalCases
/-- A `Methods` implementation for `ℤ`.
This tells `interval_cases` how to work on integers.  -/
Mathlib.Tactic.IntervalCases.intMethods : Mathlib.Tactic.IntervalCases.Methods
-- Std.Do.WP.Monad
Std.Do.Except.instWPMonad : {ε : Type u_1} → Std.Do.WPMonad (Except ε) (Std.Do.PostShape.except ε Std.Do.PostShape.pure)