mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.MonadicityInternal.unitCofork_pt : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} (A : adj.toMonad.Algebra)
  [inst_2 : CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))],
  (CategoryTheory.Monad.MonadicityInternal.unitCofork A).pt =
    G.obj (CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.obj A.A)))
-- Mathlib.Algebra.Group.Basic
mul_zpow_self : ∀ {G : Type u_3} [inst : Group G] (a : G) (n : ℤ), a ^ n * a = a ^ (n + 1)
-- Mathlib.Data.PFun
PFun.comp_id : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β), f.comp (PFun.id α) = f
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_eq_ofReal_of_isSelfAdjoint : ∀ {K : Type u_1} [inst : RCLike K] {x : K} {y : ℝ}, IsSelfAdjoint x → (RCLike.re x = y ↔ x = ↑y)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Choose a representative element from a given archimedean class.  -/
ArchimedeanClass.out : {M : Type u_1} →
  [inst : AddCommGroup M] → [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → ArchimedeanClass M → M
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.hurwitzEvenFEPair.eq_1 : ∀ (a : UnitAddCircle),
  HurwitzZeta.hurwitzEvenFEPair a =
    { f := Complex.ofReal ∘ HurwitzZeta.evenKernel a, g := Complex.ofReal ∘ HurwitzZeta.cosKernel a, k := 1 / 2, ε := 1,
      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := HurwitzZeta.hurwitzEvenFEPair._proof_7,
      hε := HurwitzZeta.hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHSubOffset_6 : HSub Std.Time.PlainDateTime Std.Time.Nanosecond.Offset Std.Time.PlainDateTime
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_lt_iff_dist_coe_center_lt : ∀ {z w : UpperHalfPlane} {r : ℝ}, dist z w < r ↔ dist ↑z ↑(w.center r) < w.im * Real.sinh r
-- Aesop.Builder.Basic
Aesop.CoreRuleBuilderOutput.mk.sizeOf_spec : ∀ (ruleExprName : Lean.Name) (builderName : Aesop.BuilderName) (scopeName : Aesop.ScopeName) (tac : Aesop.RuleTacDescr)
  (indexingMode : Aesop.IndexingMode) (pattern? : Option Aesop.RulePattern),
  sizeOf
      { ruleExprName := ruleExprName, builderName := builderName, scopeName := scopeName, tac := tac,
        indexingMode := indexingMode, pattern? := pattern? } =
    1 + sizeOf ruleExprName + sizeOf builderName + sizeOf scopeName + sizeOf tac + sizeOf indexingMode + sizeOf pattern?
-- Init.Data.Array.Range
Array.range'_eq_empty_iff : ∀ {s n step : ℕ}, Array.range' s n step = #[] ↔ n = 0
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
/-- The natural transformation `preadditiveYoneda.obj X ⟶ F.op ⋙ preadditiveYoneda.obj (F.obj X)`
when `F : C ⥤ D` is an additive functor between preadditive categories and `X : C`.  -/
CategoryTheory.preadditiveYonedaMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v, u₁} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            (F : CategoryTheory.Functor C D) →
              [F.Additive] →
                (X : C) →
                  CategoryTheory.preadditiveYoneda.obj X ⟶ F.op.comp (CategoryTheory.preadditiveYoneda.obj (F.obj X))
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_same : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)],
  s.piecewise f f = f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.distinct_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) t.keys
-- Init.Data.SInt.Lemmas
Int32.neg_ofInt : ∀ {n : ℤ}, -Int32.ofInt n = Int32.ofInt (-n)
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dCokernelSequence_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_5),
  (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃).X₃ = X.E f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.taylor : ∀ {R : Type u_1} [inst : CommSemiring R] {p : Polynomial R}, p.Splits → ∀ (r : R), ((Polynomial.taylor r) p).Splits
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.le_dual_inv_aux : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] {I J : FractionalIdeal (nonZeroDivisors B) L},
  I ≠ 0 → I * J ≤ 1 → J ≤ FractionalIdeal.dual A K I
-- Mathlib.Order.CompleteLattice.Defs
sInf_le_iff_forall_lt : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α} {l : α}, sInf s ≤ l ↔ ∀ (b : α), l < b → ∃ a ∈ s, a < b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_of_lt_add_left : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] {a b c d : α}, a < b + c → c ≤ d → a < b + d
-- Init.Prelude
Lean.Macro.Methods.mk : (Lean.Syntax → Lean.MacroM (Option Lean.Syntax)) →
  Lean.MacroM Lean.Name →
    (Lean.Name → Lean.MacroM Bool) →
      (Lean.Name → Lean.MacroM (List Lean.Name)) →
        (Lean.Name → Lean.MacroM (List (Lean.Name × List String))) → Lean.Macro.Methods
-- Mathlib.Order.Filter.Extr
IsMaxOn.on_subset : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set α},
  IsMaxOn f t a → s ⊆ t → IsMaxOn f s a
-- Mathlib.Order.Cover
ofDual_wcovBy_ofDual_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : αᵒᵈ}, OrderDual.ofDual a ⩿ OrderDual.ofDual b ↔ b ⩿ a
-- Mathlib.Data.Ordmap.Ordnode
/-- O(m * n). The Cartesian product of two sets: `(a, b) ∈ s.prod t` iff `a ∈ s` and `b ∈ t`.

```
prod {1, 2} {2, 3} = {(1, 2), (1, 3), (2, 2), (2, 3)}
```  -/
Ordnode.prod : {α : Type u_1} → {β : Type u_2} → Ordnode α → Ordnode β → Ordnode (α × β)
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sum.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C D),
  F.sum G = (F.comp (CategoryTheory.Sum.inl_ B D)).sum' (G.comp (CategoryTheory.Sum.inr_ B D))
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.AEStronglyMeasurable.integral_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F}
  [inst_5 : NormedSpace ℝ F],
  AEMeasurable X μ →
    AEMeasurable Y μ →
      MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
        MeasureTheory.AEStronglyMeasurable (fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a))
          μ
-- Mathlib.Combinatorics.Graph.Delete
Graph.deleteEdges_inc : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {F : Set β},
  (G.deleteEdges F).Inc e x ↔ G.Inc e x ∧ e ∉ F
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourier_neg : ∀ {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : FourierTransform E F]
  [FourierAdd E F] (f : E), FourierTransform.fourier (-f) = -FourierTransform.fourier f
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.add : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {cX cY : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X cX μ →
    ProbabilityTheory.HasSubgaussianMGF Y cY μ →
      ProbabilityTheory.HasSubgaussianMGF (fun ω => X ω + Y ω) ((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) μ
-- Lean.Declaration
Lean.Declaration.defnDecl : Lean.DefinitionVal → Lean.Declaration
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
Std.IterM.toArray_append : ∀ {α₁ α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m] {it₁ : Std.IterM m β}
  {it₂ : Std.IterM m β},
  (it₁.append it₂).toArray = do
    let a₁ ← it₁.toArray
    let a₂ ← it₂.toArray
    pure (a₁ ++ a₂)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- Given `x : R` and `f : M →ₗ[R] M'`, `IsLocalizedModule.Away x f` states that `M'`
is isomorphic to the localization of `M` at the submonoid generated by `x`.  -/
IsLocalizedModule.Away : {R : Type u_1} →
  {M : Type u_2} →
    {M' : Type u_3} →
      [inst : CommSemiring R] →
        R →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] → [inst_3 : AddCommMonoid M'] → [inst_4 : Module R M'] → (M →ₗ[R] M') → Prop
-- Mathlib.Topology.Separation.Basic
minimal_nonempty_closed_eq_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X},
  IsClosed s → s.Nonempty → (∀ t ⊆ s, t.Nonempty → IsClosed t → t = s) → ∃ x, s = {x}
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.forget₁_mapComp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Adj B} (x : a ⟶ b) (x_1 : b ⟶ c),
  CategoryTheory.Bicategory.Adj.forget₁.mapComp x x_1 =
    CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp x x_1).l
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftEval.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ)
  (hi : n + i = i'), CochainComplex.shiftEval C n i i' hi = CochainComplex.shiftEval C n i i' hi
-- Std.Do.WP.Sound
/-- A `wp`-provable postcondition refines `x` via `Internal.Ensures`.  -/
Std.Do.WPSound.ensures_of_wp : ∀ {m : Type u → Type v} {ps : outParam Std.Do.PostShape} {inst : Monad m} {inst_1 : Std.Do.WP m ps}
  [self : Std.Do.WPSound m ps] {α : Type u} {x : m α} {P : α → Prop},
  (⊢ₛ (Std.Do.wp x).apply (Std.Do.PostCond.mayThrow fun a => ⌜P a⌝)) → Std.Do.Internal.Ensures P x
-- Lean.Parser.Term
/-- `+postponeValue` causes the body of the `let` to be elaborated before the value.
 -/
Lean.Parser.Term.letOptPostponeValue : Lean.Parser.Parser
-- Mathlib.Topology.Separation.Regular
T25Space.mk : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ ⦃x y : X⦄, x ≠ y → Disjoint ((nhds x).lift' closure) ((nhds y).lift' closure)) → T25Space X
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.coconeTypes_pt : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w₀)),
  F.coconeTypes.pt = F.ColimitType
-- Mathlib.Topology.MetricSpace.DilationEquiv
/-- Type of equivalences `X ≃ Y` such that `∀ x y, edist (f x) (f y) = r * edist x y` for some
`r : ℝ≥0`, `r ≠ 0`.  -/
«term_≃ᵈ_» : Lean.TrailingParserDescr
-- Init.Data.Option.Lemmas
Option.isSome_ite : ∀ {α : Type u_1} {b : α} {p : Prop} {x : Decidable p}, (if p then some b else none).isSome = true ↔ p
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits, then `F.unop : C ⥤ D` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimitsOfSize_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {k : α}, (t.erase k)[k]! = default
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_smul_closedBall : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ),
  (fun x => c • x) ⁻¹' Metric.closedBall x r = Metric.closedBall (c⁻¹ • x) r
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.toIdeal_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).toIdeal = ⨆ i, Ideal.span (⇑(GradedRing.proj 𝒜 i) '' ↑I)
-- Lean.Linter.Init
/-- Return the set of linter sets that this option is contained in.  -/
Lean.Linter.LinterOptions.getSet : {α : Type} → Lean.Linter.LinterOptions → Lean.Option α → Array Lean.Name
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.pairwise_toList_le : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [LT α] [inst_3 : Std.PRange.UpwardEnumerable α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_6 : Std.Rxc.IsAlwaysFinite α], List.Pairwise (fun a b => a ≤ b) r.toList
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.idealFactorsFunOfQuotHom_comp`. -/
idealFactorsFunOfQuotHom_comp : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} {B : Type u_4} [inst_3 : CommRing B] [inst_4 : IsDedekindDomain B] {L : Ideal B} {f : R ⧸ I →+* A ⧸ J}
  {g : A ⧸ J →+* B ⧸ L} (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g),
  (IsDedekindDomain.idealFactorsFunOfQuotHom hg).comp (IsDedekindDomain.idealFactorsFunOfQuotHom hf) =
    IsDedekindDomain.idealFactorsFunOfQuotHom ⋯
-- Init.Omega.IntList
Lean.Omega.IntList.nil_dot : ∀ (xs : Lean.Omega.IntList), Lean.Omega.IntList.dot [] xs = 0
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
_private.Mathlib.CategoryTheory.Bicategory.InducedBicategory.0.CategoryTheory.Bicategory.InducedBicategory.Hom.mk.injEq : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} (hom hom_1 : F X ⟶ F Y),
  ({ hom := hom } = { hom := hom_1 }) = (hom = hom_1)
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpaceCore.open_source : ∀ {H : Type u_5} [inst : TopologicalSpace H] {M : Type u_6} (self : ChartedSpaceCore H M) (e e' : PartialEquiv M H),
  e ∈ self.atlas → e' ∈ self.atlas → IsOpen (e.symm.trans e').source
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.fst_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : NonUnitalNonAssocSemiring C]
  [inst_8 : DistribMulAction R C] [inst_9 : Star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C),
  (NonUnitalStarAlgHom.fst R B C).comp (f.prod g) = f
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_subset_edgeSet : ∀ {V : Type u} {G₁ G₂ : SimpleGraph V}, G₁.edgeSet ⊆ G₂.edgeSet ↔ G₁ ≤ G₂
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.Hom.ext_iff : ∀ {X Y : FinBddDistLat} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.minpoly_coe : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.RingOfIntegers K), minpoly ℤ ↑x = minpoly ℤ x
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Lean.Omega.tidy?.match_1.splitter : (motive : Option (Lean.Omega.Constraint × Lean.Omega.Coeffs) → Sort u_1) →
  (x : Option (Lean.Omega.Constraint × Lean.Omega.Coeffs)) →
    (Unit → motive none) → ((s' : Lean.Omega.Constraint) → (x' : Lean.Omega.Coeffs) → motive (some (s', x'))) → motive x
-- Mathlib.Order.KrullDimension
Order.krullDim_le_of_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  StrictMono f → Order.krullDim α ≤ Order.krullDim β
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.Infinite.st_eq : ∀ {x : ℝ*}, x.Infinite → x.st = 0
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.principals_map : ∀ (X : Type v) [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] {x y : X} (f : x ⟶ y),
  (Alexandrov.principals X).map f = ⋯.hom.op
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {old : Std.Sat.AIG α} [inst_2 : SizeOf α]
  (aig : Std.Sat.AIG α) (out cout : aig.Ref) (hle : old.decls.size ≤ aig.decls.size),
  sizeOf { aig := aig, out := out, cout := cout, hle := hle } = 1 + sizeOf aig + sizeOf out + sizeOf cout + sizeOf hle
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- If `f` is `C^n` then its `m`-times iterated derivative is differentiable for `m < n`.  -/
ContDiff.differentiable_iteratedFDeriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {m : ℕ}, ↑m < n → ContDiff 𝕜 n f → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.image_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} [inst_1 : CategoryTheory.Limits.HasImages C]
  {f g : CategoryTheory.Over X} (k : f ⟶ g),
  CategoryTheory.MonoOver.image.map k =
    (CategoryTheory.MonoOver.forget X).preimage
      (CategoryTheory.Over.homMk
        (CategoryTheory.Limits.image.lift
          { I := CategoryTheory.Limits.image g.hom, m := CategoryTheory.Limits.image.ι g.hom, m_mono := ⋯,
            e :=
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left k)
                (CategoryTheory.Limits.factorThruImage g.hom),
            fac := ⋯ })
        ⋯)
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- `minSmoothness 𝕜 n` is the minimal smoothness exponent larger than or equal to `n` for which
one can do serious calculus in `𝕜`. If `𝕜` is `ℝ` or `ℂ`, this is just `n`. Otherwise,
this is `ω` as only analytic functions are well behaved on `ℚₚ`, say.  -/
minSmoothness : (𝕜 : Type u_4) → [NontriviallyNormedField 𝕜] → WithTop ℕ∞ → WithTop ℕ∞
-- Aesop.Stats.Basic
Aesop.RuleStats.elapsed : Aesop.RuleStats → Aesop.Nanos
-- Mathlib.Algebra.MonoidAlgebra.Lift
MonoidAlgebra.liftNC_mul : ∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : Semiring R]
  {g_hom : Type u_6} [inst_3 : FunLike g_hom G R] [MulHomClass g_hom G R] (f : k →+* R) (g : g_hom)
  (a b : MonoidAlgebra k G),
  (∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g y)) →
    (MonoidAlgebra.liftNC ↑f ⇑g) (a * b) = (MonoidAlgebra.liftNC ↑f ⇑g) a * (MonoidAlgebra.liftNC ↑f ⇑g) b
-- Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
PiTensorProduct.ofDFinsuppEquiv_tprod_apply : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] [inst_5 : (i : ι) → DecidableEq (κ i)]
  (x : (i : ι) → Π₀ (j : κ i), M i j) (p : (i : ι) → κ i),
  (PiTensorProduct.ofDFinsuppEquiv ((PiTensorProduct.tprod R) x)) p = (PiTensorProduct.tprod R) fun i => (x i) (p i)
-- Aesop.Forward.Substitution
/-- Given `e` with type `∀ (x₁ : T₁) ... (xₙ : Tₙ), U` and a substitution `σ`
for the arguments `xᵢ`, replace occurrences of `xᵢ` in the body `U` with fresh
metavariables (like `forallMetaTelescope`). Then, for each mapping `xᵢ ↦ tᵢ` in
`σ`, assign `tᵢ` to the metavariable corresponding to `xᵢ`. Returns the newly
created metavariables (which may be assigned!), their binder infos and the
updated body.  -/
Aesop.Substitution.openRuleType : Lean.Expr → Aesop.Substitution → Lean.MetaM (Array Lean.MVarId × Array Lean.BinderInfo × Lean.Expr)
-- Lean.ExtraModUses
Lean.ExtraModUse.mk.injEq : ∀ (module : Lean.Name) (isExported isMeta : Bool) (module_1 : Lean.Name) (isExported_1 isMeta_1 : Bool),
  ({ module := module, isExported := isExported, isMeta := isMeta } =
      { module := module_1, isExported := isExported_1, isMeta := isMeta_1 }) =
    (module = module_1 ∧ isExported = isExported_1 ∧ isMeta = isMeta_1)
-- Mathlib.Topology.Algebra.RestrictedProduct.Units
RestrictedProduct.unitsEquiv_apply : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → Monoid (R i)] {S : ι → Type u_3}
  [inst_1 : (i : ι) → SetLike (S i) (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i}
  {𝓕 : Filter ι} (i : ι) (x : (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)ˣ),
  ↑(((RestrictedProduct.unitsEquiv R) x) i) = ↑x i
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.length_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.isMaximal_def : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I.IsMaximal ↔ IsCoatom I
-- Batteries.Classes.Order
Std.LawfulBCmp.toLawfulBEqCmp : ∀ {α : Type u_1} {inst : LE α} {inst_1 : LT α} {inst_2 : BEq α} {cmp : α → α → Ordering} [self : Std.LawfulBCmp cmp],
  Std.LawfulBEqCmp cmp
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_left_le_size_union! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₁.size ≤ (m₁.union! m₂).size
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_of_contains_insertManyIfNewUnit!_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List α} {k : α},
      l.contains k = false →
        Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l) = true →
          Std.DTreeMap.Internal.Impl.contains k t = true
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instCoeToLp : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            [inst_4 : MeasurableSpace E] →
              [OpensMeasurableSpace E] →
                [SecondCountableTopologyEither E F] →
                  {p : ENNReal} →
                    {μ : MeasureTheory.Measure E} →
                      [hμ : μ.HasTemperateGrowth] → Coe (SchwartzMap E F) ↥(MeasureTheory.Lp F p μ)